:: ZF_LANG semantic presentation begin definitionfunc :::"VAR"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) equals :: ZF_LANG:def 1 "{" (Set (Var "k")) where k "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Num 5) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) "}" ; end; :: deftheorem defines :::"VAR"::: ZF_LANG:def 1 : (Bool (Set ($#k1_zf_lang :::"VAR"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set (Var "k")) where k "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Num 5) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) "}" ); registration cluster (Set ($#k1_zf_lang :::"VAR"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionmode Variable is ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ); end; definitionlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"x."::: "n" -> ($#m2_subset_1 :::"Variable":::) equals :: ZF_LANG:def 2 (Set (Num 5) ($#k2_nat_1 :::"+"::: ) "n"); end; :: deftheorem defines :::"x."::: ZF_LANG:def 2 : (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k2_zf_lang :::"x."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Num 5) ($#k2_nat_1 :::"+"::: ) (Set (Var "n"))))); definitionlet "x" be ($#m2_subset_1 :::"Variable":::); :: original: :::"<*"::: redefine func :::"<*":::"x":::"*>"::: -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); end; definitionlet "x", "y" be ($#m2_subset_1 :::"Variable":::); func "x" :::"'='"::: "y" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) equals :: ZF_LANG:def 3 (Set (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k3_zf_lang :::"<*"::: ) "x" ($#k3_zf_lang :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k3_zf_lang :::"<*"::: ) "y" ($#k3_zf_lang :::"*>"::: ) )); func "x" :::"'in'"::: "y" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) equals :: ZF_LANG:def 4 (Set (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k3_zf_lang :::"<*"::: ) "x" ($#k3_zf_lang :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k3_zf_lang :::"<*"::: ) "y" ($#k3_zf_lang :::"*>"::: ) )); end; :: deftheorem defines :::"'='"::: ZF_LANG:def 3 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) "holds" (Bool (Set (Set (Var "x")) ($#k4_zf_lang :::"'='"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k3_zf_lang :::"<*"::: ) (Set (Var "x")) ($#k3_zf_lang :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k3_zf_lang :::"<*"::: ) (Set (Var "y")) ($#k3_zf_lang :::"*>"::: ) )))); :: deftheorem defines :::"'in'"::: ZF_LANG:def 4 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) "holds" (Bool (Set (Set (Var "x")) ($#k5_zf_lang :::"'in'"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k3_zf_lang :::"<*"::: ) (Set (Var "x")) ($#k3_zf_lang :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k3_zf_lang :::"<*"::: ) (Set (Var "y")) ($#k3_zf_lang :::"*>"::: ) )))); theorem :: ZF_LANG:1 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "t")) "being" ($#m2_subset_1 :::"Variable":::) "st" (Bool (Bool (Set (Set (Var "x")) ($#k4_zf_lang :::"'='"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k4_zf_lang :::"'='"::: ) (Set (Var "t"))))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "z"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "t"))) ")" )) ; theorem :: ZF_LANG:2 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "t")) "being" ($#m2_subset_1 :::"Variable":::) "st" (Bool (Bool (Set (Set (Var "x")) ($#k5_zf_lang :::"'in'"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k5_zf_lang :::"'in'"::: ) (Set (Var "t"))))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "z"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "t"))) ")" )) ; definitionlet "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"'not'"::: "p" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) equals :: ZF_LANG:def 5 (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Num 2) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) "p"); let "q" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func "p" :::"'&'"::: "q" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) equals :: ZF_LANG:def 6 (Set (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Num 3) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) "p" ")" ) ($#k8_finseq_1 :::"^"::: ) "q"); end; :: deftheorem defines :::"'not'"::: ZF_LANG:def 5 : (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k6_zf_lang :::"'not'"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Num 2) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "p"))))); :: deftheorem defines :::"'&'"::: ZF_LANG:def 6 : (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "p")) ($#k7_zf_lang :::"'&'"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Num 3) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "p")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "q"))))); definitionlet "x" be ($#m2_subset_1 :::"Variable":::); let "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"All"::: "(" "x" "," "p" ")" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) equals :: ZF_LANG:def 7 (Set (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Num 4) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k3_zf_lang :::"<*"::: ) "x" ($#k3_zf_lang :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) "p"); end; :: deftheorem defines :::"All"::: ZF_LANG:def 7 : (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Variable":::) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k8_zf_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Num 4) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k3_zf_lang :::"<*"::: ) (Set (Var "x")) ($#k3_zf_lang :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "p")))))); theorem :: ZF_LANG:3 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) "st" (Bool (Bool (Set ($#k8_zf_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_zf_lang :::"All"::: ) "(" (Set (Var "y")) "," (Set (Var "q")) ")" ))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "q"))) ")" ))) ; definitionfunc :::"WFF"::: -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) means :: ZF_LANG:def 8 (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) it)) "holds" (Bool (Set (Var "a")) "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k4_zf_lang :::"'='"::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) it) & (Bool (Set (Set (Var "x")) ($#k5_zf_lang :::"'in'"::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) it) ")" ) ")" ) & (Bool "(" "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) it)) "holds" (Bool (Set ($#k6_zf_lang :::"'not'"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) it) ")" ) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) it) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) it)) "holds" (Bool (Set (Set (Var "p")) ($#k7_zf_lang :::"'&'"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) it) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Variable":::) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) it)) "holds" (Bool (Set ($#k8_zf_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ) ($#r2_hidden :::"in"::: ) it)) ")" ) & (Bool "(" "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set (Var "a")) "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k4_zf_lang :::"'='"::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Set (Var "x")) ($#k5_zf_lang :::"'in'"::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set ($#k6_zf_lang :::"'not'"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) ")" ) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set (Set (Var "p")) ($#k7_zf_lang :::"'&'"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Variable":::) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set ($#k8_zf_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) ")" )) "holds" (Bool it ($#r1_tarski :::"c="::: ) (Set (Var "D"))) ")" ) ")" ); end; :: deftheorem defines :::"WFF"::: ZF_LANG:def 8 : (Bool "for" (Set (Var "b1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k9_zf_lang :::"WFF"::: ) )) "iff" (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b1")))) "holds" (Bool (Set (Var "a")) "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k4_zf_lang :::"'='"::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) & (Bool (Set (Set (Var "x")) ($#k5_zf_lang :::"'in'"::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "b1")))) "holds" (Bool (Set ($#k6_zf_lang :::"'not'"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) ")" ) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "b1")))) "holds" (Bool (Set (Set (Var "p")) ($#k7_zf_lang :::"'&'"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Variable":::) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "b1")))) "holds" (Bool (Set ($#k8_zf_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ) ($#r2_hidden :::"in"::: ) (Set (Var "b1")))) ")" ) & (Bool "(" "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set (Var "a")) "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k4_zf_lang :::"'='"::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Set (Var "x")) ($#k5_zf_lang :::"'in'"::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set ($#k6_zf_lang :::"'not'"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) ")" ) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set (Set (Var "p")) ($#k7_zf_lang :::"'&'"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Variable":::) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set ($#k8_zf_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) ")" )) "holds" (Bool (Set (Var "b1")) ($#r1_tarski :::"c="::: ) (Set (Var "D"))) ")" ) ")" ) ")" )); definitionlet "IT" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); attr "IT" is :::"ZF-formula-like"::: means :: ZF_LANG:def 9 (Bool "IT" "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_zf_lang :::"WFF"::: ) )); end; :: deftheorem defines :::"ZF-formula-like"::: ZF_LANG:def 9 : (Bool "for" (Set (Var "IT")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_zf_lang :::"ZF-formula-like"::: ) ) "iff" (Bool (Set (Var "IT")) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_zf_lang :::"WFF"::: ) )) ")" )); registration cluster ($#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_FINSET_1() ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v1_zf_lang :::"ZF-formula-like"::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); end; definitionmode ZF-formula is ($#v1_zf_lang :::"ZF-formula-like"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); end; theorem :: ZF_LANG:4 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#m2_finseq_1 :::"ZF-formula":::)) "iff" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_zf_lang :::"WFF"::: ) )) ")" )) ; registrationlet "x", "y" be ($#m2_subset_1 :::"Variable":::); cluster (Set "x" ($#k4_zf_lang :::"'='"::: ) "y") -> ($#v1_zf_lang :::"ZF-formula-like"::: ) ; cluster (Set "x" ($#k5_zf_lang :::"'in'"::: ) "y") -> ($#v1_zf_lang :::"ZF-formula-like"::: ) ; end; registrationlet "H" be ($#m2_finseq_1 :::"ZF-formula":::); cluster (Set ($#k6_zf_lang :::"'not'"::: ) "H") -> ($#v1_zf_lang :::"ZF-formula-like"::: ) ; let "G" be ($#m2_finseq_1 :::"ZF-formula":::); cluster (Set "H" ($#k7_zf_lang :::"'&'"::: ) "G") -> ($#v1_zf_lang :::"ZF-formula-like"::: ) ; end; registrationlet "x" be ($#m2_subset_1 :::"Variable":::); let "H" be ($#m2_finseq_1 :::"ZF-formula":::); cluster (Set ($#k8_zf_lang :::"All"::: ) "(" "x" "," "H" ")" ) -> ($#v1_zf_lang :::"ZF-formula-like"::: ) ; end; definitionlet "H" be ($#m2_finseq_1 :::"ZF-formula":::); attr "H" is :::"being_equality"::: means :: ZF_LANG:def 10 (Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) "st" (Bool "H" ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k4_zf_lang :::"'='"::: ) (Set (Var "y"))))); attr "H" is :::"being_membership"::: means :: ZF_LANG:def 11 (Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) "st" (Bool "H" ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k5_zf_lang :::"'in'"::: ) (Set (Var "y"))))); attr "H" is :::"negative"::: means :: ZF_LANG:def 12 (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool "H" ($#r1_hidden :::"="::: ) (Set ($#k6_zf_lang :::"'not'"::: ) (Set (Var "H1"))))); attr "H" is :::"conjunctive"::: means :: ZF_LANG:def 13 (Bool "ex" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool "H" ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_zf_lang :::"'&'"::: ) (Set (Var "G"))))); attr "H" is :::"universal"::: means :: ZF_LANG:def 14 (Bool "ex" (Set (Var "x")) "being" ($#m2_subset_1 :::"Variable":::)(Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool "H" ($#r1_hidden :::"="::: ) (Set ($#k8_zf_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "H1")) ")" )))); end; :: deftheorem defines :::"being_equality"::: ZF_LANG:def 10 : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" (Bool (Set (Var "H")) "is" ($#v2_zf_lang :::"being_equality"::: ) ) "iff" (Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k4_zf_lang :::"'='"::: ) (Set (Var "y"))))) ")" )); :: deftheorem defines :::"being_membership"::: ZF_LANG:def 11 : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" (Bool (Set (Var "H")) "is" ($#v3_zf_lang :::"being_membership"::: ) ) "iff" (Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k5_zf_lang :::"'in'"::: ) (Set (Var "y"))))) ")" )); :: deftheorem defines :::"negative"::: ZF_LANG:def 12 : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" (Bool (Set (Var "H")) "is" ($#v4_zf_lang :::"negative"::: ) ) "iff" (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#k6_zf_lang :::"'not'"::: ) (Set (Var "H1"))))) ")" )); :: deftheorem defines :::"conjunctive"::: ZF_LANG:def 13 : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" (Bool (Set (Var "H")) "is" ($#v5_zf_lang :::"conjunctive"::: ) ) "iff" (Bool "ex" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_zf_lang :::"'&'"::: ) (Set (Var "G"))))) ")" )); :: deftheorem defines :::"universal"::: ZF_LANG:def 14 : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" (Bool (Set (Var "H")) "is" ($#v6_zf_lang :::"universal"::: ) ) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m2_subset_1 :::"Variable":::)(Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#k8_zf_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "H1")) ")" )))) ")" )); theorem :: ZF_LANG:5 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "H")) "is" ($#v2_zf_lang :::"being_equality"::: ) )) "implies" (Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k4_zf_lang :::"'='"::: ) (Set (Var "y"))))) ")" & "(" (Bool (Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k4_zf_lang :::"'='"::: ) (Set (Var "y")))))) "implies" (Bool (Set (Var "H")) "is" ($#v2_zf_lang :::"being_equality"::: ) ) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v3_zf_lang :::"being_membership"::: ) )) "implies" (Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k5_zf_lang :::"'in'"::: ) (Set (Var "y"))))) ")" & "(" (Bool (Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k5_zf_lang :::"'in'"::: ) (Set (Var "y")))))) "implies" (Bool (Set (Var "H")) "is" ($#v3_zf_lang :::"being_membership"::: ) ) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v4_zf_lang :::"negative"::: ) )) "implies" (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#k6_zf_lang :::"'not'"::: ) (Set (Var "H1"))))) ")" & "(" (Bool (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#k6_zf_lang :::"'not'"::: ) (Set (Var "H1")))))) "implies" (Bool (Set (Var "H")) "is" ($#v4_zf_lang :::"negative"::: ) ) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v5_zf_lang :::"conjunctive"::: ) )) "implies" (Bool "ex" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_zf_lang :::"'&'"::: ) (Set (Var "G"))))) ")" & "(" (Bool (Bool "ex" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_zf_lang :::"'&'"::: ) (Set (Var "G")))))) "implies" (Bool (Set (Var "H")) "is" ($#v5_zf_lang :::"conjunctive"::: ) ) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v6_zf_lang :::"universal"::: ) )) "implies" (Bool "ex" (Set (Var "x")) "being" ($#m2_subset_1 :::"Variable":::)(Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#k8_zf_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "H1")) ")" )))) ")" & "(" (Bool (Bool "ex" (Set (Var "x")) "being" ($#m2_subset_1 :::"Variable":::)(Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#k8_zf_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "H1")) ")" ))))) "implies" (Bool (Set (Var "H")) "is" ($#v6_zf_lang :::"universal"::: ) ) ")" ")" )) ; definitionlet "H" be ($#m2_finseq_1 :::"ZF-formula":::); attr "H" is :::"atomic"::: means :: ZF_LANG:def 15 (Bool "(" (Bool "H" "is" ($#v2_zf_lang :::"being_equality"::: ) ) "or" (Bool "H" "is" ($#v3_zf_lang :::"being_membership"::: ) ) ")" ); end; :: deftheorem defines :::"atomic"::: ZF_LANG:def 15 : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" (Bool (Set (Var "H")) "is" ($#v7_zf_lang :::"atomic"::: ) ) "iff" (Bool "(" (Bool (Set (Var "H")) "is" ($#v2_zf_lang :::"being_equality"::: ) ) "or" (Bool (Set (Var "H")) "is" ($#v3_zf_lang :::"being_membership"::: ) ) ")" ) ")" )); definitionlet "F", "G" be ($#m2_finseq_1 :::"ZF-formula":::); func "F" :::"'or'"::: "G" -> ($#m2_finseq_1 :::"ZF-formula":::) equals :: ZF_LANG:def 16 (Set ($#k6_zf_lang :::"'not'"::: ) (Set "(" (Set "(" ($#k6_zf_lang :::"'not'"::: ) "F" ")" ) ($#k7_zf_lang :::"'&'"::: ) (Set "(" ($#k6_zf_lang :::"'not'"::: ) "G" ")" ) ")" )); func "F" :::"=>"::: "G" -> ($#m2_finseq_1 :::"ZF-formula":::) equals :: ZF_LANG:def 17 (Set ($#k6_zf_lang :::"'not'"::: ) (Set "(" "F" ($#k7_zf_lang :::"'&'"::: ) (Set "(" ($#k6_zf_lang :::"'not'"::: ) "G" ")" ) ")" )); end; :: deftheorem defines :::"'or'"::: ZF_LANG:def 16 : (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool (Set (Set (Var "F")) ($#k10_zf_lang :::"'or'"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k6_zf_lang :::"'not'"::: ) (Set "(" (Set "(" ($#k6_zf_lang :::"'not'"::: ) (Set (Var "F")) ")" ) ($#k7_zf_lang :::"'&'"::: ) (Set "(" ($#k6_zf_lang :::"'not'"::: ) (Set (Var "G")) ")" ) ")" )))); :: deftheorem defines :::"=>"::: ZF_LANG:def 17 : (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool (Set (Set (Var "F")) ($#k11_zf_lang :::"=>"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k6_zf_lang :::"'not'"::: ) (Set "(" (Set (Var "F")) ($#k7_zf_lang :::"'&'"::: ) (Set "(" ($#k6_zf_lang :::"'not'"::: ) (Set (Var "G")) ")" ) ")" )))); definitionlet "F", "G" be ($#m2_finseq_1 :::"ZF-formula":::); func "F" :::"<=>"::: "G" -> ($#m2_finseq_1 :::"ZF-formula":::) equals :: ZF_LANG:def 18 (Set (Set "(" "F" ($#k11_zf_lang :::"=>"::: ) "G" ")" ) ($#k7_zf_lang :::"'&'"::: ) (Set "(" "G" ($#k11_zf_lang :::"=>"::: ) "F" ")" )); end; :: deftheorem defines :::"<=>"::: ZF_LANG:def 18 : (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool (Set (Set (Var "F")) ($#k12_zf_lang :::"<=>"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k11_zf_lang :::"=>"::: ) (Set (Var "G")) ")" ) ($#k7_zf_lang :::"'&'"::: ) (Set "(" (Set (Var "G")) ($#k11_zf_lang :::"=>"::: ) (Set (Var "F")) ")" )))); definitionlet "x" be ($#m2_subset_1 :::"Variable":::); let "H" be ($#m2_finseq_1 :::"ZF-formula":::); func :::"Ex"::: "(" "x" "," "H" ")" -> ($#m2_finseq_1 :::"ZF-formula":::) equals :: ZF_LANG:def 19 (Set ($#k6_zf_lang :::"'not'"::: ) (Set "(" ($#k8_zf_lang :::"All"::: ) "(" "x" "," (Set "(" ($#k6_zf_lang :::"'not'"::: ) "H" ")" ) ")" ")" )); end; :: deftheorem defines :::"Ex"::: ZF_LANG:def 19 : (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Variable":::) (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool (Set ($#k13_zf_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "H")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_zf_lang :::"'not'"::: ) (Set "(" ($#k8_zf_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k6_zf_lang :::"'not'"::: ) (Set (Var "H")) ")" ) ")" ")" ))))); definitionlet "H" be ($#m2_finseq_1 :::"ZF-formula":::); attr "H" is :::"disjunctive"::: means :: ZF_LANG:def 20 (Bool "ex" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool "H" ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k10_zf_lang :::"'or'"::: ) (Set (Var "G"))))); attr "H" is :::"conditional"::: means :: ZF_LANG:def 21 (Bool "ex" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool "H" ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k11_zf_lang :::"=>"::: ) (Set (Var "G"))))); attr "H" is :::"biconditional"::: means :: ZF_LANG:def 22 (Bool "ex" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool "H" ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k12_zf_lang :::"<=>"::: ) (Set (Var "G"))))); attr "H" is :::"existential"::: means :: ZF_LANG:def 23 (Bool "ex" (Set (Var "x")) "being" ($#m2_subset_1 :::"Variable":::)(Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool "H" ($#r1_hidden :::"="::: ) (Set ($#k13_zf_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "H1")) ")" )))); end; :: deftheorem defines :::"disjunctive"::: ZF_LANG:def 20 : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" (Bool (Set (Var "H")) "is" ($#v8_zf_lang :::"disjunctive"::: ) ) "iff" (Bool "ex" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k10_zf_lang :::"'or'"::: ) (Set (Var "G"))))) ")" )); :: deftheorem defines :::"conditional"::: ZF_LANG:def 21 : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" (Bool (Set (Var "H")) "is" ($#v9_zf_lang :::"conditional"::: ) ) "iff" (Bool "ex" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k11_zf_lang :::"=>"::: ) (Set (Var "G"))))) ")" )); :: deftheorem defines :::"biconditional"::: ZF_LANG:def 22 : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" (Bool (Set (Var "H")) "is" ($#v10_zf_lang :::"biconditional"::: ) ) "iff" (Bool "ex" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k12_zf_lang :::"<=>"::: ) (Set (Var "G"))))) ")" )); :: deftheorem defines :::"existential"::: ZF_LANG:def 23 : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" (Bool (Set (Var "H")) "is" ($#v11_zf_lang :::"existential"::: ) ) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m2_subset_1 :::"Variable":::)(Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#k13_zf_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "H1")) ")" )))) ")" )); theorem :: ZF_LANG:6 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "H")) "is" ($#v8_zf_lang :::"disjunctive"::: ) )) "implies" (Bool "ex" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k10_zf_lang :::"'or'"::: ) (Set (Var "G"))))) ")" & "(" (Bool (Bool "ex" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k10_zf_lang :::"'or'"::: ) (Set (Var "G")))))) "implies" (Bool (Set (Var "H")) "is" ($#v8_zf_lang :::"disjunctive"::: ) ) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v9_zf_lang :::"conditional"::: ) )) "implies" (Bool "ex" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k11_zf_lang :::"=>"::: ) (Set (Var "G"))))) ")" & "(" (Bool (Bool "ex" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k11_zf_lang :::"=>"::: ) (Set (Var "G")))))) "implies" (Bool (Set (Var "H")) "is" ($#v9_zf_lang :::"conditional"::: ) ) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v10_zf_lang :::"biconditional"::: ) )) "implies" (Bool "ex" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k12_zf_lang :::"<=>"::: ) (Set (Var "G"))))) ")" & "(" (Bool (Bool "ex" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k12_zf_lang :::"<=>"::: ) (Set (Var "G")))))) "implies" (Bool (Set (Var "H")) "is" ($#v10_zf_lang :::"biconditional"::: ) ) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v11_zf_lang :::"existential"::: ) )) "implies" (Bool "ex" (Set (Var "x")) "being" ($#m2_subset_1 :::"Variable":::)(Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#k13_zf_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "H1")) ")" )))) ")" & "(" (Bool (Bool "ex" (Set (Var "x")) "being" ($#m2_subset_1 :::"Variable":::)(Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#k13_zf_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "H1")) ")" ))))) "implies" (Bool (Set (Var "H")) "is" ($#v11_zf_lang :::"existential"::: ) ) ")" ")" )) ; definitionlet "x", "y" be ($#m2_subset_1 :::"Variable":::); let "H" be ($#m2_finseq_1 :::"ZF-formula":::); func :::"All"::: "(" "x" "," "y" "," "H" ")" -> ($#m2_finseq_1 :::"ZF-formula":::) equals :: ZF_LANG:def 24 (Set ($#k8_zf_lang :::"All"::: ) "(" "x" "," (Set "(" ($#k8_zf_lang :::"All"::: ) "(" "y" "," "H" ")" ")" ) ")" ); func :::"Ex"::: "(" "x" "," "y" "," "H" ")" -> ($#m2_finseq_1 :::"ZF-formula":::) equals :: ZF_LANG:def 25 (Set ($#k13_zf_lang :::"Ex"::: ) "(" "x" "," (Set "(" ($#k13_zf_lang :::"Ex"::: ) "(" "y" "," "H" ")" ")" ) ")" ); end; :: deftheorem defines :::"All"::: ZF_LANG:def 24 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool (Set ($#k14_zf_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "H")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_zf_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k8_zf_lang :::"All"::: ) "(" (Set (Var "y")) "," (Set (Var "H")) ")" ")" ) ")" )))); :: deftheorem defines :::"Ex"::: ZF_LANG:def 25 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool (Set ($#k15_zf_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "H")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k13_zf_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k13_zf_lang :::"Ex"::: ) "(" (Set (Var "y")) "," (Set (Var "H")) ")" ")" ) ")" )))); theorem :: ZF_LANG:7 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" (Bool (Set ($#k14_zf_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "H")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_zf_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k8_zf_lang :::"All"::: ) "(" (Set (Var "y")) "," (Set (Var "H")) ")" ")" ) ")" )) & (Bool (Set ($#k15_zf_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "H")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k13_zf_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k13_zf_lang :::"Ex"::: ) "(" (Set (Var "y")) "," (Set (Var "H")) ")" ")" ) ")" )) ")" ))) ; definitionlet "x", "y", "z" be ($#m2_subset_1 :::"Variable":::); let "H" be ($#m2_finseq_1 :::"ZF-formula":::); func :::"All"::: "(" "x" "," "y" "," "z" "," "H" ")" -> ($#m2_finseq_1 :::"ZF-formula":::) equals :: ZF_LANG:def 26 (Set ($#k8_zf_lang :::"All"::: ) "(" "x" "," (Set "(" ($#k14_zf_lang :::"All"::: ) "(" "y" "," "z" "," "H" ")" ")" ) ")" ); func :::"Ex"::: "(" "x" "," "y" "," "z" "," "H" ")" -> ($#m2_finseq_1 :::"ZF-formula":::) equals :: ZF_LANG:def 27 (Set ($#k13_zf_lang :::"Ex"::: ) "(" "x" "," (Set "(" ($#k15_zf_lang :::"Ex"::: ) "(" "y" "," "z" "," "H" ")" ")" ) ")" ); end; :: deftheorem defines :::"All"::: ZF_LANG:def 26 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m2_subset_1 :::"Variable":::) (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool (Set ($#k16_zf_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "H")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_zf_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k14_zf_lang :::"All"::: ) "(" (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "H")) ")" ")" ) ")" )))); :: deftheorem defines :::"Ex"::: ZF_LANG:def 27 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m2_subset_1 :::"Variable":::) (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool (Set ($#k17_zf_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "H")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k13_zf_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k15_zf_lang :::"Ex"::: ) "(" (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "H")) ")" ")" ) ")" )))); theorem :: ZF_LANG:8 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m2_subset_1 :::"Variable":::) (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" (Bool (Set ($#k16_zf_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "H")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_zf_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k14_zf_lang :::"All"::: ) "(" (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "H")) ")" ")" ) ")" )) & (Bool (Set ($#k17_zf_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "H")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k13_zf_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k15_zf_lang :::"Ex"::: ) "(" (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "H")) ")" ")" ) ")" )) ")" ))) ; theorem :: ZF_LANG:9 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" (Bool (Set (Var "H")) "is" ($#v2_zf_lang :::"being_equality"::: ) ) "or" (Bool (Set (Var "H")) "is" ($#v3_zf_lang :::"being_membership"::: ) ) "or" (Bool (Set (Var "H")) "is" ($#v4_zf_lang :::"negative"::: ) ) "or" (Bool (Set (Var "H")) "is" ($#v5_zf_lang :::"conjunctive"::: ) ) "or" (Bool (Set (Var "H")) "is" ($#v6_zf_lang :::"universal"::: ) ) ")" )) ; theorem :: ZF_LANG:10 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" (Bool (Set (Var "H")) "is" ($#v7_zf_lang :::"atomic"::: ) ) "or" (Bool (Set (Var "H")) "is" ($#v4_zf_lang :::"negative"::: ) ) "or" (Bool (Set (Var "H")) "is" ($#v5_zf_lang :::"conjunctive"::: ) ) "or" (Bool (Set (Var "H")) "is" ($#v6_zf_lang :::"universal"::: ) ) ")" )) ; theorem :: ZF_LANG:11 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v7_zf_lang :::"atomic"::: ) )) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Num 3))) ; theorem :: ZF_LANG:12 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" (Bool (Set (Var "H")) "is" ($#v7_zf_lang :::"atomic"::: ) ) "or" (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "H1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "H"))))) ")" )) ; theorem :: ZF_LANG:13 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool (Num 3) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "H"))))) ; theorem :: ZF_LANG:14 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Num 3))) "holds" (Bool (Set (Var "H")) "is" ($#v7_zf_lang :::"atomic"::: ) )) ; theorem :: ZF_LANG:15 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "x")) ($#k4_zf_lang :::"'='"::: ) (Set (Var "y")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" (Set (Var "x")) ($#k5_zf_lang :::"'in'"::: ) (Set (Var "y")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Num 1)) ")" )) ; theorem :: ZF_LANG:16 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k7_zf_lang :::"'&'"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Num 3))) ; theorem :: ZF_LANG:17 (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Variable":::) (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool (Set (Set "(" ($#k8_zf_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "H")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Num 4)))) ; theorem :: ZF_LANG:18 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v2_zf_lang :::"being_equality"::: ) )) "holds" (Bool (Set (Set (Var "H")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: ZF_LANG:19 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v3_zf_lang :::"being_membership"::: ) )) "holds" (Bool (Set (Set (Var "H")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: ZF_LANG:20 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v4_zf_lang :::"negative"::: ) )) "holds" (Bool (Set (Set (Var "H")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Num 2))) ; theorem :: ZF_LANG:21 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v5_zf_lang :::"conjunctive"::: ) )) "holds" (Bool (Set (Set (Var "H")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Num 3))) ; theorem :: ZF_LANG:22 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v6_zf_lang :::"universal"::: ) )) "holds" (Bool (Set (Set (Var "H")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Num 4))) ; theorem :: ZF_LANG:23 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "H")) "is" ($#v2_zf_lang :::"being_equality"::: ) ) & (Bool (Set (Set (Var "H")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) "or" (Bool "(" (Bool (Set (Var "H")) "is" ($#v3_zf_lang :::"being_membership"::: ) ) & (Bool (Set (Set (Var "H")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) "or" (Bool "(" (Bool (Set (Var "H")) "is" ($#v4_zf_lang :::"negative"::: ) ) & (Bool (Set (Set (Var "H")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Num 2)) ")" ) "or" (Bool "(" (Bool (Set (Var "H")) "is" ($#v5_zf_lang :::"conjunctive"::: ) ) & (Bool (Set (Set (Var "H")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Num 3)) ")" ) "or" (Bool "(" (Bool (Set (Var "H")) "is" ($#v6_zf_lang :::"universal"::: ) ) & (Bool (Set (Set (Var "H")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Num 4)) ")" ) ")" )) ; theorem :: ZF_LANG:24 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Set (Var "H")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "H")) "is" ($#v2_zf_lang :::"being_equality"::: ) )) ; theorem :: ZF_LANG:25 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Set (Var "H")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool (Set (Var "H")) "is" ($#v3_zf_lang :::"being_membership"::: ) )) ; theorem :: ZF_LANG:26 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Set (Var "H")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Num 2))) "holds" (Bool (Set (Var "H")) "is" ($#v4_zf_lang :::"negative"::: ) )) ; theorem :: ZF_LANG:27 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Set (Var "H")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Num 3))) "holds" (Bool (Set (Var "H")) "is" ($#v5_zf_lang :::"conjunctive"::: ) )) ; theorem :: ZF_LANG:28 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Set (Var "H")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Num 4))) "holds" (Bool (Set (Var "H")) "is" ($#v6_zf_lang :::"universal"::: ) )) ; theorem :: ZF_LANG:29 (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m2_finseq_1 :::"ZF-formula":::) (Bool "for" (Set (Var "sq")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "sq"))))) "holds" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Var "F"))))) ; theorem :: ZF_LANG:30 (Bool "for" (Set (Var "H")) "," (Set (Var "G")) "," (Set (Var "H1")) "," (Set (Var "G1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Set (Var "H")) ($#k7_zf_lang :::"'&'"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "H1")) ($#k7_zf_lang :::"'&'"::: ) (Set (Var "G1"))))) "holds" (Bool "(" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Var "H1"))) & (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set (Var "G1"))) ")" )) ; theorem :: ZF_LANG:31 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "F1")) "," (Set (Var "G1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Set (Var "F")) ($#k10_zf_lang :::"'or'"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F1")) ($#k10_zf_lang :::"'or'"::: ) (Set (Var "G1"))))) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Var "F1"))) & (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set (Var "G1"))) ")" )) ; theorem :: ZF_LANG:32 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "F1")) "," (Set (Var "G1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Set (Var "F")) ($#k11_zf_lang :::"=>"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F1")) ($#k11_zf_lang :::"=>"::: ) (Set (Var "G1"))))) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Var "F1"))) & (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set (Var "G1"))) ")" )) ; theorem :: ZF_LANG:33 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "F1")) "," (Set (Var "G1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Set (Var "F")) ($#k12_zf_lang :::"<=>"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F1")) ($#k12_zf_lang :::"<=>"::: ) (Set (Var "G1"))))) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Var "F1"))) & (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set (Var "G1"))) ")" )) ; theorem :: ZF_LANG:34 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) (Bool "for" (Set (Var "H")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set ($#k13_zf_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "H")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k13_zf_lang :::"Ex"::: ) "(" (Set (Var "y")) "," (Set (Var "G")) ")" ))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Var "G"))) ")" ))) ; definitionlet "H" be ($#m2_finseq_1 :::"ZF-formula":::); assume (Bool (Set (Const "H")) "is" ($#v7_zf_lang :::"atomic"::: ) ) ; func :::"Var1"::: "H" -> ($#m2_subset_1 :::"Variable":::) equals :: ZF_LANG:def 28 (Set "H" ($#k1_funct_1 :::"."::: ) (Num 2)); func :::"Var2"::: "H" -> ($#m2_subset_1 :::"Variable":::) equals :: ZF_LANG:def 29 (Set "H" ($#k1_funct_1 :::"."::: ) (Num 3)); end; :: deftheorem defines :::"Var1"::: ZF_LANG:def 28 : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v7_zf_lang :::"atomic"::: ) )) "holds" (Bool (Set ($#k18_zf_lang :::"Var1"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k1_funct_1 :::"."::: ) (Num 2)))); :: deftheorem defines :::"Var2"::: ZF_LANG:def 29 : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v7_zf_lang :::"atomic"::: ) )) "holds" (Bool (Set ($#k19_zf_lang :::"Var2"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k1_funct_1 :::"."::: ) (Num 3)))); theorem :: ZF_LANG:35 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v7_zf_lang :::"atomic"::: ) )) "holds" (Bool "(" (Bool (Set ($#k18_zf_lang :::"Var1"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k1_funct_1 :::"."::: ) (Num 2))) & (Bool (Set ($#k19_zf_lang :::"Var2"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k1_funct_1 :::"."::: ) (Num 3))) ")" )) ; theorem :: ZF_LANG:36 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v2_zf_lang :::"being_equality"::: ) )) "holds" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_zf_lang :::"Var1"::: ) (Set (Var "H")) ")" ) ($#k4_zf_lang :::"'='"::: ) (Set "(" ($#k19_zf_lang :::"Var2"::: ) (Set (Var "H")) ")" )))) ; theorem :: ZF_LANG:37 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v3_zf_lang :::"being_membership"::: ) )) "holds" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_zf_lang :::"Var1"::: ) (Set (Var "H")) ")" ) ($#k5_zf_lang :::"'in'"::: ) (Set "(" ($#k19_zf_lang :::"Var2"::: ) (Set (Var "H")) ")" )))) ; definitionlet "H" be ($#m2_finseq_1 :::"ZF-formula":::); assume (Bool (Set (Const "H")) "is" ($#v4_zf_lang :::"negative"::: ) ) ; func :::"the_argument_of"::: "H" -> ($#m2_finseq_1 :::"ZF-formula":::) means :: ZF_LANG:def 30 (Bool (Set ($#k6_zf_lang :::"'not'"::: ) it) ($#r1_hidden :::"="::: ) "H"); end; :: deftheorem defines :::"the_argument_of"::: ZF_LANG:def 30 : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v4_zf_lang :::"negative"::: ) )) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k20_zf_lang :::"the_argument_of"::: ) (Set (Var "H")))) "iff" (Bool (Set ($#k6_zf_lang :::"'not'"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Var "H"))) ")" ))); definitionlet "H" be ($#m2_finseq_1 :::"ZF-formula":::); assume (Bool "(" (Bool (Set (Const "H")) "is" ($#v5_zf_lang :::"conjunctive"::: ) ) "or" (Bool (Set (Const "H")) "is" ($#v8_zf_lang :::"disjunctive"::: ) ) ")" ) ; func :::"the_left_argument_of"::: "H" -> ($#m2_finseq_1 :::"ZF-formula":::) means :: ZF_LANG:def 31 (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set it ($#k7_zf_lang :::"'&'"::: ) (Set (Var "H1"))) ($#r1_hidden :::"="::: ) "H")) if (Bool "H" "is" ($#v5_zf_lang :::"conjunctive"::: ) ) otherwise (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set it ($#k10_zf_lang :::"'or'"::: ) (Set (Var "H1"))) ($#r1_hidden :::"="::: ) "H")); func :::"the_right_argument_of"::: "H" -> ($#m2_finseq_1 :::"ZF-formula":::) means :: ZF_LANG:def 32 (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Set (Var "H1")) ($#k7_zf_lang :::"'&'"::: ) it) ($#r1_hidden :::"="::: ) "H")) if (Bool "H" "is" ($#v5_zf_lang :::"conjunctive"::: ) ) otherwise (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Set (Var "H1")) ($#k10_zf_lang :::"'or'"::: ) it) ($#r1_hidden :::"="::: ) "H")); end; :: deftheorem defines :::"the_left_argument_of"::: ZF_LANG:def 31 : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool "(" (Bool (Set (Var "H")) "is" ($#v5_zf_lang :::"conjunctive"::: ) ) "or" (Bool (Set (Var "H")) "is" ($#v8_zf_lang :::"disjunctive"::: ) ) ")" )) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "H")) "is" ($#v5_zf_lang :::"conjunctive"::: ) )) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k21_zf_lang :::"the_left_argument_of"::: ) (Set (Var "H")))) "iff" (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Set (Var "b2")) ($#k7_zf_lang :::"'&'"::: ) (Set (Var "H1"))) ($#r1_hidden :::"="::: ) (Set (Var "H")))) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "H")) "is" ($#v5_zf_lang :::"conjunctive"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k21_zf_lang :::"the_left_argument_of"::: ) (Set (Var "H")))) "iff" (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Set (Var "b2")) ($#k10_zf_lang :::"'or'"::: ) (Set (Var "H1"))) ($#r1_hidden :::"="::: ) (Set (Var "H")))) ")" ) ")" ")" ))); :: deftheorem defines :::"the_right_argument_of"::: ZF_LANG:def 32 : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool "(" (Bool (Set (Var "H")) "is" ($#v5_zf_lang :::"conjunctive"::: ) ) "or" (Bool (Set (Var "H")) "is" ($#v8_zf_lang :::"disjunctive"::: ) ) ")" )) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "H")) "is" ($#v5_zf_lang :::"conjunctive"::: ) )) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k22_zf_lang :::"the_right_argument_of"::: ) (Set (Var "H")))) "iff" (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Set (Var "H1")) ($#k7_zf_lang :::"'&'"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Var "H")))) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "H")) "is" ($#v5_zf_lang :::"conjunctive"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k22_zf_lang :::"the_right_argument_of"::: ) (Set (Var "H")))) "iff" (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Set (Var "H1")) ($#k10_zf_lang :::"'or'"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Var "H")))) ")" ) ")" ")" ))); theorem :: ZF_LANG:38 (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v5_zf_lang :::"conjunctive"::: ) )) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k21_zf_lang :::"the_left_argument_of"::: ) (Set (Var "H"))))) "implies" (Bool "ex" (Set (Var "G")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Set (Var "F")) ($#k7_zf_lang :::"'&'"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Var "H")))) ")" & "(" (Bool (Bool "ex" (Set (Var "G")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Set (Var "F")) ($#k7_zf_lang :::"'&'"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Var "H"))))) "implies" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k21_zf_lang :::"the_left_argument_of"::: ) (Set (Var "H")))) ")" & "(" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k22_zf_lang :::"the_right_argument_of"::: ) (Set (Var "H"))))) "implies" (Bool "ex" (Set (Var "G")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Set (Var "G")) ($#k7_zf_lang :::"'&'"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Var "H")))) ")" & "(" (Bool (Bool "ex" (Set (Var "G")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Set (Var "G")) ($#k7_zf_lang :::"'&'"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Var "H"))))) "implies" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k22_zf_lang :::"the_right_argument_of"::: ) (Set (Var "H")))) ")" ")" )) ; theorem :: ZF_LANG:39 (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v8_zf_lang :::"disjunctive"::: ) )) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k21_zf_lang :::"the_left_argument_of"::: ) (Set (Var "H"))))) "implies" (Bool "ex" (Set (Var "G")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Set (Var "F")) ($#k10_zf_lang :::"'or'"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Var "H")))) ")" & "(" (Bool (Bool "ex" (Set (Var "G")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Set (Var "F")) ($#k10_zf_lang :::"'or'"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Var "H"))))) "implies" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k21_zf_lang :::"the_left_argument_of"::: ) (Set (Var "H")))) ")" & "(" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k22_zf_lang :::"the_right_argument_of"::: ) (Set (Var "H"))))) "implies" (Bool "ex" (Set (Var "G")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Set (Var "G")) ($#k10_zf_lang :::"'or'"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Var "H")))) ")" & "(" (Bool (Bool "ex" (Set (Var "G")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Set (Var "G")) ($#k10_zf_lang :::"'or'"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Var "H"))))) "implies" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k22_zf_lang :::"the_right_argument_of"::: ) (Set (Var "H")))) ")" ")" )) ; theorem :: ZF_LANG:40 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v5_zf_lang :::"conjunctive"::: ) )) "holds" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k21_zf_lang :::"the_left_argument_of"::: ) (Set (Var "H")) ")" ) ($#k7_zf_lang :::"'&'"::: ) (Set "(" ($#k22_zf_lang :::"the_right_argument_of"::: ) (Set (Var "H")) ")" )))) ; theorem :: ZF_LANG:41 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v8_zf_lang :::"disjunctive"::: ) )) "holds" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k21_zf_lang :::"the_left_argument_of"::: ) (Set (Var "H")) ")" ) ($#k10_zf_lang :::"'or'"::: ) (Set "(" ($#k22_zf_lang :::"the_right_argument_of"::: ) (Set (Var "H")) ")" )))) ; definitionlet "H" be ($#m2_finseq_1 :::"ZF-formula":::); assume (Bool "(" (Bool (Set (Const "H")) "is" ($#v6_zf_lang :::"universal"::: ) ) "or" (Bool (Set (Const "H")) "is" ($#v11_zf_lang :::"existential"::: ) ) ")" ) ; func :::"bound_in"::: "H" -> ($#m2_subset_1 :::"Variable":::) means :: ZF_LANG:def 33 (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set ($#k8_zf_lang :::"All"::: ) "(" it "," (Set (Var "H1")) ")" ) ($#r1_hidden :::"="::: ) "H")) if (Bool "H" "is" ($#v6_zf_lang :::"universal"::: ) ) otherwise (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set ($#k13_zf_lang :::"Ex"::: ) "(" it "," (Set (Var "H1")) ")" ) ($#r1_hidden :::"="::: ) "H")); func :::"the_scope_of"::: "H" -> ($#m2_finseq_1 :::"ZF-formula":::) means :: ZF_LANG:def 34 (Bool "ex" (Set (Var "x")) "being" ($#m2_subset_1 :::"Variable":::) "st" (Bool (Set ($#k8_zf_lang :::"All"::: ) "(" (Set (Var "x")) "," it ")" ) ($#r1_hidden :::"="::: ) "H")) if (Bool "H" "is" ($#v6_zf_lang :::"universal"::: ) ) otherwise (Bool "ex" (Set (Var "x")) "being" ($#m2_subset_1 :::"Variable":::) "st" (Bool (Set ($#k13_zf_lang :::"Ex"::: ) "(" (Set (Var "x")) "," it ")" ) ($#r1_hidden :::"="::: ) "H")); end; :: deftheorem defines :::"bound_in"::: ZF_LANG:def 33 : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool "(" (Bool (Set (Var "H")) "is" ($#v6_zf_lang :::"universal"::: ) ) "or" (Bool (Set (Var "H")) "is" ($#v11_zf_lang :::"existential"::: ) ) ")" )) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m2_subset_1 :::"Variable":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "H")) "is" ($#v6_zf_lang :::"universal"::: ) )) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k23_zf_lang :::"bound_in"::: ) (Set (Var "H")))) "iff" (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set ($#k8_zf_lang :::"All"::: ) "(" (Set (Var "b2")) "," (Set (Var "H1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "H")))) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "H")) "is" ($#v6_zf_lang :::"universal"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k23_zf_lang :::"bound_in"::: ) (Set (Var "H")))) "iff" (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set ($#k13_zf_lang :::"Ex"::: ) "(" (Set (Var "b2")) "," (Set (Var "H1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "H")))) ")" ) ")" ")" ))); :: deftheorem defines :::"the_scope_of"::: ZF_LANG:def 34 : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool "(" (Bool (Set (Var "H")) "is" ($#v6_zf_lang :::"universal"::: ) ) "or" (Bool (Set (Var "H")) "is" ($#v11_zf_lang :::"existential"::: ) ) ")" )) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "H")) "is" ($#v6_zf_lang :::"universal"::: ) )) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k24_zf_lang :::"the_scope_of"::: ) (Set (Var "H")))) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m2_subset_1 :::"Variable":::) "st" (Bool (Set ($#k8_zf_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "b2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "H")))) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "H")) "is" ($#v6_zf_lang :::"universal"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k24_zf_lang :::"the_scope_of"::: ) (Set (Var "H")))) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m2_subset_1 :::"Variable":::) "st" (Bool (Set ($#k13_zf_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "b2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "H")))) ")" ) ")" ")" ))); theorem :: ZF_LANG:42 (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Variable":::) (Bool "for" (Set (Var "H")) "," (Set (Var "H1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v6_zf_lang :::"universal"::: ) )) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k23_zf_lang :::"bound_in"::: ) (Set (Var "H"))))) "implies" (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set ($#k8_zf_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "H1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "H")))) ")" & "(" (Bool (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set ($#k8_zf_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "H1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "H"))))) "implies" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k23_zf_lang :::"bound_in"::: ) (Set (Var "H")))) ")" & "(" (Bool (Bool (Set (Var "H1")) ($#r1_hidden :::"="::: ) (Set ($#k24_zf_lang :::"the_scope_of"::: ) (Set (Var "H"))))) "implies" (Bool "ex" (Set (Var "x")) "being" ($#m2_subset_1 :::"Variable":::) "st" (Bool (Set ($#k8_zf_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "H1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "H")))) ")" & "(" (Bool (Bool "ex" (Set (Var "x")) "being" ($#m2_subset_1 :::"Variable":::) "st" (Bool (Set ($#k8_zf_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "H1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "H"))))) "implies" (Bool (Set (Var "H1")) ($#r1_hidden :::"="::: ) (Set ($#k24_zf_lang :::"the_scope_of"::: ) (Set (Var "H")))) ")" ")" ))) ; theorem :: ZF_LANG:43 (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Variable":::) (Bool "for" (Set (Var "H")) "," (Set (Var "H1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v11_zf_lang :::"existential"::: ) )) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k23_zf_lang :::"bound_in"::: ) (Set (Var "H"))))) "implies" (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set ($#k13_zf_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "H1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "H")))) ")" & "(" (Bool (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set ($#k13_zf_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "H1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "H"))))) "implies" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k23_zf_lang :::"bound_in"::: ) (Set (Var "H")))) ")" & "(" (Bool (Bool (Set (Var "H1")) ($#r1_hidden :::"="::: ) (Set ($#k24_zf_lang :::"the_scope_of"::: ) (Set (Var "H"))))) "implies" (Bool "ex" (Set (Var "x")) "being" ($#m2_subset_1 :::"Variable":::) "st" (Bool (Set ($#k13_zf_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "H1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "H")))) ")" & "(" (Bool (Bool "ex" (Set (Var "x")) "being" ($#m2_subset_1 :::"Variable":::) "st" (Bool (Set ($#k13_zf_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "H1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "H"))))) "implies" (Bool (Set (Var "H1")) ($#r1_hidden :::"="::: ) (Set ($#k24_zf_lang :::"the_scope_of"::: ) (Set (Var "H")))) ")" ")" ))) ; theorem :: ZF_LANG:44 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v6_zf_lang :::"universal"::: ) )) "holds" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k23_zf_lang :::"bound_in"::: ) (Set (Var "H")) ")" ) "," (Set "(" ($#k24_zf_lang :::"the_scope_of"::: ) (Set (Var "H")) ")" ) ")" ))) ; theorem :: ZF_LANG:45 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v11_zf_lang :::"existential"::: ) )) "holds" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#k13_zf_lang :::"Ex"::: ) "(" (Set "(" ($#k23_zf_lang :::"bound_in"::: ) (Set (Var "H")) ")" ) "," (Set "(" ($#k24_zf_lang :::"the_scope_of"::: ) (Set (Var "H")) ")" ) ")" ))) ; definitionlet "H" be ($#m2_finseq_1 :::"ZF-formula":::); assume (Bool (Set (Const "H")) "is" ($#v9_zf_lang :::"conditional"::: ) ) ; func :::"the_antecedent_of"::: "H" -> ($#m2_finseq_1 :::"ZF-formula":::) means :: ZF_LANG:def 35 (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool "H" ($#r1_hidden :::"="::: ) (Set it ($#k11_zf_lang :::"=>"::: ) (Set (Var "H1"))))); func :::"the_consequent_of"::: "H" -> ($#m2_finseq_1 :::"ZF-formula":::) means :: ZF_LANG:def 36 (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool "H" ($#r1_hidden :::"="::: ) (Set (Set (Var "H1")) ($#k11_zf_lang :::"=>"::: ) it))); end; :: deftheorem defines :::"the_antecedent_of"::: ZF_LANG:def 35 : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v9_zf_lang :::"conditional"::: ) )) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k25_zf_lang :::"the_antecedent_of"::: ) (Set (Var "H")))) "iff" (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b2")) ($#k11_zf_lang :::"=>"::: ) (Set (Var "H1"))))) ")" ))); :: deftheorem defines :::"the_consequent_of"::: ZF_LANG:def 36 : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v9_zf_lang :::"conditional"::: ) )) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k26_zf_lang :::"the_consequent_of"::: ) (Set (Var "H")))) "iff" (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "H1")) ($#k11_zf_lang :::"=>"::: ) (Set (Var "b2"))))) ")" ))); theorem :: ZF_LANG:46 (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v9_zf_lang :::"conditional"::: ) )) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k25_zf_lang :::"the_antecedent_of"::: ) (Set (Var "H"))))) "implies" (Bool "ex" (Set (Var "G")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k11_zf_lang :::"=>"::: ) (Set (Var "G"))))) ")" & "(" (Bool (Bool "ex" (Set (Var "G")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k11_zf_lang :::"=>"::: ) (Set (Var "G")))))) "implies" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k25_zf_lang :::"the_antecedent_of"::: ) (Set (Var "H")))) ")" & "(" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k26_zf_lang :::"the_consequent_of"::: ) (Set (Var "H"))))) "implies" (Bool "ex" (Set (Var "G")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k11_zf_lang :::"=>"::: ) (Set (Var "F"))))) ")" & "(" (Bool (Bool "ex" (Set (Var "G")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k11_zf_lang :::"=>"::: ) (Set (Var "F")))))) "implies" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k26_zf_lang :::"the_consequent_of"::: ) (Set (Var "H")))) ")" ")" )) ; theorem :: ZF_LANG:47 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v9_zf_lang :::"conditional"::: ) )) "holds" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k25_zf_lang :::"the_antecedent_of"::: ) (Set (Var "H")) ")" ) ($#k11_zf_lang :::"=>"::: ) (Set "(" ($#k26_zf_lang :::"the_consequent_of"::: ) (Set (Var "H")) ")" )))) ; definitionlet "H" be ($#m2_finseq_1 :::"ZF-formula":::); assume (Bool (Set (Const "H")) "is" ($#v10_zf_lang :::"biconditional"::: ) ) ; func :::"the_left_side_of"::: "H" -> ($#m2_finseq_1 :::"ZF-formula":::) means :: ZF_LANG:def 37 (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool "H" ($#r1_hidden :::"="::: ) (Set it ($#k12_zf_lang :::"<=>"::: ) (Set (Var "H1"))))); func :::"the_right_side_of"::: "H" -> ($#m2_finseq_1 :::"ZF-formula":::) means :: ZF_LANG:def 38 (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool "H" ($#r1_hidden :::"="::: ) (Set (Set (Var "H1")) ($#k12_zf_lang :::"<=>"::: ) it))); end; :: deftheorem defines :::"the_left_side_of"::: ZF_LANG:def 37 : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v10_zf_lang :::"biconditional"::: ) )) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k27_zf_lang :::"the_left_side_of"::: ) (Set (Var "H")))) "iff" (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b2")) ($#k12_zf_lang :::"<=>"::: ) (Set (Var "H1"))))) ")" ))); :: deftheorem defines :::"the_right_side_of"::: ZF_LANG:def 38 : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v10_zf_lang :::"biconditional"::: ) )) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k28_zf_lang :::"the_right_side_of"::: ) (Set (Var "H")))) "iff" (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "H1")) ($#k12_zf_lang :::"<=>"::: ) (Set (Var "b2"))))) ")" ))); theorem :: ZF_LANG:48 (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v10_zf_lang :::"biconditional"::: ) )) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k27_zf_lang :::"the_left_side_of"::: ) (Set (Var "H"))))) "implies" (Bool "ex" (Set (Var "G")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k12_zf_lang :::"<=>"::: ) (Set (Var "G"))))) ")" & "(" (Bool (Bool "ex" (Set (Var "G")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k12_zf_lang :::"<=>"::: ) (Set (Var "G")))))) "implies" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k27_zf_lang :::"the_left_side_of"::: ) (Set (Var "H")))) ")" & "(" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k28_zf_lang :::"the_right_side_of"::: ) (Set (Var "H"))))) "implies" (Bool "ex" (Set (Var "G")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k12_zf_lang :::"<=>"::: ) (Set (Var "F"))))) ")" & "(" (Bool (Bool "ex" (Set (Var "G")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k12_zf_lang :::"<=>"::: ) (Set (Var "F")))))) "implies" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k28_zf_lang :::"the_right_side_of"::: ) (Set (Var "H")))) ")" ")" )) ; theorem :: ZF_LANG:49 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v10_zf_lang :::"biconditional"::: ) )) "holds" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k27_zf_lang :::"the_left_side_of"::: ) (Set (Var "H")) ")" ) ($#k12_zf_lang :::"<=>"::: ) (Set "(" ($#k28_zf_lang :::"the_right_side_of"::: ) (Set (Var "H")) ")" )))) ; definitionlet "H", "F" be ($#m2_finseq_1 :::"ZF-formula":::); pred "H" :::"is_immediate_constituent_of"::: "F" means :: ZF_LANG:def 39 (Bool "(" (Bool "F" ($#r1_hidden :::"="::: ) (Set ($#k6_zf_lang :::"'not'"::: ) "H")) "or" (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool "(" (Bool "F" ($#r1_hidden :::"="::: ) (Set "H" ($#k7_zf_lang :::"'&'"::: ) (Set (Var "H1")))) "or" (Bool "F" ($#r1_hidden :::"="::: ) (Set (Set (Var "H1")) ($#k7_zf_lang :::"'&'"::: ) "H")) ")" )) "or" (Bool "ex" (Set (Var "x")) "being" ($#m2_subset_1 :::"Variable":::) "st" (Bool "F" ($#r1_hidden :::"="::: ) (Set ($#k8_zf_lang :::"All"::: ) "(" (Set (Var "x")) "," "H" ")" ))) ")" ); end; :: deftheorem defines :::"is_immediate_constituent_of"::: ZF_LANG:def 39 : (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" (Bool (Set (Var "H")) ($#r1_zf_lang :::"is_immediate_constituent_of"::: ) (Set (Var "F"))) "iff" (Bool "(" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k6_zf_lang :::"'not'"::: ) (Set (Var "H")))) "or" (Bool "ex" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool "(" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k7_zf_lang :::"'&'"::: ) (Set (Var "H1")))) "or" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Set (Var "H1")) ($#k7_zf_lang :::"'&'"::: ) (Set (Var "H")))) ")" )) "or" (Bool "ex" (Set (Var "x")) "being" ($#m2_subset_1 :::"Variable":::) "st" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k8_zf_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "H")) ")" ))) ")" ) ")" )); theorem :: ZF_LANG:50 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool (Bool "not" (Set (Var "H")) ($#r1_zf_lang :::"is_immediate_constituent_of"::: ) (Set (Set (Var "x")) ($#k4_zf_lang :::"'='"::: ) (Set (Var "y"))))))) ; theorem :: ZF_LANG:51 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool (Bool "not" (Set (Var "H")) ($#r1_zf_lang :::"is_immediate_constituent_of"::: ) (Set (Set (Var "x")) ($#k5_zf_lang :::"'in'"::: ) (Set (Var "y"))))))) ; theorem :: ZF_LANG:52 (Bool "for" (Set (Var "F")) "," (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r1_zf_lang :::"is_immediate_constituent_of"::: ) (Set ($#k6_zf_lang :::"'not'"::: ) (Set (Var "H")))) "iff" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Var "H"))) ")" )) ; theorem :: ZF_LANG:53 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r1_zf_lang :::"is_immediate_constituent_of"::: ) (Set (Set (Var "G")) ($#k7_zf_lang :::"'&'"::: ) (Set (Var "H")))) "iff" (Bool "(" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Var "G"))) "or" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Var "H"))) ")" ) ")" )) ; theorem :: ZF_LANG:54 (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Variable":::) (Bool "for" (Set (Var "F")) "," (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r1_zf_lang :::"is_immediate_constituent_of"::: ) (Set ($#k8_zf_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "H")) ")" )) "iff" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Var "H"))) ")" ))) ; theorem :: ZF_LANG:55 (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v7_zf_lang :::"atomic"::: ) )) "holds" (Bool "not" (Bool (Set (Var "F")) ($#r1_zf_lang :::"is_immediate_constituent_of"::: ) (Set (Var "H"))))) ; theorem :: ZF_LANG:56 (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v4_zf_lang :::"negative"::: ) )) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r1_zf_lang :::"is_immediate_constituent_of"::: ) (Set (Var "H"))) "iff" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k20_zf_lang :::"the_argument_of"::: ) (Set (Var "H")))) ")" )) ; theorem :: ZF_LANG:57 (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v5_zf_lang :::"conjunctive"::: ) )) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r1_zf_lang :::"is_immediate_constituent_of"::: ) (Set (Var "H"))) "iff" (Bool "(" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k21_zf_lang :::"the_left_argument_of"::: ) (Set (Var "H")))) "or" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k22_zf_lang :::"the_right_argument_of"::: ) (Set (Var "H")))) ")" ) ")" )) ; theorem :: ZF_LANG:58 (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v6_zf_lang :::"universal"::: ) )) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r1_zf_lang :::"is_immediate_constituent_of"::: ) (Set (Var "H"))) "iff" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k24_zf_lang :::"the_scope_of"::: ) (Set (Var "H")))) ")" )) ; definitionlet "H", "F" be ($#m2_finseq_1 :::"ZF-formula":::); pred "H" :::"is_subformula_of"::: "F" means :: ZF_LANG:def 40 (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "L")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) "H") & (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) "F") & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool "ex" (Set (Var "H1")) "," (Set (Var "F1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool "(" (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Var "H1"))) & (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "F1"))) & (Bool (Set (Var "H1")) ($#r1_zf_lang :::"is_immediate_constituent_of"::: ) (Set (Var "F1"))) ")" )) ")" ) ")" ))); end; :: deftheorem defines :::"is_subformula_of"::: ZF_LANG:def 40 : (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" (Bool (Set (Var "H")) ($#r2_zf_lang :::"is_subformula_of"::: ) (Set (Var "F"))) "iff" (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "L")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "H"))) & (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "F"))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool "ex" (Set (Var "H1")) "," (Set (Var "F1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool "(" (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Var "H1"))) & (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "F1"))) & (Bool (Set (Var "H1")) ($#r1_zf_lang :::"is_immediate_constituent_of"::: ) (Set (Var "F1"))) ")" )) ")" ) ")" ))) ")" )); theorem :: ZF_LANG:59 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool (Set (Var "H")) ($#r2_zf_lang :::"is_subformula_of"::: ) (Set (Var "H")))) ; definitionlet "H", "F" be ($#m2_finseq_1 :::"ZF-formula":::); pred "H" :::"is_proper_subformula_of"::: "F" means :: ZF_LANG:def 41 (Bool "(" (Bool "H" ($#r2_zf_lang :::"is_subformula_of"::: ) "F") & (Bool "H" ($#r1_hidden :::"<>"::: ) "F") ")" ); end; :: deftheorem defines :::"is_proper_subformula_of"::: ZF_LANG:def 41 : (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" (Bool (Set (Var "H")) ($#r3_zf_lang :::"is_proper_subformula_of"::: ) (Set (Var "F"))) "iff" (Bool "(" (Bool (Set (Var "H")) ($#r2_zf_lang :::"is_subformula_of"::: ) (Set (Var "F"))) & (Bool (Set (Var "H")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) ")" ) ")" )); theorem :: ZF_LANG:60 (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) ($#r1_zf_lang :::"is_immediate_constituent_of"::: ) (Set (Var "F")))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "H"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))))) ; theorem :: ZF_LANG:61 (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) ($#r1_zf_lang :::"is_immediate_constituent_of"::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "H")) ($#r3_zf_lang :::"is_proper_subformula_of"::: ) (Set (Var "F")))) ; theorem :: ZF_LANG:62 (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) ($#r3_zf_lang :::"is_proper_subformula_of"::: ) (Set (Var "F")))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "H"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))))) ; theorem :: ZF_LANG:63 (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) ($#r3_zf_lang :::"is_proper_subformula_of"::: ) (Set (Var "F")))) "holds" (Bool "ex" (Set (Var "G")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Set (Var "G")) ($#r1_zf_lang :::"is_immediate_constituent_of"::: ) (Set (Var "F"))))) ; theorem :: ZF_LANG:64 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "F")) ($#r3_zf_lang :::"is_proper_subformula_of"::: ) (Set (Var "G"))) & (Bool (Set (Var "G")) ($#r3_zf_lang :::"is_proper_subformula_of"::: ) (Set (Var "H")))) "holds" (Bool (Set (Var "F")) ($#r3_zf_lang :::"is_proper_subformula_of"::: ) (Set (Var "H")))) ; theorem :: ZF_LANG:65 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "F")) ($#r2_zf_lang :::"is_subformula_of"::: ) (Set (Var "G"))) & (Bool (Set (Var "G")) ($#r2_zf_lang :::"is_subformula_of"::: ) (Set (Var "H")))) "holds" (Bool (Set (Var "F")) ($#r2_zf_lang :::"is_subformula_of"::: ) (Set (Var "H")))) ; theorem :: ZF_LANG:66 (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "G")) ($#r2_zf_lang :::"is_subformula_of"::: ) (Set (Var "H"))) & (Bool (Set (Var "H")) ($#r2_zf_lang :::"is_subformula_of"::: ) (Set (Var "G")))) "holds" (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set (Var "H")))) ; theorem :: ZF_LANG:67 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool (Bool "not" (Set (Var "F")) ($#r3_zf_lang :::"is_proper_subformula_of"::: ) (Set (Set (Var "x")) ($#k4_zf_lang :::"'='"::: ) (Set (Var "y"))))))) ; theorem :: ZF_LANG:68 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool (Bool "not" (Set (Var "F")) ($#r3_zf_lang :::"is_proper_subformula_of"::: ) (Set (Set (Var "x")) ($#k5_zf_lang :::"'in'"::: ) (Set (Var "y"))))))) ; theorem :: ZF_LANG:69 (Bool "for" (Set (Var "F")) "," (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "F")) ($#r3_zf_lang :::"is_proper_subformula_of"::: ) (Set ($#k6_zf_lang :::"'not'"::: ) (Set (Var "H"))))) "holds" (Bool (Set (Var "F")) ($#r2_zf_lang :::"is_subformula_of"::: ) (Set (Var "H")))) ; theorem :: ZF_LANG:70 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" "not" (Bool (Set (Var "F")) ($#r3_zf_lang :::"is_proper_subformula_of"::: ) (Set (Set (Var "G")) ($#k7_zf_lang :::"'&'"::: ) (Set (Var "H")))) "or" (Bool (Set (Var "F")) ($#r2_zf_lang :::"is_subformula_of"::: ) (Set (Var "G"))) "or" (Bool (Set (Var "F")) ($#r2_zf_lang :::"is_subformula_of"::: ) (Set (Var "H"))) ")" )) ; theorem :: ZF_LANG:71 (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Variable":::) (Bool "for" (Set (Var "F")) "," (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "F")) ($#r3_zf_lang :::"is_proper_subformula_of"::: ) (Set ($#k8_zf_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "H")) ")" ))) "holds" (Bool (Set (Var "F")) ($#r2_zf_lang :::"is_subformula_of"::: ) (Set (Var "H"))))) ; theorem :: ZF_LANG:72 (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v7_zf_lang :::"atomic"::: ) )) "holds" (Bool "not" (Bool (Set (Var "F")) ($#r3_zf_lang :::"is_proper_subformula_of"::: ) (Set (Var "H"))))) ; theorem :: ZF_LANG:73 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v4_zf_lang :::"negative"::: ) )) "holds" (Bool (Set ($#k20_zf_lang :::"the_argument_of"::: ) (Set (Var "H"))) ($#r3_zf_lang :::"is_proper_subformula_of"::: ) (Set (Var "H")))) ; theorem :: ZF_LANG:74 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v5_zf_lang :::"conjunctive"::: ) )) "holds" (Bool "(" (Bool (Set ($#k21_zf_lang :::"the_left_argument_of"::: ) (Set (Var "H"))) ($#r3_zf_lang :::"is_proper_subformula_of"::: ) (Set (Var "H"))) & (Bool (Set ($#k22_zf_lang :::"the_right_argument_of"::: ) (Set (Var "H"))) ($#r3_zf_lang :::"is_proper_subformula_of"::: ) (Set (Var "H"))) ")" )) ; theorem :: ZF_LANG:75 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v6_zf_lang :::"universal"::: ) )) "holds" (Bool (Set ($#k24_zf_lang :::"the_scope_of"::: ) (Set (Var "H"))) ($#r3_zf_lang :::"is_proper_subformula_of"::: ) (Set (Var "H")))) ; theorem :: ZF_LANG:76 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" (Bool (Set (Var "H")) ($#r2_zf_lang :::"is_subformula_of"::: ) (Set (Set (Var "x")) ($#k4_zf_lang :::"'='"::: ) (Set (Var "y")))) "iff" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k4_zf_lang :::"'='"::: ) (Set (Var "y")))) ")" ))) ; theorem :: ZF_LANG:77 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" (Bool (Set (Var "H")) ($#r2_zf_lang :::"is_subformula_of"::: ) (Set (Set (Var "x")) ($#k5_zf_lang :::"'in'"::: ) (Set (Var "y")))) "iff" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k5_zf_lang :::"'in'"::: ) (Set (Var "y")))) ")" ))) ; definitionlet "H" be ($#m2_finseq_1 :::"ZF-formula":::); func :::"Subformulae"::: "H" -> ($#m1_hidden :::"set"::: ) means :: ZF_LANG:def 42 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool "(" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Var "F")) ($#r2_zf_lang :::"is_subformula_of"::: ) "H") ")" )) ")" )); end; :: deftheorem defines :::"Subformulae"::: ZF_LANG:def 42 : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k29_zf_lang :::"Subformulae"::: ) (Set (Var "H")))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool "(" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Var "F")) ($#r2_zf_lang :::"is_subformula_of"::: ) (Set (Var "H"))) ")" )) ")" )) ")" ))); theorem :: ZF_LANG:78 (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "G")) ($#r2_hidden :::"in"::: ) (Set ($#k29_zf_lang :::"Subformulae"::: ) (Set (Var "H"))))) "holds" (Bool (Set (Var "G")) ($#r2_zf_lang :::"is_subformula_of"::: ) (Set (Var "H")))) ; theorem :: ZF_LANG:79 (Bool "for" (Set (Var "F")) "," (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "F")) ($#r2_zf_lang :::"is_subformula_of"::: ) (Set (Var "H")))) "holds" (Bool (Set ($#k29_zf_lang :::"Subformulae"::: ) (Set (Var "F"))) ($#r1_tarski :::"c="::: ) (Set ($#k29_zf_lang :::"Subformulae"::: ) (Set (Var "H"))))) ; theorem :: ZF_LANG:80 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) "holds" (Bool (Set ($#k29_zf_lang :::"Subformulae"::: ) (Set "(" (Set (Var "x")) ($#k4_zf_lang :::"'='"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "x")) ($#k4_zf_lang :::"'='"::: ) (Set (Var "y")) ")" ) ($#k1_tarski :::"}"::: ) ))) ; theorem :: ZF_LANG:81 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) "holds" (Bool (Set ($#k29_zf_lang :::"Subformulae"::: ) (Set "(" (Set (Var "x")) ($#k5_zf_lang :::"'in'"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "x")) ($#k5_zf_lang :::"'in'"::: ) (Set (Var "y")) ")" ) ($#k1_tarski :::"}"::: ) ))) ; theorem :: ZF_LANG:82 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool (Set ($#k29_zf_lang :::"Subformulae"::: ) (Set "(" ($#k6_zf_lang :::"'not'"::: ) (Set (Var "H")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k29_zf_lang :::"Subformulae"::: ) (Set (Var "H")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k6_zf_lang :::"'not'"::: ) (Set (Var "H")) ")" ) ($#k1_tarski :::"}"::: ) )))) ; theorem :: ZF_LANG:83 (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool (Set ($#k29_zf_lang :::"Subformulae"::: ) (Set "(" (Set (Var "H")) ($#k7_zf_lang :::"'&'"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k29_zf_lang :::"Subformulae"::: ) (Set (Var "H")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k29_zf_lang :::"Subformulae"::: ) (Set (Var "F")) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "H")) ($#k7_zf_lang :::"'&'"::: ) (Set (Var "F")) ")" ) ($#k1_tarski :::"}"::: ) )))) ; theorem :: ZF_LANG:84 (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Variable":::) (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool (Set ($#k29_zf_lang :::"Subformulae"::: ) (Set "(" ($#k8_zf_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "H")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k29_zf_lang :::"Subformulae"::: ) (Set (Var "H")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k8_zf_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "H")) ")" ")" ) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: ZF_LANG:85 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" (Bool (Set (Var "H")) "is" ($#v7_zf_lang :::"atomic"::: ) ) "iff" (Bool (Set ($#k29_zf_lang :::"Subformulae"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "H")) ($#k1_tarski :::"}"::: ) )) ")" )) ; theorem :: ZF_LANG:86 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v4_zf_lang :::"negative"::: ) )) "holds" (Bool (Set ($#k29_zf_lang :::"Subformulae"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k29_zf_lang :::"Subformulae"::: ) (Set "(" ($#k20_zf_lang :::"the_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "H")) ($#k1_tarski :::"}"::: ) )))) ; theorem :: ZF_LANG:87 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v5_zf_lang :::"conjunctive"::: ) )) "holds" (Bool (Set ($#k29_zf_lang :::"Subformulae"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k29_zf_lang :::"Subformulae"::: ) (Set "(" ($#k21_zf_lang :::"the_left_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k29_zf_lang :::"Subformulae"::: ) (Set "(" ($#k22_zf_lang :::"the_right_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "H")) ($#k1_tarski :::"}"::: ) )))) ; theorem :: ZF_LANG:88 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v6_zf_lang :::"universal"::: ) )) "holds" (Bool (Set ($#k29_zf_lang :::"Subformulae"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k29_zf_lang :::"Subformulae"::: ) (Set "(" ($#k24_zf_lang :::"the_scope_of"::: ) (Set (Var "H")) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "H")) ($#k1_tarski :::"}"::: ) )))) ; theorem :: ZF_LANG:89 (Bool "for" (Set (Var "H")) "," (Set (Var "G")) "," (Set (Var "F")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool "(" (Bool (Set (Var "H")) ($#r1_zf_lang :::"is_immediate_constituent_of"::: ) (Set (Var "G"))) "or" (Bool (Set (Var "H")) ($#r3_zf_lang :::"is_proper_subformula_of"::: ) (Set (Var "G"))) "or" (Bool (Set (Var "H")) ($#r2_zf_lang :::"is_subformula_of"::: ) (Set (Var "G"))) ")" ) & (Bool (Set (Var "G")) ($#r2_hidden :::"in"::: ) (Set ($#k29_zf_lang :::"Subformulae"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Var "H")) ($#r2_hidden :::"in"::: ) (Set ($#k29_zf_lang :::"Subformulae"::: ) (Set (Var "F"))))) ; scheme :: ZF_LANG:sch 1 ZFInd{ P1[ ($#m2_finseq_1 :::"ZF-formula":::)] } : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool P1[(Set (Var "H"))])) provided (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v7_zf_lang :::"atomic"::: ) )) "holds" (Bool P1[(Set (Var "H"))])) and (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v4_zf_lang :::"negative"::: ) ) & (Bool P1[(Set ($#k20_zf_lang :::"the_argument_of"::: ) (Set (Var "H")))])) "holds" (Bool P1[(Set (Var "H"))])) and (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v5_zf_lang :::"conjunctive"::: ) ) & (Bool P1[(Set ($#k21_zf_lang :::"the_left_argument_of"::: ) (Set (Var "H")))]) & (Bool P1[(Set ($#k22_zf_lang :::"the_right_argument_of"::: ) (Set (Var "H")))])) "holds" (Bool P1[(Set (Var "H"))])) and (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) "is" ($#v6_zf_lang :::"universal"::: ) ) & (Bool P1[(Set ($#k24_zf_lang :::"the_scope_of"::: ) (Set (Var "H")))])) "holds" (Bool P1[(Set (Var "H"))])) proof end; scheme :: ZF_LANG:sch 2 ZFCompInd{ P1[ ($#m2_finseq_1 :::"ZF-formula":::)] } : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool P1[(Set (Var "H"))])) provided (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool "(" "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "F")) ($#r3_zf_lang :::"is_proper_subformula_of"::: ) (Set (Var "H")))) "holds" (Bool P1[(Set (Var "F"))]) ")" )) "holds" (Bool P1[(Set (Var "H"))])) proof end;