:: CQC_THE2 semantic presentation begin theorem :: CQC_THE2:1 (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 (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "r")) ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "r"))) "is" ($#v2_cqc_the1 :::"valid"::: ) ))) ; theorem :: CQC_THE2:2 (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 (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "r")) ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "q")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "p")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "r"))) "is" ($#v2_cqc_the1 :::"valid"::: ) ))) ; theorem :: CQC_THE2:3 (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 (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "r"))) "is" ($#v2_cqc_the1 :::"valid"::: ) )) "holds" (Bool (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "r")) ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) ))) ; theorem :: CQC_THE2:4 (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 (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "r"))) "is" ($#v2_cqc_the1 :::"valid"::: ) )) "holds" (Bool (Set (Set (Var "q")) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "r")) ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) ))) ; theorem :: CQC_THE2:5 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" ($#k15_qc_lang1 :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "s")) ")" ")" ))) "iff" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "s")))) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set (Var "x"))) ")" ) ")" )))) ; theorem :: CQC_THE2:6 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" ($#k5_qc_lang2 :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "s")) ")" ")" ))) "iff" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "s")))) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set (Var "x"))) ")" ) ")" )))) ; theorem :: CQC_THE2:7 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "s")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" (Set (Var "s")) ($#k2_qc_lang2 :::"=>"::: ) (Set (Var "h")) ")" ))) "iff" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "s")))) "or" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "h")))) ")" ) ")" )))) ; theorem :: CQC_THE2:8 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "s")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" (Set (Var "s")) ($#k14_qc_lang1 :::"'&'"::: ) (Set (Var "h")) ")" ))) "iff" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "s")))) "or" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "h")))) ")" ) ")" )))) ; theorem :: CQC_THE2:9 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "s")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" (Set (Var "s")) ($#k3_qc_lang2 :::"'or'"::: ) (Set (Var "h")) ")" ))) "iff" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "s")))) "or" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "h")))) ")" ) ")" )))) ; theorem :: CQC_THE2:10 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "s")) "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")) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" ($#k6_qc_lang2 :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "s")) ")" ")" )))) & (Bool (Bool "not" (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" ($#k6_qc_lang2 :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "s")) ")" ")" )))) ")" )))) ; theorem :: CQC_THE2:11 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "s")) "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")) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" ($#k7_qc_lang2 :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "s")) ")" ")" )))) & (Bool (Bool "not" (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set "(" ($#k7_qc_lang2 :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "s")) ")" ")" )))) ")" )))) ; theorem :: CQC_THE2:12 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "s")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set "(" (Set (Var "s")) ($#k2_qc_lang2 :::"=>"::: ) (Set (Var "h")) ")" ) ($#k13_cqc_lang :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k13_cqc_lang :::"."::: ) (Set (Var "x")) ")" ) ($#k2_qc_lang2 :::"=>"::: ) (Set "(" (Set (Var "h")) ($#k13_cqc_lang :::"."::: ) (Set (Var "x")) ")" )))))) ; theorem :: CQC_THE2:13 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "s")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set "(" (Set (Var "s")) ($#k3_qc_lang2 :::"'or'"::: ) (Set (Var "h")) ")" ) ($#k13_cqc_lang :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k13_cqc_lang :::"."::: ) (Set (Var "x")) ")" ) ($#k3_qc_lang2 :::"'or'"::: ) (Set "(" (Set (Var "h")) ($#k13_cqc_lang :::"."::: ) (Set (Var "x")) ")" )))))) ; theorem :: CQC_THE2:14 (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" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool (Set (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k13_cqc_lang :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k5_qc_lang2 :::"Ex"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k13_cqc_lang :::"."::: ) (Set (Var "y")) ")" ) ")" ))))) ; theorem :: CQC_THE2:15 (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 (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) )))) ; theorem :: CQC_THE2:16 (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")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v2_cqc_the1 :::"valid"::: ) )) "holds" (Bool (Set ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ) "is" ($#v2_cqc_the1 :::"valid"::: ) )))) ; theorem :: CQC_THE2:17 (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 (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) )))) ; theorem :: CQC_THE2:18 (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" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "y")) "," (Set (Var "p")) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) )))) ; theorem :: CQC_THE2:19 (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 (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q"))) "is" ($#v2_cqc_the1 :::"valid"::: ) ) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "q")))))) "holds" (Bool (Set (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q"))) "is" ($#v2_cqc_the1 :::"valid"::: ) )))) ; theorem :: CQC_THE2:20 (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")) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")))))) "holds" (Bool (Set (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "p"))) "is" ($#v2_cqc_the1 :::"valid"::: ) )))) ; theorem :: CQC_THE2:21 (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")) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p"))))) & (Bool (Set ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ) "is" ($#v2_cqc_the1 :::"valid"::: ) )) "holds" (Bool (Set (Var "p")) "is" ($#v2_cqc_the1 :::"valid"::: ) )))) ; theorem :: CQC_THE2:22 (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 "y")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "h")))))) "holds" (Bool (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "y")) "," (Set (Var "q")) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) ))))) ; theorem :: CQC_THE2:23 (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")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v2_cqc_the1 :::"valid"::: ) )) "holds" (Bool (Set ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ) "is" ($#v2_cqc_the1 :::"valid"::: ) )))) ; theorem :: CQC_THE2:24 (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")) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")))))) "holds" (Bool (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) )))) ; theorem :: CQC_THE2:25 (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")))))) "holds" (Bool (Set (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q"))) "is" ($#v2_cqc_the1 :::"valid"::: ) ))))) ; theorem :: CQC_THE2:26 (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 "y")) "," (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "st" (Bool (Bool (Bool "not" (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")))))) "holds" (Bool (Set (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "y")) "," (Set (Var "p")) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) )))) ; theorem :: CQC_THE2:27 (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 "p")))))) "holds" (Bool (Set (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "y")) "," (Set (Var "q")) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) ))))) ; theorem :: CQC_THE2:28 (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" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")))))) "holds" (Bool (Set (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "y")) "," (Set (Var "p")) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) )))) ; theorem :: CQC_THE2: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"))) (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 "q"))))) & (Bool (Bool "not" (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "h")))))) "holds" (Bool (Set (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "y")) "," (Set (Var "q")) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) ))))) ; theorem :: CQC_THE2: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" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" ) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" ) ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) )))) ; theorem :: CQC_THE2: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"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" ) ")" ) "is" ($#v2_cqc_the1 :::"valid"::: ) )) "holds" (Bool (Set (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) )))) ; theorem :: CQC_THE2: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"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k10_cqc_lang :::"<=>"::: ) (Set (Var "q")) ")" ) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k10_cqc_lang :::"<=>"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" ) ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) )))) ; theorem :: CQC_THE2: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" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k10_cqc_lang :::"<=>"::: ) (Set (Var "q")) ")" ) ")" ) "is" ($#v2_cqc_the1 :::"valid"::: ) )) "holds" (Bool (Set (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k10_cqc_lang :::"<=>"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) )))) ; theorem :: CQC_THE2:34 (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")) "holds" (Bool (Set (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" ) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" ) ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) )))) ; theorem :: CQC_THE2:35 (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 ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" ) ")" ) "is" ($#v2_cqc_the1 :::"valid"::: ) )) "holds" (Bool (Set (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) )))) ; theorem :: CQC_THE2:36 (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")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k7_cqc_lang :::"'&'"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" ) ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) ) & (Bool (Set (Set "(" (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k7_cqc_lang :::"'&'"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" ) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) ) ")" )))) ; theorem :: CQC_THE2: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")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ")" ")" ) ($#k10_cqc_lang :::"<=>"::: ) (Set "(" (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k7_cqc_lang :::"'&'"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" ) ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) )))) ; theorem :: CQC_THE2: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"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ")" ) "is" ($#v2_cqc_the1 :::"valid"::: ) ) "iff" (Bool (Set (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k7_cqc_lang :::"'&'"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) ) ")" )))) ; theorem :: CQC_THE2: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"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set "(" (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k9_cqc_lang :::"'or'"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" ) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "q")) ")" ) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) )))) ; theorem :: CQC_THE2: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" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "q")) ")" ) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k9_cqc_lang :::"'or'"::: ) (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" ) ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) ) & (Bool (Set (Set "(" (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k9_cqc_lang :::"'or'"::: ) (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" ) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "q")) ")" ) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) ) ")" )))) ; theorem :: CQC_THE2: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"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "q")) ")" ) ")" ")" ) ($#k10_cqc_lang :::"<=>"::: ) (Set "(" (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k9_cqc_lang :::"'or'"::: ) (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" ) ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) )))) ; theorem :: CQC_THE2:42 (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")) "holds" (Bool "(" (Bool (Set ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "q")) ")" ) ")" ) "is" ($#v2_cqc_the1 :::"valid"::: ) ) "iff" (Bool (Set (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k9_cqc_lang :::"'or'"::: ) (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) ) ")" )))) ; theorem :: CQC_THE2: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"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k7_cqc_lang :::"'&'"::: ) (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" ) ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) )))) ; theorem :: CQC_THE2: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" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ")" ) "is" ($#v2_cqc_the1 :::"valid"::: ) )) "holds" (Bool (Set (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k7_cqc_lang :::"'&'"::: ) (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) )))) ; theorem :: CQC_THE2:45 (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 "(" (Bool (Set (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ")" ) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) ) & (Bool (Set (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ")" ) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) ) ")" )))) ; theorem :: CQC_THE2:46 (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 (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ")" ) ")" ")" ) ($#k10_cqc_lang :::"<=>"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) )))) ; theorem :: CQC_THE2:47 (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 "(" (Bool (Set (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ")" ) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) ) & (Bool (Set (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ")" ) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) ) ")" )))) ; theorem :: CQC_THE2:48 (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 (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ")" ) ")" ")" ) ($#k10_cqc_lang :::"<=>"::: ) (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) )))) ; theorem :: CQC_THE2:49 (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 "(" (Bool (Set (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ")" ")" ) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) ) & (Bool (Set (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ")" ")" ) ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) ) ")" )))) ; theorem :: CQC_THE2:50 (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 (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ")" ")" ) ")" ) ($#k10_cqc_lang :::"<=>"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) )))) ; theorem :: CQC_THE2:51 (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 "(" (Bool (Set (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) ) & (Bool (Set (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) ) ")" )))) ; theorem :: CQC_THE2:52 (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 (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ")" ) ($#k10_cqc_lang :::"<=>"::: ) (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) )))) ; theorem :: CQC_THE2:53 (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 "(" (Bool (Set (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) ) & (Bool (Set (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) ) ")" )))) ; theorem :: CQC_THE2:54 (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 (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ")" ")" ) ($#k10_cqc_lang :::"<=>"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) )))) ; theorem :: CQC_THE2:55 (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" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "y")) "," (Set (Var "p")) ")" ")" ) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "y")) "," (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) ) & (Bool (Set (Set "(" ($#k6_qc_lang2 :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "p")) ")" ")" ) ($#k2_qc_lang2 :::"=>"::: ) (Set "(" ($#k6_qc_lang2 :::"All"::: ) "(" (Set (Var "y")) "," (Set (Var "x")) "," (Set (Var "p")) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) ) ")" )))) ; theorem :: CQC_THE2:56 (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 "y")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "h")))))) "holds" (Bool (Set (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "y")) "," (Set (Var "q")) ")" ")" ) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) ))))) ; theorem :: CQC_THE2:57 (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" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "y")) "," (Set (Var "p")) ")" ")" ) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "y")) "," (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) ) & (Bool (Set (Set "(" ($#k7_qc_lang2 :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "p")) ")" ")" ) ($#k2_qc_lang2 :::"=>"::: ) (Set "(" ($#k7_qc_lang2 :::"Ex"::: ) "(" (Set (Var "y")) "," (Set (Var "x")) "," (Set (Var "p")) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) ) ")" )))) ; theorem :: CQC_THE2: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 "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 "y")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "h")))))) "holds" (Bool (Set (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k2_qc_lang2 :::"=>"::: ) (Set "(" ($#k7_qc_lang2 :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "q")) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) ))))) ; theorem :: CQC_THE2:59 (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" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "y")) "," (Set (Var "p")) ")" ")" ) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "y")) "," (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) )))) ; theorem :: CQC_THE2:60 (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 ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k10_cqc_lang :::"<=>"::: ) (Set (Var "p")) ")" ) ")" ) "is" ($#v2_cqc_the1 :::"valid"::: ) )))) ; theorem :: CQC_THE2:61 (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")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" ) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" ) ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) ) & (Bool (Set (Set "(" (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" ) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" ) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) ) ")" )))) ; theorem :: CQC_THE2:62 (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")) "holds" (Bool (Set (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" ) ")" ")" ) ($#k10_cqc_lang :::"<=>"::: ) (Set "(" (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" ) ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) )))) ; theorem :: CQC_THE2:63 (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")) "holds" (Bool "(" (Bool (Set ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" ) ")" ) "is" ($#v2_cqc_the1 :::"valid"::: ) ) "iff" (Bool (Set (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) ) ")" )))) ; theorem :: CQC_THE2:64 (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")) "holds" (Bool (Set (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" ) ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) )))) ; theorem :: CQC_THE2: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 "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) )))) ; theorem :: CQC_THE2:66 (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 (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")))))) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" ) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) )))) ; theorem :: CQC_THE2:67 (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 (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p"))))) & (Bool (Set (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) )) "holds" (Bool (Set ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ")" ) "is" ($#v2_cqc_the1 :::"valid"::: ) )))) ; theorem :: CQC_THE2:68 (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 (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")))))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "p")) ($#k9_cqc_lang :::"'or'"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" ) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "q")) ")" ) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) ) & (Bool (Set (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "q")) ")" ) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k9_cqc_lang :::"'or'"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" ) ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) ) ")" )))) ; theorem :: CQC_THE2:69 (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 (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")))))) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k9_cqc_lang :::"'or'"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" ) ")" ) ($#k10_cqc_lang :::"<=>"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "q")) ")" ) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) )))) ; theorem :: CQC_THE2:70 (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 (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")))))) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k9_cqc_lang :::"'or'"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) ) "iff" (Bool (Set ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "q")) ")" ) ")" ) "is" ($#v2_cqc_the1 :::"valid"::: ) ) ")" )))) ; theorem :: CQC_THE2:71 (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 (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")))))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" ) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) ) & (Bool (Set (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" ) ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) ) ")" )))) ; theorem :: CQC_THE2:72 (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 (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")))))) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" ) ")" ) ($#k10_cqc_lang :::"<=>"::: ) (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) )))) ; theorem :: CQC_THE2:73 (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 (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")))))) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) ) "iff" (Bool (Set ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ")" ) "is" ($#v2_cqc_the1 :::"valid"::: ) ) ")" )))) ; theorem :: CQC_THE2:74 (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 (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")))))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" ) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" ) ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) ) & (Bool (Set (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" ) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" ) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) ) ")" )))) ; theorem :: CQC_THE2:75 (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 (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")))))) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" ) ")" ) ($#k10_cqc_lang :::"<=>"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" ) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) )))) ; theorem :: CQC_THE2:76 (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 (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")))))) "holds" (Bool "(" (Bool (Set ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" ) ")" ) "is" ($#v2_cqc_the1 :::"valid"::: ) ) "iff" (Bool (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) ) ")" )))) ; theorem :: CQC_THE2:77 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "q")) "," (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")) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "q")))))) "holds" (Bool (Set (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" ) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) )))) ; theorem :: CQC_THE2:78 (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")) "holds" (Bool (Set (Set "(" (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" ) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) )))) ; theorem :: CQC_THE2:79 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "q")) "," (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")) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "q")))))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q"))) "is" ($#v2_cqc_the1 :::"valid"::: ) ) "iff" (Bool (Set ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" ) ")" ) "is" ($#v2_cqc_the1 :::"valid"::: ) ) ")" )))) ; theorem :: CQC_THE2:80 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "q")) "," (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")) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "q")))))) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" ) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) ) & (Bool (Set (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" ) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) ) ")" )))) ; theorem :: CQC_THE2:81 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "q")) "," (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")) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "q")))))) "holds" (Bool (Set (Set "(" (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" ) ($#k10_cqc_lang :::"<=>"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" ) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) )))) ; theorem :: CQC_THE2:82 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "q")) "," (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")) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "q")))))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q"))) "is" ($#v2_cqc_the1 :::"valid"::: ) ) "iff" (Bool (Set ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" ) ")" ) "is" ($#v2_cqc_the1 :::"valid"::: ) ) ")" )))) ; theorem :: CQC_THE2:83 (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 (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")))))) "holds" (Bool (Set (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" ) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" ) ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) )))) ; theorem :: CQC_THE2:84 (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")) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" ) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" ) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) )))) ; theorem :: CQC_THE2:85 (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 (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")))))) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" ) ")" ) ($#k10_cqc_lang :::"<=>"::: ) (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" ) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) )))) ; theorem :: CQC_THE2:86 (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 (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")))))) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) ) "iff" (Bool (Set ($#k12_cqc_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" ) ")" ) "is" ($#v2_cqc_the1 :::"valid"::: ) ) ")" )))) ; theorem :: CQC_THE2:87 (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 ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) ) ($#r3_cqc_the1 :::"|-"::: ) (Set (Var "p"))))) ; theorem :: CQC_THE2:88 (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 ($#k1_cqc_the1 :::"Cn"::: ) (Set "(" (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "q")) ($#k6_domain_1 :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_cqc_the1 :::"Cn"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k6_domain_1 :::"}"::: ) ))))) ; theorem :: CQC_THE2:89 (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"))) "holds" (Bool "(" (Bool (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k7_domain_1 :::"}"::: ) ) ($#r3_cqc_the1 :::"|-"::: ) (Set (Var "r"))) "iff" (Bool (Set ($#k6_domain_1 :::"{"::: ) (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k6_domain_1 :::"}"::: ) ) ($#r3_cqc_the1 :::"|-"::: ) (Set (Var "r"))) ")" ))) ; theorem :: CQC_THE2:90 (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")) ")" ) (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")) "st" (Bool (Bool (Set (Var "X")) ($#r3_cqc_the1 :::"|-"::: ) (Set (Var "p")))) "holds" (Bool (Set (Var "X")) ($#r3_cqc_the1 :::"|-"::: ) (Set ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" )))))) ; theorem :: CQC_THE2:91 (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")) ")" ) (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 (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")))))) "holds" (Bool (Set (Var "X")) ($#r3_cqc_the1 :::"|-"::: ) (Set (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" ) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" ) ")" ))))))) ; theorem :: CQC_THE2:92 (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")) ")" ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "F")) "is" ($#v6_qc_lang1 :::"closed"::: ) ) & (Bool (Set (Set (Var "X")) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "F")) ($#k6_domain_1 :::"}"::: ) )) ($#r3_cqc_the1 :::"|-"::: ) (Set (Var "G")))) "holds" (Bool (Set (Var "X")) ($#r3_cqc_the1 :::"|-"::: ) (Set (Set (Var "F")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "G"))))))) ;