:: CQC_THE3 semantic presentation begin theorem :: CQC_THE3:1 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "X")) ($#r3_cqc_the1 :::"|-"::: ) (Set (Var "p")))))) ; theorem :: CQC_THE3:2 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k1_cqc_the1 :::"Cn"::: ) (Set (Var "Y"))))) "holds" (Bool (Set ($#k1_cqc_the1 :::"Cn"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_cqc_the1 :::"Cn"::: ) (Set (Var "Y")))))) ; theorem :: CQC_THE3:3 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Var "X")) ($#r3_cqc_the1 :::"|-"::: ) (Set (Var "p"))) & (Bool (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) ) ($#r3_cqc_the1 :::"|-"::: ) (Set (Var "q")))) "holds" (Bool (Set (Var "X")) ($#r3_cqc_the1 :::"|-"::: ) (Set (Var "q")))))) ; theorem :: CQC_THE3:4 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Var "X")) ($#r3_cqc_the1 :::"|-"::: ) (Set (Var "p"))) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "Y")) ($#r3_cqc_the1 :::"|-"::: ) (Set (Var "p")))))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "p", "q" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "A"))); pred "p" :::"|-"::: "q" means :: CQC_THE3:def 1 (Bool (Set ($#k6_domain_1 :::"{"::: ) "p" ($#k6_domain_1 :::"}"::: ) ) ($#r3_cqc_the1 :::"|-"::: ) "q"); end; :: deftheorem defines :::"|-"::: CQC_THE3:def 1 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_cqc_the3 :::"|-"::: ) (Set (Var "q"))) "iff" (Bool (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) ) ($#r3_cqc_the1 :::"|-"::: ) (Set (Var "q"))) ")" ))); theorem :: CQC_THE3:5 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set (Var "p")) ($#r1_cqc_the3 :::"|-"::: ) (Set (Var "p"))))) ; theorem :: CQC_THE3:6 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "p")) ($#r1_cqc_the3 :::"|-"::: ) (Set (Var "q"))) & (Bool (Set (Var "q")) ($#r1_cqc_the3 :::"|-"::: ) (Set (Var "r")))) "holds" (Bool (Set (Var "p")) ($#r1_cqc_the3 :::"|-"::: ) (Set (Var "r"))))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "X", "Y" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "A")) ")" ); pred "X" :::"|-"::: "Y" means :: CQC_THE3:def 2 (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) "A") "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) "Y")) "holds" (Bool "X" ($#r3_cqc_the1 :::"|-"::: ) (Set (Var "p")))); end; :: deftheorem defines :::"|-"::: CQC_THE3:def 2 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r2_cqc_the3 :::"|-"::: ) (Set (Var "Y"))) "iff" (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "X")) ($#r3_cqc_the1 :::"|-"::: ) (Set (Var "p")))) ")" ))); theorem :: CQC_THE3:7 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r2_cqc_the3 :::"|-"::: ) (Set (Var "Y"))) "iff" (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set ($#k1_cqc_the1 :::"Cn"::: ) (Set (Var "X")))) ")" ))) ; theorem :: CQC_THE3:8 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" ) "holds" (Bool (Set (Var "X")) ($#r2_cqc_the3 :::"|-"::: ) (Set (Var "X"))))) ; theorem :: CQC_THE3:9 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Var "X")) ($#r2_cqc_the3 :::"|-"::: ) (Set (Var "Y"))) & (Bool (Set (Var "Y")) ($#r2_cqc_the3 :::"|-"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Var "X")) ($#r2_cqc_the3 :::"|-"::: ) (Set (Var "Z"))))) ; theorem :: CQC_THE3:10 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r2_cqc_the3 :::"|-"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) )) "iff" (Bool (Set (Var "X")) ($#r3_cqc_the1 :::"|-"::: ) (Set (Var "p"))) ")" )))) ; theorem :: CQC_THE3:11 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) ) ($#r2_cqc_the3 :::"|-"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "q")) ($#k6_domain_1 :::"}"::: ) )) "iff" (Bool (Set (Var "p")) ($#r1_cqc_the3 :::"|-"::: ) (Set (Var "q"))) ")" ))) ; theorem :: CQC_THE3:12 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "Y")) ($#r2_cqc_the3 :::"|-"::: ) (Set (Var "X"))))) ; theorem :: CQC_THE3:13 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" ) "holds" (Bool (Set (Var "X")) ($#r2_cqc_the3 :::"|-"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: CQC_THE3:14 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) "holds" (Bool (Set ($#k1_subset_1 :::"{}"::: ) (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" )) ($#r2_cqc_the3 :::"|-"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A"))))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "A")) ")" ); pred :::"|-"::: "X" means :: CQC_THE3:def 3 (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) "A") "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool (Set (Var "p")) "is" ($#v2_cqc_the1 :::"valid"::: ) )); end; :: deftheorem defines :::"|-"::: CQC_THE3:def 3 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" ) "holds" (Bool "(" (Bool ($#r3_cqc_the3 :::"|-"::: ) (Set (Var "X"))) "iff" (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "p")) "is" ($#v2_cqc_the1 :::"valid"::: ) )) ")" ))); theorem :: CQC_THE3:15 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" ) "holds" (Bool "(" (Bool ($#r3_cqc_the3 :::"|-"::: ) (Set (Var "X"))) "iff" (Bool (Set ($#k1_subset_1 :::"{}"::: ) (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" )) ($#r2_cqc_the3 :::"|-"::: ) (Set (Var "X"))) ")" ))) ; theorem :: CQC_THE3:16 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) "holds" (Bool ($#r3_cqc_the3 :::"|-"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A"))))) ; theorem :: CQC_THE3:17 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" ) "holds" (Bool "(" (Bool ($#r3_cqc_the3 :::"|-"::: ) (Set (Var "X"))) "iff" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))) ")" ))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "X", "Y" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "A")) ")" ); pred "X" :::"|-|"::: "Y" means :: CQC_THE3:def 4 (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) "A") "holds" (Bool "(" (Bool "X" ($#r3_cqc_the1 :::"|-"::: ) (Set (Var "p"))) "iff" (Bool "Y" ($#r3_cqc_the1 :::"|-"::: ) (Set (Var "p"))) ")" )); reflexivity (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "A")) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "A"))) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r3_cqc_the1 :::"|-"::: ) (Set (Var "p"))) "iff" (Bool (Set (Var "X")) ($#r3_cqc_the1 :::"|-"::: ) (Set (Var "p"))) ")" ))) ; symmetry (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "A")) ")" ) "st" (Bool (Bool "(" "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "A"))) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r3_cqc_the1 :::"|-"::: ) (Set (Var "p"))) "iff" (Bool (Set (Var "Y")) ($#r3_cqc_the1 :::"|-"::: ) (Set (Var "p"))) ")" ) ")" )) "holds" (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "A"))) "holds" (Bool "(" (Bool (Set (Var "Y")) ($#r3_cqc_the1 :::"|-"::: ) (Set (Var "p"))) "iff" (Bool (Set (Var "X")) ($#r3_cqc_the1 :::"|-"::: ) (Set (Var "p"))) ")" ))) ; end; :: deftheorem defines :::"|-|"::: CQC_THE3:def 4 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r4_cqc_the3 :::"|-|"::: ) (Set (Var "Y"))) "iff" (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r3_cqc_the1 :::"|-"::: ) (Set (Var "p"))) "iff" (Bool (Set (Var "Y")) ($#r3_cqc_the1 :::"|-"::: ) (Set (Var "p"))) ")" )) ")" ))); theorem :: CQC_THE3:18 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r4_cqc_the3 :::"|-|"::: ) (Set (Var "Y"))) "iff" (Bool "(" (Bool (Set (Var "X")) ($#r2_cqc_the3 :::"|-"::: ) (Set (Var "Y"))) & (Bool (Set (Var "Y")) ($#r2_cqc_the3 :::"|-"::: ) (Set (Var "X"))) ")" ) ")" ))) ; theorem :: CQC_THE3:19 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Var "X")) ($#r4_cqc_the3 :::"|-|"::: ) (Set (Var "Y"))) & (Bool (Set (Var "Y")) ($#r4_cqc_the3 :::"|-|"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Var "X")) ($#r4_cqc_the3 :::"|-|"::: ) (Set (Var "Z"))))) ; theorem :: CQC_THE3:20 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r4_cqc_the3 :::"|-|"::: ) (Set (Var "Y"))) "iff" (Bool (Set ($#k1_cqc_the1 :::"Cn"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_cqc_the1 :::"Cn"::: ) (Set (Var "Y")))) ")" ))) ; theorem :: CQC_THE3:21 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" ) "holds" (Bool (Set (Set "(" ($#k1_cqc_the1 :::"Cn"::: ) (Set (Var "X")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_cqc_the1 :::"Cn"::: ) (Set (Var "Y")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k1_cqc_the1 :::"Cn"::: ) (Set "(" (Set (Var "X")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "Y")) ")" ))))) ; theorem :: CQC_THE3:22 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" ) "holds" (Bool (Set ($#k1_cqc_the1 :::"Cn"::: ) (Set "(" (Set (Var "X")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "Y")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_cqc_the1 :::"Cn"::: ) (Set "(" (Set "(" ($#k1_cqc_the1 :::"Cn"::: ) (Set (Var "X")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_cqc_the1 :::"Cn"::: ) (Set (Var "Y")) ")" ) ")" ))))) ; theorem :: CQC_THE3:23 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" ) "holds" (Bool (Set (Var "X")) ($#r4_cqc_the3 :::"|-|"::: ) (Set ($#k1_cqc_the1 :::"Cn"::: ) (Set (Var "X")))))) ; theorem :: CQC_THE3:24 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" ) "holds" (Bool (Set (Set (Var "X")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "Y"))) ($#r4_cqc_the3 :::"|-|"::: ) (Set (Set "(" ($#k1_cqc_the1 :::"Cn"::: ) (Set (Var "X")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_cqc_the1 :::"Cn"::: ) (Set (Var "Y")) ")" ))))) ; theorem :: CQC_THE3:25 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Var "X1")) ($#r4_cqc_the3 :::"|-|"::: ) (Set (Var "X2")))) "holds" (Bool (Set (Set (Var "X1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "Y"))) ($#r4_cqc_the3 :::"|-|"::: ) (Set (Set (Var "X2")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "Y")))))) ; theorem :: CQC_THE3:26 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Var "X1")) ($#r4_cqc_the3 :::"|-|"::: ) (Set (Var "X2"))) & (Bool (Set (Set (Var "X1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "Y"))) ($#r2_cqc_the3 :::"|-"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set (Var "X2")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "Y"))) ($#r2_cqc_the3 :::"|-"::: ) (Set (Var "Z"))))) ; theorem :: CQC_THE3:27 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Var "X1")) ($#r4_cqc_the3 :::"|-|"::: ) (Set (Var "X2"))) & (Bool (Set (Var "Y")) ($#r2_cqc_the3 :::"|-"::: ) (Set (Var "X1")))) "holds" (Bool (Set (Var "Y")) ($#r2_cqc_the3 :::"|-"::: ) (Set (Var "X2"))))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "p", "q" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "A"))); pred "p" :::"|-|"::: "q" means :: CQC_THE3:def 5 (Bool "(" (Bool "p" ($#r1_cqc_the3 :::"|-"::: ) "q") & (Bool "q" ($#r1_cqc_the3 :::"|-"::: ) "p") ")" ); reflexivity (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "A"))) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_cqc_the3 :::"|-"::: ) (Set (Var "p"))) & (Bool (Set (Var "p")) ($#r1_cqc_the3 :::"|-"::: ) (Set (Var "p"))) ")" )) ; symmetry (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "A"))) "st" (Bool (Bool (Set (Var "p")) ($#r1_cqc_the3 :::"|-"::: ) (Set (Var "q"))) & (Bool (Set (Var "q")) ($#r1_cqc_the3 :::"|-"::: ) (Set (Var "p")))) "holds" (Bool "(" (Bool (Set (Var "q")) ($#r1_cqc_the3 :::"|-"::: ) (Set (Var "p"))) & (Bool (Set (Var "p")) ($#r1_cqc_the3 :::"|-"::: ) (Set (Var "q"))) ")" )) ; end; :: deftheorem defines :::"|-|"::: CQC_THE3:def 5 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r5_cqc_the3 :::"|-|"::: ) (Set (Var "q"))) "iff" (Bool "(" (Bool (Set (Var "p")) ($#r1_cqc_the3 :::"|-"::: ) (Set (Var "q"))) & (Bool (Set (Var "q")) ($#r1_cqc_the3 :::"|-"::: ) (Set (Var "p"))) ")" ) ")" ))); theorem :: CQC_THE3:28 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "p")) ($#r5_cqc_the3 :::"|-|"::: ) (Set (Var "q"))) & (Bool (Set (Var "q")) ($#r5_cqc_the3 :::"|-|"::: ) (Set (Var "r")))) "holds" (Bool (Set (Var "p")) ($#r5_cqc_the3 :::"|-|"::: ) (Set (Var "r"))))) ; theorem :: CQC_THE3:29 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r5_cqc_the3 :::"|-|"::: ) (Set (Var "q"))) "iff" (Bool (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) ) ($#r4_cqc_the3 :::"|-|"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "q")) ($#k6_domain_1 :::"}"::: ) )) ")" ))) ; theorem :: CQC_THE3:30 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r5_cqc_the3 :::"|-|"::: ) (Set (Var "q"))) & (Bool (Set (Var "X")) ($#r3_cqc_the1 :::"|-"::: ) (Set (Var "p")))) "holds" (Bool (Set (Var "X")) ($#r3_cqc_the1 :::"|-"::: ) (Set (Var "q")))))) ; theorem :: CQC_THE3:31 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k7_domain_1 :::"}"::: ) ) ($#r4_cqc_the3 :::"|-|"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k6_domain_1 :::"}"::: ) )))) ; theorem :: CQC_THE3:32 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q"))) ($#r5_cqc_the3 :::"|-|"::: ) (Set (Set (Var "q")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "p")))))) ; theorem :: CQC_THE3:33 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r3_cqc_the1 :::"|-"::: ) (Set (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")))) "iff" (Bool "(" (Bool (Set (Var "X")) ($#r3_cqc_the1 :::"|-"::: ) (Set (Var "p"))) & (Bool (Set (Var "X")) ($#r3_cqc_the1 :::"|-"::: ) (Set (Var "q"))) ")" ) ")" )))) ; theorem :: CQC_THE3:34 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "p")) ($#r5_cqc_the3 :::"|-|"::: ) (Set (Var "q"))) & (Bool (Set (Var "r")) ($#r5_cqc_the3 :::"|-|"::: ) (Set (Var "s")))) "holds" (Bool (Set (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "r"))) ($#r5_cqc_the3 :::"|-|"::: ) (Set (Set (Var "q")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "s")))))) ; theorem :: CQC_THE3:35 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-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 "X")) ($#r3_cqc_the1 :::"|-"::: ) (Set ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" )) "iff" (Bool (Set (Var "X")) ($#r3_cqc_the1 :::"|-"::: ) (Set (Var "p"))) ")" ))))) ; theorem :: CQC_THE3:36 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ) ($#r5_cqc_the3 :::"|-|"::: ) (Set (Var "p")))))) ; theorem :: CQC_THE3:37 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "p")) ($#r5_cqc_the3 :::"|-|"::: ) (Set (Var "q")))) "holds" (Bool (Set ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ) ($#r5_cqc_the3 :::"|-|"::: ) (Set ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "y")) "," (Set (Var "q")) ")" ))))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "p", "q" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "A"))); pred "p" :::"is_an_universal_closure_of"::: "q" means :: CQC_THE3:def 6 (Bool "(" (Bool "p" "is" ($#v6_qc_lang1 :::"closed"::: ) ) & (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool "ex" (Set (Var "L")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (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 :::"="::: ) "q") & (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) "p") & (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 "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" "A"(Bool "ex" (Set (Var "r")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) "A") "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")))) & (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" )) ")" ))) ")" ) ")" )) ")" )) ")" ); end; :: deftheorem defines :::"is_an_universal_closure_of"::: CQC_THE3:def 6 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r6_cqc_the3 :::"is_an_universal_closure_of"::: ) (Set (Var "q"))) "iff" (Bool "(" (Bool (Set (Var "p")) "is" ($#v6_qc_lang1 :::"closed"::: ) ) & (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool "ex" (Set (Var "L")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (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 "q"))) & (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (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 "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A"))(Bool "ex" (Set (Var "r")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")))) & (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" )) ")" ))) ")" ) ")" )) ")" )) ")" ) ")" ))); theorem :: CQC_THE3:38 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "p")) ($#r6_cqc_the3 :::"is_an_universal_closure_of"::: ) (Set (Var "q")))) "holds" (Bool (Set (Var "p")) ($#r5_cqc_the3 :::"|-|"::: ) (Set (Var "q"))))) ; theorem :: CQC_THE3:39 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q"))) "is" ($#v2_cqc_the1 :::"valid"::: ) )) "holds" (Bool (Set (Var "p")) ($#r1_cqc_the3 :::"|-"::: ) (Set (Var "q"))))) ; theorem :: CQC_THE3:40 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Var "X")) ($#r3_cqc_the1 :::"|-"::: ) (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q"))))) "holds" (Bool (Set (Set (Var "X")) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) )) ($#r3_cqc_the1 :::"|-"::: ) (Set (Var "q")))))) ; theorem :: CQC_THE3:41 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "p")) "is" ($#v6_qc_lang1 :::"closed"::: ) ) & (Bool (Set (Var "p")) ($#r1_cqc_the3 :::"|-"::: ) (Set (Var "q")))) "holds" (Bool (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q"))) "is" ($#v2_cqc_the1 :::"valid"::: ) ))) ; theorem :: CQC_THE3:42 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Var "p1")) ($#r6_cqc_the3 :::"is_an_universal_closure_of"::: ) (Set (Var "p")))) "holds" (Bool "(" (Bool (Set (Set (Var "X")) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) )) ($#r3_cqc_the1 :::"|-"::: ) (Set (Var "q"))) "iff" (Bool (Set (Var "X")) ($#r3_cqc_the1 :::"|-"::: ) (Set (Set (Var "p1")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")))) ")" )))) ; theorem :: CQC_THE3:43 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "p")) "is" ($#v6_qc_lang1 :::"closed"::: ) ) & (Bool (Set (Var "p")) ($#r1_cqc_the3 :::"|-"::: ) (Set (Var "q")))) "holds" (Bool (Set ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "q"))) ($#r1_cqc_the3 :::"|-"::: ) (Set ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")))))) ; theorem :: CQC_THE3:44 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Var "p")) "is" ($#v6_qc_lang1 :::"closed"::: ) ) & (Bool (Set (Set (Var "X")) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) )) ($#r3_cqc_the1 :::"|-"::: ) (Set (Var "q")))) "holds" (Bool (Set (Set (Var "X")) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "q")) ")" ) ($#k6_domain_1 :::"}"::: ) )) ($#r3_cqc_the1 :::"|-"::: ) (Set ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p"))))))) ; theorem :: CQC_THE3:45 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "p")) "is" ($#v6_qc_lang1 :::"closed"::: ) ) & (Bool (Set ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p"))) ($#r1_cqc_the3 :::"|-"::: ) (Set ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "q"))))) "holds" (Bool (Set (Var "q")) ($#r1_cqc_the3 :::"|-"::: ) (Set (Var "p"))))) ; theorem :: CQC_THE3:46 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Var "p")) "is" ($#v6_qc_lang1 :::"closed"::: ) ) & (Bool (Set (Set (Var "X")) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ($#k6_domain_1 :::"}"::: ) )) ($#r3_cqc_the1 :::"|-"::: ) (Set ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "q"))))) "holds" (Bool (Set (Set (Var "X")) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "q")) ($#k6_domain_1 :::"}"::: ) )) ($#r3_cqc_the1 :::"|-"::: ) (Set (Var "p")))))) ; theorem :: CQC_THE3:47 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "p")) "is" ($#v6_qc_lang1 :::"closed"::: ) ) & (Bool (Set (Var "q")) "is" ($#v6_qc_lang1 :::"closed"::: ) )) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_cqc_the3 :::"|-"::: ) (Set (Var "q"))) "iff" (Bool (Set ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "q"))) ($#r1_cqc_the3 :::"|-"::: ) (Set ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")))) ")" ))) ; theorem :: CQC_THE3:48 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p")) "," (Set (Var "q1")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "p1")) ($#r6_cqc_the3 :::"is_an_universal_closure_of"::: ) (Set (Var "p"))) & (Bool (Set (Var "q1")) ($#r6_cqc_the3 :::"is_an_universal_closure_of"::: ) (Set (Var "q")))) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_cqc_the3 :::"|-"::: ) (Set (Var "q"))) "iff" (Bool (Set ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "q1"))) ($#r1_cqc_the3 :::"|-"::: ) (Set ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p1")))) ")" ))) ; theorem :: CQC_THE3:49 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p")) "," (Set (Var "q1")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "p1")) ($#r6_cqc_the3 :::"is_an_universal_closure_of"::: ) (Set (Var "p"))) & (Bool (Set (Var "q1")) ($#r6_cqc_the3 :::"is_an_universal_closure_of"::: ) (Set (Var "q")))) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r5_cqc_the3 :::"|-|"::: ) (Set (Var "q"))) "iff" (Bool (Set ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p1"))) ($#r5_cqc_the3 :::"|-|"::: ) (Set ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "q1")))) ")" ))) ; definitionlet "A" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "p", "q" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "A"))); pred "p" :::"<==>"::: "q" means :: CQC_THE3:def 7 (Bool (Set "p" ($#k10_cqc_lang :::"<=>"::: ) "q") "is" ($#v2_cqc_the1 :::"valid"::: ) ); reflexivity (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "A"))) "holds" (Bool (Set (Set (Var "p")) ($#k10_cqc_lang :::"<=>"::: ) (Set (Var "p"))) "is" ($#v2_cqc_the1 :::"valid"::: ) )) ; symmetry (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "A"))) "st" (Bool (Bool (Set (Set (Var "p")) ($#k10_cqc_lang :::"<=>"::: ) (Set (Var "q"))) "is" ($#v2_cqc_the1 :::"valid"::: ) )) "holds" (Bool (Set (Set (Var "q")) ($#k10_cqc_lang :::"<=>"::: ) (Set (Var "p"))) "is" ($#v2_cqc_the1 :::"valid"::: ) )) ; end; :: deftheorem defines :::"<==>"::: CQC_THE3:def 7 : (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r7_cqc_the3 :::"<==>"::: ) (Set (Var "q"))) "iff" (Bool (Set (Set (Var "p")) ($#k10_cqc_lang :::"<=>"::: ) (Set (Var "q"))) "is" ($#v2_cqc_the1 :::"valid"::: ) ) ")" ))); theorem :: CQC_THE3:50 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r7_cqc_the3 :::"<==>"::: ) (Set (Var "q"))) "iff" (Bool "(" (Bool (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q"))) "is" ($#v2_cqc_the1 :::"valid"::: ) ) & (Bool (Set (Set (Var "q")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "p"))) "is" ($#v2_cqc_the1 :::"valid"::: ) ) ")" ) ")" ))) ; theorem :: CQC_THE3:51 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "p")) ($#r7_cqc_the3 :::"<==>"::: ) (Set (Var "q"))) & (Bool (Set (Var "q")) ($#r7_cqc_the3 :::"<==>"::: ) (Set (Var "r")))) "holds" (Bool (Set (Var "p")) ($#r7_cqc_the3 :::"<==>"::: ) (Set (Var "r"))))) ; theorem :: CQC_THE3:52 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "p")) ($#r7_cqc_the3 :::"<==>"::: ) (Set (Var "q")))) "holds" (Bool (Set (Var "p")) ($#r5_cqc_the3 :::"|-|"::: ) (Set (Var "q"))))) ; theorem :: CQC_THE3:53 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r7_cqc_the3 :::"<==>"::: ) (Set (Var "q"))) "iff" (Bool (Set ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p"))) ($#r7_cqc_the3 :::"<==>"::: ) (Set ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "q")))) ")" ))) ; theorem :: CQC_THE3:54 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "p")) ($#r7_cqc_the3 :::"<==>"::: ) (Set (Var "q"))) & (Bool (Set (Var "r")) ($#r7_cqc_the3 :::"<==>"::: ) (Set (Var "s")))) "holds" (Bool (Set (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "r"))) ($#r7_cqc_the3 :::"<==>"::: ) (Set (Set (Var "q")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "s")))))) ; theorem :: CQC_THE3:55 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "p")) ($#r7_cqc_the3 :::"<==>"::: ) (Set (Var "q"))) & (Bool (Set (Var "r")) ($#r7_cqc_the3 :::"<==>"::: ) (Set (Var "s")))) "holds" (Bool (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "r"))) ($#r7_cqc_the3 :::"<==>"::: ) (Set (Set (Var "q")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "s")))))) ; theorem :: CQC_THE3:56 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "p")) ($#r7_cqc_the3 :::"<==>"::: ) (Set (Var "q"))) & (Bool (Set (Var "r")) ($#r7_cqc_the3 :::"<==>"::: ) (Set (Var "s")))) "holds" (Bool (Set (Set (Var "p")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "r"))) ($#r7_cqc_the3 :::"<==>"::: ) (Set (Set (Var "q")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "s")))))) ; theorem :: CQC_THE3:57 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "p")) ($#r7_cqc_the3 :::"<==>"::: ) (Set (Var "q"))) & (Bool (Set (Var "r")) ($#r7_cqc_the3 :::"<==>"::: ) (Set (Var "s")))) "holds" (Bool (Set (Set (Var "p")) ($#k10_cqc_lang :::"<=>"::: ) (Set (Var "r"))) ($#r7_cqc_the3 :::"<==>"::: ) (Set (Set (Var "q")) ($#k10_cqc_lang :::"<=>"::: ) (Set (Var "s")))))) ; theorem :: CQC_THE3:58 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "p")) ($#r7_cqc_the3 :::"<==>"::: ) (Set (Var "q")))) "holds" (Bool (Set ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ) ($#r7_cqc_the3 :::"<==>"::: ) (Set ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ))))) ; theorem :: CQC_THE3:59 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "p")) ($#r7_cqc_the3 :::"<==>"::: ) (Set (Var "q")))) "holds" (Bool (Set ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ) ($#r7_cqc_the3 :::"<==>"::: ) (Set ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ))))) ; theorem :: CQC_THE3:60 (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 "l")) "being" ($#m2_finseq_1 :::"QC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "A")) (Bool "for" (Set (Var "a")) "being" ($#m2_subset_1 :::"free_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k23_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "l"))) ($#r1_tarski :::"c="::: ) (Set ($#k23_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" ($#k1_cqc_lang :::"Subst"::: ) "(" (Set (Var "l")) "," (Set "(" (Set (Var "a")) ($#k2_cqc_lang :::".-->"::: ) (Set (Var "x")) ")" ) ")" ")" )))))))) ; theorem :: CQC_THE3:61 (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 "l")) "being" ($#m2_finseq_1 :::"QC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "A")) (Bool "for" (Set (Var "a")) "being" ($#m2_subset_1 :::"free_QC-variable":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k23_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" ($#k1_cqc_lang :::"Subst"::: ) "(" (Set (Var "l")) "," (Set "(" (Set (Var "a")) ($#k2_cqc_lang :::".-->"::: ) (Set (Var "x")) ")" ) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k23_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "l")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )))))))) ; theorem :: CQC_THE3: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 "h")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "h"))) ($#r1_tarski :::"c="::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" (Set (Var "h")) ($#k13_cqc_lang :::"."::: ) (Set (Var "x")) ")" )))))) ; theorem :: CQC_THE3:63 (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 :::"QC-formula":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" (Set (Var "h")) ($#k13_cqc_lang :::"."::: ) (Set (Var "x")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "h")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )))))) ; theorem :: CQC_THE3:64 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k13_cqc_lang :::"."::: ) (Set (Var "x")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool (Bool "not" (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "h")))))) "holds" (Bool "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p"))))))))) ; theorem :: CQC_THE3:65 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k13_cqc_lang :::"."::: ) (Set (Var "x")))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k13_cqc_lang :::"."::: ) (Set (Var "y")))) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "h"))))) & (Bool (Bool "not" (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "h")))))) "holds" (Bool (Set ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ) ($#r7_cqc_the3 :::"<==>"::: ) (Set ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "y")) "," (Set (Var "q")) ")" )))))) ;