{-# 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.Relation.Binary.Properties.Preorder 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.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Product
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.Structures

-- Relation.Binary.Properties.Preorder.invIsPreorder
d_invIsPreorder_64 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
d_invIsPreorder_64 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Preorder_132 -> T_IsPreorder_70
d_invIsPreorder_64 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Preorder_132
v3 = T_Preorder_132 -> T_IsPreorder_70
du_invIsPreorder_64 T_Preorder_132
v3
du_invIsPreorder_64 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
du_invIsPreorder_64 :: T_Preorder_132 -> T_IsPreorder_70
du_invIsPreorder_64 T_Preorder_132
v0
  = (T_IsEquivalence_26
 -> (Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any -> Any -> Any)
 -> T_IsPreorder_70)
-> Any -> Any -> Any -> T_IsPreorder_70
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.C_IsPreorder'46'constructor_3993
      ((T_IsPreorder_70 -> T_IsEquivalence_26) -> Any -> Any
forall a b. a -> b
coe
         T_IsPreorder_70 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
         ((T_Preorder_132 -> T_IsPreorder_70) -> Any -> Any
forall a b. a -> b
coe
            T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (T_Preorder_132 -> Any
forall a b. a -> b
coe T_Preorder_132
v0)))
      ((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v1 Any
v2 Any
v3 ->
            (T_IsPreorder_70 -> Any -> Any -> Any -> Any)
-> T_IsPreorder_70 -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
              T_IsPreorder_70 -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Structures.d_reflexive_82
              (T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (T_Preorder_132 -> T_Preorder_132
forall a b. a -> b
coe T_Preorder_132
v0)) Any
v2
              Any
v1
              ((T_IsEquivalence_26 -> Any -> Any -> Any -> Any)
-> T_IsEquivalence_26 -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                 T_IsEquivalence_26 -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
                 (T_IsPreorder_70 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
                    ((T_Preorder_132 -> T_IsPreorder_70) -> Any -> T_IsPreorder_70
forall a b. a -> b
coe
                       T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (T_Preorder_132 -> Any
forall a b. a -> b
coe T_Preorder_132
v0)))
                 Any
v1 Any
v2 Any
v3)))
      ((Any -> Any -> Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v1 Any
v2 Any
v3 Any
v4 Any
v5 ->
            (T_IsPreorder_70 -> Any -> Any -> Any -> Any -> Any -> Any)
-> T_IsPreorder_70 -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
              T_IsPreorder_70 -> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Structures.d_trans_84
              (T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (T_Preorder_132 -> T_Preorder_132
forall a b. a -> b
coe T_Preorder_132
v0)) Any
v3
              Any
v2 Any
v1 Any
v5 Any
v4))
-- Relation.Binary.Properties.Preorder.invPreorder
d_invPreorder_66 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
d_invPreorder_66 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Preorder_132 -> T_Preorder_132
d_invPreorder_66 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Preorder_132
v3 = T_Preorder_132 -> T_Preorder_132
du_invPreorder_66 T_Preorder_132
v3
du_invPreorder_66 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
du_invPreorder_66 :: T_Preorder_132 -> T_Preorder_132
du_invPreorder_66 T_Preorder_132
v0
  = (T_IsPreorder_70 -> T_Preorder_132) -> Any -> T_Preorder_132
forall a b. a -> b
coe
      T_IsPreorder_70 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.C_Preorder'46'constructor_2269
      ((T_Preorder_132 -> T_IsPreorder_70) -> Any -> Any
forall a b. a -> b
coe T_Preorder_132 -> T_IsPreorder_70
du_invIsPreorder_64 (T_Preorder_132 -> Any
forall a b. a -> b
coe T_Preorder_132
v0))
-- Relation.Binary.Properties.Preorder.InducedEquivalence
d_InducedEquivalence_68 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
d_InducedEquivalence_68 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Preorder_132 -> T_Setoid_44
d_InducedEquivalence_68 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Preorder_132
v3
  = T_Preorder_132 -> T_Setoid_44
du_InducedEquivalence_68 T_Preorder_132
v3
du_InducedEquivalence_68 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
du_InducedEquivalence_68 :: T_Preorder_132 -> T_Setoid_44
du_InducedEquivalence_68 T_Preorder_132
v0
  = (T_IsEquivalence_26 -> T_Setoid_44) -> Any -> T_Setoid_44
forall a b. a -> b
coe
      T_IsEquivalence_26 -> T_Setoid_44
MAlonzo.Code.Relation.Binary.Bundles.C_Setoid'46'constructor_727
      (((Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any -> Any -> Any)
 -> T_IsEquivalence_26)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.C_IsEquivalence'46'constructor_743
         ((Any -> Any) -> Any
forall a b. a -> b
coe
            (\ Any
v1 ->
               (Any -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
                 Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                 ((T_IsPreorder_70 -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                    T_IsPreorder_70 -> Any -> Any
MAlonzo.Code.Relation.Binary.Structures.du_refl_98
                    ((T_Preorder_132 -> T_IsPreorder_70) -> Any -> Any
forall a b. a -> b
coe
                       T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (T_Preorder_132 -> Any
forall a b. a -> b
coe T_Preorder_132
v0))
                    (Any -> Any
forall a b. a -> b
coe Any
v1))
                 ((T_IsPreorder_70 -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                    T_IsPreorder_70 -> Any -> Any
MAlonzo.Code.Relation.Binary.Structures.du_refl_98
                    ((T_Preorder_132 -> T_IsPreorder_70) -> Any -> Any
forall a b. a -> b
coe
                       T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (T_Preorder_132 -> Any
forall a b. a -> b
coe T_Preorder_132
v0))
                    (Any -> Any
forall a b. a -> b
coe Any
v1))))
         ((Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v1 Any
v2 -> (T_Σ_14 -> T_Σ_14) -> Any
forall a b. a -> b
coe T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.du_swap_386))
         ((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
            (\ Any
v1 Any
v2 Any
v3 ->
               ((Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any -> Any) -> T_Σ_14 -> T_Σ_14 -> T_Σ_14)
-> Any -> Any -> Any
forall a b. a -> b
coe
                 (Any -> Any -> Any)
-> (Any -> Any -> Any -> Any -> Any) -> T_Σ_14 -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.du_zip_218
                 ((T_IsPreorder_70 -> Any -> Any -> Any -> Any -> Any -> Any)
-> T_IsPreorder_70 -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                    T_IsPreorder_70 -> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Structures.d_trans_84
                    (T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (T_Preorder_132 -> T_Preorder_132
forall a b. a -> b
coe T_Preorder_132
v0)) Any
v1
                    Any
v2 Any
v3)
                 ((Any -> Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
                    (\ Any
v4 Any
v5 Any
v6 Any
v7 ->
                       (T_IsPreorder_70 -> Any -> Any -> Any -> Any -> Any -> Any)
-> T_IsPreorder_70 -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                         T_IsPreorder_70 -> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Structures.d_trans_84
                         (T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (T_Preorder_132 -> T_Preorder_132
forall a b. a -> b
coe T_Preorder_132
v0)) Any
v3
                         Any
v2 Any
v1 Any
v7 Any
v6)))))