{-# 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.Nullary

-- Data.Nat.DivMod.Core.mod-cong₃
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
-- Data.Nat.DivMod.Core.modₕ-skipTo0
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
-- Data.Nat.DivMod.Core.a[modₕ]1≡0
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
-- Data.Nat.DivMod.Core.n[modₕ]n≡0
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
-- Data.Nat.DivMod.Core.a[modₕ]n<n
d_a'91'mod'8341''93'n'60'n_70 ::
  Integer ->
  Integer -> Integer -> MAlonzo.Code.Data.Nat.Base.T__'8804'__18
d_a'91'mod'8341''93'n'60'n_70 :: Integer -> Integer -> Integer -> T__'8804'__18
d_a'91'mod'8341''93'n'60'n_70 Integer
v0 Integer
v1 Integer
v2
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
      Integer
0 -> (Integer -> T__'8804'__18) -> Any -> T__'8804'__18
forall a b. a -> b
coe
             Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_m'8804'm'43'n_2316 (Integer -> Any
forall a b. a -> b
coe Integer
v0)
      Integer
_ -> let v3 :: Integer
v3 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           Any -> T__'8804'__18
forall a b. a -> b
coe
             (case Integer -> Integer
forall a b. a -> b
coe Integer
v2 of
                Integer
0 -> (Integer -> Integer -> Integer -> T__'8804'__18)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                       Integer -> Integer -> Integer -> T__'8804'__18
d_a'91'mod'8341''93'n'60'n_70 (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v3)
                       (Integer -> Any
forall a b. a -> b
coe Integer
v0)
                Integer
_ -> let v4 :: Integer
v4 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v2) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
                     Any -> Any
forall a b. a -> b
coe
                       ((Integer -> Integer -> Integer -> T__'8804'__18)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                          Integer -> Integer -> Integer -> T__'8804'__18
d_a'91'mod'8341''93'n'60'n_70
                          ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0)) (Integer -> Any
forall a b. a -> b
coe Integer
v3) (Integer -> Any
forall a b. a -> b
coe Integer
v4)))
-- Data.Nat.DivMod.Core.a[modₕ]n≤a
d_a'91'mod'8341''93'n'8804'a_96 ::
  Integer ->
  Integer -> Integer -> MAlonzo.Code.Data.Nat.Base.T__'8804'__18
d_a'91'mod'8341''93'n'8804'a_96 :: Integer -> Integer -> Integer -> T__'8804'__18
d_a'91'mod'8341''93'n'8804'a_96 Integer
v0 Integer
v1 Integer
v2
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
      Integer
0 -> (Integer -> T__'8804'__18) -> Any -> T__'8804'__18
forall a b. a -> b
coe
             Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'8804''45'reflexive_1630
             ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_mod'45'helper_90 Integer
v0
                (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe Integer
v2)) (Integer
0 :: Integer) Integer
v2)
      Integer
_ -> let v3 :: Integer
v3 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           Any -> T__'8804'__18
forall a b. a -> b
coe
             (case Integer -> Integer
forall a b. a -> b
coe Integer
v2 of
                Integer
0 -> (T_IsPreorder_70
 -> (Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> T__IsRelatedTo__70
 -> Any)
-> Any -> (Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                       T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_begin__160
                       (T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
                       (\ Any
v4 Any
v5 Any
v6 ->
                          (Integer -> T__'8804'__18 -> T__'8804'__18) -> Any -> Any -> Any
forall a b. a -> b
coe
                            Integer -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''8658''8804'_1736 Any
v5 Any
v6)
                       ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                          Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_mod'45'helper_90 Integer
v0 Integer
v0 Integer
v1
                          (Integer
0 :: Integer))
                       ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
                       ((T_IsPreorder_70
 -> (Any -> Any -> Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> Any
 -> T__IsRelatedTo__70
 -> Any
 -> T__IsRelatedTo__70)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
                          T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_step'45''8804'_228
                          (T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
                          (\ Any
v4 Any
v5 Any
v6 Any
v7 Any
v8 ->
                             (T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any
forall a b. a -> b
coe
                               T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''45'trans'691'_1868 Any
v7 Any
v8)
                          ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                             Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_mod'45'helper_90 Integer
v0 Integer
v0 Integer
v1
                             (Integer
0 :: Integer))
                          (Integer -> Any
forall a b. a -> b
coe Integer
v3) ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
                          ((T_IsPreorder_70
 -> (Any -> Any -> Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> Any
 -> T__IsRelatedTo__70
 -> Any
 -> T__IsRelatedTo__70)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
                             T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_step'45''8804'_228
                             (T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
                             (\ Any
v4 Any
v5 Any
v6 Any
v7 Any
v8 ->
                                (T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any
forall a b. a -> b
coe
                                  T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''45'trans'691'_1868 Any
v7 Any
v8)
                             (Integer -> Any
forall a b. a -> b
coe Integer
v3) (Integer -> Any
forall a b. a -> b
coe Integer
v1) ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
                             ((T_IsPreorder_70
 -> (Any -> Any -> Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> Any
 -> T__IsRelatedTo__70
 -> Any
 -> T__IsRelatedTo__70)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
                                T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_step'45''8804'_228
                                (T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
                                (\ Any
v4 Any
v5 Any
v6 Any
v7 Any
v8 ->
                                   (T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any
forall a b. a -> b
coe
                                     T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''45'trans'691'_1868 Any
v7
                                     Any
v8)
                                (Integer -> Any
forall a b. a -> b
coe Integer
v1) ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
                                ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
                                ((T_IsPreorder_70 -> Any -> T__IsRelatedTo__70) -> Any -> Any -> Any
forall a b. a -> b
coe
                                   T_IsPreorder_70 -> Any -> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du__'8718'_346
                                   (T_IsPreorder_70 -> Any
forall a b. a -> b
coe
                                      T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
                                   ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
                                ((Integer -> T__'8804'__18) -> Any -> Any
forall a b. a -> b
coe
                                   Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_m'8804'n'43'm_2328 (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
                             ((Integer -> T__'8804'__18) -> Any -> Any
forall a b. a -> b
coe
                                Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.d_n'8804'1'43'n_1724 (Integer -> Any
forall a b. a -> b
coe Integer
v3)))
                          ((Integer -> Integer -> Integer -> T__'8804'__18)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                             Integer -> Integer -> Integer -> T__'8804'__18
d_a'91'mod'8341''93'n'8804'a_96 (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v3)
                             (Integer -> Any
forall a b. a -> b
coe Integer
v0)))
                Integer
_ -> let v4 :: Integer
v4 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v2) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
                     Any -> Any
forall a b. a -> b
coe
                       ((T_IsPreorder_70
 -> (Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> T__IsRelatedTo__70
 -> Any)
-> Any -> (Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                          T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_begin__160
                          (T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
                          (\ Any
v5 Any
v6 Any
v7 ->
                             (Integer -> T__'8804'__18 -> T__'8804'__18) -> Any -> Any -> Any
forall a b. a -> b
coe
                               Integer -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''8658''8804'_1736 Any
v6 Any
v7)
                          ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                             Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_mod'45'helper_90 Integer
v0
                             (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe Integer
v2)) Integer
v1 Integer
v2)
                          ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
                          ((T_IsPreorder_70
 -> (Any -> Any -> Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> Any
 -> T__IsRelatedTo__70
 -> Any
 -> T__IsRelatedTo__70)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
                             T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_step'45''8804'_228
                             (T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
                             (\ Any
v5 Any
v6 Any
v7 Any
v8 Any
v9 ->
                                (T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any
forall a b. a -> b
coe
                                  T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''45'trans'691'_1868 Any
v8 Any
v9)
                             ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_mod'45'helper_90 Integer
v0
                                (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe Integer
v2)) Integer
v1 Integer
v2)
                             ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1)) ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
                             ((T_IsPreorder_70 -> Any -> T__IsRelatedTo__70) -> Any -> Any -> Any
forall a b. a -> b
coe
                                T_IsPreorder_70 -> Any -> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du__'8718'_346
                                (T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
                                ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
                             ((Integer -> Integer -> Integer -> T__'8804'__18)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                Integer -> Integer -> Integer -> T__'8804'__18
d_a'91'mod'8341''93'n'8804'a_96
                                ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0)) (Integer -> Any
forall a b. a -> b
coe Integer
v3) (Integer -> Any
forall a b. a -> b
coe Integer
v4)))))
-- Data.Nat.DivMod.Core.a≤n⇒a[modₕ]n≡a
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
-- Data.Nat.DivMod.Core.modₕ-idem
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
-- Data.Nat.DivMod.Core.a+1[modₕ]n≡0⇒a[modₕ]n≡n-1
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
-- Data.Nat.DivMod.Core.k<1+a[modₕ]n⇒k≤a[modₕ]n
d_k'60'1'43'a'91'mod'8341''93'n'8658'k'8804'a'91'mod'8341''93'n_216 ::
  Integer ->
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__18 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__18
d_k'60'1'43'a'91'mod'8341''93'n'8658'k'8804'a'91'mod'8341''93'n_216 :: Integer
-> Integer -> Integer -> Integer -> T__'8804'__18 -> T__'8804'__18
d_k'60'1'43'a'91'mod'8341''93'n'8658'k'8804'a'91'mod'8341''93'n_216 Integer
v0
                                                                    ~Integer
v1 Integer
v2 Integer
v3 T__'8804'__18
v4
  = Integer -> Integer -> Integer -> T__'8804'__18 -> T__'8804'__18
du_k'60'1'43'a'91'mod'8341''93'n'8658'k'8804'a'91'mod'8341''93'n_216
      Integer
v0 Integer
v2 Integer
v3 T__'8804'__18
v4
du_k'60'1'43'a'91'mod'8341''93'n'8658'k'8804'a'91'mod'8341''93'n_216 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__18 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__18
du_k'60'1'43'a'91'mod'8341''93'n'8658'k'8804'a'91'mod'8341''93'n_216 :: Integer -> Integer -> Integer -> T__'8804'__18 -> T__'8804'__18
du_k'60'1'43'a'91'mod'8341''93'n'8658'k'8804'a'91'mod'8341''93'n_216 Integer
v0
                                                                     Integer
v1 Integer
v2 T__'8804'__18
v3
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
      Integer
0 -> case T__'8804'__18 -> T__'8804'__18
forall a b. a -> b
coe T__'8804'__18
v3 of
             MAlonzo.Code.Data.Nat.Base.C_s'8804's_30 T__'8804'__18
v6 -> T__'8804'__18 -> T__'8804'__18
forall a b. a -> b
coe T__'8804'__18
v6
             T__'8804'__18
_ -> T__'8804'__18
forall a. a
MAlonzo.RTE.mazUnreachableError
      Integer
_ -> let v4 :: Integer
v4 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           Any -> T__'8804'__18
forall a b. a -> b
coe
             (case Integer -> Integer
forall a b. a -> b
coe Integer
v2 of
                Integer
0 -> (Integer -> Integer -> Integer -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                       Integer -> Integer -> Integer -> T__'8804'__18 -> T__'8804'__18
du_k'60'1'43'a'91'mod'8341''93'n'8658'k'8804'a'91'mod'8341''93'n_216
                       (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v4) (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T__'8804'__18 -> Any
forall a b. a -> b
coe T__'8804'__18
v3)
                Integer
_ -> let v5 :: Integer
v5 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v2) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
                     Any -> Any
forall a b. a -> b
coe
                       ((Integer -> Integer -> Integer -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                          Integer -> Integer -> Integer -> T__'8804'__18 -> T__'8804'__18
du_k'60'1'43'a'91'mod'8341''93'n'8658'k'8804'a'91'mod'8341''93'n_216
                          ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0)) (Integer -> Any
forall a b. a -> b
coe Integer
v4) (Integer -> Any
forall a b. a -> b
coe Integer
v5)
                          (T__'8804'__18 -> Any
forall a b. a -> b
coe T__'8804'__18
v3)))
-- Data.Nat.DivMod.Core.1+a[modₕ]n≤1+k⇒a[modₕ]n≤k
d_1'43'a'91'mod'8341''93'n'8804'1'43'k'8658'a'91'mod'8341''93'n'8804'k_260 ::
  Integer ->
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__18 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__18 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__18
d_1'43'a'91'mod'8341''93'n'8804'1'43'k'8658'a'91'mod'8341''93'n'8804'k_260 :: Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__18
-> T__'8804'__18
-> T__'8804'__18
d_1'43'a'91'mod'8341''93'n'8804'1'43'k'8658'a'91'mod'8341''93'n'8804'k_260 Integer
v0
                                                                           ~Integer
v1 Integer
v2 Integer
v3 ~T__'8804'__18
v4 T__'8804'__18
v5
  = Integer -> Integer -> Integer -> T__'8804'__18 -> T__'8804'__18
du_1'43'a'91'mod'8341''93'n'8804'1'43'k'8658'a'91'mod'8341''93'n'8804'k_260
      Integer
v0 Integer
v2 Integer
v3 T__'8804'__18
v5
du_1'43'a'91'mod'8341''93'n'8804'1'43'k'8658'a'91'mod'8341''93'n'8804'k_260 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__18 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__18
du_1'43'a'91'mod'8341''93'n'8804'1'43'k'8658'a'91'mod'8341''93'n'8804'k_260 :: Integer -> Integer -> Integer -> T__'8804'__18 -> T__'8804'__18
du_1'43'a'91'mod'8341''93'n'8804'1'43'k'8658'a'91'mod'8341''93'n'8804'k_260 Integer
v0
                                                                            Integer
v1 Integer
v2 T__'8804'__18
v3
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
      Integer
0 -> case T__'8804'__18 -> T__'8804'__18
forall a b. a -> b
coe T__'8804'__18
v3 of
             MAlonzo.Code.Data.Nat.Base.C_s'8804's_30 T__'8804'__18
v6 -> T__'8804'__18 -> T__'8804'__18
forall a b. a -> b
coe T__'8804'__18
v6
             T__'8804'__18
_ -> T__'8804'__18
forall a. a
MAlonzo.RTE.mazUnreachableError
      Integer
_ -> let v4 :: Integer
v4 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           Any -> T__'8804'__18
forall a b. a -> b
coe
             (case Integer -> Integer
forall a b. a -> b
coe Integer
v2 of
                Integer
0 -> (Integer -> Integer -> Integer -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                       Integer -> Integer -> Integer -> T__'8804'__18 -> T__'8804'__18
du_1'43'a'91'mod'8341''93'n'8804'1'43'k'8658'a'91'mod'8341''93'n'8804'k_260
                       (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v4) (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T__'8804'__18 -> Any
forall a b. a -> b
coe T__'8804'__18
v3)
                Integer
_ -> let v5 :: Integer
v5 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v2) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
                     Any -> Any
forall a b. a -> b
coe
                       ((Integer -> Integer -> Integer -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                          Integer -> Integer -> Integer -> T__'8804'__18 -> T__'8804'__18
du_1'43'a'91'mod'8341''93'n'8804'1'43'k'8658'a'91'mod'8341''93'n'8804'k_260
                          ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0)) (Integer -> Any
forall a b. a -> b
coe Integer
v4) (Integer -> Any
forall a b. a -> b
coe Integer
v5)
                          (T__'8804'__18 -> Any
forall a b. a -> b
coe T__'8804'__18
v3)))
-- Data.Nat.DivMod.Core.a+n[modₕ]n≡a[modₕ]n
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
-- Data.Nat.DivMod.Core._.mod₁
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))
-- Data.Nat.DivMod.Core._.mod₂
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))
-- Data.Nat.DivMod.Core.div-cong₃
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
-- Data.Nat.DivMod.Core.acc≤divₕ[acc]
d_acc'8804'div'8341''91'acc'93'_368 ::
  Integer ->
  Integer ->
  Integer -> Integer -> MAlonzo.Code.Data.Nat.Base.T__'8804'__18
d_acc'8804'div'8341''91'acc'93'_368 :: Integer -> Integer -> Integer -> Integer -> T__'8804'__18
d_acc'8804'div'8341''91'acc'93'_368 Integer
v0 Integer
v1 Integer
v2 Integer
v3
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v2 of
      Integer
0 -> (Integer -> T__'8804'__18) -> Any -> T__'8804'__18
forall a b. a -> b
coe
             Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'refl_1634 (Integer -> Any
forall a b. a -> b
coe Integer
v0)
      Integer
_ -> let v4 :: Integer
v4 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v2) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           Any -> T__'8804'__18
forall a b. a -> b
coe
             (case Integer -> Integer
forall a b. a -> b
coe Integer
v3 of
                Integer
0 -> (T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any
forall a b. a -> b
coe
                       T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'8804''45'trans_1642
                       ((Integer -> T__'8804'__18) -> Any -> Any
forall a b. a -> b
coe
                          Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.d_n'8804'1'43'n_1724 (Integer -> Any
forall a b. a -> b
coe Integer
v0))
                       ((Integer -> Integer -> Integer -> Integer -> T__'8804'__18)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                          Integer -> Integer -> Integer -> Integer -> T__'8804'__18
d_acc'8804'div'8341''91'acc'93'_368
                          ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0)) (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v4)
                          (Integer -> Any
forall a b. a -> b
coe Integer
v1))
                Integer
_ -> let v5 :: Integer
v5 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v3) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
                     Any -> Any
forall a b. a -> b
coe
                       ((Integer -> Integer -> Integer -> Integer -> T__'8804'__18)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                          Integer -> Integer -> Integer -> Integer -> T__'8804'__18
d_acc'8804'div'8341''91'acc'93'_368 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v4)
                          (Integer -> Any
forall a b. a -> b
coe Integer
v5)))
-- Data.Nat.DivMod.Core.divₕ-offsetEq
d_div'8341''45'offsetEq_410 ::
  Integer ->
  Integer ->
  Integer ->
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__18 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__18 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_div'8341''45'offsetEq_410 :: Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__18
-> T__'8804'__18
-> T__'8846'__30
-> T__'8801'__12
d_div'8341''45'offsetEq_410 = Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__18
-> T__'8804'__18
-> T__'8846'__30
-> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.Core.div-mod-lemma
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
-- Data.Nat.DivMod.Core._.m
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)
-- Data.Nat.DivMod.Core.divₕ-restart
d_div'8341''45'restart_700 ::
  Integer ->
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__18 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_div'8341''45'restart_700 :: Integer
-> Integer -> Integer -> Integer -> T__'8804'__18 -> T__'8801'__12
d_div'8341''45'restart_700 = Integer
-> Integer -> Integer -> Integer -> T__'8804'__18 -> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.Core.divₕ-extractAcc
d_div'8341''45'extractAcc_724 ::
  Integer ->
  Integer ->
  Integer ->
  Integer -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_div'8341''45'extractAcc_724 :: Integer -> Integer -> Integer -> Integer -> T__'8801'__12
d_div'8341''45'extractAcc_724 = Integer -> Integer -> Integer -> Integer -> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.Core.divₕ-finish
d_div'8341''45'finish_756 ::
  Integer ->
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__18 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_div'8341''45'finish_756 :: Integer
-> Integer -> Integer -> Integer -> T__'8804'__18 -> T__'8801'__12
d_div'8341''45'finish_756 = Integer
-> Integer -> Integer -> Integer -> T__'8804'__18 -> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.Core.n[divₕ]n≡1
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
-- Data.Nat.DivMod.Core.a[divₕ]1≡a
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
-- Data.Nat.DivMod.Core.a*n[divₕ]n≡a
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
-- Data.Nat.DivMod.Core.+-distrib-divₕ
d_'43''45'distrib'45'div'8341'_824 ::
  Integer ->
  Integer ->
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__18 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'43''45'distrib'45'div'8341'_824 :: Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__18
-> T__'8801'__12
d_'43''45'distrib'45'div'8341'_824 = Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__18
-> T__'8801'__12
forall a. a
erased
-- Data.Nat.DivMod.Core._.case
d_case_870 ::
  Integer ->
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__18 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_case_870 :: Integer
-> Integer -> Integer -> Integer -> T__'8804'__18 -> T__'8846'__30
d_case_870 ~Integer
v0 Integer
v1 ~Integer
v2 Integer
v3 T__'8804'__18
v4 = Integer -> Integer -> T__'8804'__18 -> T__'8846'__30
du_case_870 Integer
v1 Integer
v3 T__'8804'__18
v4
du_case_870 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__18 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_case_870 :: Integer -> Integer -> T__'8804'__18 -> T__'8846'__30
du_case_870 Integer
v0 Integer
v1 T__'8804'__18
v2
  = (Any -> T__'8846'__30) -> Any -> T__'8846'__30
forall a b. a -> b
coe
      Any -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42
      ((Any -> T__'8846'__30) -> Any -> Any
forall a b. a -> b
coe
         Any -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38
         ((Any -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
            Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
forall a. a
erased
            ((Any -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
               Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
               ((Integer -> T__'8804'__18 -> T__'8804'__18) -> Any -> Any -> Any
forall a b. a -> b
coe
                  Integer -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'43''45'cancel'737''45''8804'_2242
                  ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0)) (T__'8804'__18 -> Any
forall a b. a -> b
coe T__'8804'__18
v2))
               ((Integer -> T__'8804'__18) -> Any -> Any
forall a b. a -> b
coe
                  Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_m'8804'n'43'm_2328 (Integer -> Any
forall a b. a -> b
coe Integer
v1)))))
-- Data.Nat.DivMod.Core.divₕ-mono-≤
d_div'8341''45'mono'45''8804'_886 ::
  Integer ->
  Integer ->
  Integer ->
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__18 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__18 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__18
d_div'8341''45'mono'45''8804'_886 :: Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__18
-> T__'8804'__18
-> T__'8804'__18
d_div'8341''45'mono'45''8804'_886 Integer
v0 Integer
v1 Integer
v2 Integer
v3 Integer
v4 Integer
v5 T__'8804'__18
v6 T__'8804'__18
v7
  = case T__'8804'__18 -> T__'8804'__18
forall a b. a -> b
coe T__'8804'__18
v6 of
      T__'8804'__18
MAlonzo.Code.Data.Nat.Base.C_z'8804'n_22
        -> (Integer -> Integer -> Integer -> Integer -> T__'8804'__18)
-> Any -> Any -> Any -> Any -> T__'8804'__18
forall a b. a -> b
coe
             Integer -> Integer -> Integer -> Integer -> T__'8804'__18
d_acc'8804'div'8341''91'acc'93'_368
             ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60 Integer
v0
                (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4)) (Integer
0 :: Integer) Integer
v4)
             ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v5)) (Integer -> Any
forall a b. a -> b
coe Integer
v3) (Integer -> Any
forall a b. a -> b
coe Integer
v5)
      MAlonzo.Code.Data.Nat.Base.C_s'8804's_30 T__'8804'__18
v10
        -> let v11 :: Integer
v11 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v2) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           Any -> T__'8804'__18
forall a b. a -> b
coe
             (let v12 :: Integer
v12 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v3) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
              Any -> Any
forall a b. a -> b
coe
                (let v13 :: b
v13
                       = Any -> b -> b
forall a b. a -> b -> b
seq
                           (T__'8804'__18 -> Any
forall a b. a -> b
coe T__'8804'__18
v7)
                           (let v13 :: T_Dec_32
v13
                                  = Integer -> Integer -> T_Dec_32
MAlonzo.Code.Data.Nat.Properties.d__'60''63'__1912
                                      (Integer -> Integer
forall a b. a -> b
coe Integer
v4) (Integer -> Integer
forall a b. a -> b
coe Integer
v2) in
                            Any -> b
forall a b. a -> b
coe
                              (case T_Dec_32 -> T_Dec_32
forall a b. a -> b
coe T_Dec_32
v13 of
                                 MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v14 T_Reflects_14
v15
                                   -> if Bool -> Bool
forall a b. a -> b
coe Bool
v14
                                        then (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                                               Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_14 -> Any
forall a b. a -> b
coe T_Reflects_14
v15)
                                               ((T_IsPreorder_70
 -> (Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> T__IsRelatedTo__70
 -> Any)
-> Any -> (Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                                  T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_begin__160
                                                  (T_IsPreorder_70 -> Any
forall a b. a -> b
coe
                                                     T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
                                                  (\ Any
v16 Any
v17 Any
v18 ->
                                                     (Integer -> T__'8804'__18 -> T__'8804'__18) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                       Integer -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''8658''8804'_1736
                                                       Any
v17 Any
v18)
                                                  ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                     Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                     Integer
v0 (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4)) Integer
v2 Integer
v4)
                                                  ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                     Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                     (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)) Integer
v1 Integer
v12
                                                     Integer
v1)
                                                  ((T_IsPreorder_70
 -> (Any -> Any -> Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> Any
 -> T__IsRelatedTo__70
 -> Any
 -> T__IsRelatedTo__70)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
                                                     T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_step'45''8804'_228
                                                     (T_IsPreorder_70 -> Any
forall a b. a -> b
coe
                                                        T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
                                                     (\ Any
v16 Any
v17 Any
v18 Any
v19 Any
v20 ->
                                                        (T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any
forall a b. a -> b
coe
                                                          T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''45'trans'691'_1868
                                                          Any
v19 Any
v20)
                                                     ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Any -> Integer -> Any
forall a b. a -> b
coe
                                                        Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                        (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                        (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4))
                                                        ((Integer -> Integer -> Integer) -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                           Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22
                                                           Integer
v11 Integer
v4)
                                                        (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4)))
                                                     ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                        Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                        (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)) Integer
v1
                                                        Integer
v12 Integer
v1)
                                                     ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                        Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                        (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)) Integer
v1
                                                        Integer
v12 Integer
v1)
                                                     ((T_IsPreorder_70 -> Any -> T__IsRelatedTo__70) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                        T_IsPreorder_70 -> Any -> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du__'8718'_346
                                                        (T_IsPreorder_70 -> Any
forall a b. a -> b
coe
                                                           T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
                                                        ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                           Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                           (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)) Integer
v1
                                                           Integer
v12 Integer
v1))
                                                     ((Integer
 -> Integer
 -> Integer
 -> Integer
 -> Integer
 -> Integer
 -> T__'8804'__18
 -> T__'8804'__18
 -> T__'8804'__18)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                                        Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__18
-> T__'8804'__18
-> T__'8804'__18
d_div'8341''45'mono'45''8804'_886
                                                        ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0))
                                                        (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
                                                        ((Integer -> Integer -> Integer) -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                           Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22
                                                           Integer
v11 Integer
v4)
                                                        (Integer -> Any
forall a b. a -> b
coe Integer
v12) ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v4))
                                                        (Integer -> Any
forall a b. a -> b
coe Integer
v1)
                                                        ((T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any
forall a b. a -> b
coe
                                                           T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'8804''45'trans_1642
                                                           ((Integer -> Integer -> T__'8804'__18) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                              Integer -> Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.d_m'8760'n'8804'm_3676
                                                              (Integer -> Any
forall a b. a -> b
coe Integer
v11) (Integer -> Any
forall a b. a -> b
coe Integer
v4))
                                                           (T__'8804'__18 -> Any
forall a b. a -> b
coe T__'8804'__18
v10))
                                                        ((Integer -> T__'8804'__18) -> Any -> Any
forall a b. a -> b
coe
                                                           Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_m'8804'm'43'n_2316
                                                           (Integer -> Any
forall a b. a -> b
coe Integer
v1)))))
                                        else (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                                               Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_14 -> Any
forall a b. a -> b
coe T_Reflects_14
v15)
                                               ((T_IsPreorder_70
 -> (Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> T__IsRelatedTo__70
 -> Any)
-> Any -> (Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                                  T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_begin__160
                                                  (T_IsPreorder_70 -> Any
forall a b. a -> b
coe
                                                     T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
                                                  (\ Any
v16 Any
v17 Any
v18 ->
                                                     (Integer -> T__'8804'__18 -> T__'8804'__18) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                       Integer -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''8658''8804'_1736
                                                       Any
v17 Any
v18)
                                                  ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                     Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                     Integer
v0 (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4)) Integer
v2 Integer
v4)
                                                  ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                     Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                     (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)) Integer
v1 Integer
v12
                                                     Integer
v1)
                                                  ((T_IsPreorder_70
 -> (Any -> Any -> Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> Any
 -> T__IsRelatedTo__70
 -> Any
 -> T__IsRelatedTo__70)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
                                                     T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_step'45''8804'_228
                                                     (T_IsPreorder_70 -> Any
forall a b. a -> b
coe
                                                        T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
                                                     (\ Any
v16 Any
v17 Any
v18 Any
v19 Any
v20 ->
                                                        (T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any
forall a b. a -> b
coe
                                                          T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''45'trans'691'_1868
                                                          Any
v19 Any
v20)
                                                     (Integer -> Any
forall a b. a -> b
coe Integer
v0)
                                                     ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0))
                                                     ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                        Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                        (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)) Integer
v1
                                                        Integer
v12 Integer
v1)
                                                     ((T_IsPreorder_70
 -> (Any -> Any -> Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> Any
 -> T__IsRelatedTo__70
 -> Any
 -> T__IsRelatedTo__70)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
                                                        T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_step'45''8804'_228
                                                        (T_IsPreorder_70 -> Any
forall a b. a -> b
coe
                                                           T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
                                                        (\ Any
v16 Any
v17 Any
v18 Any
v19 Any
v20 ->
                                                           (T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any
forall a b. a -> b
coe
                                                             T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''45'trans'691'_1868
                                                             Any
v19 Any
v20)
                                                        ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0))
                                                        ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                           Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                           (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)) Integer
v1
                                                           Integer
v12 Integer
v1)
                                                        ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                           Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                           (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)) Integer
v1
                                                           Integer
v12 Integer
v1)
                                                        ((T_IsPreorder_70 -> Any -> T__IsRelatedTo__70) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                           T_IsPreorder_70 -> Any -> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du__'8718'_346
                                                           (T_IsPreorder_70 -> Any
forall a b. a -> b
coe
                                                              T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
                                                           ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                              Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                              (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                              Integer
v1 Integer
v12 Integer
v1))
                                                        ((Integer -> Integer -> Integer -> Integer -> T__'8804'__18)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                                           Integer -> Integer -> Integer -> Integer -> T__'8804'__18
d_acc'8804'div'8341''91'acc'93'_368
                                                           ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                              Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0))
                                                           (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v12) (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
                                                     ((Integer -> T__'8804'__18) -> Any -> Any
forall a b. a -> b
coe
                                                        Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.d_n'8804'1'43'n_1724
                                                        (Integer -> Any
forall a b. a -> b
coe Integer
v0))))
                                 T_Dec_32
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)) in
                 Any -> Any
forall a b. a -> b
coe
                   (case Integer -> Integer
forall a b. a -> b
coe Integer
v4 of
                      Integer
0 -> case Integer -> Integer
forall a b. a -> b
coe Integer
v5 of
                             Integer
0 -> case T__'8804'__18 -> T__'8804'__18
forall a b. a -> b
coe T__'8804'__18
v7 of
                                    T__'8804'__18
MAlonzo.Code.Data.Nat.Base.C_z'8804'n_22
                                      -> let v15 :: Integer
v15 = Integer
0 :: Integer in
                                         Any -> Any
forall a b. a -> b
coe
                                           (let v16 :: T_Dec_32
v16
                                                  = Integer -> Integer -> T_Dec_32
MAlonzo.Code.Data.Nat.Properties.d__'60''63'__1912
                                                      (Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v2) in
                                            Any -> Any
forall a b. a -> b
coe
                                              (case T_Dec_32 -> T_Dec_32
forall a b. a -> b
coe T_Dec_32
v16 of
                                                 MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v17 T_Reflects_14
v18
                                                   -> if Bool -> Bool
forall a b. a -> b
coe Bool
v17
                                                        then (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                               Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_14 -> Any
forall a b. a -> b
coe T_Reflects_14
v18)
                                                               ((T_IsPreorder_70
 -> (Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> T__IsRelatedTo__70
 -> Any)
-> Any -> (Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                  T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_begin__160
                                                                  (T_IsPreorder_70 -> Any
forall a b. a -> b
coe
                                                                     T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
                                                                  (\ Any
v19 Any
v20 Any
v21 ->
                                                                     (Integer -> T__'8804'__18 -> T__'8804'__18) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                       Integer -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''8658''8804'_1736
                                                                       Any
v20 Any
v21)
                                                                  ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                     Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                     Integer
v0 Integer
v1 Integer
v2 Integer
v15)
                                                                  ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                     Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                     (Integer -> Integer -> Integer
addInt
                                                                        (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                        (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                     Integer
v1 Integer
v12 Integer
v1)
                                                                  ((T_IsPreorder_70
 -> (Any -> Any -> Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> Any
 -> T__IsRelatedTo__70
 -> Any
 -> T__IsRelatedTo__70)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
                                                                     T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_step'45''8804'_228
                                                                     (T_IsPreorder_70 -> Any
forall a b. a -> b
coe
                                                                        T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
                                                                     (\ Any
v19 Any
v20 Any
v21 Any
v22 Any
v23 ->
                                                                        (T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any
forall a b. a -> b
coe
                                                                          T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''45'trans'691'_1868
                                                                          Any
v22 Any
v23)
                                                                     ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Any -> Integer -> Any
forall a b. a -> b
coe
                                                                        Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                        (Integer -> Integer -> Integer
addInt
                                                                           (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                           (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                        Integer
v1
                                                                        ((Integer -> Integer -> Integer) -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                           Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22
                                                                           Integer
v11 Integer
v15)
                                                                        Integer
v1)
                                                                     ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                        Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                        (Integer -> Integer -> Integer
addInt
                                                                           (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                           (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                        Integer
v1 Integer
v12 Integer
v1)
                                                                     ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                        Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                        (Integer -> Integer -> Integer
addInt
                                                                           (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                           (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                        Integer
v1 Integer
v12 Integer
v1)
                                                                     ((T_IsPreorder_70 -> Any -> T__IsRelatedTo__70) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                        T_IsPreorder_70 -> Any -> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du__'8718'_346
                                                                        (T_IsPreorder_70 -> Any
forall a b. a -> b
coe
                                                                           T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
                                                                        ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                           Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                           (Integer -> Integer -> Integer
addInt
                                                                              (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                              (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                           Integer
v1 Integer
v12 Integer
v1))
                                                                     ((Integer
 -> Integer
 -> Integer
 -> Integer
 -> Integer
 -> Integer
 -> T__'8804'__18
 -> T__'8804'__18
 -> T__'8804'__18)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                        Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__18
-> T__'8804'__18
-> T__'8804'__18
d_div'8341''45'mono'45''8804'_886
                                                                        ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                           Integer -> Integer -> Integer
addInt
                                                                           (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                           (Integer -> Any
forall a b. a -> b
coe Integer
v0))
                                                                        (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
                                                                        ((Integer -> Integer -> Integer) -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                           Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22
                                                                           Integer
v11 Integer
v15)
                                                                        (Integer -> Any
forall a b. a -> b
coe Integer
v12) (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v1)
                                                                        ((T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any
forall a b. a -> b
coe
                                                                           T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'8804''45'trans_1642
                                                                           ((Integer -> Integer -> T__'8804'__18) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                              Integer -> Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.d_m'8760'n'8804'm_3676
                                                                              (Integer -> Any
forall a b. a -> b
coe Integer
v11) (Integer -> Any
forall a b. a -> b
coe Integer
v15))
                                                                           (T__'8804'__18 -> Any
forall a b. a -> b
coe T__'8804'__18
v10))
                                                                        ((Integer -> T__'8804'__18) -> Any -> Any
forall a b. a -> b
coe
                                                                           Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_m'8804'm'43'n_2316
                                                                           (Integer -> Any
forall a b. a -> b
coe Integer
v1)))))
                                                        else (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                               Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_14 -> Any
forall a b. a -> b
coe T_Reflects_14
v18)
                                                               ((T_IsPreorder_70
 -> (Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> T__IsRelatedTo__70
 -> Any)
-> Any -> (Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                  T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_begin__160
                                                                  (T_IsPreorder_70 -> Any
forall a b. a -> b
coe
                                                                     T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
                                                                  (\ Any
v19 Any
v20 Any
v21 ->
                                                                     (Integer -> T__'8804'__18 -> T__'8804'__18) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                       Integer -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''8658''8804'_1736
                                                                       Any
v20 Any
v21)
                                                                  ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                     Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                     Integer
v0 Integer
v1 Integer
v2 Integer
v15)
                                                                  ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                     Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                     (Integer -> Integer -> Integer
addInt
                                                                        (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                        (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                     Integer
v1 Integer
v12 Integer
v1)
                                                                  ((T_IsPreorder_70
 -> (Any -> Any -> Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> Any
 -> T__IsRelatedTo__70
 -> Any
 -> T__IsRelatedTo__70)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
                                                                     T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_step'45''8804'_228
                                                                     (T_IsPreorder_70 -> Any
forall a b. a -> b
coe
                                                                        T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
                                                                     (\ Any
v19 Any
v20 Any
v21 Any
v22 Any
v23 ->
                                                                        (T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any
forall a b. a -> b
coe
                                                                          T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''45'trans'691'_1868
                                                                          Any
v22 Any
v23)
                                                                     (Integer -> Any
forall a b. a -> b
coe Integer
v0)
                                                                     ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                        Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                        (Integer -> Any
forall a b. a -> b
coe Integer
v0))
                                                                     ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                        Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                        (Integer -> Integer -> Integer
addInt
                                                                           (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                           (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                        Integer
v1 Integer
v12 Integer
v1)
                                                                     ((T_IsPreorder_70
 -> (Any -> Any -> Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> Any
 -> T__IsRelatedTo__70
 -> Any
 -> T__IsRelatedTo__70)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
                                                                        T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_step'45''8804'_228
                                                                        (T_IsPreorder_70 -> Any
forall a b. a -> b
coe
                                                                           T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
                                                                        (\ Any
v19 Any
v20 Any
v21 Any
v22 Any
v23 ->
                                                                           (T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any
forall a b. a -> b
coe
                                                                             T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''45'trans'691'_1868
                                                                             Any
v22 Any
v23)
                                                                        ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                           Integer -> Integer -> Integer
addInt
                                                                           (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                           (Integer -> Any
forall a b. a -> b
coe Integer
v0))
                                                                        ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                           Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                           (Integer -> Integer -> Integer
addInt
                                                                              (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                              (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                           Integer
v1 Integer
v12 Integer
v1)
                                                                        ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                           Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                           (Integer -> Integer -> Integer
addInt
                                                                              (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                              (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                           Integer
v1 Integer
v12 Integer
v1)
                                                                        ((T_IsPreorder_70 -> Any -> T__IsRelatedTo__70) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                           T_IsPreorder_70 -> Any -> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du__'8718'_346
                                                                           (T_IsPreorder_70 -> Any
forall a b. a -> b
coe
                                                                              T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
                                                                           ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                              Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                              (Integer -> Integer -> Integer
addInt
                                                                                 (Integer -> Integer
forall a b. a -> b
coe
                                                                                    (Integer
1 :: Integer))
                                                                                 (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                              Integer
v1 Integer
v12 Integer
v1))
                                                                        ((Integer -> Integer -> Integer -> Integer -> T__'8804'__18)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                           Integer -> Integer -> Integer -> Integer -> T__'8804'__18
d_acc'8804'div'8341''91'acc'93'_368
                                                                           ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                              Integer -> Integer -> Integer
addInt
                                                                              (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                              (Integer -> Any
forall a b. a -> b
coe Integer
v0))
                                                                           (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v12)
                                                                           (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
                                                                     ((Integer -> T__'8804'__18) -> Any -> Any
forall a b. a -> b
coe
                                                                        Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.d_n'8804'1'43'n_1724
                                                                        (Integer -> Any
forall a b. a -> b
coe Integer
v0))))
                                                 T_Dec_32
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))
                                    T__'8804'__18
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                             Integer
_ -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v13
                      Integer
_ -> let v14 :: Integer
v14 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v4) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
                           Any -> Any
forall a b. a -> b
coe
                             (case Integer -> Integer
forall a b. a -> b
coe Integer
v5 of
                                Integer
0 -> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                                       Any -> Any -> Any
forall a b. a -> b -> b
seq (T__'8804'__18 -> Any
forall a b. a -> b
coe T__'8804'__18
v7)
                                       (let v15 :: T_Dec_32
v15
                                              = Integer -> Integer -> T_Dec_32
MAlonzo.Code.Data.Nat.Properties.d__'60''63'__1912
                                                  (Integer -> Integer
forall a b. a -> b
coe Integer
v4) (Integer -> Integer
forall a b. a -> b
coe Integer
v2) in
                                        Any -> Any
forall a b. a -> b
coe
                                          (case T_Dec_32 -> T_Dec_32
forall a b. a -> b
coe T_Dec_32
v15 of
                                             MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v16 T_Reflects_14
v17
                                               -> if Bool -> Bool
forall a b. a -> b
coe Bool
v16
                                                    then (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                           Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_14 -> Any
forall a b. a -> b
coe T_Reflects_14
v17)
                                                           ((T_IsPreorder_70
 -> (Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> T__IsRelatedTo__70
 -> Any)
-> Any -> (Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                                              T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_begin__160
                                                              (T_IsPreorder_70 -> Any
forall a b. a -> b
coe
                                                                 T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
                                                              (\ Any
v18 Any
v19 Any
v20 ->
                                                                 (Integer -> T__'8804'__18 -> T__'8804'__18) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                   Integer -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''8658''8804'_1736
                                                                   Any
v19 Any
v20)
                                                              ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                 Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                 Integer
v0 (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4)) Integer
v2
                                                                 Integer
v4)
                                                              ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                 Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                 (Integer -> Integer -> Integer
addInt
                                                                    (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                 Integer
v1 Integer
v12 Integer
v1)
                                                              ((T_IsPreorder_70
 -> (Any -> Any -> Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> Any
 -> T__IsRelatedTo__70
 -> Any
 -> T__IsRelatedTo__70)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
                                                                 T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_step'45''8804'_228
                                                                 (T_IsPreorder_70 -> Any
forall a b. a -> b
coe
                                                                    T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
                                                                 (\ Any
v18 Any
v19 Any
v20 Any
v21 Any
v22 ->
                                                                    (T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any
forall a b. a -> b
coe
                                                                      T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''45'trans'691'_1868
                                                                      Any
v21 Any
v22)
                                                                 ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Any -> Integer -> Any
forall a b. a -> b
coe
                                                                    Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                    (Integer -> Integer -> Integer
addInt
                                                                       (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                       (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                    (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4))
                                                                    ((Integer -> Integer -> Integer) -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                       Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22
                                                                       Integer
v11 Integer
v4)
                                                                    (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4)))
                                                                 ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                    Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                    (Integer -> Integer -> Integer
addInt
                                                                       (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                       (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                    Integer
v1 Integer
v12 Integer
v1)
                                                                 ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                    Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                    (Integer -> Integer -> Integer
addInt
                                                                       (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                       (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                    Integer
v1 Integer
v12 Integer
v1)
                                                                 ((T_IsPreorder_70 -> Any -> T__IsRelatedTo__70) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                    T_IsPreorder_70 -> Any -> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du__'8718'_346
                                                                    (T_IsPreorder_70 -> Any
forall a b. a -> b
coe
                                                                       T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
                                                                    ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                       Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                       (Integer -> Integer -> Integer
addInt
                                                                          (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                          (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                       Integer
v1 Integer
v12 Integer
v1))
                                                                 ((Integer
 -> Integer
 -> Integer
 -> Integer
 -> Integer
 -> Integer
 -> T__'8804'__18
 -> T__'8804'__18
 -> T__'8804'__18)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                    Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__18
-> T__'8804'__18
-> T__'8804'__18
d_div'8341''45'mono'45''8804'_886
                                                                    ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                       Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                       (Integer -> Any
forall a b. a -> b
coe Integer
v0))
                                                                    (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
                                                                    ((Integer -> Integer -> Integer) -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                       Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22
                                                                       Integer
v11 Integer
v4)
                                                                    (Integer -> Any
forall a b. a -> b
coe Integer
v12)
                                                                    ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v4))
                                                                    (Integer -> Any
forall a b. a -> b
coe Integer
v1)
                                                                    ((T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any
forall a b. a -> b
coe
                                                                       T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'8804''45'trans_1642
                                                                       ((Integer -> Integer -> T__'8804'__18) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                          Integer -> Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.d_m'8760'n'8804'm_3676
                                                                          (Integer -> Any
forall a b. a -> b
coe Integer
v11) (Integer -> Any
forall a b. a -> b
coe Integer
v4))
                                                                       (T__'8804'__18 -> Any
forall a b. a -> b
coe T__'8804'__18
v10))
                                                                    ((Integer -> T__'8804'__18) -> Any -> Any
forall a b. a -> b
coe
                                                                       Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_m'8804'm'43'n_2316
                                                                       (Integer -> Any
forall a b. a -> b
coe Integer
v1)))))
                                                    else (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                           Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_14 -> Any
forall a b. a -> b
coe T_Reflects_14
v17)
                                                           ((T_IsPreorder_70
 -> (Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> T__IsRelatedTo__70
 -> Any)
-> Any -> (Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                                              T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_begin__160
                                                              (T_IsPreorder_70 -> Any
forall a b. a -> b
coe
                                                                 T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
                                                              (\ Any
v18 Any
v19 Any
v20 ->
                                                                 (Integer -> T__'8804'__18 -> T__'8804'__18) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                   Integer -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''8658''8804'_1736
                                                                   Any
v19 Any
v20)
                                                              ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                 Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                 Integer
v0 (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4)) Integer
v2
                                                                 Integer
v4)
                                                              ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                 Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                 (Integer -> Integer -> Integer
addInt
                                                                    (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                 Integer
v1 Integer
v12 Integer
v1)
                                                              ((T_IsPreorder_70
 -> (Any -> Any -> Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> Any
 -> T__IsRelatedTo__70
 -> Any
 -> T__IsRelatedTo__70)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
                                                                 T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_step'45''8804'_228
                                                                 (T_IsPreorder_70 -> Any
forall a b. a -> b
coe
                                                                    T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
                                                                 (\ Any
v18 Any
v19 Any
v20 Any
v21 Any
v22 ->
                                                                    (T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any
forall a b. a -> b
coe
                                                                      T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''45'trans'691'_1868
                                                                      Any
v21 Any
v22)
                                                                 (Integer -> Any
forall a b. a -> b
coe Integer
v0)
                                                                 ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                    Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                    (Integer -> Any
forall a b. a -> b
coe Integer
v0))
                                                                 ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                    Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                    (Integer -> Integer -> Integer
addInt
                                                                       (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                       (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                    Integer
v1 Integer
v12 Integer
v1)
                                                                 ((T_IsPreorder_70
 -> (Any -> Any -> Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> Any
 -> T__IsRelatedTo__70
 -> Any
 -> T__IsRelatedTo__70)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
                                                                    T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_step'45''8804'_228
                                                                    (T_IsPreorder_70 -> Any
forall a b. a -> b
coe
                                                                       T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
                                                                    (\ Any
v18 Any
v19 Any
v20 Any
v21 Any
v22 ->
                                                                       (T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any
forall a b. a -> b
coe
                                                                         T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''45'trans'691'_1868
                                                                         Any
v21 Any
v22)
                                                                    ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                       Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                       (Integer -> Any
forall a b. a -> b
coe Integer
v0))
                                                                    ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                       Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                       (Integer -> Integer -> Integer
addInt
                                                                          (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                          (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                       Integer
v1 Integer
v12 Integer
v1)
                                                                    ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                       Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                       (Integer -> Integer -> Integer
addInt
                                                                          (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                          (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                       Integer
v1 Integer
v12 Integer
v1)
                                                                    ((T_IsPreorder_70 -> Any -> T__IsRelatedTo__70) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                       T_IsPreorder_70 -> Any -> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du__'8718'_346
                                                                       (T_IsPreorder_70 -> Any
forall a b. a -> b
coe
                                                                          T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
                                                                       ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                          Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                          (Integer -> Integer -> Integer
addInt
                                                                             (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                             (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                          Integer
v1 Integer
v12 Integer
v1))
                                                                    ((Integer -> Integer -> Integer -> Integer -> T__'8804'__18)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                       Integer -> Integer -> Integer -> Integer -> T__'8804'__18
d_acc'8804'div'8341''91'acc'93'_368
                                                                       ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                          Integer -> Integer -> Integer
addInt
                                                                          (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                          (Integer -> Any
forall a b. a -> b
coe Integer
v0))
                                                                       (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v12) (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
                                                                 ((Integer -> T__'8804'__18) -> Any -> Any
forall a b. a -> b
coe
                                                                    Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.d_n'8804'1'43'n_1724
                                                                    (Integer -> Any
forall a b. a -> b
coe Integer
v0))))
                                             T_Dec_32
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))
                                Integer
_ -> let v15 :: Integer
v15 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v5) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
                                     Any -> Any
forall a b. a -> b
coe
                                       (case T__'8804'__18 -> T__'8804'__18
forall a b. a -> b
coe T__'8804'__18
v7 of
                                          MAlonzo.Code.Data.Nat.Base.C_s'8804's_30 T__'8804'__18
v18
                                            -> (Integer
 -> Integer
 -> Integer
 -> Integer
 -> Integer
 -> Integer
 -> T__'8804'__18
 -> T__'8804'__18
 -> T__'8804'__18)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                                 Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__18
-> T__'8804'__18
-> T__'8804'__18
d_div'8341''45'mono'45''8804'_886 (Integer -> Any
forall a b. a -> b
coe Integer
v0)
                                                 ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
                                                 (Integer -> Any
forall a b. a -> b
coe Integer
v11) (Integer -> Any
forall a b. a -> b
coe Integer
v12) (Integer -> Any
forall a b. a -> b
coe Integer
v14) (Integer -> Any
forall a b. a -> b
coe Integer
v15) (T__'8804'__18 -> Any
forall a b. a -> b
coe T__'8804'__18
v10)
                                                 (T__'8804'__18 -> Any
forall a b. a -> b
coe T__'8804'__18
v18)
                                          T__'8804'__18
MAlonzo.Code.Data.Nat.Base.C_z'8804'n_22
                                            -> let v17 :: T_Dec_32
v17
                                                     = Integer -> Integer -> T_Dec_32
MAlonzo.Code.Data.Nat.Properties.d__'60''63'__1912
                                                         (Integer -> Integer
forall a b. a -> b
coe Integer
v4) (Integer -> Integer
forall a b. a -> b
coe Integer
v2) in
                                               Any -> Any
forall a b. a -> b
coe
                                                 (case T_Dec_32 -> T_Dec_32
forall a b. a -> b
coe T_Dec_32
v17 of
                                                    MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v18 T_Reflects_14
v19
                                                      -> if Bool -> Bool
forall a b. a -> b
coe Bool
v18
                                                           then (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                  Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_14 -> Any
forall a b. a -> b
coe T_Reflects_14
v19)
                                                                  ((T_IsPreorder_70
 -> (Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> T__IsRelatedTo__70
 -> Any)
-> Any -> (Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                     T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_begin__160
                                                                     (T_IsPreorder_70 -> Any
forall a b. a -> b
coe
                                                                        T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
                                                                     (\ Any
v20 Any
v21 Any
v22 ->
                                                                        (Integer -> T__'8804'__18 -> T__'8804'__18) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                          Integer -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''8658''8804'_1736
                                                                          Any
v21 Any
v22)
                                                                     ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                        Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                        Integer
v0
                                                                        (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4))
                                                                        Integer
v2 Integer
v4)
                                                                     ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                        Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                        (Integer -> Integer -> Integer
addInt
                                                                           (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                           (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                        Integer
v1 Integer
v12 Integer
v1)
                                                                     ((T_IsPreorder_70
 -> (Any -> Any -> Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> Any
 -> T__IsRelatedTo__70
 -> Any
 -> T__IsRelatedTo__70)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
                                                                        T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_step'45''8804'_228
                                                                        (T_IsPreorder_70 -> Any
forall a b. a -> b
coe
                                                                           T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
                                                                        (\ Any
v20 Any
v21 Any
v22 Any
v23 Any
v24 ->
                                                                           (T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any
forall a b. a -> b
coe
                                                                             T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''45'trans'691'_1868
                                                                             Any
v23 Any
v24)
                                                                        ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Any -> Integer -> Any
forall a b. a -> b
coe
                                                                           Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                           (Integer -> Integer -> Integer
addInt
                                                                              (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                              (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                           (Integer -> Integer -> Integer
addInt
                                                                              (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4))
                                                                           ((Integer -> Integer -> Integer) -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                              Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22
                                                                              Integer
v11 Integer
v4)
                                                                           (Integer -> Integer -> Integer
addInt
                                                                              (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4)))
                                                                        ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                           Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                           (Integer -> Integer -> Integer
addInt
                                                                              (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                              (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                           Integer
v1 Integer
v12 Integer
v1)
                                                                        ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                           Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                           (Integer -> Integer -> Integer
addInt
                                                                              (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                              (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                           Integer
v1 Integer
v12 Integer
v1)
                                                                        ((T_IsPreorder_70 -> Any -> T__IsRelatedTo__70) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                           T_IsPreorder_70 -> Any -> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du__'8718'_346
                                                                           (T_IsPreorder_70 -> Any
forall a b. a -> b
coe
                                                                              T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
                                                                           ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                              Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                              (Integer -> Integer -> Integer
addInt
                                                                                 (Integer -> Integer
forall a b. a -> b
coe
                                                                                    (Integer
1 :: Integer))
                                                                                 (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                              Integer
v1 Integer
v12 Integer
v1))
                                                                        ((Integer
 -> Integer
 -> Integer
 -> Integer
 -> Integer
 -> Integer
 -> T__'8804'__18
 -> T__'8804'__18
 -> T__'8804'__18)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                           Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__18
-> T__'8804'__18
-> T__'8804'__18
d_div'8341''45'mono'45''8804'_886
                                                                           ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                              Integer -> Integer -> Integer
addInt
                                                                              (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                              (Integer -> Any
forall a b. a -> b
coe Integer
v0))
                                                                           (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
                                                                           ((Integer -> Integer -> Integer) -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                              Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22
                                                                              Integer
v11 Integer
v4)
                                                                           (Integer -> Any
forall a b. a -> b
coe Integer
v12)
                                                                           ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                              Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe Integer
v1)
                                                                              (Integer -> Any
forall a b. a -> b
coe Integer
v4))
                                                                           (Integer -> Any
forall a b. a -> b
coe Integer
v1)
                                                                           ((T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any
forall a b. a -> b
coe
                                                                              T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'8804''45'trans_1642
                                                                              ((Integer -> Integer -> T__'8804'__18) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                 Integer -> Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.d_m'8760'n'8804'm_3676
                                                                                 (Integer -> Any
forall a b. a -> b
coe Integer
v11) (Integer -> Any
forall a b. a -> b
coe Integer
v4))
                                                                              (T__'8804'__18 -> Any
forall a b. a -> b
coe T__'8804'__18
v10))
                                                                           ((Integer -> T__'8804'__18) -> Any -> Any
forall a b. a -> b
coe
                                                                              Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_m'8804'm'43'n_2316
                                                                              (Integer -> Any
forall a b. a -> b
coe Integer
v1)))))
                                                           else (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                  Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_14 -> Any
forall a b. a -> b
coe T_Reflects_14
v19)
                                                                  ((T_IsPreorder_70
 -> (Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> T__IsRelatedTo__70
 -> Any)
-> Any -> (Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                     T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_begin__160
                                                                     (T_IsPreorder_70 -> Any
forall a b. a -> b
coe
                                                                        T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
                                                                     (\ Any
v20 Any
v21 Any
v22 ->
                                                                        (Integer -> T__'8804'__18 -> T__'8804'__18) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                          Integer -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''8658''8804'_1736
                                                                          Any
v21 Any
v22)
                                                                     ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                        Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                        Integer
v0
                                                                        (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
v4))
                                                                        Integer
v2 Integer
v4)
                                                                     ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                        Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                        (Integer -> Integer -> Integer
addInt
                                                                           (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                           (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                        Integer
v1 Integer
v12 Integer
v1)
                                                                     ((T_IsPreorder_70
 -> (Any -> Any -> Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> Any
 -> T__IsRelatedTo__70
 -> Any
 -> T__IsRelatedTo__70)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
                                                                        T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_step'45''8804'_228
                                                                        (T_IsPreorder_70 -> Any
forall a b. a -> b
coe
                                                                           T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
                                                                        (\ Any
v20 Any
v21 Any
v22 Any
v23 Any
v24 ->
                                                                           (T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any
forall a b. a -> b
coe
                                                                             T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''45'trans'691'_1868
                                                                             Any
v23 Any
v24)
                                                                        (Integer -> Any
forall a b. a -> b
coe Integer
v0)
                                                                        ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                           Integer -> Integer -> Integer
addInt
                                                                           (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                           (Integer -> Any
forall a b. a -> b
coe Integer
v0))
                                                                        ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                           Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                           (Integer -> Integer -> Integer
addInt
                                                                              (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                              (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                           Integer
v1 Integer
v12 Integer
v1)
                                                                        ((T_IsPreorder_70
 -> (Any -> Any -> Any -> Any -> Any -> Any)
 -> Any
 -> Any
 -> Any
 -> T__IsRelatedTo__70
 -> Any
 -> T__IsRelatedTo__70)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
                                                                           T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__IsRelatedTo__70
-> Any
-> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_step'45''8804'_228
                                                                           (T_IsPreorder_70 -> Any
forall a b. a -> b
coe
                                                                              T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
                                                                           (\ Any
v20 Any
v21 Any
v22 Any
v23 Any
v24 ->
                                                                              (T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''45'trans'691'_1868
                                                                                Any
v23 Any
v24)
                                                                           ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                              Integer -> Integer -> Integer
addInt
                                                                              (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
                                                                              (Integer -> Any
forall a b. a -> b
coe Integer
v0))
                                                                           ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                              Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                              (Integer -> Integer -> Integer
addInt
                                                                                 (Integer -> Integer
forall a b. a -> b
coe
                                                                                    (Integer
1 :: Integer))
                                                                                 (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                              Integer
v1 Integer
v12 Integer
v1)
                                                                           ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                              Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                              (Integer -> Integer -> Integer
addInt
                                                                                 (Integer -> Integer
forall a b. a -> b
coe
                                                                                    (Integer
1 :: Integer))
                                                                                 (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                              Integer
v1 Integer
v12 Integer
v1)
                                                                           ((T_IsPreorder_70 -> Any -> T__IsRelatedTo__70) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                              T_IsPreorder_70 -> Any -> T__IsRelatedTo__70
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du__'8718'_346
                                                                              (T_IsPreorder_70 -> Any
forall a b. a -> b
coe
                                                                                 T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_1684)
                                                                              ((Integer -> Integer -> Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
                                                                                 Integer -> Integer -> Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d_div'45'helper_60
                                                                                 (Integer -> Integer -> Integer
addInt
                                                                                    (Integer -> Integer
forall a b. a -> b
coe
                                                                                       (Integer
1 ::
                                                                                          Integer))
                                                                                    (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                                                 Integer
v1 Integer
v12 Integer
v1))
                                                                           ((Integer -> Integer -> Integer -> Integer -> T__'8804'__18)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                              Integer -> Integer -> Integer -> Integer -> T__'8804'__18
d_acc'8804'div'8341''91'acc'93'_368
                                                                              ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                 Integer -> Integer -> Integer
addInt
                                                                                 (Integer -> Any
forall a b. a -> b
coe
                                                                                    (Integer
1 :: Integer))
                                                                                 (Integer -> Any
forall a b. a -> b
coe Integer
v0))
                                                                              (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v12)
                                                                              (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
                                                                        ((Integer -> T__'8804'__18) -> Any -> Any
forall a b. a -> b
coe
                                                                           Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.d_n'8804'1'43'n_1724
                                                                           (Integer -> Any
forall a b. a -> b
coe Integer
v0))))
                                                    T_Dec_32
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
                                          T__'8804'__18
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)))))
      T__'8804'__18
_ -> T__'8804'__18
forall a. a
MAlonzo.RTE.mazUnreachableError