tt('type/sptree/spt', ty, $t > $t).
tt('const/sptree/BN', ty, ![A : $t]: (('type/sptree/spt' A) > (('type/sptree/spt' A) > ('type/sptree/spt' A)))).
tt('const/sptree/BS', ty, ![A : $t]: (('type/sptree/spt' A) > (A > (('type/sptree/spt' A) > ('type/sptree/spt' A))))).
tt('const/sptree/LN', ty, ![A : $t]: ('type/sptree/spt' A)).
tt('const/sptree/LS', ty, ![A : $t]: (A > ('type/sptree/spt' A))).
tt('const/sptree/delete', ty, ![A : $t]: ('type/num/num' > (('type/sptree/spt' A) > ('type/sptree/spt' A)))).
tt('const/sptree/difference', ty, ![A : $t, B : $t]: (('type/sptree/spt' A) > (('type/sptree/spt' B) > ('type/sptree/spt' A)))).
tt('const/sptree/domain', ty, ![A : $t]: (('type/sptree/spt' A) > ('type/num/num' > $o))).
tt('const/sptree/foldi', ty, ![A : $t, B : $t]: (('type/num/num' > (B > (A > A))) > ('type/num/num' > (A > (('type/sptree/spt' B) > A))))).
tt('const/sptree/fromAList', ty, ![A : $t]: (('type/list/list' ('type/pair/prod' 'type/num/num' A)) > ('type/sptree/spt' A))).
tt('const/sptree/fromList', ty, ![A : $t]: (('type/list/list' A) > ('type/sptree/spt' A))).
tt('const/sptree/insert', ty, ![A : $t]: ('type/num/num' > (A > (('type/sptree/spt' A) > ('type/sptree/spt' A))))).
tt('const/sptree/insert_tupled', ty, ![A : $t]: (('type/pair/prod' 'type/num/num' ('type/pair/prod' A ('type/sptree/spt' A))) > ('type/sptree/spt' A))).
tt('const/sptree/inter', ty, ![A : $t, B : $t]: (('type/sptree/spt' A) > (('type/sptree/spt' B) > ('type/sptree/spt' A)))).
tt('const/sptree/inter_eq', ty, ![A : $t]: (('type/sptree/spt' A) > (('type/sptree/spt' A) > ('type/sptree/spt' A)))).
tt('const/sptree/lookup', ty, ![A : $t]: ('type/num/num' > (('type/sptree/spt' A) > ('type/option/option' A)))).
tt('const/sptree/lookup_tupled', ty, ![A : $t]: (('type/pair/prod' 'type/num/num' ('type/sptree/spt' A)) > ('type/option/option' A))).
tt('const/sptree/lrnext', ty, ('type/num/num' > 'type/num/num')).
tt('const/sptree/mk_BN', ty, ![A : $t]: (('type/sptree/spt' A) > (('type/sptree/spt' A) > ('type/sptree/spt' A)))).
tt('const/sptree/mk_BN_tupled', ty, ![A : $t]: (('type/pair/prod' ('type/sptree/spt' A) ('type/sptree/spt' A)) > ('type/sptree/spt' A))).
tt('const/sptree/mk_BS', ty, ![A : $t]: (('type/sptree/spt' A) > (A > (('type/sptree/spt' A) > ('type/sptree/spt' A))))).
tt('const/sptree/mk_BS_tupled', ty, ![A : $t]: (('type/pair/prod' ('type/sptree/spt' A) ('type/pair/prod' A ('type/sptree/spt' A))) > ('type/sptree/spt' A))).
tt('const/sptree/mk_wf', ty, ![A : $t]: (('type/sptree/spt' A) > ('type/sptree/spt' A))).
tt('const/sptree/size', ty, ![A : $t]: (('type/sptree/spt' A) > 'type/num/num')).
tt('const/sptree/spt_CASE', ty, ![A : $t, B : $t]: (('type/sptree/spt' A) > (B > ((A > B) > ((('type/sptree/spt' A) > (('type/sptree/spt' A) > B)) > ((('type/sptree/spt' A) > (A > (('type/sptree/spt' A) > B))) > B)))))).
tt('const/sptree/spt_size', ty, ![A : $t]: ((A > 'type/num/num') > (('type/sptree/spt' A) > 'type/num/num'))).
tt('const/sptree/toAList', ty, ![A : $t]: (('type/sptree/spt' A) > ('type/list/list' ('type/pair/prod' 'type/num/num' A)))).
tt('const/sptree/toList', ty, ![A : $t]: (('type/sptree/spt' A) > ('type/list/list' A))).
tt('const/sptree/toListA', ty, ![A : $t]: (('type/list/list' A) > (('type/sptree/spt' A) > ('type/list/list' A)))).
tt('const/sptree/union', ty, ![A : $t]: (('type/sptree/spt' A) > (('type/sptree/spt' A) > ('type/sptree/spt' A)))).
tt('const/sptree/wf', ty, ![A : $t]: (('type/sptree/spt' A) > $o)).
tt('thm/sptree/spt_TY_DEF_', def, ![A : $t]: (?[rep : (('type/sptree/spt' A) > ('type/ind_type/recspace' A))]: (('const/bool/TYPE_DEFINITION' ('type/ind_type/recspace' A) ('type/sptree/spt' A)) (^['a0\'' : ('type/ind_type/recspace' A)]: (!['\'spt\'' : (('type/ind_type/recspace' A) > $o)]: ((!['a0\'0' : ('type/ind_type/recspace' A)]: ((('a0\'0' = (('const/ind_type/CONSTR' A) 'const/num/0' ('const/bool/ARB' A) (^[n : 'type/num/num']: ('const/ind_type/BOTTOM' A)))) | ((?[a : A]: ('a0\'0' = ((^[a0 : A]: (('const/ind_type/CONSTR' A) ('const/num/SUC' 'const/num/0') a0 (^[n : 'type/num/num']: ('const/ind_type/BOTTOM' A)))) a))) | ((?[a0 : ('type/ind_type/recspace' A), a1 : ('type/ind_type/recspace' A)]: (('a0\'0' = ((^[a00 : ('type/ind_type/recspace' A), a10 : ('type/ind_type/recspace' A)]: (('const/ind_type/CONSTR' A) ('const/num/SUC' ('const/num/SUC' 'const/num/0')) ('const/bool/ARB' A) (('const/ind_type/FCONS' ('type/ind_type/recspace' A)) a00 (('const/ind_type/FCONS' ('type/ind_type/recspace' A)) a10 (^[n : 'type/num/num']: ('const/ind_type/BOTTOM' A)))))) a0 a1)) & (('\'spt\'' a0) & ('\'spt\'' a1)))) | (?[a0 : ('type/ind_type/recspace' A), a1 : A, a2 : ('type/ind_type/recspace' A)]: (('a0\'0' = ((^[a00 : ('type/ind_type/recspace' A), a10 : A, a20 : ('type/ind_type/recspace' A)]: (('const/ind_type/CONSTR' A) ('const/num/SUC' ('const/num/SUC' ('const/num/SUC' 'const/num/0'))) a10 (('const/ind_type/FCONS' ('type/ind_type/recspace' A)) a00 (('const/ind_type/FCONS' ('type/ind_type/recspace' A)) a20 (^[n : 'type/num/num']: ('const/ind_type/BOTTOM' A)))))) a0 a1 a2)) & (('\'spt\'' a0) & ('\'spt\'' a2))))))) => ('\'spt\'' 'a0\'0'))) => ('\'spt\'' 'a0\'')))) rep))).
tt('thm/sptree/spt_case_def_0', def, ![B : $t, A : $t]: (![v : B, f : (A > B), f1 : (('type/sptree/spt' A) > (('type/sptree/spt' A) > B)), f2 : (('type/sptree/spt' A) > (A > (('type/sptree/spt' A) > B)))]: ((('const/sptree/spt_CASE' A B) ('const/sptree/LN' A) v f f1 f2) = v))).
tt('thm/sptree/spt_case_def_1', def, ![A : $t, B : $t]: (![a : A, v : B, f : (A > B), f1 : (('type/sptree/spt' A) > (('type/sptree/spt' A) > B)), f2 : (('type/sptree/spt' A) > (A > (('type/sptree/spt' A) > B)))]: ((('const/sptree/spt_CASE' A B) (('const/sptree/LS' A) a) v f f1 f2) = (f a)))).
tt('thm/sptree/spt_case_def_2', def, ![A : $t, B : $t]: (![a0 : ('type/sptree/spt' A), a1 : ('type/sptree/spt' A), v : B, f : (A > B), f1 : (('type/sptree/spt' A) > (('type/sptree/spt' A) > B)), f2 : (('type/sptree/spt' A) > (A > (('type/sptree/spt' A) > B)))]: ((('const/sptree/spt_CASE' A B) (('const/sptree/BN' A) a0 a1) v f f1 f2) = (f1 a0 a1)))).
tt('thm/sptree/spt_case_def_e3', def, ![A : $t, B : $t]: (![a0 : ('type/sptree/spt' A), a1 : A, a2 : ('type/sptree/spt' A), v : B, f : (A > B), f1 : (('type/sptree/spt' A) > (('type/sptree/spt' A) > B)), f2 : (('type/sptree/spt' A) > (A > (('type/sptree/spt' A) > B)))]: ((('const/sptree/spt_CASE' A B) (('const/sptree/BS' A) a0 a1 a2) v f f1 f2) = (f2 a0 a1 a2)))).
tt('thm/sptree/spt_size_def_0', def, ![A : $t]: (![f : (A > 'type/num/num')]: ((('const/sptree/spt_size' A) f ('const/sptree/LN' A)) = 'const/num/0'))).
tt('thm/sptree/spt_size_def_1', def, ![A : $t]: (![f : (A > 'type/num/num'), a : A]: ((('const/sptree/spt_size' A) f (('const/sptree/LS' A) a)) = ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) (f a))))).
tt('thm/sptree/spt_size_def_2', def, ![A : $t]: (![f : (A > 'type/num/num'), a0 : ('type/sptree/spt' A), a1 : ('type/sptree/spt' A)]: ((('const/sptree/spt_size' A) f (('const/sptree/BN' A) a0 a1)) = ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) ('const/arithmetic/+' (('const/sptree/spt_size' A) f a0) (('const/sptree/spt_size' A) f a1)))))).
tt('thm/sptree/spt_size_def_e3', def, ![A : $t]: (![f : (A > 'type/num/num'), a0 : ('type/sptree/spt' A), a1 : A, a2 : ('type/sptree/spt' A)]: ((('const/sptree/spt_size' A) f (('const/sptree/BS' A) a0 a1 a2)) = ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) ('const/arithmetic/+' (('const/sptree/spt_size' A) f a0) ('const/arithmetic/+' (f a1) (('const/sptree/spt_size' A) f a2))))))).
tt('thm/sptree/datatype_spt_', ax, ![A : $t]: (![spt : (('type/sptree/spt' A) > ((A > ('type/sptree/spt' A)) > ((('type/sptree/spt' A) > (('type/sptree/spt' A) > ('type/sptree/spt' A))) > ((('type/sptree/spt' A) > (A > (('type/sptree/spt' A) > ('type/sptree/spt' A)))) > $o))))]: (('const/bool/DATATYPE' $o) (spt ('const/sptree/LN' A) ('const/sptree/LS' A) ('const/sptree/BN' A) ('const/sptree/BS' A))))).
tt('thm/sptree/spt_11_0', ax, ![A : $t]: (![a : A, 'a\'' : A]: (((('const/sptree/LS' A) a) = (('const/sptree/LS' A) 'a\'')) = (a = 'a\'')))).
tt('thm/sptree/spt_11_1', ax, ![A : $t]: (![a0 : ('type/sptree/spt' A), a1 : ('type/sptree/spt' A), 'a0\'' : ('type/sptree/spt' A), 'a1\'' : ('type/sptree/spt' A)]: (((('const/sptree/BN' A) a0 a1) = (('const/sptree/BN' A) 'a0\'' 'a1\'')) = ((a0 = 'a0\'') & (a1 = 'a1\''))))).
tt('thm/sptree/spt_11_e2', ax, ![A : $t]: (![a0 : ('type/sptree/spt' A), a1 : A, a2 : ('type/sptree/spt' A), 'a0\'' : ('type/sptree/spt' A), 'a1\'' : A, 'a2\'' : ('type/sptree/spt' A)]: (((('const/sptree/BS' A) a0 a1 a2) = (('const/sptree/BS' A) 'a0\'' 'a1\'' 'a2\'')) = ((a0 = 'a0\'') & ((a1 = 'a1\'') & (a2 = 'a2\'')))))).
tt('thm/sptree/spt_distinct_0', ax, ![A : $t]: (![a : A]: (~ (('const/sptree/LN' A) = (('const/sptree/LS' A) a))))).
tt('thm/sptree/spt_distinct_1', ax, ![A : $t]: (![a1 : ('type/sptree/spt' A), a0 : ('type/sptree/spt' A)]: (~ (('const/sptree/LN' A) = (('const/sptree/BN' A) a0 a1))))).
tt('thm/sptree/spt_distinct_2', ax, ![A : $t]: (![a2 : ('type/sptree/spt' A), a1 : A, a0 : ('type/sptree/spt' A)]: (~ (('const/sptree/LN' A) = (('const/sptree/BS' A) a0 a1 a2))))).
tt('thm/sptree/spt_distinct_3', ax, ![A : $t]: (![a1 : ('type/sptree/spt' A), a0 : ('type/sptree/spt' A), a : A]: (~ ((('const/sptree/LS' A) a) = (('const/sptree/BN' A) a0 a1))))).
tt('thm/sptree/spt_distinct_4', ax, ![A : $t]: (![a2 : ('type/sptree/spt' A), a1 : A, a0 : ('type/sptree/spt' A), a : A]: (~ ((('const/sptree/LS' A) a) = (('const/sptree/BS' A) a0 a1 a2))))).
tt('thm/sptree/spt_distinct_e5', ax, ![A : $t]: (![a2 : ('type/sptree/spt' A), 'a1\'' : A, a1 : ('type/sptree/spt' A), 'a0\'' : ('type/sptree/spt' A), a0 : ('type/sptree/spt' A)]: (~ ((('const/sptree/BN' A) a0 a1) = (('const/sptree/BS' A) 'a0\'' 'a1\'' a2))))).
tt('thm/sptree/spt_case_cong_', ax, ![A : $t, B : $t]: (!['v\'' : B, 'f2\'' : (('type/sptree/spt' A) > (A > (('type/sptree/spt' A) > B))), 'f1\'' : (('type/sptree/spt' A) > (('type/sptree/spt' A) > B)), 'f\'' : (A > B), M : ('type/sptree/spt' A), 'M\'' : ('type/sptree/spt' A), v : B, f : (A > B), f1 : (('type/sptree/spt' A) > (('type/sptree/spt' A) > B)), f2 : (('type/sptree/spt' A) > (A > (('type/sptree/spt' A) > B)))]: (((M = 'M\'') & ((('M\'' = ('const/sptree/LN' A)) => (v = 'v\'')) & ((![a : A]: (('M\'' = (('const/sptree/LS' A) a)) => ((f a) = ('f\'' a)))) & ((![a0 : ('type/sptree/spt' A), a1 : ('type/sptree/spt' A)]: (('M\'' = (('const/sptree/BN' A) a0 a1)) => ((f1 a0 a1) = ('f1\'' a0 a1)))) & (![a0 : ('type/sptree/spt' A), a1 : A, a2 : ('type/sptree/spt' A)]: (('M\'' = (('const/sptree/BS' A) a0 a1 a2)) => ((f2 a0 a1 a2) = ('f2\'' a0 a1 a2)))))))) => ((('const/sptree/spt_CASE' A B) M v f f1 f2) = (('const/sptree/spt_CASE' A B) 'M\'' 'v\'' 'f\'' 'f1\'' 'f2\''))))).
tt('thm/sptree/spt_nchotomy_', ax, ![A : $t]: (![ss : ('type/sptree/spt' A)]: ((ss = ('const/sptree/LN' A)) | ((?[a : A]: (ss = (('const/sptree/LS' A) a))) | ((?[s : ('type/sptree/spt' A), s0 : ('type/sptree/spt' A)]: (ss = (('const/sptree/BN' A) s s0))) | (?[s : ('type/sptree/spt' A), a : A, s0 : ('type/sptree/spt' A)]: (ss = (('const/sptree/BS' A) s a s0)))))))).
tt('thm/sptree/spt_Axiom_', ax, ![A : $t, B : $t]: (![f0 : B, f1 : (A > B), f2 : (('type/sptree/spt' A) > (('type/sptree/spt' A) > (B > (B > B)))), f3 : (A > (('type/sptree/spt' A) > (('type/sptree/spt' A) > (B > (B > B)))))]: (?[fn : (('type/sptree/spt' A) > B)]: (((fn ('const/sptree/LN' A)) = f0) & ((![a : A]: ((fn (('const/sptree/LS' A) a)) = (f1 a))) & ((![a0 : ('type/sptree/spt' A), a1 : ('type/sptree/spt' A)]: ((fn (('const/sptree/BN' A) a0 a1)) = (f2 a0 a1 (fn a0) (fn a1)))) & (![a0 : ('type/sptree/spt' A), a1 : A, a2 : ('type/sptree/spt' A)]: ((fn (('const/sptree/BS' A) a0 a1 a2)) = (f3 a1 a0 a2 (fn a0) (fn a2)))))))))).
tt('thm/sptree/spt_induction_', ax, ![A : $t]: (![P : (('type/sptree/spt' A) > $o)]: (((P ('const/sptree/LN' A)) & ((![a : A]: (P (('const/sptree/LS' A) a))) & ((![s : ('type/sptree/spt' A), s0 : ('type/sptree/spt' A)]: (((P s) & (P s0)) => (P (('const/sptree/BN' A) s s0)))) & (![s : ('type/sptree/spt' A), s0 : ('type/sptree/spt' A)]: (((P s) & (P s0)) => (![a : A]: (P (('const/sptree/BS' A) s a s0)))))))) => (![s : ('type/sptree/spt' A)]: (P s))))).
tt('thm/sptree/wf_def_0', def, ![A : $t]: ((('const/sptree/wf' A) ('const/sptree/LN' A)) = $true)).
tt('thm/sptree/wf_def_1', def, ![A : $t]: (![a : A]: ((('const/sptree/wf' A) (('const/sptree/LS' A) a)) = $true))).
tt('thm/sptree/wf_def_2', def, ![A : $t]: (![t1 : ('type/sptree/spt' A), t2 : ('type/sptree/spt' A)]: ((('const/sptree/wf' A) (('const/sptree/BN' A) t1 t2)) = ((('const/sptree/wf' A) t1) & ((('const/sptree/wf' A) t2) & (~ ((t1 = ('const/sptree/LN' A)) & (t2 = ('const/sptree/LN' A))))))))).
tt('thm/sptree/wf_def_e3', def, ![A : $t]: (![t1 : ('type/sptree/spt' A), a : A, t2 : ('type/sptree/spt' A)]: ((('const/sptree/wf' A) (('const/sptree/BS' A) t1 a t2)) = ((('const/sptree/wf' A) t1) & ((('const/sptree/wf' A) t2) & (~ ((t1 = ('const/sptree/LN' A)) & (t2 = ('const/sptree/LN' A))))))))).
tt('thm/sptree/lookup_tupled_primitive_def_', def, ![A : $t]: (('const/sptree/lookup_tupled' A) = (('const/relation/WFREC' ('type/pair/prod' 'type/num/num' ('type/sptree/spt' A)) ('type/option/option' A)) (('const/min/@' (('type/pair/prod' 'type/num/num' ('type/sptree/spt' A)) > (('type/pair/prod' 'type/num/num' ('type/sptree/spt' A)) > $o))) (^[R : (('type/pair/prod' 'type/num/num' ('type/sptree/spt' A)) > (('type/pair/prod' 'type/num/num' ('type/sptree/spt' A)) > $o))]: ((('const/relation/WF' ('type/pair/prod' 'type/num/num' ('type/sptree/spt' A))) R) & ((![t2 : ('type/sptree/spt' A), t1 : ('type/sptree/spt' A), k : 'type/num/num']: ((~ (k = 'const/num/0')) => (R (('const/pair/,' 'type/num/num' ('type/sptree/spt' A)) ('const/arithmetic/DIV' ('const/arithmetic/-' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) (('const/bool/COND' ('type/sptree/spt' A)) ('const/arithmetic/EVEN' k) t1 t2)) (('const/pair/,' 'type/num/num' ('type/sptree/spt' A)) k (('const/sptree/BN' A) t1 t2))))) & (![a : A, t2 : ('type/sptree/spt' A), t1 : ('type/sptree/spt' A), k : 'type/num/num']: ((~ (k = 'const/num/0')) => (R (('const/pair/,' 'type/num/num' ('type/sptree/spt' A)) ('const/arithmetic/DIV' ('const/arithmetic/-' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) (('const/bool/COND' ('type/sptree/spt' A)) ('const/arithmetic/EVEN' k) t1 t2)) (('const/pair/,' 'type/num/num' ('type/sptree/spt' A)) k (('const/sptree/BS' A) t1 a t2))))))))) (^[lookup_tupled : (('type/pair/prod' 'type/num/num' ('type/sptree/spt' A)) > ('type/option/option' A)), 'a\'' : ('type/pair/prod' 'type/num/num' ('type/sptree/spt' A))]: (('const/pair/pair_CASE' ('type/option/option' A) 'type/num/num' ('type/sptree/spt' A)) 'a\'' (^[k : 'type/num/num', v1 : ('type/sptree/spt' A)]: (('const/sptree/spt_CASE' A ('type/option/option' A)) v1 (('const/combin/I' ('type/option/option' A)) ('const/option/NONE' A)) (^[a : A]: (('const/combin/I' ('type/option/option' A)) (('const/bool/COND' ('type/option/option' A)) (k = 'const/num/0') (('const/option/SOME' A) a) ('const/option/NONE' A)))) (^[t1 : ('type/sptree/spt' A), t2 : ('type/sptree/spt' A)]: (('const/combin/I' ('type/option/option' A)) (('const/bool/COND' ('type/option/option' A)) (k = 'const/num/0') ('const/option/NONE' A) (lookup_tupled (('const/pair/,' 'type/num/num' ('type/sptree/spt' A)) ('const/arithmetic/DIV' ('const/arithmetic/-' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) (('const/bool/COND' ('type/sptree/spt' A)) ('const/arithmetic/EVEN' k) t1 t2)))))) (^['t1\'' : ('type/sptree/spt' A), 'a\'\'' : A, 't2\'' : ('type/sptree/spt' A)]: (('const/combin/I' ('type/option/option' A)) (('const/bool/COND' ('type/option/option' A)) (k = 'const/num/0') (('const/option/SOME' A) 'a\'\'') (lookup_tupled (('const/pair/,' 'type/num/num' ('type/sptree/spt' A)) ('const/arithmetic/DIV' ('const/arithmetic/-' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) (('const/bool/COND' ('type/sptree/spt' A)) ('const/arithmetic/EVEN' k) 't1\'' 't2\''))))))))))))).
tt('thm/sptree/lookup_curried_def_', def, ![A : $t]: (![x : 'type/num/num', x1 : ('type/sptree/spt' A)]: ((('const/sptree/lookup' A) x x1) = (('const/sptree/lookup_tupled' A) (('const/pair/,' 'type/num/num' ('type/sptree/spt' A)) x x1))))).
tt('thm/sptree/lookup_ind_', ax, ![A : $t]: (![P : ('type/num/num' > (('type/sptree/spt' A) > $o))]: (((![k : 'type/num/num']: (P k ('const/sptree/LN' A))) & ((![k : 'type/num/num', a : A]: (P k (('const/sptree/LS' A) a))) & ((![k : 'type/num/num', t1 : ('type/sptree/spt' A), t2 : ('type/sptree/spt' A)]: (((~ (k = 'const/num/0')) => (P ('const/arithmetic/DIV' ('const/arithmetic/-' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) (('const/bool/COND' ('type/sptree/spt' A)) ('const/arithmetic/EVEN' k) t1 t2))) => (P k (('const/sptree/BN' A) t1 t2)))) & (![k : 'type/num/num', t1 : ('type/sptree/spt' A), a : A, t2 : ('type/sptree/spt' A)]: (((~ (k = 'const/num/0')) => (P ('const/arithmetic/DIV' ('const/arithmetic/-' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) (('const/bool/COND' ('type/sptree/spt' A)) ('const/arithmetic/EVEN' k) t1 t2))) => (P k (('const/sptree/BS' A) t1 a t2))))))) => (![v : 'type/num/num', v1 : ('type/sptree/spt' A)]: (P v v1))))).
tt('thm/sptree/lookup_def_0', ax, ![A : $t]: (![k : 'type/num/num']: ((('const/sptree/lookup' A) k ('const/sptree/LN' A)) = ('const/option/NONE' A)))).
tt('thm/sptree/lookup_def_1', ax, ![A : $t]: (![k : 'type/num/num', a : A]: ((('const/sptree/lookup' A) k (('const/sptree/LS' A) a)) = (('const/bool/COND' ('type/option/option' A)) (k = 'const/num/0') (('const/option/SOME' A) a) ('const/option/NONE' A))))).
tt('thm/sptree/lookup_def_2', ax, ![A : $t]: (![t2 : ('type/sptree/spt' A), t1 : ('type/sptree/spt' A), k : 'type/num/num']: ((('const/sptree/lookup' A) k (('const/sptree/BN' A) t1 t2)) = (('const/bool/COND' ('type/option/option' A)) (k = 'const/num/0') ('const/option/NONE' A) (('const/sptree/lookup' A) ('const/arithmetic/DIV' ('const/arithmetic/-' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) (('const/bool/COND' ('type/sptree/spt' A)) ('const/arithmetic/EVEN' k) t1 t2)))))).
tt('thm/sptree/lookup_def_e3', ax, ![A : $t]: (![t2 : ('type/sptree/spt' A), t1 : ('type/sptree/spt' A), k : 'type/num/num', a : A]: ((('const/sptree/lookup' A) k (('const/sptree/BS' A) t1 a t2)) = (('const/bool/COND' ('type/option/option' A)) (k = 'const/num/0') (('const/option/SOME' A) a) (('const/sptree/lookup' A) ('const/arithmetic/DIV' ('const/arithmetic/-' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) (('const/bool/COND' ('type/sptree/spt' A)) ('const/arithmetic/EVEN' k) t1 t2)))))).
tt('thm/sptree/insert_tupled_primitive_def_', def, ![A : $t]: (('const/sptree/insert_tupled' A) = (('const/relation/WFREC' ('type/pair/prod' 'type/num/num' ('type/pair/prod' A ('type/sptree/spt' A))) ('type/sptree/spt' A)) (('const/min/@' (('type/pair/prod' 'type/num/num' ('type/pair/prod' A ('type/sptree/spt' A))) > (('type/pair/prod' 'type/num/num' ('type/pair/prod' A ('type/sptree/spt' A))) > $o))) (^[R : (('type/pair/prod' 'type/num/num' ('type/pair/prod' A ('type/sptree/spt' A))) > (('type/pair/prod' 'type/num/num' ('type/pair/prod' A ('type/sptree/spt' A))) > $o))]: ((('const/relation/WF' ('type/pair/prod' 'type/num/num' ('type/pair/prod' A ('type/sptree/spt' A)))) R) & ((![a : A, k : 'type/num/num']: (((~ (k = 'const/num/0')) & (~ ('const/arithmetic/EVEN' k))) => (R (('const/pair/,' 'type/num/num' ('type/pair/prod' A ('type/sptree/spt' A))) ('const/arithmetic/DIV' ('const/arithmetic/-' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) (('const/pair/,' A ('type/sptree/spt' A)) a ('const/sptree/LN' A))) (('const/pair/,' 'type/num/num' ('type/pair/prod' A ('type/sptree/spt' A))) k (('const/pair/,' A ('type/sptree/spt' A)) a ('const/sptree/LN' A)))))) & ((![a : A, k : 'type/num/num']: (((~ (k = 'const/num/0')) & ('const/arithmetic/EVEN' k)) => (R (('const/pair/,' 'type/num/num' ('type/pair/prod' A ('type/sptree/spt' A))) ('const/arithmetic/DIV' ('const/arithmetic/-' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) (('const/pair/,' A ('type/sptree/spt' A)) a ('const/sptree/LN' A))) (('const/pair/,' 'type/num/num' ('type/pair/prod' A ('type/sptree/spt' A))) k (('const/pair/,' A ('type/sptree/spt' A)) a ('const/sptree/LN' A)))))) & ((!['a\'' : A, a : A, k : 'type/num/num']: (((~ (k = 'const/num/0')) & (~ ('const/arithmetic/EVEN' k))) => (R (('const/pair/,' 'type/num/num' ('type/pair/prod' A ('type/sptree/spt' A))) ('const/arithmetic/DIV' ('const/arithmetic/-' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) (('const/pair/,' A ('type/sptree/spt' A)) a ('const/sptree/LN' A))) (('const/pair/,' 'type/num/num' ('type/pair/prod' A ('type/sptree/spt' A))) k (('const/pair/,' A ('type/sptree/spt' A)) a (('const/sptree/LS' A) 'a\'')))))) & ((!['a\'' : A, a : A, k : 'type/num/num']: (((~ (k = 'const/num/0')) & ('const/arithmetic/EVEN' k)) => (R (('const/pair/,' 'type/num/num' ('type/pair/prod' A ('type/sptree/spt' A))) ('const/arithmetic/DIV' ('const/arithmetic/-' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) (('const/pair/,' A ('type/sptree/spt' A)) a ('const/sptree/LN' A))) (('const/pair/,' 'type/num/num' ('type/pair/prod' A ('type/sptree/spt' A))) k (('const/pair/,' A ('type/sptree/spt' A)) a (('const/sptree/LS' A) 'a\'')))))) & ((![t1 : ('type/sptree/spt' A), t2 : ('type/sptree/spt' A), a : A, k : 'type/num/num']: (((~ (k = 'const/num/0')) & (~ ('const/arithmetic/EVEN' k))) => (R (('const/pair/,' 'type/num/num' ('type/pair/prod' A ('type/sptree/spt' A))) ('const/arithmetic/DIV' ('const/arithmetic/-' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) (('const/pair/,' A ('type/sptree/spt' A)) a t2)) (('const/pair/,' 'type/num/num' ('type/pair/prod' A ('type/sptree/spt' A))) k (('const/pair/,' A ('type/sptree/spt' A)) a (('const/sptree/BN' A) t1 t2)))))) & ((![t2 : ('type/sptree/spt' A), t1 : ('type/sptree/spt' A), a : A, k : 'type/num/num']: (((~ (k = 'const/num/0')) & ('const/arithmetic/EVEN' k)) => (R (('const/pair/,' 'type/num/num' ('type/pair/prod' A ('type/sptree/spt' A))) ('const/arithmetic/DIV' ('const/arithmetic/-' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) (('const/pair/,' A ('type/sptree/spt' A)) a t1)) (('const/pair/,' 'type/num/num' ('type/pair/prod' A ('type/sptree/spt' A))) k (('const/pair/,' A ('type/sptree/spt' A)) a (('const/sptree/BN' A) t1 t2)))))) & ((![t2 : ('type/sptree/spt' A), 'a\'' : A, t1 : ('type/sptree/spt' A), a : A, k : 'type/num/num']: (((~ (k = 'const/num/0')) & ('const/arithmetic/EVEN' k)) => (R (('const/pair/,' 'type/num/num' ('type/pair/prod' A ('type/sptree/spt' A))) ('const/arithmetic/DIV' ('const/arithmetic/-' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) (('const/pair/,' A ('type/sptree/spt' A)) a t1)) (('const/pair/,' 'type/num/num' ('type/pair/prod' A ('type/sptree/spt' A))) k (('const/pair/,' A ('type/sptree/spt' A)) a (('const/sptree/BS' A) t1 'a\'' t2)))))) & (!['a\'' : A, t1 : ('type/sptree/spt' A), t2 : ('type/sptree/spt' A), a : A, k : 'type/num/num']: (((~ (k = 'const/num/0')) & (~ ('const/arithmetic/EVEN' k))) => (R (('const/pair/,' 'type/num/num' ('type/pair/prod' A ('type/sptree/spt' A))) ('const/arithmetic/DIV' ('const/arithmetic/-' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) (('const/pair/,' A ('type/sptree/spt' A)) a t2)) (('const/pair/,' 'type/num/num' ('type/pair/prod' A ('type/sptree/spt' A))) k (('const/pair/,' A ('type/sptree/spt' A)) a (('const/sptree/BS' A) t1 'a\'' t2)))))))))))))))) (^[insert_tupled : (('type/pair/prod' 'type/num/num' ('type/pair/prod' A ('type/sptree/spt' A))) > ('type/sptree/spt' A)), 'a\'\'' : ('type/pair/prod' 'type/num/num' ('type/pair/prod' A ('type/sptree/spt' A)))]: (('const/pair/pair_CASE' ('type/sptree/spt' A) 'type/num/num' ('type/pair/prod' A ('type/sptree/spt' A))) 'a\'\'' (^[k : 'type/num/num', v1 : ('type/pair/prod' A ('type/sptree/spt' A))]: (('const/pair/pair_CASE' ('type/sptree/spt' A) A ('type/sptree/spt' A)) v1 (^[a : A, v3 : ('type/sptree/spt' A)]: (('const/sptree/spt_CASE' A ('type/sptree/spt' A)) v3 (('const/combin/I' ('type/sptree/spt' A)) (('const/bool/COND' ('type/sptree/spt' A)) (k = 'const/num/0') (('const/sptree/LS' A) a) (('const/bool/COND' ('type/sptree/spt' A)) ('const/arithmetic/EVEN' k) (('const/sptree/BN' A) (insert_tupled (('const/pair/,' 'type/num/num' ('type/pair/prod' A ('type/sptree/spt' A))) ('const/arithmetic/DIV' ('const/arithmetic/-' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) (('const/pair/,' A ('type/sptree/spt' A)) a ('const/sptree/LN' A)))) ('const/sptree/LN' A)) (('const/sptree/BN' A) ('const/sptree/LN' A) (insert_tupled (('const/pair/,' 'type/num/num' ('type/pair/prod' A ('type/sptree/spt' A))) ('const/arithmetic/DIV' ('const/arithmetic/-' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) (('const/pair/,' A ('type/sptree/spt' A)) a ('const/sptree/LN' A)))))))) (^['a\'' : A]: (('const/combin/I' ('type/sptree/spt' A)) (('const/bool/COND' ('type/sptree/spt' A)) (k = 'const/num/0') (('const/sptree/LS' A) a) (('const/bool/COND' ('type/sptree/spt' A)) ('const/arithmetic/EVEN' k) (('const/sptree/BS' A) (insert_tupled (('const/pair/,' 'type/num/num' ('type/pair/prod' A ('type/sptree/spt' A))) ('const/arithmetic/DIV' ('const/arithmetic/-' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) (('const/pair/,' A ('type/sptree/spt' A)) a ('const/sptree/LN' A)))) 'a\'' ('const/sptree/LN' A)) (('const/sptree/BS' A) ('const/sptree/LN' A) 'a\'' (insert_tupled (('const/pair/,' 'type/num/num' ('type/pair/prod' A ('type/sptree/spt' A))) ('const/arithmetic/DIV' ('const/arithmetic/-' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) (('const/pair/,' A ('type/sptree/spt' A)) a ('const/sptree/LN' A))))))))) (^[t1 : ('type/sptree/spt' A), t2 : ('type/sptree/spt' A)]: (('const/combin/I' ('type/sptree/spt' A)) (('const/bool/COND' ('type/sptree/spt' A)) (k = 'const/num/0') (('const/sptree/BS' A) t1 a t2) (('const/bool/COND' ('type/sptree/spt' A)) ('const/arithmetic/EVEN' k) (('const/sptree/BN' A) (insert_tupled (('const/pair/,' 'type/num/num' ('type/pair/prod' A ('type/sptree/spt' A))) ('const/arithmetic/DIV' ('const/arithmetic/-' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) (('const/pair/,' A ('type/sptree/spt' A)) a t1))) t2) (('const/sptree/BN' A) t1 (insert_tupled (('const/pair/,' 'type/num/num' ('type/pair/prod' A ('type/sptree/spt' A))) ('const/arithmetic/DIV' ('const/arithmetic/-' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) (('const/pair/,' A ('type/sptree/spt' A)) a t2)))))))) (^['t1\'' : ('type/sptree/spt' A), 'a\'\'\'' : A, 't2\'' : ('type/sptree/spt' A)]: (('const/combin/I' ('type/sptree/spt' A)) (('const/bool/COND' ('type/sptree/spt' A)) (k = 'const/num/0') (('const/sptree/BS' A) 't1\'' a 't2\'') (('const/bool/COND' ('type/sptree/spt' A)) ('const/arithmetic/EVEN' k) (('const/sptree/BS' A) (insert_tupled (('const/pair/,' 'type/num/num' ('type/pair/prod' A ('type/sptree/spt' A))) ('const/arithmetic/DIV' ('const/arithmetic/-' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) (('const/pair/,' A ('type/sptree/spt' A)) a 't1\''))) 'a\'\'\'' 't2\'') (('const/sptree/BS' A) 't1\'' 'a\'\'\'' (insert_tupled (('const/pair/,' 'type/num/num' ('type/pair/prod' A ('type/sptree/spt' A))) ('const/arithmetic/DIV' ('const/arithmetic/-' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) (('const/pair/,' A ('type/sptree/spt' A)) a 't2\''))))))))))))))))).
tt('thm/sptree/insert_curried_def_', def, ![A : $t]: (![x : 'type/num/num', x1 : A, x2 : ('type/sptree/spt' A)]: ((('const/sptree/insert' A) x x1 x2) = (('const/sptree/insert_tupled' A) (('const/pair/,' 'type/num/num' ('type/pair/prod' A ('type/sptree/spt' A))) x (('const/pair/,' A ('type/sptree/spt' A)) x1 x2)))))).
tt('thm/sptree/insert_ind_', ax, ![A : $t]: (![P : ('type/num/num' > (A > (('type/sptree/spt' A) > $o)))]: (((![k : 'type/num/num', a : A]: (((((~ (k = 'const/num/0')) & ('const/arithmetic/EVEN' k)) => (P ('const/arithmetic/DIV' ('const/arithmetic/-' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) a ('const/sptree/LN' A))) & (((~ (k = 'const/num/0')) & (~ ('const/arithmetic/EVEN' k))) => (P ('const/arithmetic/DIV' ('const/arithmetic/-' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) a ('const/sptree/LN' A)))) => (P k a ('const/sptree/LN' A)))) & ((![k : 'type/num/num', a : A, 'a\'' : A]: (((((~ (k = 'const/num/0')) & ('const/arithmetic/EVEN' k)) => (P ('const/arithmetic/DIV' ('const/arithmetic/-' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) a ('const/sptree/LN' A))) & (((~ (k = 'const/num/0')) & (~ ('const/arithmetic/EVEN' k))) => (P ('const/arithmetic/DIV' ('const/arithmetic/-' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) a ('const/sptree/LN' A)))) => (P k a (('const/sptree/LS' A) 'a\'')))) & ((![k : 'type/num/num', a : A, t1 : ('type/sptree/spt' A), t2 : ('type/sptree/spt' A)]: (((((~ (k = 'const/num/0')) & ('const/arithmetic/EVEN' k)) => (P ('const/arithmetic/DIV' ('const/arithmetic/-' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) a t1)) & (((~ (k = 'const/num/0')) & (~ ('const/arithmetic/EVEN' k))) => (P ('const/arithmetic/DIV' ('const/arithmetic/-' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) a t2))) => (P k a (('const/sptree/BN' A) t1 t2)))) & (![k : 'type/num/num', a : A, t1 : ('type/sptree/spt' A), 'a\'' : A, t2 : ('type/sptree/spt' A)]: (((((~ (k = 'const/num/0')) & ('const/arithmetic/EVEN' k)) => (P ('const/arithmetic/DIV' ('const/arithmetic/-' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) a t1)) & (((~ (k = 'const/num/0')) & (~ ('const/arithmetic/EVEN' k))) => (P ('const/arithmetic/DIV' ('const/arithmetic/-' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) a t2))) => (P k a (('const/sptree/BS' A) t1 'a\'' t2))))))) => (![v : 'type/num/num', v1 : A, v2 : ('type/sptree/spt' A)]: (P v v1 v2))))).
tt('thm/sptree/insert_def_0', ax, ![A : $t]: (![k : 'type/num/num', a : A]: ((('const/sptree/insert' A) k a ('const/sptree/LN' A)) = (('const/bool/COND' ('type/sptree/spt' A)) (k = 'const/num/0') (('const/sptree/LS' A) a) (('const/bool/COND' ('type/sptree/spt' A)) ('const/arithmetic/EVEN' k) (('const/sptree/BN' A) (('const/sptree/insert' A) ('const/arithmetic/DIV' ('const/arithmetic/-' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) a ('const/sptree/LN' A)) ('const/sptree/LN' A)) (('const/sptree/BN' A) ('const/sptree/LN' A) (('const/sptree/insert' A) ('const/arithmetic/DIV' ('const/arithmetic/-' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) a ('const/sptree/LN' A)))))))).
tt('thm/sptree/insert_def_1', ax, ![A : $t]: (![k : 'type/num/num', 'a\'' : A, a : A]: ((('const/sptree/insert' A) k a (('const/sptree/LS' A) 'a\'')) = (('const/bool/COND' ('type/sptree/spt' A)) (k = 'const/num/0') (('const/sptree/LS' A) a) (('const/bool/COND' ('type/sptree/spt' A)) ('const/arithmetic/EVEN' k) (('const/sptree/BS' A) (('const/sptree/insert' A) ('const/arithmetic/DIV' ('const/arithmetic/-' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) a ('const/sptree/LN' A)) 'a\'' ('const/sptree/LN' A)) (('const/sptree/BS' A) ('const/sptree/LN' A) 'a\'' (('const/sptree/insert' A) ('const/arithmetic/DIV' ('const/arithmetic/-' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) a ('const/sptree/LN' A)))))))).
tt('thm/sptree/insert_def_2', ax, ![A : $t]: (![t2 : ('type/sptree/spt' A), t1 : ('type/sptree/spt' A), k : 'type/num/num', a : A]: ((('const/sptree/insert' A) k a (('const/sptree/BN' A) t1 t2)) = (('const/bool/COND' ('type/sptree/spt' A)) (k = 'const/num/0') (('const/sptree/BS' A) t1 a t2) (('const/bool/COND' ('type/sptree/spt' A)) ('const/arithmetic/EVEN' k) (('const/sptree/BN' A) (('const/sptree/insert' A) ('const/arithmetic/DIV' ('const/arithmetic/-' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) a t1) t2) (('const/sptree/BN' A) t1 (('const/sptree/insert' A) ('const/arithmetic/DIV' ('const/arithmetic/-' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) a t2))))))).
tt('thm/sptree/insert_def_e3', ax, ![A : $t]: (![t2 : ('type/sptree/spt' A), t1 : ('type/sptree/spt' A), k : 'type/num/num', 'a\'' : A, a : A]: ((('const/sptree/insert' A) k a (('const/sptree/BS' A) t1 'a\'' t2)) = (('const/bool/COND' ('type/sptree/spt' A)) (k = 'const/num/0') (('const/sptree/BS' A) t1 a t2) (('const/bool/COND' ('type/sptree/spt' A)) ('const/arithmetic/EVEN' k) (('const/sptree/BS' A) (('const/sptree/insert' A) ('const/arithmetic/DIV' ('const/arithmetic/-' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) a t1) 'a\'' t2) (('const/sptree/BS' A) t1 'a\'' (('const/sptree/insert' A) ('const/arithmetic/DIV' ('const/arithmetic/-' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) a t2))))))).
tt('thm/sptree/mk_BN_tupled_primitive_def_', def, ![A : $t]: (('const/sptree/mk_BN_tupled' A) = (('const/relation/WFREC' ('type/pair/prod' ('type/sptree/spt' A) ('type/sptree/spt' A)) ('type/sptree/spt' A)) (('const/min/@' (('type/pair/prod' ('type/sptree/spt' A) ('type/sptree/spt' A)) > (('type/pair/prod' ('type/sptree/spt' A) ('type/sptree/spt' A)) > $o))) (^[R : (('type/pair/prod' ('type/sptree/spt' A) ('type/sptree/spt' A)) > (('type/pair/prod' ('type/sptree/spt' A) ('type/sptree/spt' A)) > $o))]: (('const/relation/WF' ('type/pair/prod' ('type/sptree/spt' A) ('type/sptree/spt' A))) R))) (^[mk_BN_tupled : (('type/pair/prod' ('type/sptree/spt' A) ('type/sptree/spt' A)) > ('type/sptree/spt' A)), a : ('type/pair/prod' ('type/sptree/spt' A) ('type/sptree/spt' A))]: (('const/pair/pair_CASE' ('type/sptree/spt' A) ('type/sptree/spt' A) ('type/sptree/spt' A)) a (^[v : ('type/sptree/spt' A), v1 : ('type/sptree/spt' A)]: (('const/sptree/spt_CASE' A ('type/sptree/spt' A)) v (('const/sptree/spt_CASE' A ('type/sptree/spt' A)) v1 (('const/combin/I' ('type/sptree/spt' A)) ('const/sptree/LN' A)) (^[v20 : A]: (('const/combin/I' ('type/sptree/spt' A)) (('const/sptree/BN' A) ('const/sptree/LN' A) (('const/sptree/LS' A) v20)))) (^[v21 : ('type/sptree/spt' A), v22 : ('type/sptree/spt' A)]: (('const/combin/I' ('type/sptree/spt' A)) (('const/sptree/BN' A) ('const/sptree/LN' A) (('const/sptree/BN' A) v21 v22)))) (^[v23 : ('type/sptree/spt' A), v24 : A, v25 : ('type/sptree/spt' A)]: (('const/combin/I' ('type/sptree/spt' A)) (('const/sptree/BN' A) ('const/sptree/LN' A) (('const/sptree/BS' A) v23 v24 v25))))) (^[v8 : A]: (('const/combin/I' ('type/sptree/spt' A)) (('const/sptree/BN' A) (('const/sptree/LS' A) v8) v1))) (^[v9 : ('type/sptree/spt' A), v10 : ('type/sptree/spt' A)]: (('const/combin/I' ('type/sptree/spt' A)) (('const/sptree/BN' A) (('const/sptree/BN' A) v9 v10) v1))) (^[v11 : ('type/sptree/spt' A), v12 : A, v13 : ('type/sptree/spt' A)]: (('const/combin/I' ('type/sptree/spt' A)) (('const/sptree/BN' A) (('const/sptree/BS' A) v11 v12 v13) v1)))))))))).
tt('thm/sptree/mk_BN_curried_def_', def, ![A : $t]: (![x : ('type/sptree/spt' A), x1 : ('type/sptree/spt' A)]: ((('const/sptree/mk_BN' A) x x1) = (('const/sptree/mk_BN_tupled' A) (('const/pair/,' ('type/sptree/spt' A) ('type/sptree/spt' A)) x x1))))).
tt('thm/sptree/mk_BN_ind_', ax, ![A : $t]: (![P : (('type/sptree/spt' A) > (('type/sptree/spt' A) > $o))]: (((P ('const/sptree/LN' A) ('const/sptree/LN' A)) & ((![v14 : A]: (P ('const/sptree/LN' A) (('const/sptree/LS' A) v14))) & ((![v15 : ('type/sptree/spt' A), v16 : ('type/sptree/spt' A)]: (P ('const/sptree/LN' A) (('const/sptree/BN' A) v15 v16))) & ((![v17 : ('type/sptree/spt' A), v18 : A, v19 : ('type/sptree/spt' A)]: (P ('const/sptree/LN' A) (('const/sptree/BS' A) v17 v18 v19))) & ((![v2 : A, t2 : ('type/sptree/spt' A)]: (P (('const/sptree/LS' A) v2) t2)) & ((![v3 : ('type/sptree/spt' A), v4 : ('type/sptree/spt' A), t2 : ('type/sptree/spt' A)]: (P (('const/sptree/BN' A) v3 v4) t2)) & (![v5 : ('type/sptree/spt' A), v6 : A, v7 : ('type/sptree/spt' A), t2 : ('type/sptree/spt' A)]: (P (('const/sptree/BS' A) v5 v6 v7) t2)))))))) => (![v : ('type/sptree/spt' A), v1 : ('type/sptree/spt' A)]: (P v v1))))).
tt('thm/sptree/mk_BN_def_0', ax, ![A : $t]: ((('const/sptree/mk_BN' A) ('const/sptree/LN' A) ('const/sptree/LN' A)) = ('const/sptree/LN' A))).
tt('thm/sptree/mk_BN_def_1', ax, ![A : $t]: (![v14 : A]: ((('const/sptree/mk_BN' A) ('const/sptree/LN' A) (('const/sptree/LS' A) v14)) = (('const/sptree/BN' A) ('const/sptree/LN' A) (('const/sptree/LS' A) v14))))).
tt('thm/sptree/mk_BN_def_2', ax, ![A : $t]: (![v16 : ('type/sptree/spt' A), v15 : ('type/sptree/spt' A)]: ((('const/sptree/mk_BN' A) ('const/sptree/LN' A) (('const/sptree/BN' A) v15 v16)) = (('const/sptree/BN' A) ('const/sptree/LN' A) (('const/sptree/BN' A) v15 v16))))).
tt('thm/sptree/mk_BN_def_3', ax, ![A : $t]: (![v19 : ('type/sptree/spt' A), v18 : A, v17 : ('type/sptree/spt' A)]: ((('const/sptree/mk_BN' A) ('const/sptree/LN' A) (('const/sptree/BS' A) v17 v18 v19)) = (('const/sptree/BN' A) ('const/sptree/LN' A) (('const/sptree/BS' A) v17 v18 v19))))).
tt('thm/sptree/mk_BN_def_4', ax, ![A : $t]: (![v2 : A, t2 : ('type/sptree/spt' A)]: ((('const/sptree/mk_BN' A) (('const/sptree/LS' A) v2) t2) = (('const/sptree/BN' A) (('const/sptree/LS' A) v2) t2)))).
tt('thm/sptree/mk_BN_def_5', ax, ![A : $t]: (![v4 : ('type/sptree/spt' A), v3 : ('type/sptree/spt' A), t2 : ('type/sptree/spt' A)]: ((('const/sptree/mk_BN' A) (('const/sptree/BN' A) v3 v4) t2) = (('const/sptree/BN' A) (('const/sptree/BN' A) v3 v4) t2)))).
tt('thm/sptree/mk_BN_def_e6', ax, ![A : $t]: (![v7 : ('type/sptree/spt' A), v6 : A, v5 : ('type/sptree/spt' A), t2 : ('type/sptree/spt' A)]: ((('const/sptree/mk_BN' A) (('const/sptree/BS' A) v5 v6 v7) t2) = (('const/sptree/BN' A) (('const/sptree/BS' A) v5 v6 v7) t2)))).
tt('thm/sptree/mk_BS_tupled_primitive_def_', def, ![A : $t]: (('const/sptree/mk_BS_tupled' A) = (('const/relation/WFREC' ('type/pair/prod' ('type/sptree/spt' A) ('type/pair/prod' A ('type/sptree/spt' A))) ('type/sptree/spt' A)) (('const/min/@' (('type/pair/prod' ('type/sptree/spt' A) ('type/pair/prod' A ('type/sptree/spt' A))) > (('type/pair/prod' ('type/sptree/spt' A) ('type/pair/prod' A ('type/sptree/spt' A))) > $o))) (^[R : (('type/pair/prod' ('type/sptree/spt' A) ('type/pair/prod' A ('type/sptree/spt' A))) > (('type/pair/prod' ('type/sptree/spt' A) ('type/pair/prod' A ('type/sptree/spt' A))) > $o))]: (('const/relation/WF' ('type/pair/prod' ('type/sptree/spt' A) ('type/pair/prod' A ('type/sptree/spt' A)))) R))) (^[mk_BS_tupled : (('type/pair/prod' ('type/sptree/spt' A) ('type/pair/prod' A ('type/sptree/spt' A))) > ('type/sptree/spt' A)), a : ('type/pair/prod' ('type/sptree/spt' A) ('type/pair/prod' A ('type/sptree/spt' A)))]: (('const/pair/pair_CASE' ('type/sptree/spt' A) ('type/sptree/spt' A) ('type/pair/prod' A ('type/sptree/spt' A))) a (^[v : ('type/sptree/spt' A), v1 : ('type/pair/prod' A ('type/sptree/spt' A))]: (('const/pair/pair_CASE' ('type/sptree/spt' A) A ('type/sptree/spt' A)) v1 (^[x : A, v3 : ('type/sptree/spt' A)]: (('const/sptree/spt_CASE' A ('type/sptree/spt' A)) v3 (('const/sptree/spt_CASE' A ('type/sptree/spt' A)) v (('const/combin/I' ('type/sptree/spt' A)) (('const/sptree/LS' A) x)) (^[v22 : A]: (('const/combin/I' ('type/sptree/spt' A)) (('const/sptree/BS' A) (('const/sptree/LS' A) v22) x ('const/sptree/LN' A)))) (^[v23 : ('type/sptree/spt' A), v24 : ('type/sptree/spt' A)]: (('const/combin/I' ('type/sptree/spt' A)) (('const/sptree/BS' A) (('const/sptree/BN' A) v23 v24) x ('const/sptree/LN' A)))) (^[v25 : ('type/sptree/spt' A), v26 : A, v27 : ('type/sptree/spt' A)]: (('const/combin/I' ('type/sptree/spt' A)) (('const/sptree/BS' A) (('const/sptree/BS' A) v25 v26 v27) x ('const/sptree/LN' A))))) (^[v10 : A]: (('const/combin/I' ('type/sptree/spt' A)) (('const/sptree/BS' A) v x (('const/sptree/LS' A) v10)))) (^[v11 : ('type/sptree/spt' A), v12 : ('type/sptree/spt' A)]: (('const/combin/I' ('type/sptree/spt' A)) (('const/sptree/BS' A) v x (('const/sptree/BN' A) v11 v12)))) (^[v13 : ('type/sptree/spt' A), v14 : A, v15 : ('type/sptree/spt' A)]: (('const/combin/I' ('type/sptree/spt' A)) (('const/sptree/BS' A) v x (('const/sptree/BS' A) v13 v14 v15))))))))))))).
tt('thm/sptree/mk_BS_curried_def_', def, ![A : $t]: (![x : ('type/sptree/spt' A), x1 : A, x2 : ('type/sptree/spt' A)]: ((('const/sptree/mk_BS' A) x x1 x2) = (('const/sptree/mk_BS_tupled' A) (('const/pair/,' ('type/sptree/spt' A) ('type/pair/prod' A ('type/sptree/spt' A))) x (('const/pair/,' A ('type/sptree/spt' A)) x1 x2)))))).
tt('thm/sptree/mk_BS_ind_', ax, ![A : $t]: (![P : (('type/sptree/spt' A) > (A > (('type/sptree/spt' A) > $o)))]: (((![x : A]: (P ('const/sptree/LN' A) x ('const/sptree/LN' A))) & ((![v16 : A, x : A]: (P (('const/sptree/LS' A) v16) x ('const/sptree/LN' A))) & ((![v17 : ('type/sptree/spt' A), v18 : ('type/sptree/spt' A), x : A]: (P (('const/sptree/BN' A) v17 v18) x ('const/sptree/LN' A))) & ((![v19 : ('type/sptree/spt' A), v20 : A, v21 : ('type/sptree/spt' A), x : A]: (P (('const/sptree/BS' A) v19 v20 v21) x ('const/sptree/LN' A))) & ((![t1 : ('type/sptree/spt' A), x : A, v4 : A]: (P t1 x (('const/sptree/LS' A) v4))) & ((![t1 : ('type/sptree/spt' A), x : A, v5 : ('type/sptree/spt' A), v6 : ('type/sptree/spt' A)]: (P t1 x (('const/sptree/BN' A) v5 v6))) & (![t1 : ('type/sptree/spt' A), x : A, v7 : ('type/sptree/spt' A), v8 : A, v9 : ('type/sptree/spt' A)]: (P t1 x (('const/sptree/BS' A) v7 v8 v9))))))))) => (![v : ('type/sptree/spt' A), v1 : A, v2 : ('type/sptree/spt' A)]: (P v v1 v2))))).
tt('thm/sptree/mk_BS_def_0', ax, ![A : $t]: (![x : A]: ((('const/sptree/mk_BS' A) ('const/sptree/LN' A) x ('const/sptree/LN' A)) = (('const/sptree/LS' A) x)))).
tt('thm/sptree/mk_BS_def_1', ax, ![A : $t]: (![x : A, v16 : A]: ((('const/sptree/mk_BS' A) (('const/sptree/LS' A) v16) x ('const/sptree/LN' A)) = (('const/sptree/BS' A) (('const/sptree/LS' A) v16) x ('const/sptree/LN' A))))).
tt('thm/sptree/mk_BS_def_2', ax, ![A : $t]: (![x : A, v18 : ('type/sptree/spt' A), v17 : ('type/sptree/spt' A)]: ((('const/sptree/mk_BS' A) (('const/sptree/BN' A) v17 v18) x ('const/sptree/LN' A)) = (('const/sptree/BS' A) (('const/sptree/BN' A) v17 v18) x ('const/sptree/LN' A))))).
tt('thm/sptree/mk_BS_def_3', ax, ![A : $t]: (![x : A, v21 : ('type/sptree/spt' A), v20 : A, v19 : ('type/sptree/spt' A)]: ((('const/sptree/mk_BS' A) (('const/sptree/BS' A) v19 v20 v21) x ('const/sptree/LN' A)) = (('const/sptree/BS' A) (('const/sptree/BS' A) v19 v20 v21) x ('const/sptree/LN' A))))).
tt('thm/sptree/mk_BS_def_4', ax, ![A : $t]: (![x : A, v4 : A, t1 : ('type/sptree/spt' A)]: ((('const/sptree/mk_BS' A) t1 x (('const/sptree/LS' A) v4)) = (('const/sptree/BS' A) t1 x (('const/sptree/LS' A) v4))))).
tt('thm/sptree/mk_BS_def_5', ax, ![A : $t]: (![x : A, v6 : ('type/sptree/spt' A), v5 : ('type/sptree/spt' A), t1 : ('type/sptree/spt' A)]: ((('const/sptree/mk_BS' A) t1 x (('const/sptree/BN' A) v5 v6)) = (('const/sptree/BS' A) t1 x (('const/sptree/BN' A) v5 v6))))).
tt('thm/sptree/mk_BS_def_e6', ax, ![A : $t]: (![x : A, v9 : ('type/sptree/spt' A), v8 : A, v7 : ('type/sptree/spt' A), t1 : ('type/sptree/spt' A)]: ((('const/sptree/mk_BS' A) t1 x (('const/sptree/BS' A) v7 v8 v9)) = (('const/sptree/BS' A) t1 x (('const/sptree/BS' A) v7 v8 v9))))).
tt('thm/sptree/delete_def_0', def, ![A : $t]: (![k : 'type/num/num']: ((('const/sptree/delete' A) k ('const/sptree/LN' A)) = ('const/sptree/LN' A)))).
tt('thm/sptree/delete_def_1', def, ![A : $t]: (![k : 'type/num/num', a : A]: ((('const/sptree/delete' A) k (('const/sptree/LS' A) a)) = (('const/bool/COND' ('type/sptree/spt' A)) (k = 'const/num/0') ('const/sptree/LN' A) (('const/sptree/LS' A) a))))).
tt('thm/sptree/delete_def_2', def, ![A : $t]: (![k : 'type/num/num', t1 : ('type/sptree/spt' A), t2 : ('type/sptree/spt' A)]: ((('const/sptree/delete' A) k (('const/sptree/BN' A) t1 t2)) = (('const/bool/COND' ('type/sptree/spt' A)) (k = 'const/num/0') (('const/sptree/BN' A) t1 t2) (('const/bool/COND' ('type/sptree/spt' A)) ('const/arithmetic/EVEN' k) (('const/sptree/mk_BN' A) (('const/sptree/delete' A) ('const/arithmetic/DIV' ('const/arithmetic/-' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) t1) t2) (('const/sptree/mk_BN' A) t1 (('const/sptree/delete' A) ('const/arithmetic/DIV' ('const/arithmetic/-' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) t2))))))).
tt('thm/sptree/delete_def_e3', def, ![A : $t]: (![k : 'type/num/num', t1 : ('type/sptree/spt' A), a : A, t2 : ('type/sptree/spt' A)]: ((('const/sptree/delete' A) k (('const/sptree/BS' A) t1 a t2)) = (('const/bool/COND' ('type/sptree/spt' A)) (k = 'const/num/0') (('const/sptree/BN' A) t1 t2) (('const/bool/COND' ('type/sptree/spt' A)) ('const/arithmetic/EVEN' k) (('const/sptree/mk_BS' A) (('const/sptree/delete' A) ('const/arithmetic/DIV' ('const/arithmetic/-' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) t1) a t2) (('const/sptree/mk_BS' A) t1 a (('const/sptree/delete' A) ('const/arithmetic/DIV' ('const/arithmetic/-' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) t2))))))).
tt('thm/sptree/fromList_def_', def, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/sptree/fromList' A) l) = (('const/pair/SND' 'type/num/num' ('type/sptree/spt' A)) (('const/list/FOLDL' A ('type/pair/prod' 'type/num/num' ('type/sptree/spt' A))) (('const/pair/UNCURRY' 'type/num/num' ('type/sptree/spt' A) (A > ('type/pair/prod' 'type/num/num' ('type/sptree/spt' A)))) (^[i : 'type/num/num', t : ('type/sptree/spt' A), a : A]: (('const/pair/,' 'type/num/num' ('type/sptree/spt' A)) ('const/arithmetic/+' i ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) (('const/sptree/insert' A) i a t)))) (('const/pair/,' 'type/num/num' ('type/sptree/spt' A)) 'const/num/0' ('const/sptree/LN' A)) l))))).
tt('thm/sptree/size_def_0', def, ![A : $t]: ((('const/sptree/size' A) ('const/sptree/LN' A)) = 'const/num/0')).
tt('thm/sptree/size_def_1', def, ![A : $t]: (![a : A]: ((('const/sptree/size' A) (('const/sptree/LS' A) a)) = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/sptree/size_def_2', def, ![A : $t]: (![t1 : ('type/sptree/spt' A), t2 : ('type/sptree/spt' A)]: ((('const/sptree/size' A) (('const/sptree/BN' A) t1 t2)) = ('const/arithmetic/+' (('const/sptree/size' A) t1) (('const/sptree/size' A) t2))))).
tt('thm/sptree/size_def_e3', def, ![A : $t]: (![t1 : ('type/sptree/spt' A), a : A, t2 : ('type/sptree/spt' A)]: ((('const/sptree/size' A) (('const/sptree/BS' A) t1 a t2)) = ('const/arithmetic/+' ('const/arithmetic/+' (('const/sptree/size' A) t1) (('const/sptree/size' A) t2)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
tt('thm/sptree/insert_notEmpty_', ax, ![A : $t]: (![t : ('type/sptree/spt' A), k : 'type/num/num', a : A]: (~ ((('const/sptree/insert' A) k a t) = ('const/sptree/LN' A))))).
tt('thm/sptree/wf_insert_', ax, ![A : $t]: (![k : 'type/num/num', a : A, t : ('type/sptree/spt' A)]: ((('const/sptree/wf' A) t) => (('const/sptree/wf' A) (('const/sptree/insert' A) k a t))))).
tt('thm/sptree/wf_delete_', ax, ![A : $t]: (![t : ('type/sptree/spt' A), k : 'type/num/num']: ((('const/sptree/wf' A) t) => (('const/sptree/wf' A) (('const/sptree/delete' A) k t))))).
tt('thm/sptree/lookup_insert1_', ax, ![A : $t]: (![k : 'type/num/num', a : A, t : ('type/sptree/spt' A)]: ((('const/sptree/lookup' A) k (('const/sptree/insert' A) k a t)) = (('const/option/SOME' A) a)))).
tt('thm/sptree/lookup_insert_', ax, ![A : $t]: (![k2 : 'type/num/num', v : A, t : ('type/sptree/spt' A), k1 : 'type/num/num']: ((('const/sptree/lookup' A) k1 (('const/sptree/insert' A) k2 v t)) = (('const/bool/COND' ('type/option/option' A)) (k1 = k2) (('const/option/SOME' A) v) (('const/sptree/lookup' A) k1 t))))).
tt('thm/sptree/union_def_0', def, ![A : $t]: (![t : ('type/sptree/spt' A)]: ((('const/sptree/union' A) ('const/sptree/LN' A) t) = t))).
tt('thm/sptree/union_def_1', def, ![A : $t]: (![a : A, t : ('type/sptree/spt' A)]: ((('const/sptree/union' A) (('const/sptree/LS' A) a) t) = (('const/sptree/spt_CASE' A ('type/sptree/spt' A)) t (('const/sptree/LS' A) a) (^[b : A]: (('const/sptree/LS' A) a)) (^[t1 : ('type/sptree/spt' A), t2 : ('type/sptree/spt' A)]: (('const/sptree/BS' A) t1 a t2)) (^['t1\'' : ('type/sptree/spt' A), v4 : A, 't2\'' : ('type/sptree/spt' A)]: (('const/sptree/BS' A) 't1\'' a 't2\'')))))).
tt('thm/sptree/union_def_2', def, ![A : $t]: (![t1 : ('type/sptree/spt' A), t2 : ('type/sptree/spt' A), t : ('type/sptree/spt' A)]: ((('const/sptree/union' A) (('const/sptree/BN' A) t1 t2) t) = (('const/sptree/spt_CASE' A ('type/sptree/spt' A)) t (('const/sptree/BN' A) t1 t2) (^[a : A]: (('const/sptree/BS' A) t1 a t2)) (^['t1\'' : ('type/sptree/spt' A), 't2\'' : ('type/sptree/spt' A)]: (('const/sptree/BN' A) (('const/sptree/union' A) t1 't1\'') (('const/sptree/union' A) t2 't2\''))) (^['t1\'\'' : ('type/sptree/spt' A), 'a\'\'' : A, 't2\'\'' : ('type/sptree/spt' A)]: (('const/sptree/BS' A) (('const/sptree/union' A) t1 't1\'\'') 'a\'\'' (('const/sptree/union' A) t2 't2\'\''))))))).
tt('thm/sptree/union_def_e3', def, ![A : $t]: (![t1 : ('type/sptree/spt' A), a : A, t2 : ('type/sptree/spt' A), t : ('type/sptree/spt' A)]: ((('const/sptree/union' A) (('const/sptree/BS' A) t1 a t2) t) = (('const/sptree/spt_CASE' A ('type/sptree/spt' A)) t (('const/sptree/BS' A) t1 a t2) (^['a\'' : A]: (('const/sptree/BS' A) t1 a t2)) (^['t1\'' : ('type/sptree/spt' A), 't2\'' : ('type/sptree/spt' A)]: (('const/sptree/BS' A) (('const/sptree/union' A) t1 't1\'') a (('const/sptree/union' A) t2 't2\''))) (^['t1\'\'' : ('type/sptree/spt' A), 'a\'\'\'' : A, 't2\'\'' : ('type/sptree/spt' A)]: (('const/sptree/BS' A) (('const/sptree/union' A) t1 't1\'\'') a (('const/sptree/union' A) t2 't2\'\''))))))).
tt('thm/sptree/isEmpty_union_', ax, ![A : $t]: (![m2 : ('type/sptree/spt' A), m1 : ('type/sptree/spt' A)]: (((('const/sptree/union' A) m1 m2) = ('const/sptree/LN' A)) = ((m1 = ('const/sptree/LN' A)) & (m2 = ('const/sptree/LN' A)))))).
tt('thm/sptree/wf_union_', ax, ![A : $t]: (![m1 : ('type/sptree/spt' A), m2 : ('type/sptree/spt' A)]: (((('const/sptree/wf' A) m1) & (('const/sptree/wf' A) m2)) => (('const/sptree/wf' A) (('const/sptree/union' A) m1 m2))))).
tt('thm/sptree/lookup_union_', ax, ![A : $t]: (![m1 : ('type/sptree/spt' A), m2 : ('type/sptree/spt' A), k : 'type/num/num']: ((('const/sptree/lookup' A) k (('const/sptree/union' A) m1 m2)) = (('const/option/option_CASE' A ('type/option/option' A)) (('const/sptree/lookup' A) k m1) (('const/sptree/lookup' A) k m2) (^[v : A]: (('const/option/SOME' A) v)))))).
tt('thm/sptree/inter_def_0', def, ![A : $t, B : $t]: (![t : ('type/sptree/spt' B)]: ((('const/sptree/inter' A B) ('const/sptree/LN' A) t) = ('const/sptree/LN' A)))).
tt('thm/sptree/inter_def_1', def, ![A : $t, B : $t]: (![a : A, t : ('type/sptree/spt' B)]: ((('const/sptree/inter' A B) (('const/sptree/LS' A) a) t) = (('const/sptree/spt_CASE' B ('type/sptree/spt' A)) t ('const/sptree/LN' A) (^[b : B]: (('const/sptree/LS' A) a)) (^[t1 : ('type/sptree/spt' B), t2 : ('type/sptree/spt' B)]: ('const/sptree/LN' A)) (^['t1\'' : ('type/sptree/spt' B), v4 : B, 't2\'' : ('type/sptree/spt' B)]: (('const/sptree/LS' A) a)))))).
tt('thm/sptree/inter_def_2', def, ![B : $t, A : $t]: (![t1 : ('type/sptree/spt' A), t2 : ('type/sptree/spt' A), t : ('type/sptree/spt' B)]: ((('const/sptree/inter' A B) (('const/sptree/BN' A) t1 t2) t) = (('const/sptree/spt_CASE' B ('type/sptree/spt' A)) t ('const/sptree/LN' A) (^[a : B]: ('const/sptree/LN' A)) (^['t1\'' : ('type/sptree/spt' B), 't2\'' : ('type/sptree/spt' B)]: (('const/sptree/mk_BN' A) (('const/sptree/inter' A B) t1 't1\'') (('const/sptree/inter' A B) t2 't2\''))) (^['t1\'\'' : ('type/sptree/spt' B), 'a\'\'' : B, 't2\'\'' : ('type/sptree/spt' B)]: (('const/sptree/mk_BN' A) (('const/sptree/inter' A B) t1 't1\'\'') (('const/sptree/inter' A B) t2 't2\'\''))))))).
tt('thm/sptree/inter_def_e3', def, ![B : $t, A : $t]: (![t1 : ('type/sptree/spt' A), a : A, t2 : ('type/sptree/spt' A), t : ('type/sptree/spt' B)]: ((('const/sptree/inter' A B) (('const/sptree/BS' A) t1 a t2) t) = (('const/sptree/spt_CASE' B ('type/sptree/spt' A)) t ('const/sptree/LN' A) (^['a\'' : B]: (('const/sptree/LS' A) a)) (^['t1\'' : ('type/sptree/spt' B), 't2\'' : ('type/sptree/spt' B)]: (('const/sptree/mk_BN' A) (('const/sptree/inter' A B) t1 't1\'') (('const/sptree/inter' A B) t2 't2\''))) (^['t1\'\'' : ('type/sptree/spt' B), 'a\'\'\'' : B, 't2\'\'' : ('type/sptree/spt' B)]: (('const/sptree/mk_BS' A) (('const/sptree/inter' A B) t1 't1\'\'') a (('const/sptree/inter' A B) t2 't2\'\''))))))).
tt('thm/sptree/inter_eq_def_0', def, ![A : $t]: (![t : ('type/sptree/spt' A)]: ((('const/sptree/inter_eq' A) ('const/sptree/LN' A) t) = ('const/sptree/LN' A)))).
tt('thm/sptree/inter_eq_def_1', def, ![A : $t]: (![a : A, t : ('type/sptree/spt' A)]: ((('const/sptree/inter_eq' A) (('const/sptree/LS' A) a) t) = (('const/sptree/spt_CASE' A ('type/sptree/spt' A)) t ('const/sptree/LN' A) (^[b : A]: (('const/bool/COND' ('type/sptree/spt' A)) (a = b) (('const/sptree/LS' A) a) ('const/sptree/LN' A))) (^[t1 : ('type/sptree/spt' A), t2 : ('type/sptree/spt' A)]: ('const/sptree/LN' A)) (^['t1\'' : ('type/sptree/spt' A), 'b\'' : A, 't2\'' : ('type/sptree/spt' A)]: (('const/bool/COND' ('type/sptree/spt' A)) (a = 'b\'') (('const/sptree/LS' A) a) ('const/sptree/LN' A))))))).
tt('thm/sptree/inter_eq_def_2', def, ![A : $t]: (![t1 : ('type/sptree/spt' A), t2 : ('type/sptree/spt' A), t : ('type/sptree/spt' A)]: ((('const/sptree/inter_eq' A) (('const/sptree/BN' A) t1 t2) t) = (('const/sptree/spt_CASE' A ('type/sptree/spt' A)) t ('const/sptree/LN' A) (^[a : A]: ('const/sptree/LN' A)) (^['t1\'' : ('type/sptree/spt' A), 't2\'' : ('type/sptree/spt' A)]: (('const/sptree/mk_BN' A) (('const/sptree/inter_eq' A) t1 't1\'') (('const/sptree/inter_eq' A) t2 't2\''))) (^['t1\'\'' : ('type/sptree/spt' A), 'a\'\'' : A, 't2\'\'' : ('type/sptree/spt' A)]: (('const/sptree/mk_BN' A) (('const/sptree/inter_eq' A) t1 't1\'\'') (('const/sptree/inter_eq' A) t2 't2\'\''))))))).
tt('thm/sptree/inter_eq_def_e3', def, ![A : $t]: (![t1 : ('type/sptree/spt' A), a : A, t2 : ('type/sptree/spt' A), t : ('type/sptree/spt' A)]: ((('const/sptree/inter_eq' A) (('const/sptree/BS' A) t1 a t2) t) = (('const/sptree/spt_CASE' A ('type/sptree/spt' A)) t ('const/sptree/LN' A) (^['a\'' : A]: (('const/bool/COND' ('type/sptree/spt' A)) ('a\'' = a) (('const/sptree/LS' A) a) ('const/sptree/LN' A))) (^['t1\'' : ('type/sptree/spt' A), 't2\'' : ('type/sptree/spt' A)]: (('const/sptree/mk_BN' A) (('const/sptree/inter_eq' A) t1 't1\'') (('const/sptree/inter_eq' A) t2 't2\''))) (^['t1\'\'' : ('type/sptree/spt' A), 'a\'\'\'' : A, 't2\'\'' : ('type/sptree/spt' A)]: (('const/bool/COND' ('type/sptree/spt' A)) ('a\'\'\'' = a) (('const/sptree/mk_BS' A) (('const/sptree/inter_eq' A) t1 't1\'\'') a (('const/sptree/inter_eq' A) t2 't2\'\'')) (('const/sptree/mk_BN' A) (('const/sptree/inter_eq' A) t1 't1\'\'') (('const/sptree/inter_eq' A) t2 't2\'\'')))))))).
tt('thm/sptree/difference_def_0', def, ![A : $t, B : $t]: (![t : ('type/sptree/spt' B)]: ((('const/sptree/difference' A B) ('const/sptree/LN' A) t) = ('const/sptree/LN' A)))).
tt('thm/sptree/difference_def_1', def, ![A : $t, B : $t]: (![a : A, t : ('type/sptree/spt' B)]: ((('const/sptree/difference' A B) (('const/sptree/LS' A) a) t) = (('const/sptree/spt_CASE' B ('type/sptree/spt' A)) t (('const/sptree/LS' A) a) (^[b : B]: ('const/sptree/LN' A)) (^[t1 : ('type/sptree/spt' B), t2 : ('type/sptree/spt' B)]: (('const/sptree/LS' A) a)) (^['t1\'' : ('type/sptree/spt' B), 'b\'' : B, 't2\'' : ('type/sptree/spt' B)]: ('const/sptree/LN' A)))))).
tt('thm/sptree/difference_def_2', def, ![B : $t, A : $t]: (![t1 : ('type/sptree/spt' A), t2 : ('type/sptree/spt' A), t : ('type/sptree/spt' B)]: ((('const/sptree/difference' A B) (('const/sptree/BN' A) t1 t2) t) = (('const/sptree/spt_CASE' B ('type/sptree/spt' A)) t (('const/sptree/BN' A) t1 t2) (^[a : B]: (('const/sptree/BN' A) t1 t2)) (^['t1\'' : ('type/sptree/spt' B), 't2\'' : ('type/sptree/spt' B)]: (('const/sptree/mk_BN' A) (('const/sptree/difference' A B) t1 't1\'') (('const/sptree/difference' A B) t2 't2\''))) (^['t1\'\'' : ('type/sptree/spt' B), 'a\'\'' : B, 't2\'\'' : ('type/sptree/spt' B)]: (('const/sptree/mk_BN' A) (('const/sptree/difference' A B) t1 't1\'\'') (('const/sptree/difference' A B) t2 't2\'\''))))))).
tt('thm/sptree/difference_def_e3', def, ![B : $t, A : $t]: (![t1 : ('type/sptree/spt' A), a : A, t2 : ('type/sptree/spt' A), t : ('type/sptree/spt' B)]: ((('const/sptree/difference' A B) (('const/sptree/BS' A) t1 a t2) t) = (('const/sptree/spt_CASE' B ('type/sptree/spt' A)) t (('const/sptree/BS' A) t1 a t2) (^['a\'' : B]: (('const/sptree/BN' A) t1 t2)) (^['t1\'' : ('type/sptree/spt' B), 't2\'' : ('type/sptree/spt' B)]: (('const/sptree/mk_BS' A) (('const/sptree/difference' A B) t1 't1\'') a (('const/sptree/difference' A B) t2 't2\''))) (^['t1\'\'' : ('type/sptree/spt' B), 'a\'\'\'' : B, 't2\'\'' : ('type/sptree/spt' B)]: (('const/sptree/mk_BN' A) (('const/sptree/difference' A B) t1 't1\'\'') (('const/sptree/difference' A B) t2 't2\'\''))))))).
tt('thm/sptree/wf_inter_', ax, ![B : $t, A : $t]: (![m1 : ('type/sptree/spt' A), m2 : ('type/sptree/spt' B)]: (('const/sptree/wf' A) (('const/sptree/inter' A B) m1 m2)))).
tt('thm/sptree/lookup_inter_', ax, ![A : $t, B : $t]: (![m1 : ('type/sptree/spt' A), m2 : ('type/sptree/spt' B), k : 'type/num/num']: ((('const/sptree/lookup' A) k (('const/sptree/inter' A B) m1 m2)) = (('const/pair/pair_CASE' ('type/option/option' A) ('type/option/option' A) ('type/option/option' B)) (('const/pair/,' ('type/option/option' A) ('type/option/option' B)) (('const/sptree/lookup' A) k m1) (('const/sptree/lookup' B) k m2)) (^[v3 : ('type/option/option' A), v4 : ('type/option/option' B)]: (('const/option/option_CASE' A ('type/option/option' A)) v3 ('const/option/NONE' A) (^[v : A]: (('const/option/option_CASE' B ('type/option/option' A)) v4 ('const/option/NONE' A) (^[w : B]: (('const/option/SOME' A) v)))))))))).
tt('thm/sptree/lookup_inter_eq_', ax, ![A : $t]: (![m1 : ('type/sptree/spt' A), m2 : ('type/sptree/spt' A), k : 'type/num/num']: ((('const/sptree/lookup' A) k (('const/sptree/inter_eq' A) m1 m2)) = (('const/option/option_CASE' A ('type/option/option' A)) (('const/sptree/lookup' A) k m1) ('const/option/NONE' A) (^[v : A]: (('const/bool/COND' ('type/option/option' A)) ((('const/sptree/lookup' A) k m2) = (('const/option/SOME' A) v)) (('const/option/SOME' A) v) ('const/option/NONE' A))))))).
tt('thm/sptree/lookup_difference_', ax, ![A : $t, B : $t]: (![m1 : ('type/sptree/spt' A), m2 : ('type/sptree/spt' B), k : 'type/num/num']: ((('const/sptree/lookup' A) k (('const/sptree/difference' A B) m1 m2)) = (('const/bool/COND' ('type/option/option' A)) ((('const/sptree/lookup' B) k m2) = ('const/option/NONE' B)) (('const/sptree/lookup' A) k m1) ('const/option/NONE' A))))).
tt('thm/sptree/lrnext_primitive_def_', def, ('const/sptree/lrnext' = (('const/relation/WFREC' 'type/num/num' 'type/num/num') (('const/min/@' ('type/num/num' > ('type/num/num' > $o))) (^[R : ('type/num/num' > ('type/num/num' > $o))]: ((('const/relation/WF' 'type/num/num') R) & (![n : 'type/num/num']: ((~ (n = 'const/num/0')) => (R ('const/arithmetic/DIV' ('const/arithmetic/-' n ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) n)))))) (^[lrnext : ('type/num/num' > 'type/num/num'), n : 'type/num/num']: (('const/combin/I' 'type/num/num') (('const/bool/COND' 'type/num/num') (n = 'const/num/0') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) ('const/arithmetic/*' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) (lrnext ('const/arithmetic/DIV' ('const/arithmetic/-' n ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))))).
tt('thm/sptree/lrnext_ind_', ax, (![P : ('type/num/num' > $o)]: ((![n : 'type/num/num']: (((~ (n = 'const/num/0')) => (P ('const/arithmetic/DIV' ('const/arithmetic/-' n ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) => (P n))) => (![v : 'type/num/num']: (P v))))).
tt('thm/sptree/lrnext_def_', ax, (![n : 'type/num/num']: (('const/sptree/lrnext' n) = (('const/bool/COND' 'type/num/num') (n = 'const/num/0') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) ('const/arithmetic/*' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) ('const/sptree/lrnext' ('const/arithmetic/DIV' ('const/arithmetic/-' n ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))).
tt('thm/sptree/lrnext_thm_0', ax, ![A : $t]: (![a : A]: (('const/sptree/lrnext' 'const/num/0') = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/sptree/lrnext_thm_1', ax, ![B : $t]: (![n : 'type/num/num', a : B]: (('const/sptree/lrnext' ('const/arithmetic/NUMERAL' n)) = ('const/sptree/lrnext' n)))).
tt('thm/sptree/lrnext_thm_2', ax, (('const/sptree/lrnext' 'const/arithmetic/ZERO') = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))).
tt('thm/sptree/lrnext_thm_3', ax, (![n : 'type/num/num']: (('const/sptree/lrnext' ('const/arithmetic/BIT1' n)) = ('const/arithmetic/*' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) ('const/sptree/lrnext' n))))).
tt('thm/sptree/lrnext_thm_e4', ax, (![n : 'type/num/num']: (('const/sptree/lrnext' ('const/arithmetic/BIT2' n)) = ('const/arithmetic/*' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) ('const/sptree/lrnext' n))))).
tt('thm/sptree/domain_def_0', def, ![A : $t]: ((('const/sptree/domain' A) ('const/sptree/LN' A)) = ('const/pred_set/EMPTY' 'type/num/num'))).
tt('thm/sptree/domain_def_1', def, ![A : $t]: (![v0 : A]: ((('const/sptree/domain' A) (('const/sptree/LS' A) v0)) = (('const/pred_set/INSERT' 'type/num/num') 'const/num/0' ('const/pred_set/EMPTY' 'type/num/num'))))).
tt('thm/sptree/domain_def_2', def, ![A : $t]: (![t1 : ('type/sptree/spt' A), t2 : ('type/sptree/spt' A)]: ((('const/sptree/domain' A) (('const/sptree/BN' A) t1 t2)) = (('const/pred_set/UNION' 'type/num/num') (('const/pred_set/IMAGE' 'type/num/num' 'type/num/num') (^[n : 'type/num/num']: ('const/arithmetic/+' ('const/arithmetic/*' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) n) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) (('const/sptree/domain' A) t1)) (('const/pred_set/IMAGE' 'type/num/num' 'type/num/num') (^[n : 'type/num/num']: ('const/arithmetic/+' ('const/arithmetic/*' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) n) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) (('const/sptree/domain' A) t2)))))).
tt('thm/sptree/domain_def_e3', def, ![A : $t]: (![t1 : ('type/sptree/spt' A), v1 : A, t2 : ('type/sptree/spt' A)]: ((('const/sptree/domain' A) (('const/sptree/BS' A) t1 v1 t2)) = (('const/pred_set/UNION' 'type/num/num') (('const/pred_set/UNION' 'type/num/num') (('const/pred_set/INSERT' 'type/num/num') 'const/num/0' ('const/pred_set/EMPTY' 'type/num/num')) (('const/pred_set/IMAGE' 'type/num/num' 'type/num/num') (^[n : 'type/num/num']: ('const/arithmetic/+' ('const/arithmetic/*' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) n) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) (('const/sptree/domain' A) t1))) (('const/pred_set/IMAGE' 'type/num/num' 'type/num/num') (^[n : 'type/num/num']: ('const/arithmetic/+' ('const/arithmetic/*' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) n) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) (('const/sptree/domain' A) t2)))))).
tt('thm/sptree/FINITE_domain_', ax, ![A : $t]: (![t : ('type/sptree/spt' A)]: (('const/pred_set/FINITE' 'type/num/num') (('const/sptree/domain' A) t)))).
tt('thm/sptree/lookup_fromList_', ax, ![A : $t]: (![n : 'type/num/num', l : ('type/list/list' A)]: ((('const/sptree/lookup' A) n (('const/sptree/fromList' A) l)) = (('const/bool/COND' ('type/option/option' A)) ('const/prim_rec/<' n (('const/list/LENGTH' A) l)) (('const/option/SOME' A) (('const/list/EL' A) n l)) ('const/option/NONE' A))))).
tt('thm/sptree/domain_lookup_', ax, ![A : $t]: (![t : ('type/sptree/spt' A), k : 'type/num/num']: ((('const/bool/IN' 'type/num/num') k (('const/sptree/domain' A) t)) = (?[v : A]: ((('const/sptree/lookup' A) k t) = (('const/option/SOME' A) v)))))).
tt('thm/sptree/lookup_NONE_domain_', ax, ![A : $t]: (![t : ('type/sptree/spt' A), k : 'type/num/num']: (((('const/sptree/lookup' A) k t) = ('const/option/NONE' A)) = (~ (('const/bool/IN' 'type/num/num') k (('const/sptree/domain' A) t)))))).
tt('thm/sptree/domain_union_', ax, ![A : $t]: (![t2 : ('type/sptree/spt' A), t1 : ('type/sptree/spt' A)]: ((('const/sptree/domain' A) (('const/sptree/union' A) t1 t2)) = (('const/pred_set/UNION' 'type/num/num') (('const/sptree/domain' A) t1) (('const/sptree/domain' A) t2))))).
tt('thm/sptree/domain_inter_', ax, ![B : $t, A : $t]: (![t2 : ('type/sptree/spt' B), t1 : ('type/sptree/spt' A)]: ((('const/sptree/domain' A) (('const/sptree/inter' A B) t1 t2)) = (('const/pred_set/INTER' 'type/num/num') (('const/sptree/domain' A) t1) (('const/sptree/domain' B) t2))))).
tt('thm/sptree/domain_insert_', ax, ![A : $t]: (![v : A, t : ('type/sptree/spt' A), k : 'type/num/num']: ((('const/sptree/domain' A) (('const/sptree/insert' A) k v t)) = (('const/pred_set/INSERT' 'type/num/num') k (('const/sptree/domain' A) t))))).
tt('thm/sptree/domain_sing_', ax, ![A : $t]: (![v : A, k : 'type/num/num']: ((('const/sptree/domain' A) (('const/sptree/insert' A) k v ('const/sptree/LN' A))) = (('const/pred_set/INSERT' 'type/num/num') k ('const/pred_set/EMPTY' 'type/num/num'))))).
tt('thm/sptree/domain_fromList_', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/sptree/domain' A) (('const/sptree/fromList' A) l)) = ('const/pred_set/count' (('const/list/LENGTH' A) l))))).
tt('thm/sptree/lookup_delete_', ax, ![A : $t]: (![t : ('type/sptree/spt' A), k1 : 'type/num/num', k2 : 'type/num/num']: ((('const/sptree/lookup' A) k1 (('const/sptree/delete' A) k2 t)) = (('const/bool/COND' ('type/option/option' A)) (k1 = k2) ('const/option/NONE' A) (('const/sptree/lookup' A) k1 t))))).
tt('thm/sptree/domain_delete_', ax, ![A : $t]: (![t : ('type/sptree/spt' A), k : 'type/num/num']: ((('const/sptree/domain' A) (('const/sptree/delete' A) k t)) = (('const/pred_set/DELETE' 'type/num/num') (('const/sptree/domain' A) t) k)))).
tt('thm/sptree/foldi_def_0', def, ![A : $t, B : $t]: (![f : ('type/num/num' > (B > (A > A))), i : 'type/num/num', acc : A]: ((('const/sptree/foldi' A B) f i acc ('const/sptree/LN' B)) = acc))).
tt('thm/sptree/foldi_def_1', def, ![A : $t, B : $t]: (![f : ('type/num/num' > (B > (A > A))), i : 'type/num/num', acc : A, a : B]: ((('const/sptree/foldi' A B) f i acc (('const/sptree/LS' B) a)) = (f i a acc)))).
tt('thm/sptree/foldi_def_2', def, ![B : $t, A : $t]: (![f : ('type/num/num' > (B > (A > A))), i : 'type/num/num', acc : A, t1 : ('type/sptree/spt' B), t2 : ('type/sptree/spt' B)]: ((('const/sptree/foldi' A B) f i acc (('const/sptree/BN' B) t1 t2)) = (('const/bool/LET' 'type/num/num' A) (^[inc : 'type/num/num']: (('const/sptree/foldi' A B) f ('const/arithmetic/+' i inc) (('const/sptree/foldi' A B) f ('const/arithmetic/+' i ('const/arithmetic/*' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) inc)) acc t1) t2)) ('const/sptree/lrnext' i))))).
tt('thm/sptree/foldi_def_e3', def, ![B : $t, A : $t]: (![f : ('type/num/num' > (B > (A > A))), i : 'type/num/num', acc : A, t1 : ('type/sptree/spt' B), a : B, t2 : ('type/sptree/spt' B)]: ((('const/sptree/foldi' A B) f i acc (('const/sptree/BS' B) t1 a t2)) = (('const/bool/LET' 'type/num/num' A) (^[inc : 'type/num/num']: (('const/sptree/foldi' A B) f ('const/arithmetic/+' i inc) (f i a (('const/sptree/foldi' A B) f ('const/arithmetic/+' i ('const/arithmetic/*' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) inc)) acc t1)) t2)) ('const/sptree/lrnext' i))))).
tt('thm/sptree/set_foldi_keys_', ax, ![A : $t]: (![t : ('type/sptree/spt' A), a : ('type/num/num' > $o), i : 'type/num/num']: ((('const/sptree/foldi' ('type/num/num' > $o) A) (^[k : 'type/num/num', v : A, a0 : ('type/num/num' > $o)]: (('const/pred_set/INSERT' 'type/num/num') k a0)) i a t) = (('const/pred_set/UNION' 'type/num/num') a (('const/pred_set/IMAGE' 'type/num/num' 'type/num/num') (^[n : 'type/num/num']: ('const/arithmetic/+' i ('const/arithmetic/*' ('const/sptree/lrnext' i) n))) (('const/sptree/domain' A) t)))))).
tt('thm/sptree/domain_foldi_', ax, ![A : $t]: (![t : ('type/sptree/spt' A)]: ((('const/sptree/domain' A) t) = (('const/sptree/foldi' ('type/num/num' > $o) A) (^[k : 'type/num/num', v : A, a : ('type/num/num' > $o)]: (('const/pred_set/INSERT' 'type/num/num') k a)) 'const/num/0' ('const/pred_set/EMPTY' 'type/num/num') t)))).
tt('thm/sptree/toAList_def_', def, ![A : $t]: (('const/sptree/toAList' A) = (('const/sptree/foldi' ('type/list/list' ('type/pair/prod' 'type/num/num' A)) A) (^[k : 'type/num/num', v : A, a : ('type/list/list' ('type/pair/prod' 'type/num/num' A))]: (('const/list/CONS' ('type/pair/prod' 'type/num/num' A)) (('const/pair/,' 'type/num/num' A) k v) a)) 'const/num/0' ('const/list/NIL' ('type/pair/prod' 'type/num/num' A))))).
tt('thm/sptree/MEM_toAList_', ax, ![A : $t]: (![t : ('type/sptree/spt' A), k : 'type/num/num', v : A]: ((('const/bool/IN' ('type/pair/prod' 'type/num/num' A)) (('const/pair/,' 'type/num/num' A) k v) (('const/list/LIST_TO_SET' ('type/pair/prod' 'type/num/num' A)) (('const/sptree/toAList' A) t))) = ((('const/sptree/lookup' A) k t) = (('const/option/SOME' A) v))))).
tt('thm/sptree/ALOOKUP_toAList_', ax, ![A : $t]: (![t : ('type/sptree/spt' A), x : 'type/num/num']: ((('const/alist/ALOOKUP' A 'type/num/num') (('const/sptree/toAList' A) t) x) = (('const/sptree/lookup' A) x t)))).
tt('thm/sptree/insert_union_', ax, ![A : $t]: (![k : 'type/num/num', v : A, s : ('type/sptree/spt' A)]: ((('const/sptree/insert' A) k v s) = (('const/sptree/union' A) (('const/sptree/insert' A) k v ('const/sptree/LN' A)) s)))).
tt('thm/sptree/domain_empty_', ax, ![A : $t]: (![t : ('type/sptree/spt' A)]: ((('const/sptree/wf' A) t) => ((t = ('const/sptree/LN' A)) = ((('const/sptree/domain' A) t) = ('const/pred_set/EMPTY' 'type/num/num')))))).
tt('thm/sptree/ALL_DISTINCT_MAP_FST_toAList_', ax, ![A : $t]: (![t : ('type/sptree/spt' A)]: (('const/list/ALL_DISTINCT' 'type/num/num') (('const/list/MAP' ('type/pair/prod' 'type/num/num' A) 'type/num/num') ('const/pair/FST' 'type/num/num' A) (('const/sptree/toAList' A) t))))).
tt('thm/sptree/foldi_FOLDR_toAList_', ax, ![A : $t, B : $t]: (![f : ('type/num/num' > (A > (B > B))), a : B, t : ('type/sptree/spt' A)]: ((('const/sptree/foldi' B A) f 'const/num/0' a t) = (('const/list/FOLDR' ('type/pair/prod' 'type/num/num' A) B) (('const/pair/UNCURRY' 'type/num/num' A (B > B)) f) a (('const/sptree/toAList' A) t))))).
tt('thm/sptree/toListA_def_0', def, ![A : $t]: (![acc : ('type/list/list' A)]: ((('const/sptree/toListA' A) acc ('const/sptree/LN' A)) = acc))).
tt('thm/sptree/toListA_def_1', def, ![A : $t]: (![acc : ('type/list/list' A), a : A]: ((('const/sptree/toListA' A) acc (('const/sptree/LS' A) a)) = (('const/list/CONS' A) a acc)))).
tt('thm/sptree/toListA_def_2', def, ![A : $t]: (![acc : ('type/list/list' A), t1 : ('type/sptree/spt' A), t2 : ('type/sptree/spt' A)]: ((('const/sptree/toListA' A) acc (('const/sptree/BN' A) t1 t2)) = (('const/sptree/toListA' A) (('const/sptree/toListA' A) acc t2) t1)))).
tt('thm/sptree/toListA_def_e3', def, ![A : $t]: (![acc : ('type/list/list' A), t1 : ('type/sptree/spt' A), a : A, t2 : ('type/sptree/spt' A)]: ((('const/sptree/toListA' A) acc (('const/sptree/BS' A) t1 a t2)) = (('const/sptree/toListA' A) (('const/list/CONS' A) a (('const/sptree/toListA' A) acc t2)) t1)))).
tt('thm/sptree/toListA_append_', ax, ![A : $t]: (![t : ('type/sptree/spt' A), acc : ('type/list/list' A)]: ((('const/sptree/toListA' A) acc t) = (('const/list/APPEND' A) (('const/sptree/toListA' A) ('const/list/NIL' A) t) acc)))).
tt('thm/sptree/isEmpty_toListA_', ax, ![A : $t]: (![t : ('type/sptree/spt' A), acc : ('type/list/list' A)]: ((('const/sptree/wf' A) t) => ((t = ('const/sptree/LN' A)) = ((('const/sptree/toListA' A) acc t) = acc))))).
tt('thm/sptree/toList_def_', def, ![A : $t]: (![m : ('type/sptree/spt' A)]: ((('const/sptree/toList' A) m) = (('const/sptree/toListA' A) ('const/list/NIL' A) m)))).
tt('thm/sptree/isEmpty_toList_', ax, ![A : $t]: (![t : ('type/sptree/spt' A)]: ((('const/sptree/wf' A) t) => ((t = ('const/sptree/LN' A)) = ((('const/sptree/toList' A) t) = ('const/list/NIL' A)))))).
tt('thm/sptree/MEM_toList_', ax, ![A : $t]: (![x : A, t : ('type/sptree/spt' A)]: ((('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) (('const/sptree/toList' A) t))) = (?[k : 'type/num/num']: ((('const/sptree/lookup' A) k t) = (('const/option/SOME' A) x)))))).
tt('thm/sptree/spt_eq_thm_', ax, ![A : $t]: (![t1 : ('type/sptree/spt' A), t2 : ('type/sptree/spt' A)]: (((('const/sptree/wf' A) t1) & (('const/sptree/wf' A) t2)) => ((t1 = t2) = (![n : 'type/num/num']: ((('const/sptree/lookup' A) n t1) = (('const/sptree/lookup' A) n t2))))))).
tt('thm/sptree/mk_wf_def_0', def, ![A : $t]: ((('const/sptree/mk_wf' A) ('const/sptree/LN' A)) = ('const/sptree/LN' A))).
tt('thm/sptree/mk_wf_def_1', def, ![A : $t]: (![x : A]: ((('const/sptree/mk_wf' A) (('const/sptree/LS' A) x)) = (('const/sptree/LS' A) x)))).
tt('thm/sptree/mk_wf_def_2', def, ![A : $t]: (![t1 : ('type/sptree/spt' A), t2 : ('type/sptree/spt' A)]: ((('const/sptree/mk_wf' A) (('const/sptree/BN' A) t1 t2)) = (('const/sptree/mk_BN' A) (('const/sptree/mk_wf' A) t1) (('const/sptree/mk_wf' A) t2))))).
tt('thm/sptree/mk_wf_def_e3', def, ![A : $t]: (![t1 : ('type/sptree/spt' A), x : A, t2 : ('type/sptree/spt' A)]: ((('const/sptree/mk_wf' A) (('const/sptree/BS' A) t1 x t2)) = (('const/sptree/mk_BS' A) (('const/sptree/mk_wf' A) t1) x (('const/sptree/mk_wf' A) t2))))).
tt('thm/sptree/wf_mk_wf_', ax, ![A : $t]: (![t : ('type/sptree/spt' A)]: (('const/sptree/wf' A) (('const/sptree/mk_wf' A) t)))).
tt('thm/sptree/wf_mk_id_', ax, ![A : $t]: (![t : ('type/sptree/spt' A)]: ((('const/sptree/wf' A) t) => ((('const/sptree/mk_wf' A) t) = t)))).
tt('thm/sptree/lookup_mk_wf_', ax, ![A : $t]: (![x : 'type/num/num', t : ('type/sptree/spt' A)]: ((('const/sptree/lookup' A) x (('const/sptree/mk_wf' A) t)) = (('const/sptree/lookup' A) x t)))).
tt('thm/sptree/domain_mk_wf_', ax, ![A : $t]: (![t : ('type/sptree/spt' A)]: ((('const/sptree/domain' A) (('const/sptree/mk_wf' A) t)) = (('const/sptree/domain' A) t)))).
tt('thm/sptree/mk_wf_eq_', ax, ![A : $t]: (![t1 : ('type/sptree/spt' A), t2 : ('type/sptree/spt' A)]: (((('const/sptree/mk_wf' A) t1) = (('const/sptree/mk_wf' A) t2)) = (![x : 'type/num/num']: ((('const/sptree/lookup' A) x t1) = (('const/sptree/lookup' A) x t2)))))).
tt('thm/sptree/inter_eq_', ax, ![C : $t, A : $t, B : $t]: (![t1 : ('type/sptree/spt' A), t2 : ('type/sptree/spt' B), t3 : ('type/sptree/spt' A), t4 : ('type/sptree/spt' C)]: (((('const/sptree/inter' A B) t1 t2) = (('const/sptree/inter' A C) t3 t4)) = (![x : 'type/num/num']: ((('const/sptree/lookup' A) x (('const/sptree/inter' A B) t1 t2)) = (('const/sptree/lookup' A) x (('const/sptree/inter' A C) t3 t4))))))).
tt('thm/sptree/union_mk_wf_', ax, ![B : $t, A : $t]: (![t1 : ('type/sptree/spt' A), t2 : ('type/sptree/spt' B)]: ((('const/sptree/inter' A B) (('const/sptree/mk_wf' A) t1) (('const/sptree/mk_wf' B) t2)) = (('const/sptree/mk_wf' A) (('const/sptree/inter' A B) t1 t2))))).
tt('thm/sptree/insert_mk_wf_', ax, ![A : $t]: (![x : 'type/num/num', v : A, t : ('type/sptree/spt' A)]: ((('const/sptree/insert' A) x v (('const/sptree/mk_wf' A) t)) = (('const/sptree/mk_wf' A) (('const/sptree/insert' A) x v t))))).
tt('thm/sptree/delete_mk_wf_', ax, ![A : $t]: (![x : 'type/num/num', t : ('type/sptree/spt' A)]: ((('const/sptree/delete' A) x (('const/sptree/mk_wf' A) t)) = (('const/sptree/mk_wf' A) (('const/sptree/delete' A) x t))))).
tt('thm/sptree/union_LN_0', ax, ![A : $t]: (![t : ('type/sptree/spt' A)]: ((('const/sptree/union' A) t ('const/sptree/LN' A)) = t))).
tt('thm/sptree/union_LN_e1', ax, ![A : $t]: (![t : ('type/sptree/spt' A)]: ((('const/sptree/union' A) ('const/sptree/LN' A) t) = t))).
tt('thm/sptree/inter_LN_0', ax, ![A : $t, B : $t]: (![t : ('type/sptree/spt' A)]: ((('const/sptree/inter' A B) t ('const/sptree/LN' B)) = ('const/sptree/LN' A)))).
tt('thm/sptree/inter_LN_e1', ax, ![C : $t, A : $t]: (![t : ('type/sptree/spt' A)]: ((('const/sptree/inter' C A) ('const/sptree/LN' C) t) = ('const/sptree/LN' C)))).
tt('thm/sptree/union_assoc_', ax, ![A : $t]: (![t1 : ('type/sptree/spt' A), t2 : ('type/sptree/spt' A), t3 : ('type/sptree/spt' A)]: ((('const/sptree/union' A) t1 (('const/sptree/union' A) t2 t3)) = (('const/sptree/union' A) (('const/sptree/union' A) t1 t2) t3)))).
tt('thm/sptree/inter_assoc_', ax, ![C : $t, B : $t, A : $t]: (![t1 : ('type/sptree/spt' A), t2 : ('type/sptree/spt' B), t3 : ('type/sptree/spt' C)]: ((('const/sptree/inter' A B) t1 (('const/sptree/inter' B C) t2 t3)) = (('const/sptree/inter' A C) (('const/sptree/inter' A B) t1 t2) t3)))).
tt('thm/sptree/lookup_compute_0', ax, ![A : $t]: (![t : ('type/sptree/spt' A), n : 'type/num/num']: ((('const/sptree/lookup' A) ('const/arithmetic/NUMERAL' n) t) = (('const/sptree/lookup' A) n t)))).
tt('thm/sptree/lookup_compute_1', ax, ![A : $t]: ((('const/sptree/lookup' A) 'const/num/0' ('const/sptree/LN' A)) = ('const/option/NONE' A))).
tt('thm/sptree/lookup_compute_2', ax, ![A : $t]: (![a : A]: ((('const/sptree/lookup' A) 'const/num/0' (('const/sptree/LS' A) a)) = (('const/option/SOME' A) a)))).
tt('thm/sptree/lookup_compute_3', ax, ![A : $t]: (![t2 : ('type/sptree/spt' A), t1 : ('type/sptree/spt' A)]: ((('const/sptree/lookup' A) 'const/num/0' (('const/sptree/BN' A) t1 t2)) = ('const/option/NONE' A)))).
tt('thm/sptree/lookup_compute_4', ax, ![A : $t]: (![t2 : ('type/sptree/spt' A), t1 : ('type/sptree/spt' A), a : A]: ((('const/sptree/lookup' A) 'const/num/0' (('const/sptree/BS' A) t1 a t2)) = (('const/option/SOME' A) a)))).
tt('thm/sptree/lookup_compute_5', ax, ![A : $t]: ((('const/sptree/lookup' A) 'const/arithmetic/ZERO' ('const/sptree/LN' A)) = ('const/option/NONE' A))).
tt('thm/sptree/lookup_compute_6', ax, ![A : $t]: (![a : A]: ((('const/sptree/lookup' A) 'const/arithmetic/ZERO' (('const/sptree/LS' A) a)) = (('const/option/SOME' A) a)))).
tt('thm/sptree/lookup_compute_7', ax, ![A : $t]: (![t2 : ('type/sptree/spt' A), t1 : ('type/sptree/spt' A)]: ((('const/sptree/lookup' A) 'const/arithmetic/ZERO' (('const/sptree/BN' A) t1 t2)) = ('const/option/NONE' A)))).
tt('thm/sptree/lookup_compute_8', ax, ![A : $t]: (![t2 : ('type/sptree/spt' A), t1 : ('type/sptree/spt' A), a : A]: ((('const/sptree/lookup' A) 'const/arithmetic/ZERO' (('const/sptree/BS' A) t1 a t2)) = (('const/option/SOME' A) a)))).
tt('thm/sptree/lookup_compute_9', ax, ![A : $t]: (![n : 'type/num/num']: ((('const/sptree/lookup' A) ('const/arithmetic/BIT1' n) ('const/sptree/LN' A)) = ('const/option/NONE' A)))).
tt('thm/sptree/lookup_compute_10', ax, ![A : $t]: (![n : 'type/num/num', a : A]: ((('const/sptree/lookup' A) ('const/arithmetic/BIT1' n) (('const/sptree/LS' A) a)) = ('const/option/NONE' A)))).
tt('thm/sptree/lookup_compute_11', ax, ![A : $t]: (![t2 : ('type/sptree/spt' A), t1 : ('type/sptree/spt' A), n : 'type/num/num']: ((('const/sptree/lookup' A) ('const/arithmetic/BIT1' n) (('const/sptree/BN' A) t1 t2)) = (('const/sptree/lookup' A) n t2)))).
tt('thm/sptree/lookup_compute_12', ax, ![A : $t]: (![t2 : ('type/sptree/spt' A), t1 : ('type/sptree/spt' A), n : 'type/num/num', a : A]: ((('const/sptree/lookup' A) ('const/arithmetic/BIT1' n) (('const/sptree/BS' A) t1 a t2)) = (('const/sptree/lookup' A) n t2)))).
tt('thm/sptree/lookup_compute_13', ax, ![A : $t]: (![n : 'type/num/num']: ((('const/sptree/lookup' A) ('const/arithmetic/BIT2' n) ('const/sptree/LN' A)) = ('const/option/NONE' A)))).
tt('thm/sptree/lookup_compute_14', ax, ![A : $t]: (![n : 'type/num/num', a : A]: ((('const/sptree/lookup' A) ('const/arithmetic/BIT2' n) (('const/sptree/LS' A) a)) = ('const/option/NONE' A)))).
tt('thm/sptree/lookup_compute_15', ax, ![A : $t]: (![t2 : ('type/sptree/spt' A), t1 : ('type/sptree/spt' A), n : 'type/num/num']: ((('const/sptree/lookup' A) ('const/arithmetic/BIT2' n) (('const/sptree/BN' A) t1 t2)) = (('const/sptree/lookup' A) n t1)))).
tt('thm/sptree/lookup_compute_e16', ax, ![A : $t]: (![t2 : ('type/sptree/spt' A), t1 : ('type/sptree/spt' A), n : 'type/num/num', a : A]: ((('const/sptree/lookup' A) ('const/arithmetic/BIT2' n) (('const/sptree/BS' A) t1 a t2)) = (('const/sptree/lookup' A) n t1)))).
tt('thm/sptree/insert_compute_0', ax, ![A : $t]: (![t : ('type/sptree/spt' A), n : 'type/num/num', a : A]: ((('const/sptree/insert' A) ('const/arithmetic/NUMERAL' n) a t) = (('const/sptree/insert' A) n a t)))).
tt('thm/sptree/insert_compute_1', ax, ![A : $t]: (![a : A]: ((('const/sptree/insert' A) 'const/num/0' a ('const/sptree/LN' A)) = (('const/sptree/LS' A) a)))).
tt('thm/sptree/insert_compute_2', ax, ![A : $t]: (!['a\'' : A, a : A]: ((('const/sptree/insert' A) 'const/num/0' a (('const/sptree/LS' A) 'a\'')) = (('const/sptree/LS' A) a)))).
tt('thm/sptree/insert_compute_3', ax, ![A : $t]: (![t2 : ('type/sptree/spt' A), t1 : ('type/sptree/spt' A), a : A]: ((('const/sptree/insert' A) 'const/num/0' a (('const/sptree/BN' A) t1 t2)) = (('const/sptree/BS' A) t1 a t2)))).
tt('thm/sptree/insert_compute_4', ax, ![A : $t]: (![t2 : ('type/sptree/spt' A), t1 : ('type/sptree/spt' A), 'a\'' : A, a : A]: ((('const/sptree/insert' A) 'const/num/0' a (('const/sptree/BS' A) t1 'a\'' t2)) = (('const/sptree/BS' A) t1 a t2)))).
tt('thm/sptree/insert_compute_5', ax, ![A : $t]: (![a : A]: ((('const/sptree/insert' A) 'const/arithmetic/ZERO' a ('const/sptree/LN' A)) = (('const/sptree/LS' A) a)))).
tt('thm/sptree/insert_compute_6', ax, ![A : $t]: (!['a\'' : A, a : A]: ((('const/sptree/insert' A) 'const/arithmetic/ZERO' a (('const/sptree/LS' A) 'a\'')) = (('const/sptree/LS' A) a)))).
tt('thm/sptree/insert_compute_7', ax, ![A : $t]: (![t2 : ('type/sptree/spt' A), t1 : ('type/sptree/spt' A), a : A]: ((('const/sptree/insert' A) 'const/arithmetic/ZERO' a (('const/sptree/BN' A) t1 t2)) = (('const/sptree/BS' A) t1 a t2)))).
tt('thm/sptree/insert_compute_8', ax, ![A : $t]: (![t2 : ('type/sptree/spt' A), t1 : ('type/sptree/spt' A), 'a\'' : A, a : A]: ((('const/sptree/insert' A) 'const/arithmetic/ZERO' a (('const/sptree/BS' A) t1 'a\'' t2)) = (('const/sptree/BS' A) t1 a t2)))).
tt('thm/sptree/insert_compute_9', ax, ![A : $t]: (![n : 'type/num/num', a : A]: ((('const/sptree/insert' A) ('const/arithmetic/BIT1' n) a ('const/sptree/LN' A)) = (('const/sptree/BN' A) ('const/sptree/LN' A) (('const/sptree/insert' A) n a ('const/sptree/LN' A)))))).
tt('thm/sptree/insert_compute_10', ax, ![A : $t]: (![n : 'type/num/num', 'a\'' : A, a : A]: ((('const/sptree/insert' A) ('const/arithmetic/BIT1' n) a (('const/sptree/LS' A) 'a\'')) = (('const/sptree/BS' A) ('const/sptree/LN' A) 'a\'' (('const/sptree/insert' A) n a ('const/sptree/LN' A)))))).
tt('thm/sptree/insert_compute_11', ax, ![A : $t]: (![t2 : ('type/sptree/spt' A), t1 : ('type/sptree/spt' A), n : 'type/num/num', a : A]: ((('const/sptree/insert' A) ('const/arithmetic/BIT1' n) a (('const/sptree/BN' A) t1 t2)) = (('const/sptree/BN' A) t1 (('const/sptree/insert' A) n a t2))))).
tt('thm/sptree/insert_compute_12', ax, ![A : $t]: (![t2 : ('type/sptree/spt' A), t1 : ('type/sptree/spt' A), n : 'type/num/num', 'a\'' : A, a : A]: ((('const/sptree/insert' A) ('const/arithmetic/BIT1' n) a (('const/sptree/BS' A) t1 'a\'' t2)) = (('const/sptree/BS' A) t1 'a\'' (('const/sptree/insert' A) n a t2))))).
tt('thm/sptree/insert_compute_13', ax, ![A : $t]: (![n : 'type/num/num', a : A]: ((('const/sptree/insert' A) ('const/arithmetic/BIT2' n) a ('const/sptree/LN' A)) = (('const/sptree/BN' A) (('const/sptree/insert' A) n a ('const/sptree/LN' A)) ('const/sptree/LN' A))))).
tt('thm/sptree/insert_compute_14', ax, ![A : $t]: (![n : 'type/num/num', 'a\'' : A, a : A]: ((('const/sptree/insert' A) ('const/arithmetic/BIT2' n) a (('const/sptree/LS' A) 'a\'')) = (('const/sptree/BS' A) (('const/sptree/insert' A) n a ('const/sptree/LN' A)) 'a\'' ('const/sptree/LN' A))))).
tt('thm/sptree/insert_compute_15', ax, ![A : $t]: (![t2 : ('type/sptree/spt' A), t1 : ('type/sptree/spt' A), n : 'type/num/num', a : A]: ((('const/sptree/insert' A) ('const/arithmetic/BIT2' n) a (('const/sptree/BN' A) t1 t2)) = (('const/sptree/BN' A) (('const/sptree/insert' A) n a t1) t2)))).
tt('thm/sptree/insert_compute_e16', ax, ![A : $t]: (![t2 : ('type/sptree/spt' A), t1 : ('type/sptree/spt' A), n : 'type/num/num', 'a\'' : A, a : A]: ((('const/sptree/insert' A) ('const/arithmetic/BIT2' n) a (('const/sptree/BS' A) t1 'a\'' t2)) = (('const/sptree/BS' A) (('const/sptree/insert' A) n a t1) 'a\'' t2)))).
tt('thm/sptree/delete_compute_0', ax, ![A : $t]: (![t : ('type/sptree/spt' A), n : 'type/num/num']: ((('const/sptree/delete' A) ('const/arithmetic/NUMERAL' n) t) = (('const/sptree/delete' A) n t)))).
tt('thm/sptree/delete_compute_1', ax, ![A : $t]: ((('const/sptree/delete' A) 'const/num/0' ('const/sptree/LN' A)) = ('const/sptree/LN' A))).
tt('thm/sptree/delete_compute_2', ax, ![A : $t]: (![a : A]: ((('const/sptree/delete' A) 'const/num/0' (('const/sptree/LS' A) a)) = ('const/sptree/LN' A)))).
tt('thm/sptree/delete_compute_3', ax, ![A : $t]: (![t2 : ('type/sptree/spt' A), t1 : ('type/sptree/spt' A)]: ((('const/sptree/delete' A) 'const/num/0' (('const/sptree/BN' A) t1 t2)) = (('const/sptree/BN' A) t1 t2)))).
tt('thm/sptree/delete_compute_4', ax, ![A : $t]: (![t2 : ('type/sptree/spt' A), t1 : ('type/sptree/spt' A), a : A]: ((('const/sptree/delete' A) 'const/num/0' (('const/sptree/BS' A) t1 a t2)) = (('const/sptree/BN' A) t1 t2)))).
tt('thm/sptree/delete_compute_5', ax, ![A : $t]: ((('const/sptree/delete' A) 'const/arithmetic/ZERO' ('const/sptree/LN' A)) = ('const/sptree/LN' A))).
tt('thm/sptree/delete_compute_6', ax, ![A : $t]: (![a : A]: ((('const/sptree/delete' A) 'const/arithmetic/ZERO' (('const/sptree/LS' A) a)) = ('const/sptree/LN' A)))).
tt('thm/sptree/delete_compute_7', ax, ![A : $t]: (![t2 : ('type/sptree/spt' A), t1 : ('type/sptree/spt' A)]: ((('const/sptree/delete' A) 'const/arithmetic/ZERO' (('const/sptree/BN' A) t1 t2)) = (('const/sptree/BN' A) t1 t2)))).
tt('thm/sptree/delete_compute_8', ax, ![A : $t]: (![t2 : ('type/sptree/spt' A), t1 : ('type/sptree/spt' A), a : A]: ((('const/sptree/delete' A) 'const/arithmetic/ZERO' (('const/sptree/BS' A) t1 a t2)) = (('const/sptree/BN' A) t1 t2)))).
tt('thm/sptree/delete_compute_9', ax, ![A : $t]: (![n : 'type/num/num']: ((('const/sptree/delete' A) ('const/arithmetic/BIT1' n) ('const/sptree/LN' A)) = ('const/sptree/LN' A)))).
tt('thm/sptree/delete_compute_10', ax, ![A : $t]: (![n : 'type/num/num', a : A]: ((('const/sptree/delete' A) ('const/arithmetic/BIT1' n) (('const/sptree/LS' A) a)) = (('const/sptree/LS' A) a)))).
tt('thm/sptree/delete_compute_11', ax, ![A : $t]: (![t2 : ('type/sptree/spt' A), t1 : ('type/sptree/spt' A), n : 'type/num/num']: ((('const/sptree/delete' A) ('const/arithmetic/BIT1' n) (('const/sptree/BN' A) t1 t2)) = (('const/sptree/mk_BN' A) t1 (('const/sptree/delete' A) n t2))))).
tt('thm/sptree/delete_compute_12', ax, ![A : $t]: (![t2 : ('type/sptree/spt' A), t1 : ('type/sptree/spt' A), n : 'type/num/num', a : A]: ((('const/sptree/delete' A) ('const/arithmetic/BIT1' n) (('const/sptree/BS' A) t1 a t2)) = (('const/sptree/mk_BS' A) t1 a (('const/sptree/delete' A) n t2))))).
tt('thm/sptree/delete_compute_13', ax, ![A : $t]: (![n : 'type/num/num']: ((('const/sptree/delete' A) ('const/arithmetic/BIT2' n) ('const/sptree/LN' A)) = ('const/sptree/LN' A)))).
tt('thm/sptree/delete_compute_14', ax, ![A : $t]: (![n : 'type/num/num', a : A]: ((('const/sptree/delete' A) ('const/arithmetic/BIT2' n) (('const/sptree/LS' A) a)) = (('const/sptree/LS' A) a)))).
tt('thm/sptree/delete_compute_15', ax, ![A : $t]: (![t2 : ('type/sptree/spt' A), t1 : ('type/sptree/spt' A), n : 'type/num/num']: ((('const/sptree/delete' A) ('const/arithmetic/BIT2' n) (('const/sptree/BN' A) t1 t2)) = (('const/sptree/mk_BN' A) (('const/sptree/delete' A) n t1) t2)))).
tt('thm/sptree/delete_compute_e16', ax, ![A : $t]: (![t2 : ('type/sptree/spt' A), t1 : ('type/sptree/spt' A), n : 'type/num/num', a : A]: ((('const/sptree/delete' A) ('const/arithmetic/BIT2' n) (('const/sptree/BS' A) t1 a t2)) = (('const/sptree/mk_BS' A) (('const/sptree/delete' A) n t1) a t2)))).
tt('thm/sptree/fromAList_primitive_def_', def, ![A : $t]: (('const/sptree/fromAList' A) = (('const/relation/WFREC' ('type/list/list' ('type/pair/prod' 'type/num/num' A)) ('type/sptree/spt' A)) (('const/min/@' (('type/list/list' ('type/pair/prod' 'type/num/num' A)) > (('type/list/list' ('type/pair/prod' 'type/num/num' A)) > $o))) (^[R : (('type/list/list' ('type/pair/prod' 'type/num/num' A)) > (('type/list/list' ('type/pair/prod' 'type/num/num' A)) > $o))]: ((('const/relation/WF' ('type/list/list' ('type/pair/prod' 'type/num/num' A))) R) & (![y : A, x : 'type/num/num', xs : ('type/list/list' ('type/pair/prod' 'type/num/num' A))]: (R xs (('const/list/CONS' ('type/pair/prod' 'type/num/num' A)) (('const/pair/,' 'type/num/num' A) x y) xs)))))) (^[fromAList : (('type/list/list' ('type/pair/prod' 'type/num/num' A)) > ('type/sptree/spt' A)), a : ('type/list/list' ('type/pair/prod' 'type/num/num' A))]: (('const/list/list_CASE' ('type/pair/prod' 'type/num/num' A) ('type/sptree/spt' A)) a (('const/combin/I' ('type/sptree/spt' A)) ('const/sptree/LN' A)) (^[v : ('type/pair/prod' 'type/num/num' A), xs : ('type/list/list' ('type/pair/prod' 'type/num/num' A))]: (('const/pair/pair_CASE' ('type/sptree/spt' A) 'type/num/num' A) v (^[x : 'type/num/num', y : A]: (('const/combin/I' ('type/sptree/spt' A)) (('const/sptree/insert' A) x y (fromAList xs))))))))))).
tt('thm/sptree/fromAList_ind_', ax, ![A : $t]: (![P : (('type/list/list' ('type/pair/prod' 'type/num/num' A)) > $o)]: (((P ('const/list/NIL' ('type/pair/prod' 'type/num/num' A))) & (![x : 'type/num/num', y : A, xs : ('type/list/list' ('type/pair/prod' 'type/num/num' A))]: ((P xs) => (P (('const/list/CONS' ('type/pair/prod' 'type/num/num' A)) (('const/pair/,' 'type/num/num' A) x y) xs))))) => (![v : ('type/list/list' ('type/pair/prod' 'type/num/num' A))]: (P v))))).
tt('thm/sptree/fromAList_def_0', ax, ![A : $t]: ((('const/sptree/fromAList' A) ('const/list/NIL' ('type/pair/prod' 'type/num/num' A))) = ('const/sptree/LN' A))).
tt('thm/sptree/fromAList_def_e1', ax, ![A : $t]: (![y : A, xs : ('type/list/list' ('type/pair/prod' 'type/num/num' A)), x : 'type/num/num']: ((('const/sptree/fromAList' A) (('const/list/CONS' ('type/pair/prod' 'type/num/num' A)) (('const/pair/,' 'type/num/num' A) x y) xs)) = (('const/sptree/insert' A) x y (('const/sptree/fromAList' A) xs))))).
tt('thm/sptree/lookup_fromAList_', ax, ![A : $t]: (![ls : ('type/list/list' ('type/pair/prod' 'type/num/num' A)), x : 'type/num/num']: ((('const/sptree/lookup' A) x (('const/sptree/fromAList' A) ls)) = (('const/alist/ALOOKUP' A 'type/num/num') ls x)))).
tt('thm/sptree/domain_fromAList_', ax, ![A : $t]: (![ls : ('type/list/list' ('type/pair/prod' 'type/num/num' A))]: ((('const/sptree/domain' A) (('const/sptree/fromAList' A) ls)) = (('const/list/LIST_TO_SET' 'type/num/num') (('const/list/MAP' ('type/pair/prod' 'type/num/num' A) 'type/num/num') ('const/pair/FST' 'type/num/num' A) ls))))).
tt('thm/sptree/lookup_fromAList_toAList_', ax, ![A : $t]: (![t : ('type/sptree/spt' A), x : 'type/num/num']: ((('const/sptree/lookup' A) x (('const/sptree/fromAList' A) (('const/sptree/toAList' A) t))) = (('const/sptree/lookup' A) x t)))).
tt('thm/sptree/wf_fromAList_', ax, ![A : $t]: (![ls : ('type/list/list' ('type/pair/prod' 'type/num/num' A))]: (('const/sptree/wf' A) (('const/sptree/fromAList' A) ls)))).
tt('thm/sptree/fromAList_toAList_', ax, ![A : $t]: (![t : ('type/sptree/spt' A)]: ((('const/sptree/wf' A) t) => ((('const/sptree/fromAList' A) (('const/sptree/toAList' A) t)) = t)))).
