{-# 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.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.Binary.Reasoning.Syntax
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'__22
d_a'91'mod'8341''93'n'60'n_70 :: Integer -> Integer -> Integer -> T__'8804'__22
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'__22) -> Any -> T__'8804'__22
forall a b. a -> b
coe
Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_m'8804'm'43'n_3482 (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'__22
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'__22)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> T__'8804'__22
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'__22)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> T__'8804'__22
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'__22
d_a'91'mod'8341''93'n'8804'a_96 :: Integer -> Integer -> Integer -> T__'8804'__22
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'__22) -> Any -> T__'8804'__22
forall a b. a -> b
coe
Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''45'reflexive_2772
((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'__22
forall a b. a -> b
coe
(case Integer -> Integer
forall a b. a -> b
coe Integer
v2 of
Integer
0 -> ((Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any)
-> Any -> Any -> Integer -> Any -> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__46
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__78
-> Any)
-> Any -> (Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__78
-> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_start_96
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
(\ Any
v4 Any
v5 Any
v6 ->
(T__'8804'__22 -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'60''8658''8804'_2854 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
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
(((Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Integer
-> Any
-> Any
-> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''45''10217'_436
(\ Any
v4 Any
v5 Any
v6 Any
v7 Any
v8 -> 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 -> 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
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
(((Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Integer -> Integer -> Any -> T__'8804'__22 -> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8804'_308
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78)
-> 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
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_'8804''45'go_138
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
(\ Any
v4 Any
v5 Any
v6 Any
v7 Any
v8 ->
(T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''45''60''45'trans_2986
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
v3 (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
(((Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Integer
-> Integer
-> Integer
-> Any
-> T__'8804'__22
-> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8804'_308
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78)
-> 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
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_'8804''45'go_138
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
(\ Any
v4 Any
v5 Any
v6 Any
v7 Any
v8 ->
(T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''45''60''45'trans_2986
Any
v7 Any
v8))
Integer
v3 Integer
v1 (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
(((Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Integer -> Integer -> Integer -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8804'_308
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78)
-> 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
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_'8804''45'go_138
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
(\ Any
v4 Any
v5 Any
v6 Any
v7 Any
v8 ->
(T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''45''60''45'trans_2986
Any
v7 Any
v8))
Integer
v1 (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe Integer
v1)) (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
(((Any -> Any) -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any) -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_492
((T_IsPreorder_70 -> Any -> T__IsRelatedTo__78) -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70 -> Any -> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_stop_166
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810))
((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'__22) -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_m'8804'n'43'm_3494
(Integer -> Any
forall a b. a -> b
coe Integer
v1)))
(Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.d_n'8804'1'43'n_2844 (Integer -> Integer
forall a b. a -> b
coe Integer
v3)))
(Integer -> Integer -> Integer -> T__'8804'__22
d_a'91'mod'8341''93'n'8804'a_96
(Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v3) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)))
Any
forall a. a
erased)
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
(((Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any)
-> Any -> Any -> Integer -> Any -> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__46
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__78
-> Any)
-> Any -> (Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__78
-> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_start_96
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
(\ Any
v5 Any
v6 Any
v7 ->
(T__'8804'__22 -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'60''8658''8804'_2854 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
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
(((Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Integer
-> Any
-> Any
-> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''45''10217'_436
(\ Any
v5 Any
v6 Any
v7 Any
v8 Any
v9 -> 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 -> 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
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
(((Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Integer -> Integer -> Any -> T__'8804'__22 -> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8804'_308
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78)
-> 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
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_'8804''45'go_138
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
(\ Any
v5 Any
v6 Any
v7 Any
v8 Any
v9 ->
(T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''45''60''45'trans_2986
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
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe Integer
v1)) (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
(((Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Integer
-> Integer
-> Integer
-> Any
-> Any
-> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''45''10217'_436
(\ Any
v5 Any
v6 Any
v7 Any
v8 Any
v9 -> Any
v9) (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
(Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe Integer
v1)) (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
(((Any -> Any) -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any) -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_492
((T_IsPreorder_70 -> Any -> T__IsRelatedTo__78) -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70 -> Any -> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_stop_166
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810))
((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)))
Any
forall a. a
erased)
(Integer -> Integer -> Integer -> T__'8804'__22
d_a'91'mod'8341''93'n'8804'a_96
((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
v3) (Integer -> Integer
forall a b. a -> b
coe Integer
v4)))
Any
forall a. a
erased)))
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'__22 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22
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'__22 -> T__'8804'__22
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'__22
v4
= Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
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'__22
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'__22 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22
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'__22 -> T__'8804'__22
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'__22
v3
= case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
Integer
0 -> case T__'8804'__22 -> T__'8804'__22
forall a b. a -> b
coe T__'8804'__22
v3 of
MAlonzo.Code.Data.Nat.Base.C_s'8804's_34 T__'8804'__22
v6 -> T__'8804'__22 -> T__'8804'__22
forall a b. a -> b
coe T__'8804'__22
v6
T__'8804'__22
_ -> T__'8804'__22
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'__22
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'__22 -> T__'8804'__22)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
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'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
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'__22 -> T__'8804'__22)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
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'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
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'__22 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22
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'__22
-> T__'8804'__22
-> T__'8804'__22
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'__22
v4 T__'8804'__22
v5
= Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
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'__22
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'__22 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22
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'__22 -> T__'8804'__22
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'__22
v3
= case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
Integer
0 -> case T__'8804'__22 -> T__'8804'__22
forall a b. a -> b
coe T__'8804'__22
v3 of
MAlonzo.Code.Data.Nat.Base.C_s'8804's_34 T__'8804'__22
v6 -> T__'8804'__22 -> T__'8804'__22
forall a b. a -> b
coe T__'8804'__22
v6
T__'8804'__22
_ -> T__'8804'__22
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'__22
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'__22 -> T__'8804'__22)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
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'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
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'__22 -> T__'8804'__22)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
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'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
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'__22
d_acc'8804'div'8341''91'acc'93'_368 :: Integer -> Integer -> Integer -> Integer -> T__'8804'__22
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'__22) -> Any -> T__'8804'__22
forall a b. a -> b
coe
Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'refl_2776 (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'__22
forall a b. a -> b
coe
(case Integer -> Integer
forall a b. a -> b
coe Integer
v3 of
Integer
0 -> (T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''45'trans_2784
((Integer -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.d_n'8804'1'43'n_2844 (Integer -> Any
forall a b. a -> b
coe Integer
v0))
((Integer -> Integer -> Integer -> Integer -> T__'8804'__22)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> T__'8804'__22
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'__22)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> T__'8804'__22
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'__22 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
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'__22
-> T__'8804'__22
-> T__'8846'__30
-> T__'8801'__12
d_div'8341''45'offsetEq_410 = Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__22
-> T__'8804'__22
-> 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'__22 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_div'8341''45'restart_700 :: Integer
-> Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8801'__12
d_div'8341''45'restart_700 = Integer
-> Integer -> Integer -> Integer -> T__'8804'__22 -> 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'__22 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_div'8341''45'finish_756 :: Integer
-> Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8801'__12
d_div'8341''45'finish_756 = Integer
-> Integer -> Integer -> Integer -> T__'8804'__22 -> 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'__22 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'43''45'distrib'45'div'8341'_824 :: Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__22
-> T__'8801'__12
d_'43''45'distrib'45'div'8341'_824 = Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__22
-> T__'8801'__12
forall a. a
erased
d_case_870 ::
Integer ->
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_case_870 :: Integer
-> Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8846'__30
d_case_870 ~Integer
v0 Integer
v1 ~Integer
v2 Integer
v3 T__'8804'__22
v4 = Integer -> Integer -> T__'8804'__22 -> T__'8846'__30
du_case_870 Integer
v1 Integer
v3 T__'8804'__22
v4
du_case_870 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_case_870 :: Integer -> Integer -> T__'8804'__22 -> T__'8846'__30
du_case_870 Integer
v0 Integer
v1 T__'8804'__22
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'__22 -> T__'8804'__22) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'43''45'cancel'737''45''8804'_3414
((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'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
v2))
((Integer -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_m'8804'n'43'm_3494 (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'__22 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_div'8341''45'mono'45''8804'_886 :: Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__22
-> T__'8804'__22
-> T__'8804'__22
d_div'8341''45'mono'45''8804'_886 Integer
v0 Integer
v1 Integer
v2 Integer
v3 Integer
v4 Integer
v5 T__'8804'__22
v6 T__'8804'__22
v7
= case T__'8804'__22 -> T__'8804'__22
forall a b. a -> b
coe T__'8804'__22
v6 of
T__'8804'__22
MAlonzo.Code.Data.Nat.Base.C_z'8804'n_26
-> (Integer -> Integer -> Integer -> Integer -> T__'8804'__22)
-> Any -> Any -> Any -> Any -> T__'8804'__22
forall a b. a -> b
coe
Integer -> Integer -> Integer -> Integer -> T__'8804'__22
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_34 T__'8804'__22
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'__22
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'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
v7)
(let v13 :: t
v13
= ((Any -> Any) -> (Any -> Any) -> T_Dec_20 -> T_Dec_20)
-> (Any -> Any) -> Any -> Any -> t
forall a b. a -> b
coe
(Any -> Any) -> (Any -> Any) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
(\ Any
v13 ->
(Integer -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''7495''8658''8804'_2746
((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)))
((T__'8804'__22 -> Any) -> Any
forall a b. a -> b
coe
T__'8804'__22 -> Any
MAlonzo.Code.Data.Nat.Properties.du_'8804''8658''8804''7495'_2758)
((Bool -> T_Dec_20) -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.d_T'63'_66
((Integer -> Integer -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Bool
MAlonzo.Code.Data.Nat.Base.d__'8804''7495'__14
((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_20
forall a b. a -> b
coe Any
forall a. a
v13 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v14 T_Reflects_16
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_16 -> Any
forall a b. a -> b
coe T_Reflects_16
v15)
(((Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__46
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__78
-> Any)
-> Any -> (Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__78
-> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_start_96
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
(\ Any
v16 Any
v17 Any
v18 ->
(T__'8804'__22 -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe
T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'60''8658''8804'_2854
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)
(((Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''45''10217'_436
(\ Any
v16 Any
v17 Any
v18 Any
v19 Any
v20 -> 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 -> 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)
(((Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> T__'8804'__22 -> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8804'_308
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78)
-> 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
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_'8804''45'go_138
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
(\ Any
v16 Any
v17 Any
v18 Any
v19 Any
v20 ->
(T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''45''60''45'trans_2986
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)
(((Any -> Any) -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any) -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_492
((T_IsPreorder_70 -> Any -> T__IsRelatedTo__78) -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70 -> Any -> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_stop_166
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810))
((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'__22
-> T__'8804'__22
-> T__'8804'__22
d_div'8341''45'mono'45''8804'_886
((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
0 :: Integer))
((Integer -> Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22
Integer
v11 Integer
v4)
(Integer -> Integer
forall a b. a -> b
coe Integer
v12) ((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
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v4))
(Integer -> Integer
forall a b. a -> b
coe Integer
v1)
((T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> T__'8804'__22
forall a b. a -> b
coe
T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''45'trans_2784
((Integer -> Integer -> T__'8804'__22) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.d_m'8760'n'8804'm_5042
(Integer -> Any
forall a b. a -> b
coe Integer
v11) (Integer -> Any
forall a b. a -> b
coe Integer
v4))
(T__'8804'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
v10))
((Integer -> T__'8804'__22) -> Any -> T__'8804'__22
forall a b. a -> b
coe
Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_m'8804'm'43'n_3482
(Integer -> Any
forall a b. a -> b
coe Integer
v1))))
Any
forall a. a
erased))
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_16 -> Any
forall a b. a -> b
coe T_Reflects_16
v15)
(((Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__46
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__78
-> Any)
-> Any -> (Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__78
-> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_start_96
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
(\ Any
v16 Any
v17 Any
v18 ->
(T__'8804'__22 -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe
T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'60''8658''8804'_2854
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)
(((Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Integer
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''45''10217'_436
(\ Any
v16 Any
v17 Any
v18 Any
v19 Any
v20 -> 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
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)
(((Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Integer -> Integer -> Any -> Any -> T__'8804'__22 -> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8804'_308
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78)
-> 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
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_'8804''45'go_138
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
(\ Any
v16 Any
v17 Any
v18 Any
v19 Any
v20 ->
(T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''45''60''45'trans_2986
Any
v19 Any
v20))
Integer
v0 (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 -> 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)
(((Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Integer -> Any -> Any -> Any -> T__'8804'__22 -> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8804'_308
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78)
-> 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
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_'8804''45'go_138
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
(\ Any
v16 Any
v17 Any
v18 Any
v19 Any
v20 ->
(T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''45''60''45'trans_2986
Any
v19 Any
v20))
(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 -> 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)
(((Any -> Any) -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any) -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_492
((T_IsPreorder_70 -> Any -> T__IsRelatedTo__78) -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70 -> Any -> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_stop_166
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810))
((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'__22
d_acc'8804'div'8341''91'acc'93'_368
((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) (Integer -> Integer
forall a b. a -> b
coe Integer
v12) (Integer -> Integer
forall a b. a -> b
coe Integer
v1)))
(Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.d_n'8804'1'43'n_2844
(Integer -> Integer
forall a b. a -> b
coe Integer
v0)))
Any
forall a. a
erased))
T_Dec_20
_ -> 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'__22 -> T__'8804'__22
forall a b. a -> b
coe T__'8804'__22
v7 of
T__'8804'__22
MAlonzo.Code.Data.Nat.Base.C_z'8804'n_26
-> let v15 :: Integer
v15 = Integer
0 :: Integer in
Any -> Any
forall a b. a -> b
coe
(let v16 :: t
v16
= ((Any -> Any) -> (Any -> Any) -> T_Dec_20 -> T_Dec_20)
-> (Any -> Any) -> Any -> Any -> t
forall a b. a -> b
coe
(Any -> Any) -> (Any -> Any) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
(\ Any
v16 ->
(Integer -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''7495''8658''8804'_2746
(Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)))
((T__'8804'__22 -> Any) -> Any
forall a b. a -> b
coe
T__'8804'__22 -> Any
MAlonzo.Code.Data.Nat.Properties.du_'8804''8658''8804''7495'_2758)
((Bool -> T_Dec_20) -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.d_T'63'_66
((Integer -> Integer -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Bool
MAlonzo.Code.Data.Nat.Base.d__'8804''7495'__14
(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_20
forall a b. a -> b
coe Any
forall a. a
v16 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v17 T_Reflects_16
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_16 -> Any
forall a b. a -> b
coe T_Reflects_16
v18)
(((Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__46
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__78
-> Any)
-> Any -> (Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__78
-> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_start_96
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
(\ Any
v19 Any
v20 Any
v21 ->
(T__'8804'__22 -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe
T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'60''8658''8804'_2854
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)
(((Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''45''10217'_436
(\ Any
v19 Any
v20 Any
v21 Any
v22 Any
v23 -> Any
v23)
((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 -> 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)
(((Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> T__'8804'__22 -> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8804'_308
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78)
-> 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
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_'8804''45'go_138
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
(\ Any
v19 Any
v20 Any
v21 Any
v22 Any
v23 ->
(T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''45''60''45'trans_2986
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)
(((Any -> Any) -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any) -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_492
((T_IsPreorder_70 -> Any -> T__IsRelatedTo__78) -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70 -> Any -> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_stop_166
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810))
((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'__22
-> T__'8804'__22
-> T__'8804'__22
d_div'8341''45'mono'45''8804'_886
((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
0 :: Integer))
((Integer -> Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22
Integer
v11 Integer
v15)
(Integer -> Integer
forall a b. a -> b
coe Integer
v12) (Integer -> Integer
forall a b. a -> b
coe Integer
v1)
(Integer -> Integer
forall a b. a -> b
coe Integer
v1)
((T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> T__'8804'__22
forall a b. a -> b
coe
T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''45'trans_2784
((Integer -> Integer -> T__'8804'__22) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.d_m'8760'n'8804'm_5042
(Integer -> Any
forall a b. a -> b
coe Integer
v11)
(Integer -> Any
forall a b. a -> b
coe Integer
v15))
(T__'8804'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
v10))
((Integer -> T__'8804'__22) -> Any -> T__'8804'__22
forall a b. a -> b
coe
Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_m'8804'm'43'n_3482
(Integer -> Any
forall a b. a -> b
coe Integer
v1))))
Any
forall a. a
erased))
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_16 -> Any
forall a b. a -> b
coe T_Reflects_16
v18)
(((Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__46
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__78
-> Any)
-> Any -> (Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__78
-> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_start_96
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
(\ Any
v19 Any
v20 Any
v21 ->
(T__'8804'__22 -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe
T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'60''8658''8804'_2854
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)
(((Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Integer
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''45''10217'_436
(\ Any
v19 Any
v20 Any
v21 Any
v22 Any
v23 -> Any
v23)
((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
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)
(((Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Integer -> Integer -> Any -> Any -> T__'8804'__22 -> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8804'_308
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78)
-> 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
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_'8804''45'go_138
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
(\ Any
v19 Any
v20 Any
v21 Any
v22 Any
v23 ->
(T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''45''60''45'trans_2986
Any
v22 Any
v23))
Integer
v0
(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 -> 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)
(((Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Integer -> Any -> Any -> Any -> T__'8804'__22 -> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8804'_308
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78)
-> 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
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_'8804''45'go_138
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
(\ Any
v19 Any
v20 Any
v21 Any
v22
Any
v23 ->
(T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''45''60''45'trans_2986
Any
v22 Any
v23))
(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 -> 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)
(((Any -> Any) -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any) -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_492
((T_IsPreorder_70 -> Any -> T__IsRelatedTo__78) -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70 -> Any -> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_stop_166
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810))
((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'__22
d_acc'8804'div'8341''91'acc'93'_368
((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) (Integer -> Integer
forall a b. a -> b
coe Integer
v12)
(Integer -> Integer
forall a b. a -> b
coe Integer
v1)))
(Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.d_n'8804'1'43'n_2844
(Integer -> Integer
forall a b. a -> b
coe Integer
v0)))
Any
forall a. a
erased))
T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))
T__'8804'__22
_ -> 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'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
v7)
(let v15 :: t
v15
= ((Any -> Any) -> (Any -> Any) -> T_Dec_20 -> T_Dec_20)
-> (Any -> Any) -> Any -> Any -> t
forall a b. a -> b
coe
(Any -> Any) -> (Any -> Any) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
(\ Any
v15 ->
(Integer -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''7495''8658''8804'_2746
((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)))
((T__'8804'__22 -> Any) -> Any
forall a b. a -> b
coe
T__'8804'__22 -> Any
MAlonzo.Code.Data.Nat.Properties.du_'8804''8658''8804''7495'_2758)
((Bool -> T_Dec_20) -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.d_T'63'_66
((Integer -> Integer -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Bool
MAlonzo.Code.Data.Nat.Base.d__'8804''7495'__14
((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_20
forall a b. a -> b
coe Any
forall a. a
v15 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v16 T_Reflects_16
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_16 -> Any
forall a b. a -> b
coe T_Reflects_16
v17)
(((Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__46
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__78
-> Any)
-> Any -> (Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__78
-> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_start_96
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
(\ Any
v18 Any
v19 Any
v20 ->
(T__'8804'__22 -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe
T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'60''8658''8804'_2854
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)
(((Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''45''10217'_436
(\ Any
v18 Any
v19 Any
v20 Any
v21 Any
v22 -> 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 -> 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)
(((Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> T__'8804'__22 -> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8804'_308
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78)
-> 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
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_'8804''45'go_138
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
(\ Any
v18 Any
v19 Any
v20 Any
v21 Any
v22 ->
(T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''45''60''45'trans_2986
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)
(((Any -> Any) -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any) -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_492
((T_IsPreorder_70 -> Any -> T__IsRelatedTo__78) -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70 -> Any -> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_stop_166
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810))
((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'__22
-> T__'8804'__22
-> T__'8804'__22
d_div'8341''45'mono'45''8804'_886
((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
0 :: Integer))
((Integer -> Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22
Integer
v11 Integer
v4)
(Integer -> Integer
forall a b. a -> b
coe Integer
v12)
((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
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v4))
(Integer -> Integer
forall a b. a -> b
coe Integer
v1)
((T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> T__'8804'__22
forall a b. a -> b
coe
T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''45'trans_2784
((Integer -> Integer -> T__'8804'__22) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.d_m'8760'n'8804'm_5042
(Integer -> Any
forall a b. a -> b
coe Integer
v11) (Integer -> Any
forall a b. a -> b
coe Integer
v4))
(T__'8804'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
v10))
((Integer -> T__'8804'__22) -> Any -> T__'8804'__22
forall a b. a -> b
coe
Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_m'8804'm'43'n_3482
(Integer -> Any
forall a b. a -> b
coe Integer
v1))))
Any
forall a. a
erased))
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_16 -> Any
forall a b. a -> b
coe T_Reflects_16
v17)
(((Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__46
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__78
-> Any)
-> Any -> (Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__78
-> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_start_96
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
(\ Any
v18 Any
v19 Any
v20 ->
(T__'8804'__22 -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe
T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'60''8658''8804'_2854
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)
(((Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Integer
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''45''10217'_436
(\ Any
v18 Any
v19 Any
v20 Any
v21 Any
v22 -> 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
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)
(((Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Integer -> Integer -> Any -> Any -> T__'8804'__22 -> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8804'_308
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78)
-> 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
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_'8804''45'go_138
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
(\ Any
v18 Any
v19 Any
v20 Any
v21 Any
v22 ->
(T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''45''60''45'trans_2986
Any
v21 Any
v22))
Integer
v0
(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 -> 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)
(((Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Integer -> Any -> Any -> Any -> T__'8804'__22 -> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8804'_308
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78)
-> 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
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_'8804''45'go_138
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
(\ Any
v18 Any
v19 Any
v20 Any
v21 Any
v22 ->
(T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''45''60''45'trans_2986
Any
v21 Any
v22))
(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 -> 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)
(((Any -> Any) -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any) -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_492
((T_IsPreorder_70 -> Any -> T__IsRelatedTo__78) -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70 -> Any -> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_stop_166
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810))
((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'__22
d_acc'8804'div'8341''91'acc'93'_368
((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) (Integer -> Integer
forall a b. a -> b
coe Integer
v12)
(Integer -> Integer
forall a b. a -> b
coe Integer
v1)))
(Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.d_n'8804'1'43'n_2844
(Integer -> Integer
forall a b. a -> b
coe Integer
v0)))
Any
forall a. a
erased))
T_Dec_20
_ -> 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'__22 -> T__'8804'__22
forall a b. a -> b
coe T__'8804'__22
v7 of
MAlonzo.Code.Data.Nat.Base.C_s'8804's_34 T__'8804'__22
v18
-> (Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__22
-> T__'8804'__22
-> T__'8804'__22)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__22
-> T__'8804'__22
-> T__'8804'__22
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'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
v10)
(T__'8804'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
v18)
T__'8804'__22
MAlonzo.Code.Data.Nat.Base.C_z'8804'n_26
-> let v17 :: t
v17
= ((Any -> Any) -> (Any -> Any) -> T_Dec_20 -> T_Dec_20)
-> (Any -> Any) -> Any -> Any -> t
forall a b. a -> b
coe
(Any -> Any) -> (Any -> Any) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
(\ Any
v17 ->
(Integer -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''7495''8658''8804'_2746
((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)))
((T__'8804'__22 -> Any) -> Any
forall a b. a -> b
coe
T__'8804'__22 -> Any
MAlonzo.Code.Data.Nat.Properties.du_'8804''8658''8804''7495'_2758)
((Bool -> T_Dec_20) -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.d_T'63'_66
((Integer -> Integer -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Bool
MAlonzo.Code.Data.Nat.Base.d__'8804''7495'__14
((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_20
forall a b. a -> b
coe Any
forall a. a
v17 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v18 T_Reflects_16
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_16 -> Any
forall a b. a -> b
coe T_Reflects_16
v19)
(((Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__46
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__78
-> Any)
-> Any -> (Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__78
-> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_start_96
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
(\ Any
v20 Any
v21 Any
v22 ->
(T__'8804'__22 -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe
T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'60''8658''8804'_2854
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)
(((Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''45''10217'_436
(\ Any
v20 Any
v21 Any
v22 Any
v23 Any
v24 ->
Any
v24)
((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 -> 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)
(((Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> T__'8804'__22 -> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8804'_308
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78)
-> 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
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_'8804''45'go_138
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
(\ Any
v20 Any
v21 Any
v22 Any
v23
Any
v24 ->
(T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''45''60''45'trans_2986
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)
(((Any -> Any) -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any) -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_492
((T_IsPreorder_70 -> Any -> T__IsRelatedTo__78) -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70 -> Any -> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_stop_166
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810))
((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'__22
-> T__'8804'__22
-> T__'8804'__22
d_div'8341''45'mono'45''8804'_886
((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
0 :: Integer))
((Integer -> Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22
Integer
v11 Integer
v4)
(Integer -> Integer
forall a b. a -> b
coe Integer
v12)
((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
v1)
(Integer -> Any
forall a b. a -> b
coe Integer
v4))
(Integer -> Integer
forall a b. a -> b
coe Integer
v1)
((T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> T__'8804'__22
forall a b. a -> b
coe
T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''45'trans_2784
((Integer -> Integer -> T__'8804'__22) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.d_m'8760'n'8804'm_5042
(Integer -> Any
forall a b. a -> b
coe Integer
v11)
(Integer -> Any
forall a b. a -> b
coe Integer
v4))
(T__'8804'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
v10))
((Integer -> T__'8804'__22) -> Any -> T__'8804'__22
forall a b. a -> b
coe
Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_m'8804'm'43'n_3482
(Integer -> Any
forall a b. a -> b
coe Integer
v1))))
Any
forall a. a
erased))
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_16 -> Any
forall a b. a -> b
coe T_Reflects_16
v19)
(((Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__46
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__78
-> Any)
-> Any -> (Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__78
-> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_start_96
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
(\ Any
v20 Any
v21 Any
v22 ->
(T__'8804'__22 -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe
T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'60''8658''8804'_2854
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)
(((Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Integer
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''45''10217'_436
(\ Any
v20 Any
v21 Any
v22 Any
v23 Any
v24 ->
Any
v24)
((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
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)
(((Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Integer -> Integer -> Any -> Any -> T__'8804'__22 -> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8804'_308
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78)
-> 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
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_'8804''45'go_138
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
(\ Any
v20 Any
v21 Any
v22 Any
v23
Any
v24 ->
(T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''45''60''45'trans_2986
Any
v23 Any
v24))
Integer
v0
(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 -> 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)
(((Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Integer -> Any -> Any -> Any -> T__'8804'__22 -> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8804'_308
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78)
-> 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
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_'8804''45'go_138
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
(\ Any
v20 Any
v21 Any
v22 Any
v23
Any
v24 ->
(T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''45''60''45'trans_2986
Any
v23 Any
v24))
(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 -> 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)
(((Any -> Any) -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any) -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_492
((T_IsPreorder_70 -> Any -> T__IsRelatedTo__78) -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70 -> Any -> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_stop_166
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe
T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810))
((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'__22
d_acc'8804'div'8341''91'acc'93'_368
((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) (Integer -> Integer
forall a b. a -> b
coe Integer
v12)
(Integer -> Integer
forall a b. a -> b
coe Integer
v1)))
(Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.d_n'8804'1'43'n_2844
(Integer -> Integer
forall a b. a -> b
coe Integer
v0)))
Any
forall a. a
erased))
T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
T__'8804'__22
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)))))
T__'8804'__22
_ -> T__'8804'__22
forall a. a
MAlonzo.RTE.mazUnreachableError