tt('type/canonical/canonical_sum', ty, $t > $t).
tt('type/canonical/spolynom', ty, $t > $t).
tt('const/canonical/Cons_monom', ty, ![A : $t]: (A > (('type/list/list' 'type/quote/index') > (('type/canonical/canonical_sum' A) > ('type/canonical/canonical_sum' A))))).
tt('const/canonical/Cons_varlist', ty, ![A : $t]: (('type/list/list' 'type/quote/index') > (('type/canonical/canonical_sum' A) > ('type/canonical/canonical_sum' A)))).
tt('const/canonical/Nil_monom', ty, ![A : $t]: ('type/canonical/canonical_sum' A)).
tt('const/canonical/SPconst', ty, ![A : $t]: (A > ('type/canonical/spolynom' A))).
tt('const/canonical/SPmult', ty, ![A : $t]: (('type/canonical/spolynom' A) > (('type/canonical/spolynom' A) > ('type/canonical/spolynom' A)))).
tt('const/canonical/SPplus', ty, ![A : $t]: (('type/canonical/spolynom' A) > (('type/canonical/spolynom' A) > ('type/canonical/spolynom' A)))).
tt('const/canonical/SPvar', ty, ![A : $t]: ('type/quote/index' > ('type/canonical/spolynom' A))).
tt('const/canonical/canonical_sum_CASE', ty, ![A : $t, B : $t]: (('type/canonical/canonical_sum' A) > (B > ((A > (('type/list/list' 'type/quote/index') > (('type/canonical/canonical_sum' A) > B))) > ((('type/list/list' 'type/quote/index') > (('type/canonical/canonical_sum' A) > B)) > B))))).
tt('const/canonical/canonical_sum_merge', ty, ![A : $t]: (('type/semi_ring/semi_ring' A) > (('type/canonical/canonical_sum' A) > (('type/canonical/canonical_sum' A) > ('type/canonical/canonical_sum' A))))).
tt('const/canonical/canonical_sum_merge_tupled', ty, ![A : $t]: (('type/pair/prod' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))) > ('type/canonical/canonical_sum' A))).
tt('const/canonical/canonical_sum_prod', ty, ![A : $t]: (('type/semi_ring/semi_ring' A) > (('type/canonical/canonical_sum' A) > (('type/canonical/canonical_sum' A) > ('type/canonical/canonical_sum' A))))).
tt('const/canonical/canonical_sum_scalar', ty, ![A : $t]: (('type/semi_ring/semi_ring' A) > (A > (('type/canonical/canonical_sum' A) > ('type/canonical/canonical_sum' A))))).
tt('const/canonical/canonical_sum_scalar2', ty, ![A : $t]: (('type/semi_ring/semi_ring' A) > (('type/list/list' 'type/quote/index') > (('type/canonical/canonical_sum' A) > ('type/canonical/canonical_sum' A))))).
tt('const/canonical/canonical_sum_scalar3', ty, ![A : $t]: (('type/semi_ring/semi_ring' A) > (A > (('type/list/list' 'type/quote/index') > (('type/canonical/canonical_sum' A) > ('type/canonical/canonical_sum' A)))))).
tt('const/canonical/canonical_sum_simplify', ty, ![A : $t]: (('type/semi_ring/semi_ring' A) > (('type/canonical/canonical_sum' A) > ('type/canonical/canonical_sum' A)))).
tt('const/canonical/canonical_sum_size', ty, ![A : $t]: ((A > 'type/num/num') > (('type/canonical/canonical_sum' A) > 'type/num/num'))).
tt('const/canonical/ics_aux', ty, ![A : $t]: (('type/semi_ring/semi_ring' A) > (('type/quote/varmap' A) > (A > (('type/canonical/canonical_sum' A) > A))))).
tt('const/canonical/interp_cs', ty, ![A : $t]: (('type/semi_ring/semi_ring' A) > (('type/quote/varmap' A) > (('type/canonical/canonical_sum' A) > A)))).
tt('const/canonical/interp_m', ty, ![A : $t]: (('type/semi_ring/semi_ring' A) > (('type/quote/varmap' A) > (A > (('type/list/list' 'type/quote/index') > A))))).
tt('const/canonical/interp_sp', ty, ![A : $t]: (('type/semi_ring/semi_ring' A) > (('type/quote/varmap' A) > (('type/canonical/spolynom' A) > A)))).
tt('const/canonical/interp_vl', ty, ![A : $t]: (('type/semi_ring/semi_ring' A) > (('type/quote/varmap' A) > (('type/list/list' 'type/quote/index') > A)))).
tt('const/canonical/ivl_aux', ty, ![A : $t]: (('type/semi_ring/semi_ring' A) > (('type/quote/varmap' A) > ('type/quote/index' > (('type/list/list' 'type/quote/index') > A))))).
tt('const/canonical/monom_insert', ty, ![A : $t]: (('type/semi_ring/semi_ring' A) > (A > (('type/list/list' 'type/quote/index') > (('type/canonical/canonical_sum' A) > ('type/canonical/canonical_sum' A)))))).
tt('const/canonical/monom_insert_tupled', ty, ![A : $t]: (('type/pair/prod' ('type/semi_ring/semi_ring' A) ('type/pair/prod' A ('type/pair/prod' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A)))) > ('type/canonical/canonical_sum' A))).
tt('const/canonical/spolynom_CASE', ty, ![A : $t, B : $t]: (('type/canonical/spolynom' A) > (('type/quote/index' > B) > ((A > B) > ((('type/canonical/spolynom' A) > (('type/canonical/spolynom' A) > B)) > ((('type/canonical/spolynom' A) > (('type/canonical/spolynom' A) > B)) > B)))))).
tt('const/canonical/spolynom_normalize', ty, ![A : $t]: (('type/semi_ring/semi_ring' A) > (('type/canonical/spolynom' A) > ('type/canonical/canonical_sum' A)))).
tt('const/canonical/spolynom_simplify', ty, ![A : $t]: (('type/semi_ring/semi_ring' A) > (('type/canonical/spolynom' A) > ('type/canonical/canonical_sum' A)))).
tt('const/canonical/spolynom_size', ty, ![A : $t]: ((A > 'type/num/num') > (('type/canonical/spolynom' A) > 'type/num/num'))).
tt('const/canonical/varlist_insert', ty, ![A : $t]: (('type/semi_ring/semi_ring' A) > (('type/list/list' 'type/quote/index') > (('type/canonical/canonical_sum' A) > ('type/canonical/canonical_sum' A))))).
tt('const/canonical/varlist_insert_tupled', ty, ![A : $t]: (('type/pair/prod' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A))) > ('type/canonical/canonical_sum' A))).
tt('thm/canonical/canonical_sum_TY_DEF_', def, ![A : $t]: (?[rep : (('type/canonical/canonical_sum' A) > ('type/ind_type/recspace' ('type/pair/prod' A ('type/list/list' 'type/quote/index'))))]: (('const/bool/TYPE_DEFINITION' ('type/ind_type/recspace' ('type/pair/prod' A ('type/list/list' 'type/quote/index'))) ('type/canonical/canonical_sum' A)) (^['a0\'' : ('type/ind_type/recspace' ('type/pair/prod' A ('type/list/list' 'type/quote/index')))]: (!['\'canonical_sum\'' : (('type/ind_type/recspace' ('type/pair/prod' A ('type/list/list' 'type/quote/index'))) > $o)]: ((!['a0\'0' : ('type/ind_type/recspace' ('type/pair/prod' A ('type/list/list' 'type/quote/index')))]: ((('a0\'0' = (('const/ind_type/CONSTR' ('type/pair/prod' A ('type/list/list' 'type/quote/index'))) 'const/num/0' (('const/pair/,' A ('type/list/list' 'type/quote/index')) ('const/bool/ARB' A) ('const/bool/ARB' ('type/list/list' 'type/quote/index'))) (^[n : 'type/num/num']: ('const/ind_type/BOTTOM' ('type/pair/prod' A ('type/list/list' 'type/quote/index')))))) | ((?[a0 : A, a1 : ('type/list/list' 'type/quote/index'), a2 : ('type/ind_type/recspace' ('type/pair/prod' A ('type/list/list' 'type/quote/index')))]: (('a0\'0' = ((^[a00 : A, a10 : ('type/list/list' 'type/quote/index'), a20 : ('type/ind_type/recspace' ('type/pair/prod' A ('type/list/list' 'type/quote/index')))]: (('const/ind_type/CONSTR' ('type/pair/prod' A ('type/list/list' 'type/quote/index'))) ('const/num/SUC' 'const/num/0') (('const/pair/,' A ('type/list/list' 'type/quote/index')) a00 a10) (('const/ind_type/FCONS' ('type/ind_type/recspace' ('type/pair/prod' A ('type/list/list' 'type/quote/index')))) a20 (^[n : 'type/num/num']: ('const/ind_type/BOTTOM' ('type/pair/prod' A ('type/list/list' 'type/quote/index'))))))) a0 a1 a2)) & ('\'canonical_sum\'' a2))) | (?[a0 : ('type/list/list' 'type/quote/index'), a1 : ('type/ind_type/recspace' ('type/pair/prod' A ('type/list/list' 'type/quote/index')))]: (('a0\'0' = ((^[a00 : ('type/list/list' 'type/quote/index'), a10 : ('type/ind_type/recspace' ('type/pair/prod' A ('type/list/list' 'type/quote/index')))]: (('const/ind_type/CONSTR' ('type/pair/prod' A ('type/list/list' 'type/quote/index'))) ('const/num/SUC' ('const/num/SUC' 'const/num/0')) (('const/pair/,' A ('type/list/list' 'type/quote/index')) ('const/bool/ARB' A) a00) (('const/ind_type/FCONS' ('type/ind_type/recspace' ('type/pair/prod' A ('type/list/list' 'type/quote/index')))) a10 (^[n : 'type/num/num']: ('const/ind_type/BOTTOM' ('type/pair/prod' A ('type/list/list' 'type/quote/index'))))))) a0 a1)) & ('\'canonical_sum\'' a1))))) => ('\'canonical_sum\'' 'a0\'0'))) => ('\'canonical_sum\'' 'a0\'')))) rep))).
tt('thm/canonical/canonical_sum_case_def_0', def, ![B : $t, A : $t]: (![v : B, f : (A > (('type/list/list' 'type/quote/index') > (('type/canonical/canonical_sum' A) > B))), f1 : (('type/list/list' 'type/quote/index') > (('type/canonical/canonical_sum' A) > B))]: ((('const/canonical/canonical_sum_CASE' A B) ('const/canonical/Nil_monom' A) v f f1) = v))).
tt('thm/canonical/canonical_sum_case_def_1', def, ![A : $t, B : $t]: (![a0 : A, a1 : ('type/list/list' 'type/quote/index'), a2 : ('type/canonical/canonical_sum' A), v : B, f : (A > (('type/list/list' 'type/quote/index') > (('type/canonical/canonical_sum' A) > B))), f1 : (('type/list/list' 'type/quote/index') > (('type/canonical/canonical_sum' A) > B))]: ((('const/canonical/canonical_sum_CASE' A B) (('const/canonical/Cons_monom' A) a0 a1 a2) v f f1) = (f a0 a1 a2)))).
tt('thm/canonical/canonical_sum_case_def_e2', def, ![A : $t, B : $t]: (![a0 : ('type/list/list' 'type/quote/index'), a1 : ('type/canonical/canonical_sum' A), v : B, f : (A > (('type/list/list' 'type/quote/index') > (('type/canonical/canonical_sum' A) > B))), f1 : (('type/list/list' 'type/quote/index') > (('type/canonical/canonical_sum' A) > B))]: ((('const/canonical/canonical_sum_CASE' A B) (('const/canonical/Cons_varlist' A) a0 a1) v f f1) = (f1 a0 a1)))).
tt('thm/canonical/canonical_sum_size_def_0', def, ![A : $t]: (![f : (A > 'type/num/num')]: ((('const/canonical/canonical_sum_size' A) f ('const/canonical/Nil_monom' A)) = 'const/num/0'))).
tt('thm/canonical/canonical_sum_size_def_1', def, ![A : $t]: (![f : (A > 'type/num/num'), a0 : A, a1 : ('type/list/list' 'type/quote/index'), a2 : ('type/canonical/canonical_sum' A)]: ((('const/canonical/canonical_sum_size' A) f (('const/canonical/Cons_monom' A) a0 a1 a2)) = ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) ('const/arithmetic/+' (f a0) ('const/arithmetic/+' (('const/list/list_size' 'type/quote/index') 'const/quote/index_size' a1) (('const/canonical/canonical_sum_size' A) f a2))))))).
tt('thm/canonical/canonical_sum_size_def_e2', def, ![A : $t]: (![f : (A > 'type/num/num'), a0 : ('type/list/list' 'type/quote/index'), a1 : ('type/canonical/canonical_sum' A)]: ((('const/canonical/canonical_sum_size' A) f (('const/canonical/Cons_varlist' A) a0 a1)) = ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) ('const/arithmetic/+' (('const/list/list_size' 'type/quote/index') 'const/quote/index_size' a0) (('const/canonical/canonical_sum_size' A) f a1)))))).
tt('thm/canonical/datatype_canonical_sum_', ax, ![A : $t]: (![canonical_sum : (('type/canonical/canonical_sum' A) > ((A > (('type/list/list' 'type/quote/index') > (('type/canonical/canonical_sum' A) > ('type/canonical/canonical_sum' A)))) > ((('type/list/list' 'type/quote/index') > (('type/canonical/canonical_sum' A) > ('type/canonical/canonical_sum' A))) > $o)))]: (('const/bool/DATATYPE' $o) (canonical_sum ('const/canonical/Nil_monom' A) ('const/canonical/Cons_monom' A) ('const/canonical/Cons_varlist' A))))).
tt('thm/canonical/canonical_sum_11_0', ax, ![A : $t]: (![a0 : A, a1 : ('type/list/list' 'type/quote/index'), a2 : ('type/canonical/canonical_sum' A), 'a0\'' : A, 'a1\'' : ('type/list/list' 'type/quote/index'), 'a2\'' : ('type/canonical/canonical_sum' A)]: (((('const/canonical/Cons_monom' A) a0 a1 a2) = (('const/canonical/Cons_monom' A) 'a0\'' 'a1\'' 'a2\'')) = ((a0 = 'a0\'') & ((a1 = 'a1\'') & (a2 = 'a2\'')))))).
tt('thm/canonical/canonical_sum_11_e1', ax, ![A : $t]: (![a0 : ('type/list/list' 'type/quote/index'), a1 : ('type/canonical/canonical_sum' A), 'a0\'' : ('type/list/list' 'type/quote/index'), 'a1\'' : ('type/canonical/canonical_sum' A)]: (((('const/canonical/Cons_varlist' A) a0 a1) = (('const/canonical/Cons_varlist' A) 'a0\'' 'a1\'')) = ((a0 = 'a0\'') & (a1 = 'a1\''))))).
tt('thm/canonical/canonical_sum_distinct_0', ax, ![A : $t]: (![a2 : ('type/canonical/canonical_sum' A), a1 : ('type/list/list' 'type/quote/index'), a0 : A]: (~ (('const/canonical/Nil_monom' A) = (('const/canonical/Cons_monom' A) a0 a1 a2))))).
tt('thm/canonical/canonical_sum_distinct_1', ax, ![A : $t]: (![a1 : ('type/canonical/canonical_sum' A), a0 : ('type/list/list' 'type/quote/index')]: (~ (('const/canonical/Nil_monom' A) = (('const/canonical/Cons_varlist' A) a0 a1))))).
tt('thm/canonical/canonical_sum_distinct_e2', ax, ![A : $t]: (![a2 : ('type/canonical/canonical_sum' A), 'a1\'' : ('type/canonical/canonical_sum' A), a1 : ('type/list/list' 'type/quote/index'), 'a0\'' : ('type/list/list' 'type/quote/index'), a0 : A]: (~ ((('const/canonical/Cons_monom' A) a0 a1 a2) = (('const/canonical/Cons_varlist' A) 'a0\'' 'a1\''))))).
tt('thm/canonical/canonical_sum_case_cong_', ax, ![A : $t, B : $t]: (!['v\'' : B, 'f1\'' : (('type/list/list' 'type/quote/index') > (('type/canonical/canonical_sum' A) > B)), 'f\'' : (A > (('type/list/list' 'type/quote/index') > (('type/canonical/canonical_sum' A) > B))), M : ('type/canonical/canonical_sum' A), 'M\'' : ('type/canonical/canonical_sum' A), v : B, f : (A > (('type/list/list' 'type/quote/index') > (('type/canonical/canonical_sum' A) > B))), f1 : (('type/list/list' 'type/quote/index') > (('type/canonical/canonical_sum' A) > B))]: (((M = 'M\'') & ((('M\'' = ('const/canonical/Nil_monom' A)) => (v = 'v\'')) & ((![a0 : A, a1 : ('type/list/list' 'type/quote/index'), a2 : ('type/canonical/canonical_sum' A)]: (('M\'' = (('const/canonical/Cons_monom' A) a0 a1 a2)) => ((f a0 a1 a2) = ('f\'' a0 a1 a2)))) & (![a0 : ('type/list/list' 'type/quote/index'), a1 : ('type/canonical/canonical_sum' A)]: (('M\'' = (('const/canonical/Cons_varlist' A) a0 a1)) => ((f1 a0 a1) = ('f1\'' a0 a1))))))) => ((('const/canonical/canonical_sum_CASE' A B) M v f f1) = (('const/canonical/canonical_sum_CASE' A B) 'M\'' 'v\'' 'f\'' 'f1\''))))).
tt('thm/canonical/canonical_sum_nchotomy_', ax, ![A : $t]: (![cc : ('type/canonical/canonical_sum' A)]: ((cc = ('const/canonical/Nil_monom' A)) | ((?[a : A, l : ('type/list/list' 'type/quote/index'), c : ('type/canonical/canonical_sum' A)]: (cc = (('const/canonical/Cons_monom' A) a l c))) | (?[l : ('type/list/list' 'type/quote/index'), c : ('type/canonical/canonical_sum' A)]: (cc = (('const/canonical/Cons_varlist' A) l c))))))).
tt('thm/canonical/canonical_sum_Axiom_', ax, ![A : $t, B : $t]: (![f0 : B, f1 : (A > (('type/list/list' 'type/quote/index') > (('type/canonical/canonical_sum' A) > (B > B)))), f2 : (('type/list/list' 'type/quote/index') > (('type/canonical/canonical_sum' A) > (B > B)))]: (?[fn : (('type/canonical/canonical_sum' A) > B)]: (((fn ('const/canonical/Nil_monom' A)) = f0) & ((![a0 : A, a1 : ('type/list/list' 'type/quote/index'), a2 : ('type/canonical/canonical_sum' A)]: ((fn (('const/canonical/Cons_monom' A) a0 a1 a2)) = (f1 a0 a1 a2 (fn a2)))) & (![a0 : ('type/list/list' 'type/quote/index'), a1 : ('type/canonical/canonical_sum' A)]: ((fn (('const/canonical/Cons_varlist' A) a0 a1)) = (f2 a0 a1 (fn a1))))))))).
tt('thm/canonical/canonical_sum_induction_', ax, ![A : $t]: (![P : (('type/canonical/canonical_sum' A) > $o)]: (((P ('const/canonical/Nil_monom' A)) & ((![c : ('type/canonical/canonical_sum' A)]: ((P c) => (![l : ('type/list/list' 'type/quote/index'), a : A]: (P (('const/canonical/Cons_monom' A) a l c))))) & (![c : ('type/canonical/canonical_sum' A)]: ((P c) => (![l : ('type/list/list' 'type/quote/index')]: (P (('const/canonical/Cons_varlist' A) l c))))))) => (![c : ('type/canonical/canonical_sum' A)]: (P c))))).
tt('thm/canonical/canonical_sum_merge_tupled_primitive_def_', def, ![A : $t]: (('const/canonical/canonical_sum_merge_tupled' A) = (('const/relation/WFREC' ('type/pair/prod' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))) ('type/canonical/canonical_sum' A)) (('const/min/@' (('type/pair/prod' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))) > (('type/pair/prod' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))) > $o))) (^[R : (('type/pair/prod' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))) > (('type/pair/prod' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))) > $o))]: ((('const/relation/WF' ('type/pair/prod' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A)))) R) & ((![l2 : ('type/list/list' 'type/quote/index'), c2 : A, t2 : ('type/canonical/canonical_sum' A), t1 : ('type/canonical/canonical_sum' A), l1 : ('type/list/list' 'type/quote/index'), c1 : A, sr : ('type/semi_ring/semi_ring' A)]: (R (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))) sr (('const/pair/,' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A)) (('const/canonical/Cons_monom' A) c1 l1 t1) t2)) (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))) sr (('const/pair/,' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A)) (('const/canonical/Cons_monom' A) c1 l1 t1) (('const/canonical/Cons_monom' A) c2 l2 t2))))) & ((![l1 : ('type/list/list' 'type/quote/index'), c1 : A, t2 : ('type/canonical/canonical_sum' A), l2 : ('type/list/list' 'type/quote/index'), c2 : A, t1 : ('type/canonical/canonical_sum' A), sr : ('type/semi_ring/semi_ring' A)]: (R (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))) sr (('const/pair/,' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A)) t1 (('const/canonical/Cons_monom' A) c2 l2 t2))) (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))) sr (('const/pair/,' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A)) (('const/canonical/Cons_monom' A) c1 l1 t1) (('const/canonical/Cons_monom' A) c2 l2 t2))))) & ((![l2 : ('type/list/list' 'type/quote/index'), c2 : A, l1 : ('type/list/list' 'type/quote/index'), c1 : A, t2 : ('type/canonical/canonical_sum' A), t1 : ('type/canonical/canonical_sum' A), sr : ('type/semi_ring/semi_ring' A)]: (R (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))) sr (('const/pair/,' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A)) t1 t2)) (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))) sr (('const/pair/,' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A)) (('const/canonical/Cons_monom' A) c1 l1 t1) (('const/canonical/Cons_monom' A) c2 l2 t2))))) & ((![l2 : ('type/list/list' 'type/quote/index'), t2 : ('type/canonical/canonical_sum' A), t1 : ('type/canonical/canonical_sum' A), l1 : ('type/list/list' 'type/quote/index'), c1 : A, sr : ('type/semi_ring/semi_ring' A)]: (R (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))) sr (('const/pair/,' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A)) (('const/canonical/Cons_monom' A) c1 l1 t1) t2)) (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))) sr (('const/pair/,' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A)) (('const/canonical/Cons_monom' A) c1 l1 t1) (('const/canonical/Cons_varlist' A) l2 t2))))) & ((![l1 : ('type/list/list' 'type/quote/index'), c1 : A, t2 : ('type/canonical/canonical_sum' A), l2 : ('type/list/list' 'type/quote/index'), t1 : ('type/canonical/canonical_sum' A), sr : ('type/semi_ring/semi_ring' A)]: (R (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))) sr (('const/pair/,' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A)) t1 (('const/canonical/Cons_varlist' A) l2 t2))) (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))) sr (('const/pair/,' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A)) (('const/canonical/Cons_monom' A) c1 l1 t1) (('const/canonical/Cons_varlist' A) l2 t2))))) & ((![l2 : ('type/list/list' 'type/quote/index'), l1 : ('type/list/list' 'type/quote/index'), c1 : A, t2 : ('type/canonical/canonical_sum' A), t1 : ('type/canonical/canonical_sum' A), sr : ('type/semi_ring/semi_ring' A)]: (R (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))) sr (('const/pair/,' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A)) t1 t2)) (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))) sr (('const/pair/,' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A)) (('const/canonical/Cons_monom' A) c1 l1 t1) (('const/canonical/Cons_varlist' A) l2 t2))))) & ((![l2 : ('type/list/list' 'type/quote/index'), c2 : A, t2 : ('type/canonical/canonical_sum' A), t1 : ('type/canonical/canonical_sum' A), l1 : ('type/list/list' 'type/quote/index'), sr : ('type/semi_ring/semi_ring' A)]: (R (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))) sr (('const/pair/,' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A)) (('const/canonical/Cons_varlist' A) l1 t1) t2)) (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))) sr (('const/pair/,' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A)) (('const/canonical/Cons_varlist' A) l1 t1) (('const/canonical/Cons_monom' A) c2 l2 t2))))) & ((![l1 : ('type/list/list' 'type/quote/index'), t2 : ('type/canonical/canonical_sum' A), l2 : ('type/list/list' 'type/quote/index'), c2 : A, t1 : ('type/canonical/canonical_sum' A), sr : ('type/semi_ring/semi_ring' A)]: (R (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))) sr (('const/pair/,' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A)) t1 (('const/canonical/Cons_monom' A) c2 l2 t2))) (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))) sr (('const/pair/,' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A)) (('const/canonical/Cons_varlist' A) l1 t1) (('const/canonical/Cons_monom' A) c2 l2 t2))))) & ((![l2 : ('type/list/list' 'type/quote/index'), c2 : A, l1 : ('type/list/list' 'type/quote/index'), t2 : ('type/canonical/canonical_sum' A), t1 : ('type/canonical/canonical_sum' A), sr : ('type/semi_ring/semi_ring' A)]: (R (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))) sr (('const/pair/,' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A)) t1 t2)) (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))) sr (('const/pair/,' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A)) (('const/canonical/Cons_varlist' A) l1 t1) (('const/canonical/Cons_monom' A) c2 l2 t2))))) & ((![l2 : ('type/list/list' 'type/quote/index'), l1 : ('type/list/list' 'type/quote/index'), t2 : ('type/canonical/canonical_sum' A), t1 : ('type/canonical/canonical_sum' A), sr : ('type/semi_ring/semi_ring' A)]: (R (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))) sr (('const/pair/,' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A)) t1 t2)) (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))) sr (('const/pair/,' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A)) (('const/canonical/Cons_varlist' A) l1 t1) (('const/canonical/Cons_varlist' A) l2 t2))))) & ((![l1 : ('type/list/list' 'type/quote/index'), t2 : ('type/canonical/canonical_sum' A), l2 : ('type/list/list' 'type/quote/index'), t1 : ('type/canonical/canonical_sum' A), sr : ('type/semi_ring/semi_ring' A)]: (R (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))) sr (('const/pair/,' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A)) t1 (('const/canonical/Cons_varlist' A) l2 t2))) (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))) sr (('const/pair/,' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A)) (('const/canonical/Cons_varlist' A) l1 t1) (('const/canonical/Cons_varlist' A) l2 t2))))) & (![l2 : ('type/list/list' 'type/quote/index'), t2 : ('type/canonical/canonical_sum' A), t1 : ('type/canonical/canonical_sum' A), l1 : ('type/list/list' 'type/quote/index'), sr : ('type/semi_ring/semi_ring' A)]: (R (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))) sr (('const/pair/,' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A)) (('const/canonical/Cons_varlist' A) l1 t1) t2)) (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))) sr (('const/pair/,' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A)) (('const/canonical/Cons_varlist' A) l1 t1) (('const/canonical/Cons_varlist' A) l2 t2))))))))))))))))))) (^[canonical_sum_merge_tupled : (('type/pair/prod' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))) > ('type/canonical/canonical_sum' A)), a : ('type/pair/prod' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A)))]: (('const/pair/pair_CASE' ('type/canonical/canonical_sum' A) ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))) a (^[sr : ('type/semi_ring/semi_ring' A), v1 : ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))]: (('const/pair/pair_CASE' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A)) v1 (^[s1 : ('type/canonical/canonical_sum' A), v3 : ('type/canonical/canonical_sum' A)]: (('const/canonical/canonical_sum_CASE' A ('type/canonical/canonical_sum' A)) v3 (('const/combin/I' ('type/canonical/canonical_sum' A)) s1) (^[c2 : A, l2 : ('type/list/list' 'type/quote/index'), t2 : ('type/canonical/canonical_sum' A)]: (('const/canonical/canonical_sum_CASE' A ('type/canonical/canonical_sum' A)) s1 (('const/combin/I' ('type/canonical/canonical_sum' A)) (('const/canonical/Cons_monom' A) c2 l2 t2)) (^[c1 : A, l1 : ('type/list/list' 'type/quote/index'), t1 : ('type/canonical/canonical_sum' A)]: (('const/combin/I' ('type/canonical/canonical_sum' A)) (('const/prelim/compare' ('type/canonical/canonical_sum' A)) (('const/prelim/list_compare' 'type/quote/index' 'type/quote/index') 'const/quote/index_compare' l1 l2) (('const/canonical/Cons_monom' A) c1 l1 (canonical_sum_merge_tupled (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))) sr (('const/pair/,' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A)) t1 (('const/canonical/Cons_monom' A) c2 l2 t2))))) (('const/canonical/Cons_monom' A) (('const/semi_ring/semi_ring_SRP' A) sr c1 c2) l1 (canonical_sum_merge_tupled (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))) sr (('const/pair/,' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A)) t1 t2)))) (('const/canonical/Cons_monom' A) c2 l2 (canonical_sum_merge_tupled (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))) sr (('const/pair/,' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A)) (('const/canonical/Cons_monom' A) c1 l1 t1) t2))))))) (^['l1\'\'' : ('type/list/list' 'type/quote/index'), 't1\'\'' : ('type/canonical/canonical_sum' A)]: (('const/combin/I' ('type/canonical/canonical_sum' A)) (('const/prelim/compare' ('type/canonical/canonical_sum' A)) (('const/prelim/list_compare' 'type/quote/index' 'type/quote/index') 'const/quote/index_compare' 'l1\'\'' l2) (('const/canonical/Cons_varlist' A) 'l1\'\'' (canonical_sum_merge_tupled (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))) sr (('const/pair/,' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A)) 't1\'\'' (('const/canonical/Cons_monom' A) c2 l2 t2))))) (('const/canonical/Cons_monom' A) (('const/semi_ring/semi_ring_SRP' A) sr (('const/semi_ring/semi_ring_SR1' A) sr) c2) 'l1\'\'' (canonical_sum_merge_tupled (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))) sr (('const/pair/,' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A)) 't1\'\'' t2)))) (('const/canonical/Cons_monom' A) c2 l2 (canonical_sum_merge_tupled (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))) sr (('const/pair/,' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A)) (('const/canonical/Cons_varlist' A) 'l1\'\'' 't1\'\'') t2))))))))) (^['l2\'' : ('type/list/list' 'type/quote/index'), 't2\'' : ('type/canonical/canonical_sum' A)]: (('const/canonical/canonical_sum_CASE' A ('type/canonical/canonical_sum' A)) s1 (('const/combin/I' ('type/canonical/canonical_sum' A)) (('const/canonical/Cons_varlist' A) 'l2\'' 't2\'')) (^['c1\'' : A, 'l1\'' : ('type/list/list' 'type/quote/index'), 't1\'' : ('type/canonical/canonical_sum' A)]: (('const/combin/I' ('type/canonical/canonical_sum' A)) (('const/prelim/compare' ('type/canonical/canonical_sum' A)) (('const/prelim/list_compare' 'type/quote/index' 'type/quote/index') 'const/quote/index_compare' 'l1\'' 'l2\'') (('const/canonical/Cons_monom' A) 'c1\'' 'l1\'' (canonical_sum_merge_tupled (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))) sr (('const/pair/,' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A)) 't1\'' (('const/canonical/Cons_varlist' A) 'l2\'' 't2\''))))) (('const/canonical/Cons_monom' A) (('const/semi_ring/semi_ring_SRP' A) sr 'c1\'' (('const/semi_ring/semi_ring_SR1' A) sr)) 'l1\'' (canonical_sum_merge_tupled (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))) sr (('const/pair/,' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A)) 't1\'' 't2\'')))) (('const/canonical/Cons_varlist' A) 'l2\'' (canonical_sum_merge_tupled (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))) sr (('const/pair/,' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A)) (('const/canonical/Cons_monom' A) 'c1\'' 'l1\'' 't1\'') 't2\''))))))) (^['l1\'\'\'' : ('type/list/list' 'type/quote/index'), 't1\'\'\'' : ('type/canonical/canonical_sum' A)]: (('const/combin/I' ('type/canonical/canonical_sum' A)) (('const/prelim/compare' ('type/canonical/canonical_sum' A)) (('const/prelim/list_compare' 'type/quote/index' 'type/quote/index') 'const/quote/index_compare' 'l1\'\'\'' 'l2\'') (('const/canonical/Cons_varlist' A) 'l1\'\'\'' (canonical_sum_merge_tupled (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))) sr (('const/pair/,' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A)) 't1\'\'\'' (('const/canonical/Cons_varlist' A) 'l2\'' 't2\''))))) (('const/canonical/Cons_monom' A) (('const/semi_ring/semi_ring_SRP' A) sr (('const/semi_ring/semi_ring_SR1' A) sr) (('const/semi_ring/semi_ring_SR1' A) sr)) 'l1\'\'\'' (canonical_sum_merge_tupled (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))) sr (('const/pair/,' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A)) 't1\'\'\'' 't2\'')))) (('const/canonical/Cons_varlist' A) 'l2\'' (canonical_sum_merge_tupled (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))) sr (('const/pair/,' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A)) (('const/canonical/Cons_varlist' A) 'l1\'\'\'' 't1\'\'\'') 't2\'')))))))))))))))))).
tt('thm/canonical/canonical_sum_merge_curried_def_', def, ![A : $t]: (![x : ('type/semi_ring/semi_ring' A), x1 : ('type/canonical/canonical_sum' A), x2 : ('type/canonical/canonical_sum' A)]: ((('const/canonical/canonical_sum_merge' A) x x1 x2) = (('const/canonical/canonical_sum_merge_tupled' A) (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A))) x (('const/pair/,' ('type/canonical/canonical_sum' A) ('type/canonical/canonical_sum' A)) x1 x2)))))).
tt('thm/canonical/canonical_sum_merge_ind_', ax, ![A : $t]: (![P : (('type/semi_ring/semi_ring' A) > (('type/canonical/canonical_sum' A) > (('type/canonical/canonical_sum' A) > $o)))]: (((![sr : ('type/semi_ring/semi_ring' A), c1 : A, l1 : ('type/list/list' 'type/quote/index'), t1 : ('type/canonical/canonical_sum' A), c2 : A, l2 : ('type/list/list' 'type/quote/index'), t2 : ('type/canonical/canonical_sum' A)]: (((P sr t1 t2) & ((P sr t1 (('const/canonical/Cons_monom' A) c2 l2 t2)) & (P sr (('const/canonical/Cons_monom' A) c1 l1 t1) t2))) => (P sr (('const/canonical/Cons_monom' A) c1 l1 t1) (('const/canonical/Cons_monom' A) c2 l2 t2)))) & ((![sr : ('type/semi_ring/semi_ring' A), c1 : A, l1 : ('type/list/list' 'type/quote/index'), t1 : ('type/canonical/canonical_sum' A), l2 : ('type/list/list' 'type/quote/index'), t2 : ('type/canonical/canonical_sum' A)]: (((P sr t1 t2) & ((P sr t1 (('const/canonical/Cons_varlist' A) l2 t2)) & (P sr (('const/canonical/Cons_monom' A) c1 l1 t1) t2))) => (P sr (('const/canonical/Cons_monom' A) c1 l1 t1) (('const/canonical/Cons_varlist' A) l2 t2)))) & ((![sr : ('type/semi_ring/semi_ring' A), l1 : ('type/list/list' 'type/quote/index'), t1 : ('type/canonical/canonical_sum' A), c2 : A, l2 : ('type/list/list' 'type/quote/index'), t2 : ('type/canonical/canonical_sum' A)]: (((P sr t1 t2) & ((P sr t1 (('const/canonical/Cons_monom' A) c2 l2 t2)) & (P sr (('const/canonical/Cons_varlist' A) l1 t1) t2))) => (P sr (('const/canonical/Cons_varlist' A) l1 t1) (('const/canonical/Cons_monom' A) c2 l2 t2)))) & ((![sr : ('type/semi_ring/semi_ring' A), l1 : ('type/list/list' 'type/quote/index'), t1 : ('type/canonical/canonical_sum' A), l2 : ('type/list/list' 'type/quote/index'), t2 : ('type/canonical/canonical_sum' A)]: (((P sr t1 t2) & ((P sr t1 (('const/canonical/Cons_varlist' A) l2 t2)) & (P sr (('const/canonical/Cons_varlist' A) l1 t1) t2))) => (P sr (('const/canonical/Cons_varlist' A) l1 t1) (('const/canonical/Cons_varlist' A) l2 t2)))) & ((![sr : ('type/semi_ring/semi_ring' A), s1 : ('type/canonical/canonical_sum' A)]: (P sr s1 ('const/canonical/Nil_monom' A))) & ((![sr : ('type/semi_ring/semi_ring' A), v4 : A, v5 : ('type/list/list' 'type/quote/index'), v6 : ('type/canonical/canonical_sum' A)]: (P sr ('const/canonical/Nil_monom' A) (('const/canonical/Cons_monom' A) v4 v5 v6))) & (![sr : ('type/semi_ring/semi_ring' A), v7 : ('type/list/list' 'type/quote/index'), v8 : ('type/canonical/canonical_sum' A)]: (P sr ('const/canonical/Nil_monom' A) (('const/canonical/Cons_varlist' A) v7 v8))))))))) => (![v : ('type/semi_ring/semi_ring' A), v1 : ('type/canonical/canonical_sum' A), v2 : ('type/canonical/canonical_sum' A)]: (P v v1 v2))))).
tt('thm/canonical/canonical_sum_merge_def_0', ax, ![A : $t]: (![t2 : ('type/canonical/canonical_sum' A), t1 : ('type/canonical/canonical_sum' A), sr : ('type/semi_ring/semi_ring' A), l2 : ('type/list/list' 'type/quote/index'), l1 : ('type/list/list' 'type/quote/index'), c2 : A, c1 : A]: ((('const/canonical/canonical_sum_merge' A) sr (('const/canonical/Cons_monom' A) c1 l1 t1) (('const/canonical/Cons_monom' A) c2 l2 t2)) = (('const/prelim/compare' ('type/canonical/canonical_sum' A)) (('const/prelim/list_compare' 'type/quote/index' 'type/quote/index') 'const/quote/index_compare' l1 l2) (('const/canonical/Cons_monom' A) c1 l1 (('const/canonical/canonical_sum_merge' A) sr t1 (('const/canonical/Cons_monom' A) c2 l2 t2))) (('const/canonical/Cons_monom' A) (('const/semi_ring/semi_ring_SRP' A) sr c1 c2) l1 (('const/canonical/canonical_sum_merge' A) sr t1 t2)) (('const/canonical/Cons_monom' A) c2 l2 (('const/canonical/canonical_sum_merge' A) sr (('const/canonical/Cons_monom' A) c1 l1 t1) t2)))))).
tt('thm/canonical/canonical_sum_merge_def_1', ax, ![A : $t]: (![t2 : ('type/canonical/canonical_sum' A), t1 : ('type/canonical/canonical_sum' A), sr : ('type/semi_ring/semi_ring' A), l2 : ('type/list/list' 'type/quote/index'), l1 : ('type/list/list' 'type/quote/index'), c1 : A]: ((('const/canonical/canonical_sum_merge' A) sr (('const/canonical/Cons_monom' A) c1 l1 t1) (('const/canonical/Cons_varlist' A) l2 t2)) = (('const/prelim/compare' ('type/canonical/canonical_sum' A)) (('const/prelim/list_compare' 'type/quote/index' 'type/quote/index') 'const/quote/index_compare' l1 l2) (('const/canonical/Cons_monom' A) c1 l1 (('const/canonical/canonical_sum_merge' A) sr t1 (('const/canonical/Cons_varlist' A) l2 t2))) (('const/canonical/Cons_monom' A) (('const/semi_ring/semi_ring_SRP' A) sr c1 (('const/semi_ring/semi_ring_SR1' A) sr)) l1 (('const/canonical/canonical_sum_merge' A) sr t1 t2)) (('const/canonical/Cons_varlist' A) l2 (('const/canonical/canonical_sum_merge' A) sr (('const/canonical/Cons_monom' A) c1 l1 t1) t2)))))).
tt('thm/canonical/canonical_sum_merge_def_2', ax, ![A : $t]: (![t2 : ('type/canonical/canonical_sum' A), t1 : ('type/canonical/canonical_sum' A), sr : ('type/semi_ring/semi_ring' A), l2 : ('type/list/list' 'type/quote/index'), l1 : ('type/list/list' 'type/quote/index'), c2 : A]: ((('const/canonical/canonical_sum_merge' A) sr (('const/canonical/Cons_varlist' A) l1 t1) (('const/canonical/Cons_monom' A) c2 l2 t2)) = (('const/prelim/compare' ('type/canonical/canonical_sum' A)) (('const/prelim/list_compare' 'type/quote/index' 'type/quote/index') 'const/quote/index_compare' l1 l2) (('const/canonical/Cons_varlist' A) l1 (('const/canonical/canonical_sum_merge' A) sr t1 (('const/canonical/Cons_monom' A) c2 l2 t2))) (('const/canonical/Cons_monom' A) (('const/semi_ring/semi_ring_SRP' A) sr (('const/semi_ring/semi_ring_SR1' A) sr) c2) l1 (('const/canonical/canonical_sum_merge' A) sr t1 t2)) (('const/canonical/Cons_monom' A) c2 l2 (('const/canonical/canonical_sum_merge' A) sr (('const/canonical/Cons_varlist' A) l1 t1) t2)))))).
tt('thm/canonical/canonical_sum_merge_def_3', ax, ![A : $t]: (![t2 : ('type/canonical/canonical_sum' A), t1 : ('type/canonical/canonical_sum' A), sr : ('type/semi_ring/semi_ring' A), l2 : ('type/list/list' 'type/quote/index'), l1 : ('type/list/list' 'type/quote/index')]: ((('const/canonical/canonical_sum_merge' A) sr (('const/canonical/Cons_varlist' A) l1 t1) (('const/canonical/Cons_varlist' A) l2 t2)) = (('const/prelim/compare' ('type/canonical/canonical_sum' A)) (('const/prelim/list_compare' 'type/quote/index' 'type/quote/index') 'const/quote/index_compare' l1 l2) (('const/canonical/Cons_varlist' A) l1 (('const/canonical/canonical_sum_merge' A) sr t1 (('const/canonical/Cons_varlist' A) l2 t2))) (('const/canonical/Cons_monom' A) (('const/semi_ring/semi_ring_SRP' A) sr (('const/semi_ring/semi_ring_SR1' A) sr) (('const/semi_ring/semi_ring_SR1' A) sr)) l1 (('const/canonical/canonical_sum_merge' A) sr t1 t2)) (('const/canonical/Cons_varlist' A) l2 (('const/canonical/canonical_sum_merge' A) sr (('const/canonical/Cons_varlist' A) l1 t1) t2)))))).
tt('thm/canonical/canonical_sum_merge_def_4', ax, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A), s1 : ('type/canonical/canonical_sum' A)]: ((('const/canonical/canonical_sum_merge' A) sr s1 ('const/canonical/Nil_monom' A)) = s1))).
tt('thm/canonical/canonical_sum_merge_def_5', ax, ![A : $t]: (![v6 : ('type/canonical/canonical_sum' A), v5 : ('type/list/list' 'type/quote/index'), v4 : A, sr : ('type/semi_ring/semi_ring' A)]: ((('const/canonical/canonical_sum_merge' A) sr ('const/canonical/Nil_monom' A) (('const/canonical/Cons_monom' A) v4 v5 v6)) = (('const/canonical/Cons_monom' A) v4 v5 v6)))).
tt('thm/canonical/canonical_sum_merge_def_e6', ax, ![A : $t]: (![v8 : ('type/canonical/canonical_sum' A), v7 : ('type/list/list' 'type/quote/index'), sr : ('type/semi_ring/semi_ring' A)]: ((('const/canonical/canonical_sum_merge' A) sr ('const/canonical/Nil_monom' A) (('const/canonical/Cons_varlist' A) v7 v8)) = (('const/canonical/Cons_varlist' A) v7 v8)))).
tt('thm/canonical/monom_insert_tupled_primitive_def_', def, ![A : $t]: (('const/canonical/monom_insert_tupled' A) = (('const/relation/WFREC' ('type/pair/prod' ('type/semi_ring/semi_ring' A) ('type/pair/prod' A ('type/pair/prod' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A)))) ('type/canonical/canonical_sum' A)) (('const/min/@' (('type/pair/prod' ('type/semi_ring/semi_ring' A) ('type/pair/prod' A ('type/pair/prod' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A)))) > (('type/pair/prod' ('type/semi_ring/semi_ring' A) ('type/pair/prod' A ('type/pair/prod' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A)))) > $o))) (^[R : (('type/pair/prod' ('type/semi_ring/semi_ring' A) ('type/pair/prod' A ('type/pair/prod' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A)))) > (('type/pair/prod' ('type/semi_ring/semi_ring' A) ('type/pair/prod' A ('type/pair/prod' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A)))) > $o))]: ((('const/relation/WF' ('type/pair/prod' ('type/semi_ring/semi_ring' A) ('type/pair/prod' A ('type/pair/prod' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A))))) R) & ((![l2 : ('type/list/list' 'type/quote/index'), c2 : A, t2 : ('type/canonical/canonical_sum' A), l1 : ('type/list/list' 'type/quote/index'), c1 : A, sr : ('type/semi_ring/semi_ring' A)]: (R (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' A ('type/pair/prod' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A)))) sr (('const/pair/,' A ('type/pair/prod' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A))) c1 (('const/pair/,' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A)) l1 t2))) (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' A ('type/pair/prod' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A)))) sr (('const/pair/,' A ('type/pair/prod' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A))) c1 (('const/pair/,' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A)) l1 (('const/canonical/Cons_monom' A) c2 l2 t2)))))) & (![l2 : ('type/list/list' 'type/quote/index'), t2 : ('type/canonical/canonical_sum' A), l1 : ('type/list/list' 'type/quote/index'), c1 : A, sr : ('type/semi_ring/semi_ring' A)]: (R (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' A ('type/pair/prod' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A)))) sr (('const/pair/,' A ('type/pair/prod' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A))) c1 (('const/pair/,' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A)) l1 t2))) (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' A ('type/pair/prod' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A)))) sr (('const/pair/,' A ('type/pair/prod' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A))) c1 (('const/pair/,' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A)) l1 (('const/canonical/Cons_varlist' A) l2 t2)))))))))) (^[monom_insert_tupled : (('type/pair/prod' ('type/semi_ring/semi_ring' A) ('type/pair/prod' A ('type/pair/prod' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A)))) > ('type/canonical/canonical_sum' A)), a : ('type/pair/prod' ('type/semi_ring/semi_ring' A) ('type/pair/prod' A ('type/pair/prod' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A))))]: (('const/pair/pair_CASE' ('type/canonical/canonical_sum' A) ('type/semi_ring/semi_ring' A) ('type/pair/prod' A ('type/pair/prod' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A)))) a (^[sr : ('type/semi_ring/semi_ring' A), v1 : ('type/pair/prod' A ('type/pair/prod' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A)))]: (('const/pair/pair_CASE' ('type/canonical/canonical_sum' A) A ('type/pair/prod' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A))) v1 (^[c1 : A, v3 : ('type/pair/prod' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A))]: (('const/pair/pair_CASE' ('type/canonical/canonical_sum' A) ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A)) v3 (^[l1 : ('type/list/list' 'type/quote/index'), v5 : ('type/canonical/canonical_sum' A)]: (('const/canonical/canonical_sum_CASE' A ('type/canonical/canonical_sum' A)) v5 (('const/combin/I' ('type/canonical/canonical_sum' A)) (('const/canonical/Cons_monom' A) c1 l1 ('const/canonical/Nil_monom' A))) (^[c2 : A, l2 : ('type/list/list' 'type/quote/index'), t2 : ('type/canonical/canonical_sum' A)]: (('const/combin/I' ('type/canonical/canonical_sum' A)) (('const/prelim/compare' ('type/canonical/canonical_sum' A)) (('const/prelim/list_compare' 'type/quote/index' 'type/quote/index') 'const/quote/index_compare' l1 l2) (('const/canonical/Cons_monom' A) c1 l1 (('const/canonical/Cons_monom' A) c2 l2 t2)) (('const/canonical/Cons_monom' A) (('const/semi_ring/semi_ring_SRP' A) sr c1 c2) l1 t2) (('const/canonical/Cons_monom' A) c2 l2 (monom_insert_tupled (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' A ('type/pair/prod' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A)))) sr (('const/pair/,' A ('type/pair/prod' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A))) c1 (('const/pair/,' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A)) l1 t2)))))))) (^['l2\'' : ('type/list/list' 'type/quote/index'), 't2\'' : ('type/canonical/canonical_sum' A)]: (('const/combin/I' ('type/canonical/canonical_sum' A)) (('const/prelim/compare' ('type/canonical/canonical_sum' A)) (('const/prelim/list_compare' 'type/quote/index' 'type/quote/index') 'const/quote/index_compare' l1 'l2\'') (('const/canonical/Cons_monom' A) c1 l1 (('const/canonical/Cons_varlist' A) 'l2\'' 't2\'')) (('const/canonical/Cons_monom' A) (('const/semi_ring/semi_ring_SRP' A) sr c1 (('const/semi_ring/semi_ring_SR1' A) sr)) l1 't2\'') (('const/canonical/Cons_varlist' A) 'l2\'' (monom_insert_tupled (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' A ('type/pair/prod' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A)))) sr (('const/pair/,' A ('type/pair/prod' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A))) c1 (('const/pair/,' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A)) l1 't2\''))))))))))))))))))).
tt('thm/canonical/monom_insert_curried_def_', def, ![A : $t]: (![x : ('type/semi_ring/semi_ring' A), x1 : A, x2 : ('type/list/list' 'type/quote/index'), x3 : ('type/canonical/canonical_sum' A)]: ((('const/canonical/monom_insert' A) x x1 x2 x3) = (('const/canonical/monom_insert_tupled' A) (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' A ('type/pair/prod' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A)))) x (('const/pair/,' A ('type/pair/prod' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A))) x1 (('const/pair/,' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A)) x2 x3))))))).
tt('thm/canonical/monom_insert_ind_', ax, ![A : $t]: (![P : (('type/semi_ring/semi_ring' A) > (A > (('type/list/list' 'type/quote/index') > (('type/canonical/canonical_sum' A) > $o))))]: (((![sr : ('type/semi_ring/semi_ring' A), c1 : A, l1 : ('type/list/list' 'type/quote/index'), c2 : A, l2 : ('type/list/list' 'type/quote/index'), t2 : ('type/canonical/canonical_sum' A)]: ((P sr c1 l1 t2) => (P sr c1 l1 (('const/canonical/Cons_monom' A) c2 l2 t2)))) & ((![sr : ('type/semi_ring/semi_ring' A), c1 : A, l1 : ('type/list/list' 'type/quote/index'), l2 : ('type/list/list' 'type/quote/index'), t2 : ('type/canonical/canonical_sum' A)]: ((P sr c1 l1 t2) => (P sr c1 l1 (('const/canonical/Cons_varlist' A) l2 t2)))) & (![sr : ('type/semi_ring/semi_ring' A), c1 : A, l1 : ('type/list/list' 'type/quote/index')]: (P sr c1 l1 ('const/canonical/Nil_monom' A))))) => (![v : ('type/semi_ring/semi_ring' A), v1 : A, v2 : ('type/list/list' 'type/quote/index'), v3 : ('type/canonical/canonical_sum' A)]: (P v v1 v2 v3))))).
tt('thm/canonical/monom_insert_def_0', ax, ![A : $t]: (![t2 : ('type/canonical/canonical_sum' A), sr : ('type/semi_ring/semi_ring' A), l2 : ('type/list/list' 'type/quote/index'), l1 : ('type/list/list' 'type/quote/index'), c2 : A, c1 : A]: ((('const/canonical/monom_insert' A) sr c1 l1 (('const/canonical/Cons_monom' A) c2 l2 t2)) = (('const/prelim/compare' ('type/canonical/canonical_sum' A)) (('const/prelim/list_compare' 'type/quote/index' 'type/quote/index') 'const/quote/index_compare' l1 l2) (('const/canonical/Cons_monom' A) c1 l1 (('const/canonical/Cons_monom' A) c2 l2 t2)) (('const/canonical/Cons_monom' A) (('const/semi_ring/semi_ring_SRP' A) sr c1 c2) l1 t2) (('const/canonical/Cons_monom' A) c2 l2 (('const/canonical/monom_insert' A) sr c1 l1 t2)))))).
tt('thm/canonical/monom_insert_def_1', ax, ![A : $t]: (![t2 : ('type/canonical/canonical_sum' A), sr : ('type/semi_ring/semi_ring' A), l2 : ('type/list/list' 'type/quote/index'), l1 : ('type/list/list' 'type/quote/index'), c1 : A]: ((('const/canonical/monom_insert' A) sr c1 l1 (('const/canonical/Cons_varlist' A) l2 t2)) = (('const/prelim/compare' ('type/canonical/canonical_sum' A)) (('const/prelim/list_compare' 'type/quote/index' 'type/quote/index') 'const/quote/index_compare' l1 l2) (('const/canonical/Cons_monom' A) c1 l1 (('const/canonical/Cons_varlist' A) l2 t2)) (('const/canonical/Cons_monom' A) (('const/semi_ring/semi_ring_SRP' A) sr c1 (('const/semi_ring/semi_ring_SR1' A) sr)) l1 t2) (('const/canonical/Cons_varlist' A) l2 (('const/canonical/monom_insert' A) sr c1 l1 t2)))))).
tt('thm/canonical/monom_insert_def_e2', ax, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A), l1 : ('type/list/list' 'type/quote/index'), c1 : A]: ((('const/canonical/monom_insert' A) sr c1 l1 ('const/canonical/Nil_monom' A)) = (('const/canonical/Cons_monom' A) c1 l1 ('const/canonical/Nil_monom' A))))).
tt('thm/canonical/varlist_insert_tupled_primitive_def_', def, ![A : $t]: (('const/canonical/varlist_insert_tupled' A) = (('const/relation/WFREC' ('type/pair/prod' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A))) ('type/canonical/canonical_sum' A)) (('const/min/@' (('type/pair/prod' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A))) > (('type/pair/prod' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A))) > $o))) (^[R : (('type/pair/prod' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A))) > (('type/pair/prod' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A))) > $o))]: ((('const/relation/WF' ('type/pair/prod' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A)))) R) & ((![l2 : ('type/list/list' 'type/quote/index'), c2 : A, t2 : ('type/canonical/canonical_sum' A), l1 : ('type/list/list' 'type/quote/index'), sr : ('type/semi_ring/semi_ring' A)]: (R (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A))) sr (('const/pair/,' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A)) l1 t2)) (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A))) sr (('const/pair/,' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A)) l1 (('const/canonical/Cons_monom' A) c2 l2 t2))))) & (![l2 : ('type/list/list' 'type/quote/index'), t2 : ('type/canonical/canonical_sum' A), l1 : ('type/list/list' 'type/quote/index'), sr : ('type/semi_ring/semi_ring' A)]: (R (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A))) sr (('const/pair/,' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A)) l1 t2)) (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A))) sr (('const/pair/,' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A)) l1 (('const/canonical/Cons_varlist' A) l2 t2))))))))) (^[varlist_insert_tupled : (('type/pair/prod' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A))) > ('type/canonical/canonical_sum' A)), a : ('type/pair/prod' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A)))]: (('const/pair/pair_CASE' ('type/canonical/canonical_sum' A) ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A))) a (^[sr : ('type/semi_ring/semi_ring' A), v1 : ('type/pair/prod' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A))]: (('const/pair/pair_CASE' ('type/canonical/canonical_sum' A) ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A)) v1 (^[l1 : ('type/list/list' 'type/quote/index'), v3 : ('type/canonical/canonical_sum' A)]: (('const/canonical/canonical_sum_CASE' A ('type/canonical/canonical_sum' A)) v3 (('const/combin/I' ('type/canonical/canonical_sum' A)) (('const/canonical/Cons_varlist' A) l1 ('const/canonical/Nil_monom' A))) (^[c2 : A, l2 : ('type/list/list' 'type/quote/index'), t2 : ('type/canonical/canonical_sum' A)]: (('const/combin/I' ('type/canonical/canonical_sum' A)) (('const/prelim/compare' ('type/canonical/canonical_sum' A)) (('const/prelim/list_compare' 'type/quote/index' 'type/quote/index') 'const/quote/index_compare' l1 l2) (('const/canonical/Cons_varlist' A) l1 (('const/canonical/Cons_monom' A) c2 l2 t2)) (('const/canonical/Cons_monom' A) (('const/semi_ring/semi_ring_SRP' A) sr (('const/semi_ring/semi_ring_SR1' A) sr) c2) l1 t2) (('const/canonical/Cons_monom' A) c2 l2 (varlist_insert_tupled (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A))) sr (('const/pair/,' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A)) l1 t2))))))) (^['l2\'' : ('type/list/list' 'type/quote/index'), 't2\'' : ('type/canonical/canonical_sum' A)]: (('const/combin/I' ('type/canonical/canonical_sum' A)) (('const/prelim/compare' ('type/canonical/canonical_sum' A)) (('const/prelim/list_compare' 'type/quote/index' 'type/quote/index') 'const/quote/index_compare' l1 'l2\'') (('const/canonical/Cons_varlist' A) l1 (('const/canonical/Cons_varlist' A) 'l2\'' 't2\'')) (('const/canonical/Cons_monom' A) (('const/semi_ring/semi_ring_SRP' A) sr (('const/semi_ring/semi_ring_SR1' A) sr) (('const/semi_ring/semi_ring_SR1' A) sr)) l1 't2\'') (('const/canonical/Cons_varlist' A) 'l2\'' (varlist_insert_tupled (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A))) sr (('const/pair/,' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A)) l1 't2\'')))))))))))))))).
tt('thm/canonical/varlist_insert_curried_def_', def, ![A : $t]: (![x : ('type/semi_ring/semi_ring' A), x1 : ('type/list/list' 'type/quote/index'), x2 : ('type/canonical/canonical_sum' A)]: ((('const/canonical/varlist_insert' A) x x1 x2) = (('const/canonical/varlist_insert_tupled' A) (('const/pair/,' ('type/semi_ring/semi_ring' A) ('type/pair/prod' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A))) x (('const/pair/,' ('type/list/list' 'type/quote/index') ('type/canonical/canonical_sum' A)) x1 x2)))))).
tt('thm/canonical/varlist_insert_ind_', ax, ![A : $t]: (![P : (('type/semi_ring/semi_ring' A) > (('type/list/list' 'type/quote/index') > (('type/canonical/canonical_sum' A) > $o)))]: (((![sr : ('type/semi_ring/semi_ring' A), l1 : ('type/list/list' 'type/quote/index'), c2 : A, l2 : ('type/list/list' 'type/quote/index'), t2 : ('type/canonical/canonical_sum' A)]: ((P sr l1 t2) => (P sr l1 (('const/canonical/Cons_monom' A) c2 l2 t2)))) & ((![sr : ('type/semi_ring/semi_ring' A), l1 : ('type/list/list' 'type/quote/index'), l2 : ('type/list/list' 'type/quote/index'), t2 : ('type/canonical/canonical_sum' A)]: ((P sr l1 t2) => (P sr l1 (('const/canonical/Cons_varlist' A) l2 t2)))) & (![sr : ('type/semi_ring/semi_ring' A), l1 : ('type/list/list' 'type/quote/index')]: (P sr l1 ('const/canonical/Nil_monom' A))))) => (![v : ('type/semi_ring/semi_ring' A), v1 : ('type/list/list' 'type/quote/index'), v2 : ('type/canonical/canonical_sum' A)]: (P v v1 v2))))).
tt('thm/canonical/varlist_insert_def_0', ax, ![A : $t]: (![t2 : ('type/canonical/canonical_sum' A), sr : ('type/semi_ring/semi_ring' A), l2 : ('type/list/list' 'type/quote/index'), l1 : ('type/list/list' 'type/quote/index'), c2 : A]: ((('const/canonical/varlist_insert' A) sr l1 (('const/canonical/Cons_monom' A) c2 l2 t2)) = (('const/prelim/compare' ('type/canonical/canonical_sum' A)) (('const/prelim/list_compare' 'type/quote/index' 'type/quote/index') 'const/quote/index_compare' l1 l2) (('const/canonical/Cons_varlist' A) l1 (('const/canonical/Cons_monom' A) c2 l2 t2)) (('const/canonical/Cons_monom' A) (('const/semi_ring/semi_ring_SRP' A) sr (('const/semi_ring/semi_ring_SR1' A) sr) c2) l1 t2) (('const/canonical/Cons_monom' A) c2 l2 (('const/canonical/varlist_insert' A) sr l1 t2)))))).
tt('thm/canonical/varlist_insert_def_1', ax, ![A : $t]: (![t2 : ('type/canonical/canonical_sum' A), sr : ('type/semi_ring/semi_ring' A), l2 : ('type/list/list' 'type/quote/index'), l1 : ('type/list/list' 'type/quote/index')]: ((('const/canonical/varlist_insert' A) sr l1 (('const/canonical/Cons_varlist' A) l2 t2)) = (('const/prelim/compare' ('type/canonical/canonical_sum' A)) (('const/prelim/list_compare' 'type/quote/index' 'type/quote/index') 'const/quote/index_compare' l1 l2) (('const/canonical/Cons_varlist' A) l1 (('const/canonical/Cons_varlist' A) l2 t2)) (('const/canonical/Cons_monom' A) (('const/semi_ring/semi_ring_SRP' A) sr (('const/semi_ring/semi_ring_SR1' A) sr) (('const/semi_ring/semi_ring_SR1' A) sr)) l1 t2) (('const/canonical/Cons_varlist' A) l2 (('const/canonical/varlist_insert' A) sr l1 t2)))))).
tt('thm/canonical/varlist_insert_def_e2', ax, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A), l1 : ('type/list/list' 'type/quote/index')]: ((('const/canonical/varlist_insert' A) sr l1 ('const/canonical/Nil_monom' A)) = (('const/canonical/Cons_varlist' A) l1 ('const/canonical/Nil_monom' A))))).
tt('thm/canonical/canonical_sum_scalar_def_0', def, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A), c0 : A, c : A, l : ('type/list/list' 'type/quote/index'), t : ('type/canonical/canonical_sum' A)]: ((('const/canonical/canonical_sum_scalar' A) sr c0 (('const/canonical/Cons_monom' A) c l t)) = (('const/canonical/Cons_monom' A) (('const/semi_ring/semi_ring_SRM' A) sr c0 c) l (('const/canonical/canonical_sum_scalar' A) sr c0 t))))).
tt('thm/canonical/canonical_sum_scalar_def_1', def, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A), c0 : A, l : ('type/list/list' 'type/quote/index'), t : ('type/canonical/canonical_sum' A)]: ((('const/canonical/canonical_sum_scalar' A) sr c0 (('const/canonical/Cons_varlist' A) l t)) = (('const/canonical/Cons_monom' A) c0 l (('const/canonical/canonical_sum_scalar' A) sr c0 t))))).
tt('thm/canonical/canonical_sum_scalar_def_e2', def, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A), c0 : A]: ((('const/canonical/canonical_sum_scalar' A) sr c0 ('const/canonical/Nil_monom' A)) = ('const/canonical/Nil_monom' A)))).
tt('thm/canonical/canonical_sum_scalar2_def_0', def, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A), l0 : ('type/list/list' 'type/quote/index'), c : A, l : ('type/list/list' 'type/quote/index'), t : ('type/canonical/canonical_sum' A)]: ((('const/canonical/canonical_sum_scalar2' A) sr l0 (('const/canonical/Cons_monom' A) c l t)) = (('const/canonical/monom_insert' A) sr c (('const/prelim/list_merge' 'type/quote/index') 'const/quote/index_lt' l0 l) (('const/canonical/canonical_sum_scalar2' A) sr l0 t))))).
tt('thm/canonical/canonical_sum_scalar2_def_1', def, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A), l0 : ('type/list/list' 'type/quote/index'), l : ('type/list/list' 'type/quote/index'), t : ('type/canonical/canonical_sum' A)]: ((('const/canonical/canonical_sum_scalar2' A) sr l0 (('const/canonical/Cons_varlist' A) l t)) = (('const/canonical/varlist_insert' A) sr (('const/prelim/list_merge' 'type/quote/index') 'const/quote/index_lt' l0 l) (('const/canonical/canonical_sum_scalar2' A) sr l0 t))))).
tt('thm/canonical/canonical_sum_scalar2_def_e2', def, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A), l0 : ('type/list/list' 'type/quote/index')]: ((('const/canonical/canonical_sum_scalar2' A) sr l0 ('const/canonical/Nil_monom' A)) = ('const/canonical/Nil_monom' A)))).
tt('thm/canonical/canonical_sum_scalar3_def_0', def, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A), c0 : A, l0 : ('type/list/list' 'type/quote/index'), c : A, l : ('type/list/list' 'type/quote/index'), t : ('type/canonical/canonical_sum' A)]: ((('const/canonical/canonical_sum_scalar3' A) sr c0 l0 (('const/canonical/Cons_monom' A) c l t)) = (('const/canonical/monom_insert' A) sr (('const/semi_ring/semi_ring_SRM' A) sr c0 c) (('const/prelim/list_merge' 'type/quote/index') 'const/quote/index_lt' l0 l) (('const/canonical/canonical_sum_scalar3' A) sr c0 l0 t))))).
tt('thm/canonical/canonical_sum_scalar3_def_1', def, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A), c0 : A, l0 : ('type/list/list' 'type/quote/index'), l : ('type/list/list' 'type/quote/index'), t : ('type/canonical/canonical_sum' A)]: ((('const/canonical/canonical_sum_scalar3' A) sr c0 l0 (('const/canonical/Cons_varlist' A) l t)) = (('const/canonical/monom_insert' A) sr c0 (('const/prelim/list_merge' 'type/quote/index') 'const/quote/index_lt' l0 l) (('const/canonical/canonical_sum_scalar3' A) sr c0 l0 t))))).
tt('thm/canonical/canonical_sum_scalar3_def_e2', def, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A), c0 : A, l0 : ('type/list/list' 'type/quote/index')]: ((('const/canonical/canonical_sum_scalar3' A) sr c0 l0 ('const/canonical/Nil_monom' A)) = ('const/canonical/Nil_monom' A)))).
tt('thm/canonical/canonical_sum_prod_def_0', def, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A), c1 : A, l1 : ('type/list/list' 'type/quote/index'), t1 : ('type/canonical/canonical_sum' A), s2 : ('type/canonical/canonical_sum' A)]: ((('const/canonical/canonical_sum_prod' A) sr (('const/canonical/Cons_monom' A) c1 l1 t1) s2) = (('const/canonical/canonical_sum_merge' A) sr (('const/canonical/canonical_sum_scalar3' A) sr c1 l1 s2) (('const/canonical/canonical_sum_prod' A) sr t1 s2))))).
tt('thm/canonical/canonical_sum_prod_def_1', def, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A), l1 : ('type/list/list' 'type/quote/index'), t1 : ('type/canonical/canonical_sum' A), s2 : ('type/canonical/canonical_sum' A)]: ((('const/canonical/canonical_sum_prod' A) sr (('const/canonical/Cons_varlist' A) l1 t1) s2) = (('const/canonical/canonical_sum_merge' A) sr (('const/canonical/canonical_sum_scalar2' A) sr l1 s2) (('const/canonical/canonical_sum_prod' A) sr t1 s2))))).
tt('thm/canonical/canonical_sum_prod_def_e2', def, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A), s2 : ('type/canonical/canonical_sum' A)]: ((('const/canonical/canonical_sum_prod' A) sr ('const/canonical/Nil_monom' A) s2) = ('const/canonical/Nil_monom' A)))).
tt('thm/canonical/canonical_sum_simplify_def_0', def, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A), c : A, l : ('type/list/list' 'type/quote/index'), t : ('type/canonical/canonical_sum' A)]: ((('const/canonical/canonical_sum_simplify' A) sr (('const/canonical/Cons_monom' A) c l t)) = (('const/bool/COND' ('type/canonical/canonical_sum' A)) (c = (('const/semi_ring/semi_ring_SR0' A) sr)) (('const/canonical/canonical_sum_simplify' A) sr t) (('const/bool/COND' ('type/canonical/canonical_sum' A)) (c = (('const/semi_ring/semi_ring_SR1' A) sr)) (('const/canonical/Cons_varlist' A) l (('const/canonical/canonical_sum_simplify' A) sr t)) (('const/canonical/Cons_monom' A) c l (('const/canonical/canonical_sum_simplify' A) sr t))))))).
tt('thm/canonical/canonical_sum_simplify_def_1', def, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A), l : ('type/list/list' 'type/quote/index'), t : ('type/canonical/canonical_sum' A)]: ((('const/canonical/canonical_sum_simplify' A) sr (('const/canonical/Cons_varlist' A) l t)) = (('const/canonical/Cons_varlist' A) l (('const/canonical/canonical_sum_simplify' A) sr t))))).
tt('thm/canonical/canonical_sum_simplify_def_e2', def, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A)]: ((('const/canonical/canonical_sum_simplify' A) sr ('const/canonical/Nil_monom' A)) = ('const/canonical/Nil_monom' A)))).
tt('thm/canonical/ivl_aux_def_0', def, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A), vm : ('type/quote/varmap' A), x : 'type/quote/index']: ((('const/canonical/ivl_aux' A) sr vm x ('const/list/NIL' 'type/quote/index')) = (('const/quote/varmap_find' A) x vm)))).
tt('thm/canonical/ivl_aux_def_e1', def, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A), vm : ('type/quote/varmap' A), x : 'type/quote/index', 'x\'' : 'type/quote/index', 't\'' : ('type/list/list' 'type/quote/index')]: ((('const/canonical/ivl_aux' A) sr vm x (('const/list/CONS' 'type/quote/index') 'x\'' 't\'')) = (('const/semi_ring/semi_ring_SRM' A) sr (('const/quote/varmap_find' A) x vm) (('const/canonical/ivl_aux' A) sr vm 'x\'' 't\''))))).
tt('thm/canonical/interp_vl_def_0', def, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A), vm : ('type/quote/varmap' A)]: ((('const/canonical/interp_vl' A) sr vm ('const/list/NIL' 'type/quote/index')) = (('const/semi_ring/semi_ring_SR1' A) sr)))).
tt('thm/canonical/interp_vl_def_e1', def, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A), vm : ('type/quote/varmap' A), x : 'type/quote/index', t : ('type/list/list' 'type/quote/index')]: ((('const/canonical/interp_vl' A) sr vm (('const/list/CONS' 'type/quote/index') x t)) = (('const/canonical/ivl_aux' A) sr vm x t)))).
tt('thm/canonical/interp_m_def_0', def, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A), vm : ('type/quote/varmap' A), c : A]: ((('const/canonical/interp_m' A) sr vm c ('const/list/NIL' 'type/quote/index')) = c))).
tt('thm/canonical/interp_m_def_e1', def, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A), vm : ('type/quote/varmap' A), c : A, x : 'type/quote/index', t : ('type/list/list' 'type/quote/index')]: ((('const/canonical/interp_m' A) sr vm c (('const/list/CONS' 'type/quote/index') x t)) = (('const/semi_ring/semi_ring_SRM' A) sr c (('const/canonical/ivl_aux' A) sr vm x t))))).
tt('thm/canonical/ics_aux_def_0', def, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A), vm : ('type/quote/varmap' A), a : A]: ((('const/canonical/ics_aux' A) sr vm a ('const/canonical/Nil_monom' A)) = a))).
tt('thm/canonical/ics_aux_def_1', def, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A), vm : ('type/quote/varmap' A), a : A, l : ('type/list/list' 'type/quote/index'), t : ('type/canonical/canonical_sum' A)]: ((('const/canonical/ics_aux' A) sr vm a (('const/canonical/Cons_varlist' A) l t)) = (('const/semi_ring/semi_ring_SRP' A) sr a (('const/canonical/ics_aux' A) sr vm (('const/canonical/interp_vl' A) sr vm l) t))))).
tt('thm/canonical/ics_aux_def_e2', def, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A), vm : ('type/quote/varmap' A), a : A, c : A, l : ('type/list/list' 'type/quote/index'), t : ('type/canonical/canonical_sum' A)]: ((('const/canonical/ics_aux' A) sr vm a (('const/canonical/Cons_monom' A) c l t)) = (('const/semi_ring/semi_ring_SRP' A) sr a (('const/canonical/ics_aux' A) sr vm (('const/canonical/interp_m' A) sr vm c l) t))))).
tt('thm/canonical/interp_cs_def_0', def, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A), vm : ('type/quote/varmap' A)]: ((('const/canonical/interp_cs' A) sr vm ('const/canonical/Nil_monom' A)) = (('const/semi_ring/semi_ring_SR0' A) sr)))).
tt('thm/canonical/interp_cs_def_1', def, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A), vm : ('type/quote/varmap' A), l : ('type/list/list' 'type/quote/index'), t : ('type/canonical/canonical_sum' A)]: ((('const/canonical/interp_cs' A) sr vm (('const/canonical/Cons_varlist' A) l t)) = (('const/canonical/ics_aux' A) sr vm (('const/canonical/interp_vl' A) sr vm l) t)))).
tt('thm/canonical/interp_cs_def_e2', def, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A), vm : ('type/quote/varmap' A), c : A, l : ('type/list/list' 'type/quote/index'), t : ('type/canonical/canonical_sum' A)]: ((('const/canonical/interp_cs' A) sr vm (('const/canonical/Cons_monom' A) c l t)) = (('const/canonical/ics_aux' A) sr vm (('const/canonical/interp_m' A) sr vm c l) t)))).
tt('thm/canonical/ivl_aux_ok_', ax, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A)]: ((('const/semi_ring/is_semi_ring' A) sr) => (![vm : ('type/quote/varmap' A), v : ('type/list/list' 'type/quote/index'), i : 'type/quote/index']: ((('const/canonical/ivl_aux' A) sr vm i v) = (('const/semi_ring/semi_ring_SRM' A) sr (('const/quote/varmap_find' A) i vm) (('const/canonical/interp_vl' A) sr vm v))))))).
tt('thm/canonical/varlist_merge_ok_', ax, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A)]: ((('const/semi_ring/is_semi_ring' A) sr) => (![vm : ('type/quote/varmap' A), x : ('type/list/list' 'type/quote/index'), y : ('type/list/list' 'type/quote/index')]: ((('const/canonical/interp_vl' A) sr vm (('const/prelim/list_merge' 'type/quote/index') 'const/quote/index_lt' x y)) = (('const/semi_ring/semi_ring_SRM' A) sr (('const/canonical/interp_vl' A) sr vm x) (('const/canonical/interp_vl' A) sr vm y))))))).
tt('thm/canonical/ics_aux_ok_', ax, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A)]: ((('const/semi_ring/is_semi_ring' A) sr) => (![vm : ('type/quote/varmap' A), x : A, s : ('type/canonical/canonical_sum' A)]: ((('const/canonical/ics_aux' A) sr vm x s) = (('const/semi_ring/semi_ring_SRP' A) sr x (('const/canonical/interp_cs' A) sr vm s))))))).
tt('thm/canonical/interp_m_ok_', ax, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A)]: ((('const/semi_ring/is_semi_ring' A) sr) => (![vm : ('type/quote/varmap' A), x : A, l : ('type/list/list' 'type/quote/index')]: ((('const/canonical/interp_m' A) sr vm x l) = (('const/semi_ring/semi_ring_SRM' A) sr x (('const/canonical/interp_vl' A) sr vm l))))))).
tt('thm/canonical/canonical_sum_merge_ok_', ax, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A)]: ((('const/semi_ring/is_semi_ring' A) sr) => (![vm : ('type/quote/varmap' A), x : ('type/canonical/canonical_sum' A), y : ('type/canonical/canonical_sum' A)]: ((('const/canonical/interp_cs' A) sr vm (('const/canonical/canonical_sum_merge' A) sr x y)) = (('const/semi_ring/semi_ring_SRP' A) sr (('const/canonical/interp_cs' A) sr vm x) (('const/canonical/interp_cs' A) sr vm y))))))).
tt('thm/canonical/monom_insert_ok_', ax, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A)]: ((('const/semi_ring/is_semi_ring' A) sr) => (![vm : ('type/quote/varmap' A), a : A, l : ('type/list/list' 'type/quote/index'), s : ('type/canonical/canonical_sum' A)]: ((('const/canonical/interp_cs' A) sr vm (('const/canonical/monom_insert' A) sr a l s)) = (('const/semi_ring/semi_ring_SRP' A) sr (('const/semi_ring/semi_ring_SRM' A) sr a (('const/canonical/interp_vl' A) sr vm l)) (('const/canonical/interp_cs' A) sr vm s))))))).
tt('thm/canonical/varlist_insert_ok_', ax, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A)]: ((('const/semi_ring/is_semi_ring' A) sr) => (![vm : ('type/quote/varmap' A), l : ('type/list/list' 'type/quote/index'), s : ('type/canonical/canonical_sum' A)]: ((('const/canonical/interp_cs' A) sr vm (('const/canonical/varlist_insert' A) sr l s)) = (('const/semi_ring/semi_ring_SRP' A) sr (('const/canonical/interp_vl' A) sr vm l) (('const/canonical/interp_cs' A) sr vm s))))))).
tt('thm/canonical/canonical_sum_scalar_ok_', ax, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A)]: ((('const/semi_ring/is_semi_ring' A) sr) => (![vm : ('type/quote/varmap' A), a : A, s : ('type/canonical/canonical_sum' A)]: ((('const/canonical/interp_cs' A) sr vm (('const/canonical/canonical_sum_scalar' A) sr a s)) = (('const/semi_ring/semi_ring_SRM' A) sr a (('const/canonical/interp_cs' A) sr vm s))))))).
tt('thm/canonical/canonical_sum_scalar2_ok_', ax, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A)]: ((('const/semi_ring/is_semi_ring' A) sr) => (![vm : ('type/quote/varmap' A), l : ('type/list/list' 'type/quote/index'), s : ('type/canonical/canonical_sum' A)]: ((('const/canonical/interp_cs' A) sr vm (('const/canonical/canonical_sum_scalar2' A) sr l s)) = (('const/semi_ring/semi_ring_SRM' A) sr (('const/canonical/interp_vl' A) sr vm l) (('const/canonical/interp_cs' A) sr vm s))))))).
tt('thm/canonical/canonical_sum_scalar3_ok_', ax, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A)]: ((('const/semi_ring/is_semi_ring' A) sr) => (![vm : ('type/quote/varmap' A), c : A, l : ('type/list/list' 'type/quote/index'), s : ('type/canonical/canonical_sum' A)]: ((('const/canonical/interp_cs' A) sr vm (('const/canonical/canonical_sum_scalar3' A) sr c l s)) = (('const/semi_ring/semi_ring_SRM' A) sr (('const/semi_ring/semi_ring_SRM' A) sr c (('const/canonical/interp_vl' A) sr vm l)) (('const/canonical/interp_cs' A) sr vm s))))))).
tt('thm/canonical/canonical_sum_prod_ok_', ax, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A)]: ((('const/semi_ring/is_semi_ring' A) sr) => (![vm : ('type/quote/varmap' A), x : ('type/canonical/canonical_sum' A), y : ('type/canonical/canonical_sum' A)]: ((('const/canonical/interp_cs' A) sr vm (('const/canonical/canonical_sum_prod' A) sr x y)) = (('const/semi_ring/semi_ring_SRM' A) sr (('const/canonical/interp_cs' A) sr vm x) (('const/canonical/interp_cs' A) sr vm y))))))).
tt('thm/canonical/canonical_sum_simplify_ok_', ax, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A)]: ((('const/semi_ring/is_semi_ring' A) sr) => (![vm : ('type/quote/varmap' A), s : ('type/canonical/canonical_sum' A)]: ((('const/canonical/interp_cs' A) sr vm (('const/canonical/canonical_sum_simplify' A) sr s)) = (('const/canonical/interp_cs' A) sr vm s)))))).
tt('thm/canonical/spolynom_TY_DEF_', def, ![A : $t]: (?[rep : (('type/canonical/spolynom' A) > ('type/ind_type/recspace' ('type/pair/prod' 'type/quote/index' A)))]: (('const/bool/TYPE_DEFINITION' ('type/ind_type/recspace' ('type/pair/prod' 'type/quote/index' A)) ('type/canonical/spolynom' A)) (^['a0\'' : ('type/ind_type/recspace' ('type/pair/prod' 'type/quote/index' A))]: (!['\'spolynom\'' : (('type/ind_type/recspace' ('type/pair/prod' 'type/quote/index' A)) > $o)]: ((!['a0\'0' : ('type/ind_type/recspace' ('type/pair/prod' 'type/quote/index' A))]: (((?[a : 'type/quote/index']: ('a0\'0' = ((^[a0 : 'type/quote/index']: (('const/ind_type/CONSTR' ('type/pair/prod' 'type/quote/index' A)) 'const/num/0' (('const/pair/,' 'type/quote/index' A) a0 ('const/bool/ARB' A)) (^[n : 'type/num/num']: ('const/ind_type/BOTTOM' ('type/pair/prod' 'type/quote/index' A))))) a))) | ((?[a : A]: ('a0\'0' = ((^[a0 : A]: (('const/ind_type/CONSTR' ('type/pair/prod' 'type/quote/index' A)) ('const/num/SUC' 'const/num/0') (('const/pair/,' 'type/quote/index' A) ('const/bool/ARB' 'type/quote/index') a0) (^[n : 'type/num/num']: ('const/ind_type/BOTTOM' ('type/pair/prod' 'type/quote/index' A))))) a))) | ((?[a0 : ('type/ind_type/recspace' ('type/pair/prod' 'type/quote/index' A)), a1 : ('type/ind_type/recspace' ('type/pair/prod' 'type/quote/index' A))]: (('a0\'0' = ((^[a00 : ('type/ind_type/recspace' ('type/pair/prod' 'type/quote/index' A)), a10 : ('type/ind_type/recspace' ('type/pair/prod' 'type/quote/index' A))]: (('const/ind_type/CONSTR' ('type/pair/prod' 'type/quote/index' A)) ('const/num/SUC' ('const/num/SUC' 'const/num/0')) (('const/pair/,' 'type/quote/index' A) ('const/bool/ARB' 'type/quote/index') ('const/bool/ARB' A)) (('const/ind_type/FCONS' ('type/ind_type/recspace' ('type/pair/prod' 'type/quote/index' A))) a00 (('const/ind_type/FCONS' ('type/ind_type/recspace' ('type/pair/prod' 'type/quote/index' A))) a10 (^[n : 'type/num/num']: ('const/ind_type/BOTTOM' ('type/pair/prod' 'type/quote/index' A))))))) a0 a1)) & (('\'spolynom\'' a0) & ('\'spolynom\'' a1)))) | (?[a0 : ('type/ind_type/recspace' ('type/pair/prod' 'type/quote/index' A)), a1 : ('type/ind_type/recspace' ('type/pair/prod' 'type/quote/index' A))]: (('a0\'0' = ((^[a00 : ('type/ind_type/recspace' ('type/pair/prod' 'type/quote/index' A)), a10 : ('type/ind_type/recspace' ('type/pair/prod' 'type/quote/index' A))]: (('const/ind_type/CONSTR' ('type/pair/prod' 'type/quote/index' A)) ('const/num/SUC' ('const/num/SUC' ('const/num/SUC' 'const/num/0'))) (('const/pair/,' 'type/quote/index' A) ('const/bool/ARB' 'type/quote/index') ('const/bool/ARB' A)) (('const/ind_type/FCONS' ('type/ind_type/recspace' ('type/pair/prod' 'type/quote/index' A))) a00 (('const/ind_type/FCONS' ('type/ind_type/recspace' ('type/pair/prod' 'type/quote/index' A))) a10 (^[n : 'type/num/num']: ('const/ind_type/BOTTOM' ('type/pair/prod' 'type/quote/index' A))))))) a0 a1)) & (('\'spolynom\'' a0) & ('\'spolynom\'' a1))))))) => ('\'spolynom\'' 'a0\'0'))) => ('\'spolynom\'' 'a0\'')))) rep))).
tt('thm/canonical/spolynom_case_def_0', def, ![B : $t, A : $t]: (![a : 'type/quote/index', f : ('type/quote/index' > B), f1 : (A > B), f2 : (('type/canonical/spolynom' A) > (('type/canonical/spolynom' A) > B)), f3 : (('type/canonical/spolynom' A) > (('type/canonical/spolynom' A) > B))]: ((('const/canonical/spolynom_CASE' A B) (('const/canonical/SPvar' A) a) f f1 f2 f3) = (f a)))).
tt('thm/canonical/spolynom_case_def_1', def, ![A : $t, B : $t]: (![a : A, f : ('type/quote/index' > B), f1 : (A > B), f2 : (('type/canonical/spolynom' A) > (('type/canonical/spolynom' A) > B)), f3 : (('type/canonical/spolynom' A) > (('type/canonical/spolynom' A) > B))]: ((('const/canonical/spolynom_CASE' A B) (('const/canonical/SPconst' A) a) f f1 f2 f3) = (f1 a)))).
tt('thm/canonical/spolynom_case_def_2', def, ![A : $t, B : $t]: (![a0 : ('type/canonical/spolynom' A), a1 : ('type/canonical/spolynom' A), f : ('type/quote/index' > B), f1 : (A > B), f2 : (('type/canonical/spolynom' A) > (('type/canonical/spolynom' A) > B)), f3 : (('type/canonical/spolynom' A) > (('type/canonical/spolynom' A) > B))]: ((('const/canonical/spolynom_CASE' A B) (('const/canonical/SPplus' A) a0 a1) f f1 f2 f3) = (f2 a0 a1)))).
tt('thm/canonical/spolynom_case_def_e3', def, ![A : $t, B : $t]: (![a0 : ('type/canonical/spolynom' A), a1 : ('type/canonical/spolynom' A), f : ('type/quote/index' > B), f1 : (A > B), f2 : (('type/canonical/spolynom' A) > (('type/canonical/spolynom' A) > B)), f3 : (('type/canonical/spolynom' A) > (('type/canonical/spolynom' A) > B))]: ((('const/canonical/spolynom_CASE' A B) (('const/canonical/SPmult' A) a0 a1) f f1 f2 f3) = (f3 a0 a1)))).
tt('thm/canonical/spolynom_size_def_0', def, ![A : $t]: (![f : (A > 'type/num/num'), a : 'type/quote/index']: ((('const/canonical/spolynom_size' A) f (('const/canonical/SPvar' A) a)) = ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) ('const/quote/index_size' a))))).
tt('thm/canonical/spolynom_size_def_1', def, ![A : $t]: (![f : (A > 'type/num/num'), a : A]: ((('const/canonical/spolynom_size' A) f (('const/canonical/SPconst' A) a)) = ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) (f a))))).
tt('thm/canonical/spolynom_size_def_2', def, ![A : $t]: (![f : (A > 'type/num/num'), a0 : ('type/canonical/spolynom' A), a1 : ('type/canonical/spolynom' A)]: ((('const/canonical/spolynom_size' A) f (('const/canonical/SPplus' A) a0 a1)) = ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) ('const/arithmetic/+' (('const/canonical/spolynom_size' A) f a0) (('const/canonical/spolynom_size' A) f a1)))))).
tt('thm/canonical/spolynom_size_def_e3', def, ![A : $t]: (![f : (A > 'type/num/num'), a0 : ('type/canonical/spolynom' A), a1 : ('type/canonical/spolynom' A)]: ((('const/canonical/spolynom_size' A) f (('const/canonical/SPmult' A) a0 a1)) = ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) ('const/arithmetic/+' (('const/canonical/spolynom_size' A) f a0) (('const/canonical/spolynom_size' A) f a1)))))).
tt('thm/canonical/datatype_spolynom_', ax, ![A : $t]: (![spolynom : (('type/quote/index' > ('type/canonical/spolynom' A)) > ((A > ('type/canonical/spolynom' A)) > ((('type/canonical/spolynom' A) > (('type/canonical/spolynom' A) > ('type/canonical/spolynom' A))) > ((('type/canonical/spolynom' A) > (('type/canonical/spolynom' A) > ('type/canonical/spolynom' A))) > $o))))]: (('const/bool/DATATYPE' $o) (spolynom ('const/canonical/SPvar' A) ('const/canonical/SPconst' A) ('const/canonical/SPplus' A) ('const/canonical/SPmult' A))))).
tt('thm/canonical/spolynom_11_0', ax, ![A : $t]: (![a : 'type/quote/index', 'a\'' : 'type/quote/index']: (((('const/canonical/SPvar' A) a) = (('const/canonical/SPvar' A) 'a\'')) = (a = 'a\'')))).
tt('thm/canonical/spolynom_11_1', ax, ![A : $t]: (![a : A, 'a\'' : A]: (((('const/canonical/SPconst' A) a) = (('const/canonical/SPconst' A) 'a\'')) = (a = 'a\'')))).
tt('thm/canonical/spolynom_11_2', ax, ![A : $t]: (![a0 : ('type/canonical/spolynom' A), a1 : ('type/canonical/spolynom' A), 'a0\'' : ('type/canonical/spolynom' A), 'a1\'' : ('type/canonical/spolynom' A)]: (((('const/canonical/SPplus' A) a0 a1) = (('const/canonical/SPplus' A) 'a0\'' 'a1\'')) = ((a0 = 'a0\'') & (a1 = 'a1\''))))).
tt('thm/canonical/spolynom_11_e3', ax, ![A : $t]: (![a0 : ('type/canonical/spolynom' A), a1 : ('type/canonical/spolynom' A), 'a0\'' : ('type/canonical/spolynom' A), 'a1\'' : ('type/canonical/spolynom' A)]: (((('const/canonical/SPmult' A) a0 a1) = (('const/canonical/SPmult' A) 'a0\'' 'a1\'')) = ((a0 = 'a0\'') & (a1 = 'a1\''))))).
tt('thm/canonical/spolynom_distinct_0', ax, ![A : $t]: (!['a\'' : A, a : 'type/quote/index']: (~ ((('const/canonical/SPvar' A) a) = (('const/canonical/SPconst' A) 'a\''))))).
tt('thm/canonical/spolynom_distinct_1', ax, ![A : $t]: (![a1 : ('type/canonical/spolynom' A), a0 : ('type/canonical/spolynom' A), a : 'type/quote/index']: (~ ((('const/canonical/SPvar' A) a) = (('const/canonical/SPplus' A) a0 a1))))).
tt('thm/canonical/spolynom_distinct_2', ax, ![A : $t]: (![a1 : ('type/canonical/spolynom' A), a0 : ('type/canonical/spolynom' A), a : 'type/quote/index']: (~ ((('const/canonical/SPvar' A) a) = (('const/canonical/SPmult' A) a0 a1))))).
tt('thm/canonical/spolynom_distinct_3', ax, ![A : $t]: (![a1 : ('type/canonical/spolynom' A), a0 : ('type/canonical/spolynom' A), a : A]: (~ ((('const/canonical/SPconst' A) a) = (('const/canonical/SPplus' A) a0 a1))))).
tt('thm/canonical/spolynom_distinct_4', ax, ![A : $t]: (![a1 : ('type/canonical/spolynom' A), a0 : ('type/canonical/spolynom' A), a : A]: (~ ((('const/canonical/SPconst' A) a) = (('const/canonical/SPmult' A) a0 a1))))).
tt('thm/canonical/spolynom_distinct_e5', ax, ![A : $t]: (!['a1\'' : ('type/canonical/spolynom' A), a1 : ('type/canonical/spolynom' A), 'a0\'' : ('type/canonical/spolynom' A), a0 : ('type/canonical/spolynom' A)]: (~ ((('const/canonical/SPplus' A) a0 a1) = (('const/canonical/SPmult' A) 'a0\'' 'a1\''))))).
tt('thm/canonical/spolynom_case_cong_', ax, ![A : $t, B : $t]: (!['f3\'' : (('type/canonical/spolynom' A) > (('type/canonical/spolynom' A) > B)), 'f2\'' : (('type/canonical/spolynom' A) > (('type/canonical/spolynom' A) > B)), 'f1\'' : (A > B), 'f\'' : ('type/quote/index' > B), M : ('type/canonical/spolynom' A), 'M\'' : ('type/canonical/spolynom' A), f : ('type/quote/index' > B), f1 : (A > B), f2 : (('type/canonical/spolynom' A) > (('type/canonical/spolynom' A) > B)), f3 : (('type/canonical/spolynom' A) > (('type/canonical/spolynom' A) > B))]: (((M = 'M\'') & ((![a : 'type/quote/index']: (('M\'' = (('const/canonical/SPvar' A) a)) => ((f a) = ('f\'' a)))) & ((![a : A]: (('M\'' = (('const/canonical/SPconst' A) a)) => ((f1 a) = ('f1\'' a)))) & ((![a0 : ('type/canonical/spolynom' A), a1 : ('type/canonical/spolynom' A)]: (('M\'' = (('const/canonical/SPplus' A) a0 a1)) => ((f2 a0 a1) = ('f2\'' a0 a1)))) & (![a0 : ('type/canonical/spolynom' A), a1 : ('type/canonical/spolynom' A)]: (('M\'' = (('const/canonical/SPmult' A) a0 a1)) => ((f3 a0 a1) = ('f3\'' a0 a1)))))))) => ((('const/canonical/spolynom_CASE' A B) M f f1 f2 f3) = (('const/canonical/spolynom_CASE' A B) 'M\'' 'f\'' 'f1\'' 'f2\'' 'f3\''))))).
tt('thm/canonical/spolynom_nchotomy_', ax, ![A : $t]: (![ss : ('type/canonical/spolynom' A)]: ((?[i : 'type/quote/index']: (ss = (('const/canonical/SPvar' A) i))) | ((?[a : A]: (ss = (('const/canonical/SPconst' A) a))) | ((?[s : ('type/canonical/spolynom' A), s0 : ('type/canonical/spolynom' A)]: (ss = (('const/canonical/SPplus' A) s s0))) | (?[s : ('type/canonical/spolynom' A), s0 : ('type/canonical/spolynom' A)]: (ss = (('const/canonical/SPmult' A) s s0)))))))).
tt('thm/canonical/spolynom_Axiom_', ax, ![A : $t, B : $t]: (![f0 : ('type/quote/index' > B), f1 : (A > B), f2 : (('type/canonical/spolynom' A) > (('type/canonical/spolynom' A) > (B > (B > B)))), f3 : (('type/canonical/spolynom' A) > (('type/canonical/spolynom' A) > (B > (B > B))))]: (?[fn : (('type/canonical/spolynom' A) > B)]: ((![a : 'type/quote/index']: ((fn (('const/canonical/SPvar' A) a)) = (f0 a))) & ((![a : A]: ((fn (('const/canonical/SPconst' A) a)) = (f1 a))) & ((![a0 : ('type/canonical/spolynom' A), a1 : ('type/canonical/spolynom' A)]: ((fn (('const/canonical/SPplus' A) a0 a1)) = (f2 a0 a1 (fn a0) (fn a1)))) & (![a0 : ('type/canonical/spolynom' A), a1 : ('type/canonical/spolynom' A)]: ((fn (('const/canonical/SPmult' A) a0 a1)) = (f3 a0 a1 (fn a0) (fn a1)))))))))).
tt('thm/canonical/spolynom_induction_', ax, ![A : $t]: (![P : (('type/canonical/spolynom' A) > $o)]: (((![i : 'type/quote/index']: (P (('const/canonical/SPvar' A) i))) & ((![a : A]: (P (('const/canonical/SPconst' A) a))) & ((![s : ('type/canonical/spolynom' A), s0 : ('type/canonical/spolynom' A)]: (((P s) & (P s0)) => (P (('const/canonical/SPplus' A) s s0)))) & (![s : ('type/canonical/spolynom' A), s0 : ('type/canonical/spolynom' A)]: (((P s) & (P s0)) => (P (('const/canonical/SPmult' A) s s0))))))) => (![s : ('type/canonical/spolynom' A)]: (P s))))).
tt('thm/canonical/spolynom_normalize_def_0', def, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A), i : 'type/quote/index']: ((('const/canonical/spolynom_normalize' A) sr (('const/canonical/SPvar' A) i)) = (('const/canonical/Cons_varlist' A) (('const/list/CONS' 'type/quote/index') i ('const/list/NIL' 'type/quote/index')) ('const/canonical/Nil_monom' A))))).
tt('thm/canonical/spolynom_normalize_def_1', def, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A), c : A]: ((('const/canonical/spolynom_normalize' A) sr (('const/canonical/SPconst' A) c)) = (('const/canonical/Cons_monom' A) c ('const/list/NIL' 'type/quote/index') ('const/canonical/Nil_monom' A))))).
tt('thm/canonical/spolynom_normalize_def_2', def, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A), l : ('type/canonical/spolynom' A), r : ('type/canonical/spolynom' A)]: ((('const/canonical/spolynom_normalize' A) sr (('const/canonical/SPplus' A) l r)) = (('const/canonical/canonical_sum_merge' A) sr (('const/canonical/spolynom_normalize' A) sr l) (('const/canonical/spolynom_normalize' A) sr r))))).
tt('thm/canonical/spolynom_normalize_def_e3', def, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A), l : ('type/canonical/spolynom' A), r : ('type/canonical/spolynom' A)]: ((('const/canonical/spolynom_normalize' A) sr (('const/canonical/SPmult' A) l r)) = (('const/canonical/canonical_sum_prod' A) sr (('const/canonical/spolynom_normalize' A) sr l) (('const/canonical/spolynom_normalize' A) sr r))))).
tt('thm/canonical/spolynom_simplify_def_', def, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A), x : ('type/canonical/spolynom' A)]: ((('const/canonical/spolynom_simplify' A) sr x) = (('const/canonical/canonical_sum_simplify' A) sr (('const/canonical/spolynom_normalize' A) sr x))))).
tt('thm/canonical/interp_sp_def_0', def, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A), vm : ('type/quote/varmap' A), c : A]: ((('const/canonical/interp_sp' A) sr vm (('const/canonical/SPconst' A) c)) = c))).
tt('thm/canonical/interp_sp_def_1', def, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A), vm : ('type/quote/varmap' A), i : 'type/quote/index']: ((('const/canonical/interp_sp' A) sr vm (('const/canonical/SPvar' A) i)) = (('const/quote/varmap_find' A) i vm)))).
tt('thm/canonical/interp_sp_def_2', def, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A), vm : ('type/quote/varmap' A), p1 : ('type/canonical/spolynom' A), p2 : ('type/canonical/spolynom' A)]: ((('const/canonical/interp_sp' A) sr vm (('const/canonical/SPplus' A) p1 p2)) = (('const/semi_ring/semi_ring_SRP' A) sr (('const/canonical/interp_sp' A) sr vm p1) (('const/canonical/interp_sp' A) sr vm p2))))).
tt('thm/canonical/interp_sp_def_e3', def, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A), vm : ('type/quote/varmap' A), p1 : ('type/canonical/spolynom' A), p2 : ('type/canonical/spolynom' A)]: ((('const/canonical/interp_sp' A) sr vm (('const/canonical/SPmult' A) p1 p2)) = (('const/semi_ring/semi_ring_SRM' A) sr (('const/canonical/interp_sp' A) sr vm p1) (('const/canonical/interp_sp' A) sr vm p2))))).
tt('thm/canonical/spolynomial_normalize_ok_', ax, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A)]: ((('const/semi_ring/is_semi_ring' A) sr) => (![vm : ('type/quote/varmap' A), p : ('type/canonical/spolynom' A)]: ((('const/canonical/interp_cs' A) sr vm (('const/canonical/spolynom_normalize' A) sr p)) = (('const/canonical/interp_sp' A) sr vm p)))))).
tt('thm/canonical/spolynomial_simplify_ok_', ax, ![A : $t]: (![sr : ('type/semi_ring/semi_ring' A)]: ((('const/semi_ring/is_semi_ring' A) sr) => (![vm : ('type/quote/varmap' A), p : ('type/canonical/spolynom' A)]: ((('const/canonical/interp_cs' A) sr vm (('const/canonical/spolynom_simplify' A) sr p)) = (('const/canonical/interp_sp' A) sr vm p)))))).
