:: CATALAN1  semantic presentation begin  
theorem :: CATALAN1:1 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Num 1))) "holds"  (Bool (Set (Set (Var "n"))  ($#k7_nat_d :::"-'"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 3)))) ; 
 
theorem :: CATALAN1:2 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool (Set (Set (Var "n"))  ($#k7_nat_d :::"-'"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 2)))) ; 
 
theorem :: CATALAN1:3 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Num 1))) "holds"  (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1)))) ; 
 
theorem :: CATALAN1:4 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Num 1))) "holds"  (Bool (Set (Set  "(" (Set (Var "n"))  ($#k7_nat_d :::"-'"::: )  (Num 2) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k7_nat_d :::"-'"::: )  (Num 1)))) ; 
 
theorem :: CATALAN1:5 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Num 1))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Num 4)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_xxreal_0 :::">"::: )  (Num 1))) ; 
 
theorem :: CATALAN1:6 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Num 1))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 2) ")" )  ($#k9_newton :::"!"::: )  ")" )  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k4_nat_1 :::"*"::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k9_newton :::"!"::: )  ))) ; 
 
theorem :: CATALAN1:7 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds" (Bool (Set (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Num 2)  ($#k9_real_1 :::"-"::: )  (Set  "(" (Num 3)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Num 4))) ; 
 begin  definitionlet "n" be   ($#m1_hidden :::"Nat":::); func  :::"Catalan"::: "n" ->   ($#m1_subset_1 :::"Real":::) equals :: CATALAN1:def 1 (Set (Set  "(" (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  "n" ")" )  ($#k7_nat_d :::"-'"::: )  (Num 2) ")" )  ($#k6_newton :::"choose"::: )  (Set  "(" "n"  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  "n"); end; 





:: deftheorem    defines :::"Catalan"::: CATALAN1:def 1 :  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k1_catalan1 :::"Catalan"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 2) ")" )  ($#k6_newton :::"choose"::: )  (Set  "(" (Set (Var "n"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set (Var "n"))))); 
 
theorem :: CATALAN1:8 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Num 1))) "holds"  (Bool (Set   ($#k1_catalan1 :::"Catalan"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 2) ")" )  ($#k9_newton :::"!"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "n"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" )  ($#k9_newton :::"!"::: )  ")" )  ($#k4_nat_1 :::"*"::: )  (Set  "(" (Set (Var "n"))  ($#k9_newton :::"!"::: )  ")" ) ")" )))) ; 
 
theorem :: CATALAN1:9 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Num 1))) "holds"  (Bool (Set   ($#k1_catalan1 :::"Catalan"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 4)  ($#k4_nat_1 :::"*"::: )  (Set  "(" (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 3) ")" )  ($#k6_newton :::"choose"::: )  (Set  "(" (Set (Var "n"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" )  ($#k6_newton :::"choose"::: )  (Set  "(" (Set (Var "n"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")" )))) ; 
 
theorem :: CATALAN1:10 (Bool (Set   ($#k1_catalan1 :::"Catalan"::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) ; 
 
theorem :: CATALAN1:11 (Bool (Set   ($#k1_catalan1 :::"Catalan"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Num 1)) ; 
 
theorem :: CATALAN1:12 (Bool (Set   ($#k1_catalan1 :::"Catalan"::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Num 1)) ; 
 
theorem :: CATALAN1:13 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k1_catalan1 :::"Catalan"::: )  (Set (Var "n"))) "is"   ($#m1_hidden :::"Integer":::))) ; 
 
theorem :: CATALAN1:14 (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k1_catalan1 :::"Catalan"::: )  (Set  "(" (Set (Var "k"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "k")) ")" )  ($#k9_newton :::"!"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set (Var "k"))  ($#k9_newton :::"!"::: )  ")" )  ($#k4_nat_1 :::"*"::: )  (Set  "(" (Set  "(" (Set (Var "k"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" )  ($#k9_newton :::"!"::: )  ")" ) ")" )))) ; 
 
theorem :: CATALAN1:15 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Num 1))) "holds"  (Bool (Set   ($#k1_catalan1 :::"Catalan"::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_catalan1 :::"Catalan"::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" )))) ; 
 
theorem :: CATALAN1:16 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k1_catalan1 :::"Catalan"::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_catalan1 :::"Catalan"::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" )))) ; 
 
theorem :: CATALAN1:17 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k1_catalan1 :::"Catalan"::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: CATALAN1:18 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k1_catalan1 :::"Catalan"::: )  (Set (Var "n"))) "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ))) ; 
 
theorem :: CATALAN1:19 (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   ($#k1_catalan1 :::"Catalan"::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Num 2)  ($#k9_real_1 :::"-"::: )  (Set  "(" (Num 3)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k1_catalan1 :::"Catalan"::: )  (Set (Var "n")) ")" )))) ; 
 registrationlet "n" be   ($#m1_hidden :::"Nat":::); 
cluster (Set   ($#k1_catalan1 :::"Catalan"::: )  "n") ->   ($#v7_ordinal1 :::"natural"::: )   ; 
end; 
theorem :: CATALAN1:20 (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   ($#k1_catalan1 :::"Catalan"::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 registrationlet "n" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Nat":::); 
cluster (Set   ($#k1_catalan1 :::"Catalan"::: )  "n") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; 
theorem :: CATALAN1:21 (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   ($#k1_catalan1 :::"Catalan"::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Num 4)  ($#k4_nat_1 :::"*"::: )  (Set  "("  ($#k1_catalan1 :::"Catalan"::: )  (Set (Var "n")) ")" )))) ;