:: PROCAL_1 semantic presentation begin theorem :: PROCAL_1: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"))) "holds" (Bool (Set ($#k6_cqc_lang :::"'not'"::: ) (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1:2 (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 (Set (Var "p")) ($#k9_cqc_lang :::"'or'"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1: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"))) "holds" (Bool (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "q")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1:4 (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"))) "holds" (Bool (Set (Set (Var "q")) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "q")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1: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 (Set (Set "(" (Set (Var "p")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "q")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1: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 (Set (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set "(" (Set (Var "p")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "q")) ")" ) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ($#k7_cqc_lang :::"'&'"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "q")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1: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 (Set (Set "(" (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ($#k7_cqc_lang :::"'&'"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "q")) ")" ) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set "(" (Set (Var "p")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "q")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1:8 (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 "(" (Set (Var "p")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "q")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "p")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1:9 (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 (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1:10 (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 "(" ($#k6_cqc_lang :::"'not'"::: ) (Set "(" (Set (Var "p")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "q")) ")" ) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1:11 (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 (Set "(" (Set (Var "p")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "p")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1:12 (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 (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "p")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1:13 (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 "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1:14 (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 "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "q")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1:15 (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 "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "q")) ")" ) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1:16 (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 "(" ($#k6_cqc_lang :::"'not'"::: ) (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1:17 (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 "(" ($#k6_cqc_lang :::"'not'"::: ) (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ($#k9_cqc_lang :::"'or'"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "q")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1:18 (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 "(" (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ($#k9_cqc_lang :::"'or'"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "q")) ")" ) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1: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"))) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1:20 (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 "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "q")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1:21 (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 "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1:22 (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 (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "p")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1:23 (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 "(" (Set (Var "p")) ($#k10_cqc_lang :::"<=>"::: ) (Set (Var "q")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1:24 (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 "(" (Set (Var "p")) ($#k10_cqc_lang :::"<=>"::: ) (Set (Var "q")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "p")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1:25 (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 (Set (Set "(" (Set "(" (Set (Var "p")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "q")) ")" ) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "r")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k9_cqc_lang :::"'or'"::: ) (Set "(" (Set (Var "q")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "r")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1:26 (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 (Set (Set "(" (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "r")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set "(" (Set (Var "q")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "r")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1:27 (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 (Set (Set "(" (Set (Var "p")) ($#k9_cqc_lang :::"'or'"::: ) (Set "(" (Set (Var "q")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "r")) ")" ) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "q")) ")" ) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "r")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1:28 (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")) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1: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 (Set (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set "(" (Set (Var "q")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "p")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k10_cqc_lang :::"<=>"::: ) (Set (Var "q")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1: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"))) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "q")) ")" ) ($#k10_cqc_lang :::"<=>"::: ) (Set "(" (Set (Var "q")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "p")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1:31 (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 (Set (Set "(" (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "r")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "r")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1:32 (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 (Set (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "r")) ")" ) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "r")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1:33 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "r")) "," (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 "(" (Set (Var "r")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "p")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set "(" (Set (Var "r")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "r")) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1:34 (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 (Set (Set "(" (Set "(" (Set (Var "p")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "q")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "r")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "r")) ")" ) ($#k9_cqc_lang :::"'or'"::: ) (Set "(" (Set (Var "q")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "r")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1:35 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "r")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "r")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set "(" (Set (Var "q")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "r")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "q")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "r")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1:36 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "r")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "r")) ")" ) ($#k7_cqc_lang :::"'&'"::: ) (Set "(" (Set (Var "q")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "r")) ")" ) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "q")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "r")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1: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"))) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k7_cqc_lang :::"'&'"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1:38 (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 (Set (Set "(" (Set "(" (Set (Var "p")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "q")) ")" ) ($#k7_cqc_lang :::"'&'"::: ) (Set "(" (Set (Var "p")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "r")) ")" ) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k9_cqc_lang :::"'or'"::: ) (Set "(" (Set (Var "q")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "r")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1:39 (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 (Set (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set "(" (Set (Var "q")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "r")) ")" ) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k9_cqc_lang :::"'or'"::: ) (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "r")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1:40 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "r")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "A"))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "p")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "r")) ")" ) ($#k7_cqc_lang :::"'&'"::: ) (Set "(" (Set (Var "q")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "r")) ")" ) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "r")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1:41 (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 (Set (Set "(" (Set "(" (Set (Var "p")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "q")) ")" ) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "r")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "r")) ")" ) ($#k9_cqc_lang :::"'or'"::: ) (Set "(" (Set (Var "q")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "r")) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1: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"))) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set (Var "p")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1:43 (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"))) "st" (Bool (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set (Var "p")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1: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"))) "st" (Bool (Bool (Set (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1: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 (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1: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"))) "st" (Bool (Bool (Set (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set (Var "p")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1: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")) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1:48 (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 (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "r")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "r")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1:49 (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 (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set "(" (Set (Var "r")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "p")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "r")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "q")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1:50 (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 (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set "(" (Set (Var "r")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "p")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "r")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1: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 (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "r")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "r")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1:52 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "r")) "," (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 "r")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))) & (Bool (Set (Set (Var "r")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set (Var "r")) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1:53 (Bool "for" (Set (Var "A")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "r")) "," (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 "r"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))) & (Bool (Set (Set (Var "q")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "r"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "q")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "r"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1:54 (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")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))) & (Bool (Set ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1:55 (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")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))) & (Bool (Set ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1: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 (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))) & (Bool (Set (Set (Var "r")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "s"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "r")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "s")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1: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 (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))) & (Bool (Set (Set (Var "r")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "s"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "r")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k9_cqc_lang :::"'or'"::: ) (Set (Var "s")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ; theorem :: PROCAL_1: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"))) "st" (Bool (Bool (Set (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "q")) ")" ) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "A")))))) ;