{-# 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.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.Bundles
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.Construct.NaturalOrder.Left
import qualified MAlonzo.Code.Relation.Binary.Lattice
import qualified MAlonzo.Code.Relation.Binary.Properties.Poset

-- Algebra.Properties.Semilattice.poset
d_poset_162 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Semilattice_402 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282
d_poset_162 :: T_Level_18 -> T_Level_18 -> T_Semilattice_402 -> T_Poset_282
d_poset_162 ~T_Level_18
v0 ~T_Level_18
v1 T_Semilattice_402
v2 = T_Semilattice_402 -> T_Poset_282
du_poset_162 T_Semilattice_402
v2
du_poset_162 ::
  MAlonzo.Code.Algebra.Bundles.T_Semilattice_402 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282
du_poset_162 :: T_Semilattice_402 -> T_Poset_282
du_poset_162 T_Semilattice_402
v0
  = ((Any -> Any -> Any) -> T_IsSemilattice_312 -> T_Poset_282)
-> Any -> Any -> T_Poset_282
forall a b. a -> b
coe
      (Any -> Any -> Any) -> T_IsSemilattice_312 -> T_Poset_282
MAlonzo.Code.Relation.Binary.Construct.NaturalOrder.Left.du_poset_2146
      ((T_Semilattice_402 -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Semilattice_402 -> Any -> Any -> Any
MAlonzo.Code.Algebra.Bundles.d__'8743'__420 (T_Semilattice_402 -> Any
forall a b. a -> b
coe T_Semilattice_402
v0))
      ((T_Semilattice_402 -> T_IsSemilattice_312) -> Any -> Any
forall a b. a -> b
coe T_Semilattice_402 -> T_IsSemilattice_312
MAlonzo.Code.Algebra.Bundles.d_isSemilattice_422 (T_Semilattice_402 -> Any
forall a b. a -> b
coe T_Semilattice_402
v0))
-- Algebra.Properties.Semilattice._._≤_
d__'8804'__166 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Semilattice_402 ->
  AgdaAny -> AgdaAny -> ()
d__'8804'__166 :: T_Level_18
-> T_Level_18 -> T_Semilattice_402 -> Any -> Any -> T_Level_18
d__'8804'__166 = T_Level_18
-> T_Level_18 -> T_Semilattice_402 -> Any -> Any -> T_Level_18
forall a. a
erased
-- Algebra.Properties.Semilattice._._≥_
d__'8805'__172 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Semilattice_402 ->
  AgdaAny -> AgdaAny -> ()
d__'8805'__172 :: T_Level_18
-> T_Level_18 -> T_Semilattice_402 -> Any -> Any -> T_Level_18
d__'8805'__172 = T_Level_18
-> T_Level_18 -> T_Semilattice_402 -> Any -> Any -> T_Level_18
forall a. a
erased
-- Algebra.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.Bundles.T_Semilattice_402 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_IsMeetSemilattice_438
d_'8743''45'isOrderTheoreticMeetSemilattice_176 :: T_Level_18
-> T_Level_18 -> T_Semilattice_402 -> T_IsMeetSemilattice_438
d_'8743''45'isOrderTheoreticMeetSemilattice_176 ~T_Level_18
v0 ~T_Level_18
v1 T_Semilattice_402
v2
  = T_Semilattice_402 -> T_IsMeetSemilattice_438
du_'8743''45'isOrderTheoreticMeetSemilattice_176 T_Semilattice_402
v2
du_'8743''45'isOrderTheoreticMeetSemilattice_176 ::
  MAlonzo.Code.Algebra.Bundles.T_Semilattice_402 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_IsMeetSemilattice_438
du_'8743''45'isOrderTheoreticMeetSemilattice_176 :: T_Semilattice_402 -> T_IsMeetSemilattice_438
du_'8743''45'isOrderTheoreticMeetSemilattice_176 T_Semilattice_402
v0
  = (T_IsPartialOrder_162
 -> (Any -> Any -> T_Σ_14) -> T_IsMeetSemilattice_438)
-> Any -> Any -> T_IsMeetSemilattice_438
forall a b. a -> b
coe
      T_IsPartialOrder_162
-> (Any -> Any -> T_Σ_14) -> T_IsMeetSemilattice_438
MAlonzo.Code.Relation.Binary.Lattice.C_IsMeetSemilattice'46'constructor_13939
      ((T_Poset_282 -> T_IsPartialOrder_162) -> Any -> Any
forall a b. a -> b
coe
         T_Poset_282 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_304
         ((T_Semilattice_402 -> T_Poset_282) -> Any -> Any
forall a b. a -> b
coe T_Semilattice_402 -> T_Poset_282
du_poset_162 (T_Semilattice_402 -> Any
forall a b. a -> b
coe T_Semilattice_402
v0)))
      (((Any -> Any -> Any)
 -> T_IsSemilattice_312 -> Any -> Any -> T_Σ_14)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any -> Any) -> T_IsSemilattice_312 -> Any -> Any -> T_Σ_14
MAlonzo.Code.Relation.Binary.Construct.NaturalOrder.Left.du_infimum_2002
         ((T_Semilattice_402 -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Semilattice_402 -> Any -> Any -> Any
MAlonzo.Code.Algebra.Bundles.d__'8743'__420 (T_Semilattice_402 -> Any
forall a b. a -> b
coe T_Semilattice_402
v0))
         ((T_Semilattice_402 -> T_IsSemilattice_312) -> Any -> Any
forall a b. a -> b
coe T_Semilattice_402 -> T_IsSemilattice_312
MAlonzo.Code.Algebra.Bundles.d_isSemilattice_422 (T_Semilattice_402 -> Any
forall a b. a -> b
coe T_Semilattice_402
v0)))
-- Algebra.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.Bundles.T_Semilattice_402 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_IsJoinSemilattice_68
d_'8743''45'isOrderTheoreticJoinSemilattice_178 :: T_Level_18
-> T_Level_18 -> T_Semilattice_402 -> T_IsJoinSemilattice_68
d_'8743''45'isOrderTheoreticJoinSemilattice_178 ~T_Level_18
v0 ~T_Level_18
v1 T_Semilattice_402
v2
  = T_Semilattice_402 -> T_IsJoinSemilattice_68
du_'8743''45'isOrderTheoreticJoinSemilattice_178 T_Semilattice_402
v2
du_'8743''45'isOrderTheoreticJoinSemilattice_178 ::
  MAlonzo.Code.Algebra.Bundles.T_Semilattice_402 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_IsJoinSemilattice_68
du_'8743''45'isOrderTheoreticJoinSemilattice_178 :: T_Semilattice_402 -> T_IsJoinSemilattice_68
du_'8743''45'isOrderTheoreticJoinSemilattice_178 T_Semilattice_402
v0
  = (T_IsPartialOrder_162
 -> (Any -> Any -> T_Σ_14) -> T_IsJoinSemilattice_68)
-> Any -> Any -> T_IsJoinSemilattice_68
forall a b. a -> b
coe
      T_IsPartialOrder_162
-> (Any -> Any -> T_Σ_14) -> T_IsJoinSemilattice_68
MAlonzo.Code.Relation.Binary.Lattice.C_IsJoinSemilattice'46'constructor_2281
      ((T_Poset_282 -> T_IsPartialOrder_162) -> Any -> Any
forall a b. a -> b
coe
         T_Poset_282 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Properties.Poset.du_'8805''45'isPartialOrder_146
         ((T_Semilattice_402 -> T_Poset_282) -> Any -> Any
forall a b. a -> b
coe T_Semilattice_402 -> T_Poset_282
du_poset_162 (T_Semilattice_402 -> Any
forall a b. a -> b
coe T_Semilattice_402
v0)))
      (((Any -> Any -> Any)
 -> T_IsSemilattice_312 -> Any -> Any -> T_Σ_14)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any -> Any) -> T_IsSemilattice_312 -> Any -> Any -> T_Σ_14
MAlonzo.Code.Relation.Binary.Construct.NaturalOrder.Left.du_infimum_2002
         ((T_Semilattice_402 -> Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Semilattice_402 -> Any -> Any -> Any
MAlonzo.Code.Algebra.Bundles.d__'8743'__420 (T_Semilattice_402 -> Any
forall a b. a -> b
coe T_Semilattice_402
v0))
         ((T_Semilattice_402 -> T_IsSemilattice_312) -> Any -> Any
forall a b. a -> b
coe T_Semilattice_402 -> T_IsSemilattice_312
MAlonzo.Code.Algebra.Bundles.d_isSemilattice_422 (T_Semilattice_402 -> Any
forall a b. a -> b
coe T_Semilattice_402
v0)))
-- Algebra.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.Bundles.T_Semilattice_402 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_MeetSemilattice_540
d_'8743''45'orderTheoreticMeetSemilattice_180 :: T_Level_18
-> T_Level_18 -> T_Semilattice_402 -> T_MeetSemilattice_540
d_'8743''45'orderTheoreticMeetSemilattice_180 ~T_Level_18
v0 ~T_Level_18
v1 T_Semilattice_402
v2
  = T_Semilattice_402 -> T_MeetSemilattice_540
du_'8743''45'orderTheoreticMeetSemilattice_180 T_Semilattice_402
v2
du_'8743''45'orderTheoreticMeetSemilattice_180 ::
  MAlonzo.Code.Algebra.Bundles.T_Semilattice_402 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_MeetSemilattice_540
du_'8743''45'orderTheoreticMeetSemilattice_180 :: T_Semilattice_402 -> T_MeetSemilattice_540
du_'8743''45'orderTheoreticMeetSemilattice_180 T_Semilattice_402
v0
  = ((Any -> Any -> Any)
 -> T_IsMeetSemilattice_438 -> T_MeetSemilattice_540)
-> (Any -> Any -> Any) -> Any -> T_MeetSemilattice_540
forall a b. a -> b
coe
      (Any -> Any -> Any)
-> T_IsMeetSemilattice_438 -> T_MeetSemilattice_540
MAlonzo.Code.Relation.Binary.Lattice.C_MeetSemilattice'46'constructor_18685
      (T_Semilattice_402 -> Any -> Any -> Any
MAlonzo.Code.Algebra.Bundles.d__'8743'__420 (T_Semilattice_402 -> T_Semilattice_402
forall a b. a -> b
coe T_Semilattice_402
v0))
      ((T_Semilattice_402 -> T_IsMeetSemilattice_438) -> Any -> Any
forall a b. a -> b
coe T_Semilattice_402 -> T_IsMeetSemilattice_438
du_'8743''45'isOrderTheoreticMeetSemilattice_176 (T_Semilattice_402 -> Any
forall a b. a -> b
coe T_Semilattice_402
v0))
-- Algebra.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.Bundles.T_Semilattice_402 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_JoinSemilattice_170
d_'8743''45'orderTheoreticJoinSemilattice_182 :: T_Level_18
-> T_Level_18 -> T_Semilattice_402 -> T_JoinSemilattice_170
d_'8743''45'orderTheoreticJoinSemilattice_182 ~T_Level_18
v0 ~T_Level_18
v1 T_Semilattice_402
v2
  = T_Semilattice_402 -> T_JoinSemilattice_170
du_'8743''45'orderTheoreticJoinSemilattice_182 T_Semilattice_402
v2
du_'8743''45'orderTheoreticJoinSemilattice_182 ::
  MAlonzo.Code.Algebra.Bundles.T_Semilattice_402 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_JoinSemilattice_170
du_'8743''45'orderTheoreticJoinSemilattice_182 :: T_Semilattice_402 -> T_JoinSemilattice_170
du_'8743''45'orderTheoreticJoinSemilattice_182 T_Semilattice_402
v0
  = ((Any -> Any -> Any)
 -> T_IsJoinSemilattice_68 -> T_JoinSemilattice_170)
-> (Any -> Any -> Any) -> Any -> T_JoinSemilattice_170
forall a b. a -> b
coe
      (Any -> Any -> Any)
-> T_IsJoinSemilattice_68 -> T_JoinSemilattice_170
MAlonzo.Code.Relation.Binary.Lattice.C_JoinSemilattice'46'constructor_7027
      (T_Semilattice_402 -> Any -> Any -> Any
MAlonzo.Code.Algebra.Bundles.d__'8743'__420 (T_Semilattice_402 -> T_Semilattice_402
forall a b. a -> b
coe T_Semilattice_402
v0))
      ((T_Semilattice_402 -> T_IsJoinSemilattice_68) -> Any -> Any
forall a b. a -> b
coe T_Semilattice_402 -> T_IsJoinSemilattice_68
du_'8743''45'isOrderTheoreticJoinSemilattice_178 (T_Semilattice_402 -> Any
forall a b. a -> b
coe T_Semilattice_402
v0))
-- Algebra.Properties.Semilattice.isOrderTheoreticMeetSemilattice
d_isOrderTheoreticMeetSemilattice_184 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Semilattice_402 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_IsMeetSemilattice_438
d_isOrderTheoreticMeetSemilattice_184 :: T_Level_18
-> T_Level_18 -> T_Semilattice_402 -> T_IsMeetSemilattice_438
d_isOrderTheoreticMeetSemilattice_184 ~T_Level_18
v0 ~T_Level_18
v1 T_Semilattice_402
v2
  = T_Semilattice_402 -> T_IsMeetSemilattice_438
du_isOrderTheoreticMeetSemilattice_184 T_Semilattice_402
v2
du_isOrderTheoreticMeetSemilattice_184 ::
  MAlonzo.Code.Algebra.Bundles.T_Semilattice_402 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_IsMeetSemilattice_438
du_isOrderTheoreticMeetSemilattice_184 :: T_Semilattice_402 -> T_IsMeetSemilattice_438
du_isOrderTheoreticMeetSemilattice_184 T_Semilattice_402
v0
  = (T_Semilattice_402 -> T_IsMeetSemilattice_438)
-> Any -> T_IsMeetSemilattice_438
forall a b. a -> b
coe T_Semilattice_402 -> T_IsMeetSemilattice_438
du_'8743''45'isOrderTheoreticMeetSemilattice_176 (T_Semilattice_402 -> Any
forall a b. a -> b
coe T_Semilattice_402
v0)
-- Algebra.Properties.Semilattice.isOrderTheoreticJoinSemilattice
d_isOrderTheoreticJoinSemilattice_186 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Semilattice_402 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_IsJoinSemilattice_68
d_isOrderTheoreticJoinSemilattice_186 :: T_Level_18
-> T_Level_18 -> T_Semilattice_402 -> T_IsJoinSemilattice_68
d_isOrderTheoreticJoinSemilattice_186 ~T_Level_18
v0 ~T_Level_18
v1 T_Semilattice_402
v2
  = T_Semilattice_402 -> T_IsJoinSemilattice_68
du_isOrderTheoreticJoinSemilattice_186 T_Semilattice_402
v2
du_isOrderTheoreticJoinSemilattice_186 ::
  MAlonzo.Code.Algebra.Bundles.T_Semilattice_402 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_IsJoinSemilattice_68
du_isOrderTheoreticJoinSemilattice_186 :: T_Semilattice_402 -> T_IsJoinSemilattice_68
du_isOrderTheoreticJoinSemilattice_186 T_Semilattice_402
v0
  = (T_Semilattice_402 -> T_IsJoinSemilattice_68)
-> Any -> T_IsJoinSemilattice_68
forall a b. a -> b
coe T_Semilattice_402 -> T_IsJoinSemilattice_68
du_'8743''45'isOrderTheoreticJoinSemilattice_178 (T_Semilattice_402 -> Any
forall a b. a -> b
coe T_Semilattice_402
v0)
-- Algebra.Properties.Semilattice.orderTheoreticMeetSemilattice
d_orderTheoreticMeetSemilattice_188 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Semilattice_402 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_MeetSemilattice_540
d_orderTheoreticMeetSemilattice_188 :: T_Level_18
-> T_Level_18 -> T_Semilattice_402 -> T_MeetSemilattice_540
d_orderTheoreticMeetSemilattice_188 ~T_Level_18
v0 ~T_Level_18
v1 T_Semilattice_402
v2
  = T_Semilattice_402 -> T_MeetSemilattice_540
du_orderTheoreticMeetSemilattice_188 T_Semilattice_402
v2
du_orderTheoreticMeetSemilattice_188 ::
  MAlonzo.Code.Algebra.Bundles.T_Semilattice_402 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_MeetSemilattice_540
du_orderTheoreticMeetSemilattice_188 :: T_Semilattice_402 -> T_MeetSemilattice_540
du_orderTheoreticMeetSemilattice_188 T_Semilattice_402
v0
  = (T_Semilattice_402 -> T_MeetSemilattice_540)
-> Any -> T_MeetSemilattice_540
forall a b. a -> b
coe T_Semilattice_402 -> T_MeetSemilattice_540
du_'8743''45'orderTheoreticMeetSemilattice_180 (T_Semilattice_402 -> Any
forall a b. a -> b
coe T_Semilattice_402
v0)
-- Algebra.Properties.Semilattice.orderTheoreticJoinSemilattice
d_orderTheoreticJoinSemilattice_190 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Algebra.Bundles.T_Semilattice_402 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_JoinSemilattice_170
d_orderTheoreticJoinSemilattice_190 :: T_Level_18
-> T_Level_18 -> T_Semilattice_402 -> T_JoinSemilattice_170
d_orderTheoreticJoinSemilattice_190 ~T_Level_18
v0 ~T_Level_18
v1 T_Semilattice_402
v2
  = T_Semilattice_402 -> T_JoinSemilattice_170
du_orderTheoreticJoinSemilattice_190 T_Semilattice_402
v2
du_orderTheoreticJoinSemilattice_190 ::
  MAlonzo.Code.Algebra.Bundles.T_Semilattice_402 ->
  MAlonzo.Code.Relation.Binary.Lattice.T_JoinSemilattice_170
du_orderTheoreticJoinSemilattice_190 :: T_Semilattice_402 -> T_JoinSemilattice_170
du_orderTheoreticJoinSemilattice_190 T_Semilattice_402
v0
  = (T_Semilattice_402 -> T_JoinSemilattice_170)
-> Any -> T_JoinSemilattice_170
forall a b. a -> b
coe T_Semilattice_402 -> T_JoinSemilattice_170
du_'8743''45'orderTheoreticJoinSemilattice_182 (T_Semilattice_402 -> Any
forall a b. a -> b
coe T_Semilattice_402
v0)