{-# 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 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.Data.Fin.Base
import qualified MAlonzo.Code.Data.Fin.Properties
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Data.Nat.Base
import qualified MAlonzo.Code.Data.Nat.DivMod.Core
import qualified MAlonzo.Code.Data.Nat.Divisibility.Core
import qualified MAlonzo.Code.Data.Nat.Properties
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Induction.WellFounded
import qualified MAlonzo.Code.Relation.Binary.PropositionalEquality.Core
import qualified MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple
import qualified MAlonzo.Code.Relation.Binary.Reasoning.Syntax
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Relation.Nullary.Negation.Core
import qualified MAlonzo.Code.Relation.Nullary.Reflects
d_m'8801'm'37'n'43''91'm'47'n'93''42'n_20 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_m'8801'm'37'n'43''91'm'47'n'93''42'n_20 :: Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
d_m'8801'm'37'n'43''91'm'47'n'93''42'n_20 = Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
forall a. a
erased
d_m'37'n'8801'm'8760'm'47'n'42'n_32 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_m'37'n'8801'm'8760'm'47'n'42'n_32 :: Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
d_m'37'n'8801'm'8760'm'47'n'42'n_32 = Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
forall a. a
erased
d_m'47'n'42'n_42 ::
Integer ->
Integer -> MAlonzo.Code.Data.Nat.Base.T_NonZero_112 -> Integer
d_m'47'n'42'n_42 :: Integer -> Integer -> T_NonZero_112 -> Integer
d_m'47'n'42'n_42 Integer
v0 Integer
v1 ~T_NonZero_112
v2 = Integer -> Integer -> Integer
du_m'47'n'42'n_42 Integer
v0 Integer
v1
du_m'47'n'42'n_42 :: Integer -> Integer -> Integer
du_m'47'n'42'n_42 :: Integer -> Integer -> Integer
du_m'47'n'42'n_42 Integer
v0 Integer
v1
= (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
mulInt
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (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
v1)
d_'37''45'cong'737'_48 ::
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'37''45'cong'737'_48 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8801'__12
-> T__'8801'__12
d_'37''45'cong'737'_48 = Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
d_'37''45'cong'691'_54 ::
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'37''45'cong'691'_54 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T__'8801'__12
-> T__'8801'__12
d_'37''45'cong'691'_54 = Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
d_n'37'1'8801'0_58 ::
Integer -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_n'37'1'8801'0_58 :: Integer -> T__'8801'__12
d_n'37'1'8801'0_58 = Integer -> T__'8801'__12
forall a. a
erased
d_n'37'n'8801'0_64 ::
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_n'37'n'8801'0_64 :: Integer -> T_NonZero_112 -> T__'8801'__12
d_n'37'n'8801'0_64 = Integer -> T_NonZero_112 -> T__'8801'__12
forall a. a
erased
d_m'37'n'37'n'8801'm'37'n_74 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_m'37'n'37'n'8801'm'37'n_74 :: Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
d_m'37'n'37'n'8801'm'37'n_74 = Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
forall a. a
erased
d_'91'm'43'n'93''37'n'8801'm'37'n_86 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'91'm'43'n'93''37'n'8801'm'37'n_86 :: Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
d_'91'm'43'n'93''37'n'8801'm'37'n_86 = Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
forall a. a
erased
d_'91'm'43'kn'93''37'n'8801'm'37'n_100 ::
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'91'm'43'kn'93''37'n'8801'm'37'n_100 :: Integer -> Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
d_'91'm'43'kn'93''37'n'8801'm'37'n_100 = Integer -> Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
forall a. a
erased
d_m'8804'n'8658''91'n'8760'm'93''37'm'8801'n'37'm_118 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_m'8804'n'8658''91'n'8760'm'93''37'm'8801'n'37'm_118 :: Integer
-> Integer -> T_NonZero_112 -> T__'8804'__22 -> T__'8801'__12
d_m'8804'n'8658''91'n'8760'm'93''37'm'8801'n'37'm_118 = Integer
-> Integer -> T_NonZero_112 -> T__'8804'__22 -> T__'8801'__12
forall a. a
erased
d_m'42'n'8804'o'8658''91'o'8760'm'42'n'93''37'n'8801'o'37'n_136 ::
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_m'42'n'8804'o'8658''91'o'8760'm'42'n'93''37'n'8801'o'37'n_136 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8804'__22
-> T__'8801'__12
d_m'42'n'8804'o'8658''91'o'8760'm'42'n'93''37'n'8801'o'37'n_136
= Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8804'__22
-> T__'8801'__12
forall a. a
erased
d_m'42'n'37'n'8801'0_154 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_m'42'n'37'n'8801'0_154 :: Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
d_m'42'n'37'n'8801'0_154 = Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
forall a. a
erased
d_m'37'n'60'n_166 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_m'37'n'60'n_166 :: Integer -> Integer -> T_NonZero_112 -> T__'8804'__22
d_m'37'n'60'n_166 Integer
v0 Integer
v1 ~T_NonZero_112
v2 = Integer -> Integer -> T__'8804'__22
du_m'37'n'60'n_166 Integer
v0 Integer
v1
du_m'37'n'60'n_166 ::
Integer -> Integer -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_m'37'n'60'n_166 :: Integer -> Integer -> T__'8804'__22
du_m'37'n'60'n_166 Integer
v0 Integer
v1
= let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
Any -> T__'8804'__22
forall a b. a -> b
coe
((T__'8804'__22 -> T__'8804'__22) -> T__'8804'__22 -> Any
forall a b. a -> b
coe
T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Base.C_s'8804's_34
(Integer -> Integer -> Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.DivMod.Core.d_a'91'mod'8341''93'n'60'n_70
(Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe Integer
v2)))
d_m'37'n'8804'n_178 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_m'37'n'8804'n_178 :: Integer -> Integer -> T_NonZero_112 -> T__'8804'__22
d_m'37'n'8804'n_178 Integer
v0 Integer
v1 ~T_NonZero_112
v2 = Integer -> Integer -> T__'8804'__22
du_m'37'n'8804'n_178 Integer
v0 Integer
v1
du_m'37'n'8804'n_178 ::
Integer -> Integer -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_m'37'n'8804'n_178 :: Integer -> Integer -> T__'8804'__22
du_m'37'n'8804'n_178 Integer
v0 Integer
v1
= (T__'8804'__22 -> T__'8804'__22) -> Any -> T__'8804'__22
forall a b. a -> b
coe
T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'60''8658''8804'_2854
((Integer -> Integer -> T__'8804'__22) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> T__'8804'__22
du_m'37'n'60'n_166 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
d_m'37'n'8804'm_190 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_m'37'n'8804'm_190 :: Integer -> Integer -> T_NonZero_112 -> T__'8804'__22
d_m'37'n'8804'm_190 Integer
v0 Integer
v1 ~T_NonZero_112
v2 = Integer -> Integer -> T__'8804'__22
du_m'37'n'8804'm_190 Integer
v0 Integer
v1
du_m'37'n'8804'm_190 ::
Integer -> Integer -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_m'37'n'8804'm_190 :: Integer -> Integer -> T__'8804'__22
du_m'37'n'8804'm_190 Integer
v0 Integer
v1
= let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
Any -> T__'8804'__22
forall a b. a -> b
coe
((Integer -> Integer -> Integer -> T__'8804'__22)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.DivMod.Core.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
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v2))
d_m'8804'n'8658'm'37'n'8801'm_196 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_m'8804'n'8658'm'37'n'8801'm_196 :: Integer -> Integer -> T__'8804'__22 -> T__'8801'__12
d_m'8804'n'8658'm'37'n'8801'm_196 = Integer -> Integer -> T__'8804'__22 -> T__'8801'__12
forall a. a
erased
d_m'60'n'8658'm'37'n'8801'm_210 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_m'60'n'8658'm'37'n'8801'm_210 :: Integer
-> Integer -> T_NonZero_112 -> T__'8804'__22 -> T__'8801'__12
d_m'60'n'8658'm'37'n'8801'm_210 = Integer
-> Integer -> T_NonZero_112 -> T__'8804'__22 -> T__'8801'__12
forall a. a
erased
d_'37''45'pred'45''8801'0_220 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'37''45'pred'45''8801'0_220 :: Integer
-> Integer -> T_NonZero_112 -> T__'8801'__12 -> T__'8801'__12
d_'37''45'pred'45''8801'0_220 = Integer
-> Integer -> T_NonZero_112 -> T__'8801'__12 -> T__'8801'__12
forall a. a
erased
d_m'60''91'1'43'n'37'd'93''8658'm'8804''91'n'37'd'93'_236 ::
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_m'60''91'1'43'n'37'd'93''8658'm'8804''91'n'37'd'93'_236 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8804'__22
-> T__'8804'__22
d_m'60''91'1'43'n'37'd'93''8658'm'8804''91'n'37'd'93'_236 ~Integer
v0 Integer
v1 Integer
v2
~T_NonZero_112
v3
= Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
du_m'60''91'1'43'n'37'd'93''8658'm'8804''91'n'37'd'93'_236 Integer
v1 Integer
v2
du_m'60''91'1'43'n'37'd'93''8658'm'8804''91'n'37'd'93'_236 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_m'60''91'1'43'n'37'd'93''8658'm'8804''91'n'37'd'93'_236 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
du_m'60''91'1'43'n'37'd'93''8658'm'8804''91'n'37'd'93'_236 Integer
v0 Integer
v1
= case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
Integer
0 -> (Any -> Any) -> T__'8804'__22 -> T__'8804'__22
forall a b. a -> b
coe (\ Any
v2 -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
Integer
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
Any -> T__'8804'__22 -> T__'8804'__22
forall a b. a -> b
coe
((Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.DivMod.Core.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
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v2))
d_'91'1'43'm'37'd'93''8804'1'43'n'8658''91'm'37'd'93''8804'n_252 ::
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_'91'1'43'm'37'd'93''8804'1'43'n'8658''91'm'37'd'93''8804'n_252 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8804'__22
-> T__'8804'__22
-> T__'8804'__22
d_'91'1'43'm'37'd'93''8804'1'43'n'8658''91'm'37'd'93''8804'n_252 Integer
v0
~Integer
v1 Integer
v2 ~T_NonZero_112
v3 ~T__'8804'__22
v4
= Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
du_'91'1'43'm'37'd'93''8804'1'43'n'8658''91'm'37'd'93''8804'n_252
Integer
v0 Integer
v2
du_'91'1'43'm'37'd'93''8804'1'43'n'8658''91'm'37'd'93''8804'n_252 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_'91'1'43'm'37'd'93''8804'1'43'n'8658''91'm'37'd'93''8804'n_252 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
du_'91'1'43'm'37'd'93''8804'1'43'n'8658''91'm'37'd'93''8804'n_252 Integer
v0
Integer
v1
= case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
Integer
0 -> (Any -> Any) -> T__'8804'__22 -> T__'8804'__22
forall a b. a -> b
coe (\ Any
v2 -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
Integer
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
Any -> T__'8804'__22 -> T__'8804'__22
forall a b. a -> b
coe
((Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.DivMod.Core.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
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v2))
d_'37''45'distrib'737''45''43'_270 ::
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'37''45'distrib'737''45''43'_270 :: Integer -> Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
d_'37''45'distrib'737''45''43'_270 = Integer -> Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
forall a. a
erased
d_'37''45'distrib'737''45''42'_300 ::
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'37''45'distrib'737''45''42'_300 :: Integer -> Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
d_'37''45'distrib'737''45''42'_300 = Integer -> Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
forall a. a
erased
d_m'8242'_312 ::
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 -> Integer
d_m'8242'_312 :: Integer
-> Integer -> Integer -> T_NonZero_112 -> T_NonZero_112 -> Integer
d_m'8242'_312 Integer
v0 ~Integer
v1 Integer
v2 ~T_NonZero_112
v3 = Integer -> Integer -> T_NonZero_112 -> Integer
du_m'8242'_312 Integer
v0 Integer
v2
du_m'8242'_312 ::
Integer ->
Integer -> MAlonzo.Code.Data.Nat.Base.T_NonZero_112 -> Integer
du_m'8242'_312 :: Integer -> Integer -> T_NonZero_112 -> Integer
du_m'8242'_312 Integer
v0 Integer
v1 T_NonZero_112
v2
= (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'37'__326 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1)
d_n'8242'_314 ::
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 -> Integer
d_n'8242'_314 :: Integer
-> Integer -> Integer -> T_NonZero_112 -> T_NonZero_112 -> Integer
d_n'8242'_314 ~Integer
v0 Integer
v1 Integer
v2 ~T_NonZero_112
v3 = Integer -> Integer -> T_NonZero_112 -> Integer
du_n'8242'_314 Integer
v1 Integer
v2
du_n'8242'_314 ::
Integer ->
Integer -> MAlonzo.Code.Data.Nat.Base.T_NonZero_112 -> Integer
du_n'8242'_314 :: Integer -> Integer -> T_NonZero_112 -> Integer
du_n'8242'_314 Integer
v0 Integer
v1 T_NonZero_112
v2
= (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'37'__326 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1)
d_k_316 ::
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 -> Integer
d_k_316 :: Integer
-> Integer -> Integer -> T_NonZero_112 -> T_NonZero_112 -> Integer
d_k_316 Integer
v0 ~Integer
v1 Integer
v2 ~T_NonZero_112
v3 = Integer -> Integer -> T_NonZero_112 -> Integer
du_k_316 Integer
v0 Integer
v2
du_k_316 ::
Integer ->
Integer -> MAlonzo.Code.Data.Nat.Base.T_NonZero_112 -> Integer
du_k_316 :: Integer -> Integer -> T_NonZero_112 -> Integer
du_k_316 Integer
v0 Integer
v1 T_NonZero_112
v2
= (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1)
d_j_318 ::
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 -> Integer
d_j_318 :: Integer
-> Integer -> Integer -> T_NonZero_112 -> T_NonZero_112 -> Integer
d_j_318 ~Integer
v0 Integer
v1 Integer
v2 ~T_NonZero_112
v3 = Integer -> Integer -> T_NonZero_112 -> Integer
du_j_318 Integer
v1 Integer
v2
du_j_318 ::
Integer ->
Integer -> MAlonzo.Code.Data.Nat.Base.T_NonZero_112 -> Integer
du_j_318 :: Integer -> Integer -> T_NonZero_112 -> Integer
du_j_318 Integer
v0 Integer
v1 T_NonZero_112
v2
= (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1)
d_lemma_320 ::
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_lemma_320 :: Integer -> Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
d_lemma_320 = Integer -> Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
forall a. a
erased
d_'37''45'remove'45''43''737'_340 ::
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'37''45'remove'45''43''737'_340 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8739'__20
-> T__'8801'__12
d_'37''45'remove'45''43''737'_340 = Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8739'__20
-> T__'8801'__12
forall a. a
erased
d_'37''45'remove'45''43''691'_360 ::
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'37''45'remove'45''43''691'_360 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8739'__20
-> T__'8801'__12
d_'37''45'remove'45''43''691'_360 = Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8739'__20
-> T__'8801'__12
forall a. a
erased
d_'47''45'cong'737'_372 ::
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'47''45'cong'737'_372 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8801'__12
-> T__'8801'__12
d_'47''45'cong'737'_372 = Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
d_'47''45'cong'691'_378 ::
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'47''45'cong'691'_378 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T__'8801'__12
-> T__'8801'__12
d_'47''45'cong'691'_378 = Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
d_0'47'n'8801'0_384 ::
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_0'47'n'8801'0_384 :: Integer -> T_NonZero_112 -> T__'8801'__12
d_0'47'n'8801'0_384 = Integer -> T_NonZero_112 -> T__'8801'__12
forall a. a
erased
d_n'47'1'8801'n_388 ::
Integer -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_n'47'1'8801'n_388 :: Integer -> T__'8801'__12
d_n'47'1'8801'n_388 = Integer -> T__'8801'__12
forall a. a
erased
d_n'47'n'8801'1_396 ::
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_n'47'n'8801'1_396 :: Integer -> T_NonZero_112 -> T__'8801'__12
d_n'47'n'8801'1_396 = Integer -> T_NonZero_112 -> T__'8801'__12
forall a. a
erased
d_m'42'n'47'n'8801'm_406 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_m'42'n'47'n'8801'm_406 :: Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
d_m'42'n'47'n'8801'm_406 = Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
forall a. a
erased
d_m'47'n'42'n'8801'm_418 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_m'47'n'42'n'8801'm_418 :: Integer
-> Integer -> T_NonZero_112 -> T__'8739'__20 -> T__'8801'__12
d_m'47'n'42'n'8801'm_418 = Integer
-> Integer -> T_NonZero_112 -> T__'8739'__20 -> T__'8801'__12
forall a. a
erased
d_m'42''91'n'47'm'93''8801'n_428 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_m'42''91'n'47'm'93''8801'n_428 :: Integer
-> Integer -> T_NonZero_112 -> T__'8739'__20 -> T__'8801'__12
d_m'42''91'n'47'm'93''8801'n_428 = Integer
-> Integer -> T_NonZero_112 -> T__'8739'__20 -> T__'8801'__12
forall a. a
erased
d_m'47'n'42'n'8804'm_440 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_m'47'n'42'n'8804'm_440 :: Integer -> Integer -> T_NonZero_112 -> T__'8804'__22
d_m'47'n'42'n'8804'm_440 Integer
v0 Integer
v1 ~T_NonZero_112
v2
= Integer -> Integer -> T__'8804'__22
du_m'47'n'42'n'8804'm_440 Integer
v0 Integer
v1
du_m'47'n'42'n'8804'm_440 ::
Integer -> Integer -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_m'47'n'42'n'8804'm_440 :: Integer -> Integer -> T__'8804'__22
du_m'47'n'42'n'8804'm_440 Integer
v0 Integer
v1
= ((Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any)
-> Any -> Integer -> Integer -> Any -> T__'8804'__22
forall a b. a -> b
coe
(Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__46
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__78
-> Any)
-> Any -> (Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__78
-> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_start_96
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
(\ Any
v2 Any
v3 Any
v4 ->
(T__'8804'__22 -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'60''8658''8804'_2854 Any
v4))
(Integer -> Integer -> Integer
mulInt
((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
(Integer -> Integer
forall a b. a -> b
coe Integer
v1))
Integer
v0
(((Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Integer -> Integer -> Integer -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8804'_308
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78)
-> Any -> (Any -> Any -> Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_'8804''45'go_138
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
(\ Any
v2 Any
v3 Any
v4 Any
v5 Any
v6 ->
(T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''45''60''45'trans_2986 Any
v5
Any
v6))
(Integer -> Integer -> Integer
mulInt
((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
(Integer -> Integer
forall a b. a -> b
coe Integer
v1))
(Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'37'__326 (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 -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
mulInt
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (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
v1)))
Integer
v0
(((Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Integer
-> Integer
-> Integer
-> Any
-> Any
-> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''45''10217'_436
(\ Any
v2 Any
v3 Any
v4 Any
v5 Any
v6 -> Any
v6)
(Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'37'__326 (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 -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
mulInt
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (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
v1)))
(Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'37'__326 (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 -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
mulInt
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (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
v1)))
Integer
v0
(((Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Integer
-> Integer
-> Integer
-> Any
-> Any
-> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''45''10216'_448
(\ Any
v2 Any
v3 Any
v4 Any
v5 Any
v6 -> Any
v6)
(Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'37'__326 (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 -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
mulInt
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (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
v1)))
Integer
v0 Integer
v0
(((Any -> Any) -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any) -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_492
((T_IsPreorder_70 -> Any -> T__IsRelatedTo__78) -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70 -> Any -> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_stop_166
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810))
(Integer -> Any
forall a b. a -> b
coe Integer
v0))
Any
forall a. a
erased)
Any
forall a. a
erased)
((Integer -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_m'8804'm'43'n_3482
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
mulInt
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (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
v1))))
d_m'47'n'8804'm_452 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_m'47'n'8804'm_452 :: Integer -> Integer -> T_NonZero_112 -> T__'8804'__22
d_m'47'n'8804'm_452 Integer
v0 Integer
v1 ~T_NonZero_112
v2 = Integer -> Integer -> T__'8804'__22
du_m'47'n'8804'm_452 Integer
v0 Integer
v1
du_m'47'n'8804'm_452 ::
Integer -> Integer -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_m'47'n'8804'm_452 :: Integer -> Integer -> T__'8804'__22
du_m'47'n'8804'm_452 Integer
v0 Integer
v1
= (Integer -> T__'8804'__22) -> Any -> T__'8804'__22
forall a b. a -> b
coe
Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'42''45'cancel'691''45''8804'_4030
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
d_m'47'n'60'm_466 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_m'47'n'60'm_466 :: Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T__'8804'__22
-> T__'8804'__22
d_m'47'n'60'm_466 Integer
v0 Integer
v1 ~T_NonZero_112
v2 ~T_NonZero_112
v3 ~T__'8804'__22
v4 = Integer -> Integer -> T__'8804'__22
du_m'47'n'60'm_466 Integer
v0 Integer
v1
du_m'47'n'60'm_466 ::
Integer -> Integer -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_m'47'n'60'm_466 :: Integer -> Integer -> T__'8804'__22
du_m'47'n'60'm_466 Integer
v0 Integer
v1
= (Integer -> Integer -> Integer -> T__'8804'__22)
-> Any -> Any -> Any -> T__'8804'__22
forall a b. a -> b
coe
Integer -> Integer -> Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'42''45'cancel'691''45''60'_4192
(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
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (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
v0)
d_'47''45'mono'45''8804'_478 ::
Integer ->
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_'47''45'mono'45''8804'_478 :: Integer
-> Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T__'8804'__22
-> T__'8804'__22
-> T__'8804'__22
d_'47''45'mono'45''8804'_478 Integer
v0 Integer
v1 Integer
v2 Integer
v3 ~T_NonZero_112
v4 ~T_NonZero_112
v5 T__'8804'__22
v6 T__'8804'__22
v7
= Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__22
-> T__'8804'__22
-> T__'8804'__22
du_'47''45'mono'45''8804'_478 Integer
v0 Integer
v1 Integer
v2 Integer
v3 T__'8804'__22
v6 T__'8804'__22
v7
du_'47''45'mono'45''8804'_478 ::
Integer ->
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_'47''45'mono'45''8804'_478 :: Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__22
-> T__'8804'__22
-> T__'8804'__22
du_'47''45'mono'45''8804'_478 Integer
v0 Integer
v1 Integer
v2 Integer
v3 T__'8804'__22
v4 T__'8804'__22
v5
= case T__'8804'__22 -> T__'8804'__22
forall a b. a -> b
coe T__'8804'__22
v5 of
MAlonzo.Code.Data.Nat.Base.C_s'8804's_34 T__'8804'__22
v8
-> let v9 :: Integer
v9 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
Any -> T__'8804'__22
forall a b. a -> b
coe
(let v10 :: Integer
v10 = 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 -> Any
forall a b. a -> b
coe
((Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__22
-> T__'8804'__22
-> T__'8804'__22)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__22
-> T__'8804'__22
-> T__'8804'__22
MAlonzo.Code.Data.Nat.DivMod.Core.d_div'8341''45'mono'45''8804'_886
(Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v3)
(Integer -> Any
forall a b. a -> b
coe Integer
v9) (Integer -> Any
forall a b. a -> b
coe Integer
v10) (T__'8804'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
v4) (T__'8804'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
v8)))
T__'8804'__22
_ -> T__'8804'__22
forall a. a
MAlonzo.RTE.mazUnreachableError
d_'47''45'mono'737''45''8804'_488 ::
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_'47''45'mono'737''45''8804'_488 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8804'__22
-> T__'8804'__22
d_'47''45'mono'737''45''8804'_488 Integer
v0 Integer
v1 Integer
v2 ~T_NonZero_112
v3 T__'8804'__22
v4
= Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
du_'47''45'mono'737''45''8804'_488 Integer
v0 Integer
v1 Integer
v2 T__'8804'__22
v4
du_'47''45'mono'737''45''8804'_488 ::
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_'47''45'mono'737''45''8804'_488 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
du_'47''45'mono'737''45''8804'_488 Integer
v0 Integer
v1 Integer
v2 T__'8804'__22
v3
= (Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__22
-> T__'8804'__22
-> T__'8804'__22)
-> Any -> Any -> Any -> Any -> Any -> Any -> T__'8804'__22
forall a b. a -> b
coe
Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__22
-> T__'8804'__22
-> T__'8804'__22
du_'47''45'mono'45''8804'_478 (Integer -> Any
forall a b. a -> b
coe Integer
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1)
(T__'8804'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
v3)
((Integer -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'refl_2776 (Integer -> Any
forall a b. a -> b
coe Integer
v2))
d_'47''45'mono'691''45''8804'_504 ::
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_'47''45'mono'691''45''8804'_504 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T__'8804'__22
-> T__'8804'__22
d_'47''45'mono'691''45''8804'_504 Integer
v0 Integer
v1 Integer
v2 ~T_NonZero_112
v3 ~T_NonZero_112
v4 T__'8804'__22
v5
= Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
du_'47''45'mono'691''45''8804'_504 Integer
v0 Integer
v1 Integer
v2 T__'8804'__22
v5
du_'47''45'mono'691''45''8804'_504 ::
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_'47''45'mono'691''45''8804'_504 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
du_'47''45'mono'691''45''8804'_504 Integer
v0 Integer
v1 Integer
v2 T__'8804'__22
v3
= (Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__22
-> T__'8804'__22
-> T__'8804'__22)
-> Any -> Any -> Any -> Any -> Any -> Any -> T__'8804'__22
forall a b. a -> b
coe
Integer
-> Integer
-> Integer
-> Integer
-> T__'8804'__22
-> T__'8804'__22
-> T__'8804'__22
du_'47''45'mono'45''8804'_478 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v0)
((Integer -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'refl_2776 (Integer -> Any
forall a b. a -> b
coe Integer
v0))
(T__'8804'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
v3)
d_'47''45'cancel'691''45''8801'_518 ::
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'47''45'cancel'691''45''8801'_518 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8739'__20
-> T__'8739'__20
-> T__'8801'__12
-> T__'8801'__12
d_'47''45'cancel'691''45''8801'_518 = Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8739'__20
-> T__'8739'__20
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
d_m'60'n'8658'm'47'n'8801'0_540 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_m'60'n'8658'm'47'n'8801'0_540 :: Integer
-> Integer -> T_NonZero_112 -> T__'8804'__22 -> T__'8801'__12
d_m'60'n'8658'm'47'n'8801'0_540 = Integer
-> Integer -> T_NonZero_112 -> T__'8804'__22 -> T__'8801'__12
forall a. a
erased
d_m'8805'n'8658'm'47'n'62'0_554 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_m'8805'n'8658'm'47'n'62'0_554 :: Integer
-> Integer -> T_NonZero_112 -> T__'8804'__22 -> T__'8804'__22
d_m'8805'n'8658'm'47'n'62'0_554 Integer
v0 Integer
v1 ~T_NonZero_112
v2 T__'8804'__22
v3
= Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
du_m'8805'n'8658'm'47'n'62'0_554 Integer
v0 Integer
v1 T__'8804'__22
v3
du_m'8805'n'8658'm'47'n'62'0_554 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_m'8805'n'8658'm'47'n'62'0_554 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
du_m'8805'n'8658'm'47'n'62'0_554 Integer
v0 Integer
v1 T__'8804'__22
v2
= ((Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any)
-> Any -> Integer -> Any -> Any -> T__'8804'__22
forall a b. a -> b
coe
(Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__46
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__78
-> Any)
-> Any -> (Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__78
-> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_start_96
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
(\ Any
v3 Any
v4 Any
v5 ->
(T__'8804'__22 -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'60''8658''8804'_2854 Any
v5))
(Integer
1 :: Integer)
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
(((Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Integer
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''45''10216'_448
(\ Any
v3 Any
v4 Any
v5 Any
v6 Any
v7 -> Any
v7) (Integer
1 :: Integer)
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (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
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
(((Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8804'_308
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78)
-> Any -> (Any -> Any -> Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_'8804''45'go_138
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
(\ Any
v3 Any
v4 Any
v5 Any
v6 Any
v7 ->
(T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''45''60''45'trans_2986 Any
v6
Any
v7))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (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
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (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
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
(((Any -> Any) -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any) -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_492
((T_IsPreorder_70 -> Any -> T__IsRelatedTo__78) -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70 -> Any -> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_stop_166
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (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'__22 -> T__'8804'__22)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
du_'47''45'mono'691''45''8804'_504 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1)
(T__'8804'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
v2)))
Any
forall a. a
erased)
d_m'47'n'8801'0'8658'm'60'n_568 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_m'47'n'8801'0'8658'm'60'n_568 :: Integer
-> Integer -> T_NonZero_112 -> T__'8801'__12 -> T__'8804'__22
d_m'47'n'8801'0'8658'm'60'n_568 Integer
v0 Integer
v1 ~T_NonZero_112
v2 ~T__'8801'__12
v3
= Integer -> Integer -> T__'8804'__22
du_m'47'n'8801'0'8658'm'60'n_568 Integer
v0 Integer
v1
du_m'47'n'8801'0'8658'm'60'n_568 ::
Integer -> Integer -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_m'47'n'8801'0'8658'm'60'n_568 :: Integer -> Integer -> T__'8804'__22
du_m'47'n'8801'0'8658'm'60'n_568 Integer
v0 Integer
v1
= let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
Any -> T__'8804'__22
forall a b. a -> b
coe
(let v3 :: t
v3
= (T__'8846'__30 -> T__'8846'__30) -> Any -> t
forall a b. a -> b
coe
T__'8846'__30 -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.du_swap_78
(let v3 :: t
v3
= ((Any -> Any) -> (Any -> Any) -> T_Dec_20 -> T_Dec_20)
-> (Any -> Any) -> Any -> Any -> t
forall a b. a -> b
coe
(Any -> Any) -> (Any -> Any) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
(\ Any
v3 ->
(Integer -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''7495''8658''8804'_2746
(Integer -> Any
forall a b. a -> b
coe Integer
v1))
((T__'8804'__22 -> Any) -> Any
forall a b. a -> b
coe
T__'8804'__22 -> Any
MAlonzo.Code.Data.Nat.Properties.du_'8804''8658''8804''7495'_2758)
((Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
((Integer -> Integer -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Bool
ltInt (Integer -> Any
forall a b. a -> b
coe Integer
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v0))
((Bool -> T_Reflects_16) -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.d_T'45'reflects_66
((Integer -> Integer -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Bool
ltInt (Integer -> Any
forall a b. a -> b
coe Integer
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v0)))) in
Any -> Any
forall a b. a -> b
coe
(case Any -> T_Dec_20
forall a b. a -> b
coe Any
forall a. a
v3 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v4 T_Reflects_16
v5
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v4
then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v5 of
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 Any
v6
-> (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
forall a b. a -> b
coe Any
v6)
T_Reflects_16
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
else (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
v5)
((Any -> T__'8846'__30) -> Any -> Any
forall a b. a -> b
coe
Any -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42
((Integer -> Integer -> T__'8804'__22) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8816''8658''62'_2888
(Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v0)))
T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)) in
Any -> Any
forall a b. a -> b
coe
(case Any -> T__'8846'__30
forall a b. a -> b
coe Any
forall a. a
v3 of
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 Any
v4 -> Any -> Any
forall a b. a -> b
coe Any
v4
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 Any
v4
-> ((Any -> T_Irrelevant_20) -> Any) -> Any -> Any
forall a b. a -> b
coe
(Any -> T_Irrelevant_20) -> Any
MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_44
Any
forall a. a
erased
T__'8846'__30
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))
d_m'47'n'8802'0'8658'n'8804'm_608 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
(MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_m'47'n'8802'0'8658'n'8804'm_608 :: Integer
-> Integer
-> T_NonZero_112
-> (T__'8801'__12 -> T_Irrelevant_20)
-> T__'8804'__22
d_m'47'n'8802'0'8658'n'8804'm_608 Integer
v0 Integer
v1 ~T_NonZero_112
v2 ~T__'8801'__12 -> T_Irrelevant_20
v3
= Integer -> Integer -> T__'8804'__22
du_m'47'n'8802'0'8658'n'8804'm_608 Integer
v0 Integer
v1
du_m'47'n'8802'0'8658'n'8804'm_608 ::
Integer -> Integer -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_m'47'n'8802'0'8658'n'8804'm_608 :: Integer -> Integer -> T__'8804'__22
du_m'47'n'8802'0'8658'n'8804'm_608 Integer
v0 Integer
v1
= let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
Any -> T__'8804'__22
forall a b. a -> b
coe
(let v3 :: t
v3
= (T__'8846'__30 -> T__'8846'__30) -> Any -> t
forall a b. a -> b
coe
T__'8846'__30 -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.du_swap_78
(let v3 :: t
v3
= ((Any -> Any) -> (Any -> Any) -> T_Dec_20 -> T_Dec_20)
-> (Any -> Any) -> Any -> Any -> t
forall a b. a -> b
coe
(Any -> Any) -> (Any -> Any) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
(\ Any
v3 ->
(Integer -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''7495''8658''8804'_2746
(Integer -> Any
forall a b. a -> b
coe Integer
v1))
((T__'8804'__22 -> Any) -> Any
forall a b. a -> b
coe
T__'8804'__22 -> Any
MAlonzo.Code.Data.Nat.Properties.du_'8804''8658''8804''7495'_2758)
((Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
((Integer -> Integer -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Bool
ltInt (Integer -> Any
forall a b. a -> b
coe Integer
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v0))
((Bool -> T_Reflects_16) -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.d_T'45'reflects_66
((Integer -> Integer -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Bool
ltInt (Integer -> Any
forall a b. a -> b
coe Integer
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v0)))) in
Any -> Any
forall a b. a -> b
coe
(case Any -> T_Dec_20
forall a b. a -> b
coe Any
forall a. a
v3 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v4 T_Reflects_16
v5
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v4
then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v5 of
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 Any
v6
-> (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
forall a b. a -> b
coe Any
v6)
T_Reflects_16
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
else (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
v5)
((Any -> T__'8846'__30) -> Any -> Any
forall a b. a -> b
coe
Any -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42
((Integer -> Integer -> T__'8804'__22) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8816''8658''62'_2888
(Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v0)))
T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)) in
Any -> Any
forall a b. a -> b
coe
(case Any -> T__'8846'__30
forall a b. a -> b
coe Any
forall a. a
v3 of
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 Any
v4
-> ((Any -> T_Irrelevant_20) -> Any) -> Any -> Any
forall a b. a -> b
coe
(Any -> T_Irrelevant_20) -> Any
MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_44
Any
forall a. a
erased
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 Any
v4 -> Any -> Any
forall a b. a -> b
coe Any
v4
T__'8846'__30
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))
d_'43''45'distrib'45''47'_644 ::
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'43''45'distrib'45''47'_644 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8804'__22
-> T__'8801'__12
d_'43''45'distrib'45''47'_644 = Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8804'__22
-> T__'8801'__12
forall a. a
erased
d_'43''45'distrib'45''47''45''8739''737'_662 ::
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'43''45'distrib'45''47''45''8739''737'_662 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8739'__20
-> T__'8801'__12
d_'43''45'distrib'45''47''45''8739''737'_662 = Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8739'__20
-> T__'8801'__12
forall a. a
erased
d_'43''45'distrib'45''47''45''8739''691'_682 ::
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'43''45'distrib'45''47''45''8739''691'_682 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8739'__20
-> T__'8801'__12
d_'43''45'distrib'45''47''45''8739''691'_682 = Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8739'__20
-> T__'8801'__12
forall a. a
erased
d_m'47'n'8801'1'43''91'm'8760'n'93''47'n_700 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_m'47'n'8801'1'43''91'm'8760'n'93''47'n_700 :: Integer
-> Integer -> T_NonZero_112 -> T__'8804'__22 -> T__'8801'__12
d_m'47'n'8801'1'43''91'm'8760'n'93''47'n_700 = Integer
-> Integer -> T_NonZero_112 -> T__'8804'__22 -> T__'8801'__12
forall a. a
erased
d_'91'm'8760'n'93''47'n'8801'm'47'n'8760'1_718 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'91'm'8760'n'93''47'n'8801'm'47'n'8760'1_718 :: Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
d_'91'm'8760'n'93''47'n'8801'm'47'n'8760'1_718 = Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
forall a. a
erased
d_m'8739'n'8658'o'37'n'37'm'8801'o'37'm_750 ::
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_m'8739'n'8658'o'37'n'37'm'8801'o'37'm_750 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T__'8739'__20
-> T__'8801'__12
d_m'8739'n'8658'o'37'n'37'm'8801'o'37'm_750 = Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T__'8739'__20
-> T__'8801'__12
forall a. a
erased
d_pm_764 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
Integer -> MAlonzo.Code.Data.Nat.Base.T_NonZero_112 -> Integer
d_pm_764 :: Integer
-> Integer -> T_NonZero_112 -> Integer -> T_NonZero_112 -> Integer
d_pm_764 Integer
v0 ~Integer
v1 ~T_NonZero_112
v2 Integer
v3 ~T_NonZero_112
v4 = Integer -> Integer -> Integer
du_pm_764 Integer
v0 Integer
v3
du_pm_764 :: Integer -> Integer -> Integer
du_pm_764 :: Integer -> Integer -> Integer
du_pm_764 Integer
v0 Integer
v1 = (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
mulInt (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v0)
d_lem_766 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_lem_766 :: Integer
-> Integer
-> T_NonZero_112
-> Integer
-> T_NonZero_112
-> T__'8804'__22
d_lem_766 Integer
v0 Integer
v1 ~T_NonZero_112
v2 Integer
v3 ~T_NonZero_112
v4 = Integer -> Integer -> Integer -> T__'8804'__22
du_lem_766 Integer
v0 Integer
v1 Integer
v3
du_lem_766 ::
Integer ->
Integer -> Integer -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_lem_766 :: Integer -> Integer -> Integer -> T__'8804'__22
du_lem_766 Integer
v0 Integer
v1 Integer
v2
= ((Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any)
-> Any -> Integer -> Integer -> Any -> T__'8804'__22
forall a b. a -> b
coe
(Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__46
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__78
-> Any)
-> Any -> (Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__78
-> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_start_96
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
(\ Any
v3 Any
v4 Any
v5 ->
(T__'8804'__22 -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'60''8658''8804'_2854 Any
v5))
(Integer -> Integer -> Integer
mulInt
((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
mulInt
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (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
du_pm_764 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v2)))
(Integer -> Any
forall a b. a -> b
coe Integer
v2))
(Integer -> Integer
forall a b. a -> b
coe Integer
v0))
Integer
v1
(((Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Integer
-> Integer
-> Integer
-> Any
-> Any
-> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''45''10217'_436
(\ Any
v3 Any
v4 Any
v5 Any
v6 Any
v7 -> Any
v7)
(Integer -> Integer -> Integer
mulInt
((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
mulInt
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (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
du_pm_764 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v2)))
(Integer -> Any
forall a b. a -> b
coe Integer
v2))
(Integer -> Integer
forall a b. a -> b
coe Integer
v0))
(Integer -> Integer -> Integer
mulInt
((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (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
du_pm_764 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v2)))
((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
du_pm_764 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v2)))
Integer
v1
(((Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Integer -> Integer -> Integer -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8804'_308
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78)
-> Any -> (Any -> Any -> Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_'8804''45'go_138
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
(\ Any
v3 Any
v4 Any
v5 Any
v6 Any
v7 ->
(T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''45''60''45'trans_2986 Any
v6
Any
v7))
(Integer -> Integer -> Integer
mulInt
((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (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
du_pm_764 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v2)))
((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
du_pm_764 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v2)))
Integer
v1 Integer
v1
(((Any -> Any) -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any) -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_492
((T_IsPreorder_70 -> Any -> T__IsRelatedTo__78) -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70 -> Any -> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_stop_166
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810))
(Integer -> Any
forall a b. a -> b
coe Integer
v1))
((Integer -> Integer -> T__'8804'__22) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> T__'8804'__22
du_m'47'n'42'n'8804'm_440 (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
du_pm_764 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v2))))
Any
forall a. a
erased)
d_m'42'n'47'm'42'o'8801'n'47'o_780 ::
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_m'42'n'47'm'42'o'8801'n'47'o_780 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T__'8801'__12
d_m'42'n'47'm'42'o'8801'n'47'o_780 = Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T__'8801'__12
forall a. a
erased
d_helper_796 ::
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
Integer ->
MAlonzo.Code.Induction.WellFounded.T_Acc_42 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_helper_796 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> Integer
-> T_Acc_42
-> T__'8801'__12
d_helper_796 = Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> Integer
-> T_Acc_42
-> T__'8801'__12
forall a. a
erased
d_n'8760'o'60'n_828 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
(Integer ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
MAlonzo.Code.Induction.WellFounded.T_Acc_42) ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_n'8760'o'60'n_828 :: Integer
-> Integer
-> T__'8804'__22
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> (Integer -> T__'8804'__22 -> T_Acc_42)
-> T__'8804'__22
d_n'8760'o'60'n_828 Integer
v0 Integer
v1 T__'8804'__22
v2 ~Integer
v3 ~Integer
v4 ~T_NonZero_112
v5 ~T_NonZero_112
v6 ~Integer -> T__'8804'__22 -> T_Acc_42
v7
= Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
du_n'8760'o'60'n_828 Integer
v0 Integer
v1 T__'8804'__22
v2
du_n'8760'o'60'n_828 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_n'8760'o'60'n_828 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
du_n'8760'o'60'n_828 Integer
v0 Integer
v1 T__'8804'__22
v2
= (Integer
-> Integer
-> Integer
-> T__'8804'__22
-> T__'8804'__22
-> T__'8804'__22)
-> Any -> Any -> Any -> Any -> Any -> T__'8804'__22
forall a b. a -> b
coe
Integer
-> Integer
-> Integer
-> T__'8804'__22
-> T__'8804'__22
-> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.d_'8760''45'mono'691''45''60'_5134
(Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
((Integer -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_n'8802'0'8658'n'62'0_3090
(Integer -> Any
forall a b. a -> b
coe Integer
v0))
(T__'8804'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
v2)
d_m'42'n'47'o'42'n'8801'm'47'o_842 ::
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_m'42'n'47'o'42'n'8801'm'47'o_842 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T__'8801'__12
d_m'42'n'47'o'42'n'8801'm'47'o_842 = Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T__'8801'__12
forall a. a
erased
d_m'60'n'42'o'8658'm'47'o'60'n_866 ::
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_m'60'n'42'o'8658'm'47'o'60'n_866 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8804'__22
-> T__'8804'__22
d_m'60'n'42'o'8658'm'47'o'60'n_866 Integer
v0 Integer
v1 Integer
v2 ~T_NonZero_112
v3 ~T__'8804'__22
v4
= Integer -> Integer -> Integer -> T__'8804'__22
du_m'60'n'42'o'8658'm'47'o'60'n_866 Integer
v0 Integer
v1 Integer
v2
du_m'60'n'42'o'8658'm'47'o'60'n_866 ::
Integer ->
Integer -> Integer -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_m'60'n'42'o'8658'm'47'o'60'n_866 :: Integer -> Integer -> Integer -> T__'8804'__22
du_m'60'n'42'o'8658'm'47'o'60'n_866 Integer
v0 Integer
v1 Integer
v2
= case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
Integer
1 -> let v3 :: Integer
v3 = Integer -> Integer -> Integer
mulInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v2) in
Any -> T__'8804'__22
forall a b. a -> b
coe
(let v4 :: b
v4
= T_SubRelation_60 -> b
forall a b. a -> b
coe
T_SubRelation_60
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_strictRelation_202 in
Any -> Any
forall a b. a -> b
coe
((T_SubRelation_60 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_SubRelation_60 -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__126
(Any -> Any
forall a b. a -> b
coe Any
forall a. a
v4)
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (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
1 :: Integer))
(((Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Integer
-> Integer
-> Any
-> Any
-> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''45''10217'_436
(\ Any
v5 Any
v6 Any
v7 Any
v8 Any
v9 -> Any
v9)
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v3))
(Integer
0 :: Integer) (Integer
1 :: Integer)
(((Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Integer -> Integer -> Integer -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''60'_312
(((Any -> Any -> Any -> Any -> Any -> Any)
-> T_Σ_14
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> Any -> Any -> Any)
-> T_Σ_14
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_'60''45'go_152
(\ Any
v5 Any
v6 Any
v7 Any
v8 Any
v9 ->
(Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'60''45'trans_2980 Any
v6 Any
v8 Any
v9)
(T_Σ_14 -> Any
forall a b. a -> b
coe
T_Σ_14
MAlonzo.Code.Relation.Binary.PropositionalEquality.Core.du_resp'8322'_160)
(\ Any
v5 Any
v6 Any
v7 Any
v8 Any
v9 ->
(T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'60''45''8804''45'trans_2992 Any
v8
Any
v9))
(Integer
0 :: Integer) (Integer
1 :: Integer) (Integer
1 :: Integer)
(((Any -> Any) -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any) -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_492
((T_IsPreorder_70 -> Any -> T__IsRelatedTo__78) -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70 -> Any -> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_stop_166
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810))
(Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)))
((T__'8804'__22 -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe
T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Base.C_s'8804's_34
(T__'8804'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
MAlonzo.Code.Data.Nat.Base.C_z'8804'n_26)))
Any
forall a. a
erased)))
Integer
_ -> (Integer -> Integer -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Integer -> Any -> T__'8804'__22
forall a b. a -> b
coe
Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.d_pred'45'cancel'45''60'_5686
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v2)) Integer
v1
(let v3 :: b
v3
= T_SubRelation_60 -> b
forall a b. a -> b
coe
T_SubRelation_60
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_strictRelation_202 in
Any -> Any
forall a b. a -> b
coe
((T_SubRelation_60 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_SubRelation_60 -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__126
(Any -> Any
forall a b. a -> b
coe Any
forall a. a
v3)
((Integer -> Integer) -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer
MAlonzo.Code.Data.Nat.Base.d_pred_192
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v2)))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
subInt (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)))
(((Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Integer
-> Any
-> Integer
-> Any
-> Any
-> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''45''10216'_448
(\ Any
v4 Any
v5 Any
v6 Any
v7 Any
v8 -> Any
v8)
(Integer -> Integer
MAlonzo.Code.Data.Nat.Base.d_pred_192
((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v2)))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314
((Integer -> Integer -> Integer) -> Integer -> Integer -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22 Integer
v0 Integer
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v2))
(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)))
(((Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Integer -> Integer -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''60'_312
(((Any -> Any -> Any -> Any -> Any -> Any)
-> T_Σ_14
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> Any -> Any -> Any)
-> T_Σ_14
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_'60''45'go_152
(\ Any
v4 Any
v5 Any
v6 Any
v7 Any
v8 ->
(Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'60''45'trans_2980 Any
v5 Any
v7 Any
v8)
(T_Σ_14 -> Any
forall a b. a -> b
coe
T_Σ_14
MAlonzo.Code.Relation.Binary.PropositionalEquality.Core.du_resp'8322'_160)
(\ Any
v4 Any
v5 Any
v6 Any
v7 Any
v8 ->
(T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'60''45''8804''45'trans_2992 Any
v7
Any
v8))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314
((Integer -> Integer -> Integer) -> Integer -> Integer -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22 Integer
v0 Integer
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v2))
(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)))
(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)))
(((Any -> Any) -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any) -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_492
((T_IsPreorder_70 -> Any -> T__IsRelatedTo__78) -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70 -> Any -> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_stop_166
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
subInt (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))))
((Integer -> Integer -> Integer -> T__'8804'__22)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer -> T__'8804'__22
du_m'60'n'42'o'8658'm'47'o'60'n_866
((Integer -> Integer -> Integer) -> Integer -> Integer -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22 Integer
v0 Integer
v2)
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
subInt (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))) (Integer -> Any
forall a b. a -> b
coe Integer
v2)))
Any
forall a. a
erased)))
d_'91'm'8760'n'42'o'93''47'o'8801'm'47'o'8760'n_900 ::
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'91'm'8760'n'42'o'93''47'o'8801'm'47'o'8760'n_900 :: Integer -> Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
d_'91'm'8760'n'42'o'93''47'o'8801'm'47'o'8760'n_900 = Integer -> Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
forall a. a
erased
d_m'47'n'47'o'8801'm'47''91'n'42'o'93'_926 ::
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_m'47'n'47'o'8801'm'47''91'n'42'o'93'_926 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T_NonZero_112
-> T__'8801'__12
d_m'47'n'47'o'8801'm'47''91'n'42'o'93'_926 = Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T_NonZero_112
-> T__'8801'__12
forall a. a
erased
d_n'42'o_938 ::
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 -> Integer
d_n'42'o_938 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T_NonZero_112
-> Integer
d_n'42'o_938 ~Integer
v0 Integer
v1 Integer
v2 ~T_NonZero_112
v3 ~T_NonZero_112
v4 ~T_NonZero_112
v5 = Integer -> Integer -> Integer
du_n'42'o_938 Integer
v1 Integer
v2
du_n'42'o_938 :: Integer -> Integer -> Integer
du_n'42'o_938 :: Integer -> Integer -> Integer
du_n'42'o_938 Integer
v0 Integer
v1 = (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
mulInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1)
d_o'42'n_940 ::
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 -> Integer
d_o'42'n_940 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T_NonZero_112
-> Integer
d_o'42'n_940 ~Integer
v0 Integer
v1 Integer
v2 ~T_NonZero_112
v3 ~T_NonZero_112
v4 ~T_NonZero_112
v5 = Integer -> Integer -> Integer
du_o'42'n_940 Integer
v1 Integer
v2
du_o'42'n_940 :: Integer -> Integer -> Integer
du_o'42'n_940 :: Integer -> Integer -> Integer
du_o'42'n_940 Integer
v0 Integer
v1 = (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
mulInt (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v0)
d_lem'8321'_942 ::
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
d_lem'8321'_942 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T_NonZero_112
-> T__'8739'__20
d_lem'8321'_942 Integer
v0 Integer
v1 Integer
v2 ~T_NonZero_112
v3 ~T_NonZero_112
v4 ~T_NonZero_112
v5 = Integer -> Integer -> Integer -> T__'8739'__20
du_lem'8321'_942 Integer
v0 Integer
v1 Integer
v2
du_lem'8321'_942 ::
Integer ->
Integer ->
Integer -> MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
du_lem'8321'_942 :: Integer -> Integer -> Integer -> T__'8739'__20
du_lem'8321'_942 Integer
v0 Integer
v1 Integer
v2
= (Integer -> T__'8739'__20) -> Integer -> T__'8739'__20
forall a b. a -> b
coe
Integer -> T__'8739'__20
MAlonzo.Code.Data.Nat.Divisibility.Core.C_divides_34
(Integer -> Integer -> Integer
mulInt
((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (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
du_n'42'o_938 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v2)))
(Integer -> Integer
forall a b. a -> b
coe Integer
v2))
d_lem'8322'_946 ::
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_lem'8322'_946 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T_NonZero_112
-> T__'8801'__12
d_lem'8322'_946 = Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T_NonZero_112
-> T__'8801'__12
forall a. a
erased
d_lem'8323'_950 ::
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_lem'8323'_950 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T_NonZero_112
-> T__'8804'__22
d_lem'8323'_950 Integer
v0 Integer
v1 Integer
v2 ~T_NonZero_112
v3 ~T_NonZero_112
v4 ~T_NonZero_112
v5 = Integer -> Integer -> Integer -> T__'8804'__22
du_lem'8323'_950 Integer
v0 Integer
v1 Integer
v2
du_lem'8323'_950 ::
Integer ->
Integer -> Integer -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_lem'8323'_950 :: Integer -> Integer -> Integer -> T__'8804'__22
du_lem'8323'_950 Integer
v0 Integer
v1 Integer
v2
= let v3 :: b
v3
= T_SubRelation_60 -> b
forall a b. a -> b
coe
T_SubRelation_60
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_strictRelation_202 in
Any -> T__'8804'__22
forall a b. a -> b
coe
((T_SubRelation_60 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_SubRelation_60 -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__126
(Any -> Any
forall a b. a -> b
coe Any
forall a. a
v3)
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'37'__326 (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
du_n'42'o_938 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v2)))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_o'42'n_940 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v2))
(((Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''60'_312
(((Any -> Any -> Any -> Any -> Any -> Any)
-> T_Σ_14
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> Any -> Any -> Any)
-> T_Σ_14
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_'60''45'go_152
(\ Any
v4 Any
v5 Any
v6 Any
v7 Any
v8 ->
(Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'60''45'trans_2980 Any
v5 Any
v7 Any
v8)
(T_Σ_14 -> Any
forall a b. a -> b
coe
T_Σ_14
MAlonzo.Code.Relation.Binary.PropositionalEquality.Core.du_resp'8322'_160)
(\ Any
v4 Any
v5 Any
v6 Any
v7 Any
v8 ->
(T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'60''45''8804''45'trans_2992 Any
v7
Any
v8))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'37'__326 (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
du_n'42'o_938 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v2)))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_n'42'o_938 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v2))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_o'42'n_940 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v2))
(((Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''45''10217'_436
(\ Any
v4 Any
v5 Any
v6 Any
v7 Any
v8 -> Any
v8) ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_n'42'o_938 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v2))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_o'42'n_940 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v2))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_o'42'n_940 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v2))
(((Any -> Any) -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any) -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_492
((T_IsPreorder_70 -> Any -> T__IsRelatedTo__78) -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70 -> Any -> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_stop_166
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_o'42'n_940 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v2)))
Any
forall a. a
erased)
((Integer -> Integer -> T__'8804'__22) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> T__'8804'__22
du_m'37'n'60'n_166 (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
du_n'42'o_938 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v2)))))
d_'42''45''47''45'assoc_966 ::
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'42''45''47''45'assoc_966 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8739'__20
-> T__'8801'__12
d_'42''45''47''45'assoc_966 = Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8739'__20
-> T__'8801'__12
forall a. a
erased
d_'47''45''42''45'interchange_988 ::
Integer ->
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'47''45''42''45'interchange_988 :: Integer
-> Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T_NonZero_112
-> T__'8739'__20
-> T__'8739'__20
-> T__'8801'__12
d_'47''45''42''45'interchange_988 = Integer
-> Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T_NonZero_112
-> T__'8739'__20
-> T__'8739'__20
-> T__'8801'__12
forall a. a
erased
d_m'42'n'47'm'33''8801'n'47''91'm'8760'1'93''33'_1012 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_m'42'n'47'm'33''8801'n'47''91'm'8760'1'93''33'_1012 :: Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
d_m'42'n'47'm'33''8801'n'47''91'm'8760'1'93''33'_1012 = Integer -> Integer -> T_NonZero_112 -> T__'8801'__12
forall a. a
erased
d_m'37''91'n'42'o'93''47'o'8801'm'47'o'37'n_1040 ::
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_m'37''91'n'42'o'93''47'o'8801'm'47'o'37'n_1040 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T_NonZero_112
-> T__'8801'__12
d_m'37''91'n'42'o'93''47'o'8801'm'47'o'37'n_1040 = Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T_NonZero_112
-> T__'8801'__12
forall a. a
erased
d_m'37'n'42'o'8801'm'42'o'37''91'n'42'o'93'_1070 ::
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_m'37'n'42'o'8801'm'42'o'37''91'n'42'o'93'_1070 :: Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T__'8801'__12
d_m'37'n'42'o'8801'm'42'o'37''91'n'42'o'93'_1070 = Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T_NonZero_112
-> T__'8801'__12
forall a. a
erased
d_'91'm'42'n'43'o'93''37''91'p'42'n'93''8801''91'm'42'n'93''37''91'p'42'n'93''43'o_1094 ::
Integer ->
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'91'm'42'n'43'o'93''37''91'p'42'n'93''8801''91'm'42'n'93''37''91'p'42'n'93''43'o_1094 :: Integer
-> Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8804'__22
-> T__'8801'__12
d_'91'm'42'n'43'o'93''37''91'p'42'n'93''8801''91'm'42'n'93''37''91'p'42'n'93''43'o_1094
= Integer
-> Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8804'__22
-> T__'8801'__12
forall a. a
erased
d_mn_1112 ::
Integer ->
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22 -> Integer
d_mn_1112 :: Integer
-> Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8804'__22
-> Integer
d_mn_1112 Integer
v0 Integer
v1 ~Integer
v2 ~Integer
v3 ~T_NonZero_112
v4 ~T__'8804'__22
v5 = Integer -> Integer -> Integer
du_mn_1112 Integer
v0 Integer
v1
du_mn_1112 :: Integer -> Integer -> Integer
du_mn_1112 :: Integer -> Integer -> Integer
du_mn_1112 Integer
v0 Integer
v1 = (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
mulInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1)
d_pn_1114 ::
Integer ->
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22 -> Integer
d_pn_1114 :: Integer
-> Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8804'__22
-> Integer
d_pn_1114 ~Integer
v0 Integer
v1 ~Integer
v2 Integer
v3 ~T_NonZero_112
v4 ~T__'8804'__22
v5 = Integer -> Integer -> Integer
du_pn_1114 Integer
v1 Integer
v3
du_pn_1114 :: Integer -> Integer -> Integer
du_pn_1114 :: Integer -> Integer -> Integer
du_pn_1114 Integer
v0 Integer
v1
= (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
mulInt ((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
v0)
d_lem'8321'_1116 ::
Integer ->
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_lem'8321'_1116 :: Integer
-> Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8804'__22
-> T__'8804'__22
d_lem'8321'_1116 Integer
v0 Integer
v1 ~Integer
v2 Integer
v3 ~T_NonZero_112
v4 ~T__'8804'__22
v5 = Integer -> Integer -> Integer -> T__'8804'__22
du_lem'8321'_1116 Integer
v0 Integer
v1 Integer
v3
du_lem'8321'_1116 ::
Integer ->
Integer -> Integer -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_lem'8321'_1116 :: Integer -> Integer -> Integer -> T__'8804'__22
du_lem'8321'_1116 Integer
v0 Integer
v1 Integer
v2
= ((Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any)
-> Any -> Any -> Integer -> Any -> T__'8804'__22
forall a b. a -> b
coe
(Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__46
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__78
-> Any)
-> Any -> (Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any)
-> Any
-> Any
-> T__IsRelatedTo__78
-> Any
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_start_96
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
(\ Any
v3 Any
v4 Any
v5 ->
(T__'8804'__22 -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'60''8658''8804'_2854 Any
v5))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'37'__326
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_mn_1112 (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
du_pn_1114 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v2)))
(Integer -> Integer -> Integer
mulInt (Integer -> Integer
forall a b. a -> b
coe Integer
v2) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
(((Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Integer
-> Integer
-> Any
-> Any
-> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''45''10216'_448
(\ Any
v3 Any
v4 Any
v5 Any
v6 Any
v7 -> Any
v7)
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'37'__326
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_mn_1112 (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
du_pn_1114 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v2)))
(Integer -> Integer -> Integer
mulInt
((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'37'__326 (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
v2)))
(Integer -> Integer
forall a b. a -> b
coe Integer
v1))
(Integer -> Integer -> Integer
mulInt (Integer -> Integer
forall a b. a -> b
coe Integer
v2) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
(((Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Integer -> Integer -> Integer -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8804'_308
((T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78)
-> Any -> (Any -> Any -> Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_'8804''45'go_138
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
(\ Any
v3 Any
v4 Any
v5 Any
v6 Any
v7 ->
(T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''45''60''45'trans_2986 Any
v6
Any
v7))
(Integer -> Integer -> Integer
mulInt
((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'37'__326 (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
v2)))
(Integer -> Integer
forall a b. a -> b
coe Integer
v1))
(Integer -> Integer -> Integer
mulInt (Integer -> Integer
forall a b. a -> b
coe Integer
v2) (Integer -> Integer
forall a b. a -> b
coe Integer
v1)) (Integer -> Integer -> Integer
mulInt (Integer -> Integer
forall a b. a -> b
coe Integer
v2) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
(((Any -> Any) -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any) -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_492
((T_IsPreorder_70 -> Any -> T__IsRelatedTo__78) -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70 -> Any -> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_stop_166
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
mulInt (Integer -> Any
forall a b. a -> b
coe Integer
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
((Integer -> Integer -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'42''45'mono'737''45''8804'_4070
(Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v2)
((T__'8804'__22 -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe
T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_m'60'1'43'n'8658'm'8804'n_3122
((Integer -> Integer -> T__'8804'__22) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> T__'8804'__22
du_m'37'n'60'n_166 (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
v2))))))
Any
forall a. a
erased)
d_lem'8322'_1118 ::
Integer ->
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_lem'8322'_1118 :: Integer
-> Integer
-> Integer
-> Integer
-> T_NonZero_112
-> T__'8804'__22
-> T__'8804'__22
d_lem'8322'_1118 Integer
v0 Integer
v1 Integer
v2 Integer
v3 ~T_NonZero_112
v4 T__'8804'__22
v5
= Integer
-> Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
du_lem'8322'_1118 Integer
v0 Integer
v1 Integer
v2 Integer
v3 T__'8804'__22
v5
du_lem'8322'_1118 ::
Integer ->
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_lem'8322'_1118 :: Integer
-> Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22
du_lem'8322'_1118 Integer
v0 Integer
v1 Integer
v2 Integer
v3 T__'8804'__22
v4
= let v5 :: b
v5
= T_SubRelation_60 -> b
forall a b. a -> b
coe
T_SubRelation_60
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_strictRelation_202 in
Any -> T__'8804'__22
forall a b. a -> b
coe
((T_SubRelation_60 -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_SubRelation_60 -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__126
(Any -> Any
forall a b. a -> b
coe Any
forall a. a
v5)
((Integer -> Integer -> Integer) -> Any -> Any -> Any
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
MAlonzo.Code.Data.Nat.Base.du__'37'__326
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_mn_1112 (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
du_pn_1114 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v3)))
(Integer -> Any
forall a b. a -> b
coe Integer
v2))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_pn_1114 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v3))
(((Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Integer -> Integer -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''60'_312
(((Any -> Any -> Any -> Any -> Any -> Any)
-> T_Σ_14
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> Any -> Any -> Any)
-> T_Σ_14
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_'60''45'go_152
(\ Any
v6 Any
v7 Any
v8 Any
v9 Any
v10 ->
(Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'60''45'trans_2980 Any
v7 Any
v9 Any
v10)
(T_Σ_14 -> Any
forall a b. a -> b
coe
T_Σ_14
MAlonzo.Code.Relation.Binary.PropositionalEquality.Core.du_resp'8322'_160)
(\ Any
v6 Any
v7 Any
v8 Any
v9 Any
v10 ->
(T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'60''45''8804''45'trans_2992 Any
v9
Any
v10))
(Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'37'__326
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_mn_1112 (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
du_pn_1114 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v3)))
(Integer -> Integer
forall a b. a -> b
coe Integer
v2))
(Integer -> Integer -> Integer
addInt ((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
mulInt (Integer -> Any
forall a b. a -> b
coe Integer
v3) (Integer -> Any
forall a b. a -> b
coe Integer
v1)) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_pn_1114 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v3))
(((Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Integer
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> T__'8801'__12 -> Any -> Any)
-> Any -> Any -> Any -> Any -> T__'8801'__12 -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''45''10217'_436
(\ Any
v6 Any
v7 Any
v8 Any
v9 Any
v10 -> Any
v10)
(Integer -> Integer -> Integer
addInt ((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
mulInt (Integer -> Any
forall a b. a -> b
coe Integer
v3) (Integer -> Any
forall a b. a -> b
coe Integer
v1)) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_pn_1114 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (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
du_pn_1114 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v3))
(((Any -> Any) -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any) -> Any -> Any
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_492
((T_IsPreorder_70 -> Any -> T__IsRelatedTo__78) -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70 -> Any -> T__IsRelatedTo__78
MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_stop_166
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_pn_1114 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v3)))
Any
forall a. a
erased)
((Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'43''45'mono'45''8804''45''60'_3570
(Integer -> Any
forall a b. a -> b
coe Integer
v1) ((Integer -> Integer -> Integer -> T__'8804'__22)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer -> T__'8804'__22
du_lem'8321'_1116 (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
v3))
(T__'8804'__22 -> Any
forall a b. a -> b
coe T__'8804'__22
v4))))
d_DivMod_1126 :: p -> p -> ()
d_DivMod_1126 p
a0 p
a1 = ()
data T_DivMod_1126
= C_result_1146 Integer MAlonzo.Code.Data.Fin.Base.T_Fin_10
d_quotient_1138 :: T_DivMod_1126 -> Integer
d_quotient_1138 :: T_DivMod_1126 -> Integer
d_quotient_1138 T_DivMod_1126
v0
= case T_DivMod_1126 -> T_DivMod_1126
forall a b. a -> b
coe T_DivMod_1126
v0 of
C_result_1146 Integer
v1 T_Fin_10
v2 -> Integer -> Integer
forall a b. a -> b
coe Integer
v1
T_DivMod_1126
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
d_remainder_1140 ::
T_DivMod_1126 -> MAlonzo.Code.Data.Fin.Base.T_Fin_10
d_remainder_1140 :: T_DivMod_1126 -> T_Fin_10
d_remainder_1140 T_DivMod_1126
v0
= case T_DivMod_1126 -> T_DivMod_1126
forall a b. a -> b
coe T_DivMod_1126
v0 of
C_result_1146 Integer
v1 T_Fin_10
v2 -> T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v2
T_DivMod_1126
_ -> T_Fin_10
forall a. a
MAlonzo.RTE.mazUnreachableError
d_property_1142 ::
T_DivMod_1126 -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_property_1142 :: T_DivMod_1126 -> T__'8801'__12
d_property_1142 = T_DivMod_1126 -> T__'8801'__12
forall a. a
erased
d_nonZeroDivisor_1144 ::
Integer ->
Integer ->
T_DivMod_1126 -> MAlonzo.Code.Data.Nat.Base.T_NonZero_112
d_nonZeroDivisor_1144 :: Integer -> Integer -> T_DivMod_1126 -> T_NonZero_112
d_nonZeroDivisor_1144 ~Integer
v0 ~Integer
v1 ~T_DivMod_1126
v2 = T_NonZero_112
du_nonZeroDivisor_1144
du_nonZeroDivisor_1144 :: MAlonzo.Code.Data.Nat.Base.T_NonZero_112
du_nonZeroDivisor_1144 :: T_NonZero_112
du_nonZeroDivisor_1144
= T_NonZero_112 -> T_NonZero_112
forall a b. a -> b
coe T_NonZero_112
MAlonzo.Code.Data.Fin.Properties.du_nonZeroIndex_22
d__div__1154 ::
Integer ->
Integer -> MAlonzo.Code.Data.Nat.Base.T_NonZero_112 -> Integer
d__div__1154 :: Integer -> Integer -> T_NonZero_112 -> Integer
d__div__1154 Integer
v0 Integer
v1 T_NonZero_112
v2
= (Integer -> Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 Integer
v0 Integer
v1
d__mod__1162 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Fin.Base.T_Fin_10
d__mod__1162 :: Integer -> Integer -> T_NonZero_112 -> T_Fin_10
d__mod__1162 Integer
v0 Integer
v1 ~T_NonZero_112
v2 = Integer -> Integer -> T_Fin_10
du__mod__1162 Integer
v0 Integer
v1
du__mod__1162 ::
Integer -> Integer -> MAlonzo.Code.Data.Fin.Base.T_Fin_10
du__mod__1162 :: Integer -> Integer -> T_Fin_10
du__mod__1162 Integer
v0 Integer
v1
= (Integer -> T_Fin_10) -> Any -> T_Fin_10
forall a b. a -> b
coe
Integer -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.du_fromℕ'60'_52
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'37'__326 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
d__divMod__1174 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 -> T_DivMod_1126
d__divMod__1174 :: Integer -> Integer -> T_NonZero_112 -> T_DivMod_1126
d__divMod__1174 Integer
v0 Integer
v1 ~T_NonZero_112
v2 = Integer -> Integer -> T_DivMod_1126
du__divMod__1174 Integer
v0 Integer
v1
du__divMod__1174 :: Integer -> Integer -> T_DivMod_1126
du__divMod__1174 :: Integer -> Integer -> T_DivMod_1126
du__divMod__1174 Integer
v0 Integer
v1
= (Integer -> T_Fin_10 -> T_DivMod_1126)
-> Any -> Any -> T_DivMod_1126
forall a b. a -> b
coe
Integer -> T_Fin_10 -> T_DivMod_1126
C_result_1146
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
((Integer -> Integer -> T_Fin_10) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> T_Fin_10
du__mod__1162 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
d_'91'm'47'n'93''42'n_1184 ::
Integer ->
Integer -> MAlonzo.Code.Data.Nat.Base.T_NonZero_112 -> Integer
d_'91'm'47'n'93''42'n_1184 :: Integer -> Integer -> T_NonZero_112 -> Integer
d_'91'm'47'n'93''42'n_1184 Integer
v0 Integer
v1 ~T_NonZero_112
v2
= Integer -> Integer -> Integer
du_'91'm'47'n'93''42'n_1184 Integer
v0 Integer
v1
du_'91'm'47'n'93''42'n_1184 :: Integer -> Integer -> Integer
du_'91'm'47'n'93''42'n_1184 :: Integer -> Integer -> Integer
du_'91'm'47'n'93''42'n_1184 Integer
v0 Integer
v1
= (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
mulInt
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314 (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
v1)
d_'91'm'37'n'93''60'n_1186 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_'91'm'37'n'93''60'n_1186 :: Integer
-> Integer -> T_NonZero_112 -> T_NonZero_112 -> T__'8804'__22
d_'91'm'37'n'93''60'n_1186 Integer
v0 Integer
v1 ~T_NonZero_112
v2
= Integer -> Integer -> T_NonZero_112 -> T__'8804'__22
du_'91'm'37'n'93''60'n_1186 Integer
v0 Integer
v1
du_'91'm'37'n'93''60'n_1186 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_'91'm'37'n'93''60'n_1186 :: Integer -> Integer -> T_NonZero_112 -> T__'8804'__22
du_'91'm'37'n'93''60'n_1186 Integer
v0 Integer
v1 T_NonZero_112
v2
= (Integer -> Integer -> T__'8804'__22)
-> Any -> Any -> T__'8804'__22
forall a b. a -> b
coe Integer -> Integer -> T__'8804'__22
du_m'37'n'60'n_166 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1)