tt('const/transc/Dint', ty, (('type/pair/prod' 'type/realax/real' 'type/realax/real') > (('type/realax/real' > 'type/realax/real') > ('type/realax/real' > $o)))).
tt('const/transc/acs', ty, ('type/realax/real' > 'type/realax/real')).
tt('const/transc/asn', ty, ('type/realax/real' > 'type/realax/real')).
tt('const/transc/atn', ty, ('type/realax/real' > 'type/realax/real')).
tt('const/transc/cos', ty, ('type/realax/real' > 'type/realax/real')).
tt('const/transc/division', ty, (('type/pair/prod' 'type/realax/real' 'type/realax/real') > (('type/num/num' > 'type/realax/real') > $o))).
tt('const/transc/dsize', ty, (('type/num/num' > 'type/realax/real') > 'type/num/num')).
tt('const/transc/exp', ty, ('type/realax/real' > 'type/realax/real')).
tt('const/transc/fine', ty, (('type/realax/real' > 'type/realax/real') > (('type/pair/prod' ('type/num/num' > 'type/realax/real') ('type/num/num' > 'type/realax/real')) > $o))).
tt('const/transc/gauge', ty, (('type/realax/real' > $o) > (('type/realax/real' > 'type/realax/real') > $o))).
tt('const/transc/ln', ty, ('type/realax/real' > 'type/realax/real')).
tt('const/transc/pi', ty, 'type/realax/real').
tt('const/transc/root', ty, ('type/num/num' > ('type/realax/real' > 'type/realax/real'))).
tt('const/transc/rpow', ty, ('type/realax/real' > ('type/realax/real' > 'type/realax/real'))).
tt('const/transc/rsum', ty, (('type/pair/prod' ('type/num/num' > 'type/realax/real') ('type/num/num' > 'type/realax/real')) > (('type/realax/real' > 'type/realax/real') > 'type/realax/real'))).
tt('const/transc/sin', ty, ('type/realax/real' > 'type/realax/real')).
tt('const/transc/sqrt', ty, ('type/realax/real' > 'type/realax/real')).
tt('const/transc/tan', ty, ('type/realax/real' > 'type/realax/real')).
tt('const/transc/tdiv', ty, (('type/pair/prod' 'type/realax/real' 'type/realax/real') > (('type/pair/prod' ('type/num/num' > 'type/realax/real') ('type/num/num' > 'type/realax/real')) > $o))).
tt('thm/transc/exp_', def, (![x : 'type/realax/real']: (('const/transc/exp' x) = ('const/seq/suminf' (^[n : 'type/num/num']: ('const/realax/real_mul' ((^[n0 : 'type/num/num']: ('const/realax/inv' ('const/real/real_of_num' ('const/arithmetic/FACT' n0)))) n) ('const/real/pow' x n))))))).
tt('thm/transc/cos_', def, (![x : 'type/realax/real']: (('const/transc/cos' x) = ('const/seq/suminf' (^[n : 'type/num/num']: ('const/realax/real_mul' ((^[n0 : 'type/num/num']: (('const/bool/COND' 'type/realax/real') ('const/arithmetic/EVEN' n0) ('const/real/#slash#' ('const/real/pow' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) ('const/arithmetic/DIV' n0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) ('const/real/real_of_num' ('const/arithmetic/FACT' n0))) ('const/real/real_of_num' 'const/num/0'))) n) ('const/real/pow' x n))))))).
tt('thm/transc/sin_', def, (![x : 'type/realax/real']: (('const/transc/sin' x) = ('const/seq/suminf' (^[n : 'type/num/num']: ('const/realax/real_mul' ((^[n0 : 'type/num/num']: (('const/bool/COND' 'type/realax/real') ('const/arithmetic/EVEN' n0) ('const/real/real_of_num' 'const/num/0') ('const/real/#slash#' ('const/real/pow' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) ('const/arithmetic/DIV' ('const/arithmetic/-' n0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) ('const/real/real_of_num' ('const/arithmetic/FACT' n0))))) n) ('const/real/pow' x n))))))).
tt('thm/transc/EXP_CONVERGES_', ax, (![x : 'type/realax/real']: ('const/seq/sums' (^[n : 'type/num/num']: ('const/realax/real_mul' ((^[n0 : 'type/num/num']: ('const/realax/inv' ('const/real/real_of_num' ('const/arithmetic/FACT' n0)))) n) ('const/real/pow' x n))) ('const/transc/exp' x)))).
tt('thm/transc/SIN_CONVERGES_', ax, (![x : 'type/realax/real']: ('const/seq/sums' (^[n : 'type/num/num']: ('const/realax/real_mul' ((^[n0 : 'type/num/num']: (('const/bool/COND' 'type/realax/real') ('const/arithmetic/EVEN' n0) ('const/real/real_of_num' 'const/num/0') ('const/real/#slash#' ('const/real/pow' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) ('const/arithmetic/DIV' ('const/arithmetic/-' n0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) ('const/real/real_of_num' ('const/arithmetic/FACT' n0))))) n) ('const/real/pow' x n))) ('const/transc/sin' x)))).
tt('thm/transc/COS_CONVERGES_', ax, (![x : 'type/realax/real']: ('const/seq/sums' (^[n : 'type/num/num']: ('const/realax/real_mul' ((^[n0 : 'type/num/num']: (('const/bool/COND' 'type/realax/real') ('const/arithmetic/EVEN' n0) ('const/real/#slash#' ('const/real/pow' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) ('const/arithmetic/DIV' n0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) ('const/real/real_of_num' ('const/arithmetic/FACT' n0))) ('const/real/real_of_num' 'const/num/0'))) n) ('const/real/pow' x n))) ('const/transc/cos' x)))).
tt('thm/transc/EXP_FDIFF_', ax, (('const/powser/diffs' (^[n : 'type/num/num']: ('const/realax/inv' ('const/real/real_of_num' ('const/arithmetic/FACT' n))))) = (^[n : 'type/num/num']: ('const/realax/inv' ('const/real/real_of_num' ('const/arithmetic/FACT' n)))))).
tt('thm/transc/SIN_FDIFF_', ax, (('const/powser/diffs' (^[n : 'type/num/num']: (('const/bool/COND' 'type/realax/real') ('const/arithmetic/EVEN' n) ('const/real/real_of_num' 'const/num/0') ('const/real/#slash#' ('const/real/pow' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) ('const/arithmetic/DIV' ('const/arithmetic/-' n ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) ('const/real/real_of_num' ('const/arithmetic/FACT' n)))))) = (^[n : 'type/num/num']: (('const/bool/COND' 'type/realax/real') ('const/arithmetic/EVEN' n) ('const/real/#slash#' ('const/real/pow' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) ('const/arithmetic/DIV' n ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) ('const/real/real_of_num' ('const/arithmetic/FACT' n))) ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/transc/COS_FDIFF_', ax, (('const/powser/diffs' (^[n : 'type/num/num']: (('const/bool/COND' 'type/realax/real') ('const/arithmetic/EVEN' n) ('const/real/#slash#' ('const/real/pow' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) ('const/arithmetic/DIV' n ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) ('const/real/real_of_num' ('const/arithmetic/FACT' n))) ('const/real/real_of_num' 'const/num/0')))) = (^[n : 'type/num/num']: ('const/realax/real_neg' ((^[n0 : 'type/num/num']: (('const/bool/COND' 'type/realax/real') ('const/arithmetic/EVEN' n0) ('const/real/real_of_num' 'const/num/0') ('const/real/#slash#' ('const/real/pow' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) ('const/arithmetic/DIV' ('const/arithmetic/-' n0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) ('const/real/real_of_num' ('const/arithmetic/FACT' n0))))) n))))).
tt('thm/transc/SIN_NEGLEMMA_', ax, (![x : 'type/realax/real']: (('const/realax/real_neg' ('const/transc/sin' x)) = ('const/seq/suminf' (^[n : 'type/num/num']: ('const/realax/real_neg' ('const/realax/real_mul' ((^[n0 : 'type/num/num']: (('const/bool/COND' 'type/realax/real') ('const/arithmetic/EVEN' n0) ('const/real/real_of_num' 'const/num/0') ('const/real/#slash#' ('const/real/pow' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) ('const/arithmetic/DIV' ('const/arithmetic/-' n0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) ('const/real/real_of_num' ('const/arithmetic/FACT' n0))))) n) ('const/real/pow' x n)))))))).
tt('thm/transc/DIFF_EXP_', ax, (![x : 'type/realax/real']: ('const/lim/diffl' 'const/transc/exp' ('const/transc/exp' x) x))).
tt('thm/transc/DIFF_SIN_', ax, (![x : 'type/realax/real']: ('const/lim/diffl' 'const/transc/sin' ('const/transc/cos' x) x))).
tt('thm/transc/DIFF_COS_', ax, (![x : 'type/realax/real']: ('const/lim/diffl' 'const/transc/cos' ('const/realax/real_neg' ('const/transc/sin' x)) x))).
tt('thm/transc/DIFF_COMPOSITE_0', ax, (![x : 'type/realax/real', l : 'type/realax/real', f : ('type/realax/real' > 'type/realax/real')]: ((('const/lim/diffl' f l x) & (~ ((f x) = ('const/real/real_of_num' 'const/num/0')))) => ('const/lim/diffl' (^[x0 : 'type/realax/real']: ('const/realax/inv' (f x0))) ('const/realax/real_neg' ('const/real/#slash#' l ('const/real/pow' (f x) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) x)))).
tt('thm/transc/DIFF_COMPOSITE_1', ax, (![x : 'type/realax/real', m : 'type/realax/real', l : 'type/realax/real', g : ('type/realax/real' > 'type/realax/real'), f : ('type/realax/real' > 'type/realax/real')]: ((('const/lim/diffl' f l x) & (('const/lim/diffl' g m x) & (~ ((g x) = ('const/real/real_of_num' 'const/num/0'))))) => ('const/lim/diffl' (^[x0 : 'type/realax/real']: ('const/real/#slash#' (f x0) (g x0))) ('const/real/#slash#' ('const/real/real_sub' ('const/realax/real_mul' l (g x)) ('const/realax/real_mul' m (f x))) ('const/real/pow' (g x) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) x)))).
tt('thm/transc/DIFF_COMPOSITE_2', ax, (![x : 'type/realax/real', m : 'type/realax/real', l : 'type/realax/real', g : ('type/realax/real' > 'type/realax/real'), f : ('type/realax/real' > 'type/realax/real')]: ((('const/lim/diffl' f l x) & ('const/lim/diffl' g m x)) => ('const/lim/diffl' (^[x0 : 'type/realax/real']: ('const/realax/real_add' (f x0) (g x0))) ('const/realax/real_add' l m) x)))).
tt('thm/transc/DIFF_COMPOSITE_3', ax, (![x : 'type/realax/real', m : 'type/realax/real', l : 'type/realax/real', g : ('type/realax/real' > 'type/realax/real'), f : ('type/realax/real' > 'type/realax/real')]: ((('const/lim/diffl' f l x) & ('const/lim/diffl' g m x)) => ('const/lim/diffl' (^[x0 : 'type/realax/real']: ('const/realax/real_mul' (f x0) (g x0))) ('const/realax/real_add' ('const/realax/real_mul' l (g x)) ('const/realax/real_mul' m (f x))) x)))).
tt('thm/transc/DIFF_COMPOSITE_4', ax, (![x : 'type/realax/real', m : 'type/realax/real', l : 'type/realax/real', g : ('type/realax/real' > 'type/realax/real'), f : ('type/realax/real' > 'type/realax/real')]: ((('const/lim/diffl' f l x) & ('const/lim/diffl' g m x)) => ('const/lim/diffl' (^[x0 : 'type/realax/real']: ('const/real/real_sub' (f x0) (g x0))) ('const/real/real_sub' l m) x)))).
tt('thm/transc/DIFF_COMPOSITE_5', ax, (![x : 'type/realax/real', l : 'type/realax/real', f : ('type/realax/real' > 'type/realax/real')]: (('const/lim/diffl' f l x) => ('const/lim/diffl' (^[x0 : 'type/realax/real']: ('const/realax/real_neg' (f x0))) ('const/realax/real_neg' l) x)))).
tt('thm/transc/DIFF_COMPOSITE_6', ax, (![x : 'type/realax/real', n : 'type/num/num', m : 'type/realax/real', g : ('type/realax/real' > 'type/realax/real')]: (('const/lim/diffl' g m x) => ('const/lim/diffl' (^[x0 : 'type/realax/real']: ('const/real/pow' (g x0) n)) ('const/realax/real_mul' ('const/realax/real_mul' ('const/real/real_of_num' n) ('const/real/pow' (g x) ('const/arithmetic/-' n ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) m) x)))).
tt('thm/transc/DIFF_COMPOSITE_7', ax, (![x : 'type/realax/real', m : 'type/realax/real', g : ('type/realax/real' > 'type/realax/real')]: (('const/lim/diffl' g m x) => ('const/lim/diffl' (^[x0 : 'type/realax/real']: ('const/transc/exp' (g x0))) ('const/realax/real_mul' ('const/transc/exp' (g x)) m) x)))).
tt('thm/transc/DIFF_COMPOSITE_8', ax, (![x : 'type/realax/real', m : 'type/realax/real', g : ('type/realax/real' > 'type/realax/real')]: (('const/lim/diffl' g m x) => ('const/lim/diffl' (^[x0 : 'type/realax/real']: ('const/transc/sin' (g x0))) ('const/realax/real_mul' ('const/transc/cos' (g x)) m) x)))).
tt('thm/transc/DIFF_COMPOSITE_e9', ax, (![x : 'type/realax/real', m : 'type/realax/real', g : ('type/realax/real' > 'type/realax/real')]: (('const/lim/diffl' g m x) => ('const/lim/diffl' (^[x0 : 'type/realax/real']: ('const/transc/cos' (g x0))) ('const/realax/real_mul' ('const/realax/real_neg' ('const/transc/sin' (g x))) m) x)))).
tt('thm/transc/EXP_0_', ax, (('const/transc/exp' ('const/real/real_of_num' 'const/num/0')) = ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/transc/EXP_LE_X_', ax, (![x : 'type/realax/real']: (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) => ('const/real/real_lte' ('const/realax/real_add' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) x) ('const/transc/exp' x))))).
tt('thm/transc/EXP_LT_1_', ax, (![x : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) => ('const/realax/real_lt' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/transc/exp' x))))).
tt('thm/transc/EXP_ADD_MUL_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/realax/real_mul' ('const/transc/exp' ('const/realax/real_add' x y)) ('const/transc/exp' ('const/realax/real_neg' x))) = ('const/transc/exp' y)))).
tt('thm/transc/EXP_NEG_MUL_', ax, (![x : 'type/realax/real']: (('const/realax/real_mul' ('const/transc/exp' x) ('const/transc/exp' ('const/realax/real_neg' x))) = ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
tt('thm/transc/EXP_NEG_MUL2_', ax, (![x : 'type/realax/real']: (('const/realax/real_mul' ('const/transc/exp' ('const/realax/real_neg' x)) ('const/transc/exp' x)) = ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
tt('thm/transc/EXP_NEG_', ax, (![x : 'type/realax/real']: (('const/transc/exp' ('const/realax/real_neg' x)) = ('const/realax/inv' ('const/transc/exp' x))))).
tt('thm/transc/EXP_ADD_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/transc/exp' ('const/realax/real_add' x y)) = ('const/realax/real_mul' ('const/transc/exp' x) ('const/transc/exp' y))))).
tt('thm/transc/EXP_POS_LE_', ax, (![x : 'type/realax/real']: ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') ('const/transc/exp' x)))).
tt('thm/transc/EXP_NZ_', ax, (![x : 'type/realax/real']: (~ (('const/transc/exp' x) = ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/transc/EXP_POS_LT_', ax, (![x : 'type/realax/real']: ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/transc/exp' x)))).
tt('thm/transc/EXP_N_', ax, (![n : 'type/num/num', x : 'type/realax/real']: (('const/transc/exp' ('const/realax/real_mul' ('const/real/real_of_num' n) x)) = ('const/real/pow' ('const/transc/exp' x) n)))).
tt('thm/transc/EXP_SUB_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/transc/exp' ('const/real/real_sub' x y)) = ('const/real/#slash#' ('const/transc/exp' x) ('const/transc/exp' y))))).
tt('thm/transc/EXP_MONO_IMP_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/realax/real_lt' x y) => ('const/realax/real_lt' ('const/transc/exp' x) ('const/transc/exp' y))))).
tt('thm/transc/EXP_MONO_LT_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/realax/real_lt' ('const/transc/exp' x) ('const/transc/exp' y)) = ('const/realax/real_lt' x y)))).
tt('thm/transc/EXP_MONO_LE_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/real/real_lte' ('const/transc/exp' x) ('const/transc/exp' y)) = ('const/real/real_lte' x y)))).
tt('thm/transc/EXP_INJ_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((('const/transc/exp' x) = ('const/transc/exp' y)) = (x = y)))).
tt('thm/transc/EXP_TOTAL_LEMMA_', ax, (![y : 'type/realax/real']: (('const/real/real_lte' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) y) => (?[x : 'type/realax/real']: (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) & (('const/real/real_lte' x ('const/real/real_sub' y ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) & (('const/transc/exp' x) = y))))))).
tt('thm/transc/EXP_TOTAL_', ax, (![y : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') y) => (?[x : 'type/realax/real']: (('const/transc/exp' x) = y))))).
tt('thm/transc/ln_', def, (![x : 'type/realax/real']: (('const/transc/ln' x) = (('const/min/@' 'type/realax/real') (^[u : 'type/realax/real']: (('const/transc/exp' u) = x)))))).
tt('thm/transc/LN_EXP_', ax, (![x : 'type/realax/real']: (('const/transc/ln' ('const/transc/exp' x)) = x))).
tt('thm/transc/EXP_LN_', ax, (![x : 'type/realax/real']: ((('const/transc/exp' ('const/transc/ln' x)) = x) = ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x)))).
tt('thm/transc/LN_MUL_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) & ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') y)) => (('const/transc/ln' ('const/realax/real_mul' x y)) = ('const/realax/real_add' ('const/transc/ln' x) ('const/transc/ln' y)))))).
tt('thm/transc/LN_INJ_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) & ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') y)) => ((('const/transc/ln' x) = ('const/transc/ln' y)) = (x = y))))).
tt('thm/transc/LN_1_', ax, (('const/transc/ln' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = ('const/real/real_of_num' 'const/num/0'))).
tt('thm/transc/LN_INV_', ax, (![x : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) => (('const/transc/ln' ('const/realax/inv' x)) = ('const/realax/real_neg' ('const/transc/ln' x)))))).
tt('thm/transc/LN_DIV_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) & ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') y)) => (('const/transc/ln' ('const/real/#slash#' x y)) = ('const/real/real_sub' ('const/transc/ln' x) ('const/transc/ln' y)))))).
tt('thm/transc/LN_MONO_LT_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) & ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') y)) => (('const/realax/real_lt' ('const/transc/ln' x) ('const/transc/ln' y)) = ('const/realax/real_lt' x y))))).
tt('thm/transc/LN_MONO_LE_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) & ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') y)) => (('const/real/real_lte' ('const/transc/ln' x) ('const/transc/ln' y)) = ('const/real/real_lte' x y))))).
tt('thm/transc/LN_POW_', ax, (![n : 'type/num/num', x : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) => (('const/transc/ln' ('const/real/pow' x n)) = ('const/realax/real_mul' ('const/real/real_of_num' n) ('const/transc/ln' x)))))).
tt('thm/transc/LN_LE_', ax, (![x : 'type/realax/real']: (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) => ('const/real/real_lte' ('const/transc/ln' ('const/realax/real_add' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) x)) x)))).
tt('thm/transc/LN_LT_X_', ax, (![x : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) => ('const/realax/real_lt' ('const/transc/ln' x) x)))).
tt('thm/transc/LN_POS_', ax, (![x : 'type/realax/real']: (('const/real/real_lte' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) x) => ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') ('const/transc/ln' x))))).
tt('thm/transc/root_', def, (![n : 'type/num/num', x : 'type/realax/real']: (('const/transc/root' n x) = (('const/min/@' 'type/realax/real') (^[u : 'type/realax/real']: ((('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) => ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') u)) & (('const/real/pow' u n) = x))))))).
tt('thm/transc/sqrt_', def, (![x : 'type/realax/real']: (('const/transc/sqrt' x) = ('const/transc/root' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) x)))).
tt('thm/transc/ROOT_LT_LEMMA_', ax, (![n : 'type/num/num', x : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) => (('const/real/pow' ('const/transc/exp' ('const/real/#slash#' ('const/transc/ln' x) ('const/real/real_of_num' ('const/num/SUC' n)))) ('const/num/SUC' n)) = x)))).
tt('thm/transc/ROOT_LN_', ax, (![n : 'type/num/num', x : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) => (('const/transc/root' ('const/num/SUC' n) x) = ('const/transc/exp' ('const/real/#slash#' ('const/transc/ln' x) ('const/real/real_of_num' ('const/num/SUC' n)))))))).
tt('thm/transc/ROOT_0_', ax, (![n : 'type/num/num']: (('const/transc/root' ('const/num/SUC' n) ('const/real/real_of_num' 'const/num/0')) = ('const/real/real_of_num' 'const/num/0')))).
tt('thm/transc/ROOT_1_', ax, (![n : 'type/num/num']: (('const/transc/root' ('const/num/SUC' n) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
tt('thm/transc/ROOT_POS_LT_', ax, (![n : 'type/num/num', x : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) => ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/transc/root' ('const/num/SUC' n) x))))).
tt('thm/transc/ROOT_POW_POS_', ax, (![n : 'type/num/num', x : 'type/realax/real']: (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) => (('const/real/pow' ('const/transc/root' ('const/num/SUC' n) x) ('const/num/SUC' n)) = x)))).
tt('thm/transc/POW_ROOT_POS_', ax, (![n : 'type/num/num', x : 'type/realax/real']: (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) => (('const/transc/root' ('const/num/SUC' n) ('const/real/pow' x ('const/num/SUC' n))) = x)))).
tt('thm/transc/ROOT_POS_', ax, (![n : 'type/num/num', x : 'type/realax/real']: (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) => ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') ('const/transc/root' ('const/num/SUC' n) x))))).
tt('thm/transc/ROOT_POS_UNIQ_', ax, (![n : 'type/num/num', x : 'type/realax/real', y : 'type/realax/real']: ((('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) & (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') y) & (('const/real/pow' y ('const/num/SUC' n)) = x))) => (('const/transc/root' ('const/num/SUC' n) x) = y)))).
tt('thm/transc/ROOT_MUL_', ax, (![n : 'type/num/num', x : 'type/realax/real', y : 'type/realax/real']: ((('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) & ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') y)) => (('const/transc/root' ('const/num/SUC' n) ('const/realax/real_mul' x y)) = ('const/realax/real_mul' ('const/transc/root' ('const/num/SUC' n) x) ('const/transc/root' ('const/num/SUC' n) y)))))).
tt('thm/transc/ROOT_INV_', ax, (![n : 'type/num/num', x : 'type/realax/real']: (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) => (('const/transc/root' ('const/num/SUC' n) ('const/realax/inv' x)) = ('const/realax/inv' ('const/transc/root' ('const/num/SUC' n) x)))))).
tt('thm/transc/ROOT_DIV_', ax, (![n : 'type/num/num', x : 'type/realax/real', y : 'type/realax/real']: ((('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) & ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') y)) => (('const/transc/root' ('const/num/SUC' n) ('const/real/#slash#' x y)) = ('const/real/#slash#' ('const/transc/root' ('const/num/SUC' n) x) ('const/transc/root' ('const/num/SUC' n) y)))))).
tt('thm/transc/ROOT_MONO_LE_', ax, (![n : 'type/num/num', x : 'type/realax/real', y : 'type/realax/real']: ((('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) & ('const/real/real_lte' x y)) => ('const/real/real_lte' ('const/transc/root' ('const/num/SUC' n) x) ('const/transc/root' ('const/num/SUC' n) y))))).
tt('thm/transc/SQRT_0_', ax, (('const/transc/sqrt' ('const/real/real_of_num' 'const/num/0')) = ('const/real/real_of_num' 'const/num/0'))).
tt('thm/transc/SQRT_1_', ax, (('const/transc/sqrt' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/transc/SQRT_POS_LT_', ax, (![x : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) => ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/transc/sqrt' x))))).
tt('thm/transc/SQRT_POS_LE_', ax, (![x : 'type/realax/real']: (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) => ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') ('const/transc/sqrt' x))))).
tt('thm/transc/SQRT_POW2_', ax, (![x : 'type/realax/real']: ((('const/real/pow' ('const/transc/sqrt' x) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) = x) = ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x)))).
tt('thm/transc/SQRT_POW_2_', ax, (![x : 'type/realax/real']: (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) => (('const/real/pow' ('const/transc/sqrt' x) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) = x)))).
tt('thm/transc/POW_2_SQRT_', ax, (![x : 'type/realax/real']: (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) => (('const/transc/sqrt' ('const/real/pow' x ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) = x)))).
tt('thm/transc/SQRT_POS_UNIQ_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) & (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') y) & (('const/real/pow' y ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) = x))) => (('const/transc/sqrt' x) = y)))).
tt('thm/transc/SQRT_MUL_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) & ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') y)) => (('const/transc/sqrt' ('const/realax/real_mul' x y)) = ('const/realax/real_mul' ('const/transc/sqrt' x) ('const/transc/sqrt' y)))))).
tt('thm/transc/SQRT_INV_', ax, (![x : 'type/realax/real']: (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) => (('const/transc/sqrt' ('const/realax/inv' x)) = ('const/realax/inv' ('const/transc/sqrt' x)))))).
tt('thm/transc/SQRT_DIV_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) & ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') y)) => (('const/transc/sqrt' ('const/real/#slash#' x y)) = ('const/real/#slash#' ('const/transc/sqrt' x) ('const/transc/sqrt' y)))))).
tt('thm/transc/SQRT_MONO_LE_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) & ('const/real/real_lte' x y)) => ('const/real/real_lte' ('const/transc/sqrt' x) ('const/transc/sqrt' y))))).
tt('thm/transc/SQRT_EVEN_POW2_', ax, (![n : 'type/num/num']: (('const/arithmetic/EVEN' n) => (('const/transc/sqrt' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) n)) = ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/DIV' n ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))))).
tt('thm/transc/REAL_DIV_SQRT_', ax, (![x : 'type/realax/real']: (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) => (('const/real/#slash#' x ('const/transc/sqrt' x)) = ('const/transc/sqrt' x))))).
tt('thm/transc/SQRT_EQ_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (((('const/real/pow' x ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) = y) & ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x)) => (x = ('const/transc/sqrt' y))))).
tt('thm/transc/SIN_0_', ax, (('const/transc/sin' ('const/real/real_of_num' 'const/num/0')) = ('const/real/real_of_num' 'const/num/0'))).
tt('thm/transc/COS_0_', ax, (('const/transc/cos' ('const/real/real_of_num' 'const/num/0')) = ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/transc/SIN_CIRCLE_', ax, (![x : 'type/realax/real']: (('const/realax/real_add' ('const/real/pow' ('const/transc/sin' x) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/real/pow' ('const/transc/cos' x) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) = ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
tt('thm/transc/SIN_BOUND_', ax, (![x : 'type/realax/real']: ('const/real/real_lte' ('const/real/abs' ('const/transc/sin' x)) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
tt('thm/transc/SIN_BOUNDS_0', ax, (![x : 'type/realax/real']: ('const/real/real_lte' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) ('const/transc/sin' x)))).
tt('thm/transc/SIN_BOUNDS_e1', ax, (![x : 'type/realax/real']: ('const/real/real_lte' ('const/transc/sin' x) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
tt('thm/transc/COS_BOUND_', ax, (![x : 'type/realax/real']: ('const/real/real_lte' ('const/real/abs' ('const/transc/cos' x)) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
tt('thm/transc/COS_BOUNDS_0', ax, (![x : 'type/realax/real']: ('const/real/real_lte' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) ('const/transc/cos' x)))).
tt('thm/transc/COS_BOUNDS_e1', ax, (![x : 'type/realax/real']: ('const/real/real_lte' ('const/transc/cos' x) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
tt('thm/transc/SIN_COS_ADD_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/realax/real_add' ('const/real/pow' ('const/real/real_sub' ('const/transc/sin' ('const/realax/real_add' x y)) ('const/realax/real_add' ('const/realax/real_mul' ('const/transc/sin' x) ('const/transc/cos' y)) ('const/realax/real_mul' ('const/transc/cos' x) ('const/transc/sin' y)))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/real/pow' ('const/real/real_sub' ('const/transc/cos' ('const/realax/real_add' x y)) ('const/real/real_sub' ('const/realax/real_mul' ('const/transc/cos' x) ('const/transc/cos' y)) ('const/realax/real_mul' ('const/transc/sin' x) ('const/transc/sin' y)))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) = ('const/real/real_of_num' 'const/num/0')))).
tt('thm/transc/SIN_COS_NEG_', ax, (![x : 'type/realax/real']: (('const/realax/real_add' ('const/real/pow' ('const/realax/real_add' ('const/transc/sin' ('const/realax/real_neg' x)) ('const/transc/sin' x)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/real/pow' ('const/real/real_sub' ('const/transc/cos' ('const/realax/real_neg' x)) ('const/transc/cos' x)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) = ('const/real/real_of_num' 'const/num/0')))).
tt('thm/transc/SIN_ADD_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/transc/sin' ('const/realax/real_add' x y)) = ('const/realax/real_add' ('const/realax/real_mul' ('const/transc/sin' x) ('const/transc/cos' y)) ('const/realax/real_mul' ('const/transc/cos' x) ('const/transc/sin' y)))))).
tt('thm/transc/COS_ADD_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/transc/cos' ('const/realax/real_add' x y)) = ('const/real/real_sub' ('const/realax/real_mul' ('const/transc/cos' x) ('const/transc/cos' y)) ('const/realax/real_mul' ('const/transc/sin' x) ('const/transc/sin' y)))))).
tt('thm/transc/SIN_NEG_', ax, (![x : 'type/realax/real']: (('const/transc/sin' ('const/realax/real_neg' x)) = ('const/realax/real_neg' ('const/transc/sin' x))))).
tt('thm/transc/COS_NEG_', ax, (![x : 'type/realax/real']: (('const/transc/cos' ('const/realax/real_neg' x)) = ('const/transc/cos' x)))).
tt('thm/transc/SIN_DOUBLE_', ax, (![x : 'type/realax/real']: (('const/transc/sin' ('const/realax/real_mul' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) x)) = ('const/realax/real_mul' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/realax/real_mul' ('const/transc/sin' x) ('const/transc/cos' x)))))).
tt('thm/transc/COS_DOUBLE_', ax, (![x : 'type/realax/real']: (('const/transc/cos' ('const/realax/real_mul' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) x)) = ('const/real/real_sub' ('const/real/pow' ('const/transc/cos' x) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/real/pow' ('const/transc/sin' x) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))).
tt('thm/transc/SIN_PAIRED_', ax, (![x : 'type/realax/real']: ('const/seq/sums' (^[n : 'type/num/num']: ('const/realax/real_mul' ('const/real/#slash#' ('const/real/pow' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) n) ('const/real/real_of_num' ('const/arithmetic/FACT' ('const/arithmetic/+' ('const/arithmetic/*' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) n) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))) ('const/real/pow' x ('const/arithmetic/+' ('const/arithmetic/*' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) n) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))) ('const/transc/sin' x)))).
tt('thm/transc/SIN_POS_', ax, (![x : 'type/realax/real']: ((('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) & ('const/realax/real_lt' x ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) => ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/transc/sin' x))))).
tt('thm/transc/COS_PAIRED_', ax, (![x : 'type/realax/real']: ('const/seq/sums' (^[n : 'type/num/num']: ('const/realax/real_mul' ('const/real/#slash#' ('const/real/pow' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) n) ('const/real/real_of_num' ('const/arithmetic/FACT' ('const/arithmetic/*' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) n)))) ('const/real/pow' x ('const/arithmetic/*' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) n)))) ('const/transc/cos' x)))).
tt('thm/transc/COS_2_', ax, ('const/realax/real_lt' ('const/transc/cos' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) ('const/real/real_of_num' 'const/num/0'))).
tt('thm/transc/COS_ISZERO_', ax, (('const/bool/?!' 'type/realax/real') (^[x : 'type/realax/real']: (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) & (('const/real/real_lte' x ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) & (('const/transc/cos' x) = ('const/real/real_of_num' 'const/num/0'))))))).
tt('thm/transc/pi_', def, ('const/transc/pi' = ('const/realax/real_mul' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) (('const/min/@' 'type/realax/real') (^[x : 'type/realax/real']: (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) & (('const/real/real_lte' x ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) & (('const/transc/cos' x) = ('const/real/real_of_num' 'const/num/0'))))))))).
tt('thm/transc/PI2_', ax, (('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) = (('const/min/@' 'type/realax/real') (^[x : 'type/realax/real']: (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) & (('const/real/real_lte' x ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) & (('const/transc/cos' x) = ('const/real/real_of_num' 'const/num/0')))))))).
tt('thm/transc/COS_PI2_', ax, (('const/transc/cos' ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) = ('const/real/real_of_num' 'const/num/0'))).
tt('thm/transc/PI2_BOUNDS_0', ax, ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))).
tt('thm/transc/PI2_BOUNDS_e1', ax, ('const/realax/real_lt' ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))).
tt('thm/transc/PI_POS_', ax, ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') 'const/transc/pi')).
tt('thm/transc/SIN_PI2_', ax, (('const/transc/sin' ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) = ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/transc/COS_PI_', ax, (('const/transc/cos' 'const/transc/pi') = ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
tt('thm/transc/SIN_PI_', ax, (('const/transc/sin' 'const/transc/pi') = ('const/real/real_of_num' 'const/num/0'))).
tt('thm/transc/SIN_COS_', ax, (![x : 'type/realax/real']: (('const/transc/sin' x) = ('const/transc/cos' ('const/real/real_sub' ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) x))))).
tt('thm/transc/COS_SIN_', ax, (![x : 'type/realax/real']: (('const/transc/cos' x) = ('const/transc/sin' ('const/real/real_sub' ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) x))))).
tt('thm/transc/SIN_PERIODIC_PI_', ax, (![x : 'type/realax/real']: (('const/transc/sin' ('const/realax/real_add' x 'const/transc/pi')) = ('const/realax/real_neg' ('const/transc/sin' x))))).
tt('thm/transc/COS_PERIODIC_PI_', ax, (![x : 'type/realax/real']: (('const/transc/cos' ('const/realax/real_add' x 'const/transc/pi')) = ('const/realax/real_neg' ('const/transc/cos' x))))).
tt('thm/transc/SIN_PERIODIC_', ax, (![x : 'type/realax/real']: (('const/transc/sin' ('const/realax/real_add' x ('const/realax/real_mul' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) 'const/transc/pi'))) = ('const/transc/sin' x)))).
tt('thm/transc/COS_PERIODIC_', ax, (![x : 'type/realax/real']: (('const/transc/cos' ('const/realax/real_add' x ('const/realax/real_mul' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) 'const/transc/pi'))) = ('const/transc/cos' x)))).
tt('thm/transc/COS_NPI_', ax, (![n : 'type/num/num']: (('const/transc/cos' ('const/realax/real_mul' ('const/real/real_of_num' n) 'const/transc/pi')) = ('const/real/pow' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) n)))).
tt('thm/transc/SIN_NPI_', ax, (![n : 'type/num/num']: (('const/transc/sin' ('const/realax/real_mul' ('const/real/real_of_num' n) 'const/transc/pi')) = ('const/real/real_of_num' 'const/num/0')))).
tt('thm/transc/SIN_POS_PI2_', ax, (![x : 'type/realax/real']: ((('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) & ('const/realax/real_lt' x ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))) => ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/transc/sin' x))))).
tt('thm/transc/COS_POS_PI2_', ax, (![x : 'type/realax/real']: ((('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) & ('const/realax/real_lt' x ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))) => ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/transc/cos' x))))).
tt('thm/transc/COS_POS_PI_', ax, (![x : 'type/realax/real']: ((('const/realax/real_lt' ('const/realax/real_neg' ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) x) & ('const/realax/real_lt' x ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))) => ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/transc/cos' x))))).
tt('thm/transc/SIN_POS_PI_', ax, (![x : 'type/realax/real']: ((('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) & ('const/realax/real_lt' x 'const/transc/pi')) => ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/transc/sin' x))))).
tt('thm/transc/COS_POS_PI2_LE_', ax, (![x : 'type/realax/real']: ((('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) & ('const/real/real_lte' x ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))) => ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') ('const/transc/cos' x))))).
tt('thm/transc/COS_POS_PI_LE_', ax, (![x : 'type/realax/real']: ((('const/real/real_lte' ('const/realax/real_neg' ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) x) & ('const/real/real_lte' x ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))) => ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') ('const/transc/cos' x))))).
tt('thm/transc/SIN_POS_PI2_LE_', ax, (![x : 'type/realax/real']: ((('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) & ('const/real/real_lte' x ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))) => ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') ('const/transc/sin' x))))).
tt('thm/transc/SIN_POS_PI_LE_', ax, (![x : 'type/realax/real']: ((('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) & ('const/real/real_lte' x 'const/transc/pi')) => ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') ('const/transc/sin' x))))).
tt('thm/transc/COS_TOTAL_', ax, (![y : 'type/realax/real']: ((('const/real/real_lte' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y) & ('const/real/real_lte' y ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) => (('const/bool/?!' 'type/realax/real') (^[x : 'type/realax/real']: (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) & (('const/real/real_lte' x 'const/transc/pi') & (('const/transc/cos' x) = y)))))))).
tt('thm/transc/SIN_TOTAL_', ax, (![y : 'type/realax/real']: ((('const/real/real_lte' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y) & ('const/real/real_lte' y ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) => (('const/bool/?!' 'type/realax/real') (^[x : 'type/realax/real']: (('const/real/real_lte' ('const/realax/real_neg' ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) x) & (('const/real/real_lte' x ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) & (('const/transc/sin' x) = y)))))))).
tt('thm/transc/COS_ZERO_LEMMA_', ax, (![x : 'type/realax/real']: ((('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) & (('const/transc/cos' x) = ('const/real/real_of_num' 'const/num/0'))) => (?[n : 'type/num/num']: ((~ ('const/arithmetic/EVEN' n)) & (x = ('const/realax/real_mul' ('const/real/real_of_num' n) ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))))).
tt('thm/transc/SIN_ZERO_LEMMA_', ax, (![x : 'type/realax/real']: ((('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) & (('const/transc/sin' x) = ('const/real/real_of_num' 'const/num/0'))) => (?[n : 'type/num/num']: (('const/arithmetic/EVEN' n) & (x = ('const/realax/real_mul' ('const/real/real_of_num' n) ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))))).
tt('thm/transc/COS_ZERO_', ax, (![x : 'type/realax/real']: ((('const/transc/cos' x) = ('const/real/real_of_num' 'const/num/0')) = ((?[n : 'type/num/num']: ((~ ('const/arithmetic/EVEN' n)) & (x = ('const/realax/real_mul' ('const/real/real_of_num' n) ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))))) | (?[n : 'type/num/num']: ((~ ('const/arithmetic/EVEN' n)) & (x = ('const/realax/real_neg' ('const/realax/real_mul' ('const/real/real_of_num' n) ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))))))).
tt('thm/transc/SIN_ZERO_', ax, (![x : 'type/realax/real']: ((('const/transc/sin' x) = ('const/real/real_of_num' 'const/num/0')) = ((?[n : 'type/num/num']: (('const/arithmetic/EVEN' n) & (x = ('const/realax/real_mul' ('const/real/real_of_num' n) ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))))) | (?[n : 'type/num/num']: (('const/arithmetic/EVEN' n) & (x = ('const/realax/real_neg' ('const/realax/real_mul' ('const/real/real_of_num' n) ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))))))).
tt('thm/transc/tan_', def, (![x : 'type/realax/real']: (('const/transc/tan' x) = ('const/real/#slash#' ('const/transc/sin' x) ('const/transc/cos' x))))).
tt('thm/transc/TAN_0_', ax, (('const/transc/tan' ('const/real/real_of_num' 'const/num/0')) = ('const/real/real_of_num' 'const/num/0'))).
tt('thm/transc/TAN_PI_', ax, (('const/transc/tan' 'const/transc/pi') = ('const/real/real_of_num' 'const/num/0'))).
tt('thm/transc/TAN_NPI_', ax, (![n : 'type/num/num']: (('const/transc/tan' ('const/realax/real_mul' ('const/real/real_of_num' n) 'const/transc/pi')) = ('const/real/real_of_num' 'const/num/0')))).
tt('thm/transc/TAN_NEG_', ax, (![x : 'type/realax/real']: (('const/transc/tan' ('const/realax/real_neg' x)) = ('const/realax/real_neg' ('const/transc/tan' x))))).
tt('thm/transc/TAN_PERIODIC_', ax, (![x : 'type/realax/real']: (('const/transc/tan' ('const/realax/real_add' x ('const/realax/real_mul' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) 'const/transc/pi'))) = ('const/transc/tan' x)))).
tt('thm/transc/TAN_ADD_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (((~ (('const/transc/cos' x) = ('const/real/real_of_num' 'const/num/0'))) & ((~ (('const/transc/cos' y) = ('const/real/real_of_num' 'const/num/0'))) & (~ (('const/transc/cos' ('const/realax/real_add' x y)) = ('const/real/real_of_num' 'const/num/0'))))) => (('const/transc/tan' ('const/realax/real_add' x y)) = ('const/real/#slash#' ('const/realax/real_add' ('const/transc/tan' x) ('const/transc/tan' y)) ('const/real/real_sub' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/realax/real_mul' ('const/transc/tan' x) ('const/transc/tan' y)))))))).
tt('thm/transc/TAN_DOUBLE_', ax, (![x : 'type/realax/real']: (((~ (('const/transc/cos' x) = ('const/real/real_of_num' 'const/num/0'))) & (~ (('const/transc/cos' ('const/realax/real_mul' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) x)) = ('const/real/real_of_num' 'const/num/0')))) => (('const/transc/tan' ('const/realax/real_mul' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) x)) = ('const/real/#slash#' ('const/realax/real_mul' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/transc/tan' x)) ('const/real/real_sub' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/real/pow' ('const/transc/tan' x) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))).
tt('thm/transc/TAN_POS_PI2_', ax, (![x : 'type/realax/real']: ((('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) & ('const/realax/real_lt' x ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))) => ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/transc/tan' x))))).
tt('thm/transc/DIFF_TAN_', ax, (![x : 'type/realax/real']: ((~ (('const/transc/cos' x) = ('const/real/real_of_num' 'const/num/0'))) => ('const/lim/diffl' 'const/transc/tan' ('const/realax/inv' ('const/real/pow' ('const/transc/cos' x) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) x)))).
tt('thm/transc/TAN_TOTAL_LEMMA_', ax, (![y : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') y) => (?[x : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) & (('const/realax/real_lt' x ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) & ('const/realax/real_lt' y ('const/transc/tan' x)))))))).
tt('thm/transc/TAN_TOTAL_POS_', ax, (![y : 'type/realax/real']: (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') y) => (?[x : 'type/realax/real']: (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) & (('const/realax/real_lt' x ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) & (('const/transc/tan' x) = y))))))).
tt('thm/transc/TAN_TOTAL_', ax, (![y : 'type/realax/real']: (('const/bool/?!' 'type/realax/real') (^[x : 'type/realax/real']: (('const/realax/real_lt' ('const/realax/real_neg' ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) x) & (('const/realax/real_lt' x ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) & (('const/transc/tan' x) = y))))))).
tt('thm/transc/asn_', def, (![y : 'type/realax/real']: (('const/transc/asn' y) = (('const/min/@' 'type/realax/real') (^[x : 'type/realax/real']: (('const/real/real_lte' ('const/realax/real_neg' ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) x) & (('const/real/real_lte' x ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) & (('const/transc/sin' x) = y)))))))).
tt('thm/transc/acs_', def, (![y : 'type/realax/real']: (('const/transc/acs' y) = (('const/min/@' 'type/realax/real') (^[x : 'type/realax/real']: (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) & (('const/real/real_lte' x 'const/transc/pi') & (('const/transc/cos' x) = y)))))))).
tt('thm/transc/atn_', def, (![y : 'type/realax/real']: (('const/transc/atn' y) = (('const/min/@' 'type/realax/real') (^[x : 'type/realax/real']: (('const/realax/real_lt' ('const/realax/real_neg' ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) x) & (('const/realax/real_lt' x ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) & (('const/transc/tan' x) = y)))))))).
tt('thm/transc/ASN_', ax, (![y : 'type/realax/real']: ((('const/real/real_lte' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y) & ('const/real/real_lte' y ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) => (('const/real/real_lte' ('const/realax/real_neg' ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) ('const/transc/asn' y)) & (('const/real/real_lte' ('const/transc/asn' y) ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) & (('const/transc/sin' ('const/transc/asn' y)) = y)))))).
tt('thm/transc/ASN_SIN_', ax, (![y : 'type/realax/real']: ((('const/real/real_lte' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y) & ('const/real/real_lte' y ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) => (('const/transc/sin' ('const/transc/asn' y)) = y)))).
tt('thm/transc/ASN_BOUNDS_', ax, (![y : 'type/realax/real']: ((('const/real/real_lte' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y) & ('const/real/real_lte' y ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) => (('const/real/real_lte' ('const/realax/real_neg' ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) ('const/transc/asn' y)) & ('const/real/real_lte' ('const/transc/asn' y) ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))).
tt('thm/transc/ASN_BOUNDS_LT_', ax, (![y : 'type/realax/real']: ((('const/realax/real_lt' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y) & ('const/realax/real_lt' y ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) => (('const/realax/real_lt' ('const/realax/real_neg' ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) ('const/transc/asn' y)) & ('const/realax/real_lt' ('const/transc/asn' y) ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))).
tt('thm/transc/SIN_ASN_', ax, (![x : 'type/realax/real']: ((('const/real/real_lte' ('const/realax/real_neg' ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) x) & ('const/real/real_lte' x ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))) => (('const/transc/asn' ('const/transc/sin' x)) = x)))).
tt('thm/transc/ACS_', ax, (![y : 'type/realax/real']: ((('const/real/real_lte' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y) & ('const/real/real_lte' y ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) => (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') ('const/transc/acs' y)) & (('const/real/real_lte' ('const/transc/acs' y) 'const/transc/pi') & (('const/transc/cos' ('const/transc/acs' y)) = y)))))).
tt('thm/transc/ACS_COS_', ax, (![y : 'type/realax/real']: ((('const/real/real_lte' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y) & ('const/real/real_lte' y ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) => (('const/transc/cos' ('const/transc/acs' y)) = y)))).
tt('thm/transc/ACS_BOUNDS_', ax, (![y : 'type/realax/real']: ((('const/real/real_lte' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y) & ('const/real/real_lte' y ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) => (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') ('const/transc/acs' y)) & ('const/real/real_lte' ('const/transc/acs' y) 'const/transc/pi'))))).
tt('thm/transc/ACS_BOUNDS_LT_', ax, (![y : 'type/realax/real']: ((('const/realax/real_lt' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y) & ('const/realax/real_lt' y ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) => (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/transc/acs' y)) & ('const/realax/real_lt' ('const/transc/acs' y) 'const/transc/pi'))))).
tt('thm/transc/COS_ACS_', ax, (![x : 'type/realax/real']: ((('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) & ('const/real/real_lte' x 'const/transc/pi')) => (('const/transc/acs' ('const/transc/cos' x)) = x)))).
tt('thm/transc/ATN_0', ax, (![y : 'type/realax/real']: ('const/realax/real_lt' ('const/realax/real_neg' ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) ('const/transc/atn' y)))).
tt('thm/transc/ATN_1', ax, (![y : 'type/realax/real']: ('const/realax/real_lt' ('const/transc/atn' y) ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))).
tt('thm/transc/ATN_e2', ax, (![y : 'type/realax/real']: (('const/transc/tan' ('const/transc/atn' y)) = y))).
tt('thm/transc/ATN_TAN_', ax, (![y : 'type/realax/real']: (('const/transc/tan' ('const/transc/atn' y)) = y))).
tt('thm/transc/ATN_BOUNDS_0', ax, (![y : 'type/realax/real']: ('const/realax/real_lt' ('const/realax/real_neg' ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) ('const/transc/atn' y)))).
tt('thm/transc/ATN_BOUNDS_e1', ax, (![y : 'type/realax/real']: ('const/realax/real_lt' ('const/transc/atn' y) ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))).
tt('thm/transc/TAN_ATN_', ax, (![x : 'type/realax/real']: ((('const/realax/real_lt' ('const/realax/real_neg' ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) x) & ('const/realax/real_lt' x ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))) => (('const/transc/atn' ('const/transc/tan' x)) = x)))).
tt('thm/transc/TAN_SEC_', ax, (![x : 'type/realax/real']: ((~ (('const/transc/cos' x) = ('const/real/real_of_num' 'const/num/0'))) => (('const/realax/real_add' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/real/pow' ('const/transc/tan' x) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) = ('const/real/pow' ('const/realax/inv' ('const/transc/cos' x)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))).
tt('thm/transc/SIN_COS_SQ_', ax, (![x : 'type/realax/real']: ((('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) & ('const/real/real_lte' x 'const/transc/pi')) => (('const/transc/sin' x) = ('const/transc/sqrt' ('const/real/real_sub' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/real/pow' ('const/transc/cos' x) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))).
tt('thm/transc/COS_SIN_SQ_', ax, (![x : 'type/realax/real']: ((('const/real/real_lte' ('const/realax/real_neg' ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) x) & ('const/real/real_lte' x ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))) => (('const/transc/cos' x) = ('const/transc/sqrt' ('const/real/real_sub' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/real/pow' ('const/transc/sin' x) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))).
tt('thm/transc/COS_ATN_NZ_', ax, (![x : 'type/realax/real']: (~ (('const/transc/cos' ('const/transc/atn' x)) = ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/transc/COS_ASN_NZ_', ax, (![x : 'type/realax/real']: ((('const/realax/real_lt' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) x) & ('const/realax/real_lt' x ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) => (~ (('const/transc/cos' ('const/transc/asn' x)) = ('const/real/real_of_num' 'const/num/0')))))).
tt('thm/transc/SIN_ACS_NZ_', ax, (![x : 'type/realax/real']: ((('const/realax/real_lt' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) x) & ('const/realax/real_lt' x ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) => (~ (('const/transc/sin' ('const/transc/acs' x)) = ('const/real/real_of_num' 'const/num/0')))))).
tt('thm/transc/COS_SIN_SQRT_', ax, (![x : 'type/realax/real']: (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') ('const/transc/cos' x)) => (('const/transc/cos' x) = ('const/transc/sqrt' ('const/real/real_sub' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/real/pow' ('const/transc/sin' x) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))).
tt('thm/transc/SIN_COS_SQRT_', ax, (![x : 'type/realax/real']: (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') ('const/transc/sin' x)) => (('const/transc/sin' x) = ('const/transc/sqrt' ('const/real/real_sub' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/real/pow' ('const/transc/cos' x) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))).
tt('thm/transc/DIFF_LN_', ax, (![x : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) => ('const/lim/diffl' 'const/transc/ln' ('const/realax/inv' x) x)))).
tt('thm/transc/DIFF_ASN_LEMMA_', ax, (![x : 'type/realax/real']: ((('const/realax/real_lt' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) x) & ('const/realax/real_lt' x ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) => ('const/lim/diffl' 'const/transc/asn' ('const/realax/inv' ('const/transc/cos' ('const/transc/asn' x))) x)))).
tt('thm/transc/DIFF_ASN_', ax, (![x : 'type/realax/real']: ((('const/realax/real_lt' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) x) & ('const/realax/real_lt' x ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) => ('const/lim/diffl' 'const/transc/asn' ('const/realax/inv' ('const/transc/sqrt' ('const/real/real_sub' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/real/pow' x ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))) x)))).
tt('thm/transc/DIFF_ACS_LEMMA_', ax, (![x : 'type/realax/real']: ((('const/realax/real_lt' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) x) & ('const/realax/real_lt' x ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) => ('const/lim/diffl' 'const/transc/acs' ('const/realax/inv' ('const/realax/real_neg' ('const/transc/sin' ('const/transc/acs' x)))) x)))).
tt('thm/transc/DIFF_ACS_', ax, (![x : 'type/realax/real']: ((('const/realax/real_lt' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) x) & ('const/realax/real_lt' x ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) => ('const/lim/diffl' 'const/transc/acs' ('const/realax/real_neg' ('const/realax/inv' ('const/transc/sqrt' ('const/real/real_sub' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/real/pow' x ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))) x)))).
tt('thm/transc/DIFF_ATN_', ax, (![x : 'type/realax/real']: ('const/lim/diffl' 'const/transc/atn' ('const/realax/inv' ('const/realax/real_add' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/real/pow' x ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) x))).
tt('thm/transc/division_', def, (![a : 'type/realax/real', b : 'type/realax/real', D : ('type/num/num' > 'type/realax/real')]: (('const/transc/division' (('const/pair/,' 'type/realax/real' 'type/realax/real') a b) D) = (((D 'const/num/0') = a) & (?[N : 'type/num/num']: ((![n : 'type/num/num']: (('const/prim_rec/<' n N) => ('const/realax/real_lt' (D n) (D ('const/num/SUC' n))))) & (![n : 'type/num/num']: (('const/arithmetic/>=' n N) => ((D n) = b))))))))).
tt('thm/transc/dsize_', def, (![D : ('type/num/num' > 'type/realax/real')]: (('const/transc/dsize' D) = (('const/min/@' 'type/num/num') (^[N : 'type/num/num']: ((![n : 'type/num/num']: (('const/prim_rec/<' n N) => ('const/realax/real_lt' (D n) (D ('const/num/SUC' n))))) & (![n : 'type/num/num']: (('const/arithmetic/>=' n N) => ((D n) = (D N)))))))))).
tt('thm/transc/tdiv_', def, (![a : 'type/realax/real', b : 'type/realax/real', D : ('type/num/num' > 'type/realax/real'), p : ('type/num/num' > 'type/realax/real')]: (('const/transc/tdiv' (('const/pair/,' 'type/realax/real' 'type/realax/real') a b) (('const/pair/,' ('type/num/num' > 'type/realax/real') ('type/num/num' > 'type/realax/real')) D p)) = (('const/transc/division' (('const/pair/,' 'type/realax/real' 'type/realax/real') a b) D) & (![n : 'type/num/num']: (('const/real/real_lte' (D n) (p n)) & ('const/real/real_lte' (p n) (D ('const/num/SUC' n))))))))).
tt('thm/transc/gauge_', def, (![E : ('type/realax/real' > $o), g : ('type/realax/real' > 'type/realax/real')]: (('const/transc/gauge' E g) = (![x : 'type/realax/real']: ((E x) => ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') (g x))))))).
tt('thm/transc/fine_', def, (![g : ('type/realax/real' > 'type/realax/real'), D : ('type/num/num' > 'type/realax/real'), p : ('type/num/num' > 'type/realax/real')]: (('const/transc/fine' g (('const/pair/,' ('type/num/num' > 'type/realax/real') ('type/num/num' > 'type/realax/real')) D p)) = (![n : 'type/num/num']: (('const/prim_rec/<' n ('const/transc/dsize' D)) => ('const/realax/real_lt' ('const/real/real_sub' (D ('const/num/SUC' n)) (D n)) (g (p n)))))))).
tt('thm/transc/rsum_', def, (![D : ('type/num/num' > 'type/realax/real'), p : ('type/num/num' > 'type/realax/real'), f : ('type/realax/real' > 'type/realax/real')]: (('const/transc/rsum' (('const/pair/,' ('type/num/num' > 'type/realax/real') ('type/num/num' > 'type/realax/real')) D p) f) = ('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') 'const/num/0' ('const/transc/dsize' D)) (^[n : 'type/num/num']: ('const/realax/real_mul' (f (p n)) ('const/real/real_sub' (D ('const/num/SUC' n)) (D n)))))))).
tt('thm/transc/Dint_', def, (![a : 'type/realax/real', b : 'type/realax/real', f : ('type/realax/real' > 'type/realax/real'), k : 'type/realax/real']: (('const/transc/Dint' (('const/pair/,' 'type/realax/real' 'type/realax/real') a b) f k) = (![e : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') e) => (?[g : ('type/realax/real' > 'type/realax/real')]: (('const/transc/gauge' (^[x : 'type/realax/real']: (('const/real/real_lte' a x) & ('const/real/real_lte' x b))) g) & (![D : ('type/num/num' > 'type/realax/real'), p : ('type/num/num' > 'type/realax/real')]: ((('const/transc/tdiv' (('const/pair/,' 'type/realax/real' 'type/realax/real') a b) (('const/pair/,' ('type/num/num' > 'type/realax/real') ('type/num/num' > 'type/realax/real')) D p)) & ('const/transc/fine' g (('const/pair/,' ('type/num/num' > 'type/realax/real') ('type/num/num' > 'type/realax/real')) D p))) => ('const/realax/real_lt' ('const/real/abs' ('const/real/real_sub' ('const/transc/rsum' (('const/pair/,' ('type/num/num' > 'type/realax/real') ('type/num/num' > 'type/realax/real')) D p) f) k)) e)))))))))).
tt('thm/transc/DIVISION_0_', ax, (![a : 'type/realax/real', b : 'type/realax/real']: ((a = b) => (('const/transc/dsize' (^[n : 'type/num/num']: (('const/bool/COND' 'type/realax/real') (n = 'const/num/0') a b))) = 'const/num/0')))).
tt('thm/transc/DIVISION_1_', ax, (![a : 'type/realax/real', b : 'type/realax/real']: (('const/realax/real_lt' a b) => (('const/transc/dsize' (^[n : 'type/num/num']: (('const/bool/COND' 'type/realax/real') (n = 'const/num/0') a b))) = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
tt('thm/transc/DIVISION_SINGLE_', ax, (![a : 'type/realax/real', b : 'type/realax/real']: (('const/real/real_lte' a b) => ('const/transc/division' (('const/pair/,' 'type/realax/real' 'type/realax/real') a b) (^[n : 'type/num/num']: (('const/bool/COND' 'type/realax/real') (n = 'const/num/0') a b)))))).
tt('thm/transc/DIVISION_LHS_', ax, (![D : ('type/num/num' > 'type/realax/real'), a : 'type/realax/real', b : 'type/realax/real']: (('const/transc/division' (('const/pair/,' 'type/realax/real' 'type/realax/real') a b) D) => ((D 'const/num/0') = a)))).
tt('thm/transc/DIVISION_THM_', ax, (![D : ('type/num/num' > 'type/realax/real'), a : 'type/realax/real', b : 'type/realax/real']: (('const/transc/division' (('const/pair/,' 'type/realax/real' 'type/realax/real') a b) D) = (((D 'const/num/0') = a) & ((![n : 'type/num/num']: (('const/prim_rec/<' n ('const/transc/dsize' D)) => ('const/realax/real_lt' (D n) (D ('const/num/SUC' n))))) & (![n : 'type/num/num']: (('const/arithmetic/>=' n ('const/transc/dsize' D)) => ((D n) = b)))))))).
tt('thm/transc/DIVISION_RHS_', ax, (![D : ('type/num/num' > 'type/realax/real'), a : 'type/realax/real', b : 'type/realax/real']: (('const/transc/division' (('const/pair/,' 'type/realax/real' 'type/realax/real') a b) D) => ((D ('const/transc/dsize' D)) = b)))).
tt('thm/transc/DIVISION_LT_GEN_', ax, (![D : ('type/num/num' > 'type/realax/real'), a : 'type/realax/real', b : 'type/realax/real', m : 'type/num/num', n : 'type/num/num']: ((('const/transc/division' (('const/pair/,' 'type/realax/real' 'type/realax/real') a b) D) & (('const/prim_rec/<' m n) & ('const/arithmetic/<=' n ('const/transc/dsize' D)))) => ('const/realax/real_lt' (D m) (D n))))).
tt('thm/transc/DIVISION_LT_', ax, (![D : ('type/num/num' > 'type/realax/real'), a : 'type/realax/real', b : 'type/realax/real']: (('const/transc/division' (('const/pair/,' 'type/realax/real' 'type/realax/real') a b) D) => (![n : 'type/num/num']: (('const/prim_rec/<' n ('const/transc/dsize' D)) => ('const/realax/real_lt' (D 'const/num/0') (D ('const/num/SUC' n)))))))).
tt('thm/transc/DIVISION_LE_', ax, (![D : ('type/num/num' > 'type/realax/real'), a : 'type/realax/real', b : 'type/realax/real']: (('const/transc/division' (('const/pair/,' 'type/realax/real' 'type/realax/real') a b) D) => ('const/real/real_lte' a b)))).
tt('thm/transc/DIVISION_GT_', ax, (![D : ('type/num/num' > 'type/realax/real'), a : 'type/realax/real', b : 'type/realax/real']: (('const/transc/division' (('const/pair/,' 'type/realax/real' 'type/realax/real') a b) D) => (![n : 'type/num/num']: (('const/prim_rec/<' n ('const/transc/dsize' D)) => ('const/realax/real_lt' (D n) (D ('const/transc/dsize' D)))))))).
tt('thm/transc/DIVISION_EQ_', ax, (![D : ('type/num/num' > 'type/realax/real'), a : 'type/realax/real', b : 'type/realax/real']: (('const/transc/division' (('const/pair/,' 'type/realax/real' 'type/realax/real') a b) D) => ((a = b) = (('const/transc/dsize' D) = 'const/num/0'))))).
tt('thm/transc/DIVISION_LBOUND_', ax, (![D : ('type/num/num' > 'type/realax/real'), a : 'type/realax/real', b : 'type/realax/real']: (('const/transc/division' (('const/pair/,' 'type/realax/real' 'type/realax/real') a b) D) => (![r : 'type/num/num']: ('const/real/real_lte' a (D r)))))).
tt('thm/transc/DIVISION_LBOUND_LT_', ax, (![D : ('type/num/num' > 'type/realax/real'), a : 'type/realax/real', b : 'type/realax/real']: ((('const/transc/division' (('const/pair/,' 'type/realax/real' 'type/realax/real') a b) D) & (~ (('const/transc/dsize' D) = 'const/num/0'))) => (![n : 'type/num/num']: ('const/realax/real_lt' a (D ('const/num/SUC' n))))))).
tt('thm/transc/DIVISION_UBOUND_', ax, (![D : ('type/num/num' > 'type/realax/real'), a : 'type/realax/real', b : 'type/realax/real']: (('const/transc/division' (('const/pair/,' 'type/realax/real' 'type/realax/real') a b) D) => (![r : 'type/num/num']: ('const/real/real_lte' (D r) b))))).
tt('thm/transc/DIVISION_UBOUND_LT_', ax, (![D : ('type/num/num' > 'type/realax/real'), a : 'type/realax/real', b : 'type/realax/real', n : 'type/num/num']: ((('const/transc/division' (('const/pair/,' 'type/realax/real' 'type/realax/real') a b) D) & ('const/prim_rec/<' n ('const/transc/dsize' D))) => ('const/realax/real_lt' (D n) b)))).
tt('thm/transc/DIVISION_APPEND_', ax, (![g : ('type/realax/real' > 'type/realax/real'), a : 'type/realax/real', b : 'type/realax/real', c : 'type/realax/real']: (((?[D1 : ('type/num/num' > 'type/realax/real'), p1 : ('type/num/num' > 'type/realax/real')]: (('const/transc/tdiv' (('const/pair/,' 'type/realax/real' 'type/realax/real') a b) (('const/pair/,' ('type/num/num' > 'type/realax/real') ('type/num/num' > 'type/realax/real')) D1 p1)) & ('const/transc/fine' g (('const/pair/,' ('type/num/num' > 'type/realax/real') ('type/num/num' > 'type/realax/real')) D1 p1)))) & (?[D2 : ('type/num/num' > 'type/realax/real'), p2 : ('type/num/num' > 'type/realax/real')]: (('const/transc/tdiv' (('const/pair/,' 'type/realax/real' 'type/realax/real') b c) (('const/pair/,' ('type/num/num' > 'type/realax/real') ('type/num/num' > 'type/realax/real')) D2 p2)) & ('const/transc/fine' g (('const/pair/,' ('type/num/num' > 'type/realax/real') ('type/num/num' > 'type/realax/real')) D2 p2))))) => (?[D : ('type/num/num' > 'type/realax/real'), p : ('type/num/num' > 'type/realax/real')]: (('const/transc/tdiv' (('const/pair/,' 'type/realax/real' 'type/realax/real') a c) (('const/pair/,' ('type/num/num' > 'type/realax/real') ('type/num/num' > 'type/realax/real')) D p)) & ('const/transc/fine' g (('const/pair/,' ('type/num/num' > 'type/realax/real') ('type/num/num' > 'type/realax/real')) D p))))))).
tt('thm/transc/DIVISION_EXISTS_', ax, (![a : 'type/realax/real', b : 'type/realax/real', g : ('type/realax/real' > 'type/realax/real')]: ((('const/real/real_lte' a b) & ('const/transc/gauge' (^[x : 'type/realax/real']: (('const/real/real_lte' a x) & ('const/real/real_lte' x b))) g)) => (?[D : ('type/num/num' > 'type/realax/real'), p : ('type/num/num' > 'type/realax/real')]: (('const/transc/tdiv' (('const/pair/,' 'type/realax/real' 'type/realax/real') a b) (('const/pair/,' ('type/num/num' > 'type/realax/real') ('type/num/num' > 'type/realax/real')) D p)) & ('const/transc/fine' g (('const/pair/,' ('type/num/num' > 'type/realax/real') ('type/num/num' > 'type/realax/real')) D p))))))).
tt('thm/transc/GAUGE_MIN_', ax, (![E : ('type/realax/real' > $o), g1 : ('type/realax/real' > 'type/realax/real'), g2 : ('type/realax/real' > 'type/realax/real')]: ((('const/transc/gauge' E g1) & ('const/transc/gauge' E g2)) => ('const/transc/gauge' E (^[x : 'type/realax/real']: (('const/bool/COND' 'type/realax/real') ('const/realax/real_lt' (g1 x) (g2 x)) (g1 x) (g2 x))))))).
tt('thm/transc/FINE_MIN_', ax, (![g1 : ('type/realax/real' > 'type/realax/real'), g2 : ('type/realax/real' > 'type/realax/real'), D : ('type/num/num' > 'type/realax/real'), p : ('type/num/num' > 'type/realax/real')]: (('const/transc/fine' (^[x : 'type/realax/real']: (('const/bool/COND' 'type/realax/real') ('const/realax/real_lt' (g1 x) (g2 x)) (g1 x) (g2 x))) (('const/pair/,' ('type/num/num' > 'type/realax/real') ('type/num/num' > 'type/realax/real')) D p)) => (('const/transc/fine' g1 (('const/pair/,' ('type/num/num' > 'type/realax/real') ('type/num/num' > 'type/realax/real')) D p)) & ('const/transc/fine' g2 (('const/pair/,' ('type/num/num' > 'type/realax/real') ('type/num/num' > 'type/realax/real')) D p)))))).
tt('thm/transc/DINT_UNIQ_', ax, (![a : 'type/realax/real', b : 'type/realax/real', f : ('type/realax/real' > 'type/realax/real'), k1 : 'type/realax/real', k2 : 'type/realax/real']: ((('const/real/real_lte' a b) & (('const/transc/Dint' (('const/pair/,' 'type/realax/real' 'type/realax/real') a b) f k1) & ('const/transc/Dint' (('const/pair/,' 'type/realax/real' 'type/realax/real') a b) f k2))) => (k1 = k2)))).
tt('thm/transc/INTEGRAL_NULL_', ax, (![f : ('type/realax/real' > 'type/realax/real'), a : 'type/realax/real']: ('const/transc/Dint' (('const/pair/,' 'type/realax/real' 'type/realax/real') a a) f ('const/real/real_of_num' 'const/num/0')))).
tt('thm/transc/FTC1_', ax, (![f : ('type/realax/real' > 'type/realax/real'), 'f\'' : ('type/realax/real' > 'type/realax/real'), a : 'type/realax/real', b : 'type/realax/real']: ((('const/real/real_lte' a b) & (![x : 'type/realax/real']: ((('const/real/real_lte' a x) & ('const/real/real_lte' x b)) => ('const/lim/diffl' f ('f\'' x) x)))) => ('const/transc/Dint' (('const/pair/,' 'type/realax/real' 'type/realax/real') a b) 'f\'' ('const/real/real_sub' (f b) (f a)))))).
tt('thm/transc/MCLAURIN_', ax, (![f : ('type/realax/real' > 'type/realax/real'), diff : ('type/num/num' > ('type/realax/real' > 'type/realax/real')), h : 'type/realax/real', n : 'type/num/num']: ((('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') h) & (('const/prim_rec/<' 'const/num/0' n) & (((diff 'const/num/0') = f) & (![m : 'type/num/num', t : 'type/realax/real']: ((('const/prim_rec/<' m n) & (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') t) & ('const/real/real_lte' t h))) => ('const/lim/diffl' (diff m) (diff ('const/num/SUC' m) t) t)))))) => (?[t : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') t) & (('const/realax/real_lt' t h) & ((f h) = ('const/realax/real_add' ('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') 'const/num/0' n) (^[m : 'type/num/num']: ('const/realax/real_mul' ('const/real/#slash#' (diff m ('const/real/real_of_num' 'const/num/0')) ('const/real/real_of_num' ('const/arithmetic/FACT' m))) ('const/real/pow' h m)))) ('const/realax/real_mul' ('const/real/#slash#' (diff n t) ('const/real/real_of_num' ('const/arithmetic/FACT' n))) ('const/real/pow' h n)))))))))).
tt('thm/transc/MCLAURIN_NEG_', ax, (![f : ('type/realax/real' > 'type/realax/real'), diff : ('type/num/num' > ('type/realax/real' > 'type/realax/real')), h : 'type/realax/real', n : 'type/num/num']: ((('const/realax/real_lt' h ('const/real/real_of_num' 'const/num/0')) & (('const/prim_rec/<' 'const/num/0' n) & (((diff 'const/num/0') = f) & (![m : 'type/num/num', t : 'type/realax/real']: ((('const/prim_rec/<' m n) & (('const/real/real_lte' h t) & ('const/real/real_lte' t ('const/real/real_of_num' 'const/num/0')))) => ('const/lim/diffl' (diff m) (diff ('const/num/SUC' m) t) t)))))) => (?[t : 'type/realax/real']: (('const/realax/real_lt' h t) & (('const/realax/real_lt' t ('const/real/real_of_num' 'const/num/0')) & ((f h) = ('const/realax/real_add' ('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') 'const/num/0' n) (^[m : 'type/num/num']: ('const/realax/real_mul' ('const/real/#slash#' (diff m ('const/real/real_of_num' 'const/num/0')) ('const/real/real_of_num' ('const/arithmetic/FACT' m))) ('const/real/pow' h m)))) ('const/realax/real_mul' ('const/real/#slash#' (diff n t) ('const/real/real_of_num' ('const/arithmetic/FACT' n))) ('const/real/pow' h n)))))))))).
tt('thm/transc/MCLAURIN_ALL_LT_', ax, (![f : ('type/realax/real' > 'type/realax/real'), diff : ('type/num/num' > ('type/realax/real' > 'type/realax/real'))]: ((((diff 'const/num/0') = f) & (![m : 'type/num/num', x : 'type/realax/real']: ('const/lim/diffl' (diff m) (diff ('const/num/SUC' m) x) x))) => (![x : 'type/realax/real', n : 'type/num/num']: (((~ (x = ('const/real/real_of_num' 'const/num/0'))) & ('const/prim_rec/<' 'const/num/0' n)) => (?[t : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/real/abs' t)) & (('const/realax/real_lt' ('const/real/abs' t) ('const/real/abs' x)) & ((f x) = ('const/realax/real_add' ('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') 'const/num/0' n) (^[m : 'type/num/num']: ('const/realax/real_mul' ('const/real/#slash#' (diff m ('const/real/real_of_num' 'const/num/0')) ('const/real/real_of_num' ('const/arithmetic/FACT' m))) ('const/real/pow' x m)))) ('const/realax/real_mul' ('const/real/#slash#' (diff n t) ('const/real/real_of_num' ('const/arithmetic/FACT' n))) ('const/real/pow' x n)))))))))))).
tt('thm/transc/MCLAURIN_ZERO_', ax, (![diff : ('type/num/num' > ('type/realax/real' > 'type/realax/real')), n : 'type/num/num', x : 'type/realax/real']: (((x = ('const/real/real_of_num' 'const/num/0')) & ('const/prim_rec/<' 'const/num/0' n)) => (('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') 'const/num/0' n) (^[m : 'type/num/num']: ('const/realax/real_mul' ('const/real/#slash#' (diff m ('const/real/real_of_num' 'const/num/0')) ('const/real/real_of_num' ('const/arithmetic/FACT' m))) ('const/real/pow' x m)))) = (diff 'const/num/0' ('const/real/real_of_num' 'const/num/0')))))).
tt('thm/transc/MCLAURIN_ALL_LE_', ax, (![f : ('type/realax/real' > 'type/realax/real'), diff : ('type/num/num' > ('type/realax/real' > 'type/realax/real'))]: ((((diff 'const/num/0') = f) & (![m : 'type/num/num', x : 'type/realax/real']: ('const/lim/diffl' (diff m) (diff ('const/num/SUC' m) x) x))) => (![x : 'type/realax/real', n : 'type/num/num']: (?[t : 'type/realax/real']: (('const/real/real_lte' ('const/real/abs' t) ('const/real/abs' x)) & ((f x) = ('const/realax/real_add' ('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') 'const/num/0' n) (^[m : 'type/num/num']: ('const/realax/real_mul' ('const/real/#slash#' (diff m ('const/real/real_of_num' 'const/num/0')) ('const/real/real_of_num' ('const/arithmetic/FACT' m))) ('const/real/pow' x m)))) ('const/realax/real_mul' ('const/real/#slash#' (diff n t) ('const/real/real_of_num' ('const/arithmetic/FACT' n))) ('const/real/pow' x n)))))))))).
tt('thm/transc/MCLAURIN_EXP_LT_', ax, (![x : 'type/realax/real', n : 'type/num/num']: (((~ (x = ('const/real/real_of_num' 'const/num/0'))) & ('const/prim_rec/<' 'const/num/0' n)) => (?[t : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/real/abs' t)) & (('const/realax/real_lt' ('const/real/abs' t) ('const/real/abs' x)) & (('const/transc/exp' x) = ('const/realax/real_add' ('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') 'const/num/0' n) (^[m : 'type/num/num']: ('const/real/#slash#' ('const/real/pow' x m) ('const/real/real_of_num' ('const/arithmetic/FACT' m))))) ('const/realax/real_mul' ('const/real/#slash#' ('const/transc/exp' t) ('const/real/real_of_num' ('const/arithmetic/FACT' n))) ('const/real/pow' x n)))))))))).
tt('thm/transc/MCLAURIN_EXP_LE_', ax, (![x : 'type/realax/real', n : 'type/num/num']: (?[t : 'type/realax/real']: (('const/real/real_lte' ('const/real/abs' t) ('const/real/abs' x)) & (('const/transc/exp' x) = ('const/realax/real_add' ('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') 'const/num/0' n) (^[m : 'type/num/num']: ('const/real/#slash#' ('const/real/pow' x m) ('const/real/real_of_num' ('const/arithmetic/FACT' m))))) ('const/realax/real_mul' ('const/real/#slash#' ('const/transc/exp' t) ('const/real/real_of_num' ('const/arithmetic/FACT' n))) ('const/real/pow' x n)))))))).
tt('thm/transc/DIFF_LN_COMPOSITE_', ax, (![g : ('type/realax/real' > 'type/realax/real'), m : 'type/realax/real', x : 'type/realax/real']: ((('const/lim/diffl' g m x) & ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') (g x))) => ('const/lim/diffl' (^[x0 : 'type/realax/real']: ('const/transc/ln' (g x0))) ('const/realax/real_mul' ('const/realax/inv' (g x)) m) x)))).
tt('thm/transc/rpow_def_', def, (![a : 'type/realax/real', b : 'type/realax/real']: (('const/transc/rpow' a b) = ('const/transc/exp' ('const/realax/real_mul' b ('const/transc/ln' a)))))).
tt('thm/transc/GEN_RPOW_', ax, (![a : 'type/realax/real', n : 'type/num/num']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') a) => (('const/real/pow' a n) = ('const/transc/rpow' a ('const/real/real_of_num' n)))))).
tt('thm/transc/RPOW_SUC_N_', ax, (![a : 'type/realax/real', n : 'type/num/num']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') a) => (('const/transc/rpow' a ('const/realax/real_add' ('const/real/real_of_num' n) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) = ('const/real/pow' a ('const/num/SUC' n)))))).
tt('thm/transc/RPOW_0_', ax, (![a : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') a) => (('const/transc/rpow' a ('const/real/real_of_num' 'const/num/0')) = ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))).
tt('thm/transc/RPOW_1_', ax, (![a : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') a) => (('const/transc/rpow' a ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = a)))).
tt('thm/transc/ONE_RPOW_', ax, (![a : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') a) => (('const/transc/rpow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) a) = ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))).
tt('thm/transc/RPOW_POS_LT_', ax, (![a : 'type/realax/real', b : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') a) => ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/transc/rpow' a b))))).
tt('thm/transc/RPOW_NZ_', ax, (![a : 'type/realax/real', b : 'type/realax/real']: ((~ (('const/real/real_of_num' 'const/num/0') = a)) => (~ (('const/transc/rpow' a b) = ('const/real/real_of_num' 'const/num/0')))))).
tt('thm/transc/LN_RPOW_', ax, (![a : 'type/realax/real', b : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') a) => (('const/transc/ln' ('const/transc/rpow' a b)) = ('const/realax/real_mul' b ('const/transc/ln' a)))))).
tt('thm/transc/RPOW_ADD_', ax, (![a : 'type/realax/real', b : 'type/realax/real', c : 'type/realax/real']: (('const/transc/rpow' a ('const/realax/real_add' b c)) = ('const/realax/real_mul' ('const/transc/rpow' a b) ('const/transc/rpow' a c))))).
tt('thm/transc/RPOW_ADD_MUL_', ax, (![a : 'type/realax/real', b : 'type/realax/real', c : 'type/realax/real']: (('const/realax/real_mul' ('const/transc/rpow' a ('const/realax/real_add' b c)) ('const/transc/rpow' a ('const/realax/real_neg' b))) = ('const/transc/rpow' a c)))).
tt('thm/transc/RPOW_SUB_', ax, (![a : 'type/realax/real', b : 'type/realax/real', c : 'type/realax/real']: (('const/transc/rpow' a ('const/real/real_sub' b c)) = ('const/real/#slash#' ('const/transc/rpow' a b) ('const/transc/rpow' a c))))).
tt('thm/transc/RPOW_DIV_', ax, (![a : 'type/realax/real', b : 'type/realax/real', c : 'type/realax/real']: ((('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') a) & ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') b)) => (('const/transc/rpow' ('const/real/#slash#' a b) c) = ('const/real/#slash#' ('const/transc/rpow' a c) ('const/transc/rpow' b c)))))).
tt('thm/transc/RPOW_INV_', ax, (![a : 'type/realax/real', b : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') a) => (('const/transc/rpow' ('const/realax/inv' a) b) = ('const/realax/inv' ('const/transc/rpow' a b)))))).
tt('thm/transc/RPOW_MUL_', ax, (![a : 'type/realax/real', b : 'type/realax/real', c : 'type/realax/real']: ((('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') a) & ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') b)) => (('const/transc/rpow' ('const/realax/real_mul' a b) c) = ('const/realax/real_mul' ('const/transc/rpow' a c) ('const/transc/rpow' b c)))))).
tt('thm/transc/RPOW_RPOW_', ax, (![a : 'type/realax/real', b : 'type/realax/real', c : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') a) => (('const/transc/rpow' ('const/transc/rpow' a b) c) = ('const/transc/rpow' a ('const/realax/real_mul' b c)))))).
tt('thm/transc/RPOW_LT_', ax, (![a : 'type/realax/real', b : 'type/realax/real', c : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) a) => (('const/realax/real_lt' ('const/transc/rpow' a b) ('const/transc/rpow' a c)) = ('const/realax/real_lt' b c))))).
tt('thm/transc/RPOW_LE_', ax, (![a : 'type/realax/real', b : 'type/realax/real', c : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) a) => (('const/real/real_lte' ('const/transc/rpow' a b) ('const/transc/rpow' a c)) = ('const/real/real_lte' b c))))).
tt('thm/transc/BASE_RPOW_LE_', ax, (![a : 'type/realax/real', b : 'type/realax/real', c : 'type/realax/real']: ((('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') a) & (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') c) & ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') b))) => (('const/real/real_lte' ('const/transc/rpow' a b) ('const/transc/rpow' c b)) = ('const/real/real_lte' a c))))).
tt('thm/transc/BASE_RPOW_LT_', ax, (![a : 'type/realax/real', b : 'type/realax/real', c : 'type/realax/real']: ((('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') a) & (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') c) & ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') b))) => (('const/realax/real_lt' ('const/transc/rpow' a b) ('const/transc/rpow' c b)) = ('const/realax/real_lt' a c))))).
tt('thm/transc/RPOW_UNIQ_BASE_', ax, (![a : 'type/realax/real', b : 'type/realax/real', c : 'type/realax/real']: ((('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') a) & (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') c) & ((~ (('const/real/real_of_num' 'const/num/0') = b)) & (('const/transc/rpow' a b) = ('const/transc/rpow' c b))))) => (a = c)))).
tt('thm/transc/RPOW_UNIQ_EXP_', ax, (![a : 'type/realax/real', b : 'type/realax/real', c : 'type/realax/real']: ((('const/realax/real_lt' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) a) & (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') c) & (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') b) & (('const/transc/rpow' a b) = ('const/transc/rpow' a c))))) => (b = c)))).
tt('thm/transc/RPOW_DIV_BASE_', ax, (![x : 'type/realax/real', t : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) => (('const/real/#slash#' ('const/transc/rpow' x t) x) = ('const/transc/rpow' x ('const/real/real_sub' t ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))).
tt('thm/transc/DIFF_COMPOSITE_EXP_', ax, (![g : ('type/realax/real' > 'type/realax/real'), m : 'type/realax/real', x : 'type/realax/real']: (('const/lim/diffl' g m x) => ('const/lim/diffl' (^[x0 : 'type/realax/real']: ('const/transc/exp' (g x0))) ('const/realax/real_mul' ('const/transc/exp' (g x)) m) x)))).
tt('thm/transc/DIFF_RPOW_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) => ('const/lim/diffl' (^[x0 : 'type/realax/real']: ('const/transc/rpow' x0 y)) ('const/realax/real_mul' y ('const/transc/rpow' x ('const/real/real_sub' y ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))) x)))).
