{-# 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_314
d_poset_162 :: T_Level_18 -> T_Level_18 -> T_Semilattice_10 -> T_Poset_314
d_poset_162 ~T_Level_18
v0 ~T_Level_18
v1 T_Semilattice_10
v2 = T_Semilattice_10 -> T_Poset_314
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_314
du_poset_162 :: T_Semilattice_10 -> T_Poset_314
du_poset_162 T_Semilattice_10
v0
  = ((Any -> Any -> Any) -> T_IsCommutativeBand_590 -> T_Poset_314)
-> Any -> Any -> T_Poset_314
forall a b. a -> b
coe
      (Any -> Any -> Any) -> T_IsCommutativeBand_590 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Construct.NaturalOrder.Left.du_poset_3784
      ((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_590) -> Any -> Any
forall a b. a -> b
coe
         T_Semilattice_10 -> T_IsCommutativeBand_590
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__'8819'__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__'8819'__168 :: T_Level_18
-> T_Level_18 -> T_Semilattice_10 -> Any -> Any -> T_Level_18
d__'8819'__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_180
d_'8743''45'isOrderTheoreticMeetSemilattice_176 :: T_Level_18
-> T_Level_18 -> T_Semilattice_10 -> T_IsMeetSemilattice_180
d_'8743''45'isOrderTheoreticMeetSemilattice_176 ~T_Level_18
v0 ~T_Level_18
v1 T_Semilattice_10
v2
  = T_Semilattice_10 -> T_IsMeetSemilattice_180
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_180
du_'8743''45'isOrderTheoreticMeetSemilattice_176 :: T_Semilattice_10 -> T_IsMeetSemilattice_180
du_'8743''45'isOrderTheoreticMeetSemilattice_176 T_Semilattice_10
v0
  = (T_IsPartialOrder_174
 -> (Any -> Any -> T_Σ_14) -> T_IsMeetSemilattice_180)
-> Any -> Any -> T_IsMeetSemilattice_180
forall a b. a -> b
coe
      T_IsPartialOrder_174
-> (Any -> Any -> T_Σ_14) -> T_IsMeetSemilattice_180
MAlonzo.Code.Relation.Binary.Lattice.Structures.C_IsMeetSemilattice'46'constructor_7577
      ((T_Poset_314 -> T_IsPartialOrder_174) -> Any -> Any
forall a b. a -> b
coe
         T_Poset_314 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_336
         ((T_Semilattice_10 -> T_Poset_314) -> Any -> Any
forall a b. a -> b
coe T_Semilattice_10 -> T_Poset_314
du_poset_162 (T_Semilattice_10 -> Any
forall a b. a -> b
coe T_Semilattice_10
v0)))
      (((Any -> Any -> Any)
 -> T_IsCommutativeBand_590 -> Any -> Any -> T_Σ_14)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any -> Any)
-> T_IsCommutativeBand_590 -> Any -> Any -> T_Σ_14
MAlonzo.Code.Relation.Binary.Construct.NaturalOrder.Left.du_infimum_3640
         ((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_590) -> Any -> Any
forall a b. a -> b
coe
            T_Semilattice_10 -> T_IsCommutativeBand_590
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_174
 -> (Any -> Any -> T_Σ_14) -> T_IsJoinSemilattice_22)
-> Any -> Any -> T_IsJoinSemilattice_22
forall a b. a -> b
coe
      T_IsPartialOrder_174
-> (Any -> Any -> T_Σ_14) -> T_IsJoinSemilattice_22
MAlonzo.Code.Relation.Binary.Lattice.Structures.C_IsJoinSemilattice'46'constructor_527
      ((T_Poset_314 -> T_IsPartialOrder_174) -> Any -> Any
forall a b. a -> b
coe
         T_Poset_314 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Properties.Poset.du_'8805''45'isPartialOrder_142
         ((T_Semilattice_10 -> T_Poset_314) -> Any -> Any
forall a b. a -> b
coe T_Semilattice_10 -> T_Poset_314
du_poset_162 (T_Semilattice_10 -> Any
forall a b. a -> b
coe T_Semilattice_10
v0)))
      (((Any -> Any -> Any)
 -> T_IsCommutativeBand_590 -> Any -> Any -> T_Σ_14)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any -> Any)
-> T_IsCommutativeBand_590 -> Any -> Any -> T_Σ_14
MAlonzo.Code.Relation.Binary.Construct.NaturalOrder.Left.du_infimum_3640
         ((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_590) -> Any -> Any
forall a b. a -> b
coe
            T_Semilattice_10 -> T_IsCommutativeBand_590
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_200
d_'8743''45'orderTheoreticMeetSemilattice_180 :: T_Level_18
-> T_Level_18 -> T_Semilattice_10 -> T_MeetSemilattice_200
d_'8743''45'orderTheoreticMeetSemilattice_180 ~T_Level_18
v0 ~T_Level_18
v1 T_Semilattice_10
v2
  = T_Semilattice_10 -> T_MeetSemilattice_200
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_200
du_'8743''45'orderTheoreticMeetSemilattice_180 :: T_Semilattice_10 -> T_MeetSemilattice_200
du_'8743''45'orderTheoreticMeetSemilattice_180 T_Semilattice_10
v0
  = ((Any -> Any -> Any)
 -> T_IsMeetSemilattice_180 -> T_MeetSemilattice_200)
-> (Any -> Any -> Any) -> Any -> T_MeetSemilattice_200
forall a b. a -> b
coe
      (Any -> Any -> Any)
-> T_IsMeetSemilattice_180 -> T_MeetSemilattice_200
MAlonzo.Code.Relation.Binary.Lattice.Bundles.C_MeetSemilattice'46'constructor_4629
      (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_180) -> Any -> Any
forall a b. a -> b
coe T_Semilattice_10 -> T_IsMeetSemilattice_180
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_JoinSemilattice'46'constructor_371
      (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))