:: QC_LANG3 semantic presentation begin scheme :: QC_LANG3:sch 1 QCFuncUniq{ F1() -> ($#m1_qc_lang1 :::"QC-alphabet"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" ) ")" ) "," (Set F2 "(" ")" ), F4() -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" ) ")" ) "," (Set F2 "(" ")" ), F5() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F6( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F7( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F8( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F9( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) } : (Bool (Set F3 "(" ")" ) ($#r2_funct_2 :::"="::: ) (Set F4 "(" ")" )) provided (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k12_qc_lang1 :::"VERUM"::: ) (Set F1 "(" ")" )))) "implies" (Bool (Set (Set F3 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F5 "(" ")" )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v2_qc_lang1 :::"atomic"::: ) )) "implies" (Bool (Set (Set F3 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "p")) ")" )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v3_qc_lang1 :::"negative"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set F3 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set (Var "p")) ")" )))) "implies" (Bool (Set (Set F3 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set (Var "d1")) ")" )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set F3 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k19_qc_lang1 :::"the_left_argument_of"::: ) (Set (Var "p")) ")" ))) & (Bool (Set (Var "d2")) ($#r1_hidden :::"="::: ) (Set (Set F3 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k20_qc_lang1 :::"the_right_argument_of"::: ) (Set (Var "p")) ")" )))) "implies" (Bool (Set (Set F3 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F8 "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v5_qc_lang1 :::"universal"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set F3 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k22_qc_lang1 :::"the_scope_of"::: ) (Set (Var "p")) ")" )))) "implies" (Bool (Set (Set F3 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F9 "(" (Set (Var "p")) "," (Set (Var "d1")) ")" )) ")" ")" ))) and (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k12_qc_lang1 :::"VERUM"::: ) (Set F1 "(" ")" )))) "implies" (Bool (Set (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F5 "(" ")" )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v2_qc_lang1 :::"atomic"::: ) )) "implies" (Bool (Set (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "p")) ")" )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v3_qc_lang1 :::"negative"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set (Var "p")) ")" )))) "implies" (Bool (Set (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set (Var "d1")) ")" )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k19_qc_lang1 :::"the_left_argument_of"::: ) (Set (Var "p")) ")" ))) & (Bool (Set (Var "d2")) ($#r1_hidden :::"="::: ) (Set (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k20_qc_lang1 :::"the_right_argument_of"::: ) (Set (Var "p")) ")" )))) "implies" (Bool (Set (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F8 "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v5_qc_lang1 :::"universal"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k22_qc_lang1 :::"the_scope_of"::: ) (Set (Var "p")) ")" )))) "implies" (Bool (Set (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F9 "(" (Set (Var "p")) "," (Set (Var "d1")) ")" )) ")" ")" ))) proof end; scheme :: QC_LANG3:sch 2 QCDefD{ F1() -> ($#m1_qc_lang1 :::"QC-alphabet"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F4() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" )), F5( ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" ))) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F6( ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" )) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F7( ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "," ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" )) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F8( ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" )) "," ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" )) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) } : (Bool "(" (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" )(Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" ) ")" ) "," (Set F2 "(" ")" ) "st" (Bool "(" (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set F4 "(" ")" ))) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k12_qc_lang1 :::"VERUM"::: ) (Set F1 "(" ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v2_qc_lang1 :::"atomic"::: ) )) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "p")) ")" )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v3_qc_lang1 :::"negative"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set (Var "p")) ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "d1")) ")" )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k19_qc_lang1 :::"the_left_argument_of"::: ) (Set (Var "p")) ")" ))) & (Bool (Set (Var "d2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k20_qc_lang1 :::"the_right_argument_of"::: ) (Set (Var "p")) ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v5_qc_lang1 :::"universal"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k22_qc_lang1 :::"the_scope_of"::: ) (Set (Var "p")) ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F8 "(" (Set (Var "p")) "," (Set (Var "d1")) ")" )) ")" ")" )) ")" ) ")" ))) & (Bool "(" "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "st" (Bool (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" ) ")" ) "," (Set F2 "(" ")" ) "st" (Bool "(" (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set F4 "(" ")" ))) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k12_qc_lang1 :::"VERUM"::: ) (Set F1 "(" ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v2_qc_lang1 :::"atomic"::: ) )) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "p")) ")" )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v3_qc_lang1 :::"negative"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set (Var "p")) ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "d1")) ")" )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k19_qc_lang1 :::"the_left_argument_of"::: ) (Set (Var "p")) ")" ))) & (Bool (Set (Var "d2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k20_qc_lang1 :::"the_right_argument_of"::: ) (Set (Var "p")) ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v5_qc_lang1 :::"universal"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k22_qc_lang1 :::"the_scope_of"::: ) (Set (Var "p")) ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F8 "(" (Set (Var "p")) "," (Set (Var "d1")) ")" )) ")" ")" )) ")" ) ")" )) & (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" ) ")" ) "," (Set F2 "(" ")" ) "st" (Bool "(" (Bool (Set (Var "x2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set F4 "(" ")" ))) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k12_qc_lang1 :::"VERUM"::: ) (Set F1 "(" ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v2_qc_lang1 :::"atomic"::: ) )) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "p")) ")" )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v3_qc_lang1 :::"negative"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set (Var "p")) ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "d1")) ")" )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k19_qc_lang1 :::"the_left_argument_of"::: ) (Set (Var "p")) ")" ))) & (Bool (Set (Var "d2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k20_qc_lang1 :::"the_right_argument_of"::: ) (Set (Var "p")) ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v5_qc_lang1 :::"universal"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k22_qc_lang1 :::"the_scope_of"::: ) (Set (Var "p")) ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F8 "(" (Set (Var "p")) "," (Set (Var "d1")) ")" )) ")" ")" )) ")" ) ")" ))) "holds" (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) ")" ) ")" ) proof end; scheme :: QC_LANG3:sch 3 QCDResult9VERUM{ F1() -> ($#m1_qc_lang1 :::"QC-alphabet"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3( ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" ))) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F4() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F5( ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" ))) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F6( ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" )) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F7( ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "," ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" )) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F8( ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" )) "," ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" )) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) } : (Bool (Set F3 "(" (Set "(" ($#k12_qc_lang1 :::"VERUM"::: ) (Set F1 "(" ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set F4 "(" ")" )) provided (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool "(" (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "p")) ")" )) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" ) ")" ) "," (Set F2 "(" ")" ) "st" (Bool "(" (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p")))) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k12_qc_lang1 :::"VERUM"::: ) (Set F1 "(" ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F4 "(" ")" )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v2_qc_lang1 :::"atomic"::: ) )) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "p")) ")" )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v3_qc_lang1 :::"negative"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set (Var "p")) ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "d1")) ")" )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k19_qc_lang1 :::"the_left_argument_of"::: ) (Set (Var "p")) ")" ))) & (Bool (Set (Var "d2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k20_qc_lang1 :::"the_right_argument_of"::: ) (Set (Var "p")) ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v5_qc_lang1 :::"universal"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k22_qc_lang1 :::"the_scope_of"::: ) (Set (Var "p")) ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F8 "(" (Set (Var "p")) "," (Set (Var "d1")) ")" )) ")" ")" )) ")" ) ")" )) ")" ))) proof end; scheme :: QC_LANG3:sch 4 QCDResult9atomic{ F1() -> ($#m1_qc_lang1 :::"QC-alphabet"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F4( ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" ))) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F5() -> ($#m1_subset_1 :::"QC-formula":::) "of" (Set F1 "(" ")" ), F6( ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" ))) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F7( ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" )) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F8( ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "," ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" )) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F9( ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" )) "," ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" )) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) } : (Bool (Set F4 "(" (Set F5 "(" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set F5 "(" ")" ) ")" )) provided (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool "(" (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "p")) ")" )) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" ) ")" ) "," (Set F2 "(" ")" ) "st" (Bool "(" (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p")))) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k12_qc_lang1 :::"VERUM"::: ) (Set F1 "(" ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v2_qc_lang1 :::"atomic"::: ) )) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "p")) ")" )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v3_qc_lang1 :::"negative"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set (Var "p")) ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set (Var "d1")) ")" )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k19_qc_lang1 :::"the_left_argument_of"::: ) (Set (Var "p")) ")" ))) & (Bool (Set (Var "d2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k20_qc_lang1 :::"the_right_argument_of"::: ) (Set (Var "p")) ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F8 "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v5_qc_lang1 :::"universal"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k22_qc_lang1 :::"the_scope_of"::: ) (Set (Var "p")) ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F9 "(" (Set (Var "p")) "," (Set (Var "d1")) ")" )) ")" ")" )) ")" ) ")" )) ")" ))) and (Bool (Set F5 "(" ")" ) "is" ($#v2_qc_lang1 :::"atomic"::: ) ) proof end; scheme :: QC_LANG3:sch 5 QCDResult9negative{ F1() -> ($#m1_qc_lang1 :::"QC-alphabet"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F4() -> ($#m1_subset_1 :::"QC-formula":::) "of" (Set F1 "(" ")" ), F5( ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" ))) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F6( ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" )) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F7( ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "," ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" )) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F8( ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" )) "," ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" )) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F9( ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" ))) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) } : (Bool (Set F9 "(" (Set F4 "(" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set F9 "(" (Set "(" ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set F4 "(" ")" ) ")" ) ")" ) ")" )) provided (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool "(" (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set F9 "(" (Set (Var "p")) ")" )) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" ) ")" ) "," (Set F2 "(" ")" ) "st" (Bool "(" (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p")))) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k12_qc_lang1 :::"VERUM"::: ) (Set F1 "(" ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v2_qc_lang1 :::"atomic"::: ) )) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "p")) ")" )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v3_qc_lang1 :::"negative"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set (Var "p")) ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "d1")) ")" )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k19_qc_lang1 :::"the_left_argument_of"::: ) (Set (Var "p")) ")" ))) & (Bool (Set (Var "d2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k20_qc_lang1 :::"the_right_argument_of"::: ) (Set (Var "p")) ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v5_qc_lang1 :::"universal"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k22_qc_lang1 :::"the_scope_of"::: ) (Set (Var "p")) ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F8 "(" (Set (Var "p")) "," (Set (Var "d1")) ")" )) ")" ")" )) ")" ) ")" )) ")" ))) and (Bool (Set F4 "(" ")" ) "is" ($#v3_qc_lang1 :::"negative"::: ) ) proof end; scheme :: QC_LANG3:sch 6 QCDResult9conjunctive{ F1() -> ($#m1_qc_lang1 :::"QC-alphabet"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F4( ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" ))) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F5( ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" )) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F6( ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "," ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" )) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F7( ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" )) "," ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" )) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F8( ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" ))) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F9() -> ($#m1_subset_1 :::"QC-formula":::) "of" (Set F1 "(" ")" ) } : (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "st" (Bool (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set F8 "(" (Set "(" ($#k19_qc_lang1 :::"the_left_argument_of"::: ) (Set F9 "(" ")" ) ")" ) ")" )) & (Bool (Set (Var "d2")) ($#r1_hidden :::"="::: ) (Set F8 "(" (Set "(" ($#k20_qc_lang1 :::"the_right_argument_of"::: ) (Set F9 "(" ")" ) ")" ) ")" ))) "holds" (Bool (Set F8 "(" (Set F9 "(" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" ))) provided (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool "(" (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set F8 "(" (Set (Var "p")) ")" )) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" ) ")" ) "," (Set F2 "(" ")" ) "st" (Bool "(" (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p")))) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k12_qc_lang1 :::"VERUM"::: ) (Set F1 "(" ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v2_qc_lang1 :::"atomic"::: ) )) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "p")) ")" )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v3_qc_lang1 :::"negative"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set (Var "p")) ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "d1")) ")" )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k19_qc_lang1 :::"the_left_argument_of"::: ) (Set (Var "p")) ")" ))) & (Bool (Set (Var "d2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k20_qc_lang1 :::"the_right_argument_of"::: ) (Set (Var "p")) ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v5_qc_lang1 :::"universal"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k22_qc_lang1 :::"the_scope_of"::: ) (Set (Var "p")) ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set (Var "p")) "," (Set (Var "d1")) ")" )) ")" ")" )) ")" ) ")" )) ")" ))) and (Bool (Set F9 "(" ")" ) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) ) proof end; scheme :: QC_LANG3:sch 7 QCDResult9universal{ F1() -> ($#m1_qc_lang1 :::"QC-alphabet"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F4() -> ($#m1_subset_1 :::"QC-formula":::) "of" (Set F1 "(" ")" ), F5( ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" ))) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F6( ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" )) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F7( ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "," ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" )) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F8( ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" )) "," ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" )) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F9( ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" ))) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) } : (Bool (Set F9 "(" (Set F4 "(" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set F8 "(" (Set F4 "(" ")" ) "," (Set F9 "(" (Set "(" ($#k22_qc_lang1 :::"the_scope_of"::: ) (Set F4 "(" ")" ) ")" ) ")" ) ")" )) provided (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool "(" (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set F9 "(" (Set (Var "p")) ")" )) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" ) ")" ) "," (Set F2 "(" ")" ) "st" (Bool "(" (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p")))) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k12_qc_lang1 :::"VERUM"::: ) (Set F1 "(" ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v2_qc_lang1 :::"atomic"::: ) )) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "p")) ")" )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v3_qc_lang1 :::"negative"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set (Var "p")) ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "d1")) ")" )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k19_qc_lang1 :::"the_left_argument_of"::: ) (Set (Var "p")) ")" ))) & (Bool (Set (Var "d2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k20_qc_lang1 :::"the_right_argument_of"::: ) (Set (Var "p")) ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v5_qc_lang1 :::"universal"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k22_qc_lang1 :::"the_scope_of"::: ) (Set (Var "p")) ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F8 "(" (Set (Var "p")) "," (Set (Var "d1")) ")" )) ")" ")" )) ")" ) ")" )) ")" ))) and (Bool (Set F4 "(" ")" ) "is" ($#v5_qc_lang1 :::"universal"::: ) ) proof end; theorem :: QC_LANG3:1 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "A")) "holds" (Bool (Set (Var "P")) "is" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set "(" ($#k7_qc_lang1 :::"the_arity_of"::: ) (Set (Var "P")) ")" ) "," (Set (Var "A"))))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "l" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_qc_lang1 :::"QC-variables"::: ) (Set (Const "A"))); let "V" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_qc_lang1 :::"QC-variables"::: ) (Set (Const "A")) ")" ); func :::"variables_in"::: "(" "l" "," "V" ")" -> ($#m1_subset_1 :::"Subset":::) "of" "V" equals :: QC_LANG3:def 1 "{" (Set "(" "l" ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ) where k "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "l")) & (Bool (Set "l" ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r2_hidden :::"in"::: ) "V") ")" ) "}" ; end; :: deftheorem defines :::"variables_in"::: QC_LANG3:def 1 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "l")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_qc_lang1 :::"QC-variables"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_qc_lang1 :::"QC-variables"::: ) (Set (Var "A")) ")" ) "holds" (Bool (Set ($#k1_qc_lang3 :::"variables_in"::: ) "(" (Set (Var "l")) "," (Set (Var "V")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "l")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ) where k "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "l")))) & (Bool (Set (Set (Var "l")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) ")" ) "}" )))); theorem :: QC_LANG3:2 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "l")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_qc_lang1 :::"QC-variables"::: ) (Set (Var "A"))) "holds" (Bool (Set ($#k23_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set ($#k1_qc_lang3 :::"variables_in"::: ) "(" (Set (Var "l")) "," (Set "(" ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A")) ")" ) ")" )))) ; theorem :: QC_LANG3:3 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) "holds" (Bool (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" ($#k12_qc_lang1 :::"VERUM"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: QC_LANG3:4 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v2_qc_lang1 :::"atomic"::: ) )) "holds" (Bool (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k23_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" ($#k17_qc_lang1 :::"the_arguments_of"::: ) (Set (Var "p")) ")" ))))) ; theorem :: QC_LANG3:5 (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set (Var "A")) (Bool "for" (Set (Var "l")) "being" ($#m2_finseq_1 :::"QC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "A")) "holds" (Bool (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" (Set (Var "P")) ($#k10_qc_lang1 :::"!"::: ) (Set (Var "l")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k23_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "l")))))))) ; theorem :: QC_LANG3:6 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v3_qc_lang1 :::"negative"::: ) )) "holds" (Bool (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set (Var "p")) ")" ))))) ; theorem :: QC_LANG3:7 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" ($#k13_qc_lang1 :::"'not'"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")))))) ; theorem :: QC_LANG3:8 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) "holds" (Bool (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" ($#k1_qc_lang2 :::"FALSUM"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: QC_LANG3:9 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) )) "holds" (Bool (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" ($#k19_qc_lang1 :::"the_left_argument_of"::: ) (Set (Var "p")) ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" ($#k20_qc_lang1 :::"the_right_argument_of"::: ) (Set (Var "p")) ")" ) ")" ))))) ; theorem :: QC_LANG3:10 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" (Set (Var "p")) ($#k14_qc_lang1 :::"'&'"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "q")) ")" ))))) ; theorem :: QC_LANG3:11 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v5_qc_lang1 :::"universal"::: ) )) "holds" (Bool (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" ($#k22_qc_lang1 :::"the_scope_of"::: ) (Set (Var "p")) ")" ) ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k21_qc_lang1 :::"bound_in"::: ) (Set (Var "p")) ")" ) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: QC_LANG3:12 (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 :::"QC-formula":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" ($#k15_qc_lang1 :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )))))) ; theorem :: QC_LANG3:13 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v1_qc_lang2 :::"disjunctive"::: ) )) "holds" (Bool (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" ($#k10_qc_lang2 :::"the_left_disjunct_of"::: ) (Set (Var "p")) ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" ($#k11_qc_lang2 :::"the_right_disjunct_of"::: ) (Set (Var "p")) ")" ) ")" ))))) ; theorem :: QC_LANG3:14 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" (Set (Var "p")) ($#k3_qc_lang2 :::"'or'"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "q")) ")" ))))) ; theorem :: QC_LANG3:15 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v2_qc_lang2 :::"conditional"::: ) )) "holds" (Bool (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" ($#k12_qc_lang2 :::"the_antecedent_of"::: ) (Set (Var "p")) ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" ($#k11_qc_lang2 :::"the_consequent_of"::: ) (Set (Var "p")) ")" ) ")" ))))) ; theorem :: QC_LANG3:16 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" (Set (Var "p")) ($#k2_qc_lang2 :::"=>"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "q")) ")" ))))) ; theorem :: QC_LANG3:17 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v3_qc_lang2 :::"biconditional"::: ) )) "holds" (Bool (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" ($#k13_qc_lang2 :::"the_left_side_of"::: ) (Set (Var "p")) ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" ($#k14_qc_lang2 :::"the_right_side_of"::: ) (Set (Var "p")) ")" ) ")" ))))) ; theorem :: QC_LANG3:18 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" (Set (Var "p")) ($#k4_qc_lang2 :::"<=>"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "q")) ")" ))))) ; theorem :: QC_LANG3:19 (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 :::"QC-formula":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" ($#k5_qc_lang2 :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )))))) ; theorem :: QC_LANG3:20 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) "holds" (Bool "(" (Bool (Set ($#k12_qc_lang1 :::"VERUM"::: ) (Set (Var "A"))) "is" ($#v6_qc_lang1 :::"closed"::: ) ) & (Bool (Set ($#k1_qc_lang2 :::"FALSUM"::: ) (Set (Var "A"))) "is" ($#v6_qc_lang1 :::"closed"::: ) ) ")" )) ; theorem :: QC_LANG3:21 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "p")) "is" ($#v6_qc_lang1 :::"closed"::: ) ) "iff" (Bool (Set ($#k13_qc_lang1 :::"'not'"::: ) (Set (Var "p"))) "is" ($#v6_qc_lang1 :::"closed"::: ) ) ")" ))) ; theorem :: QC_LANG3:22 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "p")) "is" ($#v6_qc_lang1 :::"closed"::: ) ) & (Bool (Set (Var "q")) "is" ($#v6_qc_lang1 :::"closed"::: ) ) ")" ) "iff" (Bool (Set (Set (Var "p")) ($#k14_qc_lang1 :::"'&'"::: ) (Set (Var "q"))) "is" ($#v6_qc_lang1 :::"closed"::: ) ) ")" ))) ; theorem :: QC_LANG3:23 (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 :::"QC-formula":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set ($#k15_qc_lang1 :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ) "is" ($#v6_qc_lang1 :::"closed"::: ) ) "iff" (Bool (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) ")" )))) ; theorem :: QC_LANG3:24 (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 :::"QC-formula":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v6_qc_lang1 :::"closed"::: ) )) "holds" (Bool (Set ($#k15_qc_lang1 :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ) "is" ($#v6_qc_lang1 :::"closed"::: ) )))) ; theorem :: QC_LANG3:25 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "p")) "is" ($#v6_qc_lang1 :::"closed"::: ) ) & (Bool (Set (Var "q")) "is" ($#v6_qc_lang1 :::"closed"::: ) ) ")" ) "iff" (Bool (Set (Set (Var "p")) ($#k3_qc_lang2 :::"'or'"::: ) (Set (Var "q"))) "is" ($#v6_qc_lang1 :::"closed"::: ) ) ")" ))) ; theorem :: QC_LANG3:26 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "p")) "is" ($#v6_qc_lang1 :::"closed"::: ) ) & (Bool (Set (Var "q")) "is" ($#v6_qc_lang1 :::"closed"::: ) ) ")" ) "iff" (Bool (Set (Set (Var "p")) ($#k2_qc_lang2 :::"=>"::: ) (Set (Var "q"))) "is" ($#v6_qc_lang1 :::"closed"::: ) ) ")" ))) ; theorem :: QC_LANG3:27 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "p")) "is" ($#v6_qc_lang1 :::"closed"::: ) ) & (Bool (Set (Var "q")) "is" ($#v6_qc_lang1 :::"closed"::: ) ) ")" ) "iff" (Bool (Set (Set (Var "p")) ($#k4_qc_lang2 :::"<=>"::: ) (Set (Var "q"))) "is" ($#v6_qc_lang1 :::"closed"::: ) ) ")" ))) ; theorem :: QC_LANG3:28 (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 :::"QC-formula":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set ($#k5_qc_lang2 :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ) "is" ($#v6_qc_lang1 :::"closed"::: ) ) "iff" (Bool (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) ")" )))) ; theorem :: QC_LANG3:29 (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 :::"QC-formula":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v6_qc_lang1 :::"closed"::: ) )) "holds" (Bool (Set ($#k5_qc_lang2 :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ) "is" ($#v6_qc_lang1 :::"closed"::: ) )))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "s" be ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Const "A")); func :::"x."::: "s" -> ($#m2_subset_1 :::"bound_QC-variable":::) "of" "A" equals :: QC_LANG3:def 2 (Set ($#k4_tarski :::"["::: ) (Num 4) "," "s" ($#k4_tarski :::"]"::: ) ); end; :: deftheorem defines :::"x."::: QC_LANG3:def 2 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k2_qc_lang3 :::"x."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Num 4) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) )))); theorem :: QC_LANG3:30 (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 "ex" (Set (Var "t")) "being" ($#m1_subset_1 :::"QC-symbol":::) "of" (Set (Var "A")) "st" (Bool (Set ($#k2_qc_lang3 :::"x."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Var "x")))))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "k" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func "A" :::"a."::: "k" -> ($#m2_subset_1 :::"free_QC-variable":::) "of" "A" equals :: QC_LANG3:def 3 (Set ($#k4_tarski :::"["::: ) (Num 6) "," "k" ($#k4_tarski :::"]"::: ) ); end; :: deftheorem defines :::"a."::: QC_LANG3:def 3 : (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"::: ) ) "holds" (Bool (Set (Set (Var "A")) ($#k3_qc_lang3 :::"a."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Num 6) "," (Set (Var "k")) ($#k4_tarski :::"]"::: ) )))); theorem :: QC_LANG3:31 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "a")) "being" ($#m2_subset_1 :::"free_QC-variable":::) "of" (Set (Var "A")) (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Set (Var "A")) ($#k3_qc_lang3 :::"a."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "a")))))) ; theorem :: QC_LANG3:32 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "c")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_qc_lang1 :::"fixed_QC-variables"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "a")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_qc_lang1 :::"free_QC-variables"::: ) (Set (Var "A"))) "holds" (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "a")))))) ; theorem :: QC_LANG3:33 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "c")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_qc_lang1 :::"fixed_QC-variables"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A"))) "holds" (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "x")))))) ; theorem :: QC_LANG3:34 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "a")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_qc_lang1 :::"free_QC-variables"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_qc_lang1 :::"bound_QC-variables"::: ) (Set (Var "A"))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "x")))))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "V" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_qc_lang1 :::"QC-variables"::: ) (Set (Const "A")) ")" ); let "p" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Const "A"))); func :::"Vars"::: "(" "p" "," "V" ")" -> ($#m1_subset_1 :::"Subset":::) "of" "V" means :: QC_LANG3:def 4 (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_qc_lang1 :::"QC-WFF"::: ) "A" ")" ) "," (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) "V" ")" ) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) "p")) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) "A") (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Subset":::) "of" "V" "holds" (Bool "(" "(" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k12_qc_lang1 :::"VERUM"::: ) "A"))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_subset_1 :::"{}"::: ) "V")) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v2_qc_lang1 :::"atomic"::: ) )) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_qc_lang3 :::"variables_in"::: ) "(" (Set "(" ($#k17_qc_lang1 :::"the_arguments_of"::: ) (Set (Var "p")) ")" ) "," "V" ")" )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v3_qc_lang1 :::"negative"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set (Var "p")) ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "d1"))) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k19_qc_lang1 :::"the_left_argument_of"::: ) (Set (Var "p")) ")" ))) & (Bool (Set (Var "d2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k20_qc_lang1 :::"the_right_argument_of"::: ) (Set (Var "p")) ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "d1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "d2")))) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v5_qc_lang1 :::"universal"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k22_qc_lang1 :::"the_scope_of"::: ) (Set (Var "p")) ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "d1"))) ")" ")" )) ")" ) ")" )); end; :: deftheorem defines :::"Vars"::: QC_LANG3:def 4 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_qc_lang1 :::"QC-variables"::: ) (Set (Var "A")) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k4_qc_lang3 :::"Vars"::: ) "(" (Set (Var "p")) "," (Set (Var "V")) ")" )) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set (Var "V")) ")" ) "st" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p")))) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k12_qc_lang1 :::"VERUM"::: ) (Set (Var "A"))))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_subset_1 :::"{}"::: ) (Set (Var "V")))) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v2_qc_lang1 :::"atomic"::: ) )) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_qc_lang3 :::"variables_in"::: ) "(" (Set "(" ($#k17_qc_lang1 :::"the_arguments_of"::: ) (Set (Var "p")) ")" ) "," (Set (Var "V")) ")" )) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v3_qc_lang1 :::"negative"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set (Var "p")) ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "d1"))) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k19_qc_lang1 :::"the_left_argument_of"::: ) (Set (Var "p")) ")" ))) & (Bool (Set (Var "d2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k20_qc_lang1 :::"the_right_argument_of"::: ) (Set (Var "p")) ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "d1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "d2")))) ")" & "(" (Bool (Bool (Set (Var "p")) "is" ($#v5_qc_lang1 :::"universal"::: ) ) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k22_qc_lang1 :::"the_scope_of"::: ) (Set (Var "p")) ")" )))) "implies" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "d1"))) ")" ")" )) ")" ) ")" )) ")" ))))); theorem :: QC_LANG3:35 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_qc_lang1 :::"QC-variables"::: ) (Set (Var "A")) ")" ) "holds" (Bool (Set ($#k4_qc_lang3 :::"Vars"::: ) "(" (Set "(" ($#k12_qc_lang1 :::"VERUM"::: ) (Set (Var "A")) ")" ) "," (Set (Var "V")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: QC_LANG3:36 (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"))) (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_qc_lang1 :::"QC-variables"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Var "p")) "is" ($#v2_qc_lang1 :::"atomic"::: ) )) "holds" (Bool "(" (Bool (Set ($#k4_qc_lang3 :::"Vars"::: ) "(" (Set (Var "p")) "," (Set (Var "V")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_qc_lang3 :::"variables_in"::: ) "(" (Set "(" ($#k17_qc_lang1 :::"the_arguments_of"::: ) (Set (Var "p")) ")" ) "," (Set (Var "V")) ")" )) & (Bool (Set ($#k4_qc_lang3 :::"Vars"::: ) "(" (Set (Var "p")) "," (Set (Var "V")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set "(" ($#k17_qc_lang1 :::"the_arguments_of"::: ) (Set (Var "p")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ) where k "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k17_qc_lang1 :::"the_arguments_of"::: ) (Set (Var "p")) ")" ))) & (Bool (Set (Set "(" ($#k17_qc_lang1 :::"the_arguments_of"::: ) (Set (Var "p")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) ")" ) "}" ) ")" )))) ; theorem :: QC_LANG3:37 (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_qc_lang1 :::"QC-variables"::: ) (Set (Var "A")) ")" ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set (Var "A")) (Bool "for" (Set (Var "l")) "being" ($#m2_finseq_1 :::"QC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "A")) "holds" (Bool "(" (Bool (Set ($#k4_qc_lang3 :::"Vars"::: ) "(" (Set "(" (Set (Var "P")) ($#k10_qc_lang1 :::"!"::: ) (Set (Var "l")) ")" ) "," (Set (Var "V")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_qc_lang3 :::"variables_in"::: ) "(" (Set (Var "l")) "," (Set (Var "V")) ")" )) & (Bool (Set ($#k4_qc_lang3 :::"Vars"::: ) "(" (Set "(" (Set (Var "P")) ($#k10_qc_lang1 :::"!"::: ) (Set (Var "l")) ")" ) "," (Set (Var "V")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "l")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) where i "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "l")))) & (Bool (Set (Set (Var "l")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) ")" ) "}" ) ")" )))))) ; theorem :: QC_LANG3:38 (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"))) (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_qc_lang1 :::"QC-variables"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Var "p")) "is" ($#v3_qc_lang1 :::"negative"::: ) )) "holds" (Bool (Set ($#k4_qc_lang3 :::"Vars"::: ) "(" (Set (Var "p")) "," (Set (Var "V")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_qc_lang3 :::"Vars"::: ) "(" (Set "(" ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set (Var "p")) ")" ) "," (Set (Var "V")) ")" ))))) ; theorem :: QC_LANG3:39 (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"))) (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_qc_lang1 :::"QC-variables"::: ) (Set (Var "A")) ")" ) "holds" (Bool (Set ($#k4_qc_lang3 :::"Vars"::: ) "(" (Set "(" ($#k13_qc_lang1 :::"'not'"::: ) (Set (Var "p")) ")" ) "," (Set (Var "V")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_qc_lang3 :::"Vars"::: ) "(" (Set (Var "p")) "," (Set (Var "V")) ")" ))))) ; theorem :: QC_LANG3:40 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_qc_lang1 :::"QC-variables"::: ) (Set (Var "A")) ")" ) "holds" (Bool (Set ($#k4_qc_lang3 :::"Vars"::: ) "(" (Set "(" ($#k1_qc_lang2 :::"FALSUM"::: ) (Set (Var "A")) ")" ) "," (Set (Var "V")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: QC_LANG3:41 (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"))) (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_qc_lang1 :::"QC-variables"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Var "p")) "is" ($#v4_qc_lang1 :::"conjunctive"::: ) )) "holds" (Bool (Set ($#k4_qc_lang3 :::"Vars"::: ) "(" (Set (Var "p")) "," (Set (Var "V")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_qc_lang3 :::"Vars"::: ) "(" (Set "(" ($#k19_qc_lang1 :::"the_left_argument_of"::: ) (Set (Var "p")) ")" ) "," (Set (Var "V")) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k4_qc_lang3 :::"Vars"::: ) "(" (Set "(" ($#k20_qc_lang1 :::"the_right_argument_of"::: ) (Set (Var "p")) ")" ) "," (Set (Var "V")) ")" ")" )))))) ; theorem :: QC_LANG3:42 (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"))) (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_qc_lang1 :::"QC-variables"::: ) (Set (Var "A")) ")" ) "holds" (Bool (Set ($#k4_qc_lang3 :::"Vars"::: ) "(" (Set "(" (Set (Var "p")) ($#k14_qc_lang1 :::"'&'"::: ) (Set (Var "q")) ")" ) "," (Set (Var "V")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_qc_lang3 :::"Vars"::: ) "(" (Set (Var "p")) "," (Set (Var "V")) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k4_qc_lang3 :::"Vars"::: ) "(" (Set (Var "q")) "," (Set (Var "V")) ")" ")" )))))) ; theorem :: QC_LANG3:43 (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"))) (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_qc_lang1 :::"QC-variables"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Var "p")) "is" ($#v5_qc_lang1 :::"universal"::: ) )) "holds" (Bool (Set ($#k4_qc_lang3 :::"Vars"::: ) "(" (Set (Var "p")) "," (Set (Var "V")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_qc_lang3 :::"Vars"::: ) "(" (Set "(" ($#k22_qc_lang1 :::"the_scope_of"::: ) (Set (Var "p")) ")" ) "," (Set (Var "V")) ")" ))))) ; theorem :: QC_LANG3:44 (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"))) (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_qc_lang1 :::"QC-variables"::: ) (Set (Var "A")) ")" ) "holds" (Bool (Set ($#k4_qc_lang3 :::"Vars"::: ) "(" (Set "(" ($#k15_qc_lang1 :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "V")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_qc_lang3 :::"Vars"::: ) "(" (Set (Var "p")) "," (Set (Var "V")) ")" )))))) ; theorem :: QC_LANG3:45 (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"))) (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_qc_lang1 :::"QC-variables"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Var "p")) "is" ($#v1_qc_lang2 :::"disjunctive"::: ) )) "holds" (Bool (Set ($#k4_qc_lang3 :::"Vars"::: ) "(" (Set (Var "p")) "," (Set (Var "V")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_qc_lang3 :::"Vars"::: ) "(" (Set "(" ($#k10_qc_lang2 :::"the_left_disjunct_of"::: ) (Set (Var "p")) ")" ) "," (Set (Var "V")) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k4_qc_lang3 :::"Vars"::: ) "(" (Set "(" ($#k11_qc_lang2 :::"the_right_disjunct_of"::: ) (Set (Var "p")) ")" ) "," (Set (Var "V")) ")" ")" )))))) ; theorem :: QC_LANG3:46 (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"))) (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_qc_lang1 :::"QC-variables"::: ) (Set (Var "A")) ")" ) "holds" (Bool (Set ($#k4_qc_lang3 :::"Vars"::: ) "(" (Set "(" (Set (Var "p")) ($#k3_qc_lang2 :::"'or'"::: ) (Set (Var "q")) ")" ) "," (Set (Var "V")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_qc_lang3 :::"Vars"::: ) "(" (Set (Var "p")) "," (Set (Var "V")) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k4_qc_lang3 :::"Vars"::: ) "(" (Set (Var "q")) "," (Set (Var "V")) ")" ")" )))))) ; theorem :: QC_LANG3:47 (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"))) (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_qc_lang1 :::"QC-variables"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Var "p")) "is" ($#v2_qc_lang2 :::"conditional"::: ) )) "holds" (Bool (Set ($#k4_qc_lang3 :::"Vars"::: ) "(" (Set (Var "p")) "," (Set (Var "V")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_qc_lang3 :::"Vars"::: ) "(" (Set "(" ($#k12_qc_lang2 :::"the_antecedent_of"::: ) (Set (Var "p")) ")" ) "," (Set (Var "V")) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k4_qc_lang3 :::"Vars"::: ) "(" (Set "(" ($#k11_qc_lang2 :::"the_consequent_of"::: ) (Set (Var "p")) ")" ) "," (Set (Var "V")) ")" ")" )))))) ; theorem :: QC_LANG3:48 (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"))) (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_qc_lang1 :::"QC-variables"::: ) (Set (Var "A")) ")" ) "holds" (Bool (Set ($#k4_qc_lang3 :::"Vars"::: ) "(" (Set "(" (Set (Var "p")) ($#k2_qc_lang2 :::"=>"::: ) (Set (Var "q")) ")" ) "," (Set (Var "V")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_qc_lang3 :::"Vars"::: ) "(" (Set (Var "p")) "," (Set (Var "V")) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k4_qc_lang3 :::"Vars"::: ) "(" (Set (Var "q")) "," (Set (Var "V")) ")" ")" )))))) ; theorem :: QC_LANG3:49 (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"))) (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_qc_lang1 :::"QC-variables"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Var "p")) "is" ($#v3_qc_lang2 :::"biconditional"::: ) )) "holds" (Bool (Set ($#k4_qc_lang3 :::"Vars"::: ) "(" (Set (Var "p")) "," (Set (Var "V")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_qc_lang3 :::"Vars"::: ) "(" (Set "(" ($#k13_qc_lang2 :::"the_left_side_of"::: ) (Set (Var "p")) ")" ) "," (Set (Var "V")) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k4_qc_lang3 :::"Vars"::: ) "(" (Set "(" ($#k14_qc_lang2 :::"the_right_side_of"::: ) (Set (Var "p")) ")" ) "," (Set (Var "V")) ")" ")" )))))) ; theorem :: QC_LANG3:50 (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"))) (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_qc_lang1 :::"QC-variables"::: ) (Set (Var "A")) ")" ) "holds" (Bool (Set ($#k4_qc_lang3 :::"Vars"::: ) "(" (Set "(" (Set (Var "p")) ($#k4_qc_lang2 :::"<=>"::: ) (Set (Var "q")) ")" ) "," (Set (Var "V")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_qc_lang3 :::"Vars"::: ) "(" (Set (Var "p")) "," (Set (Var "V")) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k4_qc_lang3 :::"Vars"::: ) "(" (Set (Var "q")) "," (Set (Var "V")) ")" ")" )))))) ; theorem :: QC_LANG3:51 (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"))) (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_qc_lang1 :::"QC-variables"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Var "p")) "is" ($#v4_qc_lang2 :::"existential"::: ) )) "holds" (Bool (Set ($#k4_qc_lang3 :::"Vars"::: ) "(" (Set (Var "p")) "," (Set (Var "V")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_qc_lang3 :::"Vars"::: ) "(" (Set "(" ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set "(" ($#k22_qc_lang1 :::"the_scope_of"::: ) (Set "(" ($#k18_qc_lang1 :::"the_argument_of"::: ) (Set (Var "p")) ")" ) ")" ) ")" ) "," (Set (Var "V")) ")" ))))) ; theorem :: QC_LANG3:52 (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"))) (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_qc_lang1 :::"QC-variables"::: ) (Set (Var "A")) ")" ) "holds" (Bool (Set ($#k4_qc_lang3 :::"Vars"::: ) "(" (Set "(" ($#k5_qc_lang2 :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) "," (Set (Var "V")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_qc_lang3 :::"Vars"::: ) "(" (Set (Var "p")) "," (Set (Var "V")) ")" )))))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "p" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Const "A"))); func :::"Free"::: "p" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k5_qc_lang1 :::"free_QC-variables"::: ) "A" ")" ) equals :: QC_LANG3:def 5 (Set ($#k4_qc_lang3 :::"Vars"::: ) "(" "p" "," (Set "(" ($#k5_qc_lang1 :::"free_QC-variables"::: ) "A" ")" ) ")" ); end; :: deftheorem defines :::"Free"::: QC_LANG3:def 5 : (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 ($#k5_qc_lang3 :::"Free"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k4_qc_lang3 :::"Vars"::: ) "(" (Set (Var "p")) "," (Set "(" ($#k5_qc_lang1 :::"free_QC-variables"::: ) (Set (Var "A")) ")" ) ")" )))); theorem :: QC_LANG3:53 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) "holds" (Bool (Set ($#k5_qc_lang3 :::"Free"::: ) (Set "(" ($#k12_qc_lang1 :::"VERUM"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: QC_LANG3:54 (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set (Var "A")) (Bool "for" (Set (Var "l")) "being" ($#m2_finseq_1 :::"QC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "A")) "holds" (Bool (Set ($#k5_qc_lang3 :::"Free"::: ) (Set "(" (Set (Var "P")) ($#k10_qc_lang1 :::"!"::: ) (Set (Var "l")) ")" )) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "l")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) where i "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "l")))) & (Bool (Set (Set (Var "l")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set ($#k5_qc_lang1 :::"free_QC-variables"::: ) (Set (Var "A")))) ")" ) "}" ))))) ; theorem :: QC_LANG3:55 (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 ($#k5_qc_lang3 :::"Free"::: ) (Set "(" ($#k13_qc_lang1 :::"'not'"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_qc_lang3 :::"Free"::: ) (Set (Var "p")))))) ; theorem :: QC_LANG3:56 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) "holds" (Bool (Set ($#k5_qc_lang3 :::"Free"::: ) (Set "(" ($#k1_qc_lang2 :::"FALSUM"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: QC_LANG3:57 (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 ($#k5_qc_lang3 :::"Free"::: ) (Set "(" (Set (Var "p")) ($#k14_qc_lang1 :::"'&'"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_qc_lang3 :::"Free"::: ) (Set (Var "p")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k5_qc_lang3 :::"Free"::: ) (Set (Var "q")) ")" ))))) ; theorem :: QC_LANG3:58 (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_lang3 :::"Free"::: ) (Set "(" ($#k15_qc_lang1 :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_qc_lang3 :::"Free"::: ) (Set (Var "p"))))))) ; theorem :: QC_LANG3:59 (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 ($#k5_qc_lang3 :::"Free"::: ) (Set "(" (Set (Var "p")) ($#k3_qc_lang2 :::"'or'"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_qc_lang3 :::"Free"::: ) (Set (Var "p")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k5_qc_lang3 :::"Free"::: ) (Set (Var "q")) ")" ))))) ; theorem :: QC_LANG3:60 (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 ($#k5_qc_lang3 :::"Free"::: ) (Set "(" (Set (Var "p")) ($#k2_qc_lang2 :::"=>"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_qc_lang3 :::"Free"::: ) (Set (Var "p")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k5_qc_lang3 :::"Free"::: ) (Set (Var "q")) ")" ))))) ; theorem :: QC_LANG3:61 (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 ($#k5_qc_lang3 :::"Free"::: ) (Set "(" (Set (Var "p")) ($#k4_qc_lang2 :::"<=>"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_qc_lang3 :::"Free"::: ) (Set (Var "p")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k5_qc_lang3 :::"Free"::: ) (Set (Var "q")) ")" ))))) ; theorem :: QC_LANG3:62 (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_lang3 :::"Free"::: ) (Set "(" ($#k5_qc_lang2 :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_qc_lang3 :::"Free"::: ) (Set (Var "p"))))))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "p" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_qc_lang1 :::"QC-WFF"::: ) (Set (Const "A"))); func :::"Fixed"::: "p" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k4_qc_lang1 :::"fixed_QC-variables"::: ) "A" ")" ) equals :: QC_LANG3:def 6 (Set ($#k4_qc_lang3 :::"Vars"::: ) "(" "p" "," (Set "(" ($#k4_qc_lang1 :::"fixed_QC-variables"::: ) "A" ")" ) ")" ); end; :: deftheorem defines :::"Fixed"::: QC_LANG3:def 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"))) "holds" (Bool (Set ($#k6_qc_lang3 :::"Fixed"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k4_qc_lang3 :::"Vars"::: ) "(" (Set (Var "p")) "," (Set "(" ($#k4_qc_lang1 :::"fixed_QC-variables"::: ) (Set (Var "A")) ")" ) ")" )))); theorem :: QC_LANG3:63 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) "holds" (Bool (Set ($#k6_qc_lang3 :::"Fixed"::: ) (Set "(" ($#k12_qc_lang1 :::"VERUM"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: QC_LANG3:64 (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "P")) "being" ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set (Var "A")) (Bool "for" (Set (Var "l")) "being" ($#m2_finseq_1 :::"QC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "A")) "holds" (Bool (Set ($#k6_qc_lang3 :::"Fixed"::: ) (Set "(" (Set (Var "P")) ($#k10_qc_lang1 :::"!"::: ) (Set (Var "l")) ")" )) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "l")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) where i "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "l")))) & (Bool (Set (Set (Var "l")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_qc_lang1 :::"fixed_QC-variables"::: ) (Set (Var "A")))) ")" ) "}" ))))) ; theorem :: QC_LANG3:65 (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 ($#k6_qc_lang3 :::"Fixed"::: ) (Set "(" ($#k13_qc_lang1 :::"'not'"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_qc_lang3 :::"Fixed"::: ) (Set (Var "p")))))) ; theorem :: QC_LANG3:66 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) "holds" (Bool (Set ($#k6_qc_lang3 :::"Fixed"::: ) (Set "(" ($#k1_qc_lang2 :::"FALSUM"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: QC_LANG3:67 (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 ($#k6_qc_lang3 :::"Fixed"::: ) (Set "(" (Set (Var "p")) ($#k14_qc_lang1 :::"'&'"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_qc_lang3 :::"Fixed"::: ) (Set (Var "p")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k6_qc_lang3 :::"Fixed"::: ) (Set (Var "q")) ")" ))))) ; theorem :: QC_LANG3:68 (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 ($#k6_qc_lang3 :::"Fixed"::: ) (Set "(" ($#k15_qc_lang1 :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_qc_lang3 :::"Fixed"::: ) (Set (Var "p"))))))) ; theorem :: QC_LANG3:69 (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 ($#k6_qc_lang3 :::"Fixed"::: ) (Set "(" (Set (Var "p")) ($#k3_qc_lang2 :::"'or'"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_qc_lang3 :::"Fixed"::: ) (Set (Var "p")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k6_qc_lang3 :::"Fixed"::: ) (Set (Var "q")) ")" ))))) ; theorem :: QC_LANG3:70 (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 ($#k6_qc_lang3 :::"Fixed"::: ) (Set "(" (Set (Var "p")) ($#k2_qc_lang2 :::"=>"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_qc_lang3 :::"Fixed"::: ) (Set (Var "p")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k6_qc_lang3 :::"Fixed"::: ) (Set (Var "q")) ")" ))))) ; theorem :: QC_LANG3:71 (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 ($#k6_qc_lang3 :::"Fixed"::: ) (Set "(" (Set (Var "p")) ($#k4_qc_lang2 :::"<=>"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_qc_lang3 :::"Fixed"::: ) (Set (Var "p")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k6_qc_lang3 :::"Fixed"::: ) (Set (Var "q")) ")" ))))) ; theorem :: QC_LANG3:72 (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 ($#k6_qc_lang3 :::"Fixed"::: ) (Set "(" ($#k5_qc_lang2 :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_qc_lang3 :::"Fixed"::: ) (Set (Var "p"))))))) ;