{-# 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.Data.Nat.DivMod.Core 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.Equality
import qualified MAlonzo.Code.Agda.Builtin.Nat
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Data.Bool.Properties
import qualified MAlonzo.Code.Data.Nat.Base
import qualified MAlonzo.Code.Data.Nat.Properties
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple
import qualified MAlonzo.Code.Relation.Nullary
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
d_mod'45'cong'8323'_18 ::
Integer ->
Integer ->
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_mod'45'cong'8323'_18 :: Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8801'__12
-> T__'8801'__12
d_mod'45'cong'8323'_18 = Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
d_mod'8341''45'skipTo0_28 ::
Integer ->
Integer ->
Integer ->
Integer -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_mod'8341''45'skipTo0_28 :: Integer -> Integer -> Integer -> Integer -> T__'8801'__12
d_mod'8341''45'skipTo0_28 = Integer -> Integer -> Integer -> Integer -> T__'8801'__12
forall a. a
erased
d_a'91'mod'8341''93'1'8801'0_50 ::
Integer -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_a'91'mod'8341''93'1'8801'0_50 :: Integer -> T__'8801'__12
d_a'91'mod'8341''93'1'8801'0_50 = Integer -> T__'8801'__12
forall a. a
erased
d_n'91'mod'8341''93'n'8801'0_58 ::
Integer ->
Integer -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_n'91'mod'8341''93'n'8801'0_58 :: Integer -> Integer -> T__'8801'__12
d_n'91'mod'8341''93'n'8801'0_58 = Integer -> Integer -> T__'8801'__12
forall a. a
erased
d_a'91'mod'8341''93'n'60'n_70 ::
Integer ->
Integer -> Integer -> MAlonzo.Code.Data.Nat.Base.T__'8804'__18
d_a'91'mod'8341''93'n'60'n_70 :: Integer -> Integer -> Integer -> T__'8804'__18
d_a'91'mod'8341''93'n'60'n_70 Integer
v0 Integer
v1 Integer
v2
= case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
Integer
0 -> (Integer -> T__'8804'__18) -> Any -> T__'8804'__18
forall a b. a -> b
coe
Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_m'8804'm'43'n_2316 (Integer -> Any
forall a b. a -> b
coe Integer
v0)
Integer
_ -> let v3 :: Integer
v3 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
Any -> T__'8804'__18
forall a b. a -> b
coe
(case Integer -> Integer
forall a b. a -> b
coe Integer
v2 of
Integer
0 -> (Integer -> Integer -> Integer -> T__'8804'__18)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> T__'8804'__18
d_a'91'mod'8341''93'n'60'n_70 (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v3)
(Integer -> Any
forall a b. a -> b
coe Integer
v0)
Integer
_ -> let v4 :: Integer
v4 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v2) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
Any -> Any
forall a b. a -> b
coe
((Integer -> Integer -> Integer -> T__'8804'__18)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> T__'8804'__18
d_a'91'mod'8341''93'n'60'n_70
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0)) (Integer -> Any
forall a b. a -> b
coe Integer
v3) (Integer -> Any
forall a b. a -> b
coe Integer
v4)))
d_a'91'mod'8341''93'n'8804'a_96 ::
Integer ->
Integer -> Integer -> MAlonzo.Code.Data.Nat.Base.T__'8804'__18
d_a'91'mod'8341''93'n'8804'a_96 :: Integer -> Integer -> Integer -> T__'8804'__18
d_a'91'mod'8341''93'n'8804'a_96 Integer
v0 Integer
v1 Integer
v2
= case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
Integer
0 -> (Integer -> T__'8804'__18) -> Any -> T__'8804'__18
forall a b. a -> b
coe
Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'8804''45'reflexive_1630
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_mod'45'helper_90 Integer
v0
(Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe Integer
v2)) (Integer
0 :: Integer) Integer
v2)
Integer
_ -> let v3 :: Integer
v3 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
Any -> T__'8804'__18
forall a b. a -> b
coe
(case Integer -> Integer
forall a b. a -> b
coe Integer
v2 of
Integer
0 -> (T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any)
-> Any -> (Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_begin__160
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
(\ Any
v4 Any
v5 Any
v6 ->
(Integer -> T__'8804'__18 -> T__'8804'__18) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''8658''8804'_1736 Any
v5 Any
v6)
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_mod'45'helper_90 Integer
v0 Integer
v0 Integer
v1
(Integer
0 :: Integer))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_step'45''8804'_228
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
(\ Any
v4 Any
v5 Any
v6 Any
v7 Any
v8 ->
(T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''45'trans'691'_1868 Any
v7 Any
v8)
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_mod'45'helper_90 Integer
v0 Integer
v0 Integer
v1
(Integer
0 :: Integer))
(Integer -> Any
forall a b. a -> b
coe Integer
v3) ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_step'45''8804'_228
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
(\ Any
v4 Any
v5 Any
v6 Any
v7 Any
v8 ->
(T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''45'trans'691'_1868 Any
v7 Any
v8)
(Integer -> Any
forall a b. a -> b
coe Integer
v3) (Integer -> Any
forall a b. a -> b
coe Integer
v1) ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_step'45''8804'_228
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
(\ Any
v4 Any
v5 Any
v6 Any
v7 Any
v8 ->
(T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''45'trans'691'_1868 Any
v7
Any
v8)
(Integer -> Any
forall a b. a -> b
coe Integer
v1) ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
((T_IsPreorder_70 -> Any -> T__IsRelatedTo__70) -> Any -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70 -> Any -> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du__'8718'_346
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
((Integer -> T__'8804'__18) -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_m'8804'n'43'm_2328 (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
((Integer -> T__'8804'__18) -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.d_n'8804'1'43'n_1724 (Integer -> Any
forall a b. a -> b
coe Integer
v3)))
((Integer -> Integer -> Integer -> T__'8804'__18)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> T__'8804'__18
d_a'91'mod'8341''93'n'8804'a_96 (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v3)
(Integer -> Any
forall a b. a -> b
coe Integer
v0)))
Integer
_ -> let v4 :: Integer
v4 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v2) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
Any -> Any
forall a b. a -> b
coe
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any)
-> Any -> (Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_begin__160
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
(\ Any
v5 Any
v6 Any
v7 ->
(Integer -> T__'8804'__18 -> T__'8804'__18) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''8658''8804'_1736 Any
v6 Any
v7)
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_mod'45'helper_90 Integer
v0
(Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe Integer
v2)) Integer
v1 Integer
v2)
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_step'45''8804'_228
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
(\ Any
v5 Any
v6 Any
v7 Any
v8 Any
v9 ->
(T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''45'trans'691'_1868 Any
v8 Any
v9)
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_mod'45'helper_90 Integer
v0
(Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe Integer
v2)) Integer
v1 Integer
v2)
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1)) ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
((T_IsPreorder_70 -> Any -> T__IsRelatedTo__70) -> Any -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70 -> Any -> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du__'8718'_346
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
((Integer -> Integer -> Integer -> T__'8804'__18)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> T__'8804'__18
d_a'91'mod'8341''93'n'8804'a_96
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0)) (Integer -> Any
forall a b. a -> b
coe Integer
v3) (Integer -> Any
forall a b. a -> b
coe Integer
v4)))))
d_a'8804'n'8658'a'91'mod'8341''93'n'8801'a_124 ::
Integer ->
Integer ->
Integer ->
Integer -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_a'8804'n'8658'a'91'mod'8341''93'n'8801'a_124 :: Integer -> Integer -> Integer -> Integer -> T__'8801'__12
d_a'8804'n'8658'a'91'mod'8341''93'n'8801'a_124 = Integer -> Integer -> Integer -> Integer -> T__'8801'__12
forall a. a
erased
d_mod'8341''45'idem_146 ::
Integer ->
Integer ->
Integer -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_mod'8341''45'idem_146 :: Integer -> Integer -> Integer -> T__'8801'__12
d_mod'8341''45'idem_146 = Integer -> Integer -> Integer -> T__'8801'__12
forall a. a
erased
d_a'43'1'91'mod'8341''93'n'8801'0'8658'a'91'mod'8341''93'n'8801'n'45'1_176 ::
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_a'43'1'91'mod'8341''93'n'8801'0'8658'a'91'mod'8341''93'n'8801'n'45'1_176 :: Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8801'__12
d_a'43'1'91'mod'8341''93'n'8801'0'8658'a'91'mod'8341''93'n'8801'n'45'1_176
= Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8801'__12
forall a. a
erased
d_k'60'1'43'a'91'mod'8341''93'n'8658'k'8804'a'91'mod'8341''93'n_216 ::
Integer ->
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__18 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__18
d_k'60'1'43'a'91'mod'8341''93'n'8658'k'8804'a'91'mod'8341''93'n_216 :: Integer
-> Integer -> Integer -> Integer -> T__'8804'__18 -> T__'8804'__18
d_k'60'1'43'a'91'mod'8341''93'n'8658'k'8804'a'91'mod'8341''93'n_216 Integer
v0
~Integer
v1 Integer
v2 Integer
v3 T__'8804'__18
v4
= Integer -> Integer -> Integer -> T__'8804'__18 -> T__'8804'__18
du_k'60'1'43'a'91'mod'8341''93'n'8658'k'8804'a'91'mod'8341''93'n_216
Integer
v0 Integer
v2 Integer
v3 T__'8804'__18
v4
du_k'60'1'43'a'91'mod'8341''93'n'8658'k'8804'a'91'mod'8341''93'n_216 ::
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__18 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__18
du_k'60'1'43'a'91'mod'8341''93'n'8658'k'8804'a'91'mod'8341''93'n_216 :: Integer -> Integer -> Integer -> T__'8804'__18 -> T__'8804'__18
du_k'60'1'43'a'91'mod'8341''93'n'8658'k'8804'a'91'mod'8341''93'n_216 Integer
v0
Integer
v1 Integer
v2 T__'8804'__18
v3
= case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
Integer
0 -> case T__'8804'__18 -> T__'8804'__18
forall a b. a -> b
coe T__'8804'__18
v3 of
MAlonzo.Code.Data.Nat.Base.C_s'8804's_30 T__'8804'__18
v6 -> T__'8804'__18 -> T__'8804'__18
forall a b. a -> b
coe T__'8804'__18
v6
T__'8804'__18
_ -> T__'8804'__18
forall a. a
MAlonzo.RTE.mazUnreachableError
Integer
_ -> let v4 :: Integer
v4 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
Any -> T__'8804'__18
forall a b. a -> b
coe
(case Integer -> Integer
forall a b. a -> b
coe Integer
v2 of
Integer
0 -> (Integer -> Integer -> Integer -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> T__'8804'__18 -> T__'8804'__18
du_k'60'1'43'a'91'mod'8341''93'n'8658'k'8804'a'91'mod'8341''93'n_216
(Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v4) (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T__'8804'__18 -> Any
forall a b. a -> b
coe T__'8804'__18
v3)
Integer
_ -> let v5 :: Integer
v5 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v2) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
Any -> Any
forall a b. a -> b
coe
((Integer -> Integer -> Integer -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> T__'8804'__18 -> T__'8804'__18
du_k'60'1'43'a'91'mod'8341''93'n'8658'k'8804'a'91'mod'8341''93'n_216
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0)) (Integer -> Any
forall a b. a -> b
coe Integer
v4) (Integer -> Any
forall a b. a -> b
coe Integer
v5)
(T__'8804'__18 -> Any
forall a b. a -> b
coe T__'8804'__18
v3)))
d_1'43'a'91'mod'8341''93'n'8804'1'43'k'8658'a'91'mod'8341''93'n'8804'k_260 ::
Integer ->
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__18 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__18 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__18
d_1'43'a'91'mod'8341''93'n'8804'1'43'k'8658'a'91'mod'8341''93'n'8804'k_260 :: Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__18
-> T__'8804'__18
-> T__'8804'__18
d_1'43'a'91'mod'8341''93'n'8804'1'43'k'8658'a'91'mod'8341''93'n'8804'k_260 Integer
v0
~Integer
v1 Integer
v2 Integer
v3 ~T__'8804'__18
v4 T__'8804'__18
v5
= Integer -> Integer -> Integer -> T__'8804'__18 -> T__'8804'__18
du_1'43'a'91'mod'8341''93'n'8804'1'43'k'8658'a'91'mod'8341''93'n'8804'k_260
Integer
v0 Integer
v2 Integer
v3 T__'8804'__18
v5
du_1'43'a'91'mod'8341''93'n'8804'1'43'k'8658'a'91'mod'8341''93'n'8804'k_260 ::
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__18 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__18
du_1'43'a'91'mod'8341''93'n'8804'1'43'k'8658'a'91'mod'8341''93'n'8804'k_260 :: Integer -> Integer -> Integer -> T__'8804'__18 -> T__'8804'__18
du_1'43'a'91'mod'8341''93'n'8804'1'43'k'8658'a'91'mod'8341''93'n'8804'k_260 Integer
v0
Integer
v1 Integer
v2 T__'8804'__18
v3
= case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
Integer
0 -> case T__'8804'__18 -> T__'8804'__18
forall a b. a -> b
coe T__'8804'__18
v3 of
MAlonzo.Code.Data.Nat.Base.C_s'8804's_30 T__'8804'__18
v6 -> T__'8804'__18 -> T__'8804'__18
forall a b. a -> b
coe T__'8804'__18
v6
T__'8804'__18
_ -> T__'8804'__18
forall a. a
MAlonzo.RTE.mazUnreachableError
Integer
_ -> let v4 :: Integer
v4 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
Any -> T__'8804'__18
forall a b. a -> b
coe
(case Integer -> Integer
forall a b. a -> b
coe Integer
v2 of
Integer
0 -> (Integer -> Integer -> Integer -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> T__'8804'__18 -> T__'8804'__18
du_1'43'a'91'mod'8341''93'n'8804'1'43'k'8658'a'91'mod'8341''93'n'8804'k_260
(Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v4) (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T__'8804'__18 -> Any
forall a b. a -> b
coe T__'8804'__18
v3)
Integer
_ -> let v5 :: Integer
v5 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v2) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
Any -> Any
forall a b. a -> b
coe
((Integer -> Integer -> Integer -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> T__'8804'__18 -> T__'8804'__18
du_1'43'a'91'mod'8341''93'n'8804'1'43'k'8658'a'91'mod'8341''93'n'8804'k_260
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0)) (Integer -> Any
forall a b. a -> b
coe Integer
v4) (Integer -> Any
forall a b. a -> b
coe Integer
v5)
(T__'8804'__18 -> Any
forall a b. a -> b
coe T__'8804'__18
v3)))
d_a'43'n'91'mod'8341''93'n'8801'a'91'mod'8341''93'n_308 ::
Integer ->
Integer ->
Integer -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_a'43'n'91'mod'8341''93'n'8801'a'91'mod'8341''93'n_308 :: Integer -> Integer -> Integer -> T__'8801'__12
d_a'43'n'91'mod'8341''93'n'8801'a'91'mod'8341''93'n_308 = Integer -> Integer -> Integer -> T__'8801'__12
forall a. a
erased
d_mod'8321'_336 ::
Integer -> Integer -> Integer -> Integer -> Integer -> Integer
d_mod'8321'_336 :: Integer -> Integer -> Integer -> Integer -> Integer -> Integer
d_mod'8321'_336 Integer
v0 Integer
v1 ~Integer
v2 = Integer -> Integer -> Integer -> Integer -> Integer
du_mod'8321'_336 Integer
v0 Integer
v1
du_mod'8321'_336 ::
Integer -> Integer -> Integer -> Integer -> Integer
du_mod'8321'_336 :: Integer -> Integer -> Integer -> Integer -> Integer
du_mod'8321'_336 Integer
v0 Integer
v1
= (Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_mod'45'helper_90 Integer
v0
(Integer -> Integer -> Integer
addInt ((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0)) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
d_mod'8322'_338 ::
Integer -> Integer -> Integer -> Integer -> Integer -> Integer
d_mod'8322'_338 :: Integer -> Integer -> Integer -> Integer -> Integer -> Integer
d_mod'8322'_338 Integer
v0 Integer
v1 ~Integer
v2 = Integer -> Integer -> Integer -> Integer -> Integer
du_mod'8322'_338 Integer
v0 Integer
v1
du_mod'8322'_338 ::
Integer -> Integer -> Integer -> Integer -> Integer
du_mod'8322'_338 :: Integer -> Integer -> Integer -> Integer -> Integer
du_mod'8322'_338 Integer
v0 Integer
v1
= (Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_mod'45'helper_90
(Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
(Integer -> Integer -> Integer
addInt ((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0)) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
d_div'45'cong'8323'_358 ::
Integer ->
Integer ->
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_div'45'cong'8323'_358 :: Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8801'__12
-> T__'8801'__12
d_div'45'cong'8323'_358 = Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
d_acc'8804'div'8341''91'acc'93'_368 ::
Integer ->
Integer ->
Integer -> Integer -> MAlonzo.Code.Data.Nat.Base.T__'8804'__18
d_acc'8804'div'8341''91'acc'93'_368 :: Integer -> Integer -> Integer -> Integer -> T__'8804'__18
d_acc'8804'div'8341''91'acc'93'_368 Integer
v0 Integer
v1 Integer
v2 Integer
v3
= case Integer -> Integer
forall a b. a -> b
coe Integer
v2 of
Integer
0 -> (Integer -> T__'8804'__18) -> Any -> T__'8804'__18
forall a b. a -> b
coe
Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'refl_1634 (Integer -> Any
forall a b. a -> b
coe Integer
v0)
Integer
_ -> let v4 :: Integer
v4 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v2) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
Any -> T__'8804'__18
forall a b. a -> b
coe
(case Integer -> Integer
forall a b. a -> b
coe Integer
v3 of
Integer
0 -> (T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'8804''45'trans_1642
((Integer -> T__'8804'__18) -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.d_n'8804'1'43'n_1724 (Integer -> Any
forall a b. a -> b
coe Integer
v0))
((Integer -> Integer -> Integer -> Integer -> T__'8804'__18)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> T__'8804'__18
d_acc'8804'div'8341''91'acc'93'_368
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0)) (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v4)
(Integer -> Any
forall a b. a -> b
coe Integer
v1))
Integer
_ -> let v5 :: Integer
v5 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v3) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
Any -> Any
forall a b. a -> b
coe
((Integer -> Integer -> Integer -> Integer -> T__'8804'__18)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> T__'8804'__18
d_acc'8804'div'8341''91'acc'93'_368 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v4)
(Integer -> Any
forall a b. a -> b
coe Integer
v5)))
d_div'8341''45'offsetEq_410 ::
Integer ->
Integer ->
Integer ->
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__18 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__18 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_div'8341''45'offsetEq_410 :: Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__18
-> T__'8804'__18
-> T__'8846'__30
-> T__'8801'__12
d_div'8341''45'offsetEq_410 = Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__18
-> T__'8804'__18
-> T__'8846'__30
-> T__'8801'__12
forall a. a
erased
d_div'45'mod'45'lemma_656 ::
Integer ->
Integer ->
Integer ->
Integer -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_div'45'mod'45'lemma_656 :: Integer -> Integer -> Integer -> Integer -> T__'8801'__12
d_div'45'mod'45'lemma_656 = Integer -> Integer -> Integer -> Integer -> T__'8801'__12
forall a. a
erased
d_m_686 :: Integer -> Integer -> Integer -> Integer -> Integer
d_m_686 :: Integer -> Integer -> Integer -> Integer -> Integer
d_m_686 Integer
v0 Integer
v1 ~Integer
v2 ~Integer
v3 = Integer -> Integer -> Integer
du_m_686 Integer
v0 Integer
v1
du_m_686 :: Integer -> Integer -> Integer
du_m_686 :: Integer -> Integer -> Integer
du_m_686 Integer
v0 Integer
v1
= (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
2 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0)) (Integer -> Any
forall a b. a -> b
coe Integer
v1)
d_div'8341''45'restart_700 ::
Integer ->
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__18 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_div'8341''45'restart_700 :: Integer
-> Integer -> Integer -> Integer -> T__'8804'__18 -> T__'8801'__12
d_div'8341''45'restart_700 = Integer
-> Integer -> Integer -> Integer -> T__'8804'__18 -> T__'8801'__12
forall a. a
erased
d_div'8341''45'extractAcc_724 ::
Integer ->
Integer ->
Integer ->
Integer -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
= Integer -> Integer -> Integer -> Integer -> T__'8801'__12
forall a. a
erased
d_div'8341''45'finish_756 ::
Integer ->
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__18 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_div'8341''45'finish_756 :: Integer
-> Integer -> Integer -> Integer -> T__'8804'__18 -> T__'8801'__12
d_div'8341''45'finish_756 = Integer
-> Integer -> Integer -> Integer -> T__'8804'__18 -> T__'8801'__12
forall a. a
erased
d_n'91'div'8341''93'n'8801'1_776 ::
Integer ->
Integer -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_n'91'div'8341''93'n'8801'1_776 :: Integer -> Integer -> T__'8801'__12
d_n'91'div'8341''93'n'8801'1_776 = Integer -> Integer -> T__'8801'__12
forall a. a
erased
d_a'91'div'8341''93'1'8801'a_788 ::
Integer ->
Integer -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_a'91'div'8341''93'1'8801'a_788 :: Integer -> Integer -> T__'8801'__12
d_a'91'div'8341''93'1'8801'a_788 = Integer -> Integer -> T__'8801'__12
forall a. a
erased
d_a'42'n'91'div'8341''93'n'8801'a_802 ::
Integer ->
Integer ->
Integer -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_a'42'n'91'div'8341''93'n'8801'a_802 :: Integer -> Integer -> Integer -> T__'8801'__12
d_a'42'n'91'div'8341''93'n'8801'a_802 = Integer -> Integer -> Integer -> T__'8801'__12
forall a. a
erased
d_'43''45'distrib'45'div'8341'_824 ::
Integer ->
Integer ->
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__18 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'43''45'distrib'45'div'8341'_824 :: Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__18
-> T__'8801'__12
d_'43''45'distrib'45'div'8341'_824 = Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__18
-> T__'8801'__12
forall a. a
erased
d_case_870 ::
Integer ->
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__18 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_case_870 :: Integer
-> Integer -> Integer -> Integer -> T__'8804'__18 -> T__'8846'__30
d_case_870 ~Integer
v0 Integer
v1 ~Integer
v2 Integer
v3 T__'8804'__18
v4 = Integer -> Integer -> T__'8804'__18 -> T__'8846'__30
du_case_870 Integer
v1 Integer
v3 T__'8804'__18
v4
du_case_870 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__18 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_case_870 :: Integer -> Integer -> T__'8804'__18 -> T__'8846'__30
du_case_870 Integer
v0 Integer
v1 T__'8804'__18
v2
= (Any -> T__'8846'__30) -> Any -> T__'8846'__30
forall a b. a -> b
coe
Any -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42
((Any -> T__'8846'__30) -> Any -> Any
forall a b. a -> b
coe
Any -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38
((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 Any
forall a. a
erased
((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
((Integer -> T__'8804'__18 -> T__'8804'__18) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'43''45'cancel'737''45''8804'_2242
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0)) (T__'8804'__18 -> Any
forall a b. a -> b
coe T__'8804'__18
v2))
((Integer -> T__'8804'__18) -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_m'8804'n'43'm_2328 (Integer -> Any
forall a b. a -> b
coe Integer
v1)))))
d_div'8341''45'mono'45''8804'_886 ::
Integer ->
Integer ->
Integer ->
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__18 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__18 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__18
d_div'8341''45'mono'45''8804'_886 :: Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__18
-> T__'8804'__18
-> T__'8804'__18
d_div'8341''45'mono'45''8804'_886 Integer
v0 Integer
v1 Integer
v2 Integer
v3 Integer
v4 Integer
v5 T__'8804'__18
v6 T__'8804'__18
v7
= case T__'8804'__18 -> T__'8804'__18
forall a b. a -> b
coe T__'8804'__18
v6 of
T__'8804'__18
MAlonzo.Code.Data.Nat.Base.C_z'8804'n_22
-> (Integer -> Integer -> Integer -> Integer -> T__'8804'__18)
-> Any -> Any -> Any -> Any -> T__'8804'__18
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> T__'8804'__18
d_acc'8804'div'8341''91'acc'93'_368
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60 Integer
v0
(Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4)) (Integer
0 :: Integer) Integer
v4)
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v5)) (Integer -> Any
forall a b. a -> b
coe Integer
v3) (Integer -> Any
forall a b. a -> b
coe Integer
v5)
MAlonzo.Code.Data.Nat.Base.C_s'8804's_30 T__'8804'__18
v10
-> let v11 :: Integer
v11 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v2) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
Any -> T__'8804'__18
forall a b. a -> b
coe
(let v12 :: Integer
v12 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v3) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
Any -> Any
forall a b. a -> b
coe
(let v13 :: b
v13
= Any -> b -> b
forall a b. a -> b -> b
seq
(T__'8804'__18 -> Any
forall a b. a -> b
coe T__'8804'__18
v7)
(let v13 :: t
v13
= ((Any -> Any) -> T_Dec_32 -> T_Dec_32) -> (Any -> Any) -> Any -> t
forall a b. a -> b
coe
(Any -> Any) -> T_Dec_32 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
(\ Any
v13 ->
(Integer -> T__'8804'__18) -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'8804''7495''8658''8804'_1600
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v4)))
((Bool -> T_Dec_32) -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Dec_32
MAlonzo.Code.Data.Bool.Properties.d_T'63'_2210
((Integer -> Integer -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Bool
MAlonzo.Code.Data.Nat.Base.d__'8804''7495'__10
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v4)) (Integer -> Any
forall a b. a -> b
coe Integer
v2))) in
Any -> b
forall a b. a -> b
coe
(case Any -> T_Dec_32
forall a b. a -> b
coe Any
forall a. a
v13 of
MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v14 T_Reflects_14
v15
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v14
then (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_14 -> Any
forall a b. a -> b
coe T_Reflects_14
v15)
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any)
-> Any -> (Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_begin__160
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
(\ Any
v16 Any
v17 Any
v18 ->
(Integer -> T__'8804'__18 -> T__'8804'__18) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''8658''8804'_1736
Any
v17 Any
v18)
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
Integer
v0 (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4)) Integer
v2 Integer
v4)
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
(Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)) Integer
v1 Integer
v12
Integer
v1)
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_step'45''8804'_228
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
(\ Any
v16 Any
v17 Any
v18 Any
v19 Any
v20 ->
(T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''45'trans'691'_1868
Any
v19 Any
v20)
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Any -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
(Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
(Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4))
((Integer -> Integer -> Integer) -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22
Integer
v11 Integer
v4)
(Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4)))
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
(Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)) Integer
v1
Integer
v12 Integer
v1)
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
(Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)) Integer
v1
Integer
v12 Integer
v1)
((T_IsPreorder_70 -> Any -> T__IsRelatedTo__70) -> Any -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70 -> Any -> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du__'8718'_346
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
(Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)) Integer
v1
Integer
v12 Integer
v1))
((Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__18
-> T__'8804'__18
-> T__'8804'__18)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__18
-> T__'8804'__18
-> T__'8804'__18
d_div'8341''45'mono'45''8804'_886
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0))
(Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
((Integer -> Integer -> Integer) -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22
Integer
v11 Integer
v4)
(Integer -> Any
forall a b. a -> b
coe Integer
v12) ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v4))
(Integer -> Any
forall a b. a -> b
coe Integer
v1)
((T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'8804''45'trans_1642
((Integer -> Integer -> T__'8804'__18) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.d_m'8760'n'8804'm_3676
(Integer -> Any
forall a b. a -> b
coe Integer
v11) (Integer -> Any
forall a b. a -> b
coe Integer
v4))
(T__'8804'__18 -> Any
forall a b. a -> b
coe T__'8804'__18
v10))
((Integer -> T__'8804'__18) -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_m'8804'm'43'n_2316
(Integer -> Any
forall a b. a -> b
coe Integer
v1)))))
else (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_14 -> Any
forall a b. a -> b
coe T_Reflects_14
v15)
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any)
-> Any -> (Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_begin__160
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
(\ Any
v16 Any
v17 Any
v18 ->
(Integer -> T__'8804'__18 -> T__'8804'__18) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''8658''8804'_1736
Any
v17 Any
v18)
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
Integer
v0 (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4)) Integer
v2 Integer
v4)
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
(Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)) Integer
v1 Integer
v12
Integer
v1)
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_step'45''8804'_228
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
(\ Any
v16 Any
v17 Any
v18 Any
v19 Any
v20 ->
(T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''45'trans'691'_1868
Any
v19 Any
v20)
(Integer -> Any
forall a b. a -> b
coe Integer
v0)
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0))
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
(Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)) Integer
v1
Integer
v12 Integer
v1)
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_step'45''8804'_228
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
(\ Any
v16 Any
v17 Any
v18 Any
v19 Any
v20 ->
(T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''45'trans'691'_1868
Any
v19 Any
v20)
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0))
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
(Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)) Integer
v1
Integer
v12 Integer
v1)
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
(Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)) Integer
v1
Integer
v12 Integer
v1)
((T_IsPreorder_70 -> Any -> T__IsRelatedTo__70) -> Any -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70 -> Any -> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du__'8718'_346
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
(Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
Integer
v1 Integer
v12 Integer
v1))
((Integer -> Integer -> Integer -> Integer -> T__'8804'__18)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> T__'8804'__18
d_acc'8804'div'8341''91'acc'93'_368
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0))
(Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v12) (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
((Integer -> T__'8804'__18) -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.d_n'8804'1'43'n_1724
(Integer -> Any
forall a b. a -> b
coe Integer
v0))))
T_Dec_32
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)) in
Any -> Any
forall a b. a -> b
coe
(case Integer -> Integer
forall a b. a -> b
coe Integer
v4 of
Integer
0 -> case Integer -> Integer
forall a b. a -> b
coe Integer
v5 of
Integer
0 -> case T__'8804'__18 -> T__'8804'__18
forall a b. a -> b
coe T__'8804'__18
v7 of
T__'8804'__18
MAlonzo.Code.Data.Nat.Base.C_z'8804'n_22
-> let v15 :: Integer
v15 = Integer
0 :: Integer in
Any -> Any
forall a b. a -> b
coe
(let v16 :: t
v16
= ((Any -> Any) -> T_Dec_32 -> T_Dec_32) -> (Any -> Any) -> Any -> t
forall a b. a -> b
coe
(Any -> Any) -> T_Dec_32 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
(\ Any
v16 ->
(Integer -> T__'8804'__18) -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'8804''7495''8658''8804'_1600
(Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)))
((Bool -> T_Dec_32) -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Dec_32
MAlonzo.Code.Data.Bool.Properties.d_T'63'_2210
((Integer -> Integer -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Bool
MAlonzo.Code.Data.Nat.Base.d__'8804''7495'__10
(Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v2))) in
Any -> Any
forall a b. a -> b
coe
(case Any -> T_Dec_32
forall a b. a -> b
coe Any
forall a. a
v16 of
MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v17 T_Reflects_14
v18
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v17
then (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_14 -> Any
forall a b. a -> b
coe T_Reflects_14
v18)
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any)
-> Any -> (Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_begin__160
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
(\ Any
v19 Any
v20 Any
v21 ->
(Integer -> T__'8804'__18 -> T__'8804'__18) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''8658''8804'_1736
Any
v20 Any
v21)
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
Integer
v0 Integer
v1 Integer
v2 Integer
v15)
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
(Integer -> Integer -> Integer
addInt
(Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
(Integer -> Integer
forall a b. a -> b
coe Integer
v0))
Integer
v1 Integer
v12 Integer
v1)
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_step'45''8804'_228
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
(\ Any
v19 Any
v20 Any
v21 Any
v22 Any
v23 ->
(T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''45'trans'691'_1868
Any
v22 Any
v23)
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Any -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
(Integer -> Integer -> Integer
addInt
(Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
(Integer -> Integer
forall a b. a -> b
coe Integer
v0))
Integer
v1
((Integer -> Integer -> Integer) -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22
Integer
v11 Integer
v15)
Integer
v1)
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
(Integer -> Integer -> Integer
addInt
(Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
(Integer -> Integer
forall a b. a -> b
coe Integer
v0))
Integer
v1 Integer
v12 Integer
v1)
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
(Integer -> Integer -> Integer
addInt
(Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
(Integer -> Integer
forall a b. a -> b
coe Integer
v0))
Integer
v1 Integer
v12 Integer
v1)
((T_IsPreorder_70 -> Any -> T__IsRelatedTo__70) -> Any -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70 -> Any -> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du__'8718'_346
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
(Integer -> Integer -> Integer
addInt
(Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
(Integer -> Integer
forall a b. a -> b
coe Integer
v0))
Integer
v1 Integer
v12 Integer
v1))
((Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__18
-> T__'8804'__18
-> T__'8804'__18)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__18
-> T__'8804'__18
-> T__'8804'__18
d_div'8341''45'mono'45''8804'_886
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
(Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
(Integer -> Any
forall a b. a -> b
coe Integer
v0))
(Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
((Integer -> Integer -> Integer) -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22
Integer
v11 Integer
v15)
(Integer -> Any
forall a b. a -> b
coe Integer
v12) (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v1)
((T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'8804''45'trans_1642
((Integer -> Integer -> T__'8804'__18) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.d_m'8760'n'8804'm_3676
(Integer -> Any
forall a b. a -> b
coe Integer
v11) (Integer -> Any
forall a b. a -> b
coe Integer
v15))
(T__'8804'__18 -> Any
forall a b. a -> b
coe T__'8804'__18
v10))
((Integer -> T__'8804'__18) -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_m'8804'm'43'n_2316
(Integer -> Any
forall a b. a -> b
coe Integer
v1)))))
else (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_14 -> Any
forall a b. a -> b
coe T_Reflects_14
v18)
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any)
-> Any -> (Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_begin__160
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
(\ Any
v19 Any
v20 Any
v21 ->
(Integer -> T__'8804'__18 -> T__'8804'__18) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''8658''8804'_1736
Any
v20 Any
v21)
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
Integer
v0 Integer
v1 Integer
v2 Integer
v15)
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
(Integer -> Integer -> Integer
addInt
(Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
(Integer -> Integer
forall a b. a -> b
coe Integer
v0))
Integer
v1 Integer
v12 Integer
v1)
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_step'45''8804'_228
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
(\ Any
v19 Any
v20 Any
v21 Any
v22 Any
v23 ->
(T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''45'trans'691'_1868
Any
v22 Any
v23)
(Integer -> Any
forall a b. a -> b
coe Integer
v0)
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
(Integer -> Any
forall a b. a -> b
coe Integer
v0))
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
(Integer -> Integer -> Integer
addInt
(Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
(Integer -> Integer
forall a b. a -> b
coe Integer
v0))
Integer
v1 Integer
v12 Integer
v1)
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_step'45''8804'_228
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
(\ Any
v19 Any
v20 Any
v21 Any
v22 Any
v23 ->
(T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''45'trans'691'_1868
Any
v22 Any
v23)
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
(Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
(Integer -> Any
forall a b. a -> b
coe Integer
v0))
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
(Integer -> Integer -> Integer
addInt
(Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
(Integer -> Integer
forall a b. a -> b
coe Integer
v0))
Integer
v1 Integer
v12 Integer
v1)
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
(Integer -> Integer -> Integer
addInt
(Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
(Integer -> Integer
forall a b. a -> b
coe Integer
v0))
Integer
v1 Integer
v12 Integer
v1)
((T_IsPreorder_70 -> Any -> T__IsRelatedTo__70) -> Any -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70 -> Any -> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du__'8718'_346
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
(Integer -> Integer -> Integer
addInt
(Integer -> Integer
forall a b. a -> b
coe
(Integer
1 :: Integer))
(Integer -> Integer
forall a b. a -> b
coe Integer
v0))
Integer
v1 Integer
v12 Integer
v1))
((Integer -> Integer -> Integer -> Integer -> T__'8804'__18)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> T__'8804'__18
d_acc'8804'div'8341''91'acc'93'_368
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
(Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
(Integer -> Any
forall a b. a -> b
coe Integer
v0))
(Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v12)
(Integer -> Any
forall a b. a -> b
coe Integer
v1)))
((Integer -> T__'8804'__18) -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.d_n'8804'1'43'n_1724
(Integer -> Any
forall a b. a -> b
coe Integer
v0))))
T_Dec_32
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))
T__'8804'__18
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
Integer
_ -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v13
Integer
_ -> let v14 :: Integer
v14 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v4) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
Any -> Any
forall a b. a -> b
coe
(case Integer -> Integer
forall a b. a -> b
coe Integer
v5 of
Integer
0 -> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq (T__'8804'__18 -> Any
forall a b. a -> b
coe T__'8804'__18
v7)
(let v15 :: t
v15
= ((Any -> Any) -> T_Dec_32 -> T_Dec_32) -> (Any -> Any) -> Any -> t
forall a b. a -> b
coe
(Any -> Any) -> T_Dec_32 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
(\ Any
v15 ->
(Integer -> T__'8804'__18) -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'8804''7495''8658''8804'_1600
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v4)))
((Bool -> T_Dec_32) -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Dec_32
MAlonzo.Code.Data.Bool.Properties.d_T'63'_2210
((Integer -> Integer -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Bool
MAlonzo.Code.Data.Nat.Base.d__'8804''7495'__10
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v4))
(Integer -> Any
forall a b. a -> b
coe Integer
v2))) in
Any -> Any
forall a b. a -> b
coe
(case Any -> T_Dec_32
forall a b. a -> b
coe Any
forall a. a
v15 of
MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v16 T_Reflects_14
v17
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v16
then (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_14 -> Any
forall a b. a -> b
coe T_Reflects_14
v17)
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any)
-> Any -> (Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_begin__160
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
(\ Any
v18 Any
v19 Any
v20 ->
(Integer -> T__'8804'__18 -> T__'8804'__18) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''8658''8804'_1736
Any
v19 Any
v20)
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
Integer
v0 (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4)) Integer
v2
Integer
v4)
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
(Integer -> Integer -> Integer
addInt
(Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
Integer
v1 Integer
v12 Integer
v1)
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_step'45''8804'_228
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
(\ Any
v18 Any
v19 Any
v20 Any
v21 Any
v22 ->
(T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''45'trans'691'_1868
Any
v21 Any
v22)
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Any -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
(Integer -> Integer -> Integer
addInt
(Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
(Integer -> Integer
forall a b. a -> b
coe Integer
v0))
(Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4))
((Integer -> Integer -> Integer) -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22
Integer
v11 Integer
v4)
(Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4)))
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
(Integer -> Integer -> Integer
addInt
(Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
(Integer -> Integer
forall a b. a -> b
coe Integer
v0))
Integer
v1 Integer
v12 Integer
v1)
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
(Integer -> Integer -> Integer
addInt
(Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
(Integer -> Integer
forall a b. a -> b
coe Integer
v0))
Integer
v1 Integer
v12 Integer
v1)
((T_IsPreorder_70 -> Any -> T__IsRelatedTo__70) -> Any -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70 -> Any -> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du__'8718'_346
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
(Integer -> Integer -> Integer
addInt
(Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
(Integer -> Integer
forall a b. a -> b
coe Integer
v0))
Integer
v1 Integer
v12 Integer
v1))
((Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__18
-> T__'8804'__18
-> T__'8804'__18)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__18
-> T__'8804'__18
-> T__'8804'__18
d_div'8341''45'mono'45''8804'_886
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
(Integer -> Any
forall a b. a -> b
coe Integer
v0))
(Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
((Integer -> Integer -> Integer) -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22
Integer
v11 Integer
v4)
(Integer -> Any
forall a b. a -> b
coe Integer
v12)
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v4))
(Integer -> Any
forall a b. a -> b
coe Integer
v1)
((T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'8804''45'trans_1642
((Integer -> Integer -> T__'8804'__18) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.d_m'8760'n'8804'm_3676
(Integer -> Any
forall a b. a -> b
coe Integer
v11) (Integer -> Any
forall a b. a -> b
coe Integer
v4))
(T__'8804'__18 -> Any
forall a b. a -> b
coe T__'8804'__18
v10))
((Integer -> T__'8804'__18) -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_m'8804'm'43'n_2316
(Integer -> Any
forall a b. a -> b
coe Integer
v1)))))
else (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_14 -> Any
forall a b. a -> b
coe T_Reflects_14
v17)
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any)
-> Any -> (Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_begin__160
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
(\ Any
v18 Any
v19 Any
v20 ->
(Integer -> T__'8804'__18 -> T__'8804'__18) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''8658''8804'_1736
Any
v19 Any
v20)
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
Integer
v0 (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4)) Integer
v2
Integer
v4)
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
(Integer -> Integer -> Integer
addInt
(Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
Integer
v1 Integer
v12 Integer
v1)
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_step'45''8804'_228
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
(\ Any
v18 Any
v19 Any
v20 Any
v21 Any
v22 ->
(T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''45'trans'691'_1868
Any
v21 Any
v22)
(Integer -> Any
forall a b. a -> b
coe Integer
v0)
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
(Integer -> Any
forall a b. a -> b
coe Integer
v0))
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
(Integer -> Integer -> Integer
addInt
(Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
(Integer -> Integer
forall a b. a -> b
coe Integer
v0))
Integer
v1 Integer
v12 Integer
v1)
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_step'45''8804'_228
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
(\ Any
v18 Any
v19 Any
v20 Any
v21 Any
v22 ->
(T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''45'trans'691'_1868
Any
v21 Any
v22)
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
(Integer -> Any
forall a b. a -> b
coe Integer
v0))
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
(Integer -> Integer -> Integer
addInt
(Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
(Integer -> Integer
forall a b. a -> b
coe Integer
v0))
Integer
v1 Integer
v12 Integer
v1)
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
(Integer -> Integer -> Integer
addInt
(Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
(Integer -> Integer
forall a b. a -> b
coe Integer
v0))
Integer
v1 Integer
v12 Integer
v1)
((T_IsPreorder_70 -> Any -> T__IsRelatedTo__70) -> Any -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70 -> Any -> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du__'8718'_346
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
(Integer -> Integer -> Integer
addInt
(Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
(Integer -> Integer
forall a b. a -> b
coe Integer
v0))
Integer
v1 Integer
v12 Integer
v1))
((Integer -> Integer -> Integer -> Integer -> T__'8804'__18)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> T__'8804'__18
d_acc'8804'div'8341''91'acc'93'_368
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
(Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
(Integer -> Any
forall a b. a -> b
coe Integer
v0))
(Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v12) (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
((Integer -> T__'8804'__18) -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.d_n'8804'1'43'n_1724
(Integer -> Any
forall a b. a -> b
coe Integer
v0))))
T_Dec_32
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))
Integer
_ -> let v15 :: Integer
v15 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v5) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
Any -> Any
forall a b. a -> b
coe
(case T__'8804'__18 -> T__'8804'__18
forall a b. a -> b
coe T__'8804'__18
v7 of
MAlonzo.Code.Data.Nat.Base.C_s'8804's_30 T__'8804'__18
v18
-> (Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__18
-> T__'8804'__18
-> T__'8804'__18)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__18
-> T__'8804'__18
-> T__'8804'__18
d_div'8341''45'mono'45''8804'_886 (Integer -> Any
forall a b. a -> b
coe Integer
v0)
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
(Integer -> Any
forall a b. a -> b
coe Integer
v11) (Integer -> Any
forall a b. a -> b
coe Integer
v12) (Integer -> Any
forall a b. a -> b
coe Integer
v14) (Integer -> Any
forall a b. a -> b
coe Integer
v15) (T__'8804'__18 -> Any
forall a b. a -> b
coe T__'8804'__18
v10)
(T__'8804'__18 -> Any
forall a b. a -> b
coe T__'8804'__18
v18)
T__'8804'__18
MAlonzo.Code.Data.Nat.Base.C_z'8804'n_22
-> let v17 :: t
v17
= ((Any -> Any) -> T_Dec_32 -> T_Dec_32) -> (Any -> Any) -> Any -> t
forall a b. a -> b
coe
(Any -> Any) -> T_Dec_32 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
(\ Any
v17 ->
(Integer -> T__'8804'__18) -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'8804''7495''8658''8804'_1600
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
(Integer -> Any
forall a b. a -> b
coe Integer
v4)))
((Bool -> T_Dec_32) -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Dec_32
MAlonzo.Code.Data.Bool.Properties.d_T'63'_2210
((Integer -> Integer -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Bool
MAlonzo.Code.Data.Nat.Base.d__'8804''7495'__10
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
(Integer -> Any
forall a b. a -> b
coe Integer
v4))
(Integer -> Any
forall a b. a -> b
coe Integer
v2))) in
Any -> Any
forall a b. a -> b
coe
(case Any -> T_Dec_32
forall a b. a -> b
coe Any
forall a. a
v17 of
MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v18 T_Reflects_14
v19
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v18
then (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_14 -> Any
forall a b. a -> b
coe T_Reflects_14
v19)
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any)
-> Any -> (Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_begin__160
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
(\ Any
v20 Any
v21 Any
v22 ->
(Integer -> T__'8804'__18 -> T__'8804'__18) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''8658''8804'_1736
Any
v21 Any
v22)
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
Integer
v0
(Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4))
Integer
v2 Integer
v4)
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
(Integer -> Integer -> Integer
addInt
(Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
(Integer -> Integer
forall a b. a -> b
coe Integer
v0))
Integer
v1 Integer
v12 Integer
v1)
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_step'45''8804'_228
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
(\ Any
v20 Any
v21 Any
v22 Any
v23 Any
v24 ->
(T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''45'trans'691'_1868
Any
v23 Any
v24)
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Any -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
(Integer -> Integer -> Integer
addInt
(Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
(Integer -> Integer
forall a b. a -> b
coe Integer
v0))
(Integer -> Integer -> Integer
addInt
(Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4))
((Integer -> Integer -> Integer) -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22
Integer
v11 Integer
v4)
(Integer -> Integer -> Integer
addInt
(Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4)))
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
(Integer -> Integer -> Integer
addInt
(Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
(Integer -> Integer
forall a b. a -> b
coe Integer
v0))
Integer
v1 Integer
v12 Integer
v1)
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
(Integer -> Integer -> Integer
addInt
(Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
(Integer -> Integer
forall a b. a -> b
coe Integer
v0))
Integer
v1 Integer
v12 Integer
v1)
((T_IsPreorder_70 -> Any -> T__IsRelatedTo__70) -> Any -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70 -> Any -> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du__'8718'_346
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
(Integer -> Integer -> Integer
addInt
(Integer -> Integer
forall a b. a -> b
coe
(Integer
1 :: Integer))
(Integer -> Integer
forall a b. a -> b
coe Integer
v0))
Integer
v1 Integer
v12 Integer
v1))
((Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__18
-> T__'8804'__18
-> T__'8804'__18)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__18
-> T__'8804'__18
-> T__'8804'__18
d_div'8341''45'mono'45''8804'_886
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
(Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
(Integer -> Any
forall a b. a -> b
coe Integer
v0))
(Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
((Integer -> Integer -> Integer) -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22
Integer
v11 Integer
v4)
(Integer -> Any
forall a b. a -> b
coe Integer
v12)
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe Integer
v1)
(Integer -> Any
forall a b. a -> b
coe Integer
v4))
(Integer -> Any
forall a b. a -> b
coe Integer
v1)
((T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'8804''45'trans_1642
((Integer -> Integer -> T__'8804'__18) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.d_m'8760'n'8804'm_3676
(Integer -> Any
forall a b. a -> b
coe Integer
v11) (Integer -> Any
forall a b. a -> b
coe Integer
v4))
(T__'8804'__18 -> Any
forall a b. a -> b
coe T__'8804'__18
v10))
((Integer -> T__'8804'__18) -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_m'8804'm'43'n_2316
(Integer -> Any
forall a b. a -> b
coe Integer
v1)))))
else (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_14 -> Any
forall a b. a -> b
coe T_Reflects_14
v19)
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any)
-> Any -> (Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_begin__160
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
(\ Any
v20 Any
v21 Any
v22 ->
(Integer -> T__'8804'__18 -> T__'8804'__18) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''8658''8804'_1736
Any
v21 Any
v22)
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
Integer
v0
(Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4))
Integer
v2 Integer
v4)
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
(Integer -> Integer -> Integer
addInt
(Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
(Integer -> Integer
forall a b. a -> b
coe Integer
v0))
Integer
v1 Integer
v12 Integer
v1)
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_step'45''8804'_228
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
(\ Any
v20 Any
v21 Any
v22 Any
v23 Any
v24 ->
(T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''45'trans'691'_1868
Any
v23 Any
v24)
(Integer -> Any
forall a b. a -> b
coe Integer
v0)
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
(Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
(Integer -> Any
forall a b. a -> b
coe Integer
v0))
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
(Integer -> Integer -> Integer
addInt
(Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
(Integer -> Integer
forall a b. a -> b
coe Integer
v0))
Integer
v1 Integer
v12 Integer
v1)
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_step'45''8804'_228
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
(\ Any
v20 Any
v21 Any
v22 Any
v23 Any
v24 ->
(T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''45'trans'691'_1868
Any
v23 Any
v24)
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
(Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
(Integer -> Any
forall a b. a -> b
coe Integer
v0))
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
(Integer -> Integer -> Integer
addInt
(Integer -> Integer
forall a b. a -> b
coe
(Integer
1 :: Integer))
(Integer -> Integer
forall a b. a -> b
coe Integer
v0))
Integer
v1 Integer
v12 Integer
v1)
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
(Integer -> Integer -> Integer
addInt
(Integer -> Integer
forall a b. a -> b
coe
(Integer
1 :: Integer))
(Integer -> Integer
forall a b. a -> b
coe Integer
v0))
Integer
v1 Integer
v12 Integer
v1)
((T_IsPreorder_70 -> Any -> T__IsRelatedTo__70) -> Any -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70 -> Any -> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du__'8718'_346
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
(Integer -> Integer -> Integer
addInt
(Integer -> Integer
forall a b. a -> b
coe
(Integer
1 ::
Integer))
(Integer -> Integer
forall a b. a -> b
coe Integer
v0))
Integer
v1 Integer
v12 Integer
v1))
((Integer -> Integer -> Integer -> Integer -> T__'8804'__18)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> T__'8804'__18
d_acc'8804'div'8341''91'acc'93'_368
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
(Integer -> Any
forall a b. a -> b
coe
(Integer
1 :: Integer))
(Integer -> Any
forall a b. a -> b
coe Integer
v0))
(Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v12)
(Integer -> Any
forall a b. a -> b
coe Integer
v1)))
((Integer -> T__'8804'__18) -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.d_n'8804'1'43'n_1724
(Integer -> Any
forall a b. a -> b
coe Integer
v0))))
T_Dec_32
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
T__'8804'__18
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)))))
T__'8804'__18
_ -> T__'8804'__18
forall a. a
MAlonzo.RTE.mazUnreachableError