:: FLANG_1 semantic presentation begin definitionlet "E" be ($#m1_hidden :::"set"::: ) ; let "a", "b" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Const "E")) ($#k3_catalan2 :::"^omega"::: ) ); :: original: :::"^"::: redefine func "a" :::"^"::: "b" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set "E" ($#k3_catalan2 :::"^omega"::: ) ); end; definitionlet "E" be ($#m1_hidden :::"set"::: ) ; :: original: :::"<%>"::: redefine func :::"<%>"::: "E" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set "E" ($#k3_catalan2 :::"^omega"::: ) ); end; definitionlet "E" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "e" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "E")); :: original: :::"<%"::: redefine func :::"<%":::"e":::"%>"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set "E" ($#k3_catalan2 :::"^omega"::: ) ); end; definitionlet "E" be ($#m1_hidden :::"set"::: ) ; let "a" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Const "E")) ($#k3_catalan2 :::"^omega"::: ) ); :: original: :::"{"::: redefine func :::"{":::"a":::"}"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" "E" ($#k3_catalan2 :::"^omega"::: ) ")" ); end; definitionlet "E" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Const "E")) ")" ); let "n" be ($#m1_hidden :::"Nat":::); :: original: :::"."::: redefine func "f" :::"."::: "n" -> ($#m1_subset_1 :::"Subset":::) "of" "E"; end; theorem :: FLANG_1:1 (Bool "for" (Set (Var "n1")) "," (Set (Var "n")) "," (Set (Var "n2")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool "(" (Bool (Set (Var "n1")) ($#r1_xxreal_0 :::">"::: ) (Set (Var "n"))) "or" (Bool (Set (Var "n2")) ($#r1_xxreal_0 :::">"::: ) (Set (Var "n"))) ")" )) "holds" (Bool (Set (Set (Var "n1")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "n2"))) ($#r1_xxreal_0 :::">"::: ) (Set (Var "n")))) ; theorem :: FLANG_1:2 (Bool "for" (Set (Var "n1")) "," (Set (Var "n")) "," (Set (Var "n2")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "n1")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "n2")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "n1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n2")))) ; theorem :: FLANG_1:3 (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Set (Var "n1")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "n2"))) ($#r1_hidden :::"="::: ) (Num 1)) "iff" (Bool "(" (Bool "(" (Bool (Set (Var "n1")) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "n2")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) "or" (Bool "(" (Bool (Set (Var "n1")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "n2")) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) ")" ) ")" )) ; theorem :: FLANG_1:4 (Bool "for" (Set (Var "x")) "," (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k1_flang_1 :::"^"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x")) ($#k5_afinsq_1 :::"%>"::: ) )) "iff" (Bool "(" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x")) ($#k5_afinsq_1 :::"%>"::: ) )) ")" ) "or" (Bool "(" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")))) & (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x")) ($#k5_afinsq_1 :::"%>"::: ) )) ")" ) ")" ) ")" ))) ; theorem :: FLANG_1:5 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"XFinSequence":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_ordinal4 :::"^"::: ) (Set (Var "q"))))) "holds" (Bool "(" (Bool (Set (Var "p")) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) )) & (Bool (Set (Var "q")) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) )) ")" )))) ; theorem :: FLANG_1:6 (Bool "for" (Set (Var "x")) "," (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x")) ($#k5_afinsq_1 :::"%>"::: ) ) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) ; theorem :: FLANG_1:7 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)))) "holds" (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) )(Bool "ex" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "st" (Bool "(" (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Set (Var "c")) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "e")) ($#k5_afinsq_1 :::"%>"::: ) ))) ")" )))))) ; theorem :: FLANG_1:8 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"XFinSequence":::) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "ex" (Set (Var "q")) "being" ($#m1_hidden :::"XFinSequence":::)(Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x")) ($#k5_afinsq_1 :::"%>"::: ) ) ($#k1_ordinal4 :::"^"::: ) (Set (Var "q"))))))) ; theorem :: FLANG_1:9 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)))) "holds" (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) )(Bool "ex" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "st" (Bool "(" (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Set ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "e")) ($#k5_afinsq_1 :::"%>"::: ) ) ($#k1_ordinal4 :::"^"::: ) (Set (Var "c")))) ")" )))))) ; theorem :: FLANG_1:10 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "m"))))) "holds" (Bool "ex" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ) "st" (Bool "(" (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "c1"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "c2"))) ($#r1_hidden :::"="::: ) (Set (Var "m"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Set (Var "c1")) ($#k1_flang_1 :::"^"::: ) (Set (Var "c2")))) ")" ))))) ; theorem :: FLANG_1:11 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ) "st" (Bool (Bool (Set (Set (Var "a")) ($#k1_flang_1 :::"^"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a")))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; begin definitionlet "E" be ($#m1_hidden :::"set"::: ) ; let "A", "B" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Const "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ); func "A" :::"^^"::: "B" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" "E" ($#k3_catalan2 :::"^omega"::: ) ")" ) means :: FLANG_1:def 1 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "E" ($#k3_catalan2 :::"^omega"::: ) ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) "A") & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) "B") & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_flang_1 :::"^"::: ) (Set (Var "b")))) ")" )) ")" )); end; :: deftheorem defines :::"^^"::: FLANG_1:def 1 : (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "b4")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k6_flang_1 :::"^^"::: ) (Set (Var "B")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b4"))) "iff" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_flang_1 :::"^"::: ) (Set (Var "b")))) ")" )) ")" )) ")" ))); theorem :: FLANG_1:12 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k6_flang_1 :::"^^"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "iff" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" ))) ; theorem :: FLANG_1:13 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k6_flang_1 :::"^^"::: ) (Set ($#k4_flang_1 :::"{"::: ) (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool (Set (Set ($#k4_flang_1 :::"{"::: ) (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) ) ($#k6_flang_1 :::"^^"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))) ")" ))) ; theorem :: FLANG_1:14 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k6_flang_1 :::"^^"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k4_flang_1 :::"{"::: ) (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) )) "iff" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k4_flang_1 :::"{"::: ) (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) )) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k4_flang_1 :::"{"::: ) (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) )) ")" ) ")" ))) ; theorem :: FLANG_1:15 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) "holds" (Bool "(" (Bool (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k6_flang_1 :::"^^"::: ) (Set (Var "B")))) "iff" (Bool "(" (Bool (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) ")" ) ")" ))) ; theorem :: FLANG_1:16 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) "st" (Bool (Bool (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k6_flang_1 :::"^^"::: ) (Set (Var "B")))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k6_flang_1 :::"^^"::: ) (Set (Var "A")))) ")" ))) ; theorem :: FLANG_1:17 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "C")) "," (Set (Var "B")) "," (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "D")))) "holds" (Bool (Set (Set (Var "A")) ($#k6_flang_1 :::"^^"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "C")) ($#k6_flang_1 :::"^^"::: ) (Set (Var "D")))))) ; theorem :: FLANG_1:18 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k6_flang_1 :::"^^"::: ) (Set (Var "B")) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "B")) ($#k6_flang_1 :::"^^"::: ) (Set (Var "C")) ")" ))))) ; theorem :: FLANG_1:19 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "B")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "C")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "A")) ($#k6_flang_1 :::"^^"::: ) (Set (Var "B")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "A")) ($#k6_flang_1 :::"^^"::: ) (Set (Var "C")) ")" ))) & (Bool (Set (Set "(" (Set (Var "B")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "C")) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "B")) ($#k6_flang_1 :::"^^"::: ) (Set (Var "A")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "C")) ($#k6_flang_1 :::"^^"::: ) (Set (Var "A")) ")" ))) ")" ))) ; theorem :: FLANG_1:20 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "A")) ($#k6_flang_1 :::"^^"::: ) (Set (Var "B")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "A")) ($#k6_flang_1 :::"^^"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "B")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C")) ")" ))) & (Bool (Set (Set "(" (Set (Var "B")) ($#k6_flang_1 :::"^^"::: ) (Set (Var "A")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "C")) ($#k6_flang_1 :::"^^"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "B")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C")) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set (Var "A")))) ")" ))) ; theorem :: FLANG_1:21 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "A")) ($#k6_flang_1 :::"^^"::: ) (Set (Var "B")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" (Set (Var "A")) ($#k6_flang_1 :::"^^"::: ) (Set (Var "C")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "B")) ($#k7_subset_1 :::"\"::: ) (Set (Var "C")) ")" ))) & (Bool (Set (Set "(" (Set (Var "B")) ($#k6_flang_1 :::"^^"::: ) (Set (Var "A")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" (Set (Var "C")) ($#k6_flang_1 :::"^^"::: ) (Set (Var "A")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "B")) ($#k7_subset_1 :::"\"::: ) (Set (Var "C")) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set (Var "A")))) ")" ))) ; theorem :: FLANG_1:22 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "A")) ($#k6_flang_1 :::"^^"::: ) (Set (Var "B")) ")" ) ($#k5_subset_1 :::"\+\"::: ) (Set "(" (Set (Var "A")) ($#k6_flang_1 :::"^^"::: ) (Set (Var "C")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "B")) ($#k5_subset_1 :::"\+\"::: ) (Set (Var "C")) ")" ))) & (Bool (Set (Set "(" (Set (Var "B")) ($#k6_flang_1 :::"^^"::: ) (Set (Var "A")) ")" ) ($#k5_subset_1 :::"\+\"::: ) (Set "(" (Set (Var "C")) ($#k6_flang_1 :::"^^"::: ) (Set (Var "A")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "B")) ($#k5_subset_1 :::"\+\"::: ) (Set (Var "C")) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set (Var "A")))) ")" ))) ; begin definitionlet "E" be ($#m1_hidden :::"set"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Const "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ); let "n" be ($#m1_hidden :::"Nat":::); func "A" :::"|^"::: "n" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" "E" ($#k3_catalan2 :::"^omega"::: ) ")" ) means :: FLANG_1:def 2 (Bool "ex" (Set (Var "concat")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "(" "E" ($#k3_catalan2 :::"^omega"::: ) ")" ) ")" ) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "concat")) ($#k5_flang_1 :::"."::: ) "n")) & (Bool (Set (Set (Var "concat")) ($#k5_flang_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_flang_1 :::"{"::: ) (Set "(" ($#k2_flang_1 :::"<%>"::: ) "E" ")" ) ($#k4_flang_1 :::"}"::: ) )) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "concat")) ($#k5_flang_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "concat")) ($#k5_flang_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k6_flang_1 :::"^^"::: ) "A")) ")" ) ")" )); end; :: deftheorem defines :::"|^"::: FLANG_1:def 2 : (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "n")))) "iff" (Bool "ex" (Set (Var "concat")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) ")" ) "st" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "concat")) ($#k5_flang_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Set (Var "concat")) ($#k5_flang_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_flang_1 :::"{"::: ) (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) )) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "concat")) ($#k5_flang_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "concat")) ($#k5_flang_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set (Var "A")))) ")" ) ")" )) ")" ))))); theorem :: FLANG_1:23 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "n")) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set (Var "A"))))))) ; theorem :: FLANG_1:24 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) "holds" (Bool (Set (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_flang_1 :::"{"::: ) (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) )))) ; theorem :: FLANG_1:25 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) "holds" (Bool (Set (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "A"))))) ; theorem :: FLANG_1:26 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) "holds" (Bool (Set (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k6_flang_1 :::"^^"::: ) (Set (Var "A")))))) ; theorem :: FLANG_1:27 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "iff" (Bool "(" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" )))) ; theorem :: FLANG_1:28 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set ($#k4_flang_1 :::"{"::: ) (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) ) ($#k7_flang_1 :::"|^"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k4_flang_1 :::"{"::: ) (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) )))) ; theorem :: FLANG_1:29 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k4_flang_1 :::"{"::: ) (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) )) "iff" (Bool "(" (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k4_flang_1 :::"{"::: ) (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) )) ")" ) ")" )))) ; theorem :: FLANG_1:30 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "n"))))))) ; theorem :: FLANG_1:31 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "n")))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set (Var "A")))))) ; theorem :: FLANG_1:32 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "n")) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "n")) ")" )))))) ; theorem :: FLANG_1:33 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set "(" (Set (Var "m")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "m")) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "n")) ")" )))))) ; theorem :: FLANG_1:34 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "m")) ")" ) ($#k7_flang_1 :::"|^"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set "(" (Set (Var "m")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "n")) ")" )))))) ; theorem :: FLANG_1:35 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "n"))))))) ; theorem :: FLANG_1:36 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::">"::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "m"))))))) ; theorem :: FLANG_1:37 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "n"))))))) ; theorem :: FLANG_1:38 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "n")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "B")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "n")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" ) ($#k7_flang_1 :::"|^"::: ) (Set (Var "n"))))))) ; theorem :: FLANG_1:39 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B")) ")" ) ($#k7_flang_1 :::"|^"::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "n")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "B")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "n")) ")" )))))) ; theorem :: FLANG_1:40 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "C")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "m")))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "C")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set (Var "a")) ($#k1_flang_1 :::"^"::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "C")) ($#k7_flang_1 :::"|^"::: ) (Set "(" (Set (Var "m")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "n")) ")" ))))))) ; begin definitionlet "E" be ($#m1_hidden :::"set"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Const "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ); func "A" :::"*"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" "E" ($#k3_catalan2 :::"^omega"::: ) ")" ) equals :: FLANG_1:def 3 (Set ($#k3_tarski :::"union"::: ) "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" "E" ($#k3_catalan2 :::"^omega"::: ) ")" ) : (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set "A" ($#k7_flang_1 :::"|^"::: ) (Set (Var "n"))))) "}" ); end; :: deftheorem defines :::"*"::: FLANG_1:def 3 : (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) "holds" (Bool (Set (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) : (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "n"))))) "}" )))); theorem :: FLANG_1:41 (Bool "for" (Set (Var "E")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) )) "iff" (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "n"))))) ")" ))) ; theorem :: FLANG_1:42 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ))))) ; theorem :: FLANG_1:43 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) "holds" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) )))) ; theorem :: FLANG_1:44 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) "holds" (Bool (Set (Set (Var "A")) ($#k6_flang_1 :::"^^"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) )))) ; theorem :: FLANG_1:45 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "C")) ($#k8_flang_1 :::"*"::: ) )) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "C")) ($#k8_flang_1 :::"*"::: ) ))) "holds" (Bool (Set (Set (Var "a")) ($#k1_flang_1 :::"^"::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "C")) ($#k8_flang_1 :::"*"::: ) ))))) ; theorem :: FLANG_1:46 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "C")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "C")) ($#k8_flang_1 :::"*"::: ) )) & (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "C")) ($#k8_flang_1 :::"*"::: ) ))) "holds" (Bool (Set (Set (Var "A")) ($#k6_flang_1 :::"^^"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "C")) ($#k8_flang_1 :::"*"::: ) )))) ; theorem :: FLANG_1:47 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_flang_1 :::"{"::: ) (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) )) "iff" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k4_flang_1 :::"{"::: ) (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) )) ")" ) ")" ))) ; theorem :: FLANG_1:48 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) "holds" (Bool (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) )))) ; theorem :: FLANG_1:49 (Bool "for" (Set (Var "x")) "," (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) "st" (Bool (Bool (Set (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")))))) ; theorem :: FLANG_1:50 (Bool "for" (Set (Var "E")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set "(" (Set (Var "m")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set (Var "A")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ")" ))) ")" )))) ; theorem :: FLANG_1:51 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set "(" (Set (Var "m")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set (Var "A")))) & (Bool (Set (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set "(" (Set (Var "m")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ")" ))) ")" )))) ; theorem :: FLANG_1:52 (Bool "for" (Set (Var "E")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) "st" (Bool (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set (Var "A")))) "or" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ")" ))) ")" )) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) )))) ; theorem :: FLANG_1:53 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) )) & (Bool (Set (Set (Var "A")) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) )) ")" ))) ; theorem :: FLANG_1:54 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) "st" (Bool (Bool (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set (Var "A")))) & (Bool (Set (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ")" ))) ")" ))) ; theorem :: FLANG_1:55 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "n")) ")" ))) & (Bool (Set (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "n")) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ")" ))) ")" )))) ; theorem :: FLANG_1:56 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_flang_1 :::"{"::: ) (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "A")) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ")" ) ")" ))) & (Bool (Set (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_flang_1 :::"{"::: ) (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set "(" (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set (Var "A")) ")" ))) ")" ))) ; theorem :: FLANG_1:57 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) "holds" (Bool (Set (Set (Var "A")) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set (Var "A")))))) ; theorem :: FLANG_1:58 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "n")) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "n")) ")" )))))) ; theorem :: FLANG_1:59 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k8_flang_1 :::"*"::: ) ))) "holds" (Bool (Set (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k8_flang_1 :::"*"::: ) ))))) ; theorem :: FLANG_1:60 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k8_flang_1 :::"*"::: ) ))) "holds" (Bool (Set (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k8_flang_1 :::"*"::: ) )))) ; theorem :: FLANG_1:61 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k8_flang_1 :::"*"::: ) )))) ; theorem :: FLANG_1:62 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ")" ) ($#k8_flang_1 :::"*"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) )))) ; theorem :: FLANG_1:63 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) )))) ; theorem :: FLANG_1:64 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "n")) ")" ) ($#k8_flang_1 :::"*"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ))))) ; theorem :: FLANG_1:65 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ")" ) ($#k7_flang_1 :::"|^"::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ))))) ; theorem :: FLANG_1:66 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) (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 (Set "(" (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ")" ) ($#k7_flang_1 :::"|^"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ))))) ; theorem :: FLANG_1:67 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k8_flang_1 :::"*"::: ) ))) "holds" (Bool (Set (Set (Var "B")) ($#k8_flang_1 :::"*"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "B")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A")) ")" ) ($#k8_flang_1 :::"*"::: ) )))) ; theorem :: FLANG_1:68 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ))) "holds" (Bool (Set (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set ($#k4_flang_1 :::"{"::: ) (Set (Var "a")) ($#k4_flang_1 :::"}"::: ) ) ")" ) ($#k8_flang_1 :::"*"::: ) ))))) ; theorem :: FLANG_1:69 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) "holds" (Bool (Set (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set ($#k4_flang_1 :::"{"::: ) (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) ) ")" ) ($#k8_flang_1 :::"*"::: ) )))) ; theorem :: FLANG_1:70 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "B")) ($#k8_flang_1 :::"*"::: ) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" ) ($#k8_flang_1 :::"*"::: ) )))) ; theorem :: FLANG_1:71 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B")) ")" ) ($#k8_flang_1 :::"*"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "B")) ($#k8_flang_1 :::"*"::: ) ")" ))))) ; theorem :: FLANG_1:72 (Bool "for" (Set (Var "E")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) "holds" (Bool "(" (Bool (Set ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x")) ($#k5_afinsq_1 :::"%>"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) )) "iff" (Bool (Set ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x")) ($#k5_afinsq_1 :::"%>"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ))) ; begin definitionlet "E" be ($#m1_hidden :::"set"::: ) ; func :::"Lex"::: "E" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" "E" ($#k3_catalan2 :::"^omega"::: ) ")" ) means :: FLANG_1:def 4 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "E" "st" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) "E") & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "e")) ($#k5_afinsq_1 :::"%>"::: ) )) ")" )) ")" )); end; :: deftheorem defines :::"Lex"::: FLANG_1:def 4 : (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k9_flang_1 :::"Lex"::: ) (Set (Var "E")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "ex" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "st" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Var "E"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "e")) ($#k5_afinsq_1 :::"%>"::: ) )) ")" )) ")" )) ")" ))); theorem :: FLANG_1:73 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ) "holds" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k9_flang_1 :::"Lex"::: ) (Set (Var "E")) ")" ) ($#k7_flang_1 :::"|^"::: ) (Set "(" ($#k1_afinsq_1 :::"len"::: ) (Set (Var "a")) ")" ))))) ; theorem :: FLANG_1:74 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" ($#k9_flang_1 :::"Lex"::: ) (Set (Var "E")) ")" ) ($#k8_flang_1 :::"*"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ))) ; theorem :: FLANG_1:75 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ")" ) "st" (Bool (Bool (Set (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "E")) ($#k3_catalan2 :::"^omega"::: ) ))) "holds" (Bool (Set ($#k9_flang_1 :::"Lex"::: ) (Set (Var "E"))) ($#r1_tarski :::"c="::: ) (Set (Var "A"))))) ;