{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wno-overlapping-patterns #-}

module MAlonzo.Code.Algebra.Lattice.Properties.Semilattice where

import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
                    quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
                    rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Algebra.Lattice.Bundles
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.Construct.NaturalOrder.Left
import qualified MAlonzo.Code.Relation.Binary.Lattice.Bundles
import qualified MAlonzo.Code.Relation.Binary.Lattice.Structures
import qualified MAlonzo.Code.Relation.Binary.Properties.Poset

-- Algebra.Lattice.Properties.Semilattice.poset
d_poset_162 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492
d_poset_162 :: T_Level_18 -> T_Level_18 -> T_Semilattice_10 -> T_Poset_492
d_poset_162 ~T_Level_18
v0 ~T_Level_18
v1 T_Semilattice_10
v2 = T_Semilattice_10 -> T_Poset_492
du_poset_162 T_Semilattice_10
v2
du_poset_162 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492
du_poset_162 :: T_Semilattice_10 -> T_Poset_492
du_poset_162 T_Semilattice_10
v0
  = ((Any -> Any -> Any) -> T_IsCommutativeBand_612 -> T_Poset_492)
-> Any -> Any -> T_Poset_492
forall a b. a -> b
coe
      (Any -> Any -> Any) -> T_IsCommutativeBand_612 -> T_Poset_492
MAlonzo.Code.Relation.Binary.Construct.NaturalOrder.Left.du_poset_3898
      ((T_Semilattice_10 -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Semilattice_10 -> Any -> Any -> Any
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8729'__28 (T_Semilattice_10 -> Any
forall a b. a -> b
coe T_Semilattice_10
v0))
      ((T_Semilattice_10 -> T_IsCommutativeBand_612) -> Any -> Any
forall a b. a -> b
coe
         T_Semilattice_10 -> T_IsCommutativeBand_612
MAlonzo.Code.Algebra.Lattice.Bundles.d_isSemilattice_30 (T_Semilattice_10 -> Any
forall a b. a -> b
coe T_Semilattice_10
v0))
-- Algebra.Lattice.Properties.Semilattice._._≤_
d__'8804'__166 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10 ->
  AgdaAny -> AgdaAny -> ()
d__'8804'__166 :: T_Level_18
-> T_Level_18 -> T_Semilattice_10 -> Any -> Any -> T_Level_18
d__'8804'__166 = T_Level_18
-> T_Level_18 -> T_Semilattice_10 -> Any -> Any -> T_Level_18
forall a. a
erased
-- Algebra.Lattice.Properties.Semilattice._._∼ᵒ_
d__'8764''7506'__168 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10 ->
  AgdaAny -> AgdaAny -> ()
d__'8764''7506'__168 :: T_Level_18
-> T_Level_18 -> T_Semilattice_10 -> Any -> Any -> T_Level_18
d__'8764''7506'__168 = T_Level_18
-> T_Level_18 -> T_Semilattice_10 -> Any -> Any -> T_Level_18
forall a. a
erased
-- Algebra.Lattice.Properties.Semilattice.∧-isOrderTheoreticMeetSemilattice
d_'8743''45'isOrderTheoreticMeetSemilattice_176 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10 ->
  MAlonzo.Code.Relation.Binary.Lattice.Structures.T_IsMeetSemilattice_184
d_'8743''45'isOrderTheoreticMeetSemilattice_176 :: T_Level_18
-> T_Level_18 -> T_Semilattice_10 -> T_IsMeetSemilattice_184
d_'8743''45'isOrderTheoreticMeetSemilattice_176 ~T_Level_18
v0 ~T_Level_18
v1 T_Semilattice_10
v2
  = T_Semilattice_10 -> T_IsMeetSemilattice_184
du_'8743''45'isOrderTheoreticMeetSemilattice_176 T_Semilattice_10
v2
du_'8743''45'isOrderTheoreticMeetSemilattice_176 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10 ->
  MAlonzo.Code.Relation.Binary.Lattice.Structures.T_IsMeetSemilattice_184
du_'8743''45'isOrderTheoreticMeetSemilattice_176 :: T_Semilattice_10 -> T_IsMeetSemilattice_184
du_'8743''45'isOrderTheoreticMeetSemilattice_176 T_Semilattice_10
v0
  = (T_IsPartialOrder_248
 -> (Any -> Any -> T_Σ_14) -> T_IsMeetSemilattice_184)
-> Any -> Any -> T_IsMeetSemilattice_184
forall a b. a -> b
coe
      T_IsPartialOrder_248
-> (Any -> Any -> T_Σ_14) -> T_IsMeetSemilattice_184
MAlonzo.Code.Relation.Binary.Lattice.Structures.C_constructor_274
      ((T_Poset_492 -> T_IsPartialOrder_248) -> Any -> Any
forall a b. a -> b
coe
         T_Poset_492 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_514
         ((T_Semilattice_10 -> T_Poset_492) -> Any -> Any
forall a b. a -> b
coe T_Semilattice_10 -> T_Poset_492
du_poset_162 (T_Semilattice_10 -> Any
forall a b. a -> b
coe T_Semilattice_10
v0)))
      (((Any -> Any -> Any)
 -> T_IsCommutativeBand_612 -> Any -> Any -> T_Σ_14)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any -> Any)
-> T_IsCommutativeBand_612 -> Any -> Any -> T_Σ_14
MAlonzo.Code.Relation.Binary.Construct.NaturalOrder.Left.du_infimum_3754
         ((T_Semilattice_10 -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Semilattice_10 -> Any -> Any -> Any
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8729'__28 (T_Semilattice_10 -> Any
forall a b. a -> b
coe T_Semilattice_10
v0))
         ((T_Semilattice_10 -> T_IsCommutativeBand_612) -> Any -> Any
forall a b. a -> b
coe
            T_Semilattice_10 -> T_IsCommutativeBand_612
MAlonzo.Code.Algebra.Lattice.Bundles.d_isSemilattice_30 (T_Semilattice_10 -> Any
forall a b. a -> b
coe T_Semilattice_10
v0)))
-- Algebra.Lattice.Properties.Semilattice.∧-isOrderTheoreticJoinSemilattice
d_'8743''45'isOrderTheoreticJoinSemilattice_178 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10 ->
  MAlonzo.Code.Relation.Binary.Lattice.Structures.T_IsJoinSemilattice_22
d_'8743''45'isOrderTheoreticJoinSemilattice_178 :: T_Level_18
-> T_Level_18 -> T_Semilattice_10 -> T_IsJoinSemilattice_22
d_'8743''45'isOrderTheoreticJoinSemilattice_178 ~T_Level_18
v0 ~T_Level_18
v1 T_Semilattice_10
v2
  = T_Semilattice_10 -> T_IsJoinSemilattice_22
du_'8743''45'isOrderTheoreticJoinSemilattice_178 T_Semilattice_10
v2
du_'8743''45'isOrderTheoreticJoinSemilattice_178 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10 ->
  MAlonzo.Code.Relation.Binary.Lattice.Structures.T_IsJoinSemilattice_22
du_'8743''45'isOrderTheoreticJoinSemilattice_178 :: T_Semilattice_10 -> T_IsJoinSemilattice_22
du_'8743''45'isOrderTheoreticJoinSemilattice_178 T_Semilattice_10
v0
  = (T_IsPartialOrder_248
 -> (Any -> Any -> T_Σ_14) -> T_IsJoinSemilattice_22)
-> Any -> Any -> T_IsJoinSemilattice_22
forall a b. a -> b
coe
      T_IsPartialOrder_248
-> (Any -> Any -> T_Σ_14) -> T_IsJoinSemilattice_22
MAlonzo.Code.Relation.Binary.Lattice.Structures.C_constructor_112
      ((T_Poset_492 -> T_IsPartialOrder_248) -> Any -> Any
forall a b. a -> b
coe
         T_Poset_492 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Properties.Poset.du_'8805''45'isPartialOrder_150
         ((T_Semilattice_10 -> T_Poset_492) -> Any -> Any
forall a b. a -> b
coe T_Semilattice_10 -> T_Poset_492
du_poset_162 (T_Semilattice_10 -> Any
forall a b. a -> b
coe T_Semilattice_10
v0)))
      (((Any -> Any -> Any)
 -> T_IsCommutativeBand_612 -> Any -> Any -> T_Σ_14)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any -> Any)
-> T_IsCommutativeBand_612 -> Any -> Any -> T_Σ_14
MAlonzo.Code.Relation.Binary.Construct.NaturalOrder.Left.du_infimum_3754
         ((T_Semilattice_10 -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Semilattice_10 -> Any -> Any -> Any
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8729'__28 (T_Semilattice_10 -> Any
forall a b. a -> b
coe T_Semilattice_10
v0))
         ((T_Semilattice_10 -> T_IsCommutativeBand_612) -> Any -> Any
forall a b. a -> b
coe
            T_Semilattice_10 -> T_IsCommutativeBand_612
MAlonzo.Code.Algebra.Lattice.Bundles.d_isSemilattice_30 (T_Semilattice_10 -> Any
forall a b. a -> b
coe T_Semilattice_10
v0)))
-- Algebra.Lattice.Properties.Semilattice.∧-orderTheoreticMeetSemilattice
d_'8743''45'orderTheoreticMeetSemilattice_180 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10 ->
  MAlonzo.Code.Relation.Binary.Lattice.Bundles.T_MeetSemilattice_204
d_'8743''45'orderTheoreticMeetSemilattice_180 :: T_Level_18
-> T_Level_18 -> T_Semilattice_10 -> T_MeetSemilattice_204
d_'8743''45'orderTheoreticMeetSemilattice_180 ~T_Level_18
v0 ~T_Level_18
v1 T_Semilattice_10
v2
  = T_Semilattice_10 -> T_MeetSemilattice_204
du_'8743''45'orderTheoreticMeetSemilattice_180 T_Semilattice_10
v2
du_'8743''45'orderTheoreticMeetSemilattice_180 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10 ->
  MAlonzo.Code.Relation.Binary.Lattice.Bundles.T_MeetSemilattice_204
du_'8743''45'orderTheoreticMeetSemilattice_180 :: T_Semilattice_10 -> T_MeetSemilattice_204
du_'8743''45'orderTheoreticMeetSemilattice_180 T_Semilattice_10
v0
  = ((Any -> Any -> Any)
 -> T_IsMeetSemilattice_184 -> T_MeetSemilattice_204)
-> (Any -> Any -> Any) -> Any -> T_MeetSemilattice_204
forall a b. a -> b
coe
      (Any -> Any -> Any)
-> T_IsMeetSemilattice_184 -> T_MeetSemilattice_204
MAlonzo.Code.Relation.Binary.Lattice.Bundles.C_constructor_286
      (T_Semilattice_10 -> Any -> Any -> Any
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8729'__28 (T_Semilattice_10 -> T_Semilattice_10
forall a b. a -> b
coe T_Semilattice_10
v0))
      ((T_Semilattice_10 -> T_IsMeetSemilattice_184) -> Any -> Any
forall a b. a -> b
coe T_Semilattice_10 -> T_IsMeetSemilattice_184
du_'8743''45'isOrderTheoreticMeetSemilattice_176 (T_Semilattice_10 -> Any
forall a b. a -> b
coe T_Semilattice_10
v0))
-- Algebra.Lattice.Properties.Semilattice.∧-orderTheoreticJoinSemilattice
d_'8743''45'orderTheoreticJoinSemilattice_182 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10 ->
  MAlonzo.Code.Relation.Binary.Lattice.Bundles.T_JoinSemilattice_14
d_'8743''45'orderTheoreticJoinSemilattice_182 :: T_Level_18
-> T_Level_18 -> T_Semilattice_10 -> T_JoinSemilattice_14
d_'8743''45'orderTheoreticJoinSemilattice_182 ~T_Level_18
v0 ~T_Level_18
v1 T_Semilattice_10
v2
  = T_Semilattice_10 -> T_JoinSemilattice_14
du_'8743''45'orderTheoreticJoinSemilattice_182 T_Semilattice_10
v2
du_'8743''45'orderTheoreticJoinSemilattice_182 ::
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10 ->
  MAlonzo.Code.Relation.Binary.Lattice.Bundles.T_JoinSemilattice_14
du_'8743''45'orderTheoreticJoinSemilattice_182 :: T_Semilattice_10 -> T_JoinSemilattice_14
du_'8743''45'orderTheoreticJoinSemilattice_182 T_Semilattice_10
v0
  = ((Any -> Any -> Any)
 -> T_IsJoinSemilattice_22 -> T_JoinSemilattice_14)
-> (Any -> Any -> Any) -> Any -> T_JoinSemilattice_14
forall a b. a -> b
coe
      (Any -> Any -> Any)
-> T_IsJoinSemilattice_22 -> T_JoinSemilattice_14
MAlonzo.Code.Relation.Binary.Lattice.Bundles.C_constructor_96
      (T_Semilattice_10 -> Any -> Any -> Any
MAlonzo.Code.Algebra.Lattice.Bundles.d__'8729'__28 (T_Semilattice_10 -> T_Semilattice_10
forall a b. a -> b
coe T_Semilattice_10
v0))
      ((T_Semilattice_10 -> T_IsJoinSemilattice_22) -> Any -> Any
forall a b. a -> b
coe T_Semilattice_10 -> T_IsJoinSemilattice_22
du_'8743''45'isOrderTheoreticJoinSemilattice_178 (T_Semilattice_10 -> Any
forall a b. a -> b
coe T_Semilattice_10
v0))