{-# 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.Reasoning.Base.Double 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.Bool
import qualified MAlonzo.Code.Agda.Builtin.Equality
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Relation.Binary.Structures
import qualified MAlonzo.Code.Relation.Nullary
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core

-- Relation.Binary.Reasoning.Base.Double._IsRelatedTo_
d__IsRelatedTo__56 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> ()
d__IsRelatedTo__56 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 p
a7 p
a8 = ()
data T__IsRelatedTo__56
  = C_nonstrict_64 AgdaAny | C_equals_68 AgdaAny
-- Relation.Binary.Reasoning.Base.Double.IsEquality
d_IsEquality_74 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> ()
d_IsEquality_74 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 p
a7 p
a8 p
a9 = ()
data T_IsEquality_74 = C_isEquality_82
-- Relation.Binary.Reasoning.Base.Double.IsEquality?
d_IsEquality'63'_90 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny ->
  AgdaAny ->
  T__IsRelatedTo__56 -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d_IsEquality'63'_90 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__56
-> T_Dec_32
d_IsEquality'63'_90 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> AgdaAny -> ()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~T_IsPreorder_70
v6 ~AgdaAny
v7 ~AgdaAny
v8 T__IsRelatedTo__56
v9
  = T__IsRelatedTo__56 -> T_Dec_32
du_IsEquality'63'_90 T__IsRelatedTo__56
v9
du_IsEquality'63'_90 ::
  T__IsRelatedTo__56 -> MAlonzo.Code.Relation.Nullary.T_Dec_32
du_IsEquality'63'_90 :: T__IsRelatedTo__56 -> T_Dec_32
du_IsEquality'63'_90 T__IsRelatedTo__56
v0
  = case T__IsRelatedTo__56 -> T__IsRelatedTo__56
forall a b. a -> b
coe T__IsRelatedTo__56
v0 of
      C_nonstrict_64 AgdaAny
v1
        -> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
             Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
             (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
             (T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
      C_equals_68 AgdaAny
v1
        -> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
             Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
             (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
             ((AgdaAny -> T_Reflects_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                AgdaAny -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'696'_22 (T_IsEquality_74 -> AgdaAny
forall a b. a -> b
coe T_IsEquality_74
C_isEquality_82))
      T__IsRelatedTo__56
_ -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Reasoning.Base.Double.extractEquality
d_extractEquality_100 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny ->
  AgdaAny -> T__IsRelatedTo__56 -> T_IsEquality_74 -> AgdaAny
d_extractEquality_100 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__56
-> T_IsEquality_74
-> AgdaAny
d_extractEquality_100 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> AgdaAny -> ()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~T_IsPreorder_70
v6 ~AgdaAny
v7 ~AgdaAny
v8 T__IsRelatedTo__56
v9 T_IsEquality_74
v10
  = T__IsRelatedTo__56 -> T_IsEquality_74 -> AgdaAny
du_extractEquality_100 T__IsRelatedTo__56
v9 T_IsEquality_74
v10
du_extractEquality_100 ::
  T__IsRelatedTo__56 -> T_IsEquality_74 -> AgdaAny
du_extractEquality_100 :: T__IsRelatedTo__56 -> T_IsEquality_74 -> AgdaAny
du_extractEquality_100 T__IsRelatedTo__56
v0 T_IsEquality_74
v1
  = (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_IsEquality_74 -> AgdaAny
forall a b. a -> b
coe T_IsEquality_74
v1)
      (case T__IsRelatedTo__56 -> T__IsRelatedTo__56
forall a b. a -> b
coe T__IsRelatedTo__56
v0 of
         C_equals_68 AgdaAny
v2 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2
         T__IsRelatedTo__56
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Relation.Binary.Reasoning.Base.Double.begin_
d_begin__110 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny -> AgdaAny -> T__IsRelatedTo__56 -> AgdaAny
d_begin__110 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__56
-> AgdaAny
d_begin__110 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> AgdaAny -> ()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsPreorder_70
v6 AgdaAny
v7 AgdaAny
v8 T__IsRelatedTo__56
v9
  = T_IsPreorder_70
-> AgdaAny -> AgdaAny -> T__IsRelatedTo__56 -> AgdaAny
du_begin__110 T_IsPreorder_70
v6 AgdaAny
v7 AgdaAny
v8 T__IsRelatedTo__56
v9
du_begin__110 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny -> AgdaAny -> T__IsRelatedTo__56 -> AgdaAny
du_begin__110 :: T_IsPreorder_70
-> AgdaAny -> AgdaAny -> T__IsRelatedTo__56 -> AgdaAny
du_begin__110 T_IsPreorder_70
v0 AgdaAny
v1 AgdaAny
v2 T__IsRelatedTo__56
v3
  = case T__IsRelatedTo__56 -> T__IsRelatedTo__56
forall a b. a -> b
coe T__IsRelatedTo__56
v3 of
      C_nonstrict_64 AgdaAny
v4 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4
      C_equals_68 AgdaAny
v4
        -> (T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_reflexive_82 T_IsPreorder_70
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v4
      T__IsRelatedTo__56
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Reasoning.Base.Double.begin-equality_
d_begin'45'equality__124 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny -> AgdaAny -> T__IsRelatedTo__56 -> AgdaAny -> AgdaAny
d_begin'45'equality__124 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__56
-> AgdaAny
-> AgdaAny
d_begin'45'equality__124 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> AgdaAny -> ()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~T_IsPreorder_70
v6 ~AgdaAny
v7 ~AgdaAny
v8 T__IsRelatedTo__56
v9
                         ~AgdaAny
v10
  = T__IsRelatedTo__56 -> AgdaAny
du_begin'45'equality__124 T__IsRelatedTo__56
v9
du_begin'45'equality__124 :: T__IsRelatedTo__56 -> AgdaAny
du_begin'45'equality__124 :: T__IsRelatedTo__56 -> AgdaAny
du_begin'45'equality__124 T__IsRelatedTo__56
v0
  = (T__IsRelatedTo__56 -> T_IsEquality_74 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T__IsRelatedTo__56 -> T_IsEquality_74 -> AgdaAny
du_extractEquality_100 (T__IsRelatedTo__56 -> AgdaAny
forall a b. a -> b
coe T__IsRelatedTo__56
v0)
      ((T_Dec_32 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Dec_32 -> AgdaAny
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_toWitness_36
         ((T__IsRelatedTo__56 -> T_Dec_32) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__IsRelatedTo__56 -> T_Dec_32
du_IsEquality'63'_90 (T__IsRelatedTo__56 -> AgdaAny
forall a b. a -> b
coe T__IsRelatedTo__56
v0)))
-- Relation.Binary.Reasoning.Base.Double.step-∼
d_step'45''8764'_136 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> T__IsRelatedTo__56 -> AgdaAny -> T__IsRelatedTo__56
d_step'45''8764'_136 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__56
-> AgdaAny
-> T__IsRelatedTo__56
d_step'45''8764'_136 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> AgdaAny -> ()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsPreorder_70
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 T__IsRelatedTo__56
v10 AgdaAny
v11
  = T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__56
-> AgdaAny
-> T__IsRelatedTo__56
du_step'45''8764'_136 T_IsPreorder_70
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 T__IsRelatedTo__56
v10 AgdaAny
v11
du_step'45''8764'_136 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> T__IsRelatedTo__56 -> AgdaAny -> T__IsRelatedTo__56
du_step'45''8764'_136 :: T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__56
-> AgdaAny
-> T__IsRelatedTo__56
du_step'45''8764'_136 T_IsPreorder_70
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 T__IsRelatedTo__56
v4 AgdaAny
v5
  = case T__IsRelatedTo__56 -> T__IsRelatedTo__56
forall a b. a -> b
coe T__IsRelatedTo__56
v4 of
      C_nonstrict_64 AgdaAny
v6
        -> (AgdaAny -> T__IsRelatedTo__56) -> AgdaAny -> T__IsRelatedTo__56
forall a b. a -> b
coe
             AgdaAny -> T__IsRelatedTo__56
C_nonstrict_64
             ((T_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_84 T_IsPreorder_70
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v5
                AgdaAny
v6)
      C_equals_68 AgdaAny
v6
        -> (AgdaAny -> T__IsRelatedTo__56) -> AgdaAny -> T__IsRelatedTo__56
forall a b. a -> b
coe
             AgdaAny -> T__IsRelatedTo__56
C_nonstrict_64
             ((T_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_'8764''45'resp'691''45''8776'_106
                (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5))
      T__IsRelatedTo__56
_ -> T__IsRelatedTo__56
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Reasoning.Base.Double.step-≈
d_step'45''8776'_156 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> T__IsRelatedTo__56 -> AgdaAny -> T__IsRelatedTo__56
d_step'45''8776'_156 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__56
-> AgdaAny
-> T__IsRelatedTo__56
d_step'45''8776'_156 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> AgdaAny -> ()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsPreorder_70
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 T__IsRelatedTo__56
v10 AgdaAny
v11
  = T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__56
-> AgdaAny
-> T__IsRelatedTo__56
du_step'45''8776'_156 T_IsPreorder_70
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 T__IsRelatedTo__56
v10 AgdaAny
v11
du_step'45''8776'_156 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> T__IsRelatedTo__56 -> AgdaAny -> T__IsRelatedTo__56
du_step'45''8776'_156 :: T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__56
-> AgdaAny
-> T__IsRelatedTo__56
du_step'45''8776'_156 T_IsPreorder_70
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 T__IsRelatedTo__56
v4 AgdaAny
v5
  = case T__IsRelatedTo__56 -> T__IsRelatedTo__56
forall a b. a -> b
coe T__IsRelatedTo__56
v4 of
      C_nonstrict_64 AgdaAny
v6
        -> (AgdaAny -> T__IsRelatedTo__56) -> AgdaAny -> T__IsRelatedTo__56
forall a b. a -> b
coe
             AgdaAny -> T__IsRelatedTo__56
C_nonstrict_64
             ((T_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_'8764''45'resp'737''45''8776'_100
                (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
                ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
                   (T_IsPreorder_70 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
                      (T_IsPreorder_70 -> T_IsPreorder_70
forall a b. a -> b
coe T_IsPreorder_70
v0))
                   AgdaAny
v1 AgdaAny
v2 AgdaAny
v5)
                (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6))
      C_equals_68 AgdaAny
v6
        -> (AgdaAny -> T__IsRelatedTo__56) -> AgdaAny -> T__IsRelatedTo__56
forall a b. a -> b
coe
             AgdaAny -> T__IsRelatedTo__56
C_equals_68
             ((T_IsEquivalence_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
                (T_IsPreorder_70 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
                   (T_IsPreorder_70 -> T_IsPreorder_70
forall a b. a -> b
coe T_IsPreorder_70
v0))
                AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v5 AgdaAny
v6)
      T__IsRelatedTo__56
_ -> T__IsRelatedTo__56
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Reasoning.Base.Double.step-≈˘
d_step'45''8776''728'_176 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> T__IsRelatedTo__56 -> AgdaAny -> T__IsRelatedTo__56
d_step'45''8776''728'_176 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__56
-> AgdaAny
-> T__IsRelatedTo__56
d_step'45''8776''728'_176 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> AgdaAny -> ()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsPreorder_70
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 T__IsRelatedTo__56
v10
                          AgdaAny
v11
  = T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__56
-> AgdaAny
-> T__IsRelatedTo__56
du_step'45''8776''728'_176 T_IsPreorder_70
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 T__IsRelatedTo__56
v10 AgdaAny
v11
du_step'45''8776''728'_176 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> T__IsRelatedTo__56 -> AgdaAny -> T__IsRelatedTo__56
du_step'45''8776''728'_176 :: T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__56
-> AgdaAny
-> T__IsRelatedTo__56
du_step'45''8776''728'_176 T_IsPreorder_70
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 T__IsRelatedTo__56
v4 AgdaAny
v5
  = (T_IsPreorder_70
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__56
 -> AgdaAny
 -> T__IsRelatedTo__56)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__56
forall a b. a -> b
coe
      T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__56
-> AgdaAny
-> T__IsRelatedTo__56
du_step'45''8776'_156 (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3) (T__IsRelatedTo__56 -> AgdaAny
forall a b. a -> b
coe T__IsRelatedTo__56
v4)
      ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
         (T_IsPreorder_70 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
            (T_IsPreorder_70 -> T_IsPreorder_70
forall a b. a -> b
coe T_IsPreorder_70
v0))
         AgdaAny
v2 AgdaAny
v1 AgdaAny
v5)
-- Relation.Binary.Reasoning.Base.Double.step-≡
d_step'45''8801'_190 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  T__IsRelatedTo__56 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  T__IsRelatedTo__56
d_step'45''8801'_190 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__56
-> T__'8801'__12
-> T__IsRelatedTo__56
d_step'45''8801'_190 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> AgdaAny -> ()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~T_IsPreorder_70
v6 ~AgdaAny
v7 ~AgdaAny
v8 ~AgdaAny
v9 T__IsRelatedTo__56
v10
                     ~T__'8801'__12
v11
  = T__IsRelatedTo__56 -> T__IsRelatedTo__56
du_step'45''8801'_190 T__IsRelatedTo__56
v10
du_step'45''8801'_190 :: T__IsRelatedTo__56 -> T__IsRelatedTo__56
du_step'45''8801'_190 :: T__IsRelatedTo__56 -> T__IsRelatedTo__56
du_step'45''8801'_190 T__IsRelatedTo__56
v0 = T__IsRelatedTo__56 -> T__IsRelatedTo__56
forall a b. a -> b
coe T__IsRelatedTo__56
v0
-- Relation.Binary.Reasoning.Base.Double..extendedlambda0
d_'46'extendedlambda0_198 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_'46'extendedlambda0_198 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
-> AgdaAny
d_'46'extendedlambda0_198 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> AgdaAny -> ()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~T_IsPreorder_70
v6 ~AgdaAny
v7 ~AgdaAny
v8 ~AgdaAny
v9
                          AgdaAny
v10 ~T__'8801'__12
v11 ~T__'8801'__12
v12
  = AgdaAny -> AgdaAny
du_'46'extendedlambda0_198 AgdaAny
v10
du_'46'extendedlambda0_198 :: AgdaAny -> AgdaAny
du_'46'extendedlambda0_198 :: AgdaAny -> AgdaAny
du_'46'extendedlambda0_198 AgdaAny
v0 = AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0
-- Relation.Binary.Reasoning.Base.Double..extendedlambda1
d_'46'extendedlambda1_206 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_'46'extendedlambda1_206 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
-> AgdaAny
d_'46'extendedlambda1_206 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> AgdaAny -> ()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~T_IsPreorder_70
v6 ~AgdaAny
v7 ~AgdaAny
v8 ~AgdaAny
v9
                          AgdaAny
v10 ~T__'8801'__12
v11 ~T__'8801'__12
v12
  = AgdaAny -> AgdaAny
du_'46'extendedlambda1_206 AgdaAny
v10
du_'46'extendedlambda1_206 :: AgdaAny -> AgdaAny
du_'46'extendedlambda1_206 :: AgdaAny -> AgdaAny
du_'46'extendedlambda1_206 AgdaAny
v0 = AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0
-- Relation.Binary.Reasoning.Base.Double.step-≡˘
d_step'45''8801''728'_214 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  T__IsRelatedTo__56 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  T__IsRelatedTo__56
d_step'45''8801''728'_214 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__56
-> T__'8801'__12
-> T__IsRelatedTo__56
d_step'45''8801''728'_214 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> AgdaAny -> ()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~T_IsPreorder_70
v6 ~AgdaAny
v7 ~AgdaAny
v8 ~AgdaAny
v9
                          T__IsRelatedTo__56
v10 ~T__'8801'__12
v11
  = T__IsRelatedTo__56 -> T__IsRelatedTo__56
du_step'45''8801''728'_214 T__IsRelatedTo__56
v10
du_step'45''8801''728'_214 ::
  T__IsRelatedTo__56 -> T__IsRelatedTo__56
du_step'45''8801''728'_214 :: T__IsRelatedTo__56 -> T__IsRelatedTo__56
du_step'45''8801''728'_214 T__IsRelatedTo__56
v0 = T__IsRelatedTo__56 -> T__IsRelatedTo__56
forall a b. a -> b
coe T__IsRelatedTo__56
v0
-- Relation.Binary.Reasoning.Base.Double._≡⟨⟩_
d__'8801''10216''10217'__226 ::
  T__IsRelatedTo__56 -> T__IsRelatedTo__56
d__'8801''10216''10217'__226 :: T__IsRelatedTo__56 -> T__IsRelatedTo__56
d__'8801''10216''10217'__226 T__IsRelatedTo__56
v0 = T__IsRelatedTo__56 -> T__IsRelatedTo__56
forall a b. a -> b
coe T__IsRelatedTo__56
v0
-- Relation.Binary.Reasoning.Base.Double._∎
d__'8718'_234 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny -> T__IsRelatedTo__56
d__'8718'_234 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> AgdaAny
-> T__IsRelatedTo__56
d__'8718'_234 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> AgdaAny -> ()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsPreorder_70
v6 AgdaAny
v7 = T_IsPreorder_70 -> AgdaAny -> T__IsRelatedTo__56
du__'8718'_234 T_IsPreorder_70
v6 AgdaAny
v7
du__'8718'_234 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny -> T__IsRelatedTo__56
du__'8718'_234 :: T_IsPreorder_70 -> AgdaAny -> T__IsRelatedTo__56
du__'8718'_234 T_IsPreorder_70
v0 AgdaAny
v1
  = (AgdaAny -> T__IsRelatedTo__56) -> AgdaAny -> T__IsRelatedTo__56
forall a b. a -> b
coe
      AgdaAny -> T__IsRelatedTo__56
C_equals_68
      ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
         (T_IsPreorder_70 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
            (T_IsPreorder_70 -> T_IsPreorder_70
forall a b. a -> b
coe T_IsPreorder_70
v0))
         AgdaAny
v1)