:: CATALAN2  semantic presentation begin  





























definitionlet "p", "q" be   ($#m1_hidden :::"XFinSequence":::) "of" ; :: original: :::"^"::: redefine func "p" :::"^"::: "q" ->   ($#m1_hidden :::"XFinSequence":::) "of" ; end; 
theorem :: CATALAN2:1 (Bool  "for" (Set (Var "D")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "pd")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"  (Bool  "ex" (Set (Var "qd")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"  "st" (Bool (Set (Var "pd"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "pd"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "n")) ")" )  ($#k1_ordinal4 :::"^"::: )  (Set (Var "qd")))))))) ; 
 definitionlet "p" be   ($#m1_hidden :::"XFinSequence":::) "of" ; attr "p" is  :::"dominated_by_0":::  means :: CATALAN2:def 1 (Bool  "("  (Bool (Set   ($#k2_relset_1 :::"rng"::: )  "p")  ($#r1_tarski :::"c="::: )  (Set  ($#k7_domain_1 :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) )) & (Bool  "("   "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  "p"))) "holds"  (Bool (Set (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set  "("  ($#k7_afinsq_2 :::"Sum"::: )  (Set  "(" "p"  ($#k5_relat_1 :::"|"::: )  (Set (Var "k")) ")" ) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k")))  ")" )  ")" ); end; 




:: deftheorem    defines :::"dominated_by_0"::: CATALAN2:def 1 :  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"  "holds"   (Bool  "("  (Bool (Set (Var "p")) "is"   ($#v1_catalan2 :::"dominated_by_0"::: )  ) "iff" (Bool  "("  (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "p")))  ($#r1_tarski :::"c="::: )  (Set  ($#k7_domain_1 :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) )) & (Bool  "("   "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "p"))))) "holds"  (Bool (Set (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set  "("  ($#k7_afinsq_2 :::"Sum"::: )  (Set  "(" (Set (Var "p"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "k")) ")" ) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k")))  ")" )  ")" )  ")" )); 
 
theorem :: CATALAN2:2 (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"   "st" (Bool (Bool (Set (Var "p")) "is"   ($#v1_catalan2 :::"dominated_by_0"::: )  )) "holds"  (Bool (Set (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set  "("  ($#k7_afinsq_2 :::"Sum"::: )  (Set  "(" (Set (Var "p"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "k")) ")" ) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))))) ; 
 
theorem :: CATALAN2:3 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"   "st" (Bool (Bool (Set (Var "p")) "is"   ($#v1_catalan2 :::"dominated_by_0"::: )  )) "holds"  (Bool (Set (Set (Var "p"))  ($#k1_recdef_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 registrationlet "x" be    ($#m1_hidden :::"set"::: )  ; let "k" be   ($#m1_hidden :::"Nat":::); 
cluster (Set "x"  ($#k2_funcop_1 :::"-->"::: )  "k") -> (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v5_relat_1 :::"-valued"::: )   ; 
end; registration
cluster   ($#v1_xboole_0 :::"empty"::: )     ($#v5_ordinal1 :::"T-Sequence-like"::: )     ($#v1_relat_1 :::"Relation-like"::: )   (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )   (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_VALUED_0() bbbadV2_VALUED_0() bbbadV3_VALUED_0() bbbadV4_VALUED_0()   ($#v1_finset_1 :::"finite"::: )     ($#v4_partfun3 :::"nonnegative-yielding"::: )   bbbadV1_AFINSQ_1()   ($#v1_catalan2 :::"dominated_by_0"::: )    for    ($#m1_hidden :::"set"::: )  ; 

cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v5_ordinal1 :::"T-Sequence-like"::: )     ($#v1_relat_1 :::"Relation-like"::: )   (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )   (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_VALUED_0() bbbadV2_VALUED_0() bbbadV3_VALUED_0() bbbadV4_VALUED_0()   ($#v1_finset_1 :::"finite"::: )     ($#v4_partfun3 :::"nonnegative-yielding"::: )   bbbadV1_AFINSQ_1()   ($#v1_catalan2 :::"dominated_by_0"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; 
theorem :: CATALAN2:4 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "n"))  ($#k8_funcop_1 :::"-->"::: )  (Set  ($#k6_numbers :::"0"::: ) )) "is"   ($#v1_catalan2 :::"dominated_by_0"::: )  )) ; 
 
theorem :: CATALAN2:5 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "m")))) "holds"  (Bool (Set (Set  "(" (Set (Var "n"))  ($#k8_funcop_1 :::"-->"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k1_catalan2 :::"^"::: )  (Set  "(" (Set (Var "m"))  ($#k8_funcop_1 :::"-->"::: )  (Num 1) ")" )) "is"   ($#v1_catalan2 :::"dominated_by_0"::: )  )) ; 
 
theorem :: CATALAN2:6 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"   "st" (Bool (Bool (Set (Var "p")) "is"   ($#v1_catalan2 :::"dominated_by_0"::: )  )) "holds"  (Bool (Set (Set (Var "p"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "n"))) "is"   ($#v1_catalan2 :::"dominated_by_0"::: )  ))) ; 
 
theorem :: CATALAN2:7 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"   "st" (Bool (Bool (Set (Var "p")) "is"   ($#v1_catalan2 :::"dominated_by_0"::: )  ) & (Bool (Set (Var "q")) "is"   ($#v1_catalan2 :::"dominated_by_0"::: )  )) "holds"  (Bool (Set (Set (Var "p"))  ($#k1_catalan2 :::"^"::: )  (Set (Var "q"))) "is"   ($#v1_catalan2 :::"dominated_by_0"::: )  )) ; 
 
theorem :: CATALAN2:8 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"   "st" (Bool (Bool (Set (Var "p")) "is"   ($#v1_catalan2 :::"dominated_by_0"::: )  )) "holds"  (Bool (Set (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set  "("  ($#k7_afinsq_2 :::"Sum"::: )  (Set  "(" (Set (Var "p"))  ($#k5_relat_1 :::"|"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set (Var "n")) ")" )  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ) ")" ) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "(" (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set (Var "n")) ")" )  ($#k23_binop_2 :::"+"::: )  (Num 1))))) ; 
 
theorem :: CATALAN2:9 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"   "st" (Bool (Bool (Set (Var "p")) "is"   ($#v1_catalan2 :::"dominated_by_0"::: )  ) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p")) ")" )  ($#k21_binop_2 :::"-"::: )  (Set  "(" (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set  "("  ($#k7_afinsq_2 :::"Sum"::: )  (Set (Var "p")) ")" ) ")" )))) "holds"  (Bool (Set (Set (Var "p"))  ($#k1_catalan2 :::"^"::: )  (Set  "(" (Set (Var "n"))  ($#k8_funcop_1 :::"-->"::: )  (Num 1) ")" )) "is"   ($#v1_catalan2 :::"dominated_by_0"::: )  ))) ; 
 
theorem :: CATALAN2:10 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"   "st" (Bool (Bool (Set (Var "p")) "is"   ($#v1_catalan2 :::"dominated_by_0"::: )  ) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "k"))  ($#k23_binop_2 :::"+"::: )  (Set  "("  ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p")) ")" ) ")" )  ($#k21_binop_2 :::"-"::: )  (Set  "(" (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set  "("  ($#k7_afinsq_2 :::"Sum"::: )  (Set (Var "p")) ")" ) ")" )))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "k"))  ($#k8_funcop_1 :::"-->"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k1_catalan2 :::"^"::: )  (Set (Var "p")) ")" )  ($#k1_catalan2 :::"^"::: )  (Set  "(" (Set (Var "n"))  ($#k8_funcop_1 :::"-->"::: )  (Num 1) ")" )) "is"   ($#v1_catalan2 :::"dominated_by_0"::: )  ))) ; 
 
theorem :: CATALAN2:11 (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"   "st" (Bool (Bool (Set (Var "p")) "is"   ($#v1_catalan2 :::"dominated_by_0"::: )  ) & (Bool (Set (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set  "("  ($#k7_afinsq_2 :::"Sum"::: )  (Set  "(" (Set (Var "p"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "k")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "k")))) "holds"  (Bool  "("  (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p")))) & (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set  "(" (Set (Var "p"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "k")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "k")))  ")" ))) ; 
 
theorem :: CATALAN2:12 (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"   "st" (Bool (Bool (Set (Var "p")) "is"   ($#v1_catalan2 :::"dominated_by_0"::: )  ) & (Bool (Set (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set  "("  ($#k7_afinsq_2 :::"Sum"::: )  (Set  "(" (Set (Var "p"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "k")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "k"))) & (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "k")) ")" )  ($#k1_catalan2 :::"^"::: )  (Set (Var "q"))))) "holds"  (Bool (Set (Var "q")) "is"   ($#v1_catalan2 :::"dominated_by_0"::: )  ))) ; 
 
theorem :: CATALAN2:13 (Bool  "for" (Set (Var "k")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"   "st" (Bool (Bool (Set (Var "p")) "is"   ($#v1_catalan2 :::"dominated_by_0"::: )  ) & (Bool (Set (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set  "("  ($#k7_afinsq_2 :::"Sum"::: )  (Set  "(" (Set (Var "p"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "k")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "k"))) & (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k23_binop_2 :::"+"::: )  (Num 1)))) "holds"  (Bool (Set (Set (Var "p"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "n")) ")" )  ($#k1_catalan2 :::"^"::: )  (Set  "(" (Num 1)  ($#k8_funcop_1 :::"-->"::: )  (Num 1) ")" ))))) ; 
 
theorem :: CATALAN2:14 (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"   "st" (Bool (Bool (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_nat_1 :::"min*"::: )   "{"  (Set (Var "N")) where N "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool  "("  (Bool (Set (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set  "("  ($#k7_afinsq_2 :::"Sum"::: )  (Set  "(" (Set (Var "p"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "N")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "N"))) & (Bool (Set (Var "N"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  "}"  )) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "p")) "is"   ($#v1_catalan2 :::"dominated_by_0"::: )  )) "holds"  (Bool  "ex" (Set (Var "q")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"  "st"  (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 1)  ($#k8_funcop_1 :::"-->"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k1_catalan2 :::"^"::: )  (Set (Var "q")) ")" )  ($#k1_catalan2 :::"^"::: )  (Set  "(" (Num 1)  ($#k8_funcop_1 :::"-->"::: )  (Num 1) ")" ))) & (Bool (Set (Var "q")) "is"   ($#v1_catalan2 :::"dominated_by_0"::: )  )  ")" )))) ; 
 
theorem :: CATALAN2:15 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"   "st" (Bool (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "p")))  ($#r1_tarski :::"c="::: )  (Set  ($#k7_domain_1 :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) )) & (Bool (Bool  "not" (Set (Var "p")) "is"   ($#v1_catalan2 :::"dominated_by_0"::: )  ))) "holds"  (Bool  "ex" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "st"  (Bool  "("  (Bool (Set (Set  "(" (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set (Var "k")) ")" )  ($#k23_binop_2 :::"+"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set   ($#k5_nat_1 :::"min*"::: )   "{"  (Set (Var "N")) where N "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool (Set (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set  "("  ($#k7_afinsq_2 :::"Sum"::: )  (Set  "(" (Set (Var "p"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "N")) ")" ) ")" ))  ($#r1_xxreal_0 :::">"::: )  (Set (Var "N")))  "}"  )) & (Bool (Set (Set  "(" (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set (Var "k")) ")" )  ($#k23_binop_2 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "p")))) & (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Set   ($#k7_afinsq_2 :::"Sum"::: )  (Set  "(" (Set (Var "p"))  ($#k5_relat_1 :::"|"::: )  (Set  "(" (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set (Var "k")) ")" ) ")" ))) & (Bool (Set (Set (Var "p"))  ($#k1_recdef_1 :::"."::: )  (Set  "(" (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set (Var "k")) ")" ))  ($#r1_hidden :::"="::: )  (Num 1))  ")" ))) ; 
 
theorem :: CATALAN2:16 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"   (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Set (Var "p"))  ($#k5_relat_1 :::"|"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set (Var "k")) ")" )  ($#k23_binop_2 :::"+"::: )  (Set  "("  ($#k1_afinsq_1 :::"len"::: )  (Set (Var "q")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "k"))  ($#k8_funcop_1 :::"-->"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k1_catalan2 :::"^"::: )  (Set (Var "q")) ")" )  ($#k1_catalan2 :::"^"::: )  (Set  "(" (Set (Var "k"))  ($#k8_funcop_1 :::"-->"::: )  (Num 1) ")" ))) & (Bool (Set (Var "q")) "is"   ($#v1_catalan2 :::"dominated_by_0"::: )  ) & (Bool (Set (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set  "("  ($#k7_afinsq_2 :::"Sum"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "q")))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k5_nat_1 :::"min*"::: )   "{"  (Set (Var "N")) where N "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool  "("  (Bool (Set (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set  "("  ($#k7_afinsq_2 :::"Sum"::: )  (Set  "(" (Set (Var "p"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "N")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "N"))) & (Bool (Set (Var "N"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  "}"  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set (Var "k")) ")" )  ($#k23_binop_2 :::"+"::: )  (Set  "("  ($#k1_afinsq_1 :::"len"::: )  (Set (Var "q")) ")" ))))) ; 
 
theorem :: CATALAN2:17 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"   "st" (Bool (Bool (Set (Var "p")) "is"   ($#v1_catalan2 :::"dominated_by_0"::: )  ) & (Bool  "{"  (Set (Var "N")) where N "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool  "("  (Bool (Set (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set  "("  ($#k7_afinsq_2 :::"Sum"::: )  (Set  "(" (Set (Var "p"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "N")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "N"))) & (Bool (Set (Var "N"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  "}"    ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "ex" (Set (Var "q")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"  "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k5_afinsq_1 :::"%>"::: ) )  ($#k1_catalan2 :::"^"::: )  (Set (Var "q")))) & (Bool (Set (Var "q")) "is"   ($#v1_catalan2 :::"dominated_by_0"::: )  )  ")" ))) ; 
 
theorem :: CATALAN2:18 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"   "st" (Bool (Bool (Set (Var "p")) "is"   ($#v1_catalan2 :::"dominated_by_0"::: )  )) "holds"  (Bool  "("  (Bool (Set (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k5_afinsq_1 :::"%>"::: ) )  ($#k1_catalan2 :::"^"::: )  (Set (Var "p"))) "is"   ($#v1_catalan2 :::"dominated_by_0"::: )  ) & (Bool  "{"  (Set (Var "N")) where N "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool  "("  (Bool (Set (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set  "("  ($#k7_afinsq_2 :::"Sum"::: )  (Set  "(" (Set  "(" (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k5_afinsq_1 :::"%>"::: ) )  ($#k1_catalan2 :::"^"::: )  (Set (Var "p")) ")" )  ($#k5_relat_1 :::"|"::: )  (Set (Var "N")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "N"))) & (Bool (Set (Var "N"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  "}"    ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" )) ; 
 
theorem :: CATALAN2:19 (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"   "st" (Bool (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "p")))  ($#r1_tarski :::"c="::: )  (Set  ($#k7_domain_1 :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) )) & (Bool (Set (Set  "(" (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set (Var "k")) ")" )  ($#k23_binop_2 :::"+"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set   ($#k5_nat_1 :::"min*"::: )   "{"  (Set (Var "N")) where N "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool (Set (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set  "("  ($#k7_afinsq_2 :::"Sum"::: )  (Set  "(" (Set (Var "p"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "N")) ")" ) ")" ))  ($#r1_xxreal_0 :::">"::: )  (Set (Var "N")))  "}"  ))) "holds"  (Bool (Set (Set (Var "p"))  ($#k5_relat_1 :::"|"::: )  (Set  "(" (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set (Var "k")) ")" )) "is"   ($#v1_catalan2 :::"dominated_by_0"::: )  ))) ; 
 begin  definitionlet "n", "m" be   ($#m1_hidden :::"Nat":::); func  :::"Domin_0":::  "(" "n" "," "m" ")"  ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set  ($#k7_domain_1 :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) )  ($#k8_afinsq_1 :::"^omega"::: )  ")" ) means :: CATALAN2:def 2 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "ex" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"  "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Var "x"))) & (Bool (Set (Var "p")) "is"   ($#v1_catalan2 :::"dominated_by_0"::: )  ) & (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  "n") & (Bool (Set   ($#k7_afinsq_2 :::"Sum"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  "m")  ")" ))  ")" )); end; 






:: deftheorem    defines :::"Domin_0"::: CATALAN2:def 2 :  (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set  ($#k7_domain_1 :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) )  ($#k8_afinsq_1 :::"^omega"::: )  ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_catalan2 :::"Domin_0"::: )   "(" (Set (Var "n")) "," (Set (Var "m")) ")" )) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b3"))) "iff" (Bool  "ex" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"  "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Var "x"))) & (Bool (Set (Var "p")) "is"   ($#v1_catalan2 :::"dominated_by_0"::: )  ) & (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (Bool (Set   ($#k7_afinsq_2 :::"Sum"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "m")))  ")" ))  ")" ))  ")" ))); 
 
theorem :: CATALAN2:20 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"  "holds"   (Bool  "("  (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_catalan2 :::"Domin_0"::: )   "(" (Set (Var "n")) "," (Set (Var "m")) ")" )) "iff" (Bool  "("  (Bool (Set (Var "p")) "is"   ($#v1_catalan2 :::"dominated_by_0"::: )  ) & (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (Bool (Set   ($#k7_afinsq_2 :::"Sum"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "m")))  ")" )  ")" ))) ; 
 
theorem :: CATALAN2:21 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k2_catalan2 :::"Domin_0"::: )   "(" (Set (Var "n")) "," (Set (Var "m")) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_card_fin :::"Choose"::: )   "(" (Set (Var "n")) "," (Set (Var "m")) "," (Num 1) "," (Set  ($#k6_numbers :::"0"::: ) ) ")" ))) ; 
 registrationlet "n", "m" be   ($#m1_hidden :::"Nat":::); 
cluster (Set   ($#k2_catalan2 :::"Domin_0"::: )   "(" "n" "," "m" ")" ) ->   ($#v1_finset_1 :::"finite"::: )   ; 
end; 
theorem :: CATALAN2:22 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set   ($#k2_catalan2 :::"Domin_0"::: )   "(" (Set (Var "n")) "," (Set (Var "m")) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ) "iff" (Bool (Set (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set (Var "m")))  ($#r1_xxreal_0 :::">"::: )  (Set (Var "n")))  ")" )) ; 
 
theorem :: CATALAN2:23 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k2_catalan2 :::"Domin_0"::: )   "(" (Set (Var "n")) "," (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  "(" (Set (Var "n"))  ($#k8_funcop_1 :::"-->"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) ($#k6_domain_1 :::"}"::: ) ))) ; 
 
theorem :: CATALAN2:24 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k2_catalan2 :::"Domin_0"::: )   "(" (Set (Var "n")) "," (Set  ($#k6_numbers :::"0"::: ) ) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: CATALAN2:25 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"   (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "p")))  ($#r1_tarski :::"c="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n")) ($#k2_tarski :::"}"::: ) ))) "holds"  (Bool  "ex" (Set (Var "q")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"  "st"  (Bool  "("  (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "q")))) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "q")))  ($#r1_tarski :::"c="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n")) ($#k2_tarski :::"}"::: ) )) & (Bool  "("   "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p"))))) "holds"  (Bool (Set (Set  "("  ($#k7_afinsq_2 :::"Sum"::: )  (Set  "(" (Set (Var "p"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "k")) ")" ) ")" )  ($#k8_complex1 :::"+"::: )  (Set  "("  ($#k7_afinsq_2 :::"Sum"::: )  (Set  "(" (Set (Var "q"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "k")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k24_binop_2 :::"*"::: )  (Set (Var "k"))))  ")" ) & (Bool  "("   "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p"))))) "holds"  (Bool (Set (Set (Var "q"))  ($#k1_recdef_1 :::"."::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k21_binop_2 :::"-"::: )  (Set  "(" (Set (Var "p"))  ($#k1_recdef_1 :::"."::: )  (Set (Var "k")) ")" )))  ")" )  ")" )))) ; 
 
theorem :: CATALAN2:26 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set (Var "n"))  ($#k6_newton :::"choose"::: )  (Set (Var "m")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: CATALAN2:27 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set  "(" (Set (Var "m"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "(" (Set  "("  ($#k1_card_fin :::"Choose"::: )   "(" (Set (Var "n")) "," (Set  "(" (Set (Var "m"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ) "," (Num 1) "," (Set  ($#k6_numbers :::"0"::: ) ) ")"  ")" )  ($#k7_subset_1 :::"\"::: )  (Set  "("  ($#k2_catalan2 :::"Domin_0"::: )   "(" (Set (Var "n")) "," (Set  "(" (Set (Var "m"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ) ")"  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k1_card_fin :::"Choose"::: )   "(" (Set (Var "n")) "," (Set (Var "m")) "," (Num 1) "," (Set  ($#k6_numbers :::"0"::: ) ) ")"  ")" )))) ; 
 
theorem :: CATALAN2:28 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set  "(" (Set (Var "m"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k2_catalan2 :::"Domin_0"::: )   "(" (Set (Var "n")) "," (Set  "(" (Set (Var "m"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "n"))  ($#k6_newton :::"choose"::: )  (Set  "(" (Set (Var "m"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k21_binop_2 :::"-"::: )  (Set  "(" (Set (Var "n"))  ($#k6_newton :::"choose"::: )  (Set (Var "m")) ")" )))) ; 
 
theorem :: CATALAN2:29 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set (Var "m")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k2_catalan2 :::"Domin_0"::: )   "(" (Set (Var "n")) "," (Set (Var "m")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "n"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" )  ($#k21_binop_2 :::"-"::: )  (Set  "(" (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set (Var "m")) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "(" (Set  "(" (Set (Var "n"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" )  ($#k21_binop_2 :::"-"::: )  (Set (Var "m")) ")" ) ")" )  ($#k11_binop_2 :::"*"::: )  (Set  "(" (Set (Var "n"))  ($#k6_newton :::"choose"::: )  (Set (Var "m")) ")" )))) ; 
 
theorem :: CATALAN2:30 (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k2_catalan2 :::"Domin_0"::: )   "(" (Set  "(" (Num 2)  ($#k23_binop_2 :::"+"::: )  (Set (Var "k")) ")" ) "," (Num 1) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k23_binop_2 :::"+"::: )  (Num 1)))) ; 
 
theorem :: CATALAN2:31 (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k2_catalan2 :::"Domin_0"::: )   "(" (Set  "(" (Num 4)  ($#k23_binop_2 :::"+"::: )  (Set (Var "k")) ")" ) "," (Num 2) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "k"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" )  ($#k24_binop_2 :::"*"::: )  (Set  "(" (Set (Var "k"))  ($#k23_binop_2 :::"+"::: )  (Num 4) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 2)))) ; 
 
theorem :: CATALAN2:32 (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k2_catalan2 :::"Domin_0"::: )   "(" (Set  "(" (Num 6)  ($#k23_binop_2 :::"+"::: )  (Set (Var "k")) ")" ) "," (Num 3) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "k"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" )  ($#k24_binop_2 :::"*"::: )  (Set  "(" (Set (Var "k"))  ($#k23_binop_2 :::"+"::: )  (Num 5) ")" ) ")" )  ($#k24_binop_2 :::"*"::: )  (Set  "(" (Set (Var "k"))  ($#k23_binop_2 :::"+"::: )  (Num 6) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 6)))) ; 
 
theorem :: CATALAN2:33 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k2_catalan2 :::"Domin_0"::: )   "(" (Set  "(" (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set (Var "n")) ")" ) "," (Set (Var "n")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set (Var "n")) ")" )  ($#k6_newton :::"choose"::: )  (Set (Var "n")) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "(" (Set (Var "n"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" )))) ; 
 
theorem :: CATALAN2:34 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k2_catalan2 :::"Domin_0"::: )   "(" (Set  "(" (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set (Var "n")) ")" ) "," (Set (Var "n")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_catalan1 :::"Catalan"::: )  (Set  "(" (Set (Var "n"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" )))) ; 
 definitionlet "D" be    ($#m1_hidden :::"set"::: )  ; mode  :::"OMEGA":::  "of" "D" ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v4_funct_1 :::"functional"::: )     ($#m1_hidden :::"set"::: )   means :: CATALAN2:def 3 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  it)) "holds"  (Bool (Set (Var "x")) "is"   ($#m1_hidden :::"XFinSequence":::) "of" )); end; 





:: deftheorem    defines :::"OMEGA"::: CATALAN2:def 3 :  (Bool  "for" (Set (Var "D")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b2")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v4_funct_1 :::"functional"::: )     ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b2")) "is"    ($#m1_catalan2 :::"OMEGA"::: )   "of" (Set (Var "D"))) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b2")))) "holds"  (Bool (Set (Var "x")) "is"   ($#m1_hidden :::"XFinSequence":::) "of" ))  ")" ))); 
 definitionlet "D" be    ($#m1_hidden :::"set"::: )  ; :: original: :::"^omega"::: redefine func "D" :::"^omega":::  ->    ($#m1_catalan2 :::"OMEGA"::: )   "of" "D"; end; registrationlet "D" be    ($#m1_hidden :::"set"::: )  ; let "F" be    ($#m1_catalan2 :::"OMEGA"::: )   "of" (Set (Const "D")); 
cluster   ->   ($#v5_ordinal1 :::"T-Sequence-like"::: )   "D"  ($#v5_relat_1 :::"-valued"::: )     ($#v1_finset_1 :::"finite"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" "F"; 
end; 




theorem :: CATALAN2:35 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )   "{"  (Set (Var "pN")) where pN "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Set  ($#k5_numbers :::"NAT"::: ) )  ($#k3_catalan2 :::"^omega"::: )  ) : (Bool  "("  (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "pN")))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set (Var "n")))) & (Bool (Set (Var "pN")) "is"   ($#v1_catalan2 :::"dominated_by_0"::: )  )  ")" )  "}"  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set (Var "n")) ")" )  ($#k6_newton :::"choose"::: )  (Set (Var "n"))))) ; 
 
theorem :: CATALAN2:36 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "k")) "," (Set (Var "j")) "," (Set (Var "l")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "j"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k21_binop_2 :::"-"::: )  (Set  "(" (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set  "(" (Set (Var "k"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ) ")" ))) & (Bool (Set (Var "l"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k21_binop_2 :::"-"::: )  (Set  "(" (Set (Var "k"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" )))) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )   "{"  (Set (Var "pN")) where pN "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Set  ($#k5_numbers :::"NAT"::: ) )  ($#k3_catalan2 :::"^omega"::: )  ) : (Bool  "("  (Bool (Set (Var "pN"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_catalan2 :::"Domin_0"::: )   "(" (Set (Var "n")) "," (Set (Var "m")) ")" )) & (Bool (Set (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set  "(" (Set (Var "k"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_nat_1 :::"min*"::: )   "{"  (Set (Var "N")) where N "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool  "("  (Bool (Set (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set  "("  ($#k7_afinsq_2 :::"Sum"::: )  (Set  "(" (Set (Var "pN"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "N")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "N"))) & (Bool (Set (Var "N"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  "}"  ))  ")" )  "}"  )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k2_catalan2 :::"Domin_0"::: )   "(" (Set  "(" (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set (Var "k")) ")" ) "," (Set (Var "k")) ")"  ")" ) ")" )  ($#k24_binop_2 :::"*"::: )  (Set  "("  ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k2_catalan2 :::"Domin_0"::: )   "(" (Set (Var "j")) "," (Set (Var "l")) ")"  ")" ) ")" )))) ; 
 
theorem :: CATALAN2:37 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set (Var "m")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool  "ex" (Set (Var "CardF")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"  "st"  (Bool  "("  (Bool (Set   ($#k1_card_1 :::"card"::: )   "{"  (Set (Var "pN")) where pN "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Set  ($#k5_numbers :::"NAT"::: ) )  ($#k3_catalan2 :::"^omega"::: )  ) : (Bool  "("  (Bool (Set (Var "pN"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_catalan2 :::"Domin_0"::: )   "(" (Set (Var "n")) "," (Set (Var "m")) ")" )) & (Bool  "{"  (Set (Var "N")) where N "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool  "("  (Bool (Set (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set  "("  ($#k7_afinsq_2 :::"Sum"::: )  (Set  "(" (Set (Var "pN"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "N")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "N"))) & (Bool (Set (Var "N"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  "}"    ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" )  "}"  )  ($#r1_hidden :::"="::: )  (Set   ($#k7_afinsq_2 :::"Sum"::: )  (Set (Var "CardF")))) & (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "CardF")))  ($#r1_hidden :::"="::: )  (Set (Var "m"))) & (Bool  "("   "for" (Set (Var "j")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "m")))) "holds"  (Bool (Set (Set (Var "CardF"))  ($#k1_recdef_1 :::"."::: )  (Set (Var "j")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k2_catalan2 :::"Domin_0"::: )   "(" (Set  "(" (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set (Var "j")) ")" ) "," (Set (Var "j")) ")"  ")" ) ")" )  ($#k24_binop_2 :::"*"::: )  (Set  "("  ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k2_catalan2 :::"Domin_0"::: )   "(" (Set  "(" (Set (Var "n"))  ($#k7_nat_d :::"-'"::: )  (Set  "(" (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set  "(" (Set (Var "j"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ) ")" ) ")" ) "," (Set  "(" (Set (Var "m"))  ($#k7_nat_d :::"-'"::: )  (Set  "(" (Set (Var "j"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ) ")" ) ")"  ")" ) ")" )))  ")" )  ")" ))) ; 
 
theorem :: CATALAN2:38 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k2_catalan2 :::"Domin_0"::: )   "(" (Set  "(" (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set (Var "n")) ")" ) "," (Set (Var "n")) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set (Var "pN")) where pN "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Set  ($#k5_numbers :::"NAT"::: ) )  ($#k3_catalan2 :::"^omega"::: )  ) : (Bool  "("  (Bool (Set (Var "pN"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_catalan2 :::"Domin_0"::: )   "(" (Set  "(" (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set (Var "n")) ")" ) "," (Set (Var "n")) ")" )) & (Bool  "{"  (Set (Var "N")) where N "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool  "("  (Bool (Set (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set  "("  ($#k7_afinsq_2 :::"Sum"::: )  (Set  "(" (Set (Var "pN"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "N")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "N"))) & (Bool (Set (Var "N"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  "}"    ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" )  "}"  )) ; 
 
theorem :: CATALAN2:39 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "ex" (Set (Var "Catal")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"  "st"  (Bool  "("  (Bool (Set   ($#k7_afinsq_2 :::"Sum"::: )  (Set (Var "Catal")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_catalan1 :::"Catalan"::: )  (Set  "(" (Set (Var "n"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ))) & (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "Catal")))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (Bool  "("   "for" (Set (Var "j")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set (Var "Catal"))  ($#k1_recdef_1 :::"."::: )  (Set (Var "j")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_catalan1 :::"Catalan"::: )  (Set  "(" (Set (Var "j"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k11_binop_2 :::"*"::: )  (Set  "("  ($#k1_catalan1 :::"Catalan"::: )  (Set  "(" (Set (Var "n"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "j")) ")" ) ")" )))  ")" )  ")" ))) ; 
 
theorem :: CATALAN2:40 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )   "{"  (Set (Var "pN")) where pN "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Set  ($#k5_numbers :::"NAT"::: ) )  ($#k3_catalan2 :::"^omega"::: )  ) : (Bool  "("  (Bool (Set (Var "pN"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_catalan2 :::"Domin_0"::: )   "(" (Set  "(" (Set (Var "n"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "m")) ")" )) & (Bool  "{"  (Set (Var "N")) where N "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool  "("  (Bool (Set (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set  "("  ($#k7_afinsq_2 :::"Sum"::: )  (Set  "(" (Set (Var "pN"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "N")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "N"))) & (Bool (Set (Var "N"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  "}"    ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" )  "}"  )  ($#r1_hidden :::"="::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k2_catalan2 :::"Domin_0"::: )   "(" (Set (Var "n")) "," (Set (Var "m")) ")"  ")" )))) ; 
 
theorem :: CATALAN2:41 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set (Var "m")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool  "ex" (Set (Var "CardF")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"  "st"  (Bool  "("  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k2_catalan2 :::"Domin_0"::: )   "(" (Set (Var "n")) "," (Set (Var "m")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k7_afinsq_2 :::"Sum"::: )  (Set (Var "CardF")) ")" )  ($#k23_binop_2 :::"+"::: )  (Set  "("  ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k2_catalan2 :::"Domin_0"::: )   "(" (Set  "(" (Set (Var "n"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) "," (Set (Var "m")) ")"  ")" ) ")" ))) & (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "CardF")))  ($#r1_hidden :::"="::: )  (Set (Var "m"))) & (Bool  "("   "for" (Set (Var "j")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "m")))) "holds"  (Bool (Set (Set (Var "CardF"))  ($#k1_recdef_1 :::"."::: )  (Set (Var "j")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k2_catalan2 :::"Domin_0"::: )   "(" (Set  "(" (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set (Var "j")) ")" ) "," (Set (Var "j")) ")"  ")" ) ")" )  ($#k24_binop_2 :::"*"::: )  (Set  "("  ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k2_catalan2 :::"Domin_0"::: )   "(" (Set  "(" (Set (Var "n"))  ($#k7_nat_d :::"-'"::: )  (Set  "(" (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set  "(" (Set (Var "j"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ) ")" ) ")" ) "," (Set  "(" (Set (Var "m"))  ($#k7_nat_d :::"-'"::: )  (Set  "(" (Set (Var "j"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ) ")" ) ")"  ")" ) ")" )))  ")" )  ")" ))) ; 
 
theorem :: CATALAN2:42 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) (Bool  "ex" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"  "st"  (Bool  "("  (Bool (Set   ($#k7_afinsq_2 :::"Sum"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k2_catalan2 :::"Domin_0"::: )   "(" (Set  "(" (Set  "(" (Set  "(" (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set (Var "n")) ")" )  ($#k23_binop_2 :::"+"::: )  (Num 2) ")" )  ($#k23_binop_2 :::"+"::: )  (Set (Var "k")) ")" ) "," (Set  "(" (Set (Var "n"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ) ")"  ")" ))) & (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k23_binop_2 :::"+"::: )  (Num 1))) & (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k")))) "holds"  (Bool (Set (Set (Var "p"))  ($#k1_recdef_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k2_catalan2 :::"Domin_0"::: )   "(" (Set  "(" (Set  "(" (Set  "(" (Num 2)  ($#k24_binop_2 :::"*"::: )  (Set (Var "n")) ")" )  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" )  ($#k23_binop_2 :::"+"::: )  (Set (Var "i")) ")" ) "," (Set (Var "n")) ")"  ")" )))  ")" )  ")" ))) ; 
 begin  















definitionlet "seq1", "seq2" be   ($#m1_subset_1 :::"Real_Sequence":::); func "seq1" :::"(##)"::: "seq2" ->   ($#m1_subset_1 :::"Real_Sequence":::) means :: CATALAN2:def 4 (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) (Bool  "ex" (Set (Var "Fr")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"  "st"  (Bool  "("  (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "Fr")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k23_binop_2 :::"+"::: )  (Num 1))) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "k"))  ($#k23_binop_2 :::"+"::: )  (Num 1)))) "holds"  (Bool (Set (Set (Var "Fr"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" "seq1"  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k11_binop_2 :::"*"::: )  (Set  "(" "seq2"  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "k"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "n")) ")" ) ")" )))  ")" ) & (Bool (Set   ($#k7_afinsq_2 :::"Sum"::: )  (Set (Var "Fr")))  ($#r1_hidden :::"="::: )  (Set it  ($#k1_seq_1 :::"."::: )  (Set (Var "k"))))  ")" ))); commutativity  
(Bool  "for" (Set (Var "b1")) "," (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool  "("   "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) (Bool  "ex" (Set (Var "Fr")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"  "st"  (Bool  "("  (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "Fr")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k23_binop_2 :::"+"::: )  (Num 1))) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "k"))  ($#k23_binop_2 :::"+"::: )  (Num 1)))) "holds"  (Bool (Set (Set (Var "Fr"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "seq1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k11_binop_2 :::"*"::: )  (Set  "(" (Set (Var "seq2"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "k"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "n")) ")" ) ")" )))  ")" ) & (Bool (Set   ($#k7_afinsq_2 :::"Sum"::: )  (Set (Var "Fr")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "k"))))  ")" ))  ")" )) "holds"  (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) (Bool  "ex" (Set (Var "Fr")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"  "st"  (Bool  "("  (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "Fr")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k23_binop_2 :::"+"::: )  (Num 1))) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "k"))  ($#k23_binop_2 :::"+"::: )  (Num 1)))) "holds"  (Bool (Set (Set (Var "Fr"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "seq2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k11_binop_2 :::"*"::: )  (Set  "(" (Set (Var "seq1"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "k"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "n")) ")" ) ")" )))  ")" ) & (Bool (Set   ($#k7_afinsq_2 :::"Sum"::: )  (Set (Var "Fr")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "k"))))  ")" ))))
 ; end; 






:: deftheorem    defines :::"(##)"::: CATALAN2:def 4 :  (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "," (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "seq1"))  ($#k4_catalan2 :::"(##)"::: )  (Set (Var "seq2")))) "iff" (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) (Bool  "ex" (Set (Var "Fr")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"  "st"  (Bool  "("  (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "Fr")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k23_binop_2 :::"+"::: )  (Num 1))) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "k"))  ($#k23_binop_2 :::"+"::: )  (Num 1)))) "holds"  (Bool (Set (Set (Var "Fr"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "seq1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k11_binop_2 :::"*"::: )  (Set  "(" (Set (Var "seq2"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "k"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "n")) ")" ) ")" )))  ")" ) & (Bool (Set   ($#k7_afinsq_2 :::"Sum"::: )  (Set (Var "Fr")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b3"))  ($#k1_seq_1 :::"."::: )  (Set (Var "k"))))  ")" )))  ")" )); 
 
theorem :: CATALAN2:43 (Bool  "for" (Set (Var "Fr1")) "," (Set (Var "Fr2")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"   "st" (Bool (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "Fr1")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "Fr2")))) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "Fr1"))))) "holds"  (Bool (Set (Set (Var "Fr1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "Fr2"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set  "("  ($#k1_afinsq_1 :::"len"::: )  (Set (Var "Fr1")) ")" )  ($#k7_nat_d :::"-'"::: )  (Set  "(" (Num 1)  ($#k23_binop_2 :::"+"::: )  (Set (Var "n")) ")" ) ")" )))  ")" )) "holds"  (Bool (Set   ($#k7_afinsq_2 :::"Sum"::: )  (Set (Var "Fr1")))  ($#r1_hidden :::"="::: )  (Set   ($#k7_afinsq_2 :::"Sum"::: )  (Set (Var "Fr2"))))) ; 
 
theorem :: CATALAN2:44 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "Fr1")) "," (Set (Var "Fr2")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"   "st" (Bool (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "Fr1")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "Fr2")))) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "Fr1"))))) "holds"  (Bool (Set (Set (Var "Fr1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k11_binop_2 :::"*"::: )  (Set  "(" (Set (Var "Fr2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )))  ")" )) "holds"  (Bool (Set   ($#k7_afinsq_2 :::"Sum"::: )  (Set (Var "Fr1")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k11_binop_2 :::"*"::: )  (Set  "("  ($#k7_afinsq_2 :::"Sum"::: )  (Set (Var "Fr2")) ")" ))))) ; 
 
theorem :: CATALAN2:45 (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "seq1"))  ($#k4_catalan2 :::"(##)"::: )  (Set  "(" (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "seq2")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "seq1"))  ($#k4_catalan2 :::"(##)"::: )  (Set (Var "seq2")) ")" ))))) ; 
 
theorem :: CATALAN2:46 (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "," (Set (Var "seq3")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"  (Bool (Set (Set (Var "seq1"))  ($#k4_catalan2 :::"(##)"::: )  (Set  "(" (Set (Var "seq2"))  ($#k1_series_1 :::"+"::: )  (Set (Var "seq3")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "seq1"))  ($#k4_catalan2 :::"(##)"::: )  (Set (Var "seq2")) ")" )  ($#k1_series_1 :::"+"::: )  (Set  "(" (Set (Var "seq1"))  ($#k4_catalan2 :::"(##)"::: )  (Set (Var "seq3")) ")" )))) ; 
 
theorem :: CATALAN2:47 (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"  (Bool (Set (Set  "(" (Set (Var "seq1"))  ($#k4_catalan2 :::"(##)"::: )  (Set (Var "seq2")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "seq1"))  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k11_binop_2 :::"*"::: )  (Set  "(" (Set (Var "seq2"))  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )))) ; 
 
theorem :: CATALAN2:48 (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) (Bool  "ex" (Set (Var "Fr")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"  "st"  (Bool  "("  (Bool (Set (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set  "(" (Set (Var "seq1"))  ($#k4_catalan2 :::"(##)"::: )  (Set (Var "seq2")) ")" ) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k7_afinsq_2 :::"Sum"::: )  (Set (Var "Fr")))) & (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "Fr")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k23_binop_2 :::"+"::: )  (Num 1))) & (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "n"))  ($#k23_binop_2 :::"+"::: )  (Num 1)))) "holds"  (Bool (Set (Set (Var "Fr"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "seq1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")) ")" )  ($#k11_binop_2 :::"*"::: )  (Set  "(" (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set (Var "seq2")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "i")) ")" ) ")" )))  ")" )  ")" )))) ; 
 
theorem :: CATALAN2:49 (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "seq2")) "is"   ($#v1_series_1 :::"summable"::: )  )) "holds"  (Bool  "ex" (Set (Var "Fr")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"  "st"  (Bool  "("  (Bool (Set (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set  "(" (Set (Var "seq1"))  ($#k4_catalan2 :::"(##)"::: )  (Set (Var "seq2")) ")" ) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k4_series_1 :::"Sum"::: )  (Set (Var "seq2")) ")" )  ($#k11_binop_2 :::"*"::: )  (Set  "(" (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set (Var "seq1")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ) ")" )  ($#k10_binop_2 :::"-"::: )  (Set  "("  ($#k7_afinsq_2 :::"Sum"::: )  (Set (Var "Fr")) ")" ))) & (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "Fr")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k23_binop_2 :::"+"::: )  (Num 1))) & (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "n"))  ($#k23_binop_2 :::"+"::: )  (Num 1)))) "holds"  (Bool (Set (Set (Var "Fr"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "seq1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")) ")" )  ($#k11_binop_2 :::"*"::: )  (Set  "("  ($#k4_series_1 :::"Sum"::: )  (Set  "(" (Set (Var "seq2"))  ($#k10_nat_1 :::"^\"::: )  (Set  "(" (Set  "(" (Set (Var "n"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "i")) ")" )  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ) ")" ) ")" )))  ")" )  ")" )))) ; 
 
theorem :: CATALAN2:50 (Bool  "for" (Set (Var "Fr")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"  (Bool  "ex" (Set (Var "absFr")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"  "st"  (Bool  "("  (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "absFr")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "Fr")))) & (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "("  ($#k7_afinsq_2 :::"Sum"::: )  (Set (Var "Fr")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k7_afinsq_2 :::"Sum"::: )  (Set (Var "absFr")))) & (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "absFr"))))) "holds"  (Bool (Set (Set (Var "absFr"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "Fr"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")) ")" )))  ")" )  ")" ))) ; 
 
theorem :: CATALAN2:51 (Bool  "for" (Set (Var "seq1")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "seq1")) "is"   ($#v1_series_1 :::"summable"::: )  )) "holds"  (Bool  "ex" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r"))) & (Bool  "("   "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "holds" (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "("  ($#k4_series_1 :::"Sum"::: )  (Set  "(" (Set (Var "seq1"))  ($#k10_nat_1 :::"^\"::: )  (Set (Var "k")) ")" ) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))  ")" )  ")" ))) ; 
 
theorem :: CATALAN2:52 (Bool  "for" (Set (Var "seq1")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m"))) & (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "seq1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool (Set (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set (Var "seq1")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set (Var "seq1")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "m")))))) ; 
 
theorem :: CATALAN2:53 (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "seq1")) "is"   ($#v2_series_1 :::"absolutely_summable"::: )  ) & (Bool (Set (Var "seq2")) "is"   ($#v1_series_1 :::"summable"::: )  )) "holds"  (Bool  "("  (Bool (Set (Set (Var "seq1"))  ($#k4_catalan2 :::"(##)"::: )  (Set (Var "seq2"))) "is"   ($#v1_series_1 :::"summable"::: )  ) & (Bool (Set   ($#k4_series_1 :::"Sum"::: )  (Set  "(" (Set (Var "seq1"))  ($#k4_catalan2 :::"(##)"::: )  (Set (Var "seq2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_series_1 :::"Sum"::: )  (Set (Var "seq1")) ")" )  ($#k11_binop_2 :::"*"::: )  (Set  "("  ($#k4_series_1 :::"Sum"::: )  (Set (Var "seq2")) ")" )))  ")" )) ; 
 begin  
theorem :: CATALAN2:54 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   (Bool  "ex" (Set (Var "Catal")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "st"  (Bool  "("  (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "Catal"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_catalan1 :::"Catalan"::: )  (Set  "(" (Set (Var "n"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k11_binop_2 :::"*"::: )  (Set  "(" (Set (Var "r"))  ($#k1_newton :::"|^"::: )  (Set (Var "n")) ")" )))  ")" ) &  "("  (Bool (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set (Var "r")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Num 1)  ($#k13_complex1 :::"/"::: )  (Num 4)))) "implies" (Bool  "("  (Bool (Set (Var "Catal")) "is"   ($#v2_series_1 :::"absolutely_summable"::: )  ) & (Bool (Set   ($#k4_series_1 :::"Sum"::: )  (Set (Var "Catal")))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k9_binop_2 :::"+"::: )  (Set  "(" (Set (Var "r"))  ($#k11_binop_2 :::"*"::: )  (Set  "(" (Set  "("  ($#k4_series_1 :::"Sum"::: )  (Set (Var "Catal")) ")" )  ($#k2_newton :::"|^"::: )  (Num 2) ")" ) ")" ))) & (Bool (Set   ($#k4_series_1 :::"Sum"::: )  (Set (Var "Catal")))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k13_complex1 :::"/"::: )  (Set  "(" (Num 1)  ($#k9_binop_2 :::"+"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k10_binop_2 :::"-"::: )  (Set  "(" (Num 4)  ($#k11_binop_2 :::"*"::: )  (Set (Var "r")) ")" ) ")" ) ")" ) ")" ))) &  "("  (Bool (Bool (Set (Var "r"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool (Set   ($#k4_series_1 :::"Sum"::: )  (Set (Var "Catal")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 1)  ($#k10_binop_2 :::"-"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Num 1)  ($#k10_binop_2 :::"-"::: )  (Set  "(" (Num 4)  ($#k11_binop_2 :::"*"::: )  (Set (Var "r")) ")" ) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "(" (Num 2)  ($#k11_binop_2 :::"*"::: )  (Set (Var "r")) ")" )))  ")"   ")" )  ")"   ")" ))) ;