tt('const/arithmetic/*', ty, ('type/num/num' > ('type/num/num' > 'type/num/num'))).
tt('const/arithmetic/+', ty, ('type/num/num' > ('type/num/num' > 'type/num/num'))).
tt('const/arithmetic/-', ty, ('type/num/num' > ('type/num/num' > 'type/num/num'))).
tt('const/arithmetic/<=', ty, ('type/num/num' > ('type/num/num' > $o))).
tt('const/arithmetic/>', ty, ('type/num/num' > ('type/num/num' > $o))).
tt('const/arithmetic/>=', ty, ('type/num/num' > ('type/num/num' > $o))).
tt('const/arithmetic/ABS_DIFF', ty, ('type/num/num' > ('type/num/num' > 'type/num/num'))).
tt('const/arithmetic/BIT1', ty, ('type/num/num' > 'type/num/num')).
tt('const/arithmetic/BIT2', ty, ('type/num/num' > 'type/num/num')).
tt('const/arithmetic/DIV', ty, ('type/num/num' > ('type/num/num' > 'type/num/num'))).
tt('const/arithmetic/DIV2', ty, ('type/num/num' > 'type/num/num')).
tt('const/arithmetic/DIVMOD', ty, (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) > ('type/pair/prod' 'type/num/num' 'type/num/num'))).
tt('const/arithmetic/EVEN', ty, ('type/num/num' > $o)).
tt('const/arithmetic/EXP', ty, ('type/num/num' > ('type/num/num' > 'type/num/num'))).
tt('const/arithmetic/FACT', ty, ('type/num/num' > 'type/num/num')).
tt('const/arithmetic/FUNPOW', ty, ![A : $t]: ((A > A) > ('type/num/num' > (A > A)))).
tt('const/arithmetic/MAX', ty, ('type/num/num' > ('type/num/num' > 'type/num/num'))).
tt('const/arithmetic/MIN', ty, ('type/num/num' > ('type/num/num' > 'type/num/num'))).
tt('const/arithmetic/MOD', ty, ('type/num/num' > ('type/num/num' > 'type/num/num'))).
tt('const/arithmetic/MODEQ', ty, ('type/num/num' > ('type/num/num' > ('type/num/num' > $o)))).
tt('const/arithmetic/NRC', ty, ![A : $t]: ((A > (A > $o)) > ('type/num/num' > (A > (A > $o))))).
tt('const/arithmetic/NUMERAL', ty, ('type/num/num' > 'type/num/num')).
tt('const/arithmetic/ODD', ty, ('type/num/num' > $o)).
tt('const/arithmetic/ZERO', ty, 'type/num/num').
tt('const/arithmetic/findq', ty, (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) > 'type/num/num')).
tt('const/arithmetic/nat_elim__magic', ty, ('type/num/num' > 'type/num/num')).
tt('const/arithmetic/num_CASE', ty, ![A : $t]: ('type/num/num' > (A > (('type/num/num' > A) > A)))).
tt('thm/arithmetic/ADD_0', def, (![n : 'type/num/num']: (('const/arithmetic/+' 'const/num/0' n) = n))).
tt('thm/arithmetic/ADD_e1', def, (![m : 'type/num/num', n : 'type/num/num']: (('const/arithmetic/+' ('const/num/SUC' m) n) = ('const/num/SUC' ('const/arithmetic/+' m n))))).
tt('thm/arithmetic/NUMERAL_DEF_', def, (![x : 'type/num/num']: (('const/arithmetic/NUMERAL' x) = x))).
tt('thm/arithmetic/ALT_ZERO_', def, ('const/arithmetic/ZERO' = 'const/num/0')).
tt('thm/arithmetic/BIT1_', def, (![n : 'type/num/num']: (('const/arithmetic/BIT1' n) = ('const/arithmetic/+' n ('const/arithmetic/+' n ('const/num/SUC' 'const/num/0')))))).
tt('thm/arithmetic/BIT2_', def, (![n : 'type/num/num']: (('const/arithmetic/BIT2' n) = ('const/arithmetic/+' n ('const/arithmetic/+' n ('const/num/SUC' ('const/num/SUC' 'const/num/0'))))))).
tt('thm/arithmetic/nat_elim__magic_', def, (![n : 'type/num/num']: (('const/arithmetic/nat_elim__magic' n) = n))).
tt('thm/arithmetic/SUB_0', def, (![m : 'type/num/num']: (('const/arithmetic/-' 'const/num/0' m) = 'const/num/0'))).
tt('thm/arithmetic/SUB_e1', def, (![m : 'type/num/num', n : 'type/num/num']: (('const/arithmetic/-' ('const/num/SUC' m) n) = (('const/bool/COND' 'type/num/num') ('const/prim_rec/<' m n) 'const/num/0' ('const/num/SUC' ('const/arithmetic/-' m n)))))).
tt('thm/arithmetic/MULT_0', def, (![n : 'type/num/num']: (('const/arithmetic/*' 'const/num/0' n) = 'const/num/0'))).
tt('thm/arithmetic/MULT_e1', def, (![m : 'type/num/num', n : 'type/num/num']: (('const/arithmetic/*' ('const/num/SUC' m) n) = ('const/arithmetic/+' ('const/arithmetic/*' m n) n)))).
tt('thm/arithmetic/EXP_0', def, (![m : 'type/num/num']: (('const/arithmetic/EXP' m 'const/num/0') = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/arithmetic/EXP_e1', def, (![m : 'type/num/num', n : 'type/num/num']: (('const/arithmetic/EXP' m ('const/num/SUC' n)) = ('const/arithmetic/*' m ('const/arithmetic/EXP' m n))))).
tt('thm/arithmetic/GREATER_DEF_', def, (![m : 'type/num/num', n : 'type/num/num']: (('const/arithmetic/>' m n) = ('const/prim_rec/<' n m)))).
tt('thm/arithmetic/LESS_OR_EQ_', def, (![m : 'type/num/num', n : 'type/num/num']: (('const/arithmetic/<=' m n) = (('const/prim_rec/<' m n) | (m = n))))).
tt('thm/arithmetic/GREATER_OR_EQ_', def, (![m : 'type/num/num', n : 'type/num/num']: (('const/arithmetic/>=' m n) = (('const/arithmetic/>' m n) | (m = n))))).
tt('thm/arithmetic/EVEN_0', def, (('const/arithmetic/EVEN' 'const/num/0') = $true)).
tt('thm/arithmetic/EVEN_e1', def, (![n : 'type/num/num']: (('const/arithmetic/EVEN' ('const/num/SUC' n)) = (~ ('const/arithmetic/EVEN' n))))).
tt('thm/arithmetic/ODD_0', def, (('const/arithmetic/ODD' 'const/num/0') = $false)).
tt('thm/arithmetic/ODD_e1', def, (![n : 'type/num/num']: (('const/arithmetic/ODD' ('const/num/SUC' n)) = (~ ('const/arithmetic/ODD' n))))).
tt('thm/arithmetic/num_case_def_0', def, ![A : $t]: (![v : A, f : ('type/num/num' > A)]: ((('const/arithmetic/num_CASE' A) 'const/num/0' v f) = v))).
tt('thm/arithmetic/num_case_def_e1', def, ![A : $t]: (![n : 'type/num/num', v : A, f : ('type/num/num' > A)]: ((('const/arithmetic/num_CASE' A) ('const/num/SUC' n) v f) = (f n)))).
tt('thm/arithmetic/FUNPOW_0', def, ![A : $t]: (![f : (A > A), x : A]: ((('const/arithmetic/FUNPOW' A) f 'const/num/0' x) = x))).
tt('thm/arithmetic/FUNPOW_e1', def, ![A : $t]: (![f : (A > A), n : 'type/num/num', x : A]: ((('const/arithmetic/FUNPOW' A) f ('const/num/SUC' n) x) = (('const/arithmetic/FUNPOW' A) f n (f x))))).
tt('thm/arithmetic/NRC_0', def, ![A : $t]: (![R : (A > (A > $o)), x : A, y : A]: ((('const/arithmetic/NRC' A) R 'const/num/0' x y) = (x = y)))).
tt('thm/arithmetic/NRC_e1', def, ![A : $t]: (![R : (A > (A > $o)), n : 'type/num/num', x : A, y : A]: ((('const/arithmetic/NRC' A) R ('const/num/SUC' n) x y) = (?[z : A]: ((R x z) & (('const/arithmetic/NRC' A) R n z y)))))).
tt('thm/arithmetic/ONE_', ax, (('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) = ('const/num/SUC' 'const/num/0'))).
tt('thm/arithmetic/TWO_', ax, (('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) = ('const/num/SUC' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/arithmetic/NORM_0_', ax, (('const/arithmetic/NUMERAL' 'const/arithmetic/ZERO') = 'const/num/0')).
tt('thm/arithmetic/num_case_compute_', ax, ![A : $t]: (![g : ('type/num/num' > A), f : A, n : 'type/num/num']: ((('const/arithmetic/num_CASE' A) n f g) = (('const/bool/COND' A) (n = 'const/num/0') f (g ('const/prim_rec/PRE' n)))))).
tt('thm/arithmetic/SUC_NOT_', ax, (![n : 'type/num/num']: (~ ('const/num/0' = ('const/num/SUC' n))))).
tt('thm/arithmetic/ADD_0_', ax, (![m : 'type/num/num']: (('const/arithmetic/+' m 'const/num/0') = m))).
tt('thm/arithmetic/ADD_SUC_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/num/SUC' ('const/arithmetic/+' m n)) = ('const/arithmetic/+' m ('const/num/SUC' n))))).
tt('thm/arithmetic/ADD_CLAUSES_0', ax, (![m : 'type/num/num']: (('const/arithmetic/+' 'const/num/0' m) = m))).
tt('thm/arithmetic/ADD_CLAUSES_1', ax, (![m : 'type/num/num']: (('const/arithmetic/+' m 'const/num/0') = m))).
tt('thm/arithmetic/ADD_CLAUSES_2', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/arithmetic/+' ('const/num/SUC' m) n) = ('const/num/SUC' ('const/arithmetic/+' m n))))).
tt('thm/arithmetic/ADD_CLAUSES_e3', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/arithmetic/+' m ('const/num/SUC' n)) = ('const/num/SUC' ('const/arithmetic/+' m n))))).
tt('thm/arithmetic/ADD_SYM_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/arithmetic/+' m n) = ('const/arithmetic/+' n m)))).
tt('thm/arithmetic/ADD_COMM_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/arithmetic/+' m n) = ('const/arithmetic/+' n m)))).
tt('thm/arithmetic/ADD_ASSOC_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: (('const/arithmetic/+' m ('const/arithmetic/+' n p)) = ('const/arithmetic/+' ('const/arithmetic/+' m n) p)))).
tt('thm/arithmetic/num_CASES_', ax, (![m : 'type/num/num']: ((m = 'const/num/0') | (?[n : 'type/num/num']: (m = ('const/num/SUC' n)))))).
tt('thm/arithmetic/NOT_ZERO_LT_ZERO_', ax, (![n : 'type/num/num']: ((~ (n = 'const/num/0')) = ('const/prim_rec/<' 'const/num/0' n)))).
tt('thm/arithmetic/NOT_LT_ZERO_EQ_ZERO_', ax, (![n : 'type/num/num']: ((~ ('const/prim_rec/<' 'const/num/0' n)) = (n = 'const/num/0')))).
tt('thm/arithmetic/LESS_ADD_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/prim_rec/<' n m) => (?[p : 'type/num/num']: (('const/arithmetic/+' p n) = m))))).
tt('thm/arithmetic/LESS_TRANS_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: ((('const/prim_rec/<' m n) & ('const/prim_rec/<' n p)) => ('const/prim_rec/<' m p)))).
tt('thm/arithmetic/transitive_LESS_', ax, (('const/relation/transitive' 'type/num/num') 'const/prim_rec/<')).
tt('thm/arithmetic/LESS_ANTISYM_', ax, (![m : 'type/num/num', n : 'type/num/num']: (~ (('const/prim_rec/<' m n) & ('const/prim_rec/<' n m))))).
tt('thm/arithmetic/LESS_LESS_SUC_', ax, (![m : 'type/num/num', n : 'type/num/num']: (~ (('const/prim_rec/<' m n) & ('const/prim_rec/<' n ('const/num/SUC' m)))))).
tt('thm/arithmetic/transitive_measure_', ax, ![A : $t]: (![f : (A > 'type/num/num')]: (('const/relation/transitive' A) (('const/prim_rec/measure' A) f)))).
tt('thm/arithmetic/LESS_MONO_REV_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/prim_rec/<' ('const/num/SUC' m) ('const/num/SUC' n)) => ('const/prim_rec/<' m n)))).
tt('thm/arithmetic/LESS_MONO_EQ_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/prim_rec/<' ('const/num/SUC' m) ('const/num/SUC' n)) = ('const/prim_rec/<' m n)))).
tt('thm/arithmetic/LESS_OR_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/prim_rec/<' m n) => ('const/arithmetic/<=' ('const/num/SUC' m) n)))).
tt('thm/arithmetic/OR_LESS_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/arithmetic/<=' ('const/num/SUC' m) n) => ('const/prim_rec/<' m n)))).
tt('thm/arithmetic/LESS_EQ_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/prim_rec/<' m n) = ('const/arithmetic/<=' ('const/num/SUC' m) n)))).
tt('thm/arithmetic/LESS_SUC_EQ_COR_', ax, (![m : 'type/num/num', n : 'type/num/num']: ((('const/prim_rec/<' m n) & (~ (('const/num/SUC' m) = n))) => ('const/prim_rec/<' ('const/num/SUC' m) n)))).
tt('thm/arithmetic/LESS_NOT_SUC_', ax, (![m : 'type/num/num', n : 'type/num/num']: ((('const/prim_rec/<' m n) & (~ (n = ('const/num/SUC' m)))) => ('const/prim_rec/<' ('const/num/SUC' m) n)))).
tt('thm/arithmetic/LESS_0_CASES_', ax, (![m : 'type/num/num']: (('const/num/0' = m) | ('const/prim_rec/<' 'const/num/0' m)))).
tt('thm/arithmetic/LESS_CASES_IMP_', ax, (![m : 'type/num/num', n : 'type/num/num']: (((~ ('const/prim_rec/<' m n)) & (~ (m = n))) => ('const/prim_rec/<' n m)))).
tt('thm/arithmetic/LESS_CASES_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/prim_rec/<' m n) | ('const/arithmetic/<=' n m)))).
tt('thm/arithmetic/ADD_INV_0_', ax, (![m : 'type/num/num', n : 'type/num/num']: ((('const/arithmetic/+' m n) = m) => (n = 'const/num/0')))).
tt('thm/arithmetic/LESS_EQ_ADD_', ax, (![m : 'type/num/num', n : 'type/num/num']: ('const/arithmetic/<=' m ('const/arithmetic/+' m n)))).
tt('thm/arithmetic/LESS_EQ_ADD_EXISTS_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/arithmetic/<=' n m) => (?[p : 'type/num/num']: (('const/arithmetic/+' p n) = m))))).
tt('thm/arithmetic/LESS_STRONG_ADD_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/prim_rec/<' n m) => (?[p : 'type/num/num']: (('const/arithmetic/+' ('const/num/SUC' p) n) = m))))).
tt('thm/arithmetic/LESS_EQ_SUC_REFL_', ax, (![m : 'type/num/num']: ('const/arithmetic/<=' m ('const/num/SUC' m)))).
tt('thm/arithmetic/LESS_ADD_NONZERO_', ax, (![m : 'type/num/num', n : 'type/num/num']: ((~ (n = 'const/num/0')) => ('const/prim_rec/<' m ('const/arithmetic/+' m n))))).
tt('thm/arithmetic/LESS_EQ_ANTISYM_', ax, (![m : 'type/num/num', n : 'type/num/num']: (~ (('const/prim_rec/<' m n) & ('const/arithmetic/<=' n m))))).
tt('thm/arithmetic/NOT_LESS_', ax, (![m : 'type/num/num', n : 'type/num/num']: ((~ ('const/prim_rec/<' m n)) = ('const/arithmetic/<=' n m)))).
tt('thm/arithmetic/SUB_0_0', ax, (![m : 'type/num/num']: (('const/arithmetic/-' 'const/num/0' m) = 'const/num/0'))).
tt('thm/arithmetic/SUB_0_e1', ax, (![m : 'type/num/num']: (('const/arithmetic/-' m 'const/num/0') = m))).
tt('thm/arithmetic/SUB_EQ_0_', ax, (![m : 'type/num/num', n : 'type/num/num']: ((('const/arithmetic/-' m n) = 'const/num/0') = ('const/arithmetic/<=' m n)))).
tt('thm/arithmetic/ADD1_', ax, (![m : 'type/num/num']: (('const/num/SUC' m) = ('const/arithmetic/+' m ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
tt('thm/arithmetic/SUC_SUB1_', ax, (![m : 'type/num/num']: (('const/arithmetic/-' ('const/num/SUC' m) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) = m))).
tt('thm/arithmetic/PRE_SUB1_', ax, (![m : 'type/num/num']: (('const/prim_rec/PRE' m) = ('const/arithmetic/-' m ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
tt('thm/arithmetic/MULT_0_', ax, (![m : 'type/num/num']: (('const/arithmetic/*' m 'const/num/0') = 'const/num/0'))).
tt('thm/arithmetic/MULT_SUC_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/arithmetic/*' m ('const/num/SUC' n)) = ('const/arithmetic/+' m ('const/arithmetic/*' m n))))).
tt('thm/arithmetic/MULT_LEFT_1_', ax, (![m : 'type/num/num']: (('const/arithmetic/*' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) m) = m))).
tt('thm/arithmetic/MULT_RIGHT_1_', ax, (![m : 'type/num/num']: (('const/arithmetic/*' m ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) = m))).
tt('thm/arithmetic/MULT_CLAUSES_0', ax, (![m : 'type/num/num']: (('const/arithmetic/*' 'const/num/0' m) = 'const/num/0'))).
tt('thm/arithmetic/MULT_CLAUSES_1', ax, (![m : 'type/num/num']: (('const/arithmetic/*' m 'const/num/0') = 'const/num/0'))).
tt('thm/arithmetic/MULT_CLAUSES_2', ax, (![m : 'type/num/num']: (('const/arithmetic/*' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) m) = m))).
tt('thm/arithmetic/MULT_CLAUSES_3', ax, (![m : 'type/num/num']: (('const/arithmetic/*' m ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) = m))).
tt('thm/arithmetic/MULT_CLAUSES_4', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/arithmetic/*' ('const/num/SUC' m) n) = ('const/arithmetic/+' ('const/arithmetic/*' m n) n)))).
tt('thm/arithmetic/MULT_CLAUSES_e5', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/arithmetic/*' m ('const/num/SUC' n)) = ('const/arithmetic/+' m ('const/arithmetic/*' m n))))).
tt('thm/arithmetic/MULT_SYM_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/arithmetic/*' m n) = ('const/arithmetic/*' n m)))).
tt('thm/arithmetic/MULT_COMM_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/arithmetic/*' m n) = ('const/arithmetic/*' n m)))).
tt('thm/arithmetic/RIGHT_ADD_DISTRIB_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: (('const/arithmetic/*' ('const/arithmetic/+' m n) p) = ('const/arithmetic/+' ('const/arithmetic/*' m p) ('const/arithmetic/*' n p))))).
tt('thm/arithmetic/LEFT_ADD_DISTRIB_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: (('const/arithmetic/*' p ('const/arithmetic/+' m n)) = ('const/arithmetic/+' ('const/arithmetic/*' p m) ('const/arithmetic/*' p n))))).
tt('thm/arithmetic/MULT_ASSOC_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: (('const/arithmetic/*' m ('const/arithmetic/*' n p)) = ('const/arithmetic/*' ('const/arithmetic/*' m n) p)))).
tt('thm/arithmetic/SUB_ADD_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/arithmetic/<=' n m) => (('const/arithmetic/+' ('const/arithmetic/-' m n) n) = m)))).
tt('thm/arithmetic/PRE_SUB_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/prim_rec/PRE' ('const/arithmetic/-' m n)) = ('const/arithmetic/-' ('const/prim_rec/PRE' m) n)))).
tt('thm/arithmetic/ADD_EQ_0_', ax, (![m : 'type/num/num', n : 'type/num/num']: ((('const/arithmetic/+' m n) = 'const/num/0') = ((m = 'const/num/0') & (n = 'const/num/0'))))).
tt('thm/arithmetic/ADD_EQ_1_', ax, (![m : 'type/num/num', n : 'type/num/num']: ((('const/arithmetic/+' m n) = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) = (((m = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) & (n = 'const/num/0')) | ((m = 'const/num/0') & (n = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))).
tt('thm/arithmetic/ADD_INV_0_EQ_', ax, (![m : 'type/num/num', n : 'type/num/num']: ((('const/arithmetic/+' m n) = m) = (n = 'const/num/0')))).
tt('thm/arithmetic/PRE_SUC_EQ_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' n) => ((m = ('const/prim_rec/PRE' n)) = (('const/num/SUC' m) = n))))).
tt('thm/arithmetic/INV_PRE_EQ_', ax, (![m : 'type/num/num', n : 'type/num/num']: ((('const/prim_rec/<' 'const/num/0' m) & ('const/prim_rec/<' 'const/num/0' n)) => ((('const/prim_rec/PRE' m) = ('const/prim_rec/PRE' n)) = (m = n))))).
tt('thm/arithmetic/LESS_SUC_NOT_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/prim_rec/<' m n) => (~ ('const/prim_rec/<' n ('const/num/SUC' m)))))).
tt('thm/arithmetic/ADD_EQ_SUB_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: (('const/arithmetic/<=' n p) => ((('const/arithmetic/+' m n) = p) = (m = ('const/arithmetic/-' p n)))))).
tt('thm/arithmetic/LESS_MONO_ADD_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: (('const/prim_rec/<' m n) => ('const/prim_rec/<' ('const/arithmetic/+' m p) ('const/arithmetic/+' n p))))).
tt('thm/arithmetic/LESS_MONO_ADD_INV_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: (('const/prim_rec/<' ('const/arithmetic/+' m p) ('const/arithmetic/+' n p)) => ('const/prim_rec/<' m n)))).
tt('thm/arithmetic/LESS_MONO_ADD_EQ_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: (('const/prim_rec/<' ('const/arithmetic/+' m p) ('const/arithmetic/+' n p)) = ('const/prim_rec/<' m n)))).
tt('thm/arithmetic/LT_ADD_RCANCEL_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: (('const/prim_rec/<' ('const/arithmetic/+' m p) ('const/arithmetic/+' n p)) = ('const/prim_rec/<' m n)))).
tt('thm/arithmetic/LT_ADD_LCANCEL_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: (('const/prim_rec/<' ('const/arithmetic/+' p m) ('const/arithmetic/+' p n)) = ('const/prim_rec/<' m n)))).
tt('thm/arithmetic/EQ_MONO_ADD_EQ_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: ((('const/arithmetic/+' m p) = ('const/arithmetic/+' n p)) = (m = n)))).
tt('thm/arithmetic/LESS_EQ_MONO_ADD_EQ_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: (('const/arithmetic/<=' ('const/arithmetic/+' m p) ('const/arithmetic/+' n p)) = ('const/arithmetic/<=' m n)))).
tt('thm/arithmetic/LESS_EQ_TRANS_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: ((('const/arithmetic/<=' m n) & ('const/arithmetic/<=' n p)) => ('const/arithmetic/<=' m p)))).
tt('thm/arithmetic/LESS_EQ_LESS_EQ_MONO_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num', q : 'type/num/num']: ((('const/arithmetic/<=' m p) & ('const/arithmetic/<=' n q)) => ('const/arithmetic/<=' ('const/arithmetic/+' m n) ('const/arithmetic/+' p q))))).
tt('thm/arithmetic/LESS_EQ_REFL_', ax, (![m : 'type/num/num']: ('const/arithmetic/<=' m m))).
tt('thm/arithmetic/LESS_IMP_LESS_OR_EQ_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/prim_rec/<' m n) => ('const/arithmetic/<=' m n)))).
tt('thm/arithmetic/LESS_MONO_MULT_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: (('const/arithmetic/<=' m n) => ('const/arithmetic/<=' ('const/arithmetic/*' m p) ('const/arithmetic/*' n p))))).
tt('thm/arithmetic/LESS_MONO_MULT2_', ax, (![m : 'type/num/num', n : 'type/num/num', i : 'type/num/num', j : 'type/num/num']: ((('const/arithmetic/<=' m i) & ('const/arithmetic/<=' n j)) => ('const/arithmetic/<=' ('const/arithmetic/*' m n) ('const/arithmetic/*' i j))))).
tt('thm/arithmetic/RIGHT_SUB_DISTRIB_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: (('const/arithmetic/*' ('const/arithmetic/-' m n) p) = ('const/arithmetic/-' ('const/arithmetic/*' m p) ('const/arithmetic/*' n p))))).
tt('thm/arithmetic/LEFT_SUB_DISTRIB_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: (('const/arithmetic/*' p ('const/arithmetic/-' m n)) = ('const/arithmetic/-' ('const/arithmetic/*' p m) ('const/arithmetic/*' p n))))).
tt('thm/arithmetic/LESS_ADD_1_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/prim_rec/<' n m) => (?[p : 'type/num/num']: (m = ('const/arithmetic/+' n ('const/arithmetic/+' p ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))).
tt('thm/arithmetic/EXP_ADD_', ax, (![p : 'type/num/num', q : 'type/num/num', n : 'type/num/num']: (('const/arithmetic/EXP' n ('const/arithmetic/+' p q)) = ('const/arithmetic/*' ('const/arithmetic/EXP' n p) ('const/arithmetic/EXP' n q))))).
tt('thm/arithmetic/NOT_ODD_EQ_EVEN_', ax, (![n : 'type/num/num', m : 'type/num/num']: (~ (('const/num/SUC' ('const/arithmetic/+' n n)) = ('const/arithmetic/+' m m))))).
tt('thm/arithmetic/MULT_SUC_EQ_', ax, (![p : 'type/num/num', m : 'type/num/num', n : 'type/num/num']: ((('const/arithmetic/*' n ('const/num/SUC' p)) = ('const/arithmetic/*' m ('const/num/SUC' p))) = (n = m)))).
tt('thm/arithmetic/MULT_EXP_MONO_', ax, (![p : 'type/num/num', q : 'type/num/num', n : 'type/num/num', m : 'type/num/num']: ((('const/arithmetic/*' n ('const/arithmetic/EXP' ('const/num/SUC' q) p)) = ('const/arithmetic/*' m ('const/arithmetic/EXP' ('const/num/SUC' q) p))) = (n = m)))).
tt('thm/arithmetic/LESS_EQUAL_ANTISYM_', ax, (![n : 'type/num/num', m : 'type/num/num']: ((('const/arithmetic/<=' n m) & ('const/arithmetic/<=' m n)) => (n = m)))).
tt('thm/arithmetic/LESS_ADD_SUC_', ax, (![m : 'type/num/num', n : 'type/num/num']: ('const/prim_rec/<' m ('const/arithmetic/+' m ('const/num/SUC' n))))).
tt('thm/arithmetic/ZERO_LESS_EQ_', ax, (![n : 'type/num/num']: ('const/arithmetic/<=' 'const/num/0' n))).
tt('thm/arithmetic/LESS_EQ_MONO_', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/arithmetic/<=' ('const/num/SUC' n) ('const/num/SUC' m)) = ('const/arithmetic/<=' n m)))).
tt('thm/arithmetic/LESS_OR_EQ_ADD_', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/prim_rec/<' n m) | (?[p : 'type/num/num']: (n = ('const/arithmetic/+' p m)))))).
tt('thm/arithmetic/WOP_', ax, (![P : ('type/num/num' > $o)]: ((?[n : 'type/num/num']: (P n)) => (?[n : 'type/num/num']: ((P n) & (![m : 'type/num/num']: (('const/prim_rec/<' m n) => (~ (P m))))))))).
tt('thm/arithmetic/COMPLETE_INDUCTION_', ax, (![P : ('type/num/num' > $o)]: ((![n : 'type/num/num']: ((![m : 'type/num/num']: (('const/prim_rec/<' m n) => (P m))) => (P n))) => (![n : 'type/num/num']: (P n))))).
tt('thm/arithmetic/FORALL_NUM_THM_', ax, (![P : ('type/num/num' > $o)]: ((![n : 'type/num/num']: (P n)) = ((P 'const/num/0') & (![n : 'type/num/num']: ((P n) => (P ('const/num/SUC' n)))))))).
tt('thm/arithmetic/SUB_MONO_EQ_', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/arithmetic/-' ('const/num/SUC' n) ('const/num/SUC' m)) = ('const/arithmetic/-' n m)))).
tt('thm/arithmetic/SUB_PLUS_', ax, (![a : 'type/num/num', b : 'type/num/num', c : 'type/num/num']: (('const/arithmetic/-' a ('const/arithmetic/+' b c)) = ('const/arithmetic/-' ('const/arithmetic/-' a b) c)))).
tt('thm/arithmetic/INV_PRE_LESS_', ax, (![m : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' m) => (![n : 'type/num/num']: (('const/prim_rec/<' ('const/prim_rec/PRE' m) ('const/prim_rec/PRE' n)) = ('const/prim_rec/<' m n)))))).
tt('thm/arithmetic/INV_PRE_LESS_EQ_', ax, (![n : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' n) => (![m : 'type/num/num']: (('const/arithmetic/<=' ('const/prim_rec/PRE' m) ('const/prim_rec/PRE' n)) = ('const/arithmetic/<=' m n)))))).
tt('thm/arithmetic/SUB_LESS_EQ_', ax, (![n : 'type/num/num', m : 'type/num/num']: ('const/arithmetic/<=' ('const/arithmetic/-' n m) n))).
tt('thm/arithmetic/SUB_EQ_EQ_0_', ax, (![m : 'type/num/num', n : 'type/num/num']: ((('const/arithmetic/-' m n) = m) = ((m = 'const/num/0') | (n = 'const/num/0'))))).
tt('thm/arithmetic/SUB_LESS_0_', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/prim_rec/<' m n) = ('const/prim_rec/<' 'const/num/0' ('const/arithmetic/-' n m))))).
tt('thm/arithmetic/SUB_LESS_OR_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/prim_rec/<' n m) => ('const/arithmetic/<=' n ('const/arithmetic/-' m ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))).
tt('thm/arithmetic/LESS_SUB_ADD_LESS_', ax, (![n : 'type/num/num', m : 'type/num/num', i : 'type/num/num']: (('const/prim_rec/<' i ('const/arithmetic/-' n m)) => ('const/prim_rec/<' ('const/arithmetic/+' i m) n)))).
tt('thm/arithmetic/TIMES2_', ax, (![n : 'type/num/num']: (('const/arithmetic/*' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) n) = ('const/arithmetic/+' n n)))).
tt('thm/arithmetic/LESS_MULT_MONO_', ax, (![m : 'type/num/num', i : 'type/num/num', n : 'type/num/num']: (('const/prim_rec/<' ('const/arithmetic/*' ('const/num/SUC' n) m) ('const/arithmetic/*' ('const/num/SUC' n) i)) = ('const/prim_rec/<' m i)))).
tt('thm/arithmetic/MULT_MONO_EQ_', ax, (![m : 'type/num/num', i : 'type/num/num', n : 'type/num/num']: ((('const/arithmetic/*' ('const/num/SUC' n) m) = ('const/arithmetic/*' ('const/num/SUC' n) i)) = (m = i)))).
tt('thm/arithmetic/EQ_ADD_LCANCEL_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: ((('const/arithmetic/+' m n) = ('const/arithmetic/+' m p)) = (n = p)))).
tt('thm/arithmetic/EQ_ADD_RCANCEL_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: ((('const/arithmetic/+' m p) = ('const/arithmetic/+' n p)) = (m = n)))).
tt('thm/arithmetic/EQ_MULT_LCANCEL_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: ((('const/arithmetic/*' m n) = ('const/arithmetic/*' m p)) = ((m = 'const/num/0') | (n = p))))).
tt('thm/arithmetic/ADD_SUB_', ax, (![a : 'type/num/num', c : 'type/num/num']: (('const/arithmetic/-' ('const/arithmetic/+' a c) c) = a))).
tt('thm/arithmetic/LESS_EQ_ADD_SUB_', ax, (![c : 'type/num/num', b : 'type/num/num']: (('const/arithmetic/<=' c b) => (![a : 'type/num/num']: (('const/arithmetic/-' ('const/arithmetic/+' a b) c) = ('const/arithmetic/+' a ('const/arithmetic/-' b c))))))).
tt('thm/arithmetic/SUB_EQUAL_0_', ax, (![c : 'type/num/num']: (('const/arithmetic/-' c c) = 'const/num/0'))).
tt('thm/arithmetic/LESS_EQ_SUB_LESS_', ax, (![a : 'type/num/num', b : 'type/num/num']: (('const/arithmetic/<=' b a) => (![c : 'type/num/num']: (('const/prim_rec/<' ('const/arithmetic/-' a b) c) = ('const/prim_rec/<' a ('const/arithmetic/+' b c))))))).
tt('thm/arithmetic/NOT_SUC_LESS_EQ_', ax, (![n : 'type/num/num', m : 'type/num/num']: ((~ ('const/arithmetic/<=' ('const/num/SUC' n) m)) = ('const/arithmetic/<=' m n)))).
tt('thm/arithmetic/SUB_SUB_', ax, (![b : 'type/num/num', c : 'type/num/num']: (('const/arithmetic/<=' c b) => (![a : 'type/num/num']: (('const/arithmetic/-' a ('const/arithmetic/-' b c)) = ('const/arithmetic/-' ('const/arithmetic/+' a c) b)))))).
tt('thm/arithmetic/LESS_IMP_LESS_ADD_', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/prim_rec/<' n m) => (![p : 'type/num/num']: ('const/prim_rec/<' n ('const/arithmetic/+' m p)))))).
tt('thm/arithmetic/LESS_EQ_IMP_LESS_SUC_', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/arithmetic/<=' n m) => ('const/prim_rec/<' n ('const/num/SUC' m))))).
tt('thm/arithmetic/SUB_LESS_EQ_ADD_', ax, (![m : 'type/num/num', p : 'type/num/num']: (('const/arithmetic/<=' m p) => (![n : 'type/num/num']: (('const/arithmetic/<=' ('const/arithmetic/-' p m) n) = ('const/arithmetic/<=' p ('const/arithmetic/+' m n))))))).
tt('thm/arithmetic/SUB_CANCEL_', ax, (![p : 'type/num/num', n : 'type/num/num', m : 'type/num/num']: ((('const/arithmetic/<=' n p) & ('const/arithmetic/<=' m p)) => ((('const/arithmetic/-' p n) = ('const/arithmetic/-' p m)) = (n = m))))).
tt('thm/arithmetic/CANCEL_SUB_', ax, (![p : 'type/num/num', n : 'type/num/num', m : 'type/num/num']: ((('const/arithmetic/<=' p n) & ('const/arithmetic/<=' p m)) => ((('const/arithmetic/-' n p) = ('const/arithmetic/-' m p)) = (n = m))))).
tt('thm/arithmetic/NOT_EXP_0_', ax, (![m : 'type/num/num', n : 'type/num/num']: (~ (('const/arithmetic/EXP' ('const/num/SUC' n) m) = 'const/num/0')))).
tt('thm/arithmetic/ZERO_LESS_EXP_', ax, (![m : 'type/num/num', n : 'type/num/num']: ('const/prim_rec/<' 'const/num/0' ('const/arithmetic/EXP' ('const/num/SUC' n) m)))).
tt('thm/arithmetic/ODD_OR_EVEN_', ax, (![n : 'type/num/num']: (?[m : 'type/num/num']: ((n = ('const/arithmetic/*' ('const/num/SUC' ('const/num/SUC' 'const/num/0')) m)) | (n = ('const/arithmetic/+' ('const/arithmetic/*' ('const/num/SUC' ('const/num/SUC' 'const/num/0')) m) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))).
tt('thm/arithmetic/LESS_EXP_SUC_MONO_', ax, (![n : 'type/num/num', m : 'type/num/num']: ('const/prim_rec/<' ('const/arithmetic/EXP' ('const/num/SUC' ('const/num/SUC' m)) n) ('const/arithmetic/EXP' ('const/num/SUC' ('const/num/SUC' m)) ('const/num/SUC' n))))).
tt('thm/arithmetic/LESS_LESS_CASES_', ax, (![m : 'type/num/num', n : 'type/num/num']: ((m = n) | (('const/prim_rec/<' m n) | ('const/prim_rec/<' n m))))).
tt('thm/arithmetic/GREATER_EQ_', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/arithmetic/>=' n m) = ('const/arithmetic/<=' m n)))).
tt('thm/arithmetic/LESS_EQ_CASES_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/arithmetic/<=' m n) | ('const/arithmetic/<=' n m)))).
tt('thm/arithmetic/LESS_EQUAL_ADD_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/arithmetic/<=' m n) => (?[p : 'type/num/num']: (n = ('const/arithmetic/+' m p)))))).
tt('thm/arithmetic/LESS_EQ_EXISTS_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/arithmetic/<=' m n) = (?[p : 'type/num/num']: (n = ('const/arithmetic/+' m p)))))).
tt('thm/arithmetic/NOT_LESS_EQUAL_', ax, (![m : 'type/num/num', n : 'type/num/num']: ((~ ('const/arithmetic/<=' m n)) = ('const/prim_rec/<' n m)))).
tt('thm/arithmetic/LESS_EQ_0_', ax, (![n : 'type/num/num']: (('const/arithmetic/<=' n 'const/num/0') = (n = 'const/num/0')))).
tt('thm/arithmetic/MULT_EQ_0_', ax, (![m : 'type/num/num', n : 'type/num/num']: ((('const/arithmetic/*' m n) = 'const/num/0') = ((m = 'const/num/0') | (n = 'const/num/0'))))).
tt('thm/arithmetic/MULT_EQ_1_', ax, (![x : 'type/num/num', y : 'type/num/num']: ((('const/arithmetic/*' x y) = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) = ((x = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) & (y = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))).
tt('thm/arithmetic/MULT_EQ_ID_', ax, (![m : 'type/num/num', n : 'type/num/num']: ((('const/arithmetic/*' m n) = n) = ((m = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) | (n = 'const/num/0'))))).
tt('thm/arithmetic/LESS_MULT2_', ax, (![m : 'type/num/num', n : 'type/num/num']: ((('const/prim_rec/<' 'const/num/0' m) & ('const/prim_rec/<' 'const/num/0' n)) => ('const/prim_rec/<' 'const/num/0' ('const/arithmetic/*' m n))))).
tt('thm/arithmetic/ZERO_LESS_MULT_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' ('const/arithmetic/*' m n)) = (('const/prim_rec/<' 'const/num/0' m) & ('const/prim_rec/<' 'const/num/0' n))))).
tt('thm/arithmetic/ZERO_LESS_ADD_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' ('const/arithmetic/+' m n)) = (('const/prim_rec/<' 'const/num/0' m) | ('const/prim_rec/<' 'const/num/0' n))))).
tt('thm/arithmetic/LESS_EQ_LESS_TRANS_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: ((('const/arithmetic/<=' m n) & ('const/prim_rec/<' n p)) => ('const/prim_rec/<' m p)))).
tt('thm/arithmetic/LESS_LESS_EQ_TRANS_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: ((('const/prim_rec/<' m n) & ('const/arithmetic/<=' n p)) => ('const/prim_rec/<' m p)))).
tt('thm/arithmetic/FACT_0', def, (('const/arithmetic/FACT' 'const/num/0') = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))).
tt('thm/arithmetic/FACT_e1', def, (![n : 'type/num/num']: (('const/arithmetic/FACT' ('const/num/SUC' n)) = ('const/arithmetic/*' ('const/num/SUC' n) ('const/arithmetic/FACT' n))))).
tt('thm/arithmetic/FACT_LESS_', ax, (![n : 'type/num/num']: ('const/prim_rec/<' 'const/num/0' ('const/arithmetic/FACT' n)))).
tt('thm/arithmetic/EVEN_ODD_', ax, (![n : 'type/num/num']: (('const/arithmetic/EVEN' n) = (~ ('const/arithmetic/ODD' n))))).
tt('thm/arithmetic/ODD_EVEN_', ax, (![n : 'type/num/num']: (('const/arithmetic/ODD' n) = (~ ('const/arithmetic/EVEN' n))))).
tt('thm/arithmetic/EVEN_OR_ODD_', ax, (![n : 'type/num/num']: (('const/arithmetic/EVEN' n) | ('const/arithmetic/ODD' n)))).
tt('thm/arithmetic/EVEN_AND_ODD_', ax, (![n : 'type/num/num']: (~ (('const/arithmetic/EVEN' n) & ('const/arithmetic/ODD' n))))).
tt('thm/arithmetic/EVEN_ADD_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/arithmetic/EVEN' ('const/arithmetic/+' m n)) = (('const/arithmetic/EVEN' m) = ('const/arithmetic/EVEN' n))))).
tt('thm/arithmetic/EVEN_MULT_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/arithmetic/EVEN' ('const/arithmetic/*' m n)) = (('const/arithmetic/EVEN' m) | ('const/arithmetic/EVEN' n))))).
tt('thm/arithmetic/ODD_ADD_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/arithmetic/ODD' ('const/arithmetic/+' m n)) = (~ (('const/arithmetic/ODD' m) = ('const/arithmetic/ODD' n)))))).
tt('thm/arithmetic/ODD_MULT_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/arithmetic/ODD' ('const/arithmetic/*' m n)) = (('const/arithmetic/ODD' m) & ('const/arithmetic/ODD' n))))).
tt('thm/arithmetic/EVEN_DOUBLE_', ax, (![n : 'type/num/num']: ('const/arithmetic/EVEN' ('const/arithmetic/*' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) n)))).
tt('thm/arithmetic/ODD_DOUBLE_', ax, (![n : 'type/num/num']: ('const/arithmetic/ODD' ('const/num/SUC' ('const/arithmetic/*' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) n))))).
tt('thm/arithmetic/EVEN_ODD_EXISTS_0', ax, (![n : 'type/num/num']: (('const/arithmetic/EVEN' n) => (?[m : 'type/num/num']: (n = ('const/arithmetic/*' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) m)))))).
tt('thm/arithmetic/EVEN_ODD_EXISTS_e1', ax, (![n : 'type/num/num']: (('const/arithmetic/ODD' n) => (?[m : 'type/num/num']: (n = ('const/num/SUC' ('const/arithmetic/*' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) m))))))).
tt('thm/arithmetic/EVEN_EXISTS_', ax, (![n : 'type/num/num']: (('const/arithmetic/EVEN' n) = (?[m : 'type/num/num']: (n = ('const/arithmetic/*' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) m)))))).
tt('thm/arithmetic/ODD_EXISTS_', ax, (![n : 'type/num/num']: (('const/arithmetic/ODD' n) = (?[m : 'type/num/num']: (n = ('const/num/SUC' ('const/arithmetic/*' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) m))))))).
tt('thm/arithmetic/EVEN_EXP_', ax, (![m : 'type/num/num', n : 'type/num/num']: ((('const/prim_rec/<' 'const/num/0' n) & ('const/arithmetic/EVEN' m)) => ('const/arithmetic/EVEN' ('const/arithmetic/EXP' m n))))).
tt('thm/arithmetic/EQ_LESS_EQ_', ax, (![m : 'type/num/num', n : 'type/num/num']: ((m = n) = (('const/arithmetic/<=' m n) & ('const/arithmetic/<=' n m))))).
tt('thm/arithmetic/ADD_MONO_LESS_EQ_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: (('const/arithmetic/<=' ('const/arithmetic/+' m n) ('const/arithmetic/+' m p)) = ('const/arithmetic/<=' n p)))).
tt('thm/arithmetic/LE_ADD_LCANCEL_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: (('const/arithmetic/<=' ('const/arithmetic/+' m n) ('const/arithmetic/+' m p)) = ('const/arithmetic/<=' n p)))).
tt('thm/arithmetic/LE_ADD_RCANCEL_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: (('const/arithmetic/<=' ('const/arithmetic/+' n m) ('const/arithmetic/+' p m)) = ('const/arithmetic/<=' n p)))).
tt('thm/arithmetic/NOT_SUC_LESS_EQ_0_', ax, (![n : 'type/num/num']: (~ ('const/arithmetic/<=' ('const/num/SUC' n) 'const/num/0')))).
tt('thm/arithmetic/NOT_LEQ_', ax, (![m : 'type/num/num', n : 'type/num/num']: ((~ ('const/arithmetic/<=' m n)) = ('const/arithmetic/<=' ('const/num/SUC' n) m)))).
tt('thm/arithmetic/NOT_NUM_EQ_', ax, (![m : 'type/num/num', n : 'type/num/num']: ((~ (m = n)) = (('const/arithmetic/<=' ('const/num/SUC' m) n) | ('const/arithmetic/<=' ('const/num/SUC' n) m))))).
tt('thm/arithmetic/NOT_GREATER_', ax, (![m : 'type/num/num', n : 'type/num/num']: ((~ ('const/arithmetic/>' m n)) = ('const/arithmetic/<=' m n)))).
tt('thm/arithmetic/NOT_GREATER_EQ_', ax, (![m : 'type/num/num', n : 'type/num/num']: ((~ ('const/arithmetic/>=' m n)) = ('const/arithmetic/<=' ('const/num/SUC' m) n)))).
tt('thm/arithmetic/SUC_ONE_ADD_', ax, (![n : 'type/num/num']: (('const/num/SUC' n) = ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) n)))).
tt('thm/arithmetic/SUC_ADD_SYM_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/num/SUC' ('const/arithmetic/+' m n)) = ('const/arithmetic/+' ('const/num/SUC' n) m)))).
tt('thm/arithmetic/NOT_SUC_ADD_LESS_EQ_', ax, (![m : 'type/num/num', n : 'type/num/num']: (~ ('const/arithmetic/<=' ('const/num/SUC' ('const/arithmetic/+' m n)) m)))).
tt('thm/arithmetic/MULT_LESS_EQ_SUC_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: (('const/arithmetic/<=' m n) = ('const/arithmetic/<=' ('const/arithmetic/*' ('const/num/SUC' p) m) ('const/arithmetic/*' ('const/num/SUC' p) n))))).
tt('thm/arithmetic/LE_MULT_LCANCEL_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: (('const/arithmetic/<=' ('const/arithmetic/*' m n) ('const/arithmetic/*' m p)) = ((m = 'const/num/0') | ('const/arithmetic/<=' n p))))).
tt('thm/arithmetic/LE_MULT_RCANCEL_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: (('const/arithmetic/<=' ('const/arithmetic/*' m n) ('const/arithmetic/*' p n)) = ((n = 'const/num/0') | ('const/arithmetic/<=' m p))))).
tt('thm/arithmetic/LT_MULT_LCANCEL_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: (('const/prim_rec/<' ('const/arithmetic/*' m n) ('const/arithmetic/*' m p)) = (('const/prim_rec/<' 'const/num/0' m) & ('const/prim_rec/<' n p))))).
tt('thm/arithmetic/LT_MULT_RCANCEL_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: (('const/prim_rec/<' ('const/arithmetic/*' m n) ('const/arithmetic/*' p n)) = (('const/prim_rec/<' 'const/num/0' n) & ('const/prim_rec/<' m p))))).
tt('thm/arithmetic/LT_MULT_CANCEL_LBARE_0', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/prim_rec/<' m ('const/arithmetic/*' m n)) = (('const/prim_rec/<' 'const/num/0' m) & ('const/prim_rec/<' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) n))))).
tt('thm/arithmetic/LT_MULT_CANCEL_LBARE_e1', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/prim_rec/<' m ('const/arithmetic/*' n m)) = (('const/prim_rec/<' 'const/num/0' m) & ('const/prim_rec/<' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) n))))).
tt('thm/arithmetic/LT_MULT_CANCEL_RBARE_0', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/prim_rec/<' ('const/arithmetic/*' m n) m) = (('const/prim_rec/<' 'const/num/0' m) & (n = 'const/num/0'))))).
tt('thm/arithmetic/LT_MULT_CANCEL_RBARE_e1', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/prim_rec/<' ('const/arithmetic/*' m n) n) = (('const/prim_rec/<' 'const/num/0' n) & (m = 'const/num/0'))))).
tt('thm/arithmetic/LE_MULT_CANCEL_LBARE_0', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/arithmetic/<=' m ('const/arithmetic/*' m n)) = ((m = 'const/num/0') | ('const/prim_rec/<' 'const/num/0' n))))).
tt('thm/arithmetic/LE_MULT_CANCEL_LBARE_e1', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/arithmetic/<=' m ('const/arithmetic/*' n m)) = ((m = 'const/num/0') | ('const/prim_rec/<' 'const/num/0' n))))).
tt('thm/arithmetic/LE_MULT_CANCEL_RBARE_0', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/arithmetic/<=' ('const/arithmetic/*' m n) m) = ((m = 'const/num/0') | ('const/arithmetic/<=' n ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))).
tt('thm/arithmetic/LE_MULT_CANCEL_RBARE_e1', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/arithmetic/<=' ('const/arithmetic/*' m n) n) = ((n = 'const/num/0') | ('const/arithmetic/<=' m ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))).
tt('thm/arithmetic/SUB_LEFT_ADD_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: (('const/arithmetic/+' m ('const/arithmetic/-' n p)) = (('const/bool/COND' 'type/num/num') ('const/arithmetic/<=' n p) m ('const/arithmetic/-' ('const/arithmetic/+' m n) p))))).
tt('thm/arithmetic/SUB_RIGHT_ADD_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: (('const/arithmetic/+' ('const/arithmetic/-' m n) p) = (('const/bool/COND' 'type/num/num') ('const/arithmetic/<=' m n) p ('const/arithmetic/-' ('const/arithmetic/+' m p) n))))).
tt('thm/arithmetic/SUB_LEFT_SUB_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: (('const/arithmetic/-' m ('const/arithmetic/-' n p)) = (('const/bool/COND' 'type/num/num') ('const/arithmetic/<=' n p) m ('const/arithmetic/-' ('const/arithmetic/+' m p) n))))).
tt('thm/arithmetic/SUB_RIGHT_SUB_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: (('const/arithmetic/-' ('const/arithmetic/-' m n) p) = ('const/arithmetic/-' m ('const/arithmetic/+' n p))))).
tt('thm/arithmetic/SUB_LEFT_SUC_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/num/SUC' ('const/arithmetic/-' m n)) = (('const/bool/COND' 'type/num/num') ('const/arithmetic/<=' m n) ('const/num/SUC' 'const/num/0') ('const/arithmetic/-' ('const/num/SUC' m) n))))).
tt('thm/arithmetic/SUB_LEFT_LESS_EQ_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: (('const/arithmetic/<=' m ('const/arithmetic/-' n p)) = (('const/arithmetic/<=' ('const/arithmetic/+' m p) n) | ('const/arithmetic/<=' m 'const/num/0'))))).
tt('thm/arithmetic/SUB_RIGHT_LESS_EQ_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: (('const/arithmetic/<=' ('const/arithmetic/-' m n) p) = ('const/arithmetic/<=' m ('const/arithmetic/+' n p))))).
tt('thm/arithmetic/SUB_LEFT_LESS_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: (('const/prim_rec/<' m ('const/arithmetic/-' n p)) = ('const/prim_rec/<' ('const/arithmetic/+' m p) n)))).
tt('thm/arithmetic/SUB_RIGHT_LESS_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: (('const/prim_rec/<' ('const/arithmetic/-' m n) p) = (('const/prim_rec/<' m ('const/arithmetic/+' n p)) & ('const/prim_rec/<' 'const/num/0' p))))).
tt('thm/arithmetic/SUB_LEFT_GREATER_EQ_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: (('const/arithmetic/>=' m ('const/arithmetic/-' n p)) = ('const/arithmetic/>=' ('const/arithmetic/+' m p) n)))).
tt('thm/arithmetic/SUB_RIGHT_GREATER_EQ_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: (('const/arithmetic/>=' ('const/arithmetic/-' m n) p) = (('const/arithmetic/>=' m ('const/arithmetic/+' n p)) | ('const/arithmetic/>=' 'const/num/0' p))))).
tt('thm/arithmetic/SUB_LEFT_GREATER_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: (('const/arithmetic/>' m ('const/arithmetic/-' n p)) = (('const/arithmetic/>' ('const/arithmetic/+' m p) n) & ('const/arithmetic/>' m 'const/num/0'))))).
tt('thm/arithmetic/SUB_RIGHT_GREATER_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: (('const/arithmetic/>' ('const/arithmetic/-' m n) p) = ('const/arithmetic/>' m ('const/arithmetic/+' n p))))).
tt('thm/arithmetic/SUB_LEFT_EQ_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: ((m = ('const/arithmetic/-' n p)) = ((('const/arithmetic/+' m p) = n) | (('const/arithmetic/<=' m 'const/num/0') & ('const/arithmetic/<=' n p)))))).
tt('thm/arithmetic/SUB_RIGHT_EQ_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: ((('const/arithmetic/-' m n) = p) = ((m = ('const/arithmetic/+' n p)) | (('const/arithmetic/<=' m n) & ('const/arithmetic/<=' p 'const/num/0')))))).
tt('thm/arithmetic/LE_0', ax, (![n : 'type/num/num']: (('const/arithmetic/<=' n 'const/num/0') = (n = 'const/num/0')))).
tt('thm/arithmetic/LE_e1', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/arithmetic/<=' m ('const/num/SUC' n)) = ((m = ('const/num/SUC' n)) | ('const/arithmetic/<=' m n))))).
tt('thm/arithmetic/DA_', ax, (![k : 'type/num/num', n : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' n) => (?[r : 'type/num/num', q : 'type/num/num']: ((k = ('const/arithmetic/+' ('const/arithmetic/*' q n) r)) & ('const/prim_rec/<' r n)))))).
tt('thm/arithmetic/DIVISION_', def, (![n : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' n) => (![k : 'type/num/num']: ((k = ('const/arithmetic/+' ('const/arithmetic/*' ('const/arithmetic/DIV' k n) n) ('const/arithmetic/MOD' k n))) & ('const/prim_rec/<' ('const/arithmetic/MOD' k n) n)))))).
tt('thm/arithmetic/DIV2_def_', def, (![n : 'type/num/num']: (('const/arithmetic/DIV2' n) = ('const/arithmetic/DIV' n ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))).
tt('thm/arithmetic/MOD_ONE_', ax, (![k : 'type/num/num']: (('const/arithmetic/MOD' k ('const/num/SUC' 'const/num/0')) = 'const/num/0'))).
tt('thm/arithmetic/MOD_1_', ax, (![k : 'type/num/num']: (('const/arithmetic/MOD' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) = 'const/num/0'))).
tt('thm/arithmetic/DIV_LESS_EQ_', ax, (![n : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' n) => (![k : 'type/num/num']: ('const/arithmetic/<=' ('const/arithmetic/DIV' k n) k))))).
tt('thm/arithmetic/DIV_UNIQUE_', ax, (![n : 'type/num/num', k : 'type/num/num', q : 'type/num/num']: ((?[r : 'type/num/num']: ((k = ('const/arithmetic/+' ('const/arithmetic/*' q n) r)) & ('const/prim_rec/<' r n))) => (('const/arithmetic/DIV' k n) = q)))).
tt('thm/arithmetic/MOD_UNIQUE_', ax, (![n : 'type/num/num', k : 'type/num/num', r : 'type/num/num']: ((?[q : 'type/num/num']: ((k = ('const/arithmetic/+' ('const/arithmetic/*' q n) r)) & ('const/prim_rec/<' r n))) => (('const/arithmetic/MOD' k n) = r)))).
tt('thm/arithmetic/DIV_MULT_', ax, (![n : 'type/num/num', r : 'type/num/num']: (('const/prim_rec/<' r n) => (![q : 'type/num/num']: (('const/arithmetic/DIV' ('const/arithmetic/+' ('const/arithmetic/*' q n) r) n) = q))))).
tt('thm/arithmetic/LESS_MOD_', ax, (![n : 'type/num/num', k : 'type/num/num']: (('const/prim_rec/<' k n) => (('const/arithmetic/MOD' k n) = k)))).
tt('thm/arithmetic/MOD_EQ_0_', ax, (![n : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' n) => (![k : 'type/num/num']: (('const/arithmetic/MOD' ('const/arithmetic/*' k n) n) = 'const/num/0'))))).
tt('thm/arithmetic/ZERO_MOD_', ax, (![n : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' n) => (('const/arithmetic/MOD' 'const/num/0' n) = 'const/num/0')))).
tt('thm/arithmetic/ZERO_DIV_', ax, (![n : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' n) => (('const/arithmetic/DIV' 'const/num/0' n) = 'const/num/0')))).
tt('thm/arithmetic/MOD_MULT_', ax, (![n : 'type/num/num', r : 'type/num/num']: (('const/prim_rec/<' r n) => (![q : 'type/num/num']: (('const/arithmetic/MOD' ('const/arithmetic/+' ('const/arithmetic/*' q n) r) n) = r))))).
tt('thm/arithmetic/MOD_TIMES_', ax, (![n : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' n) => (![q : 'type/num/num', r : 'type/num/num']: (('const/arithmetic/MOD' ('const/arithmetic/+' ('const/arithmetic/*' q n) r) n) = ('const/arithmetic/MOD' r n)))))).
tt('thm/arithmetic/MOD_TIMES_SUB_', ax, (![n : 'type/num/num', q : 'type/num/num', r : 'type/num/num']: ((('const/prim_rec/<' 'const/num/0' n) & (('const/prim_rec/<' 'const/num/0' q) & ('const/arithmetic/<=' r n))) => (('const/arithmetic/MOD' ('const/arithmetic/-' ('const/arithmetic/*' q n) r) n) = ('const/arithmetic/MOD' ('const/arithmetic/-' n r) n))))).
tt('thm/arithmetic/MOD_PLUS_', ax, (![n : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' n) => (![j : 'type/num/num', k : 'type/num/num']: (('const/arithmetic/MOD' ('const/arithmetic/+' ('const/arithmetic/MOD' j n) ('const/arithmetic/MOD' k n)) n) = ('const/arithmetic/MOD' ('const/arithmetic/+' j k) n)))))).
tt('thm/arithmetic/MOD_MOD_', ax, (![n : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' n) => (![k : 'type/num/num']: (('const/arithmetic/MOD' ('const/arithmetic/MOD' k n) n) = ('const/arithmetic/MOD' k n)))))).
tt('thm/arithmetic/LESS_DIV_EQ_ZERO_', ax, (![r : 'type/num/num', n : 'type/num/num']: (('const/prim_rec/<' r n) => (('const/arithmetic/DIV' r n) = 'const/num/0')))).
tt('thm/arithmetic/MULT_DIV_', ax, (![n : 'type/num/num', q : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' n) => (('const/arithmetic/DIV' ('const/arithmetic/*' q n) n) = q)))).
tt('thm/arithmetic/ADD_DIV_ADD_DIV_', ax, (![n : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' n) => (![x : 'type/num/num', r : 'type/num/num']: (('const/arithmetic/DIV' ('const/arithmetic/+' ('const/arithmetic/*' x n) r) n) = ('const/arithmetic/+' x ('const/arithmetic/DIV' r n))))))).
tt('thm/arithmetic/ADD_DIV_RWT_', ax, (![n : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' n) => (![m : 'type/num/num', p : 'type/num/num']: (((('const/arithmetic/MOD' m n) = 'const/num/0') | (('const/arithmetic/MOD' p n) = 'const/num/0')) => (('const/arithmetic/DIV' ('const/arithmetic/+' m p) n) = ('const/arithmetic/+' ('const/arithmetic/DIV' m n) ('const/arithmetic/DIV' p n)))))))).
tt('thm/arithmetic/MOD_MULT_MOD_', ax, (![m : 'type/num/num', n : 'type/num/num']: ((('const/prim_rec/<' 'const/num/0' n) & ('const/prim_rec/<' 'const/num/0' m)) => (![x : 'type/num/num']: (('const/arithmetic/MOD' ('const/arithmetic/MOD' x ('const/arithmetic/*' n m)) n) = ('const/arithmetic/MOD' x n)))))).
tt('thm/arithmetic/DIV_ONE_', ax, (![q : 'type/num/num']: (('const/arithmetic/DIV' q ('const/num/SUC' 'const/num/0')) = q))).
tt('thm/arithmetic/DIV_1_', ax, (![q : 'type/num/num']: (('const/arithmetic/DIV' q ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) = q))).
tt('thm/arithmetic/DIVMOD_ID_', ax, (![n : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' n) => ((('const/arithmetic/DIV' n n) = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) & (('const/arithmetic/MOD' n n) = 'const/num/0'))))).
tt('thm/arithmetic/DIV_DIV_DIV_MULT_', ax, (![m : 'type/num/num', n : 'type/num/num']: ((('const/prim_rec/<' 'const/num/0' m) & ('const/prim_rec/<' 'const/num/0' n)) => (![x : 'type/num/num']: (('const/arithmetic/DIV' ('const/arithmetic/DIV' x m) n) = ('const/arithmetic/DIV' x ('const/arithmetic/*' m n))))))).
tt('thm/arithmetic/SUC_PRE_', ax, (![m : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' m) = (('const/num/SUC' ('const/prim_rec/PRE' m)) = m)))).
tt('thm/arithmetic/DIV_LESS_', ax, (![n : 'type/num/num', d : 'type/num/num']: ((('const/prim_rec/<' 'const/num/0' n) & ('const/prim_rec/<' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) d)) => ('const/prim_rec/<' ('const/arithmetic/DIV' n d) n)))).
tt('thm/arithmetic/MOD_LESS_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' n) => ('const/prim_rec/<' ('const/arithmetic/MOD' m n) n)))).
tt('thm/arithmetic/ADD_MODULUS_0', ax, (![n : 'type/num/num', x : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' n) => (('const/arithmetic/MOD' ('const/arithmetic/+' x n) n) = ('const/arithmetic/MOD' x n))))).
tt('thm/arithmetic/ADD_MODULUS_e1', ax, (![n : 'type/num/num', x : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' n) => (('const/arithmetic/MOD' ('const/arithmetic/+' n x) n) = ('const/arithmetic/MOD' x n))))).
tt('thm/arithmetic/ADD_MODULUS_LEFT_', ax, (![n : 'type/num/num', x : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' n) => (('const/arithmetic/MOD' ('const/arithmetic/+' x n) n) = ('const/arithmetic/MOD' x n))))).
tt('thm/arithmetic/ADD_MODULUS_RIGHT_', ax, (![n : 'type/num/num', x : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' n) => (('const/arithmetic/MOD' ('const/arithmetic/+' n x) n) = ('const/arithmetic/MOD' x n))))).
tt('thm/arithmetic/DIV_P_', ax, (![P : ('type/num/num' > $o), p : 'type/num/num', q : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' q) => ((P ('const/arithmetic/DIV' p q)) = (?[k : 'type/num/num', r : 'type/num/num']: ((p = ('const/arithmetic/+' ('const/arithmetic/*' k q) r)) & (('const/prim_rec/<' r q) & (P k)))))))).
tt('thm/arithmetic/DIV_P_UNIV_', ax, (![P : ('type/num/num' > $o), m : 'type/num/num', n : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' n) => ((P ('const/arithmetic/DIV' m n)) = (![q : 'type/num/num', r : 'type/num/num']: (((m = ('const/arithmetic/+' ('const/arithmetic/*' q n) r)) & ('const/prim_rec/<' r n)) => (P q))))))).
tt('thm/arithmetic/MOD_P_', ax, (![P : ('type/num/num' > $o), p : 'type/num/num', q : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' q) => ((P ('const/arithmetic/MOD' p q)) = (?[k : 'type/num/num', r : 'type/num/num']: ((p = ('const/arithmetic/+' ('const/arithmetic/*' k q) r)) & (('const/prim_rec/<' r q) & (P r)))))))).
tt('thm/arithmetic/MOD_P_UNIV_', ax, (![P : ('type/num/num' > $o), m : 'type/num/num', n : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' n) => ((P ('const/arithmetic/MOD' m n)) = (![q : 'type/num/num', r : 'type/num/num']: (((m = ('const/arithmetic/+' ('const/arithmetic/*' q n) r)) & ('const/prim_rec/<' r n)) => (P r))))))).
tt('thm/arithmetic/MOD_TIMES2_', ax, (![n : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' n) => (![j : 'type/num/num', k : 'type/num/num']: (('const/arithmetic/MOD' ('const/arithmetic/*' ('const/arithmetic/MOD' j n) ('const/arithmetic/MOD' k n)) n) = ('const/arithmetic/MOD' ('const/arithmetic/*' j k) n)))))).
tt('thm/arithmetic/MOD_COMMON_FACTOR_', ax, (![n : 'type/num/num', p : 'type/num/num', q : 'type/num/num']: ((('const/prim_rec/<' 'const/num/0' n) & ('const/prim_rec/<' 'const/num/0' q)) => (('const/arithmetic/*' n ('const/arithmetic/MOD' p q)) = ('const/arithmetic/MOD' ('const/arithmetic/*' n p) ('const/arithmetic/*' n q)))))).
tt('thm/arithmetic/X_MOD_Y_EQ_X_', ax, (![x : 'type/num/num', y : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' y) => ((('const/arithmetic/MOD' x y) = x) = ('const/prim_rec/<' x y))))).
tt('thm/arithmetic/DIV_LE_MONOTONE_', ax, (![n : 'type/num/num', x : 'type/num/num', y : 'type/num/num']: ((('const/prim_rec/<' 'const/num/0' n) & ('const/arithmetic/<=' x y)) => ('const/arithmetic/<=' ('const/arithmetic/DIV' x n) ('const/arithmetic/DIV' y n))))).
tt('thm/arithmetic/LE_LT1_', ax, (![x : 'type/num/num', y : 'type/num/num']: (('const/arithmetic/<=' x y) = ('const/prim_rec/<' x ('const/arithmetic/+' y ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))).
tt('thm/arithmetic/X_LE_DIV_', ax, (![x : 'type/num/num', y : 'type/num/num', z : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' z) => (('const/arithmetic/<=' x ('const/arithmetic/DIV' y z)) = ('const/arithmetic/<=' ('const/arithmetic/*' x z) y))))).
tt('thm/arithmetic/X_LT_DIV_', ax, (![x : 'type/num/num', y : 'type/num/num', z : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' z) => (('const/prim_rec/<' x ('const/arithmetic/DIV' y z)) = ('const/arithmetic/<=' ('const/arithmetic/*' ('const/arithmetic/+' x ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) z) y))))).
tt('thm/arithmetic/DIV_LT_X_', ax, (![x : 'type/num/num', y : 'type/num/num', z : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' z) => (('const/prim_rec/<' ('const/arithmetic/DIV' y z) x) = ('const/prim_rec/<' y ('const/arithmetic/*' x z)))))).
tt('thm/arithmetic/DIV_LE_X_', ax, (![x : 'type/num/num', y : 'type/num/num', z : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' z) => (('const/arithmetic/<=' ('const/arithmetic/DIV' y z) x) = ('const/prim_rec/<' y ('const/arithmetic/*' ('const/arithmetic/+' x ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) z)))))).
tt('thm/arithmetic/DIV_EQ_X_', ax, (![x : 'type/num/num', y : 'type/num/num', z : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' z) => ((('const/arithmetic/DIV' y z) = x) = (('const/arithmetic/<=' ('const/arithmetic/*' x z) y) & ('const/prim_rec/<' y ('const/arithmetic/*' ('const/num/SUC' x) z))))))).
tt('thm/arithmetic/DIV_MOD_MOD_DIV_', ax, (![m : 'type/num/num', n : 'type/num/num', k : 'type/num/num']: ((('const/prim_rec/<' 'const/num/0' n) & ('const/prim_rec/<' 'const/num/0' k)) => (('const/arithmetic/MOD' ('const/arithmetic/DIV' m n) k) = ('const/arithmetic/DIV' ('const/arithmetic/MOD' m ('const/arithmetic/*' n k)) n))))).
tt('thm/arithmetic/MULT_EQ_DIV_', ax, (![z : 'type/num/num', y : 'type/num/num', x : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' x) => ((('const/arithmetic/*' x y) = z) = ((y = ('const/arithmetic/DIV' z x)) & (('const/arithmetic/MOD' z x) = 'const/num/0')))))).
tt('thm/arithmetic/NUMERAL_MULT_EQ_DIV_0', ax, (![z : 'type/num/num', y : 'type/num/num', x : 'type/num/num']: ((('const/arithmetic/*' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' x)) y) = ('const/arithmetic/NUMERAL' z)) = ((y = ('const/arithmetic/DIV' ('const/arithmetic/NUMERAL' z) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' x)))) & (('const/arithmetic/MOD' ('const/arithmetic/NUMERAL' z) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' x))) = 'const/num/0'))))).
tt('thm/arithmetic/NUMERAL_MULT_EQ_DIV_e1', ax, (![z : 'type/num/num', y : 'type/num/num', x : 'type/num/num']: ((('const/arithmetic/*' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' x)) y) = ('const/arithmetic/NUMERAL' z)) = ((y = ('const/arithmetic/DIV' ('const/arithmetic/NUMERAL' z) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' x)))) & (('const/arithmetic/MOD' ('const/arithmetic/NUMERAL' z) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' x))) = 'const/num/0'))))).
tt('thm/arithmetic/MOD_EQ_0_DIVISOR_', ax, (![n : 'type/num/num', k : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' n) => ((('const/arithmetic/MOD' k n) = 'const/num/0') = (?[d : 'type/num/num']: (k = ('const/arithmetic/*' d n))))))).
tt('thm/arithmetic/MOD_SUC_', ax, (![y : 'type/num/num', x : 'type/num/num']: ((('const/prim_rec/<' 'const/num/0' y) & (~ (('const/num/SUC' x) = ('const/arithmetic/*' ('const/num/SUC' ('const/arithmetic/DIV' x y)) y)))) => (('const/arithmetic/MOD' ('const/num/SUC' x) y) = ('const/num/SUC' ('const/arithmetic/MOD' x y)))))).
tt('thm/arithmetic/MOD_SUC_IFF_', ax, (![y : 'type/num/num', x : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' y) => ((('const/arithmetic/MOD' ('const/num/SUC' x) y) = ('const/num/SUC' ('const/arithmetic/MOD' x y))) = (~ (('const/num/SUC' x) = ('const/arithmetic/*' ('const/num/SUC' ('const/arithmetic/DIV' x y)) y))))))).
tt('thm/arithmetic/ONE_MOD_', ax, (![n : 'type/num/num']: (('const/prim_rec/<' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) n) => (('const/arithmetic/MOD' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) n) = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
tt('thm/arithmetic/ONE_MOD_IFF_', ax, (![n : 'type/num/num']: (('const/prim_rec/<' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) n) = (('const/prim_rec/<' 'const/num/0' n) & (('const/arithmetic/MOD' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) n) = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))).
tt('thm/arithmetic/MOD_LESS_EQ_', ax, (![y : 'type/num/num', x : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' y) => ('const/arithmetic/<=' ('const/arithmetic/MOD' x y) x)))).
tt('thm/arithmetic/MOD_LIFT_PLUS_', ax, (![x : 'type/num/num', n : 'type/num/num', k : 'type/num/num']: ((('const/prim_rec/<' 'const/num/0' n) & ('const/prim_rec/<' k ('const/arithmetic/-' n ('const/arithmetic/MOD' x n)))) => (('const/arithmetic/MOD' ('const/arithmetic/+' x k) n) = ('const/arithmetic/+' ('const/arithmetic/MOD' x n) k))))).
tt('thm/arithmetic/MOD_LIFT_PLUS_IFF_', ax, (![x : 'type/num/num', n : 'type/num/num', k : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' n) => ((('const/arithmetic/MOD' ('const/arithmetic/+' x k) n) = ('const/arithmetic/+' ('const/arithmetic/MOD' x n) k)) = ('const/prim_rec/<' k ('const/arithmetic/-' n ('const/arithmetic/MOD' x n))))))).
tt('thm/arithmetic/num_case_cong_', ax, ![A : $t]: (!['v\'' : A, 'f\'' : ('type/num/num' > A), M : 'type/num/num', 'M\'' : 'type/num/num', v : A, f : ('type/num/num' > A)]: (((M = 'M\'') & ((('M\'' = 'const/num/0') => (v = 'v\'')) & (![n : 'type/num/num']: (('M\'' = ('const/num/SUC' n)) => ((f n) = ('f\'' n)))))) => ((('const/arithmetic/num_CASE' A) M v f) = (('const/arithmetic/num_CASE' A) 'M\'' 'v\'' 'f\''))))).
tt('thm/arithmetic/SUC_ELIM_THM_', ax, (![P : ('type/num/num' > ('type/num/num' > $o))]: ((![n : 'type/num/num']: (P ('const/num/SUC' n) n)) = (![n : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' n) => (P n ('const/arithmetic/-' n ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))).
tt('thm/arithmetic/SUC_ELIM_NUMERALS_', ax, ![A : $t]: (![f : ('type/num/num' > ('type/num/num' > A)), g : ('type/num/num' > A)]: ((![n : 'type/num/num']: ((g ('const/num/SUC' n)) = (f n ('const/num/SUC' n)))) = ((![n : 'type/num/num']: ((g ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))) = (f ('const/arithmetic/-' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))))) & (![n : 'type/num/num']: ((g ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n))) = (f ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n))))))))).
tt('thm/arithmetic/SUB_ELIM_THM_', ax, (![b : 'type/num/num', a : 'type/num/num', P : ('type/num/num' > $o)]: ((P ('const/arithmetic/-' a b)) = (![d : 'type/num/num']: (((b = ('const/arithmetic/+' a d)) => (P 'const/num/0')) & ((a = ('const/arithmetic/+' b d)) => (P d))))))).
tt('thm/arithmetic/PRE_ELIM_THM_', ax, (![n : 'type/num/num', P : ('type/num/num' > $o)]: ((P ('const/prim_rec/PRE' n)) = (![m : 'type/num/num']: (((n = 'const/num/0') => (P 'const/num/0')) & ((n = ('const/num/SUC' m)) => (P m))))))).
tt('thm/arithmetic/MULT_INCREASES_', ax, (![m : 'type/num/num', n : 'type/num/num']: ((('const/prim_rec/<' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) m) & ('const/prim_rec/<' 'const/num/0' n)) => ('const/arithmetic/<=' ('const/num/SUC' n) ('const/arithmetic/*' m n))))).
tt('thm/arithmetic/EXP_ALWAYS_BIG_ENOUGH_', ax, (![b : 'type/num/num']: (('const/prim_rec/<' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) b) => (![n : 'type/num/num']: (?[m : 'type/num/num']: ('const/arithmetic/<=' n ('const/arithmetic/EXP' b m))))))).
tt('thm/arithmetic/EXP_EQ_0_', ax, (![n : 'type/num/num', m : 'type/num/num']: ((('const/arithmetic/EXP' n m) = 'const/num/0') = ((n = 'const/num/0') & ('const/prim_rec/<' 'const/num/0' m))))).
tt('thm/arithmetic/ZERO_LT_EXP_', ax, (![y : 'type/num/num', x : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' ('const/arithmetic/EXP' x y)) = (('const/prim_rec/<' 'const/num/0' x) | (y = 'const/num/0'))))).
tt('thm/arithmetic/EXP_1_0', ax, (![n : 'type/num/num']: (('const/arithmetic/EXP' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) n) = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/arithmetic/EXP_1_e1', ax, (![n : 'type/num/num']: (('const/arithmetic/EXP' n ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) = n))).
tt('thm/arithmetic/EXP_EQ_1_', ax, (![n : 'type/num/num', m : 'type/num/num']: ((('const/arithmetic/EXP' n m) = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) = ((n = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) | (m = 'const/num/0'))))).
tt('thm/arithmetic/EXP_BASE_LE_MONO_', ax, (![b : 'type/num/num']: (('const/prim_rec/<' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) b) => (![n : 'type/num/num', m : 'type/num/num']: (('const/arithmetic/<=' ('const/arithmetic/EXP' b m) ('const/arithmetic/EXP' b n)) = ('const/arithmetic/<=' m n)))))).
tt('thm/arithmetic/EXP_BASE_LT_MONO_', ax, (![b : 'type/num/num']: (('const/prim_rec/<' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) b) => (![n : 'type/num/num', m : 'type/num/num']: (('const/prim_rec/<' ('const/arithmetic/EXP' b m) ('const/arithmetic/EXP' b n)) = ('const/prim_rec/<' m n)))))).
tt('thm/arithmetic/EXP_BASE_INJECTIVE_', ax, (![b : 'type/num/num']: (('const/prim_rec/<' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) b) => (![n : 'type/num/num', m : 'type/num/num']: ((('const/arithmetic/EXP' b n) = ('const/arithmetic/EXP' b m)) = (n = m)))))).
tt('thm/arithmetic/EXP_BASE_LEQ_MONO_IMP_', ax, (![n : 'type/num/num', m : 'type/num/num', b : 'type/num/num']: ((('const/prim_rec/<' 'const/num/0' b) & ('const/arithmetic/<=' m n)) => ('const/arithmetic/<=' ('const/arithmetic/EXP' b m) ('const/arithmetic/EXP' b n))))).
tt('thm/arithmetic/EXP_BASE_LEQ_MONO_SUC_IMP_', ax, (![n : 'type/num/num', m : 'type/num/num', b : 'type/num/num']: (('const/arithmetic/<=' m n) => ('const/arithmetic/<=' ('const/arithmetic/EXP' ('const/num/SUC' b) m) ('const/arithmetic/EXP' ('const/num/SUC' b) n))))).
tt('thm/arithmetic/EXP_BASE_LE_IFF_', ax, (![n : 'type/num/num', m : 'type/num/num', b : 'type/num/num']: (('const/arithmetic/<=' ('const/arithmetic/EXP' b m) ('const/arithmetic/EXP' b n)) = (((b = 'const/num/0') & (n = 'const/num/0')) | (((b = 'const/num/0') & ('const/prim_rec/<' 'const/num/0' m)) | ((b = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) | (('const/prim_rec/<' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) b) & ('const/arithmetic/<=' m n)))))))).
tt('thm/arithmetic/X_LE_X_EXP_', ax, (![x : 'type/num/num', n : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' n) => ('const/arithmetic/<=' x ('const/arithmetic/EXP' x n))))).
tt('thm/arithmetic/X_LT_EXP_X_', ax, (![x : 'type/num/num', b : 'type/num/num']: (('const/prim_rec/<' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) b) => ('const/prim_rec/<' x ('const/arithmetic/EXP' b x))))).
tt('thm/arithmetic/ZERO_EXP_', ax, (![x : 'type/num/num']: (('const/arithmetic/EXP' 'const/num/0' x) = (('const/bool/COND' 'type/num/num') (x = 'const/num/0') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) 'const/num/0')))).
tt('thm/arithmetic/X_LT_EXP_X_IFF_', ax, (![x : 'type/num/num', b : 'type/num/num']: (('const/prim_rec/<' x ('const/arithmetic/EXP' b x)) = (('const/prim_rec/<' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) b) | (x = 'const/num/0'))))).
tt('thm/arithmetic/EXP_EXP_LT_MONO_', ax, (![n : 'type/num/num', a : 'type/num/num', b : 'type/num/num']: (('const/prim_rec/<' ('const/arithmetic/EXP' a n) ('const/arithmetic/EXP' b n)) = (('const/prim_rec/<' a b) & ('const/prim_rec/<' 'const/num/0' n))))).
tt('thm/arithmetic/EXP_EXP_LE_MONO_', ax, (![n : 'type/num/num', a : 'type/num/num', b : 'type/num/num']: (('const/arithmetic/<=' ('const/arithmetic/EXP' a n) ('const/arithmetic/EXP' b n)) = (('const/arithmetic/<=' a b) | (n = 'const/num/0'))))).
tt('thm/arithmetic/EXP_EXP_INJECTIVE_', ax, (![b1 : 'type/num/num', b2 : 'type/num/num', x : 'type/num/num']: ((('const/arithmetic/EXP' b1 x) = ('const/arithmetic/EXP' b2 x)) = ((x = 'const/num/0') | (b1 = b2))))).
tt('thm/arithmetic/EXP_SUB_', ax, (![p : 'type/num/num', q : 'type/num/num', n : 'type/num/num']: ((('const/prim_rec/<' 'const/num/0' n) & ('const/arithmetic/<=' q p)) => (('const/arithmetic/EXP' n ('const/arithmetic/-' p q)) = ('const/arithmetic/DIV' ('const/arithmetic/EXP' n p) ('const/arithmetic/EXP' n q)))))).
tt('thm/arithmetic/EXP_SUB_NUMERAL_', ax, (![x : 'type/num/num', n : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' n) => ((('const/arithmetic/DIV' ('const/arithmetic/EXP' n ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' x))) n) = ('const/arithmetic/EXP' n ('const/arithmetic/-' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' x)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) & (('const/arithmetic/DIV' ('const/arithmetic/EXP' n ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' x))) n) = ('const/arithmetic/EXP' n ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' x)))))))).
tt('thm/arithmetic/EXP_BASE_MULT_', ax, (![z : 'type/num/num', x : 'type/num/num', y : 'type/num/num']: (('const/arithmetic/EXP' ('const/arithmetic/*' x y) z) = ('const/arithmetic/*' ('const/arithmetic/EXP' x z) ('const/arithmetic/EXP' y z))))).
tt('thm/arithmetic/EXP_EXP_MULT_', ax, (![z : 'type/num/num', x : 'type/num/num', y : 'type/num/num']: (('const/arithmetic/EXP' x ('const/arithmetic/*' y z)) = ('const/arithmetic/EXP' ('const/arithmetic/EXP' x y) z)))).
tt('thm/arithmetic/MAX_DEF_', def, (![m : 'type/num/num', n : 'type/num/num']: (('const/arithmetic/MAX' m n) = (('const/bool/COND' 'type/num/num') ('const/prim_rec/<' m n) n m)))).
tt('thm/arithmetic/MIN_DEF_', def, (![m : 'type/num/num', n : 'type/num/num']: (('const/arithmetic/MIN' m n) = (('const/bool/COND' 'type/num/num') ('const/prim_rec/<' m n) m n)))).
tt('thm/arithmetic/MAX_COMM_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/arithmetic/MAX' m n) = ('const/arithmetic/MAX' n m)))).
tt('thm/arithmetic/MIN_COMM_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/arithmetic/MIN' m n) = ('const/arithmetic/MIN' n m)))).
tt('thm/arithmetic/MAX_ASSOC_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: (('const/arithmetic/MAX' m ('const/arithmetic/MAX' n p)) = ('const/arithmetic/MAX' ('const/arithmetic/MAX' m n) p)))).
tt('thm/arithmetic/MIN_ASSOC_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: (('const/arithmetic/MIN' m ('const/arithmetic/MIN' n p)) = ('const/arithmetic/MIN' ('const/arithmetic/MIN' m n) p)))).
tt('thm/arithmetic/MIN_MAX_EQ_', ax, (![m : 'type/num/num', n : 'type/num/num']: ((('const/arithmetic/MIN' m n) = ('const/arithmetic/MAX' m n)) = (m = n)))).
tt('thm/arithmetic/MIN_MAX_LT_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/prim_rec/<' ('const/arithmetic/MIN' m n) ('const/arithmetic/MAX' m n)) = (~ (m = n))))).
tt('thm/arithmetic/MIN_MAX_LE_', ax, (![m : 'type/num/num', n : 'type/num/num']: ('const/arithmetic/<=' ('const/arithmetic/MIN' m n) ('const/arithmetic/MAX' m n)))).
tt('thm/arithmetic/MIN_MAX_PRED_', ax, (![P : ('type/num/num' > $o), m : 'type/num/num', n : 'type/num/num']: (((P m) & (P n)) => ((P ('const/arithmetic/MIN' m n)) & (P ('const/arithmetic/MAX' m n)))))).
tt('thm/arithmetic/MIN_LT_0', ax, (![p : 'type/num/num', n : 'type/num/num', m : 'type/num/num']: (('const/prim_rec/<' ('const/arithmetic/MIN' m n) p) = (('const/prim_rec/<' m p) | ('const/prim_rec/<' n p))))).
tt('thm/arithmetic/MIN_LT_e1', ax, (![p : 'type/num/num', n : 'type/num/num', m : 'type/num/num']: (('const/prim_rec/<' p ('const/arithmetic/MIN' m n)) = (('const/prim_rec/<' p m) & ('const/prim_rec/<' p n))))).
tt('thm/arithmetic/MAX_LT_0', ax, (![p : 'type/num/num', n : 'type/num/num', m : 'type/num/num']: (('const/prim_rec/<' p ('const/arithmetic/MAX' m n)) = (('const/prim_rec/<' p m) | ('const/prim_rec/<' p n))))).
tt('thm/arithmetic/MAX_LT_e1', ax, (![p : 'type/num/num', n : 'type/num/num', m : 'type/num/num']: (('const/prim_rec/<' ('const/arithmetic/MAX' m n) p) = (('const/prim_rec/<' m p) & ('const/prim_rec/<' n p))))).
tt('thm/arithmetic/MIN_LE_0', ax, (![p : 'type/num/num', n : 'type/num/num', m : 'type/num/num']: (('const/arithmetic/<=' ('const/arithmetic/MIN' m n) p) = (('const/arithmetic/<=' m p) | ('const/arithmetic/<=' n p))))).
tt('thm/arithmetic/MIN_LE_e1', ax, (![p : 'type/num/num', n : 'type/num/num', m : 'type/num/num']: (('const/arithmetic/<=' p ('const/arithmetic/MIN' m n)) = (('const/arithmetic/<=' p m) & ('const/arithmetic/<=' p n))))).
tt('thm/arithmetic/MAX_LE_0', ax, (![p : 'type/num/num', n : 'type/num/num', m : 'type/num/num']: (('const/arithmetic/<=' p ('const/arithmetic/MAX' m n)) = (('const/arithmetic/<=' p m) | ('const/arithmetic/<=' p n))))).
tt('thm/arithmetic/MAX_LE_e1', ax, (![p : 'type/num/num', n : 'type/num/num', m : 'type/num/num']: (('const/arithmetic/<=' ('const/arithmetic/MAX' m n) p) = (('const/arithmetic/<=' m p) & ('const/arithmetic/<=' n p))))).
tt('thm/arithmetic/MIN_0_0', ax, (![n : 'type/num/num']: (('const/arithmetic/MIN' n 'const/num/0') = 'const/num/0'))).
tt('thm/arithmetic/MIN_0_e1', ax, (![n : 'type/num/num']: (('const/arithmetic/MIN' 'const/num/0' n) = 'const/num/0'))).
tt('thm/arithmetic/MAX_0_0', ax, (![n : 'type/num/num']: (('const/arithmetic/MAX' n 'const/num/0') = n))).
tt('thm/arithmetic/MAX_0_e1', ax, (![n : 'type/num/num']: (('const/arithmetic/MAX' 'const/num/0' n) = n))).
tt('thm/arithmetic/MIN_IDEM_', ax, (![n : 'type/num/num']: (('const/arithmetic/MIN' n n) = n))).
tt('thm/arithmetic/MAX_IDEM_', ax, (![n : 'type/num/num']: (('const/arithmetic/MAX' n n) = n))).
tt('thm/arithmetic/EXISTS_GREATEST_', ax, (![P : ('type/num/num' > $o)]: (((?[x : 'type/num/num']: (P x)) & (?[x : 'type/num/num']: (![y : 'type/num/num']: (('const/arithmetic/>' y x) => (~ (P y)))))) = (?[x : 'type/num/num']: ((P x) & (![y : 'type/num/num']: (('const/arithmetic/>' y x) => (~ (P y))))))))).
tt('thm/arithmetic/EXISTS_NUM_', ax, (![P : ('type/num/num' > $o)]: ((?[n : 'type/num/num']: (P n)) = ((P 'const/num/0') | (?[m : 'type/num/num']: (P ('const/num/SUC' m))))))).
tt('thm/arithmetic/FORALL_NUM_', ax, (![P : ('type/num/num' > $o)]: ((![n : 'type/num/num']: (P n)) = ((P 'const/num/0') & (![n : 'type/num/num']: (P ('const/num/SUC' n))))))).
tt('thm/arithmetic/BOUNDED_FORALL_THM_', ax, (![P : ('type/num/num' > $o), c : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' c) => ((![n : 'type/num/num']: (('const/prim_rec/<' n c) => (P n))) = ((P ('const/arithmetic/-' c ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) & (![n : 'type/num/num']: (('const/prim_rec/<' n ('const/arithmetic/-' c ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) => (P n)))))))).
tt('thm/arithmetic/BOUNDED_EXISTS_THM_', ax, (![P : ('type/num/num' > $o), c : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' c) => ((?[n : 'type/num/num']: (('const/prim_rec/<' n c) & (P n))) = ((P ('const/arithmetic/-' c ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) | (?[n : 'type/num/num']: (('const/prim_rec/<' n ('const/arithmetic/-' c ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) & (P n)))))))).
tt('thm/arithmetic/transitive_monotone_', ax, ![A : $t]: (![R : (A > (A > $o)), f : ('type/num/num' > A)]: (((('const/relation/transitive' A) R) & (![n : 'type/num/num']: (R (f n) (f ('const/num/SUC' n))))) => (![m : 'type/num/num', n : 'type/num/num']: (('const/prim_rec/<' m n) => (R (f m) (f n))))))).
tt('thm/arithmetic/STRICTLY_INCREASING_TC_', ax, (![f : ('type/num/num' > 'type/num/num')]: ((![n : 'type/num/num']: ('const/prim_rec/<' (f n) (f ('const/num/SUC' n)))) => (![m : 'type/num/num', n : 'type/num/num']: (('const/prim_rec/<' m n) => ('const/prim_rec/<' (f m) (f n))))))).
tt('thm/arithmetic/STRICTLY_INCREASING_ONE_ONE_', ax, (![f : ('type/num/num' > 'type/num/num')]: ((![n : 'type/num/num']: ('const/prim_rec/<' (f n) (f ('const/num/SUC' n)))) => (('const/bool/ONE_ONE' 'type/num/num' 'type/num/num') f)))).
tt('thm/arithmetic/ONE_ONE_UNBOUNDED_', ax, (![f : ('type/num/num' > 'type/num/num')]: ((('const/bool/ONE_ONE' 'type/num/num' 'type/num/num') f) => (![b : 'type/num/num']: (?[n : 'type/num/num']: ('const/prim_rec/<' b (f n))))))).
tt('thm/arithmetic/STRICTLY_INCREASING_UNBOUNDED_', ax, (![f : ('type/num/num' > 'type/num/num')]: ((![n : 'type/num/num']: ('const/prim_rec/<' (f n) (f ('const/num/SUC' n)))) => (![b : 'type/num/num']: (?[n : 'type/num/num']: ('const/prim_rec/<' b (f n))))))).
tt('thm/arithmetic/NOT_STRICTLY_DECREASING_', ax, (![f : ('type/num/num' > 'type/num/num')]: (~ (![n : 'type/num/num']: ('const/prim_rec/<' (f ('const/num/SUC' n)) (f n)))))).
tt('thm/arithmetic/ABS_DIFF_def_', def, (![n : 'type/num/num', m : 'type/num/num']: (('const/arithmetic/ABS_DIFF' n m) = (('const/bool/COND' 'type/num/num') ('const/prim_rec/<' n m) ('const/arithmetic/-' m n) ('const/arithmetic/-' n m))))).
tt('thm/arithmetic/ABS_DIFF_SYM_', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/arithmetic/ABS_DIFF' n m) = ('const/arithmetic/ABS_DIFF' m n)))).
tt('thm/arithmetic/ABS_DIFF_COMM_', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/arithmetic/ABS_DIFF' n m) = ('const/arithmetic/ABS_DIFF' m n)))).
tt('thm/arithmetic/ABS_DIFF_EQS_', ax, (![n : 'type/num/num']: (('const/arithmetic/ABS_DIFF' n n) = 'const/num/0'))).
tt('thm/arithmetic/ABS_DIFF_EQ_0_', ax, (![n : 'type/num/num', m : 'type/num/num']: ((('const/arithmetic/ABS_DIFF' n m) = 'const/num/0') = (n = m)))).
tt('thm/arithmetic/ABS_DIFF_ZERO_0', ax, (![n : 'type/num/num']: (('const/arithmetic/ABS_DIFF' n 'const/num/0') = n))).
tt('thm/arithmetic/ABS_DIFF_ZERO_e1', ax, (![n : 'type/num/num']: (('const/arithmetic/ABS_DIFF' 'const/num/0' n) = n))).
tt('thm/arithmetic/ABS_DIFF_TRIANGLE_', ax, (![x : 'type/num/num', y : 'type/num/num', z : 'type/num/num']: ('const/arithmetic/<=' ('const/arithmetic/ABS_DIFF' x z) ('const/arithmetic/+' ('const/arithmetic/ABS_DIFF' x y) ('const/arithmetic/ABS_DIFF' y z))))).
tt('thm/arithmetic/ABS_DIFF_ADD_SAME_', ax, (![n : 'type/num/num', m : 'type/num/num', p : 'type/num/num']: (('const/arithmetic/ABS_DIFF' ('const/arithmetic/+' n p) ('const/arithmetic/+' m p)) = ('const/arithmetic/ABS_DIFF' n m)))).
tt('thm/arithmetic/LT_SUB_RCANCEL_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: (('const/prim_rec/<' ('const/arithmetic/-' n m) ('const/arithmetic/-' p m)) = (('const/prim_rec/<' n p) & ('const/prim_rec/<' m p))))).
tt('thm/arithmetic/LE_SUB_RCANCEL_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: (('const/arithmetic/<=' ('const/arithmetic/-' n m) ('const/arithmetic/-' p m)) = (('const/arithmetic/<=' n m) | ('const/arithmetic/<=' n p))))).
tt('thm/arithmetic/ABS_DIFF_SUMS_', ax, (![n1 : 'type/num/num', n2 : 'type/num/num', m1 : 'type/num/num', m2 : 'type/num/num']: ('const/arithmetic/<=' ('const/arithmetic/ABS_DIFF' ('const/arithmetic/+' n1 n2) ('const/arithmetic/+' m1 m2)) ('const/arithmetic/+' ('const/arithmetic/ABS_DIFF' n1 m1) ('const/arithmetic/ABS_DIFF' n2 m2))))).
tt('thm/arithmetic/FUNPOW_SUC_', ax, ![A : $t]: (![f : (A > A), n : 'type/num/num', x : A]: ((('const/arithmetic/FUNPOW' A) f ('const/num/SUC' n) x) = (f (('const/arithmetic/FUNPOW' A) f n x))))).
tt('thm/arithmetic/FUNPOW_0_', ax, ![A : $t]: (![x : A, f : (A > A)]: ((('const/arithmetic/FUNPOW' A) f 'const/num/0' x) = x))).
tt('thm/arithmetic/FUNPOW_ADD_', ax, ![A : $t]: (![x : A, f : (A > A), m : 'type/num/num', n : 'type/num/num']: ((('const/arithmetic/FUNPOW' A) f ('const/arithmetic/+' m n) x) = (('const/arithmetic/FUNPOW' A) f m (('const/arithmetic/FUNPOW' A) f n x))))).
tt('thm/arithmetic/FUNPOW_1_', ax, ![A : $t]: (![x : A, f : (A > A)]: ((('const/arithmetic/FUNPOW' A) f ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) x) = (f x)))).
tt('thm/arithmetic/NRC_0_', ax, ![A : $t]: (![R : (A > (A > $o)), x : A, y : A]: ((('const/arithmetic/NRC' A) R 'const/num/0' x y) = (x = y)))).
tt('thm/arithmetic/NRC_1_', ax, ![A : $t]: (![y : A, x : A, R : (A > (A > $o))]: ((('const/arithmetic/NRC' A) R ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) x y) = (R x y)))).
tt('thm/arithmetic/NRC_ADD_I_', ax, ![A : $t]: (![R : (A > (A > $o)), m : 'type/num/num', n : 'type/num/num', x : A, y : A, z : A]: (((('const/arithmetic/NRC' A) R m x y) & (('const/arithmetic/NRC' A) R n y z)) => (('const/arithmetic/NRC' A) R ('const/arithmetic/+' m n) x z)))).
tt('thm/arithmetic/NRC_ADD_E_', ax, ![A : $t]: (![R : (A > (A > $o)), m : 'type/num/num', n : 'type/num/num', x : A, z : A]: ((('const/arithmetic/NRC' A) R ('const/arithmetic/+' m n) x z) => (?[y : A]: ((('const/arithmetic/NRC' A) R m x y) & (('const/arithmetic/NRC' A) R n y z)))))).
tt('thm/arithmetic/NRC_ADD_EQN_', ax, ![A : $t]: (![z : A, x : A, n : 'type/num/num', m : 'type/num/num', R : (A > (A > $o))]: ((('const/arithmetic/NRC' A) R ('const/arithmetic/+' m n) x z) = (?[y : A]: ((('const/arithmetic/NRC' A) R m x y) & (('const/arithmetic/NRC' A) R n y z)))))).
tt('thm/arithmetic/NRC_SUC_RECURSE_LEFT_', ax, ![A : $t]: (![y : A, x : A, n : 'type/num/num', R : (A > (A > $o))]: ((('const/arithmetic/NRC' A) R ('const/num/SUC' n) x y) = (?[z : A]: ((('const/arithmetic/NRC' A) R n x z) & (R z y)))))).
tt('thm/arithmetic/NRC_RTC_', ax, ![A : $t]: (![R : (A > (A > $o)), n : 'type/num/num', x : A, y : A]: ((('const/arithmetic/NRC' A) R n x y) => (('const/relation/RTC' A) R x y)))).
tt('thm/arithmetic/RTC_NRC_', ax, ![A : $t]: (![R : (A > (A > $o)), x : A, y : A]: ((('const/relation/RTC' A) R x y) => (?[n : 'type/num/num']: (('const/arithmetic/NRC' A) R n x y))))).
tt('thm/arithmetic/RTC_eq_NRC_', ax, ![A : $t]: (![R : (A > (A > $o)), x : A, y : A]: ((('const/relation/RTC' A) R x y) = (?[n : 'type/num/num']: (('const/arithmetic/NRC' A) R n x y))))).
tt('thm/arithmetic/TC_eq_NRC_', ax, ![A : $t]: (![R : (A > (A > $o)), x : A, y : A]: ((('const/relation/TC' A) R x y) = (?[n : 'type/num/num']: (('const/arithmetic/NRC' A) R ('const/num/SUC' n) x y))))).
tt('thm/arithmetic/LESS_EQUAL_DIFF_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/arithmetic/<=' m n) => (?[k : 'type/num/num']: (m = ('const/arithmetic/-' n k)))))).
tt('thm/arithmetic/MOD_2_', ax, (![n : 'type/num/num']: (('const/arithmetic/MOD' n ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) = (('const/bool/COND' 'type/num/num') ('const/arithmetic/EVEN' n) 'const/num/0' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
tt('thm/arithmetic/EVEN_MOD2_', ax, (![x : 'type/num/num']: (('const/arithmetic/EVEN' x) = (('const/arithmetic/MOD' x ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) = 'const/num/0')))).
tt('thm/arithmetic/SUC_MOD_', ax, (![n : 'type/num/num', a : 'type/num/num', b : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' n) => ((('const/arithmetic/MOD' ('const/num/SUC' a) n) = ('const/arithmetic/MOD' ('const/num/SUC' b) n)) = (('const/arithmetic/MOD' a n) = ('const/arithmetic/MOD' b n)))))).
tt('thm/arithmetic/ADD_MOD_', ax, (![n : 'type/num/num', a : 'type/num/num', b : 'type/num/num', p : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' n) => ((('const/arithmetic/MOD' ('const/arithmetic/+' a p) n) = ('const/arithmetic/MOD' ('const/arithmetic/+' b p) n)) = (('const/arithmetic/MOD' a n) = ('const/arithmetic/MOD' b n)))))).
tt('thm/arithmetic/MOD_ELIM_', ax, (![P : ('type/num/num' > $o), x : 'type/num/num', n : 'type/num/num']: ((('const/prim_rec/<' 'const/num/0' n) & ((P x) & (![y : 'type/num/num']: ((P ('const/arithmetic/+' y n)) => (P y))))) => (P ('const/arithmetic/MOD' x n))))).
tt('thm/arithmetic/DOUBLE_LT_', ax, (![p : 'type/num/num', q : 'type/num/num']: (('const/prim_rec/<' ('const/arithmetic/+' ('const/arithmetic/*' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) p) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/*' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) q)) = ('const/prim_rec/<' ('const/arithmetic/*' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) p) ('const/arithmetic/*' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) q))))).
tt('thm/arithmetic/EXP2_LT_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/prim_rec/<' ('const/arithmetic/DIV' n ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/EXP' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) m)) = ('const/prim_rec/<' n ('const/arithmetic/EXP' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) ('const/num/SUC' m)))))).
tt('thm/arithmetic/SUB_LESS_', ax, (![m : 'type/num/num', n : 'type/num/num']: ((('const/prim_rec/<' 'const/num/0' n) & ('const/arithmetic/<=' n m)) => ('const/prim_rec/<' ('const/arithmetic/-' m n) m)))).
tt('thm/arithmetic/SUB_MOD_', ax, (![m : 'type/num/num', n : 'type/num/num']: ((('const/prim_rec/<' 'const/num/0' n) & ('const/arithmetic/<=' n m)) => (('const/arithmetic/MOD' ('const/arithmetic/-' m n) n) = ('const/arithmetic/MOD' m n))))).
tt('thm/arithmetic/ONE_LT_MULT_IMP_', ax, (![p : 'type/num/num', q : 'type/num/num']: ((('const/prim_rec/<' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) p) & ('const/prim_rec/<' 'const/num/0' q)) => ('const/prim_rec/<' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) ('const/arithmetic/*' p q))))).
tt('thm/arithmetic/ONE_LT_MULT_', ax, (![x : 'type/num/num', y : 'type/num/num']: (('const/prim_rec/<' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) ('const/arithmetic/*' x y)) = ((('const/prim_rec/<' 'const/num/0' x) & ('const/prim_rec/<' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) y)) | (('const/prim_rec/<' 'const/num/0' y) & ('const/prim_rec/<' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) x)))))).
tt('thm/arithmetic/ONE_LT_EXP_', ax, (![x : 'type/num/num', y : 'type/num/num']: (('const/prim_rec/<' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) ('const/arithmetic/EXP' x y)) = (('const/prim_rec/<' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) x) & ('const/prim_rec/<' 'const/num/0' y))))).
tt('thm/arithmetic/findq_def_', def, ('const/arithmetic/findq' = (('const/relation/WFREC' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) 'type/num/num') (('const/prim_rec/measure' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) (('const/pair/UNCURRY' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num') 'type/num/num') (^[a : 'type/num/num']: (('const/pair/UNCURRY' 'type/num/num' 'type/num/num' 'type/num/num') (^[m : 'type/num/num', n : 'type/num/num']: ('const/arithmetic/-' m n)))))) (^[f : (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) > 'type/num/num')]: (('const/pair/UNCURRY' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num') 'type/num/num') (^[a : 'type/num/num']: (('const/pair/UNCURRY' 'type/num/num' 'type/num/num' 'type/num/num') (^[m : 'type/num/num', n : 'type/num/num']: (('const/bool/COND' 'type/num/num') (n = 'const/num/0') a (('const/bool/LET' 'type/num/num' 'type/num/num') (^[d : 'type/num/num']: (('const/bool/COND' 'type/num/num') ('const/prim_rec/<' m d) a (f (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) ('const/arithmetic/*' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) a) (('const/pair/,' 'type/num/num' 'type/num/num') m d))))) ('const/arithmetic/*' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) n))))))))))).
tt('thm/arithmetic/findq_thm_', ax, (![n : 'type/num/num', m : 'type/num/num', a : 'type/num/num']: (('const/arithmetic/findq' (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) a (('const/pair/,' 'type/num/num' 'type/num/num') m n))) = (('const/bool/COND' 'type/num/num') (n = 'const/num/0') a (('const/bool/LET' 'type/num/num' 'type/num/num') (^[d : 'type/num/num']: (('const/bool/COND' 'type/num/num') ('const/prim_rec/<' m d) a ('const/arithmetic/findq' (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) ('const/arithmetic/*' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) a) (('const/pair/,' 'type/num/num' 'type/num/num') m d))))) ('const/arithmetic/*' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) n)))))).
tt('thm/arithmetic/findq_eq_0_', ax, (![a : 'type/num/num', m : 'type/num/num', n : 'type/num/num']: ((('const/arithmetic/findq' (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) a (('const/pair/,' 'type/num/num' 'type/num/num') m n))) = 'const/num/0') = (a = 'const/num/0')))).
tt('thm/arithmetic/findq_divisor_', ax, (![n : 'type/num/num', m : 'type/num/num', a : 'type/num/num']: (('const/arithmetic/<=' n m) => ('const/arithmetic/<=' ('const/arithmetic/*' ('const/arithmetic/findq' (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) a (('const/pair/,' 'type/num/num' 'type/num/num') m n))) n) ('const/arithmetic/*' a m))))).
tt('thm/arithmetic/DIVMOD_DEF_', def, ('const/arithmetic/DIVMOD' = (('const/relation/WFREC' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) ('type/pair/prod' 'type/num/num' 'type/num/num')) (('const/prim_rec/measure' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) (('const/combin/o' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) ('const/pair/FST' 'type/num/num' 'type/num/num') ('const/pair/SND' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')))) (^[f : (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) > ('type/pair/prod' 'type/num/num' 'type/num/num'))]: (('const/pair/UNCURRY' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num') ('type/pair/prod' 'type/num/num' 'type/num/num')) (^[a : 'type/num/num']: (('const/pair/UNCURRY' 'type/num/num' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) (^[m : 'type/num/num', n : 'type/num/num']: (('const/bool/COND' ('type/pair/prod' 'type/num/num' 'type/num/num')) (n = 'const/num/0') (('const/pair/,' 'type/num/num' 'type/num/num') 'const/num/0' 'const/num/0') (('const/bool/COND' ('type/pair/prod' 'type/num/num' 'type/num/num')) ('const/prim_rec/<' m n) (('const/pair/,' 'type/num/num' 'type/num/num') a m) (('const/bool/LET' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) (^[q : 'type/num/num']: (f (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) ('const/arithmetic/+' a q) (('const/pair/,' 'type/num/num' 'type/num/num') ('const/arithmetic/-' m ('const/arithmetic/*' n q)) n)))) ('const/arithmetic/findq' (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) (('const/pair/,' 'type/num/num' 'type/num/num') m n)))))))))))))).
tt('thm/arithmetic/DIVMOD_THM_', ax, (![n : 'type/num/num', m : 'type/num/num', a : 'type/num/num']: (('const/arithmetic/DIVMOD' (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) a (('const/pair/,' 'type/num/num' 'type/num/num') m n))) = (('const/bool/COND' ('type/pair/prod' 'type/num/num' 'type/num/num')) (n = 'const/num/0') (('const/pair/,' 'type/num/num' 'type/num/num') 'const/num/0' 'const/num/0') (('const/bool/COND' ('type/pair/prod' 'type/num/num' 'type/num/num')) ('const/prim_rec/<' m n) (('const/pair/,' 'type/num/num' 'type/num/num') a m) (('const/bool/LET' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) (^[q : 'type/num/num']: ('const/arithmetic/DIVMOD' (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) ('const/arithmetic/+' a q) (('const/pair/,' 'type/num/num' 'type/num/num') ('const/arithmetic/-' m ('const/arithmetic/*' n q)) n)))) ('const/arithmetic/findq' (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) (('const/pair/,' 'type/num/num' 'type/num/num') m n))))))))).
tt('thm/arithmetic/MOD_SUB_', ax, (![q : 'type/num/num', n : 'type/num/num', m : 'type/num/num']: ((('const/prim_rec/<' 'const/num/0' n) & ('const/arithmetic/<=' ('const/arithmetic/*' n q) m)) => (('const/arithmetic/MOD' ('const/arithmetic/-' m ('const/arithmetic/*' n q)) n) = ('const/arithmetic/MOD' m n))))).
tt('thm/arithmetic/DIV_SUB_', ax, (![q : 'type/num/num', n : 'type/num/num', m : 'type/num/num']: ((('const/prim_rec/<' 'const/num/0' n) & ('const/arithmetic/<=' ('const/arithmetic/*' n q) m)) => (('const/arithmetic/DIV' ('const/arithmetic/-' m ('const/arithmetic/*' n q)) n) = ('const/arithmetic/-' ('const/arithmetic/DIV' m n) q))))).
tt('thm/arithmetic/DIVMOD_CORRECT_', ax, (![m : 'type/num/num', n : 'type/num/num', a : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' n) => (('const/arithmetic/DIVMOD' (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) a (('const/pair/,' 'type/num/num' 'type/num/num') m n))) = (('const/pair/,' 'type/num/num' 'type/num/num') ('const/arithmetic/+' a ('const/arithmetic/DIV' m n)) ('const/arithmetic/MOD' m n)))))).
tt('thm/arithmetic/DIVMOD_CALC_0', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' n) => (('const/arithmetic/DIV' m n) = (('const/pair/FST' 'type/num/num' 'type/num/num') ('const/arithmetic/DIVMOD' (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) 'const/num/0' (('const/pair/,' 'type/num/num' 'type/num/num') m n)))))))).
tt('thm/arithmetic/DIVMOD_CALC_e1', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' n) => (('const/arithmetic/MOD' m n) = (('const/pair/SND' 'type/num/num' 'type/num/num') ('const/arithmetic/DIVMOD' (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) 'const/num/0' (('const/pair/,' 'type/num/num' 'type/num/num') m n)))))))).
tt('thm/arithmetic/MODEQ_DEF_', def, (![n : 'type/num/num', m1 : 'type/num/num', m2 : 'type/num/num']: (('const/arithmetic/MODEQ' n m1 m2) = (?[a : 'type/num/num', b : 'type/num/num']: (('const/arithmetic/+' ('const/arithmetic/*' a n) m1) = ('const/arithmetic/+' ('const/arithmetic/*' b n) m2)))))).
tt('thm/arithmetic/MODEQ_0_CONG_', ax, (![m2 : 'type/num/num', m1 : 'type/num/num']: (('const/arithmetic/MODEQ' 'const/num/0' m1 m2) = (m1 = m2)))).
tt('thm/arithmetic/MODEQ_NONZERO_MODEQUALITY_', ax, (![n : 'type/num/num', m2 : 'type/num/num', m1 : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' n) => (('const/arithmetic/MODEQ' n m1 m2) = (('const/arithmetic/MOD' m1 n) = ('const/arithmetic/MOD' m2 n)))))).
tt('thm/arithmetic/MODEQ_THM_', ax, (![n : 'type/num/num', m2 : 'type/num/num', m1 : 'type/num/num']: (('const/arithmetic/MODEQ' n m1 m2) = (((n = 'const/num/0') & (m1 = m2)) | (('const/prim_rec/<' 'const/num/0' n) & (('const/arithmetic/MOD' m1 n) = ('const/arithmetic/MOD' m2 n))))))).
tt('thm/arithmetic/MODEQ_INTRO_CONG_', ax, (![n : 'type/num/num', e1 : 'type/num/num', e0 : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' n) => (('const/arithmetic/MODEQ' n e0 e1) => (('const/arithmetic/MOD' e0 n) = ('const/arithmetic/MOD' e1 n)))))).
tt('thm/arithmetic/MODEQ_PLUS_CONG_', ax, (![y1 : 'type/num/num', y0 : 'type/num/num', x1 : 'type/num/num', x0 : 'type/num/num', n : 'type/num/num']: (('const/arithmetic/MODEQ' n x0 x1) => (('const/arithmetic/MODEQ' n y0 y1) => ('const/arithmetic/MODEQ' n ('const/arithmetic/+' x0 y0) ('const/arithmetic/+' x1 y1)))))).
tt('thm/arithmetic/MODEQ_MULT_CONG_', ax, (![y1 : 'type/num/num', y0 : 'type/num/num', x1 : 'type/num/num', x0 : 'type/num/num', n : 'type/num/num']: (('const/arithmetic/MODEQ' n x0 x1) => (('const/arithmetic/MODEQ' n y0 y1) => ('const/arithmetic/MODEQ' n ('const/arithmetic/*' x0 y0) ('const/arithmetic/*' x1 y1)))))).
tt('thm/arithmetic/MODEQ_REFL_', ax, (![n : 'type/num/num', x : 'type/num/num']: ('const/arithmetic/MODEQ' n x x))).
tt('thm/arithmetic/MODEQ_SYM_', ax, (![y : 'type/num/num', x : 'type/num/num', n : 'type/num/num']: (('const/arithmetic/MODEQ' n x y) = ('const/arithmetic/MODEQ' n y x)))).
tt('thm/arithmetic/MODEQ_TRANS_', ax, (![n : 'type/num/num', x : 'type/num/num', y : 'type/num/num', z : 'type/num/num']: ((('const/arithmetic/MODEQ' n x y) & ('const/arithmetic/MODEQ' n y z)) => ('const/arithmetic/MODEQ' n x z)))).
tt('thm/arithmetic/MODEQ_NUMERAL_0', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/arithmetic/<=' ('const/arithmetic/NUMERAL' n) ('const/arithmetic/NUMERAL' m)) => ('const/arithmetic/MODEQ' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' m)) ('const/arithmetic/MOD' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' m)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))))))).
tt('thm/arithmetic/MODEQ_NUMERAL_1', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/arithmetic/<=' ('const/arithmetic/NUMERAL' n) ('const/arithmetic/NUMERAL' m)) => ('const/arithmetic/MODEQ' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' m)) ('const/arithmetic/MOD' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' m)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))))))).
tt('thm/arithmetic/MODEQ_NUMERAL_2', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/arithmetic/<=' ('const/arithmetic/NUMERAL' n) ('const/arithmetic/NUMERAL' m)) => ('const/arithmetic/MODEQ' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' m)) ('const/arithmetic/MOD' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' m)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n))))))).
tt('thm/arithmetic/MODEQ_NUMERAL_e3', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/prim_rec/<' ('const/arithmetic/NUMERAL' n) ('const/arithmetic/NUMERAL' m)) => ('const/arithmetic/MODEQ' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' m)) ('const/arithmetic/MOD' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' m)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n))))))).
tt('thm/arithmetic/MODEQ_MOD_', ax, (![x : 'type/num/num', n : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' n) => ('const/arithmetic/MODEQ' n ('const/arithmetic/MOD' x n) x)))).
tt('thm/arithmetic/MODEQ_0_', ax, (![n : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' n) => ('const/arithmetic/MODEQ' n n 'const/num/0')))).
tt('thm/arithmetic/datatype_num_', ax, ![A : $t]: (![num : ('type/num/num' > (('type/num/num' > 'type/num/num') > A))]: (('const/bool/DATATYPE' A) (num 'const/num/0' 'const/num/SUC')))).
