tt('type/patricia/ptree', ty, $t > $t).
tt('const/patricia/ADD', ty, ![A : $t]: (('type/patricia/ptree' A) > (('type/pair/prod' 'type/num/num' A) > ('type/patricia/ptree' A)))).
tt('const/patricia/ADD_LIST', ty, ![A : $t]: (('type/patricia/ptree' A) > (('type/list/list' ('type/pair/prod' 'type/num/num' A)) > ('type/patricia/ptree' A)))).
tt('const/patricia/ADD_tupled', ty, ![A : $t]: (('type/pair/prod' ('type/patricia/ptree' A) ('type/pair/prod' 'type/num/num' A)) > ('type/patricia/ptree' A))).
tt('const/patricia/BRANCH', ty, ![A : $t]: (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A)))) > ('type/patricia/ptree' A))).
tt('const/patricia/BRANCHING_BIT', ty, ('type/num/num' > ('type/num/num' > 'type/num/num'))).
tt('const/patricia/BRANCHING_BIT_tupled', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > 'type/num/num')).
tt('const/patricia/Branch', ty, ![A : $t]: ('type/num/num' > ('type/num/num' > (('type/patricia/ptree' A) > (('type/patricia/ptree' A) > ('type/patricia/ptree' A)))))).
tt('const/patricia/DEPTH', ty, ![A : $t]: (('type/patricia/ptree' A) > 'type/num/num')).
tt('const/patricia/EVERY_LEAF', ty, ![A : $t]: (('type/num/num' > (A > $o)) > (('type/patricia/ptree' A) > $o))).
tt('const/patricia/EXISTS_LEAF', ty, ![A : $t]: (('type/num/num' > (A > $o)) > (('type/patricia/ptree' A) > $o))).
tt('const/patricia/Empty', ty, ![A : $t]: ('type/patricia/ptree' A)).
tt('const/patricia/FIND', ty, ![A : $t]: (('type/patricia/ptree' A) > ('type/num/num' > A))).
tt('const/patricia/INSERT_PTREE', ty, ('type/num/num' > (('type/patricia/ptree' 'type/one/one') > ('type/patricia/ptree' 'type/one/one')))).
tt('const/patricia/IN_PTREE', ty, ('type/num/num' > (('type/patricia/ptree' 'type/one/one') > $o))).
tt('const/patricia/IS_EMPTY', ty, ![A : $t]: (('type/patricia/ptree' A) > $o)).
tt('const/patricia/IS_PTREE', ty, ![A : $t]: (('type/patricia/ptree' A) > $o)).
tt('const/patricia/JOIN', ty, ![A : $t]: (('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/pair/prod' 'type/num/num' ('type/patricia/ptree' A)))) > ('type/patricia/ptree' A))).
tt('const/patricia/KEYS', ty, ![A : $t]: (('type/patricia/ptree' A) > ('type/list/list' 'type/num/num'))).
tt('const/patricia/Leaf', ty, ![A : $t]: ('type/num/num' > (A > ('type/patricia/ptree' A)))).
tt('const/patricia/NUMSET_OF_PTREE', ty, (('type/patricia/ptree' 'type/one/one') > ('type/num/num' > $o))).
tt('const/patricia/PEEK', ty, ![A : $t]: (('type/patricia/ptree' A) > ('type/num/num' > ('type/option/option' A)))).
tt('const/patricia/PEEK_tupled', ty, ![A : $t]: (('type/pair/prod' ('type/patricia/ptree' A) 'type/num/num') > ('type/option/option' A))).
tt('const/patricia/PTREE_OF_NUMSET', ty, (('type/patricia/ptree' 'type/one/one') > (('type/num/num' > $o) > ('type/patricia/ptree' 'type/one/one')))).
tt('const/patricia/REMOVE', ty, ![A : $t]: (('type/patricia/ptree' A) > ('type/num/num' > ('type/patricia/ptree' A)))).
tt('const/patricia/SIZE', ty, ![A : $t]: (('type/patricia/ptree' A) > 'type/num/num')).
tt('const/patricia/TRANSFORM', ty, ![A : $t, B : $t]: ((B > A) > (('type/patricia/ptree' B) > ('type/patricia/ptree' A)))).
tt('const/patricia/TRAVERSE', ty, ![A : $t]: (('type/patricia/ptree' A) > ('type/list/list' 'type/num/num'))).
tt('const/patricia/TRAVERSE_AUX', ty, ![A : $t]: (('type/patricia/ptree' A) > (('type/list/list' 'type/num/num') > ('type/list/list' 'type/num/num')))).
tt('const/patricia/UNION_PTREE', ty, (('type/patricia/ptree' 'type/one/one') > (('type/patricia/ptree' 'type/one/one') > ('type/patricia/ptree' 'type/one/one')))).
tt('const/patricia/ptree_CASE', ty, ![A : $t, B : $t]: (('type/patricia/ptree' A) > (B > (('type/num/num' > (A > B)) > (('type/num/num' > ('type/num/num' > (('type/patricia/ptree' A) > (('type/patricia/ptree' A) > B)))) > B))))).
tt('const/patricia/ptree_size', ty, ![A : $t]: ((A > 'type/num/num') > (('type/patricia/ptree' A) > 'type/num/num'))).
tt('thm/patricia/ptree_TY_DEF_', def, ![A : $t]: (?[rep : (('type/patricia/ptree' A) > ('type/ind_type/recspace' ('type/pair/prod' 'type/num/num' ('type/pair/prod' A 'type/num/num'))))]: (('const/bool/TYPE_DEFINITION' ('type/ind_type/recspace' ('type/pair/prod' 'type/num/num' ('type/pair/prod' A 'type/num/num'))) ('type/patricia/ptree' A)) (^['a0\'' : ('type/ind_type/recspace' ('type/pair/prod' 'type/num/num' ('type/pair/prod' A 'type/num/num')))]: (!['\'ptree\'' : (('type/ind_type/recspace' ('type/pair/prod' 'type/num/num' ('type/pair/prod' A 'type/num/num'))) > $o)]: ((!['a0\'0' : ('type/ind_type/recspace' ('type/pair/prod' 'type/num/num' ('type/pair/prod' A 'type/num/num')))]: ((('a0\'0' = (('const/ind_type/CONSTR' ('type/pair/prod' 'type/num/num' ('type/pair/prod' A 'type/num/num'))) 'const/num/0' (('const/pair/,' 'type/num/num' ('type/pair/prod' A 'type/num/num')) ('const/bool/ARB' 'type/num/num') (('const/pair/,' A 'type/num/num') ('const/bool/ARB' A) ('const/bool/ARB' 'type/num/num'))) (^[n : 'type/num/num']: ('const/ind_type/BOTTOM' ('type/pair/prod' 'type/num/num' ('type/pair/prod' A 'type/num/num')))))) | ((?[a0 : 'type/num/num', a1 : A]: ('a0\'0' = ((^[a00 : 'type/num/num', a10 : A]: (('const/ind_type/CONSTR' ('type/pair/prod' 'type/num/num' ('type/pair/prod' A 'type/num/num'))) ('const/num/SUC' 'const/num/0') (('const/pair/,' 'type/num/num' ('type/pair/prod' A 'type/num/num')) a00 (('const/pair/,' A 'type/num/num') a10 ('const/bool/ARB' 'type/num/num'))) (^[n : 'type/num/num']: ('const/ind_type/BOTTOM' ('type/pair/prod' 'type/num/num' ('type/pair/prod' A 'type/num/num')))))) a0 a1))) | (?[a0 : 'type/num/num', a1 : 'type/num/num', a2 : ('type/ind_type/recspace' ('type/pair/prod' 'type/num/num' ('type/pair/prod' A 'type/num/num'))), a3 : ('type/ind_type/recspace' ('type/pair/prod' 'type/num/num' ('type/pair/prod' A 'type/num/num')))]: (('a0\'0' = ((^[a00 : 'type/num/num', a10 : 'type/num/num', a20 : ('type/ind_type/recspace' ('type/pair/prod' 'type/num/num' ('type/pair/prod' A 'type/num/num'))), a30 : ('type/ind_type/recspace' ('type/pair/prod' 'type/num/num' ('type/pair/prod' A 'type/num/num')))]: (('const/ind_type/CONSTR' ('type/pair/prod' 'type/num/num' ('type/pair/prod' A 'type/num/num'))) ('const/num/SUC' ('const/num/SUC' 'const/num/0')) (('const/pair/,' 'type/num/num' ('type/pair/prod' A 'type/num/num')) a00 (('const/pair/,' A 'type/num/num') ('const/bool/ARB' A) a10)) (('const/ind_type/FCONS' ('type/ind_type/recspace' ('type/pair/prod' 'type/num/num' ('type/pair/prod' A 'type/num/num')))) a20 (('const/ind_type/FCONS' ('type/ind_type/recspace' ('type/pair/prod' 'type/num/num' ('type/pair/prod' A 'type/num/num')))) a30 (^[n : 'type/num/num']: ('const/ind_type/BOTTOM' ('type/pair/prod' 'type/num/num' ('type/pair/prod' A 'type/num/num')))))))) a0 a1 a2 a3)) & (('\'ptree\'' a2) & ('\'ptree\'' a3)))))) => ('\'ptree\'' 'a0\'0'))) => ('\'ptree\'' 'a0\'')))) rep))).
tt('thm/patricia/ptree_case_def_0', def, ![B : $t, A : $t]: (![v : B, f : ('type/num/num' > (A > B)), f1 : ('type/num/num' > ('type/num/num' > (('type/patricia/ptree' A) > (('type/patricia/ptree' A) > B))))]: ((('const/patricia/ptree_CASE' A B) ('const/patricia/Empty' A) v f f1) = v))).
tt('thm/patricia/ptree_case_def_1', def, ![A : $t, B : $t]: (![a0 : 'type/num/num', a1 : A, v : B, f : ('type/num/num' > (A > B)), f1 : ('type/num/num' > ('type/num/num' > (('type/patricia/ptree' A) > (('type/patricia/ptree' A) > B))))]: ((('const/patricia/ptree_CASE' A B) (('const/patricia/Leaf' A) a0 a1) v f f1) = (f a0 a1)))).
tt('thm/patricia/ptree_case_def_e2', def, ![A : $t, B : $t]: (![a0 : 'type/num/num', a1 : 'type/num/num', a2 : ('type/patricia/ptree' A), a3 : ('type/patricia/ptree' A), v : B, f : ('type/num/num' > (A > B)), f1 : ('type/num/num' > ('type/num/num' > (('type/patricia/ptree' A) > (('type/patricia/ptree' A) > B))))]: ((('const/patricia/ptree_CASE' A B) (('const/patricia/Branch' A) a0 a1 a2 a3) v f f1) = (f1 a0 a1 a2 a3)))).
tt('thm/patricia/ptree_size_def_0', def, ![A : $t]: (![f : (A > 'type/num/num')]: ((('const/patricia/ptree_size' A) f ('const/patricia/Empty' A)) = 'const/num/0'))).
tt('thm/patricia/ptree_size_def_1', def, ![A : $t]: (![f : (A > 'type/num/num'), a0 : 'type/num/num', a1 : A]: ((('const/patricia/ptree_size' A) f (('const/patricia/Leaf' A) a0 a1)) = ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) ('const/arithmetic/+' a0 (f a1)))))).
tt('thm/patricia/ptree_size_def_e2', def, ![A : $t]: (![f : (A > 'type/num/num'), a0 : 'type/num/num', a1 : 'type/num/num', a2 : ('type/patricia/ptree' A), a3 : ('type/patricia/ptree' A)]: ((('const/patricia/ptree_size' A) f (('const/patricia/Branch' A) a0 a1 a2 a3)) = ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) ('const/arithmetic/+' a0 ('const/arithmetic/+' a1 ('const/arithmetic/+' (('const/patricia/ptree_size' A) f a2) (('const/patricia/ptree_size' A) f a3)))))))).
tt('thm/patricia/datatype_ptree_', ax, ![A : $t]: (![ptree : (('type/patricia/ptree' A) > (('type/num/num' > (A > ('type/patricia/ptree' A))) > (('type/num/num' > ('type/num/num' > (('type/patricia/ptree' A) > (('type/patricia/ptree' A) > ('type/patricia/ptree' A))))) > $o)))]: (('const/bool/DATATYPE' $o) (ptree ('const/patricia/Empty' A) ('const/patricia/Leaf' A) ('const/patricia/Branch' A))))).
tt('thm/patricia/ptree_11_0', ax, ![A : $t]: (![a0 : 'type/num/num', a1 : A, 'a0\'' : 'type/num/num', 'a1\'' : A]: (((('const/patricia/Leaf' A) a0 a1) = (('const/patricia/Leaf' A) 'a0\'' 'a1\'')) = ((a0 = 'a0\'') & (a1 = 'a1\''))))).
tt('thm/patricia/ptree_11_e1', ax, ![A : $t]: (![a0 : 'type/num/num', a1 : 'type/num/num', a2 : ('type/patricia/ptree' A), a3 : ('type/patricia/ptree' A), 'a0\'' : 'type/num/num', 'a1\'' : 'type/num/num', 'a2\'' : ('type/patricia/ptree' A), 'a3\'' : ('type/patricia/ptree' A)]: (((('const/patricia/Branch' A) a0 a1 a2 a3) = (('const/patricia/Branch' A) 'a0\'' 'a1\'' 'a2\'' 'a3\'')) = ((a0 = 'a0\'') & ((a1 = 'a1\'') & ((a2 = 'a2\'') & (a3 = 'a3\''))))))).
tt('thm/patricia/ptree_distinct_0', ax, ![A : $t]: (![a1 : A, a0 : 'type/num/num']: (~ (('const/patricia/Empty' A) = (('const/patricia/Leaf' A) a0 a1))))).
tt('thm/patricia/ptree_distinct_1', ax, ![A : $t]: (![a3 : ('type/patricia/ptree' A), a2 : ('type/patricia/ptree' A), a1 : 'type/num/num', a0 : 'type/num/num']: (~ (('const/patricia/Empty' A) = (('const/patricia/Branch' A) a0 a1 a2 a3))))).
tt('thm/patricia/ptree_distinct_e2', ax, ![A : $t]: (![a3 : ('type/patricia/ptree' A), a2 : ('type/patricia/ptree' A), 'a1\'' : 'type/num/num', a1 : A, 'a0\'' : 'type/num/num', a0 : 'type/num/num']: (~ ((('const/patricia/Leaf' A) a0 a1) = (('const/patricia/Branch' A) 'a0\'' 'a1\'' a2 a3))))).
tt('thm/patricia/ptree_case_cong_', ax, ![A : $t, B : $t]: (!['v\'' : B, 'f1\'' : ('type/num/num' > ('type/num/num' > (('type/patricia/ptree' A) > (('type/patricia/ptree' A) > B)))), 'f\'' : ('type/num/num' > (A > B)), M : ('type/patricia/ptree' A), 'M\'' : ('type/patricia/ptree' A), v : B, f : ('type/num/num' > (A > B)), f1 : ('type/num/num' > ('type/num/num' > (('type/patricia/ptree' A) > (('type/patricia/ptree' A) > B))))]: (((M = 'M\'') & ((('M\'' = ('const/patricia/Empty' A)) => (v = 'v\'')) & ((![a0 : 'type/num/num', a1 : A]: (('M\'' = (('const/patricia/Leaf' A) a0 a1)) => ((f a0 a1) = ('f\'' a0 a1)))) & (![a0 : 'type/num/num', a1 : 'type/num/num', a2 : ('type/patricia/ptree' A), a3 : ('type/patricia/ptree' A)]: (('M\'' = (('const/patricia/Branch' A) a0 a1 a2 a3)) => ((f1 a0 a1 a2 a3) = ('f1\'' a0 a1 a2 a3))))))) => ((('const/patricia/ptree_CASE' A B) M v f f1) = (('const/patricia/ptree_CASE' A B) 'M\'' 'v\'' 'f\'' 'f1\''))))).
tt('thm/patricia/ptree_nchotomy_', ax, ![A : $t]: (![pp : ('type/patricia/ptree' A)]: ((pp = ('const/patricia/Empty' A)) | ((?[n : 'type/num/num', a : A]: (pp = (('const/patricia/Leaf' A) n a))) | (?[n0 : 'type/num/num', n : 'type/num/num', p : ('type/patricia/ptree' A), p0 : ('type/patricia/ptree' A)]: (pp = (('const/patricia/Branch' A) n0 n p p0))))))).
tt('thm/patricia/ptree_Axiom_', ax, ![A : $t, B : $t]: (![f0 : B, f1 : ('type/num/num' > (A > B)), f2 : ('type/num/num' > ('type/num/num' > (('type/patricia/ptree' A) > (('type/patricia/ptree' A) > (B > (B > B))))))]: (?[fn : (('type/patricia/ptree' A) > B)]: (((fn ('const/patricia/Empty' A)) = f0) & ((![a0 : 'type/num/num', a1 : A]: ((fn (('const/patricia/Leaf' A) a0 a1)) = (f1 a0 a1))) & (![a0 : 'type/num/num', a1 : 'type/num/num', a2 : ('type/patricia/ptree' A), a3 : ('type/patricia/ptree' A)]: ((fn (('const/patricia/Branch' A) a0 a1 a2 a3)) = (f2 a0 a1 a2 a3 (fn a2) (fn a3))))))))).
tt('thm/patricia/ptree_induction_', ax, ![A : $t]: (![P : (('type/patricia/ptree' A) > $o)]: (((P ('const/patricia/Empty' A)) & ((![n : 'type/num/num', a : A]: (P (('const/patricia/Leaf' A) n a))) & (![p : ('type/patricia/ptree' A), p0 : ('type/patricia/ptree' A)]: (((P p) & (P p0)) => (![n : 'type/num/num', n0 : 'type/num/num']: (P (('const/patricia/Branch' A) n0 n p p0))))))) => (![p : ('type/patricia/ptree' A)]: (P p))))).
tt('thm/patricia/BRANCHING_BIT_tupled_primitive_def_', def, ('const/patricia/BRANCHING_BIT_tupled' = (('const/relation/WFREC' ('type/pair/prod' 'type/num/num' 'type/num/num') 'type/num/num') (('const/min/@' (('type/pair/prod' 'type/num/num' 'type/num/num') > (('type/pair/prod' 'type/num/num' 'type/num/num') > $o))) (^[R : (('type/pair/prod' 'type/num/num' 'type/num/num') > (('type/pair/prod' 'type/num/num' 'type/num/num') > $o))]: ((('const/relation/WF' ('type/pair/prod' 'type/num/num' 'type/num/num')) R) & (![p1 : 'type/num/num', p0 : 'type/num/num']: ((~ ((('const/arithmetic/ODD' p0) = ('const/arithmetic/EVEN' p1)) | (p0 = p1))) => (R (('const/pair/,' 'type/num/num' 'type/num/num') ('const/arithmetic/DIV2' p0) ('const/arithmetic/DIV2' p1)) (('const/pair/,' 'type/num/num' 'type/num/num') p0 p1))))))) (^[BRANCHING_BIT_tupled : (('type/pair/prod' 'type/num/num' 'type/num/num') > 'type/num/num'), a : ('type/pair/prod' 'type/num/num' 'type/num/num')]: (('const/pair/pair_CASE' 'type/num/num' 'type/num/num' 'type/num/num') a (^[p0 : 'type/num/num', p1 : 'type/num/num']: (('const/combin/I' 'type/num/num') (('const/bool/COND' 'type/num/num') ((('const/arithmetic/ODD' p0) = ('const/arithmetic/EVEN' p1)) | (p0 = p1)) 'const/num/0' ('const/num/SUC' (BRANCHING_BIT_tupled (('const/pair/,' 'type/num/num' 'type/num/num') ('const/arithmetic/DIV2' p0) ('const/arithmetic/DIV2' p1)))))))))))).
tt('thm/patricia/BRANCHING_BIT_curried_def_', def, (![x : 'type/num/num', x1 : 'type/num/num']: (('const/patricia/BRANCHING_BIT' x x1) = ('const/patricia/BRANCHING_BIT_tupled' (('const/pair/,' 'type/num/num' 'type/num/num') x x1))))).
tt('thm/patricia/BRANCHING_BIT_ind_', ax, (![P : ('type/num/num' > ('type/num/num' > $o))]: ((![p0 : 'type/num/num', p1 : 'type/num/num']: (((~ ((('const/arithmetic/ODD' p0) = ('const/arithmetic/EVEN' p1)) | (p0 = p1))) => (P ('const/arithmetic/DIV2' p0) ('const/arithmetic/DIV2' p1))) => (P p0 p1))) => (![v : 'type/num/num', v1 : 'type/num/num']: (P v v1))))).
tt('thm/patricia/BRANCHING_BIT_def_', ax, (![p1 : 'type/num/num', p0 : 'type/num/num']: (('const/patricia/BRANCHING_BIT' p0 p1) = (('const/bool/COND' 'type/num/num') ((('const/arithmetic/ODD' p0) = ('const/arithmetic/EVEN' p1)) | (p0 = p1)) 'const/num/0' ('const/num/SUC' ('const/patricia/BRANCHING_BIT' ('const/arithmetic/DIV2' p0) ('const/arithmetic/DIV2' p1))))))).
tt('thm/patricia/PEEK_tupled_primitive_def_', def, ![A : $t]: (('const/patricia/PEEK_tupled' A) = (('const/relation/WFREC' ('type/pair/prod' ('type/patricia/ptree' A) 'type/num/num') ('type/option/option' A)) (('const/min/@' (('type/pair/prod' ('type/patricia/ptree' A) 'type/num/num') > (('type/pair/prod' ('type/patricia/ptree' A) 'type/num/num') > $o))) (^[R : (('type/pair/prod' ('type/patricia/ptree' A) 'type/num/num') > (('type/pair/prod' ('type/patricia/ptree' A) 'type/num/num') > $o))]: ((('const/relation/WF' ('type/pair/prod' ('type/patricia/ptree' A) 'type/num/num')) R) & (![p : 'type/num/num', r : ('type/patricia/ptree' A), l : ('type/patricia/ptree' A), k : 'type/num/num', m : 'type/num/num']: (R (('const/pair/,' ('type/patricia/ptree' A) 'type/num/num') (('const/bool/COND' ('type/patricia/ptree' A)) ('const/bit/BIT' m k) l r) k) (('const/pair/,' ('type/patricia/ptree' A) 'type/num/num') (('const/patricia/Branch' A) p m l r) k)))))) (^[PEEK_tupled : (('type/pair/prod' ('type/patricia/ptree' A) 'type/num/num') > ('type/option/option' A)), a : ('type/pair/prod' ('type/patricia/ptree' A) 'type/num/num')]: (('const/pair/pair_CASE' ('type/option/option' A) ('type/patricia/ptree' A) 'type/num/num') a (^[v : ('type/patricia/ptree' A), k : 'type/num/num']: (('const/patricia/ptree_CASE' A ('type/option/option' A)) v (('const/combin/I' ('type/option/option' A)) ('const/option/NONE' A)) (^[j : 'type/num/num', d : A]: (('const/combin/I' ('type/option/option' A)) (('const/bool/COND' ('type/option/option' A)) (k = j) (('const/option/SOME' A) d) ('const/option/NONE' A)))) (^[p : 'type/num/num', m : 'type/num/num', l : ('type/patricia/ptree' A), r : ('type/patricia/ptree' A)]: (('const/combin/I' ('type/option/option' A)) (PEEK_tupled (('const/pair/,' ('type/patricia/ptree' A) 'type/num/num') (('const/bool/COND' ('type/patricia/ptree' A)) ('const/bit/BIT' m k) l r) k))))))))))).
tt('thm/patricia/PEEK_curried_def_', def, ![A : $t]: (![x : ('type/patricia/ptree' A), x1 : 'type/num/num']: ((('const/patricia/PEEK' A) x x1) = (('const/patricia/PEEK_tupled' A) (('const/pair/,' ('type/patricia/ptree' A) 'type/num/num') x x1))))).
tt('thm/patricia/PEEK_ind_', ax, ![A : $t]: (![P : (('type/patricia/ptree' A) > ('type/num/num' > $o))]: (((![k : 'type/num/num']: (P ('const/patricia/Empty' A) k)) & ((![j : 'type/num/num', d : A, k : 'type/num/num']: (P (('const/patricia/Leaf' A) j d) k)) & (![p : 'type/num/num', m : 'type/num/num', l : ('type/patricia/ptree' A), r : ('type/patricia/ptree' A), k : 'type/num/num']: ((P (('const/bool/COND' ('type/patricia/ptree' A)) ('const/bit/BIT' m k) l r) k) => (P (('const/patricia/Branch' A) p m l r) k))))) => (![v : ('type/patricia/ptree' A), v1 : 'type/num/num']: (P v v1))))).
tt('thm/patricia/PEEK_def_0', ax, ![A : $t]: (![k : 'type/num/num']: ((('const/patricia/PEEK' A) ('const/patricia/Empty' A) k) = ('const/option/NONE' A)))).
tt('thm/patricia/PEEK_def_1', ax, ![A : $t]: (![k : 'type/num/num', j : 'type/num/num', d : A]: ((('const/patricia/PEEK' A) (('const/patricia/Leaf' A) j d) k) = (('const/bool/COND' ('type/option/option' A)) (k = j) (('const/option/SOME' A) d) ('const/option/NONE' A))))).
tt('thm/patricia/PEEK_def_e2', ax, ![A : $t]: (![r : ('type/patricia/ptree' A), p : 'type/num/num', m : 'type/num/num', l : ('type/patricia/ptree' A), k : 'type/num/num']: ((('const/patricia/PEEK' A) (('const/patricia/Branch' A) p m l r) k) = (('const/patricia/PEEK' A) (('const/bool/COND' ('type/patricia/ptree' A)) ('const/bit/BIT' m k) l r) k)))).
tt('thm/patricia/JOIN_def_', def, ![A : $t]: (![p0 : 'type/num/num', t0 : ('type/patricia/ptree' A), p1 : 'type/num/num', t1 : ('type/patricia/ptree' A)]: ((('const/patricia/JOIN' A) (('const/pair/,' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/pair/prod' 'type/num/num' ('type/patricia/ptree' A)))) p0 (('const/pair/,' ('type/patricia/ptree' A) ('type/pair/prod' 'type/num/num' ('type/patricia/ptree' A))) t0 (('const/pair/,' 'type/num/num' ('type/patricia/ptree' A)) p1 t1)))) = (('const/bool/LET' 'type/num/num' ('type/patricia/ptree' A)) (^[m : 'type/num/num']: (('const/bool/COND' ('type/patricia/ptree' A)) ('const/bit/BIT' m p0) (('const/patricia/Branch' A) ('const/bit/MOD_2EXP' m p0) m t0 t1) (('const/patricia/Branch' A) ('const/bit/MOD_2EXP' m p0) m t1 t0))) ('const/patricia/BRANCHING_BIT' p0 p1))))).
tt('thm/patricia/ADD_tupled_primitive_def_', def, ![A : $t]: (('const/patricia/ADD_tupled' A) = (('const/relation/WFREC' ('type/pair/prod' ('type/patricia/ptree' A) ('type/pair/prod' 'type/num/num' A)) ('type/patricia/ptree' A)) (('const/min/@' (('type/pair/prod' ('type/patricia/ptree' A) ('type/pair/prod' 'type/num/num' A)) > (('type/pair/prod' ('type/patricia/ptree' A) ('type/pair/prod' 'type/num/num' A)) > $o))) (^[R : (('type/pair/prod' ('type/patricia/ptree' A) ('type/pair/prod' 'type/num/num' A)) > (('type/pair/prod' ('type/patricia/ptree' A) ('type/pair/prod' 'type/num/num' A)) > $o))]: ((('const/relation/WF' ('type/pair/prod' ('type/patricia/ptree' A) ('type/pair/prod' 'type/num/num' A))) R) & ((![l : ('type/patricia/ptree' A), e : A, r : ('type/patricia/ptree' A), p : 'type/num/num', k : 'type/num/num', m : 'type/num/num']: ((('const/bit/MOD_2EXP_EQ' m k p) & (~ ('const/bit/BIT' m k))) => (R (('const/pair/,' ('type/patricia/ptree' A) ('type/pair/prod' 'type/num/num' A)) r (('const/pair/,' 'type/num/num' A) k e)) (('const/pair/,' ('type/patricia/ptree' A) ('type/pair/prod' 'type/num/num' A)) (('const/patricia/Branch' A) p m l r) (('const/pair/,' 'type/num/num' A) k e))))) & (![r : ('type/patricia/ptree' A), e : A, l : ('type/patricia/ptree' A), p : 'type/num/num', k : 'type/num/num', m : 'type/num/num']: ((('const/bit/MOD_2EXP_EQ' m k p) & ('const/bit/BIT' m k)) => (R (('const/pair/,' ('type/patricia/ptree' A) ('type/pair/prod' 'type/num/num' A)) l (('const/pair/,' 'type/num/num' A) k e)) (('const/pair/,' ('type/patricia/ptree' A) ('type/pair/prod' 'type/num/num' A)) (('const/patricia/Branch' A) p m l r) (('const/pair/,' 'type/num/num' A) k e))))))))) (^[ADD_tupled : (('type/pair/prod' ('type/patricia/ptree' A) ('type/pair/prod' 'type/num/num' A)) > ('type/patricia/ptree' A)), a : ('type/pair/prod' ('type/patricia/ptree' A) ('type/pair/prod' 'type/num/num' A))]: (('const/pair/pair_CASE' ('type/patricia/ptree' A) ('type/patricia/ptree' A) ('type/pair/prod' 'type/num/num' A)) a (^[v : ('type/patricia/ptree' A), v1 : ('type/pair/prod' 'type/num/num' A)]: (('const/pair/pair_CASE' ('type/patricia/ptree' A) 'type/num/num' A) v1 (^[k : 'type/num/num', e : A]: (('const/patricia/ptree_CASE' A ('type/patricia/ptree' A)) v (('const/combin/I' ('type/patricia/ptree' A)) (('const/patricia/Leaf' A) k e)) (^[j : 'type/num/num', d : A]: (('const/combin/I' ('type/patricia/ptree' A)) (('const/bool/COND' ('type/patricia/ptree' A)) (j = k) (('const/patricia/Leaf' A) k e) (('const/patricia/JOIN' A) (('const/pair/,' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/pair/prod' 'type/num/num' ('type/patricia/ptree' A)))) k (('const/pair/,' ('type/patricia/ptree' A) ('type/pair/prod' 'type/num/num' ('type/patricia/ptree' A))) (('const/patricia/Leaf' A) k e) (('const/pair/,' 'type/num/num' ('type/patricia/ptree' A)) j (('const/patricia/Leaf' A) j d)))))))) (^[p : 'type/num/num', m : 'type/num/num', l : ('type/patricia/ptree' A), r : ('type/patricia/ptree' A)]: (('const/combin/I' ('type/patricia/ptree' A)) (('const/bool/COND' ('type/patricia/ptree' A)) ('const/bit/MOD_2EXP_EQ' m k p) (('const/bool/COND' ('type/patricia/ptree' A)) ('const/bit/BIT' m k) (('const/patricia/Branch' A) p m (ADD_tupled (('const/pair/,' ('type/patricia/ptree' A) ('type/pair/prod' 'type/num/num' A)) l (('const/pair/,' 'type/num/num' A) k e))) r) (('const/patricia/Branch' A) p m l (ADD_tupled (('const/pair/,' ('type/patricia/ptree' A) ('type/pair/prod' 'type/num/num' A)) r (('const/pair/,' 'type/num/num' A) k e))))) (('const/patricia/JOIN' A) (('const/pair/,' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/pair/prod' 'type/num/num' ('type/patricia/ptree' A)))) k (('const/pair/,' ('type/patricia/ptree' A) ('type/pair/prod' 'type/num/num' ('type/patricia/ptree' A))) (('const/patricia/Leaf' A) k e) (('const/pair/,' 'type/num/num' ('type/patricia/ptree' A)) p (('const/patricia/Branch' A) p m l r))))))))))))))))).
tt('thm/patricia/ADD_curried_def_', def, ![A : $t]: (![x : ('type/patricia/ptree' A), x1 : ('type/pair/prod' 'type/num/num' A)]: ((('const/patricia/ADD' A) x x1) = (('const/patricia/ADD_tupled' A) (('const/pair/,' ('type/patricia/ptree' A) ('type/pair/prod' 'type/num/num' A)) x x1))))).
tt('thm/patricia/ADD_ind_', ax, ![A : $t]: (![P : (('type/patricia/ptree' A) > (('type/pair/prod' 'type/num/num' A) > $o))]: (((![k : 'type/num/num', e : A]: (P ('const/patricia/Empty' A) (('const/pair/,' 'type/num/num' A) k e))) & ((![j : 'type/num/num', d : A, k : 'type/num/num', e : A]: (P (('const/patricia/Leaf' A) j d) (('const/pair/,' 'type/num/num' A) k e))) & (![p : 'type/num/num', m : 'type/num/num', l : ('type/patricia/ptree' A), r : ('type/patricia/ptree' A), k : 'type/num/num', e : A]: ((((('const/bit/MOD_2EXP_EQ' m k p) & (~ ('const/bit/BIT' m k))) => (P r (('const/pair/,' 'type/num/num' A) k e))) & ((('const/bit/MOD_2EXP_EQ' m k p) & ('const/bit/BIT' m k)) => (P l (('const/pair/,' 'type/num/num' A) k e)))) => (P (('const/patricia/Branch' A) p m l r) (('const/pair/,' 'type/num/num' A) k e)))))) => (![v : ('type/patricia/ptree' A), v1 : 'type/num/num', v2 : A]: (P v (('const/pair/,' 'type/num/num' A) v1 v2)))))).
tt('thm/patricia/ADD_def_0', ax, ![A : $t]: (![k : 'type/num/num', e : A]: ((('const/patricia/ADD' A) ('const/patricia/Empty' A) (('const/pair/,' 'type/num/num' A) k e)) = (('const/patricia/Leaf' A) k e)))).
tt('thm/patricia/ADD_def_1', ax, ![A : $t]: (![k : 'type/num/num', j : 'type/num/num', e : A, d : A]: ((('const/patricia/ADD' A) (('const/patricia/Leaf' A) j d) (('const/pair/,' 'type/num/num' A) k e)) = (('const/bool/COND' ('type/patricia/ptree' A)) (j = k) (('const/patricia/Leaf' A) k e) (('const/patricia/JOIN' A) (('const/pair/,' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/pair/prod' 'type/num/num' ('type/patricia/ptree' A)))) k (('const/pair/,' ('type/patricia/ptree' A) ('type/pair/prod' 'type/num/num' ('type/patricia/ptree' A))) (('const/patricia/Leaf' A) k e) (('const/pair/,' 'type/num/num' ('type/patricia/ptree' A)) j (('const/patricia/Leaf' A) j d))))))))).
tt('thm/patricia/ADD_def_e2', ax, ![A : $t]: (![r : ('type/patricia/ptree' A), p : 'type/num/num', m : 'type/num/num', l : ('type/patricia/ptree' A), k : 'type/num/num', e : A]: ((('const/patricia/ADD' A) (('const/patricia/Branch' A) p m l r) (('const/pair/,' 'type/num/num' A) k e)) = (('const/bool/COND' ('type/patricia/ptree' A)) ('const/bit/MOD_2EXP_EQ' m k p) (('const/bool/COND' ('type/patricia/ptree' A)) ('const/bit/BIT' m k) (('const/patricia/Branch' A) p m (('const/patricia/ADD' A) l (('const/pair/,' 'type/num/num' A) k e)) r) (('const/patricia/Branch' A) p m l (('const/patricia/ADD' A) r (('const/pair/,' 'type/num/num' A) k e)))) (('const/patricia/JOIN' A) (('const/pair/,' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/pair/prod' 'type/num/num' ('type/patricia/ptree' A)))) k (('const/pair/,' ('type/patricia/ptree' A) ('type/pair/prod' 'type/num/num' ('type/patricia/ptree' A))) (('const/patricia/Leaf' A) k e) (('const/pair/,' 'type/num/num' ('type/patricia/ptree' A)) p (('const/patricia/Branch' A) p m l r))))))))).
tt('thm/patricia/BRANCH_primitive_def_', def, ![A : $t]: (('const/patricia/BRANCH' A) = (('const/relation/WFREC' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A)))) ('type/patricia/ptree' A)) (('const/min/@' (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A)))) > (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A)))) > $o))) (^[R : (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A)))) > (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A)))) > $o))]: (('const/relation/WF' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A))))) R))) (^[BRANCH : (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A)))) > ('type/patricia/ptree' A)), a : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A))))]: (('const/pair/pair_CASE' ('type/patricia/ptree' A) 'type/num/num' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A)))) a (^[p : 'type/num/num', v1 : ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A)))]: (('const/pair/pair_CASE' ('type/patricia/ptree' A) 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A))) v1 (^[m : 'type/num/num', v3 : ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A))]: (('const/pair/pair_CASE' ('type/patricia/ptree' A) ('type/patricia/ptree' A) ('type/patricia/ptree' A)) v3 (^[v4 : ('type/patricia/ptree' A), t : ('type/patricia/ptree' A)]: (('const/patricia/ptree_CASE' A ('type/patricia/ptree' A)) v4 (('const/combin/I' ('type/patricia/ptree' A)) t) (^[v18 : 'type/num/num', v19 : A]: (('const/patricia/ptree_CASE' A ('type/patricia/ptree' A)) t (('const/combin/I' ('type/patricia/ptree' A)) (('const/patricia/Leaf' A) v18 v19)) (^[v30 : 'type/num/num', v31 : A]: (('const/combin/I' ('type/patricia/ptree' A)) (('const/patricia/Branch' A) p m (('const/patricia/Leaf' A) v18 v19) (('const/patricia/Leaf' A) v30 v31)))) (^[v32 : 'type/num/num', v33 : 'type/num/num', v34 : ('type/patricia/ptree' A), v35 : ('type/patricia/ptree' A)]: (('const/combin/I' ('type/patricia/ptree' A)) (('const/patricia/Branch' A) p m (('const/patricia/Leaf' A) v18 v19) (('const/patricia/Branch' A) v32 v33 v34 v35)))))) (^[v20 : 'type/num/num', v21 : 'type/num/num', v22 : ('type/patricia/ptree' A), v23 : ('type/patricia/ptree' A)]: (('const/patricia/ptree_CASE' A ('type/patricia/ptree' A)) t (('const/combin/I' ('type/patricia/ptree' A)) (('const/patricia/Branch' A) v20 v21 v22 v23)) (^[v42 : 'type/num/num', v43 : A]: (('const/combin/I' ('type/patricia/ptree' A)) (('const/patricia/Branch' A) p m (('const/patricia/Branch' A) v20 v21 v22 v23) (('const/patricia/Leaf' A) v42 v43)))) (^[v44 : 'type/num/num', v45 : 'type/num/num', v46 : ('type/patricia/ptree' A), v47 : ('type/patricia/ptree' A)]: (('const/combin/I' ('type/patricia/ptree' A)) (('const/patricia/Branch' A) p m (('const/patricia/Branch' A) v20 v21 v22 v23) (('const/patricia/Branch' A) v44 v45 v46 v47))))))))))))))))).
tt('thm/patricia/BRANCH_ind_', ax, ![A : $t]: (![P : (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A)))) > $o)]: (((![p : 'type/num/num', m : 'type/num/num', t : ('type/patricia/ptree' A)]: (P (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A)))) p (('const/pair/,' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A))) m (('const/pair/,' ('type/patricia/ptree' A) ('type/patricia/ptree' A)) ('const/patricia/Empty' A) t))))) & ((![p : 'type/num/num', m : 'type/num/num', v6 : 'type/num/num', v7 : A]: (P (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A)))) p (('const/pair/,' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A))) m (('const/pair/,' ('type/patricia/ptree' A) ('type/patricia/ptree' A)) (('const/patricia/Leaf' A) v6 v7) ('const/patricia/Empty' A)))))) & ((![p : 'type/num/num', m : 'type/num/num', v8 : 'type/num/num', v9 : 'type/num/num', v10 : ('type/patricia/ptree' A), v11 : ('type/patricia/ptree' A)]: (P (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A)))) p (('const/pair/,' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A))) m (('const/pair/,' ('type/patricia/ptree' A) ('type/patricia/ptree' A)) (('const/patricia/Branch' A) v8 v9 v10 v11) ('const/patricia/Empty' A)))))) & ((![p : 'type/num/num', m : 'type/num/num', v12 : 'type/num/num', v13 : A, v24 : 'type/num/num', v25 : A]: (P (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A)))) p (('const/pair/,' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A))) m (('const/pair/,' ('type/patricia/ptree' A) ('type/patricia/ptree' A)) (('const/patricia/Leaf' A) v12 v13) (('const/patricia/Leaf' A) v24 v25)))))) & ((![p : 'type/num/num', m : 'type/num/num', v12 : 'type/num/num', v13 : A, v26 : 'type/num/num', v27 : 'type/num/num', v28 : ('type/patricia/ptree' A), v29 : ('type/patricia/ptree' A)]: (P (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A)))) p (('const/pair/,' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A))) m (('const/pair/,' ('type/patricia/ptree' A) ('type/patricia/ptree' A)) (('const/patricia/Leaf' A) v12 v13) (('const/patricia/Branch' A) v26 v27 v28 v29)))))) & ((![p : 'type/num/num', m : 'type/num/num', v14 : 'type/num/num', v15 : 'type/num/num', v16 : ('type/patricia/ptree' A), v17 : ('type/patricia/ptree' A), v36 : 'type/num/num', v37 : A]: (P (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A)))) p (('const/pair/,' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A))) m (('const/pair/,' ('type/patricia/ptree' A) ('type/patricia/ptree' A)) (('const/patricia/Branch' A) v14 v15 v16 v17) (('const/patricia/Leaf' A) v36 v37)))))) & (![p : 'type/num/num', m : 'type/num/num', v14 : 'type/num/num', v15 : 'type/num/num', v16 : ('type/patricia/ptree' A), v17 : ('type/patricia/ptree' A), v38 : 'type/num/num', v39 : 'type/num/num', v40 : ('type/patricia/ptree' A), v41 : ('type/patricia/ptree' A)]: (P (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A)))) p (('const/pair/,' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A))) m (('const/pair/,' ('type/patricia/ptree' A) ('type/patricia/ptree' A)) (('const/patricia/Branch' A) v14 v15 v16 v17) (('const/patricia/Branch' A) v38 v39 v40 v41)))))))))))) => (![v : 'type/num/num', v1 : 'type/num/num', v2 : ('type/patricia/ptree' A), v3 : ('type/patricia/ptree' A)]: (P (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A)))) v (('const/pair/,' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A))) v1 (('const/pair/,' ('type/patricia/ptree' A) ('type/patricia/ptree' A)) v2 v3)))))))).
tt('thm/patricia/BRANCH_def_0', ax, ![A : $t]: (![t : ('type/patricia/ptree' A), p : 'type/num/num', m : 'type/num/num']: ((('const/patricia/BRANCH' A) (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A)))) p (('const/pair/,' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A))) m (('const/pair/,' ('type/patricia/ptree' A) ('type/patricia/ptree' A)) ('const/patricia/Empty' A) t)))) = t))).
tt('thm/patricia/BRANCH_def_1', ax, ![A : $t]: (![v7 : A, v6 : 'type/num/num', p : 'type/num/num', m : 'type/num/num']: ((('const/patricia/BRANCH' A) (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A)))) p (('const/pair/,' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A))) m (('const/pair/,' ('type/patricia/ptree' A) ('type/patricia/ptree' A)) (('const/patricia/Leaf' A) v6 v7) ('const/patricia/Empty' A))))) = (('const/patricia/Leaf' A) v6 v7)))).
tt('thm/patricia/BRANCH_def_2', ax, ![A : $t]: (![v9 : 'type/num/num', v8 : 'type/num/num', v11 : ('type/patricia/ptree' A), v10 : ('type/patricia/ptree' A), p : 'type/num/num', m : 'type/num/num']: ((('const/patricia/BRANCH' A) (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A)))) p (('const/pair/,' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A))) m (('const/pair/,' ('type/patricia/ptree' A) ('type/patricia/ptree' A)) (('const/patricia/Branch' A) v8 v9 v10 v11) ('const/patricia/Empty' A))))) = (('const/patricia/Branch' A) v8 v9 v10 v11)))).
tt('thm/patricia/BRANCH_def_3', ax, ![A : $t]: (![v25 : A, v24 : 'type/num/num', v13 : A, v12 : 'type/num/num', p : 'type/num/num', m : 'type/num/num']: ((('const/patricia/BRANCH' A) (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A)))) p (('const/pair/,' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A))) m (('const/pair/,' ('type/patricia/ptree' A) ('type/patricia/ptree' A)) (('const/patricia/Leaf' A) v12 v13) (('const/patricia/Leaf' A) v24 v25))))) = (('const/patricia/Branch' A) p m (('const/patricia/Leaf' A) v12 v13) (('const/patricia/Leaf' A) v24 v25))))).
tt('thm/patricia/BRANCH_def_4', ax, ![A : $t]: (![v29 : ('type/patricia/ptree' A), v28 : ('type/patricia/ptree' A), v27 : 'type/num/num', v26 : 'type/num/num', v13 : A, v12 : 'type/num/num', p : 'type/num/num', m : 'type/num/num']: ((('const/patricia/BRANCH' A) (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A)))) p (('const/pair/,' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A))) m (('const/pair/,' ('type/patricia/ptree' A) ('type/patricia/ptree' A)) (('const/patricia/Leaf' A) v12 v13) (('const/patricia/Branch' A) v26 v27 v28 v29))))) = (('const/patricia/Branch' A) p m (('const/patricia/Leaf' A) v12 v13) (('const/patricia/Branch' A) v26 v27 v28 v29))))).
tt('thm/patricia/BRANCH_def_5', ax, ![A : $t]: (![v37 : A, v36 : 'type/num/num', v17 : ('type/patricia/ptree' A), v16 : ('type/patricia/ptree' A), v15 : 'type/num/num', v14 : 'type/num/num', p : 'type/num/num', m : 'type/num/num']: ((('const/patricia/BRANCH' A) (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A)))) p (('const/pair/,' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A))) m (('const/pair/,' ('type/patricia/ptree' A) ('type/patricia/ptree' A)) (('const/patricia/Branch' A) v14 v15 v16 v17) (('const/patricia/Leaf' A) v36 v37))))) = (('const/patricia/Branch' A) p m (('const/patricia/Branch' A) v14 v15 v16 v17) (('const/patricia/Leaf' A) v36 v37))))).
tt('thm/patricia/BRANCH_def_e6', ax, ![A : $t]: (![v41 : ('type/patricia/ptree' A), v40 : ('type/patricia/ptree' A), v39 : 'type/num/num', v38 : 'type/num/num', v17 : ('type/patricia/ptree' A), v16 : ('type/patricia/ptree' A), v15 : 'type/num/num', v14 : 'type/num/num', p : 'type/num/num', m : 'type/num/num']: ((('const/patricia/BRANCH' A) (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A)))) p (('const/pair/,' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A))) m (('const/pair/,' ('type/patricia/ptree' A) ('type/patricia/ptree' A)) (('const/patricia/Branch' A) v14 v15 v16 v17) (('const/patricia/Branch' A) v38 v39 v40 v41))))) = (('const/patricia/Branch' A) p m (('const/patricia/Branch' A) v14 v15 v16 v17) (('const/patricia/Branch' A) v38 v39 v40 v41))))).
tt('thm/patricia/REMOVE_def_0', def, ![A : $t]: (![k : 'type/num/num']: ((('const/patricia/REMOVE' A) ('const/patricia/Empty' A) k) = ('const/patricia/Empty' A)))).
tt('thm/patricia/REMOVE_def_1', def, ![A : $t]: (![j : 'type/num/num', d : A, k : 'type/num/num']: ((('const/patricia/REMOVE' A) (('const/patricia/Leaf' A) j d) k) = (('const/bool/COND' ('type/patricia/ptree' A)) (j = k) ('const/patricia/Empty' A) (('const/patricia/Leaf' A) j d))))).
tt('thm/patricia/REMOVE_def_e2', def, ![A : $t]: (![p : 'type/num/num', m : 'type/num/num', l : ('type/patricia/ptree' A), r : ('type/patricia/ptree' A), k : 'type/num/num']: ((('const/patricia/REMOVE' A) (('const/patricia/Branch' A) p m l r) k) = (('const/bool/COND' ('type/patricia/ptree' A)) ('const/bit/MOD_2EXP_EQ' m k p) (('const/bool/COND' ('type/patricia/ptree' A)) ('const/bit/BIT' m k) (('const/patricia/BRANCH' A) (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A)))) p (('const/pair/,' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A))) m (('const/pair/,' ('type/patricia/ptree' A) ('type/patricia/ptree' A)) (('const/patricia/REMOVE' A) l k) r)))) (('const/patricia/BRANCH' A) (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A)))) p (('const/pair/,' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A))) m (('const/pair/,' ('type/patricia/ptree' A) ('type/patricia/ptree' A)) l (('const/patricia/REMOVE' A) r k)))))) (('const/patricia/Branch' A) p m l r))))).
tt('thm/patricia/TRAVERSE_AUX_def_0', def, ![A : $t]: (![a : ('type/list/list' 'type/num/num')]: ((('const/patricia/TRAVERSE_AUX' A) ('const/patricia/Empty' A) a) = a))).
tt('thm/patricia/TRAVERSE_AUX_def_1', def, ![A : $t]: (![k : 'type/num/num', d : A, a : ('type/list/list' 'type/num/num')]: ((('const/patricia/TRAVERSE_AUX' A) (('const/patricia/Leaf' A) k d) a) = (('const/list/CONS' 'type/num/num') k a)))).
tt('thm/patricia/TRAVERSE_AUX_def_e2', def, ![A : $t]: (![p : 'type/num/num', m : 'type/num/num', l : ('type/patricia/ptree' A), r : ('type/patricia/ptree' A), a : ('type/list/list' 'type/num/num')]: ((('const/patricia/TRAVERSE_AUX' A) (('const/patricia/Branch' A) p m l r) a) = (('const/patricia/TRAVERSE_AUX' A) l (('const/patricia/TRAVERSE_AUX' A) r a))))).
tt('thm/patricia/TRAVERSE_def_0', def, ![A : $t]: ((('const/patricia/TRAVERSE' A) ('const/patricia/Empty' A)) = ('const/list/NIL' 'type/num/num'))).
tt('thm/patricia/TRAVERSE_def_1', def, ![A : $t]: (![j : 'type/num/num', d : A]: ((('const/patricia/TRAVERSE' A) (('const/patricia/Leaf' A) j d)) = (('const/list/CONS' 'type/num/num') j ('const/list/NIL' 'type/num/num'))))).
tt('thm/patricia/TRAVERSE_def_e2', def, ![A : $t]: (![p : 'type/num/num', m : 'type/num/num', l : ('type/patricia/ptree' A), r : ('type/patricia/ptree' A)]: ((('const/patricia/TRAVERSE' A) (('const/patricia/Branch' A) p m l r)) = (('const/list/APPEND' 'type/num/num') (('const/patricia/TRAVERSE' A) l) (('const/patricia/TRAVERSE' A) r))))).
tt('thm/patricia/KEYS_def_', def, ![A : $t]: (![t : ('type/patricia/ptree' A)]: ((('const/patricia/KEYS' A) t) = (('const/sorting/QSORT' 'type/num/num') 'const/prim_rec/<' (('const/patricia/TRAVERSE' A) t))))).
tt('thm/patricia/TRANSFORM_def_0', def, ![A : $t, B : $t]: (![f : (B > A)]: ((('const/patricia/TRANSFORM' A B) f ('const/patricia/Empty' B)) = ('const/patricia/Empty' A)))).
tt('thm/patricia/TRANSFORM_def_1', def, ![B : $t, A : $t]: (![f : (B > A), j : 'type/num/num', d : B]: ((('const/patricia/TRANSFORM' A B) f (('const/patricia/Leaf' B) j d)) = (('const/patricia/Leaf' A) j (f d))))).
tt('thm/patricia/TRANSFORM_def_e2', def, ![B : $t, A : $t]: (![f : (B > A), p : 'type/num/num', m : 'type/num/num', l : ('type/patricia/ptree' B), r : ('type/patricia/ptree' B)]: ((('const/patricia/TRANSFORM' A B) f (('const/patricia/Branch' B) p m l r)) = (('const/patricia/Branch' A) p m (('const/patricia/TRANSFORM' A B) f l) (('const/patricia/TRANSFORM' A B) f r))))).
tt('thm/patricia/EVERY_LEAF_def_0', def, ![A : $t]: (![P : ('type/num/num' > (A > $o))]: ((('const/patricia/EVERY_LEAF' A) P ('const/patricia/Empty' A)) = $true))).
tt('thm/patricia/EVERY_LEAF_def_1', def, ![A : $t]: (![P : ('type/num/num' > (A > $o)), j : 'type/num/num', d : A]: ((('const/patricia/EVERY_LEAF' A) P (('const/patricia/Leaf' A) j d)) = (P j d)))).
tt('thm/patricia/EVERY_LEAF_def_e2', def, ![A : $t]: (![P : ('type/num/num' > (A > $o)), p : 'type/num/num', m : 'type/num/num', l : ('type/patricia/ptree' A), r : ('type/patricia/ptree' A)]: ((('const/patricia/EVERY_LEAF' A) P (('const/patricia/Branch' A) p m l r)) = ((('const/patricia/EVERY_LEAF' A) P l) & (('const/patricia/EVERY_LEAF' A) P r))))).
tt('thm/patricia/EXISTS_LEAF_def_0', def, ![A : $t]: (![P : ('type/num/num' > (A > $o))]: ((('const/patricia/EXISTS_LEAF' A) P ('const/patricia/Empty' A)) = $false))).
tt('thm/patricia/EXISTS_LEAF_def_1', def, ![A : $t]: (![P : ('type/num/num' > (A > $o)), j : 'type/num/num', d : A]: ((('const/patricia/EXISTS_LEAF' A) P (('const/patricia/Leaf' A) j d)) = (P j d)))).
tt('thm/patricia/EXISTS_LEAF_def_e2', def, ![A : $t]: (![P : ('type/num/num' > (A > $o)), p : 'type/num/num', m : 'type/num/num', l : ('type/patricia/ptree' A), r : ('type/patricia/ptree' A)]: ((('const/patricia/EXISTS_LEAF' A) P (('const/patricia/Branch' A) p m l r)) = ((('const/patricia/EXISTS_LEAF' A) P l) | (('const/patricia/EXISTS_LEAF' A) P r))))).
tt('thm/patricia/SIZE_def_', def, ![A : $t]: (![t : ('type/patricia/ptree' A)]: ((('const/patricia/SIZE' A) t) = (('const/list/LENGTH' 'type/num/num') (('const/patricia/TRAVERSE' A) t))))).
tt('thm/patricia/DEPTH_def_0', def, ![A : $t]: ((('const/patricia/DEPTH' A) ('const/patricia/Empty' A)) = 'const/num/0')).
tt('thm/patricia/DEPTH_def_1', def, ![A : $t]: (![j : 'type/num/num', d : A]: ((('const/patricia/DEPTH' A) (('const/patricia/Leaf' A) j d)) = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/patricia/DEPTH_def_e2', def, ![A : $t]: (![p : 'type/num/num', m : 'type/num/num', l : ('type/patricia/ptree' A), r : ('type/patricia/ptree' A)]: ((('const/patricia/DEPTH' A) (('const/patricia/Branch' A) p m l r)) = ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) ('const/arithmetic/MAX' (('const/patricia/DEPTH' A) l) (('const/patricia/DEPTH' A) r)))))).
tt('thm/patricia/IS_PTREE_def_0', def, ![A : $t]: ((('const/patricia/IS_PTREE' A) ('const/patricia/Empty' A)) = $true)).
tt('thm/patricia/IS_PTREE_def_1', def, ![A : $t]: (![k : 'type/num/num', d : A]: ((('const/patricia/IS_PTREE' A) (('const/patricia/Leaf' A) k d)) = $true))).
tt('thm/patricia/IS_PTREE_def_e2', def, ![A : $t]: (![p : 'type/num/num', m : 'type/num/num', l : ('type/patricia/ptree' A), r : ('type/patricia/ptree' A)]: ((('const/patricia/IS_PTREE' A) (('const/patricia/Branch' A) p m l r)) = (('const/prim_rec/<' p ('const/arithmetic/EXP' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) m)) & ((('const/patricia/IS_PTREE' A) l) & ((('const/patricia/IS_PTREE' A) r) & ((~ (l = ('const/patricia/Empty' A))) & ((~ (r = ('const/patricia/Empty' A))) & ((('const/patricia/EVERY_LEAF' A) (^[k : 'type/num/num', d : A]: (('const/bit/MOD_2EXP_EQ' m k p) & ('const/bit/BIT' m k))) l) & (('const/patricia/EVERY_LEAF' A) (^[k : 'type/num/num', d : A]: (('const/bit/MOD_2EXP_EQ' m k p) & (~ ('const/bit/BIT' m k)))) r)))))))))).
tt('thm/patricia/IN_PTREE_def_', def, (![n : 'type/num/num', t : ('type/patricia/ptree' 'type/one/one')]: (('const/patricia/IN_PTREE' n t) = (('const/option/IS_SOME' 'type/one/one') (('const/patricia/PEEK' 'type/one/one') t n))))).
tt('thm/patricia/INSERT_PTREE_def_', def, (![n : 'type/num/num', t : ('type/patricia/ptree' 'type/one/one')]: (('const/patricia/INSERT_PTREE' n t) = (('const/patricia/ADD' 'type/one/one') t (('const/pair/,' 'type/num/num' 'type/one/one') n 'const/one/one'))))).
tt('thm/patricia/PTREE_OF_NUMSET_def_', def, (![t : ('type/patricia/ptree' 'type/one/one'), s : ('type/num/num' > $o)]: (('const/patricia/PTREE_OF_NUMSET' t s) = (('const/list/FOLDL' 'type/num/num' ('type/patricia/ptree' 'type/one/one')) (('const/combin/C' 'type/num/num' ('type/patricia/ptree' 'type/one/one') ('type/patricia/ptree' 'type/one/one')) 'const/patricia/INSERT_PTREE') t (('const/list/SET_TO_LIST' 'type/num/num') s))))).
tt('thm/patricia/NUMSET_OF_PTREE_def_', def, (![t : ('type/patricia/ptree' 'type/one/one')]: (('const/patricia/NUMSET_OF_PTREE' t) = (('const/list/LIST_TO_SET' 'type/num/num') (('const/patricia/TRAVERSE' 'type/one/one') t))))).
tt('thm/patricia/UNION_PTREE_def_', def, (![t1 : ('type/patricia/ptree' 'type/one/one'), t2 : ('type/patricia/ptree' 'type/one/one')]: (('const/patricia/UNION_PTREE' t1 t2) = ('const/patricia/PTREE_OF_NUMSET' t1 ('const/patricia/NUMSET_OF_PTREE' t2))))).
tt('thm/patricia/IS_EMPTY_primitive_def_', def, ![A : $t]: (('const/patricia/IS_EMPTY' A) = (('const/relation/WFREC' ('type/patricia/ptree' A) $o) (('const/min/@' (('type/patricia/ptree' A) > (('type/patricia/ptree' A) > $o))) (^[R : (('type/patricia/ptree' A) > (('type/patricia/ptree' A) > $o))]: (('const/relation/WF' ('type/patricia/ptree' A)) R))) (^[IS_EMPTY : (('type/patricia/ptree' A) > $o), a : ('type/patricia/ptree' A)]: (('const/patricia/ptree_CASE' A $o) a (('const/combin/I' $o) $true) (^[v6 : 'type/num/num', v7 : A]: (('const/combin/I' $o) $false)) (^[v8 : 'type/num/num', v9 : 'type/num/num', v10 : ('type/patricia/ptree' A), v11 : ('type/patricia/ptree' A)]: (('const/combin/I' $o) $false))))))).
tt('thm/patricia/IS_EMPTY_ind_', ax, ![A : $t]: (![P : (('type/patricia/ptree' A) > $o)]: (((P ('const/patricia/Empty' A)) & ((![v : 'type/num/num', v1 : A]: (P (('const/patricia/Leaf' A) v v1))) & (![v2 : 'type/num/num', v3 : 'type/num/num', v4 : ('type/patricia/ptree' A), v5 : ('type/patricia/ptree' A)]: (P (('const/patricia/Branch' A) v2 v3 v4 v5))))) => (![v : ('type/patricia/ptree' A)]: (P v))))).
tt('thm/patricia/IS_EMPTY_def_0', ax, ![A : $t]: ((('const/patricia/IS_EMPTY' A) ('const/patricia/Empty' A)) = $true)).
tt('thm/patricia/IS_EMPTY_def_1', ax, ![A : $t]: (![v1 : A, v : 'type/num/num']: ((('const/patricia/IS_EMPTY' A) (('const/patricia/Leaf' A) v v1)) = $false))).
tt('thm/patricia/IS_EMPTY_def_e2', ax, ![A : $t]: (![v5 : ('type/patricia/ptree' A), v4 : ('type/patricia/ptree' A), v3 : 'type/num/num', v2 : 'type/num/num']: ((('const/patricia/IS_EMPTY' A) (('const/patricia/Branch' A) v2 v3 v4 v5)) = $false))).
tt('thm/patricia/FIND_def_', def, ![A : $t]: (![t : ('type/patricia/ptree' A), k : 'type/num/num']: ((('const/patricia/FIND' A) t k) = (('const/option/THE' A) (('const/patricia/PEEK' A) t k))))).
tt('thm/patricia/ADD_LIST_def_', def, ![A : $t]: (('const/patricia/ADD_LIST' A) = (('const/list/FOLDL' ('type/pair/prod' 'type/num/num' A) ('type/patricia/ptree' A)) ('const/patricia/ADD' A)))).
tt('thm/patricia/BRANCHING_BIT_', ax, (![a : 'type/num/num', b : 'type/num/num']: ((~ (a = b)) => (~ (('const/bit/BIT' ('const/patricia/BRANCHING_BIT' a b) a) = ('const/bit/BIT' ('const/patricia/BRANCHING_BIT' a b) b)))))).
tt('thm/patricia/BRANCHING_BIT_ZERO_', ax, (![a : 'type/num/num', b : 'type/num/num']: ((('const/patricia/BRANCHING_BIT' a b) = 'const/num/0') = ((('const/arithmetic/ODD' a) = ('const/arithmetic/EVEN' b)) | (a = b))))).
tt('thm/patricia/BRANCHING_BIT_SYM_', ax, (![a : 'type/num/num', b : 'type/num/num']: (('const/patricia/BRANCHING_BIT' a b) = ('const/patricia/BRANCHING_BIT' b a)))).
tt('thm/patricia/EVERY_LEAF_ADD_', ax, ![A : $t]: (![P : ('type/num/num' > (A > $o)), t : ('type/patricia/ptree' A), k : 'type/num/num', d : A]: (((P k d) & (('const/patricia/EVERY_LEAF' A) P t)) => (('const/patricia/EVERY_LEAF' A) P (('const/patricia/ADD' A) t (('const/pair/,' 'type/num/num' A) k d)))))).
tt('thm/patricia/MONO_EVERY_LEAF_', ax, ![A : $t]: (![P : ('type/num/num' > (A > $o)), Q : ('type/num/num' > (A > $o)), t : ('type/patricia/ptree' A)]: (((![k : 'type/num/num', d : A]: ((P k d) => (Q k d))) & (('const/patricia/EVERY_LEAF' A) P t)) => (('const/patricia/EVERY_LEAF' A) Q t)))).
tt('thm/patricia/NOT_ADD_EMPTY_', ax, ![A : $t]: (![t : ('type/patricia/ptree' A), k : 'type/num/num', d : A]: (~ ((('const/patricia/ADD' A) t (('const/pair/,' 'type/num/num' A) k d)) = ('const/patricia/Empty' A))))).
tt('thm/patricia/EMPTY_IS_PTREE_', ax, ![A : $t]: (('const/patricia/IS_PTREE' A) ('const/patricia/Empty' A))).
tt('thm/patricia/ADD_IS_PTREE_', ax, ![A : $t]: (![t : ('type/patricia/ptree' A), x : ('type/pair/prod' 'type/num/num' A)]: ((('const/patricia/IS_PTREE' A) t) => (('const/patricia/IS_PTREE' A) (('const/patricia/ADD' A) t x))))).
tt('thm/patricia/EVERY_LEAF_BRANCH_', ax, ![A : $t]: (![P : ('type/num/num' > (A > $o)), p : 'type/num/num', m : 'type/num/num', l : ('type/patricia/ptree' A), r : ('type/patricia/ptree' A)]: ((('const/patricia/EVERY_LEAF' A) P (('const/patricia/BRANCH' A) (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A)))) p (('const/pair/,' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A))) m (('const/pair/,' ('type/patricia/ptree' A) ('type/patricia/ptree' A)) l r))))) = ((('const/patricia/EVERY_LEAF' A) P l) & (('const/patricia/EVERY_LEAF' A) P r))))).
tt('thm/patricia/EVERY_LEAF_REMOVE_', ax, ![A : $t]: (![P : ('type/num/num' > (A > $o)), t : ('type/patricia/ptree' A), k : 'type/num/num']: ((('const/patricia/EVERY_LEAF' A) P t) => (('const/patricia/EVERY_LEAF' A) P (('const/patricia/REMOVE' A) t k))))).
tt('thm/patricia/IS_PTREE_BRANCH_', ax, ![A : $t]: (![p : 'type/num/num', m : 'type/num/num', l : ('type/patricia/ptree' A), r : ('type/patricia/ptree' A)]: ((('const/prim_rec/<' p ('const/arithmetic/EXP' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) m)) & ((~ ((l = ('const/patricia/Empty' A)) & (r = ('const/patricia/Empty' A)))) & ((('const/patricia/EVERY_LEAF' A) (^[k : 'type/num/num', d : A]: (('const/bit/MOD_2EXP_EQ' m k p) & ('const/bit/BIT' m k))) l) & ((('const/patricia/EVERY_LEAF' A) (^[k : 'type/num/num', d : A]: (('const/bit/MOD_2EXP_EQ' m k p) & (~ ('const/bit/BIT' m k)))) r) & ((('const/patricia/IS_PTREE' A) l) & (('const/patricia/IS_PTREE' A) r)))))) => (('const/patricia/IS_PTREE' A) (('const/patricia/BRANCH' A) (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A)))) p (('const/pair/,' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A))) m (('const/pair/,' ('type/patricia/ptree' A) ('type/patricia/ptree' A)) l r)))))))).
tt('thm/patricia/REMOVE_IS_PTREE_', ax, ![A : $t]: (![t : ('type/patricia/ptree' A), k : 'type/num/num']: ((('const/patricia/IS_PTREE' A) t) => (('const/patricia/IS_PTREE' A) (('const/patricia/REMOVE' A) t k))))).
tt('thm/patricia/PEEK_NONE_', ax, ![A : $t]: (![P : ('type/num/num' > (A > $o)), t : ('type/patricia/ptree' A), k : 'type/num/num']: (((![d : A]: (~ (P k d))) & (('const/patricia/EVERY_LEAF' A) P t)) => ((('const/patricia/PEEK' A) t k) = ('const/option/NONE' A))))).
tt('thm/patricia/PEEK_ADD_', ax, ![A : $t]: (![t : ('type/patricia/ptree' A), k : 'type/num/num', d : A, j : 'type/num/num']: ((('const/patricia/IS_PTREE' A) t) => ((('const/patricia/PEEK' A) (('const/patricia/ADD' A) t (('const/pair/,' 'type/num/num' A) k d)) j) = (('const/bool/COND' ('type/option/option' A)) (k = j) (('const/option/SOME' A) d) (('const/patricia/PEEK' A) t j)))))).
tt('thm/patricia/BRANCH_', ax, ![A : $t]: (![p : 'type/num/num', m : 'type/num/num', l : ('type/patricia/ptree' A), r : ('type/patricia/ptree' A)]: ((('const/patricia/BRANCH' A) (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A)))) p (('const/pair/,' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A))) m (('const/pair/,' ('type/patricia/ptree' A) ('type/patricia/ptree' A)) l r)))) = (('const/bool/COND' ('type/patricia/ptree' A)) (l = ('const/patricia/Empty' A)) r (('const/bool/COND' ('type/patricia/ptree' A)) (r = ('const/patricia/Empty' A)) l (('const/patricia/Branch' A) p m l r)))))).
tt('thm/patricia/PEEK_REMOVE_', ax, ![A : $t]: (![t : ('type/patricia/ptree' A), k : 'type/num/num', j : 'type/num/num']: ((('const/patricia/IS_PTREE' A) t) => ((('const/patricia/PEEK' A) (('const/patricia/REMOVE' A) t k) j) = (('const/bool/COND' ('type/option/option' A)) (k = j) ('const/option/NONE' A) (('const/patricia/PEEK' A) t j)))))).
tt('thm/patricia/EVERY_LEAF_TRANSFORM_', ax, ![A : $t, B : $t]: (![P : ('type/num/num' > (A > $o)), Q : ('type/num/num' > (B > $o)), f : (A > B), t : ('type/patricia/ptree' A)]: (((![k : 'type/num/num', d : A]: ((P k d) => (Q k (f d)))) & (('const/patricia/EVERY_LEAF' A) P t)) => (('const/patricia/EVERY_LEAF' B) Q (('const/patricia/TRANSFORM' B A) f t))))).
tt('thm/patricia/TRANSFORM_EMPTY_', ax, ![A : $t, B : $t]: (![f : (A > B), t : ('type/patricia/ptree' A)]: (((('const/patricia/TRANSFORM' B A) f t) = ('const/patricia/Empty' B)) = (t = ('const/patricia/Empty' A))))).
tt('thm/patricia/TRANSFORM_IS_PTREE_', ax, ![A : $t, B : $t]: (![f : (A > B), t : ('type/patricia/ptree' A)]: ((('const/patricia/IS_PTREE' A) t) => (('const/patricia/IS_PTREE' B) (('const/patricia/TRANSFORM' B A) f t))))).
tt('thm/patricia/PEEK_TRANSFORM_', ax, ![A : $t, B : $t]: (![f : (A > B), t : ('type/patricia/ptree' A), k : 'type/num/num']: ((('const/patricia/PEEK' B) (('const/patricia/TRANSFORM' B A) f t) k) = (('const/option/option_CASE' A ('type/option/option' B)) (('const/patricia/PEEK' A) t k) ('const/option/NONE' B) (^[x : A]: (('const/option/SOME' B) (f x))))))).
tt('thm/patricia/ADD_TRANSFORM_', ax, ![A : $t, B : $t]: (![f : (A > B), t : ('type/patricia/ptree' A), k : 'type/num/num', d : A]: ((('const/patricia/TRANSFORM' B A) f (('const/patricia/ADD' A) t (('const/pair/,' 'type/num/num' A) k d))) = (('const/patricia/ADD' B) (('const/patricia/TRANSFORM' B A) f t) (('const/pair/,' 'type/num/num' B) k (f d)))))).
tt('thm/patricia/TRANSFORM_BRANCH_', ax, ![A : $t, B : $t]: (![f : (A > B), p : 'type/num/num', m : 'type/num/num', l : ('type/patricia/ptree' A), r : ('type/patricia/ptree' A)]: ((('const/patricia/TRANSFORM' B A) f (('const/patricia/BRANCH' A) (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A)))) p (('const/pair/,' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' A) ('type/patricia/ptree' A))) m (('const/pair/,' ('type/patricia/ptree' A) ('type/patricia/ptree' A)) l r))))) = (('const/patricia/BRANCH' B) (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' B) ('type/patricia/ptree' B)))) p (('const/pair/,' 'type/num/num' ('type/pair/prod' ('type/patricia/ptree' B) ('type/patricia/ptree' B))) m (('const/pair/,' ('type/patricia/ptree' B) ('type/patricia/ptree' B)) (('const/patricia/TRANSFORM' B A) f l) (('const/patricia/TRANSFORM' B A) f r)))))))).
tt('thm/patricia/REMOVE_TRANSFORM_', ax, ![A : $t, B : $t]: (![f : (A > B), t : ('type/patricia/ptree' A), k : 'type/num/num']: ((('const/patricia/TRANSFORM' B A) f (('const/patricia/REMOVE' A) t k)) = (('const/patricia/REMOVE' B) (('const/patricia/TRANSFORM' B A) f t) k)))).
tt('thm/patricia/REMOVE_ADD_EQ_', ax, ![A : $t]: (![t : ('type/patricia/ptree' A), k : 'type/num/num', d : A]: ((('const/patricia/REMOVE' A) (('const/patricia/ADD' A) t (('const/pair/,' 'type/num/num' A) k d)) k) = (('const/patricia/REMOVE' A) t k)))).
tt('thm/patricia/ADD_ADD_', ax, ![A : $t]: (![t : ('type/patricia/ptree' A), k : 'type/num/num', d : A, e : A]: ((('const/patricia/ADD' A) (('const/patricia/ADD' A) t (('const/pair/,' 'type/num/num' A) k d)) (('const/pair/,' 'type/num/num' A) k e)) = (('const/patricia/ADD' A) t (('const/pair/,' 'type/num/num' A) k e))))).
tt('thm/patricia/EVERY_LEAF_PEEK_', ax, ![A : $t]: (![P : ('type/num/num' > (A > $o)), t : ('type/patricia/ptree' A), k : 'type/num/num']: (((('const/patricia/EVERY_LEAF' A) P t) & (('const/option/IS_SOME' A) (('const/patricia/PEEK' A) t k))) => (P k (('const/option/THE' A) (('const/patricia/PEEK' A) t k)))))).
tt('thm/patricia/IS_PTREE_PEEK_0', ax, ![A : $t]: (![k : 'type/num/num']: (~ (('const/option/IS_SOME' A) (('const/patricia/PEEK' A) ('const/patricia/Empty' A) k))))).
tt('thm/patricia/IS_PTREE_PEEK_1', ax, ![B : $t]: (![k : 'type/num/num', j : 'type/num/num', b : B]: ((('const/option/IS_SOME' B) (('const/patricia/PEEK' B) (('const/patricia/Leaf' B) j b) k)) = (j = k)))).
tt('thm/patricia/IS_PTREE_PEEK_e2', ax, ![C : $t]: (![p : 'type/num/num', m : 'type/num/num', l : ('type/patricia/ptree' C), r : ('type/patricia/ptree' C)]: ((('const/patricia/IS_PTREE' C) (('const/patricia/Branch' C) p m l r)) => ((?[k : 'type/num/num']: (('const/bit/BIT' m k) & (('const/option/IS_SOME' C) (('const/patricia/PEEK' C) l k)))) & ((?[k : 'type/num/num']: ((~ ('const/bit/BIT' m k)) & (('const/option/IS_SOME' C) (('const/patricia/PEEK' C) r k)))) & (![k : 'type/num/num', n : 'type/num/num']: (((~ ('const/bit/MOD_2EXP_EQ' m k p)) | (('const/prim_rec/<' n m) & (~ (('const/bit/BIT' n p) = ('const/bit/BIT' n k))))) => ((~ (('const/option/IS_SOME' C) (('const/patricia/PEEK' C) l k))) & (~ (('const/option/IS_SOME' C) (('const/patricia/PEEK' C) r k))))))))))).
tt('thm/patricia/PTREE_EQ_', ax, ![A : $t]: (![t1 : ('type/patricia/ptree' A), t2 : ('type/patricia/ptree' A)]: (((('const/patricia/IS_PTREE' A) t1) & (('const/patricia/IS_PTREE' A) t2)) => ((![k : 'type/num/num']: ((('const/patricia/PEEK' A) t1 k) = (('const/patricia/PEEK' A) t2 k))) = (t1 = t2))))).
tt('thm/patricia/REMOVE_REMOVE_', ax, ![A : $t]: (![t : ('type/patricia/ptree' A), k : 'type/num/num']: ((('const/patricia/IS_PTREE' A) t) => ((('const/patricia/REMOVE' A) (('const/patricia/REMOVE' A) t k) k) = (('const/patricia/REMOVE' A) t k))))).
tt('thm/patricia/REMOVE_ADD_', ax, ![A : $t]: (![t : ('type/patricia/ptree' A), k : 'type/num/num', d : A, j : 'type/num/num']: ((('const/patricia/IS_PTREE' A) t) => ((('const/patricia/REMOVE' A) (('const/patricia/ADD' A) t (('const/pair/,' 'type/num/num' A) k d)) j) = (('const/bool/COND' ('type/patricia/ptree' A)) (k = j) (('const/patricia/REMOVE' A) t j) (('const/patricia/ADD' A) (('const/patricia/REMOVE' A) t j) (('const/pair/,' 'type/num/num' A) k d))))))).
tt('thm/patricia/ADD_ADD_SYM_', ax, ![A : $t]: (![t : ('type/patricia/ptree' A), k : 'type/num/num', j : 'type/num/num', d : A, e : A]: (((('const/patricia/IS_PTREE' A) t) & (~ (k = j))) => ((('const/patricia/ADD' A) (('const/patricia/ADD' A) t (('const/pair/,' 'type/num/num' A) k d)) (('const/pair/,' 'type/num/num' A) j e)) = (('const/patricia/ADD' A) (('const/patricia/ADD' A) t (('const/pair/,' 'type/num/num' A) j e)) (('const/pair/,' 'type/num/num' A) k d)))))).
tt('thm/patricia/FILTER_ALL_', ax, ![A : $t]: (![P : (A > $o), l : ('type/list/list' A)]: ((![n : 'type/num/num']: (('const/prim_rec/<' n (('const/list/LENGTH' A) l)) => (~ (P (('const/list/EL' A) n l))))) = ((('const/list/FILTER' A) P l) = ('const/list/NIL' A))))).
tt('thm/patricia/TRAVERSE_TRANSFORM_', ax, ![A : $t, B : $t]: (![f : (A > B), t : ('type/patricia/ptree' A)]: ((('const/patricia/TRAVERSE' B) (('const/patricia/TRANSFORM' B A) f t)) = (('const/patricia/TRAVERSE' A) t)))).
tt('thm/patricia/MEM_TRAVERSE_PEEK_', ax, ![A : $t]: (![t : ('type/patricia/ptree' A), k : 'type/num/num']: ((('const/patricia/IS_PTREE' A) t) => ((('const/bool/IN' 'type/num/num') k (('const/list/LIST_TO_SET' 'type/num/num') (('const/patricia/TRAVERSE' A) t))) = (('const/option/IS_SOME' A) (('const/patricia/PEEK' A) t k)))))).
tt('thm/patricia/IN_NUMSET_OF_PTREE_', ax, (![t : ('type/patricia/ptree' 'type/one/one'), n : 'type/num/num']: ((('const/patricia/IS_PTREE' 'type/one/one') t) => ((('const/bool/IN' 'type/num/num') n ('const/patricia/NUMSET_OF_PTREE' t)) = ('const/patricia/IN_PTREE' n t))))).
tt('thm/patricia/ADD_LIST_IS_PTREE_', ax, ![A : $t]: (![t : ('type/patricia/ptree' A), l : ('type/list/list' ('type/pair/prod' 'type/num/num' A))]: ((('const/patricia/IS_PTREE' A) t) => (('const/patricia/IS_PTREE' A) (('const/patricia/ADD_LIST' A) t l))))).
tt('thm/patricia/ADD_LIST_TO_EMPTY_IS_PTREE_', ax, ![A : $t]: (![l : ('type/list/list' ('type/pair/prod' 'type/num/num' A))]: (('const/patricia/IS_PTREE' A) (('const/patricia/ADD_LIST' A) ('const/patricia/Empty' A) l)))).
tt('thm/patricia/PTREE_OF_NUMSET_IS_PTREE_', ax, (![t : ('type/patricia/ptree' 'type/one/one'), s : ('type/num/num' > $o)]: ((('const/patricia/IS_PTREE' 'type/one/one') t) => (('const/patricia/IS_PTREE' 'type/one/one') ('const/patricia/PTREE_OF_NUMSET' t s))))).
tt('thm/patricia/PTREE_OF_NUMSET_IS_PTREE_EMPTY_', ax, (![s : ('type/num/num' > $o)]: (('const/patricia/IS_PTREE' 'type/one/one') ('const/patricia/PTREE_OF_NUMSET' ('const/patricia/Empty' 'type/one/one') s)))).
tt('thm/patricia/NOT_KEY_LEFT_AND_RIGHT_', ax, ![A : $t]: (![p : 'type/num/num', m : 'type/num/num', l : ('type/patricia/ptree' A), r : ('type/patricia/ptree' A), k : 'type/num/num', j : 'type/num/num']: (((('const/patricia/IS_PTREE' A) (('const/patricia/Branch' A) p m l r)) & ((('const/option/IS_SOME' A) (('const/patricia/PEEK' A) l k)) & (('const/option/IS_SOME' A) (('const/patricia/PEEK' A) r j)))) => (~ (k = j))))).
tt('thm/patricia/ALL_DISTINCT_TRAVERSE_', ax, ![A : $t]: (![t : ('type/patricia/ptree' A)]: ((('const/patricia/IS_PTREE' A) t) => (('const/list/ALL_DISTINCT' 'type/num/num') (('const/patricia/TRAVERSE' A) t))))).
tt('thm/patricia/MEM_ALL_DISTINCT_IMP_PERM_', ax, ![A : $t]: (![l1 : ('type/list/list' A), l2 : ('type/list/list' A)]: (((('const/list/ALL_DISTINCT' A) l1) & ((('const/list/ALL_DISTINCT' A) l2) & (![x : A]: ((('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) l1)) = (('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) l2)))))) => (('const/sorting/PERM' A) l1 l2)))).
tt('thm/patricia/MEM_TRAVERSE_', ax, (![t : ('type/patricia/ptree' 'type/one/one'), k : 'type/num/num']: ((('const/patricia/IS_PTREE' 'type/one/one') t) => ((('const/bool/IN' 'type/num/num') k (('const/list/LIST_TO_SET' 'type/num/num') (('const/patricia/TRAVERSE' 'type/one/one') t))) = (('const/bool/IN' 'type/num/num') k ('const/patricia/NUMSET_OF_PTREE' t)))))).
tt('thm/patricia/INSERT_PTREE_IS_PTREE_', ax, (![t : ('type/patricia/ptree' 'type/one/one'), x : 'type/num/num']: ((('const/patricia/IS_PTREE' 'type/one/one') t) => (('const/patricia/IS_PTREE' 'type/one/one') ('const/patricia/INSERT_PTREE' x t))))).
tt('thm/patricia/FINITE_NUMSET_OF_PTREE_', ax, (![t : ('type/patricia/ptree' 'type/one/one')]: (('const/pred_set/FINITE' 'type/num/num') ('const/patricia/NUMSET_OF_PTREE' t)))).
tt('thm/patricia/ADD_INSERT_', ax, (![v : 'type/one/one', t : ('type/patricia/ptree' 'type/one/one'), n : 'type/num/num']: ((('const/patricia/ADD' 'type/one/one') t (('const/pair/,' 'type/num/num' 'type/one/one') n v)) = ('const/patricia/INSERT_PTREE' n t)))).
tt('thm/patricia/PEEK_INSERT_PTREE_', ax, (![t : ('type/patricia/ptree' 'type/one/one'), k : 'type/num/num', j : 'type/num/num']: ((('const/patricia/IS_PTREE' 'type/one/one') t) => ((('const/patricia/PEEK' 'type/one/one') ('const/patricia/INSERT_PTREE' k t) j) = (('const/bool/COND' ('type/option/option' 'type/one/one')) (k = j) (('const/option/SOME' 'type/one/one') 'const/one/one') (('const/patricia/PEEK' 'type/one/one') t j)))))).
tt('thm/patricia/MEM_TRAVERSE_INSERT_PTREE_', ax, (![t : ('type/patricia/ptree' 'type/one/one'), x : 'type/num/num', h : 'type/num/num']: ((('const/patricia/IS_PTREE' 'type/one/one') t) => ((('const/bool/IN' 'type/num/num') x (('const/list/LIST_TO_SET' 'type/num/num') (('const/patricia/TRAVERSE' 'type/one/one') ('const/patricia/INSERT_PTREE' h t)))) = ((x = h) | ((~ (x = h)) & (('const/bool/IN' 'type/num/num') x (('const/list/LIST_TO_SET' 'type/num/num') (('const/patricia/TRAVERSE' 'type/one/one') t))))))))).
tt('thm/patricia/PERM_INSERT_PTREE_', ax, (![t : ('type/patricia/ptree' 'type/one/one'), s : ('type/num/num' > $o)]: ((('const/pred_set/FINITE' 'type/num/num') s) => ((('const/patricia/IS_PTREE' 'type/one/one') t) => (('const/sorting/PERM' 'type/num/num') (('const/patricia/TRAVERSE' 'type/one/one') (('const/list/FOLDL' 'type/num/num' ('type/patricia/ptree' 'type/one/one')) (('const/combin/C' 'type/num/num' ('type/patricia/ptree' 'type/one/one') ('type/patricia/ptree' 'type/one/one')) 'const/patricia/INSERT_PTREE') t (('const/list/SET_TO_LIST' 'type/num/num') s))) (('const/list/SET_TO_LIST' 'type/num/num') (('const/pred_set/UNION' 'type/num/num') ('const/patricia/NUMSET_OF_PTREE' t) s))))))).
tt('thm/patricia/IN_PTREE_OF_NUMSET_', ax, (![t : ('type/patricia/ptree' 'type/one/one'), s : ('type/num/num' > $o), n : 'type/num/num']: (((('const/patricia/IS_PTREE' 'type/one/one') t) & (('const/pred_set/FINITE' 'type/num/num') s)) => (('const/patricia/IN_PTREE' n ('const/patricia/PTREE_OF_NUMSET' t s)) = (('const/patricia/IN_PTREE' n t) | (('const/bool/IN' 'type/num/num') n s)))))).
tt('thm/patricia/IN_PTREE_EMPTY_', ax, (![n : 'type/num/num']: (~ ('const/patricia/IN_PTREE' n ('const/patricia/Empty' 'type/one/one'))))).
tt('thm/patricia/IN_PTREE_OF_NUMSET_EMPTY_', ax, (![s : ('type/num/num' > $o), n : 'type/num/num']: ((('const/pred_set/FINITE' 'type/num/num') s) => ((('const/bool/IN' 'type/num/num') n s) = ('const/patricia/IN_PTREE' n ('const/patricia/PTREE_OF_NUMSET' ('const/patricia/Empty' 'type/one/one') s)))))).
tt('thm/patricia/PTREE_EXTENSION_', ax, (![t1 : ('type/patricia/ptree' 'type/one/one'), t2 : ('type/patricia/ptree' 'type/one/one')]: (((('const/patricia/IS_PTREE' 'type/one/one') t1) & (('const/patricia/IS_PTREE' 'type/one/one') t2)) => ((t1 = t2) = (![x : 'type/num/num']: (('const/patricia/IN_PTREE' x t1) = ('const/patricia/IN_PTREE' x t2))))))).
tt('thm/patricia/PTREE_OF_NUMSET_NUMSET_OF_PTREE_', ax, (![t : ('type/patricia/ptree' 'type/one/one'), s : ('type/num/num' > $o)]: (((('const/patricia/IS_PTREE' 'type/one/one') t) & (('const/pred_set/FINITE' 'type/num/num') s)) => (('const/patricia/PTREE_OF_NUMSET' ('const/patricia/Empty' 'type/one/one') (('const/pred_set/UNION' 'type/num/num') ('const/patricia/NUMSET_OF_PTREE' t) s)) = ('const/patricia/PTREE_OF_NUMSET' t s))))).
tt('thm/patricia/NUMSET_OF_PTREE_PTREE_OF_NUMSET_', ax, (![t : ('type/patricia/ptree' 'type/one/one'), s : ('type/num/num' > $o)]: (((('const/patricia/IS_PTREE' 'type/one/one') t) & (('const/pred_set/FINITE' 'type/num/num') s)) => (('const/patricia/NUMSET_OF_PTREE' ('const/patricia/PTREE_OF_NUMSET' t s)) = (('const/pred_set/UNION' 'type/num/num') ('const/patricia/NUMSET_OF_PTREE' t) s))))).
tt('thm/patricia/NUMSET_OF_PTREE_EMPTY_', ax, (('const/patricia/NUMSET_OF_PTREE' ('const/patricia/Empty' 'type/one/one')) = ('const/pred_set/EMPTY' 'type/num/num'))).
tt('thm/patricia/PTREE_OF_NUMSET_EMPTY_', ax, (![t : ('type/patricia/ptree' 'type/one/one')]: (('const/patricia/PTREE_OF_NUMSET' t ('const/pred_set/EMPTY' 'type/num/num')) = t))).
tt('thm/patricia/NUMSET_OF_PTREE_PTREE_OF_NUMSET_EMPTY_', ax, (![s : ('type/num/num' > $o)]: ((('const/pred_set/FINITE' 'type/num/num') s) => (('const/patricia/NUMSET_OF_PTREE' ('const/patricia/PTREE_OF_NUMSET' ('const/patricia/Empty' 'type/one/one') s)) = s)))).
tt('thm/patricia/IN_PTREE_INSERT_PTREE_', ax, (![t : ('type/patricia/ptree' 'type/one/one'), m : 'type/num/num', n : 'type/num/num']: ((('const/patricia/IS_PTREE' 'type/one/one') t) => (('const/patricia/IN_PTREE' n ('const/patricia/INSERT_PTREE' m t)) = ((m = n) | ('const/patricia/IN_PTREE' n t)))))).
tt('thm/patricia/IN_PTREE_REMOVE_', ax, (![t : ('type/patricia/ptree' 'type/one/one'), m : 'type/num/num', n : 'type/num/num']: ((('const/patricia/IS_PTREE' 'type/one/one') t) => (('const/patricia/IN_PTREE' n (('const/patricia/REMOVE' 'type/one/one') t m)) = ((~ (n = m)) & ('const/patricia/IN_PTREE' n t)))))).
tt('thm/patricia/IN_PTREE_UNION_PTREE_', ax, (![t1 : ('type/patricia/ptree' 'type/one/one'), t2 : ('type/patricia/ptree' 'type/one/one'), n : 'type/num/num']: (((('const/patricia/IS_PTREE' 'type/one/one') t1) & (('const/patricia/IS_PTREE' 'type/one/one') t2)) => (('const/patricia/IN_PTREE' n ('const/patricia/UNION_PTREE' t1 t2)) = (('const/patricia/IN_PTREE' n t1) | ('const/patricia/IN_PTREE' n t2)))))).
tt('thm/patricia/UNION_PTREE_IS_PTREE_', ax, (![t1 : ('type/patricia/ptree' 'type/one/one'), t2 : ('type/patricia/ptree' 'type/one/one')]: (((('const/patricia/IS_PTREE' 'type/one/one') t1) & (('const/patricia/IS_PTREE' 'type/one/one') t2)) => (('const/patricia/IS_PTREE' 'type/one/one') ('const/patricia/UNION_PTREE' t1 t2))))).
tt('thm/patricia/UNION_PTREE_COMM_', ax, (![t1 : ('type/patricia/ptree' 'type/one/one'), t2 : ('type/patricia/ptree' 'type/one/one')]: (((('const/patricia/IS_PTREE' 'type/one/one') t1) & (('const/patricia/IS_PTREE' 'type/one/one') t2)) => (('const/patricia/UNION_PTREE' t1 t2) = ('const/patricia/UNION_PTREE' t2 t1))))).
tt('thm/patricia/UNION_PTREE_COMM_EMPTY_', ax, (![t : ('type/patricia/ptree' 'type/one/one')]: ((('const/patricia/IS_PTREE' 'type/one/one') t) => (('const/patricia/UNION_PTREE' ('const/patricia/Empty' 'type/one/one') t) = ('const/patricia/UNION_PTREE' t ('const/patricia/Empty' 'type/one/one')))))).
tt('thm/patricia/UNION_PTREE_EMPTY_0', ax, (![t : ('type/patricia/ptree' 'type/one/one')]: (('const/patricia/UNION_PTREE' t ('const/patricia/Empty' 'type/one/one')) = t))).
tt('thm/patricia/UNION_PTREE_EMPTY_e1', ax, (![t : ('type/patricia/ptree' 'type/one/one')]: ((('const/patricia/IS_PTREE' 'type/one/one') t) => (('const/patricia/UNION_PTREE' ('const/patricia/Empty' 'type/one/one') t) = t)))).
tt('thm/patricia/UNION_PTREE_ASSOC_', ax, (![t1 : ('type/patricia/ptree' 'type/one/one'), t2 : ('type/patricia/ptree' 'type/one/one'), t3 : ('type/patricia/ptree' 'type/one/one')]: (((('const/patricia/IS_PTREE' 'type/one/one') t1) & ((('const/patricia/IS_PTREE' 'type/one/one') t2) & (('const/patricia/IS_PTREE' 'type/one/one') t3))) => (('const/patricia/UNION_PTREE' t1 ('const/patricia/UNION_PTREE' t2 t3)) = ('const/patricia/UNION_PTREE' ('const/patricia/UNION_PTREE' t1 t2) t3))))).
tt('thm/patricia/PTREE_OF_NUMSET_UNION_', ax, (![t : ('type/patricia/ptree' 'type/one/one'), s1 : ('type/num/num' > $o), s2 : ('type/num/num' > $o)]: (((('const/patricia/IS_PTREE' 'type/one/one') t) & ((('const/pred_set/FINITE' 'type/num/num') s1) & (('const/pred_set/FINITE' 'type/num/num') s2))) => (('const/patricia/PTREE_OF_NUMSET' t (('const/pred_set/UNION' 'type/num/num') s1 s2)) = ('const/patricia/PTREE_OF_NUMSET' ('const/patricia/PTREE_OF_NUMSET' t s1) s2))))).
tt('thm/patricia/PTREE_OF_NUMSET_INSERT_', ax, (![t : ('type/patricia/ptree' 'type/one/one'), s : ('type/num/num' > $o), x : 'type/num/num']: (((('const/patricia/IS_PTREE' 'type/one/one') t) & (('const/pred_set/FINITE' 'type/num/num') s)) => (('const/patricia/PTREE_OF_NUMSET' t (('const/pred_set/INSERT' 'type/num/num') x s)) = ('const/patricia/INSERT_PTREE' x ('const/patricia/PTREE_OF_NUMSET' t s)))))).
tt('thm/patricia/PTREE_OF_NUMSET_INSERT_EMPTY_', ax, (![s : ('type/num/num' > $o), x : 'type/num/num']: ((('const/pred_set/FINITE' 'type/num/num') s) => (('const/patricia/PTREE_OF_NUMSET' ('const/patricia/Empty' 'type/one/one') (('const/pred_set/INSERT' 'type/num/num') x s)) = ('const/patricia/INSERT_PTREE' x ('const/patricia/PTREE_OF_NUMSET' ('const/patricia/Empty' 'type/one/one') s)))))).
tt('thm/patricia/PTREE_OF_NUMSET_DELETE_', ax, (![s : ('type/num/num' > $o), x : 'type/num/num']: ((('const/pred_set/FINITE' 'type/num/num') s) => (('const/patricia/PTREE_OF_NUMSET' ('const/patricia/Empty' 'type/one/one') (('const/pred_set/DELETE' 'type/num/num') s x)) = (('const/patricia/REMOVE' 'type/one/one') ('const/patricia/PTREE_OF_NUMSET' ('const/patricia/Empty' 'type/one/one') s) x))))).
tt('thm/patricia/TRAVERSE_AUX_', ax, ![A : $t]: (![t : ('type/patricia/ptree' A)]: ((('const/patricia/TRAVERSE' A) t) = (('const/patricia/TRAVERSE_AUX' A) t ('const/list/NIL' 'type/num/num'))))).
tt('thm/patricia/PTREE_TRAVERSE_EQ_', ax, ![B : $t, A : $t]: (![t1 : ('type/patricia/ptree' A), t2 : ('type/patricia/ptree' B)]: (((('const/patricia/IS_PTREE' A) t1) & (('const/patricia/IS_PTREE' B) t2)) => ((![k : 'type/num/num']: ((('const/bool/IN' 'type/num/num') k (('const/list/LIST_TO_SET' 'type/num/num') (('const/patricia/TRAVERSE' A) t1))) = (('const/bool/IN' 'type/num/num') k (('const/list/LIST_TO_SET' 'type/num/num') (('const/patricia/TRAVERSE' B) t2))))) = ((('const/patricia/TRAVERSE' A) t1) = (('const/patricia/TRAVERSE' B) t2)))))).
tt('thm/patricia/QSORT_MEM_EQ_', ax, ![A : $t]: (![l2 : ('type/list/list' A), l1 : ('type/list/list' A), R : (A > (A > $o))]: (((('const/sorting/QSORT' A) R l1) = (('const/sorting/QSORT' A) R l2)) => (![x : A]: ((('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) l1)) = (('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) l2))))))).
tt('thm/patricia/KEYS_PEEK_', ax, ![B : $t, A : $t]: (![t1 : ('type/patricia/ptree' A), t2 : ('type/patricia/ptree' B)]: (((('const/patricia/IS_PTREE' A) t1) & (('const/patricia/IS_PTREE' B) t2)) => (((('const/patricia/KEYS' A) t1) = (('const/patricia/KEYS' B) t2)) = ((('const/patricia/TRAVERSE' A) t1) = (('const/patricia/TRAVERSE' B) t2)))))).
tt('thm/patricia/PERM_ADD_', ax, ![A : $t]: (![t : ('type/patricia/ptree' A), k : 'type/num/num', d : A]: (((('const/patricia/IS_PTREE' A) t) & (~ (('const/bool/IN' 'type/num/num') k (('const/list/LIST_TO_SET' 'type/num/num') (('const/patricia/TRAVERSE' A) t))))) => (('const/sorting/PERM' 'type/num/num') (('const/patricia/TRAVERSE' A) (('const/patricia/ADD' A) t (('const/pair/,' 'type/num/num' A) k d))) (('const/list/CONS' 'type/num/num') k (('const/patricia/TRAVERSE' A) t)))))).
tt('thm/patricia/PERM_NOT_ADD_', ax, ![A : $t]: (![t : ('type/patricia/ptree' A), k : 'type/num/num', d : A]: (((('const/patricia/IS_PTREE' A) t) & (('const/bool/IN' 'type/num/num') k (('const/list/LIST_TO_SET' 'type/num/num') (('const/patricia/TRAVERSE' A) t)))) => ((('const/patricia/TRAVERSE' A) (('const/patricia/ADD' A) t (('const/pair/,' 'type/num/num' A) k d))) = (('const/patricia/TRAVERSE' A) t))))).
tt('thm/patricia/PERM_NOT_REMOVE_', ax, ![A : $t]: (![t : ('type/patricia/ptree' A), k : 'type/num/num']: (((('const/patricia/IS_PTREE' A) t) & (~ (('const/bool/IN' 'type/num/num') k (('const/list/LIST_TO_SET' 'type/num/num') (('const/patricia/TRAVERSE' A) t))))) => ((('const/patricia/TRAVERSE' A) (('const/patricia/REMOVE' A) t k)) = (('const/patricia/TRAVERSE' A) t))))).
tt('thm/patricia/PERM_DELETE_PTREE_', ax, (![t : ('type/patricia/ptree' 'type/one/one'), k : 'type/num/num']: (((('const/patricia/IS_PTREE' 'type/one/one') t) & (('const/bool/IN' 'type/num/num') k (('const/list/LIST_TO_SET' 'type/num/num') (('const/patricia/TRAVERSE' 'type/one/one') t)))) => (('const/sorting/PERM' 'type/num/num') (('const/patricia/TRAVERSE' 'type/one/one') (('const/patricia/REMOVE' 'type/one/one') t k)) (('const/list/FILTER' 'type/num/num') (^[x : 'type/num/num']: (~ (x = k))) (('const/patricia/TRAVERSE' 'type/one/one') t)))))).
tt('thm/patricia/FILTER_NONE_', ax, ![A : $t]: (![P : (A > $o), l : ('type/list/list' A)]: ((![n : 'type/num/num']: (('const/prim_rec/<' n (('const/list/LENGTH' A) l)) => (P (('const/list/EL' A) n l)))) => ((('const/list/FILTER' A) P l) = l)))).
tt('thm/patricia/PERM_REMOVE_', ax, ![A : $t]: (![t : ('type/patricia/ptree' A), k : 'type/num/num']: (((('const/patricia/IS_PTREE' A) t) & (('const/bool/IN' 'type/num/num') k (('const/list/LIST_TO_SET' 'type/num/num') (('const/patricia/TRAVERSE' A) t)))) => (('const/sorting/PERM' 'type/num/num') (('const/patricia/TRAVERSE' A) (('const/patricia/REMOVE' A) t k)) (('const/list/FILTER' 'type/num/num') (^[x : 'type/num/num']: (~ (x = k))) (('const/patricia/TRAVERSE' A) t)))))).
tt('thm/patricia/SIZE_ADD_', ax, ![A : $t]: (![t : ('type/patricia/ptree' A), k : 'type/num/num', d : A]: ((('const/patricia/IS_PTREE' A) t) => ((('const/patricia/SIZE' A) (('const/patricia/ADD' A) t (('const/pair/,' 'type/num/num' A) k d))) = (('const/bool/COND' 'type/num/num') (('const/bool/IN' 'type/num/num') k (('const/list/LIST_TO_SET' 'type/num/num') (('const/patricia/TRAVERSE' A) t))) (('const/patricia/SIZE' A) t) ('const/arithmetic/+' (('const/patricia/SIZE' A) t) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))).
tt('thm/patricia/SIZE_REMOVE_', ax, ![A : $t]: (![t : ('type/patricia/ptree' A), k : 'type/num/num']: ((('const/patricia/IS_PTREE' A) t) => ((('const/patricia/SIZE' A) (('const/patricia/REMOVE' A) t k)) = (('const/bool/COND' 'type/num/num') (('const/bool/IN' 'type/num/num') k (('const/list/LIST_TO_SET' 'type/num/num') (('const/patricia/TRAVERSE' A) t))) ('const/arithmetic/-' (('const/patricia/SIZE' A) t) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) (('const/patricia/SIZE' A) t)))))).
tt('thm/patricia/SIZE_0', ax, ![A : $t]: ((('const/patricia/SIZE' A) ('const/patricia/Empty' A)) = 'const/num/0')).
tt('thm/patricia/SIZE_1', ax, ![A : $t]: (![k : 'type/num/num', d : A]: ((('const/patricia/SIZE' A) (('const/patricia/Leaf' A) k d)) = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/patricia/SIZE_e2', ax, ![A : $t]: (![p : 'type/num/num', m : 'type/num/num', l : ('type/patricia/ptree' A), r : ('type/patricia/ptree' A)]: ((('const/patricia/SIZE' A) (('const/patricia/Branch' A) p m l r)) = ('const/arithmetic/+' (('const/patricia/SIZE' A) l) (('const/patricia/SIZE' A) r))))).
tt('thm/patricia/SIZE_PTREE_OF_NUMSET_', ax, (![t : ('type/patricia/ptree' 'type/one/one'), s : ('type/num/num' > $o)]: ((('const/pred_set/FINITE' 'type/num/num') s) => (((('const/patricia/IS_PTREE' 'type/one/one') t) & (('const/list/ALL_DISTINCT' 'type/num/num') (('const/list/APPEND' 'type/num/num') (('const/patricia/TRAVERSE' 'type/one/one') t) (('const/list/SET_TO_LIST' 'type/num/num') s)))) => ((('const/patricia/SIZE' 'type/one/one') ('const/patricia/PTREE_OF_NUMSET' t s)) = ('const/arithmetic/+' (('const/patricia/SIZE' 'type/one/one') t) (('const/pred_set/CARD' 'type/num/num') s))))))).
tt('thm/patricia/SIZE_PTREE_OF_NUMSET_EMPTY_', ax, (![s : ('type/num/num' > $o)]: ((('const/pred_set/FINITE' 'type/num/num') s) => ((('const/patricia/SIZE' 'type/one/one') ('const/patricia/PTREE_OF_NUMSET' ('const/patricia/Empty' 'type/one/one') s)) = (('const/pred_set/CARD' 'type/num/num') s))))).
tt('thm/patricia/CARD_LIST_TO_SET_', ax, ![A : $t]: (![l : ('type/list/list' A)]: ((('const/list/ALL_DISTINCT' A) l) => ((('const/pred_set/CARD' A) (('const/list/LIST_TO_SET' A) l)) = (('const/list/LENGTH' A) l))))).
tt('thm/patricia/CARD_NUMSET_OF_PTREE_', ax, (![t : ('type/patricia/ptree' 'type/one/one')]: ((('const/patricia/IS_PTREE' 'type/one/one') t) => ((('const/pred_set/CARD' 'type/num/num') ('const/patricia/NUMSET_OF_PTREE' t)) = (('const/patricia/SIZE' 'type/one/one') t))))).
tt('thm/patricia/DELETE_UNION_', ax, ![A : $t]: (![x : A, s1 : (A > $o), s2 : (A > $o)]: ((('const/pred_set/DELETE' A) (('const/pred_set/UNION' A) s1 s2) x) = (('const/pred_set/UNION' A) (('const/pred_set/DELETE' A) s1 x) (('const/pred_set/DELETE' A) s2 x))))).
