:: QC_LANG2 semantic presentation begin theorem :: QC_LANG2:1 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set "(" ($#k13_qc_lang1 :::"'not'"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "p"))))) ; theorem :: QC_LANG2:2 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "p1")) "," (Set (Var "q1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Set (Var "p")) ($#k14_qc_lang1 :::"'&'"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p1")) ($#k14_qc_lang1 :::"'&'"::: ) (Set (Var "q1"))))) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "p1"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Var "q1"))) ")" ))) ; theorem :: QC_LANG2:3 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "p")) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) )) "holds" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k19_qc_lang1 :::"the_left_argument_of"::: ) (Set (Var "p")) ")" ) ($#k14_qc_lang1 :::"'&'"::: ) (Set "(" ($#k20_qc_lang1 :::"the_right_argument_of"::: ) (Set (Var "p")) ")" ))))) ; theorem :: QC_LANG2:4 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set ($#k19_qc_lang1 :::"the_left_argument_of"::: ) (Set "(" (Set (Var "p")) ($#k14_qc_lang1 :::"'&'"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set ($#k20_qc_lang1 :::"the_right_argument_of"::: ) (Set "(" (Set (Var "p")) ($#k14_qc_lang1 :::"'&'"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "q"))) ")" ))) ; theorem :: QC_LANG2:5 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set ($#k15_qc_lang1 :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k15_qc_lang1 :::"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"))) ")" )))) ; theorem :: QC_LANG2:6 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "p")) "is" ($#v5_qc_lang1 :::"universal"::: ) )) "holds" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k15_qc_lang1 :::"All"::: ) "(" (Set "(" ($#k21_qc_lang1 :::"bound_in"::: ) (Set (Var "p")) ")" ) "," (Set "(" ($#k22_qc_lang1 :::"the_scope_of"::: ) (Set (Var "p")) ")" ) ")" )))) ; theorem :: QC_LANG2:7 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set ($#k21_qc_lang1 :::"bound_in"::: ) (Set "(" ($#k15_qc_lang1 :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set ($#k22_qc_lang1 :::"the_scope_of"::: ) (Set "(" ($#k15_qc_lang1 :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "p"))) ")" )))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; func :::"FALSUM"::: "A" -> ($#m1_subset_1 :::"QC-formula":::) "of" "A" equals :: QC_LANG2:def 1 (Set ($#k13_qc_lang1 :::"'not'"::: ) (Set "(" ($#k12_qc_lang1 :::"VERUM"::: ) "A" ")" )); let "p", "q" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Const "A"))); func "p" :::"=>"::: "q" -> ($#m1_subset_1 :::"QC-formula":::) "of" "A" equals :: QC_LANG2:def 2 (Set ($#k13_qc_lang1 :::"'not'"::: ) (Set "(" "p" ($#k14_qc_lang1 :::"'&'"::: ) (Set "(" ($#k13_qc_lang1 :::"'not'"::: ) "q" ")" ) ")" )); func "p" :::"'or'"::: "q" -> ($#m1_subset_1 :::"QC-formula":::) "of" "A" equals :: QC_LANG2:def 3 (Set ($#k13_qc_lang1 :::"'not'"::: ) (Set "(" (Set "(" ($#k13_qc_lang1 :::"'not'"::: ) "p" ")" ) ($#k14_qc_lang1 :::"'&'"::: ) (Set "(" ($#k13_qc_lang1 :::"'not'"::: ) "q" ")" ) ")" )); end; :: deftheorem defines :::"FALSUM"::: QC_LANG2:def 1 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) "holds" (Bool (Set ($#k1_qc_lang2 :::"FALSUM"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k13_qc_lang1 :::"'not'"::: ) (Set "(" ($#k12_qc_lang1 :::"VERUM"::: ) (Set (Var "A")) ")" )))); :: deftheorem defines :::"=>"::: QC_LANG2:def 2 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set (Set (Var "p")) ($#k2_qc_lang2 :::"=>"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k13_qc_lang1 :::"'not'"::: ) (Set "(" (Set (Var "p")) ($#k14_qc_lang1 :::"'&'"::: ) (Set "(" ($#k13_qc_lang1 :::"'not'"::: ) (Set (Var "q")) ")" ) ")" ))))); :: deftheorem defines :::"'or'"::: QC_LANG2:def 3 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set (Set (Var "p")) ($#k3_qc_lang2 :::"'or'"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k13_qc_lang1 :::"'not'"::: ) (Set "(" (Set "(" ($#k13_qc_lang1 :::"'not'"::: ) (Set (Var "p")) ")" ) ($#k14_qc_lang1 :::"'&'"::: ) (Set "(" ($#k13_qc_lang1 :::"'not'"::: ) (Set (Var "q")) ")" ) ")" ))))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "p", "q" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Const "A"))); func "p" :::"<=>"::: "q" -> ($#m1_subset_1 :::"QC-formula":::) "of" "A" equals :: QC_LANG2:def 4 (Set (Set "(" "p" ($#k2_qc_lang2 :::"=>"::: ) "q" ")" ) ($#k14_qc_lang1 :::"'&'"::: ) (Set "(" "q" ($#k2_qc_lang2 :::"=>"::: ) "p" ")" )); end; :: deftheorem defines :::"<=>"::: QC_LANG2:def 4 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set (Set (Var "p")) ($#k4_qc_lang2 :::"<=>"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k2_qc_lang2 :::"=>"::: ) (Set (Var "q")) ")" ) ($#k14_qc_lang1 :::"'&'"::: ) (Set "(" (Set (Var "q")) ($#k2_qc_lang2 :::"=>"::: ) (Set (Var "p")) ")" ))))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "x" be ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Const "A")); let "p" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Const "A"))); func :::"Ex"::: "(" "x" "," "p" ")" -> ($#m1_subset_1 :::"QC-formula":::) "of" "A" equals :: QC_LANG2:def 5 (Set ($#k13_qc_lang1 :::"'not'"::: ) (Set "(" ($#k15_qc_lang1 :::"All"::: ) "(" "x" "," (Set "(" ($#k13_qc_lang1 :::"'not'"::: ) "p" ")" ) ")" ")" )); end; :: deftheorem defines :::"Ex"::: QC_LANG2:def 5 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set ($#k5_qc_lang2 :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k13_qc_lang1 :::"'not'"::: ) (Set "(" ($#k15_qc_lang1 :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k13_qc_lang1 :::"'not'"::: ) (Set (Var "p")) ")" ) ")" ")" )))))); theorem :: QC_LANG2:8 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) "holds" (Bool "(" (Bool (Set ($#k1_qc_lang2 :::"FALSUM"::: ) (Set (Var "A"))) "is" ($#v3_qc_lang1 :::"negative"::: ) ) & (Bool (Set ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set "(" ($#k1_qc_lang2 :::"FALSUM"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k12_qc_lang1 :::"VERUM"::: ) (Set (Var "A")))) ")" )) ; theorem :: QC_LANG2:9 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set (Set (Var "p")) ($#k3_qc_lang2 :::"'or'"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k13_qc_lang1 :::"'not'"::: ) (Set (Var "p")) ")" ) ($#k2_qc_lang2 :::"=>"::: ) (Set (Var "q")))))) ; theorem :: QC_LANG2:10 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "p1")) "," (Set (Var "q1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Set (Var "p")) ($#k3_qc_lang2 :::"'or'"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p1")) ($#k3_qc_lang2 :::"'or'"::: ) (Set (Var "q1"))))) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "p1"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Var "q1"))) ")" ))) ; theorem :: QC_LANG2:11 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "p1")) "," (Set (Var "q1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Set (Var "p")) ($#k2_qc_lang2 :::"=>"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p1")) ($#k2_qc_lang2 :::"=>"::: ) (Set (Var "q1"))))) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "p1"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Var "q1"))) ")" ))) ; theorem :: QC_LANG2:12 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "p1")) "," (Set (Var "q1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Set (Var "p")) ($#k4_qc_lang2 :::"<=>"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p1")) ($#k4_qc_lang2 :::"<=>"::: ) (Set (Var "q1"))))) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "p1"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Var "q1"))) ")" ))) ; theorem :: QC_LANG2:13 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set ($#k5_qc_lang2 :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_qc_lang2 :::"Ex"::: ) "(" (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"))) ")" )))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "x", "y" be ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Const "A")); let "p" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Const "A"))); func :::"All"::: "(" "x" "," "y" "," "p" ")" -> ($#m1_subset_1 :::"QC-formula":::) "of" "A" equals :: QC_LANG2:def 6 (Set ($#k15_qc_lang1 :::"All"::: ) "(" "x" "," (Set "(" ($#k15_qc_lang1 :::"All"::: ) "(" "y" "," "p" ")" ")" ) ")" ); func :::"Ex"::: "(" "x" "," "y" "," "p" ")" -> ($#m1_subset_1 :::"QC-formula":::) "of" "A" equals :: QC_LANG2:def 7 (Set ($#k5_qc_lang2 :::"Ex"::: ) "(" "x" "," (Set "(" ($#k5_qc_lang2 :::"Ex"::: ) "(" "y" "," "p" ")" ")" ) ")" ); end; :: deftheorem defines :::"All"::: QC_LANG2:def 6 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set ($#k6_qc_lang2 :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k15_qc_lang1 :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k15_qc_lang1 :::"All"::: ) "(" (Set (Var "y")) "," (Set (Var "p")) ")" ")" ) ")" ))))); :: deftheorem defines :::"Ex"::: QC_LANG2:def 7 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set ($#k7_qc_lang2 :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_qc_lang2 :::"Ex"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k5_qc_lang2 :::"Ex"::: ) "(" (Set (Var "y")) "," (Set (Var "p")) ")" ")" ) ")" ))))); theorem :: QC_LANG2:14 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set ($#k6_qc_lang2 :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k15_qc_lang1 :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k15_qc_lang1 :::"All"::: ) "(" (Set (Var "y")) "," (Set (Var "p")) ")" ")" ) ")" )) & (Bool (Set ($#k7_qc_lang2 :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_qc_lang2 :::"Ex"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k5_qc_lang2 :::"Ex"::: ) "(" (Set (Var "y")) "," (Set (Var "p")) ")" ")" ) ")" )) ")" )))) ; theorem :: QC_LANG2:15 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#k6_qc_lang2 :::"All"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "p1")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_qc_lang2 :::"All"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "p2")) ")" ))) "holds" (Bool "(" (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) & (Bool (Set (Var "y1")) ($#r1_hidden :::"="::: ) (Set (Var "y2"))) & (Bool (Set (Var "p1")) ($#r1_hidden :::"="::: ) (Set (Var "p2"))) ")" )))) ; theorem :: QC_LANG2:16 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set ($#k6_qc_lang2 :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k15_qc_lang1 :::"All"::: ) "(" (Set (Var "z")) "," (Set (Var "q")) ")" ))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "z"))) & (Bool (Set ($#k15_qc_lang1 :::"All"::: ) "(" (Set (Var "y")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "q"))) ")" )))) ; theorem :: QC_LANG2:17 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#k7_qc_lang2 :::"Ex"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "p1")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_qc_lang2 :::"Ex"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "p2")) ")" ))) "holds" (Bool "(" (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) & (Bool (Set (Var "y1")) ($#r1_hidden :::"="::: ) (Set (Var "y2"))) & (Bool (Set (Var "p1")) ($#r1_hidden :::"="::: ) (Set (Var "p2"))) ")" )))) ; theorem :: QC_LANG2:18 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set ($#k7_qc_lang2 :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_qc_lang2 :::"Ex"::: ) "(" (Set (Var "z")) "," (Set (Var "q")) ")" ))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "z"))) & (Bool (Set ($#k5_qc_lang2 :::"Ex"::: ) "(" (Set (Var "y")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "q"))) ")" )))) ; theorem :: QC_LANG2:19 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set ($#k6_qc_lang2 :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "p")) ")" ) "is" ($#v5_qc_lang1 :::"universal"::: ) ) & (Bool (Set ($#k21_qc_lang1 :::"bound_in"::: ) (Set "(" ($#k6_qc_lang2 :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "p")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set ($#k22_qc_lang1 :::"the_scope_of"::: ) (Set "(" ($#k6_qc_lang2 :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "p")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k15_qc_lang1 :::"All"::: ) "(" (Set (Var "y")) "," (Set (Var "p")) ")" )) ")" )))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "x", "y", "z" be ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Const "A")); let "p" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Const "A"))); func :::"All"::: "(" "x" "," "y" "," "z" "," "p" ")" -> ($#m1_subset_1 :::"QC-formula":::) "of" "A" equals :: QC_LANG2:def 8 (Set ($#k15_qc_lang1 :::"All"::: ) "(" "x" "," (Set "(" ($#k6_qc_lang2 :::"All"::: ) "(" "y" "," "z" "," "p" ")" ")" ) ")" ); func :::"Ex"::: "(" "x" "," "y" "," "z" "," "p" ")" -> ($#m1_subset_1 :::"QC-formula":::) "of" "A" equals :: QC_LANG2:def 9 (Set ($#k5_qc_lang2 :::"Ex"::: ) "(" "x" "," (Set "(" ($#k7_qc_lang2 :::"Ex"::: ) "(" "y" "," "z" "," "p" ")" ")" ) ")" ); end; :: deftheorem defines :::"All"::: QC_LANG2:def 8 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set ($#k8_qc_lang2 :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k15_qc_lang1 :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k6_qc_lang2 :::"All"::: ) "(" (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "p")) ")" ")" ) ")" ))))); :: deftheorem defines :::"Ex"::: QC_LANG2:def 9 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set ($#k9_qc_lang2 :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_qc_lang2 :::"Ex"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k7_qc_lang2 :::"Ex"::: ) "(" (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "p")) ")" ")" ) ")" ))))); theorem :: QC_LANG2:20 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set ($#k8_qc_lang2 :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k15_qc_lang1 :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k6_qc_lang2 :::"All"::: ) "(" (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "p")) ")" ")" ) ")" )) & (Bool (Set ($#k9_qc_lang2 :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_qc_lang2 :::"Ex"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k7_qc_lang2 :::"Ex"::: ) "(" (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "p")) ")" ")" ) ")" )) ")" )))) ; theorem :: QC_LANG2:21 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#k8_qc_lang2 :::"All"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "z1")) "," (Set (Var "p1")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_qc_lang2 :::"All"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "z2")) "," (Set (Var "p2")) ")" ))) "holds" (Bool "(" (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) & (Bool (Set (Var "y1")) ($#r1_hidden :::"="::: ) (Set (Var "y2"))) & (Bool (Set (Var "z1")) ($#r1_hidden :::"="::: ) (Set (Var "z2"))) & (Bool (Set (Var "p1")) ($#r1_hidden :::"="::: ) (Set (Var "p2"))) ")" )))) ; theorem :: QC_LANG2:22 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "t")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#k8_qc_lang2 :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k15_qc_lang1 :::"All"::: ) "(" (Set (Var "t")) "," (Set (Var "q")) ")" ))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "t"))) & (Bool (Set ($#k6_qc_lang2 :::"All"::: ) "(" (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "q"))) ")" ))))) ; theorem :: QC_LANG2:23 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "t")) "," (Set (Var "s")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#k8_qc_lang2 :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_qc_lang2 :::"All"::: ) "(" (Set (Var "t")) "," (Set (Var "s")) "," (Set (Var "q")) ")" ))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "t"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "s"))) & (Bool (Set ($#k15_qc_lang1 :::"All"::: ) "(" (Set (Var "z")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "q"))) ")" ))))) ; theorem :: QC_LANG2:24 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#k9_qc_lang2 :::"Ex"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "z1")) "," (Set (Var "p1")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_qc_lang2 :::"Ex"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "z2")) "," (Set (Var "p2")) ")" ))) "holds" (Bool "(" (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) & (Bool (Set (Var "y1")) ($#r1_hidden :::"="::: ) (Set (Var "y2"))) & (Bool (Set (Var "z1")) ($#r1_hidden :::"="::: ) (Set (Var "z2"))) & (Bool (Set (Var "p1")) ($#r1_hidden :::"="::: ) (Set (Var "p2"))) ")" )))) ; theorem :: QC_LANG2:25 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "t")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#k9_qc_lang2 :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_qc_lang2 :::"Ex"::: ) "(" (Set (Var "t")) "," (Set (Var "q")) ")" ))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "t"))) & (Bool (Set ($#k7_qc_lang2 :::"Ex"::: ) "(" (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "q"))) ")" ))))) ; theorem :: QC_LANG2:26 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "t")) "," (Set (Var "s")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#k9_qc_lang2 :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_qc_lang2 :::"Ex"::: ) "(" (Set (Var "t")) "," (Set (Var "s")) "," (Set (Var "q")) ")" ))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "t"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "s"))) & (Bool (Set ($#k5_qc_lang2 :::"Ex"::: ) "(" (Set (Var "z")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "q"))) ")" ))))) ; theorem :: QC_LANG2:27 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set ($#k8_qc_lang2 :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "p")) ")" ) "is" ($#v5_qc_lang1 :::"universal"::: ) ) & (Bool (Set ($#k21_qc_lang1 :::"bound_in"::: ) (Set "(" ($#k8_qc_lang2 :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "p")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set ($#k22_qc_lang1 :::"the_scope_of"::: ) (Set "(" ($#k8_qc_lang2 :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "p")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_qc_lang2 :::"All"::: ) "(" (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "p")) ")" )) ")" )))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "H" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Const "A"))); attr "H" is :::"disjunctive"::: means :: QC_LANG2:def 10 (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) "A") "st" (Bool "H" ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k3_qc_lang2 :::"'or'"::: ) (Set (Var "q"))))); attr "H" is :::"conditional"::: means :: QC_LANG2:def 11 (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) "A") "st" (Bool "H" ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k2_qc_lang2 :::"=>"::: ) (Set (Var "q"))))); attr "H" is :::"biconditional"::: means :: QC_LANG2:def 12 (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) "A") "st" (Bool "H" ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k4_qc_lang2 :::"<=>"::: ) (Set (Var "q"))))); attr "H" is :::"existential"::: means :: QC_LANG2:def 13 (Bool "ex" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" "A"(Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) "A") "st" (Bool "H" ($#r1_hidden :::"="::: ) (Set ($#k5_qc_lang2 :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" )))); end; :: deftheorem defines :::"disjunctive"::: QC_LANG2:def 10 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "H")) "is" ($#v1_qc_lang2 :::"disjunctive"::: ) ) "iff" (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k3_qc_lang2 :::"'or'"::: ) (Set (Var "q"))))) ")" ))); :: deftheorem defines :::"conditional"::: QC_LANG2:def 11 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "H")) "is" ($#v2_qc_lang2 :::"conditional"::: ) ) "iff" (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k2_qc_lang2 :::"=>"::: ) (Set (Var "q"))))) ")" ))); :: deftheorem defines :::"biconditional"::: QC_LANG2:def 12 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "H")) "is" ($#v3_qc_lang2 :::"biconditional"::: ) ) "iff" (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k4_qc_lang2 :::"<=>"::: ) (Set (Var "q"))))) ")" ))); :: deftheorem defines :::"existential"::: QC_LANG2:def 13 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "H")) "is" ($#v4_qc_lang2 :::"existential"::: ) ) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A"))(Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#k5_qc_lang2 :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" )))) ")" ))); theorem :: QC_LANG2:28 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set ($#k7_qc_lang2 :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "p")) ")" ) "is" ($#v4_qc_lang2 :::"existential"::: ) ) & (Bool (Set ($#k9_qc_lang2 :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "p")) ")" ) "is" ($#v4_qc_lang2 :::"existential"::: ) ) ")" )))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "H" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Const "A"))); func :::"the_left_disjunct_of"::: "H" -> ($#m1_subset_1 :::"QC-formula":::) "of" "A" equals :: QC_LANG2:def 14 (Set ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set "(" ($#k19_qc_lang1 :::"the_left_argument_of"::: ) (Set "(" ($#k18_qc_lang1 :::"the_argument_of"::: ) "H" ")" ) ")" )); func :::"the_right_disjunct_of"::: "H" -> ($#m1_subset_1 :::"QC-formula":::) "of" "A" equals :: QC_LANG2:def 15 (Set ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set "(" ($#k20_qc_lang1 :::"the_right_argument_of"::: ) (Set "(" ($#k18_qc_lang1 :::"the_argument_of"::: ) "H" ")" ) ")" )); func :::"the_antecedent_of"::: "H" -> ($#m1_subset_1 :::"QC-formula":::) "of" "A" equals :: QC_LANG2:def 16 (Set ($#k19_qc_lang1 :::"the_left_argument_of"::: ) (Set "(" ($#k18_qc_lang1 :::"the_argument_of"::: ) "H" ")" )); end; :: deftheorem defines :::"the_left_disjunct_of"::: QC_LANG2:def 14 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set ($#k10_qc_lang2 :::"the_left_disjunct_of"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set "(" ($#k19_qc_lang1 :::"the_left_argument_of"::: ) (Set "(" ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set (Var "H")) ")" ) ")" ))))); :: deftheorem defines :::"the_right_disjunct_of"::: QC_LANG2:def 15 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set ($#k11_qc_lang2 :::"the_right_disjunct_of"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set "(" ($#k20_qc_lang1 :::"the_right_argument_of"::: ) (Set "(" ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set (Var "H")) ")" ) ")" ))))); :: deftheorem defines :::"the_antecedent_of"::: QC_LANG2:def 16 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set ($#k12_qc_lang2 :::"the_antecedent_of"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k19_qc_lang1 :::"the_left_argument_of"::: ) (Set "(" ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set (Var "H")) ")" ))))); notationlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "H" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Const "A"))); synonym :::"the_consequent_of"::: "H" for :::"the_right_disjunct_of"::: "H"; end; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "H" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Const "A"))); func :::"the_left_side_of"::: "H" -> ($#m1_subset_1 :::"QC-formula":::) "of" "A" equals :: QC_LANG2:def 17 (Set ($#k12_qc_lang2 :::"the_antecedent_of"::: ) (Set "(" ($#k19_qc_lang1 :::"the_left_argument_of"::: ) "H" ")" )); func :::"the_right_side_of"::: "H" -> ($#m1_subset_1 :::"QC-formula":::) "of" "A" equals :: QC_LANG2:def 18 (Set ($#k11_qc_lang2 :::"the_consequent_of"::: ) (Set "(" ($#k19_qc_lang1 :::"the_left_argument_of"::: ) "H" ")" )); end; :: deftheorem defines :::"the_left_side_of"::: QC_LANG2:def 17 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set ($#k13_qc_lang2 :::"the_left_side_of"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k12_qc_lang2 :::"the_antecedent_of"::: ) (Set "(" ($#k19_qc_lang1 :::"the_left_argument_of"::: ) (Set (Var "H")) ")" ))))); :: deftheorem defines :::"the_right_side_of"::: QC_LANG2:def 18 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set ($#k14_qc_lang2 :::"the_right_side_of"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k11_qc_lang2 :::"the_consequent_of"::: ) (Set "(" ($#k19_qc_lang1 :::"the_left_argument_of"::: ) (Set (Var "H")) ")" ))))); theorem :: QC_LANG2:29 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set ($#k10_qc_lang2 :::"the_left_disjunct_of"::: ) (Set "(" (Set (Var "F")) ($#k3_qc_lang2 :::"'or'"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "F"))) & (Bool (Set ($#k11_qc_lang2 :::"the_right_disjunct_of"::: ) (Set "(" (Set (Var "F")) ($#k3_qc_lang2 :::"'or'"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "G"))) & (Bool (Set ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set "(" (Set (Var "F")) ($#k3_qc_lang2 :::"'or'"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k13_qc_lang1 :::"'not'"::: ) (Set (Var "F")) ")" ) ($#k14_qc_lang1 :::"'&'"::: ) (Set "(" ($#k13_qc_lang1 :::"'not'"::: ) (Set (Var "G")) ")" ))) ")" ))) ; theorem :: QC_LANG2:30 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set ($#k12_qc_lang2 :::"the_antecedent_of"::: ) (Set "(" (Set (Var "F")) ($#k2_qc_lang2 :::"=>"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "F"))) & (Bool (Set ($#k11_qc_lang2 :::"the_consequent_of"::: ) (Set "(" (Set (Var "F")) ($#k2_qc_lang2 :::"=>"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "G"))) & (Bool (Set ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set "(" (Set (Var "F")) ($#k2_qc_lang2 :::"=>"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k14_qc_lang1 :::"'&'"::: ) (Set "(" ($#k13_qc_lang1 :::"'not'"::: ) (Set (Var "G")) ")" ))) ")" ))) ; theorem :: QC_LANG2:31 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set ($#k13_qc_lang2 :::"the_left_side_of"::: ) (Set "(" (Set (Var "F")) ($#k4_qc_lang2 :::"<=>"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "F"))) & (Bool (Set ($#k14_qc_lang2 :::"the_right_side_of"::: ) (Set "(" (Set (Var "F")) ($#k4_qc_lang2 :::"<=>"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "G"))) & (Bool (Set ($#k19_qc_lang1 :::"the_left_argument_of"::: ) (Set "(" (Set (Var "F")) ($#k4_qc_lang2 :::"<=>"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k2_qc_lang2 :::"=>"::: ) (Set (Var "G")))) & (Bool (Set ($#k20_qc_lang1 :::"the_right_argument_of"::: ) (Set "(" (Set (Var "F")) ($#k4_qc_lang2 :::"<=>"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k2_qc_lang2 :::"=>"::: ) (Set (Var "F")))) ")" ))) ; theorem :: QC_LANG2:32 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set "(" ($#k5_qc_lang2 :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "H")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k15_qc_lang1 :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k13_qc_lang1 :::"'not'"::: ) (Set (Var "H")) ")" ) ")" ))))) ; theorem :: QC_LANG2:33 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "H")) "is" ($#v1_qc_lang2 :::"disjunctive"::: ) )) "holds" (Bool "(" (Bool (Set (Var "H")) "is" ($#v2_qc_lang2 :::"conditional"::: ) ) & (Bool (Set (Var "H")) "is" ($#v3_qc_lang1 :::"negative"::: ) ) & (Bool (Set ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set (Var "H"))) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) ) & (Bool (Set ($#k19_qc_lang1 :::"the_left_argument_of"::: ) (Set "(" ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set (Var "H")) ")" )) "is" ($#v3_qc_lang1 :::"negative"::: ) ) & (Bool (Set ($#k20_qc_lang1 :::"the_right_argument_of"::: ) (Set "(" ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set (Var "H")) ")" )) "is" ($#v3_qc_lang1 :::"negative"::: ) ) ")" ))) ; theorem :: QC_LANG2:34 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "H")) "is" ($#v2_qc_lang2 :::"conditional"::: ) )) "holds" (Bool "(" (Bool (Set (Var "H")) "is" ($#v3_qc_lang1 :::"negative"::: ) ) & (Bool (Set ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set (Var "H"))) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) ) & (Bool (Set ($#k20_qc_lang1 :::"the_right_argument_of"::: ) (Set "(" ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set (Var "H")) ")" )) "is" ($#v3_qc_lang1 :::"negative"::: ) ) ")" ))) ; theorem :: QC_LANG2:35 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "H")) "is" ($#v3_qc_lang2 :::"biconditional"::: ) )) "holds" (Bool "(" (Bool (Set (Var "H")) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) ) & (Bool (Set ($#k19_qc_lang1 :::"the_left_argument_of"::: ) (Set (Var "H"))) "is" ($#v2_qc_lang2 :::"conditional"::: ) ) & (Bool (Set ($#k20_qc_lang1 :::"the_right_argument_of"::: ) (Set (Var "H"))) "is" ($#v2_qc_lang2 :::"conditional"::: ) ) ")" ))) ; theorem :: QC_LANG2:36 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "H")) "is" ($#v4_qc_lang2 :::"existential"::: ) )) "holds" (Bool "(" (Bool (Set (Var "H")) "is" ($#v3_qc_lang1 :::"negative"::: ) ) & (Bool (Set ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set (Var "H"))) "is" ($#v5_qc_lang1 :::"universal"::: ) ) & (Bool (Set ($#k22_qc_lang1 :::"the_scope_of"::: ) (Set "(" ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set (Var "H")) ")" )) "is" ($#v3_qc_lang1 :::"negative"::: ) ) ")" ))) ; theorem :: QC_LANG2:37 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "H")) "is" ($#v1_qc_lang2 :::"disjunctive"::: ) )) "holds" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_qc_lang2 :::"the_left_disjunct_of"::: ) (Set (Var "H")) ")" ) ($#k3_qc_lang2 :::"'or'"::: ) (Set "(" ($#k11_qc_lang2 :::"the_right_disjunct_of"::: ) (Set (Var "H")) ")" ))))) ; theorem :: QC_LANG2:38 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "H")) "is" ($#v2_qc_lang2 :::"conditional"::: ) )) "holds" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k12_qc_lang2 :::"the_antecedent_of"::: ) (Set (Var "H")) ")" ) ($#k2_qc_lang2 :::"=>"::: ) (Set "(" ($#k11_qc_lang2 :::"the_consequent_of"::: ) (Set (Var "H")) ")" ))))) ; theorem :: QC_LANG2:39 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "H")) "is" ($#v3_qc_lang2 :::"biconditional"::: ) )) "holds" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k13_qc_lang2 :::"the_left_side_of"::: ) (Set (Var "H")) ")" ) ($#k4_qc_lang2 :::"<=>"::: ) (Set "(" ($#k14_qc_lang2 :::"the_right_side_of"::: ) (Set (Var "H")) ")" ))))) ; theorem :: QC_LANG2:40 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "H")) "is" ($#v4_qc_lang2 :::"existential"::: ) )) "holds" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#k5_qc_lang2 :::"Ex"::: ) "(" (Set "(" ($#k21_qc_lang1 :::"bound_in"::: ) (Set "(" ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) "," (Set "(" ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set "(" ($#k22_qc_lang1 :::"the_scope_of"::: ) (Set "(" ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) ")" ) ")" )))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "G", "H" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Const "A"))); pred "G" :::"is_immediate_constituent_of"::: "H" means :: QC_LANG2:def 19 (Bool "(" (Bool "H" ($#r1_hidden :::"="::: ) (Set ($#k13_qc_lang1 :::"'not'"::: ) "G")) "or" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) "A") "st" (Bool "(" (Bool "H" ($#r1_hidden :::"="::: ) (Set "G" ($#k14_qc_lang1 :::"'&'"::: ) (Set (Var "F")))) "or" (Bool "H" ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k14_qc_lang1 :::"'&'"::: ) "G")) ")" )) "or" (Bool "ex" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" "A" "st" (Bool "H" ($#r1_hidden :::"="::: ) (Set ($#k15_qc_lang1 :::"All"::: ) "(" (Set (Var "x")) "," "G" ")" ))) ")" ); end; :: deftheorem defines :::"is_immediate_constituent_of"::: QC_LANG2:def 19 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "G")) ($#r1_qc_lang2 :::"is_immediate_constituent_of"::: ) (Set (Var "H"))) "iff" (Bool "(" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#k13_qc_lang1 :::"'not'"::: ) (Set (Var "G")))) "or" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool "(" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k14_qc_lang1 :::"'&'"::: ) (Set (Var "F")))) "or" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k14_qc_lang1 :::"'&'"::: ) (Set (Var "G")))) ")" )) "or" (Bool "ex" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "st" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#k15_qc_lang1 :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "G")) ")" ))) ")" ) ")" ))); theorem :: QC_LANG2:41 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Bool "not" (Set (Var "H")) ($#r1_qc_lang2 :::"is_immediate_constituent_of"::: ) (Set ($#k12_qc_lang1 :::"VERUM"::: ) (Set (Var "A"))))))) ; theorem :: QC_LANG2:42 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set (Var "A")) (Bool "for" (Set (Var "V")) "being" ($#m2_finseq_1 :::"QC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "A")) "holds" (Bool (Bool "not" (Set (Var "H")) ($#r1_qc_lang2 :::"is_immediate_constituent_of"::: ) (Set (Set (Var "P")) ($#k10_qc_lang1 :::"!"::: ) (Set (Var "V")))))))))) ; theorem :: QC_LANG2:43 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r1_qc_lang2 :::"is_immediate_constituent_of"::: ) (Set ($#k13_qc_lang1 :::"'not'"::: ) (Set (Var "H")))) "iff" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Var "H"))) ")" ))) ; theorem :: QC_LANG2:44 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "H")) ($#r1_qc_lang2 :::"is_immediate_constituent_of"::: ) (Set ($#k1_qc_lang2 :::"FALSUM"::: ) (Set (Var "A")))) "iff" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#k12_qc_lang1 :::"VERUM"::: ) (Set (Var "A")))) ")" ))) ; theorem :: QC_LANG2:45 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r1_qc_lang2 :::"is_immediate_constituent_of"::: ) (Set (Set (Var "G")) ($#k14_qc_lang1 :::"'&'"::: ) (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 :: QC_LANG2:46 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r1_qc_lang2 :::"is_immediate_constituent_of"::: ) (Set ($#k15_qc_lang1 :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "H")) ")" )) "iff" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Var "H"))) ")" )))) ; theorem :: QC_LANG2:47 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "H")) "is" ($#v2_qc_lang1 :::"atomic"::: ) )) "holds" (Bool "not" (Bool (Set (Var "F")) ($#r1_qc_lang2 :::"is_immediate_constituent_of"::: ) (Set (Var "H")))))) ; theorem :: QC_LANG2:48 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "H")) "is" ($#v3_qc_lang1 :::"negative"::: ) )) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r1_qc_lang2 :::"is_immediate_constituent_of"::: ) (Set (Var "H"))) "iff" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set (Var "H")))) ")" ))) ; theorem :: QC_LANG2:49 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "H")) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) )) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r1_qc_lang2 :::"is_immediate_constituent_of"::: ) (Set (Var "H"))) "iff" (Bool "(" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k19_qc_lang1 :::"the_left_argument_of"::: ) (Set (Var "H")))) "or" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k20_qc_lang1 :::"the_right_argument_of"::: ) (Set (Var "H")))) ")" ) ")" ))) ; theorem :: QC_LANG2:50 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "H")) "is" ($#v5_qc_lang1 :::"universal"::: ) )) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r1_qc_lang2 :::"is_immediate_constituent_of"::: ) (Set (Var "H"))) "iff" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k22_qc_lang1 :::"the_scope_of"::: ) (Set (Var "H")))) ")" ))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "G", "H" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Const "A"))); pred "G" :::"is_subformula_of"::: "H" means :: QC_LANG2:def 20 (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 :::"="::: ) "G") & (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) "H") & (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 "G1")) "," (Set (Var "H1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) "A") "st" (Bool "(" (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Var "G1"))) & (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "H1"))) & (Bool (Set (Var "G1")) ($#r1_qc_lang2 :::"is_immediate_constituent_of"::: ) (Set (Var "H1"))) ")" )) ")" ) ")" ))); reflexivity (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Const "A"))) (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 "G"))) & (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "G"))) & (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 "G1")) "," (Set (Var "H1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Const "A"))) "st" (Bool "(" (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Var "G1"))) & (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "H1"))) & (Bool (Set (Var "G1")) ($#r1_qc_lang2 :::"is_immediate_constituent_of"::: ) (Set (Var "H1"))) ")" )) ")" ) ")" )))) ; end; :: deftheorem defines :::"is_subformula_of"::: QC_LANG2:def 20 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "G")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "H"))) "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 "G"))) & (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "H"))) & (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 "G1")) "," (Set (Var "H1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool "(" (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Var "G1"))) & (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "H1"))) & (Bool (Set (Var "G1")) ($#r1_qc_lang2 :::"is_immediate_constituent_of"::: ) (Set (Var "H1"))) ")" )) ")" ) ")" ))) ")" ))); definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "H", "F" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Const "A"))); pred "H" :::"is_proper_subformula_of"::: "F" means :: QC_LANG2:def 21 (Bool "(" (Bool "H" ($#r2_qc_lang2 :::"is_subformula_of"::: ) "F") & (Bool "H" ($#r1_hidden :::"<>"::: ) "F") ")" ); irreflexivity (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Const "A"))) "holds" (Bool "(" "not" (Bool (Set (Var "H")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "H"))) "or" "not" (Bool (Set (Var "H")) ($#r1_hidden :::"<>"::: ) (Set (Var "H"))) ")" )) ; end; :: deftheorem defines :::"is_proper_subformula_of"::: QC_LANG2:def 21 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "H")) ($#r3_qc_lang2 :::"is_proper_subformula_of"::: ) (Set (Var "F"))) "iff" (Bool "(" (Bool (Set (Var "H")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "F"))) & (Bool (Set (Var "H")) ($#r1_hidden :::"<>"::: ) (Set (Var "F"))) ")" ) ")" ))); theorem :: QC_LANG2:51 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "H")) ($#r1_qc_lang2 :::"is_immediate_constituent_of"::: ) (Set (Var "F")))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set (Var "H")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set (Var "F")) ")" ))))) ; theorem :: QC_LANG2:52 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "H")) ($#r1_qc_lang2 :::"is_immediate_constituent_of"::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "H")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "F"))))) ; theorem :: QC_LANG2:53 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "H")) ($#r1_qc_lang2 :::"is_immediate_constituent_of"::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "H")) ($#r3_qc_lang2 :::"is_proper_subformula_of"::: ) (Set (Var "F"))))) ; theorem :: QC_LANG2:54 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "H")) ($#r3_qc_lang2 :::"is_proper_subformula_of"::: ) (Set (Var "F")))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set (Var "H")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k11_qc_lang1 :::"@"::: ) (Set (Var "F")) ")" ))))) ; theorem :: QC_LANG2:55 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "H")) ($#r3_qc_lang2 :::"is_proper_subformula_of"::: ) (Set (Var "F")))) "holds" (Bool "ex" (Set (Var "G")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Set (Var "G")) ($#r1_qc_lang2 :::"is_immediate_constituent_of"::: ) (Set (Var "F")))))) ; theorem :: QC_LANG2:56 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "F")) ($#r3_qc_lang2 :::"is_proper_subformula_of"::: ) (Set (Var "G"))) & (Bool (Set (Var "G")) ($#r3_qc_lang2 :::"is_proper_subformula_of"::: ) (Set (Var "H")))) "holds" (Bool (Set (Var "F")) ($#r3_qc_lang2 :::"is_proper_subformula_of"::: ) (Set (Var "H"))))) ; theorem :: QC_LANG2:57 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "F")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "G"))) & (Bool (Set (Var "G")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "H")))) "holds" (Bool (Set (Var "F")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "H"))))) ; theorem :: QC_LANG2:58 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "G")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "H"))) & (Bool (Set (Var "H")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "G")))) "holds" (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set (Var "H"))))) ; theorem :: QC_LANG2:59 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" "not" (Bool (Set (Var "G")) ($#r3_qc_lang2 :::"is_proper_subformula_of"::: ) (Set (Var "H"))) "or" "not" (Bool (Set (Var "H")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "G"))) ")" ))) ; theorem :: QC_LANG2:60 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" "not" (Bool (Set (Var "G")) ($#r3_qc_lang2 :::"is_proper_subformula_of"::: ) (Set (Var "H"))) "or" "not" (Bool (Set (Var "H")) ($#r3_qc_lang2 :::"is_proper_subformula_of"::: ) (Set (Var "G"))) ")" ))) ; theorem :: QC_LANG2:61 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" "not" (Bool (Set (Var "G")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "H"))) "or" "not" (Bool (Set (Var "H")) ($#r1_qc_lang2 :::"is_immediate_constituent_of"::: ) (Set (Var "G"))) ")" ))) ; theorem :: QC_LANG2:62 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" "not" (Bool (Set (Var "G")) ($#r3_qc_lang2 :::"is_proper_subformula_of"::: ) (Set (Var "H"))) "or" "not" (Bool (Set (Var "H")) ($#r1_qc_lang2 :::"is_immediate_constituent_of"::: ) (Set (Var "G"))) ")" ))) ; theorem :: QC_LANG2:63 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool "(" (Bool "(" (Bool (Set (Var "F")) ($#r3_qc_lang2 :::"is_proper_subformula_of"::: ) (Set (Var "G"))) & (Bool (Set (Var "G")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "H"))) ")" ) "or" (Bool "(" (Bool (Set (Var "F")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "G"))) & (Bool (Set (Var "G")) ($#r3_qc_lang2 :::"is_proper_subformula_of"::: ) (Set (Var "H"))) ")" ) "or" (Bool "(" (Bool (Set (Var "F")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "G"))) & (Bool (Set (Var "G")) ($#r1_qc_lang2 :::"is_immediate_constituent_of"::: ) (Set (Var "H"))) ")" ) "or" (Bool "(" (Bool (Set (Var "F")) ($#r1_qc_lang2 :::"is_immediate_constituent_of"::: ) (Set (Var "G"))) & (Bool (Set (Var "G")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "H"))) ")" ) "or" (Bool "(" (Bool (Set (Var "F")) ($#r3_qc_lang2 :::"is_proper_subformula_of"::: ) (Set (Var "G"))) & (Bool (Set (Var "G")) ($#r1_qc_lang2 :::"is_immediate_constituent_of"::: ) (Set (Var "H"))) ")" ) "or" (Bool "(" (Bool (Set (Var "F")) ($#r1_qc_lang2 :::"is_immediate_constituent_of"::: ) (Set (Var "G"))) & (Bool (Set (Var "G")) ($#r3_qc_lang2 :::"is_proper_subformula_of"::: ) (Set (Var "H"))) ")" ) ")" )) "holds" (Bool (Set (Var "F")) ($#r3_qc_lang2 :::"is_proper_subformula_of"::: ) (Set (Var "H"))))) ; theorem :: QC_LANG2:64 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Bool "not" (Set (Var "F")) ($#r3_qc_lang2 :::"is_proper_subformula_of"::: ) (Set ($#k12_qc_lang1 :::"VERUM"::: ) (Set (Var "A"))))))) ; theorem :: QC_LANG2:65 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set (Var "A")) (Bool "for" (Set (Var "V")) "being" ($#m2_finseq_1 :::"QC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "A")) "holds" (Bool (Bool "not" (Set (Var "F")) ($#r3_qc_lang2 :::"is_proper_subformula_of"::: ) (Set (Set (Var "P")) ($#k10_qc_lang1 :::"!"::: ) (Set (Var "V")))))))))) ; theorem :: QC_LANG2:66 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "H"))) "iff" (Bool (Set (Var "F")) ($#r3_qc_lang2 :::"is_proper_subformula_of"::: ) (Set ($#k13_qc_lang1 :::"'not'"::: ) (Set (Var "H")))) ")" ))) ; theorem :: QC_LANG2:67 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set ($#k13_qc_lang1 :::"'not'"::: ) (Set (Var "F"))) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "H")))) "holds" (Bool (Set (Var "F")) ($#r3_qc_lang2 :::"is_proper_subformula_of"::: ) (Set (Var "H"))))) ; theorem :: QC_LANG2:68 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r3_qc_lang2 :::"is_proper_subformula_of"::: ) (Set ($#k1_qc_lang2 :::"FALSUM"::: ) (Set (Var "A")))) "iff" (Bool (Set (Var "F")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set ($#k12_qc_lang1 :::"VERUM"::: ) (Set (Var "A")))) ")" ))) ; theorem :: QC_LANG2:69 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "F")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "G"))) "or" (Bool (Set (Var "F")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "H"))) ")" ) "iff" (Bool (Set (Var "F")) ($#r3_qc_lang2 :::"is_proper_subformula_of"::: ) (Set (Set (Var "G")) ($#k14_qc_lang1 :::"'&'"::: ) (Set (Var "H")))) ")" ))) ; theorem :: QC_LANG2:70 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Set (Var "F")) ($#k14_qc_lang1 :::"'&'"::: ) (Set (Var "G"))) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "H")))) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r3_qc_lang2 :::"is_proper_subformula_of"::: ) (Set (Var "H"))) & (Bool (Set (Var "G")) ($#r3_qc_lang2 :::"is_proper_subformula_of"::: ) (Set (Var "H"))) ")" ))) ; theorem :: QC_LANG2:71 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "H"))) "iff" (Bool (Set (Var "F")) ($#r3_qc_lang2 :::"is_proper_subformula_of"::: ) (Set ($#k15_qc_lang1 :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "H")) ")" )) ")" )))) ; theorem :: QC_LANG2:72 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#k15_qc_lang1 :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "H")) ")" ) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "H")) ($#r3_qc_lang2 :::"is_proper_subformula_of"::: ) (Set (Var "F")))))) ; theorem :: QC_LANG2:73 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k14_qc_lang1 :::"'&'"::: ) (Set "(" ($#k13_qc_lang1 :::"'not'"::: ) (Set (Var "G")) ")" )) ($#r3_qc_lang2 :::"is_proper_subformula_of"::: ) (Set (Set (Var "F")) ($#k2_qc_lang2 :::"=>"::: ) (Set (Var "G")))) & (Bool (Set (Var "F")) ($#r3_qc_lang2 :::"is_proper_subformula_of"::: ) (Set (Set (Var "F")) ($#k2_qc_lang2 :::"=>"::: ) (Set (Var "G")))) & (Bool (Set ($#k13_qc_lang1 :::"'not'"::: ) (Set (Var "G"))) ($#r3_qc_lang2 :::"is_proper_subformula_of"::: ) (Set (Set (Var "F")) ($#k2_qc_lang2 :::"=>"::: ) (Set (Var "G")))) & (Bool (Set (Var "G")) ($#r3_qc_lang2 :::"is_proper_subformula_of"::: ) (Set (Set (Var "F")) ($#k2_qc_lang2 :::"=>"::: ) (Set (Var "G")))) ")" ))) ; theorem :: QC_LANG2:74 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k13_qc_lang1 :::"'not'"::: ) (Set (Var "F")) ")" ) ($#k14_qc_lang1 :::"'&'"::: ) (Set "(" ($#k13_qc_lang1 :::"'not'"::: ) (Set (Var "G")) ")" )) ($#r3_qc_lang2 :::"is_proper_subformula_of"::: ) (Set (Set (Var "F")) ($#k3_qc_lang2 :::"'or'"::: ) (Set (Var "G")))) & (Bool (Set ($#k13_qc_lang1 :::"'not'"::: ) (Set (Var "F"))) ($#r3_qc_lang2 :::"is_proper_subformula_of"::: ) (Set (Set (Var "F")) ($#k3_qc_lang2 :::"'or'"::: ) (Set (Var "G")))) & (Bool (Set ($#k13_qc_lang1 :::"'not'"::: ) (Set (Var "G"))) ($#r3_qc_lang2 :::"is_proper_subformula_of"::: ) (Set (Set (Var "F")) ($#k3_qc_lang2 :::"'or'"::: ) (Set (Var "G")))) & (Bool (Set (Var "F")) ($#r3_qc_lang2 :::"is_proper_subformula_of"::: ) (Set (Set (Var "F")) ($#k3_qc_lang2 :::"'or'"::: ) (Set (Var "G")))) & (Bool (Set (Var "G")) ($#r3_qc_lang2 :::"is_proper_subformula_of"::: ) (Set (Set (Var "F")) ($#k3_qc_lang2 :::"'or'"::: ) (Set (Var "G")))) ")" ))) ; theorem :: QC_LANG2:75 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "H")) "is" ($#v2_qc_lang1 :::"atomic"::: ) )) "holds" (Bool "not" (Bool (Set (Var "F")) ($#r3_qc_lang2 :::"is_proper_subformula_of"::: ) (Set (Var "H")))))) ; theorem :: QC_LANG2:76 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "H")) "is" ($#v3_qc_lang1 :::"negative"::: ) )) "holds" (Bool (Set ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set (Var "H"))) ($#r3_qc_lang2 :::"is_proper_subformula_of"::: ) (Set (Var "H"))))) ; theorem :: QC_LANG2:77 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "H")) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) )) "holds" (Bool "(" (Bool (Set ($#k19_qc_lang1 :::"the_left_argument_of"::: ) (Set (Var "H"))) ($#r3_qc_lang2 :::"is_proper_subformula_of"::: ) (Set (Var "H"))) & (Bool (Set ($#k20_qc_lang1 :::"the_right_argument_of"::: ) (Set (Var "H"))) ($#r3_qc_lang2 :::"is_proper_subformula_of"::: ) (Set (Var "H"))) ")" ))) ; theorem :: QC_LANG2:78 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "H")) "is" ($#v5_qc_lang1 :::"universal"::: ) )) "holds" (Bool (Set ($#k22_qc_lang1 :::"the_scope_of"::: ) (Set (Var "H"))) ($#r3_qc_lang2 :::"is_proper_subformula_of"::: ) (Set (Var "H"))))) ; theorem :: QC_LANG2:79 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "H")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set ($#k12_qc_lang1 :::"VERUM"::: ) (Set (Var "A")))) "iff" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#k12_qc_lang1 :::"VERUM"::: ) (Set (Var "A")))) ")" ))) ; theorem :: QC_LANG2:80 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set (Var "A")) (Bool "for" (Set (Var "V")) "being" ($#m2_finseq_1 :::"QC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "H")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Set (Var "P")) ($#k10_qc_lang1 :::"!"::: ) (Set (Var "V")))) "iff" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k10_qc_lang1 :::"!"::: ) (Set (Var "V")))) ")" )))))) ; theorem :: QC_LANG2:81 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "H")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set ($#k1_qc_lang2 :::"FALSUM"::: ) (Set (Var "A")))) "iff" (Bool "(" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#k1_qc_lang2 :::"FALSUM"::: ) (Set (Var "A")))) "or" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#k12_qc_lang1 :::"VERUM"::: ) (Set (Var "A")))) ")" ) ")" ))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "H" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Const "A"))); func :::"Subformulae"::: "H" -> ($#m1_hidden :::"set"::: ) means :: QC_LANG2:def 22 (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" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) "A") "st" (Bool "(" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Var "F")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) "H") ")" )) ")" )); end; :: deftheorem defines :::"Subformulae"::: QC_LANG2:def 22 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k15_qc_lang2 :::"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 "b3"))) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool "(" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Var "F")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "H"))) ")" )) ")" )) ")" )))); theorem :: QC_LANG2:82 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "G")) ($#r2_hidden :::"in"::: ) (Set ($#k15_qc_lang2 :::"Subformulae"::: ) (Set (Var "H"))))) "holds" (Bool (Set (Var "G")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "H"))))) ; theorem :: QC_LANG2:83 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "F")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "H")))) "holds" (Bool (Set ($#k15_qc_lang2 :::"Subformulae"::: ) (Set (Var "F"))) ($#r1_tarski :::"c="::: ) (Set ($#k15_qc_lang2 :::"Subformulae"::: ) (Set (Var "H")))))) ; theorem :: QC_LANG2:84 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "G")) ($#r2_hidden :::"in"::: ) (Set ($#k15_qc_lang2 :::"Subformulae"::: ) (Set (Var "H"))))) "holds" (Bool (Set ($#k15_qc_lang2 :::"Subformulae"::: ) (Set (Var "G"))) ($#r1_tarski :::"c="::: ) (Set ($#k15_qc_lang2 :::"Subformulae"::: ) (Set (Var "H")))))) ; theorem :: QC_LANG2:85 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) "holds" (Bool (Set ($#k15_qc_lang2 :::"Subformulae"::: ) (Set "(" ($#k12_qc_lang1 :::"VERUM"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k12_qc_lang1 :::"VERUM"::: ) (Set (Var "A")) ")" ) ($#k1_tarski :::"}"::: ) ))) ; theorem :: QC_LANG2:86 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set (Var "A")) (Bool "for" (Set (Var "V")) "being" ($#m2_finseq_1 :::"QC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "A")) "holds" (Bool (Set ($#k15_qc_lang2 :::"Subformulae"::: ) (Set "(" (Set (Var "P")) ($#k10_qc_lang1 :::"!"::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "P")) ($#k10_qc_lang1 :::"!"::: ) (Set (Var "V")) ")" ) ($#k1_tarski :::"}"::: ) )))))) ; theorem :: QC_LANG2:87 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) "holds" (Bool (Set ($#k15_qc_lang2 :::"Subformulae"::: ) (Set "(" ($#k1_qc_lang2 :::"FALSUM"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" ($#k12_qc_lang1 :::"VERUM"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k1_qc_lang2 :::"FALSUM"::: ) (Set (Var "A")) ")" ) ($#k2_tarski :::"}"::: ) ))) ; theorem :: QC_LANG2:88 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set ($#k15_qc_lang2 :::"Subformulae"::: ) (Set "(" ($#k13_qc_lang1 :::"'not'"::: ) (Set (Var "H")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k15_qc_lang2 :::"Subformulae"::: ) (Set (Var "H")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k13_qc_lang1 :::"'not'"::: ) (Set (Var "H")) ")" ) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: QC_LANG2:89 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set ($#k15_qc_lang2 :::"Subformulae"::: ) (Set "(" (Set (Var "H")) ($#k14_qc_lang1 :::"'&'"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k15_qc_lang2 :::"Subformulae"::: ) (Set (Var "H")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k15_qc_lang2 :::"Subformulae"::: ) (Set (Var "F")) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "H")) ($#k14_qc_lang1 :::"'&'"::: ) (Set (Var "F")) ")" ) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: QC_LANG2:90 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k15_qc_lang2 :::"Subformulae"::: ) (Set "(" ($#k15_qc_lang1 :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "H")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k15_qc_lang2 :::"Subformulae"::: ) (Set (Var "H")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k15_qc_lang1 :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "H")) ")" ")" ) ($#k1_tarski :::"}"::: ) )))))) ; theorem :: QC_LANG2:91 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set ($#k15_qc_lang2 :::"Subformulae"::: ) (Set "(" (Set (Var "F")) ($#k2_qc_lang2 :::"=>"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k15_qc_lang2 :::"Subformulae"::: ) (Set (Var "F")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k15_qc_lang2 :::"Subformulae"::: ) (Set (Var "G")) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set "(" ($#k13_qc_lang1 :::"'not'"::: ) (Set (Var "G")) ")" ) "," (Set "(" (Set (Var "F")) ($#k14_qc_lang1 :::"'&'"::: ) (Set "(" ($#k13_qc_lang1 :::"'not'"::: ) (Set (Var "G")) ")" ) ")" ) "," (Set "(" (Set (Var "F")) ($#k2_qc_lang2 :::"=>"::: ) (Set (Var "G")) ")" ) ($#k1_enumset1 :::"}"::: ) ))))) ; theorem :: QC_LANG2:92 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set ($#k15_qc_lang2 :::"Subformulae"::: ) (Set "(" (Set (Var "F")) ($#k3_qc_lang2 :::"'or'"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k15_qc_lang2 :::"Subformulae"::: ) (Set (Var "F")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k15_qc_lang2 :::"Subformulae"::: ) (Set (Var "G")) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set "(" ($#k13_qc_lang1 :::"'not'"::: ) (Set (Var "G")) ")" ) "," (Set "(" ($#k13_qc_lang1 :::"'not'"::: ) (Set (Var "F")) ")" ) "," (Set "(" (Set "(" ($#k13_qc_lang1 :::"'not'"::: ) (Set (Var "F")) ")" ) ($#k14_qc_lang1 :::"'&'"::: ) (Set "(" ($#k13_qc_lang1 :::"'not'"::: ) (Set (Var "G")) ")" ) ")" ) "," (Set "(" (Set (Var "F")) ($#k3_qc_lang2 :::"'or'"::: ) (Set (Var "G")) ")" ) ($#k2_enumset1 :::"}"::: ) ))))) ; theorem :: QC_LANG2:93 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set ($#k15_qc_lang2 :::"Subformulae"::: ) (Set "(" (Set (Var "F")) ($#k4_qc_lang2 :::"<=>"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k15_qc_lang2 :::"Subformulae"::: ) (Set (Var "F")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k15_qc_lang2 :::"Subformulae"::: ) (Set (Var "G")) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k5_enumset1 :::"{"::: ) (Set "(" ($#k13_qc_lang1 :::"'not'"::: ) (Set (Var "G")) ")" ) "," (Set "(" (Set (Var "F")) ($#k14_qc_lang1 :::"'&'"::: ) (Set "(" ($#k13_qc_lang1 :::"'not'"::: ) (Set (Var "G")) ")" ) ")" ) "," (Set "(" (Set (Var "F")) ($#k2_qc_lang2 :::"=>"::: ) (Set (Var "G")) ")" ) "," (Set "(" ($#k13_qc_lang1 :::"'not'"::: ) (Set (Var "F")) ")" ) "," (Set "(" (Set (Var "G")) ($#k14_qc_lang1 :::"'&'"::: ) (Set "(" ($#k13_qc_lang1 :::"'not'"::: ) (Set (Var "F")) ")" ) ")" ) "," (Set "(" (Set (Var "G")) ($#k2_qc_lang2 :::"=>"::: ) (Set (Var "F")) ")" ) "," (Set "(" (Set (Var "F")) ($#k4_qc_lang2 :::"<=>"::: ) (Set (Var "G")) ")" ) ($#k5_enumset1 :::"}"::: ) ))))) ; theorem :: QC_LANG2:94 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set ($#k12_qc_lang1 :::"VERUM"::: ) (Set (Var "A")))) "or" (Bool (Set (Var "H")) "is" ($#v2_qc_lang1 :::"atomic"::: ) ) ")" ) "iff" (Bool (Set ($#k15_qc_lang2 :::"Subformulae"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "H")) ($#k1_tarski :::"}"::: ) )) ")" ))) ; theorem :: QC_LANG2:95 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "H")) "is" ($#v3_qc_lang1 :::"negative"::: ) )) "holds" (Bool (Set ($#k15_qc_lang2 :::"Subformulae"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k15_qc_lang2 :::"Subformulae"::: ) (Set "(" ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "H")) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: QC_LANG2:96 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "H")) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) )) "holds" (Bool (Set ($#k15_qc_lang2 :::"Subformulae"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k15_qc_lang2 :::"Subformulae"::: ) (Set "(" ($#k19_qc_lang1 :::"the_left_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k15_qc_lang2 :::"Subformulae"::: ) (Set "(" ($#k20_qc_lang1 :::"the_right_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "H")) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: QC_LANG2:97 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "H")) "is" ($#v5_qc_lang1 :::"universal"::: ) )) "holds" (Bool (Set ($#k15_qc_lang2 :::"Subformulae"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k15_qc_lang2 :::"Subformulae"::: ) (Set "(" ($#k22_qc_lang1 :::"the_scope_of"::: ) (Set (Var "H")) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "H")) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: QC_LANG2:98 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "H")) "," (Set (Var "G")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool "(" (Bool (Set (Var "H")) ($#r1_qc_lang2 :::"is_immediate_constituent_of"::: ) (Set (Var "G"))) "or" (Bool (Set (Var "H")) ($#r3_qc_lang2 :::"is_proper_subformula_of"::: ) (Set (Var "G"))) "or" (Bool (Set (Var "H")) ($#r2_qc_lang2 :::"is_subformula_of"::: ) (Set (Var "G"))) ")" ) & (Bool (Set (Var "G")) ($#r2_hidden :::"in"::: ) (Set ($#k15_qc_lang2 :::"Subformulae"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Var "H")) ($#r2_hidden :::"in"::: ) (Set ($#k15_qc_lang2 :::"Subformulae"::: ) (Set (Var "F")))))) ;