:: CQC_THE1 semantic presentation begin theorem :: CQC_THE1:1 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "{" (Set (Var "k")) where k "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1))) "}" ($#r1_hidden :::"="::: ) (Set "{" (Set (Var "i")) where i "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) "}" ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k1_tarski :::"}"::: ) )))) ; theorem :: CQC_THE1:2 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "{" (Set (Var "k")) where k "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) "}" "is" ($#v1_finset_1 :::"finite"::: ) )) ; theorem :: CQC_THE1:3 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "Z")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool "ex" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Var "B")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "Z"))) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) )) ")" ))) ; theorem :: CQC_THE1:4 (Bool "for" (Set (Var "X")) "," (Set (Var "Z")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "Z")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "Z")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool "ex" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "Z")) ($#k2_zfmisc_1 :::":]"::: ) )) ")" ))) ; definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "T" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "Al")) ")" ); attr "T" is :::"being_a_theory"::: means :: CQC_THE1:def 1 (Bool "(" (Bool (Set ($#k5_cqc_lang :::"VERUM"::: ) "Al") ($#r2_hidden :::"in"::: ) "T") & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) "Al") (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" "Al" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" "Al" "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "p")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) "T") & (Bool (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" )) ($#r2_hidden :::"in"::: ) "T") & (Bool (Set (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set "(" (Set (Var "q")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "r")) ")" ) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "r")) ")" ) ")" ) ")" )) ($#r2_hidden :::"in"::: ) "T") & (Bool (Set (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "p")) ")" )) ($#r2_hidden :::"in"::: ) "T") & "(" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) "T") & (Bool (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) "T")) "implies" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) "T") ")" & (Bool (Set (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) "T") & "(" (Bool (Bool (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) "T") & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")))))) "implies" (Bool (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" )) ($#r2_hidden :::"in"::: ) "T") ")" & "(" (Bool (Bool (Set (Set (Var "s")) ($#k13_cqc_lang :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) "Al")) & (Bool (Set (Set (Var "s")) ($#k13_cqc_lang :::"."::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) "Al")) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "s"))))) & (Bool (Set (Set (Var "s")) ($#k13_cqc_lang :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) "T")) "implies" (Bool (Set (Set (Var "s")) ($#k13_cqc_lang :::"."::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) "T") ")" ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"being_a_theory"::: CQC_THE1:def 1 : (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")) ")" ) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v1_cqc_the1 :::"being_a_theory"::: ) ) "iff" (Bool "(" (Bool (Set ($#k5_cqc_lang :::"VERUM"::: ) (Set (Var "Al"))) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (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 "Al"))) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "p")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set "(" (Set (Var "q")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "r")) ")" ) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "r")) ")" ) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "p")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & "(" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "T")))) "implies" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) ")" & (Bool (Set (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & "(" (Bool (Bool (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p")))))) "implies" (Bool (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) ")" & "(" (Bool (Bool (Set (Set (Var "s")) ($#k13_cqc_lang :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")))) & (Bool (Set (Set (Var "s")) ($#k13_cqc_lang :::"."::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")))) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "s"))))) & (Bool (Set (Set (Var "s")) ($#k13_cqc_lang :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set (Var "T")))) "implies" (Bool (Set (Set (Var "s")) ($#k13_cqc_lang :::"."::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) ")" ")" ))) ")" ) ")" ) ")" ))); theorem :: CQC_THE1:5 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "T")) "," (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")) ")" ) "st" (Bool (Bool (Set (Var "T")) "is" ($#v1_cqc_the1 :::"being_a_theory"::: ) ) & (Bool (Set (Var "S")) "is" ($#v1_cqc_the1 :::"being_a_theory"::: ) )) "holds" (Bool (Set (Set (Var "T")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "S"))) "is" ($#v1_cqc_the1 :::"being_a_theory"::: ) ))) ; definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "Al")) ")" ); func :::"Cn"::: "X" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) "Al" ")" ) means :: CQC_THE1:def 2 (Bool "for" (Set (Var "t")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) "Al") "holds" (Bool "(" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) "Al" ")" ) "st" (Bool (Bool (Set (Var "T")) "is" ($#v1_cqc_the1 :::"being_a_theory"::: ) ) & (Bool "X" ($#r1_tarski :::"c="::: ) (Set (Var "T")))) "holds" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set (Var "T")))) ")" )); end; :: deftheorem defines :::"Cn"::: CQC_THE1:def 2 : (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_cqc_the1 :::"Cn"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "t")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) "holds" (Bool "(" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")) ")" ) "st" (Bool (Bool (Set (Var "T")) "is" ($#v1_cqc_the1 :::"being_a_theory"::: ) ) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "T")))) "holds" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set (Var "T")))) ")" )) ")" ))); theorem :: CQC_THE1:6 (Bool "for" (Set (Var "Al")) "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 "Al")) ")" ) "holds" (Bool (Set ($#k5_cqc_lang :::"VERUM"::: ) (Set (Var "Al"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_cqc_the1 :::"Cn"::: ) (Set (Var "X")))))) ; theorem :: CQC_THE1:7 (Bool "for" (Set (Var "Al")) "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 "Al")) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) "holds" (Bool (Set (Set "(" (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "p")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_cqc_the1 :::"Cn"::: ) (Set (Var "X"))))))) ; theorem :: CQC_THE1:8 (Bool "for" (Set (Var "Al")) "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 "Al")) ")" ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) "holds" (Bool (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_cqc_the1 :::"Cn"::: ) (Set (Var "X"))))))) ; theorem :: CQC_THE1:9 (Bool "for" (Set (Var "Al")) "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 "Al")) ")" ) (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 "Al"))) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set "(" (Set (Var "q")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "r")) ")" ) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "r")) ")" ) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_cqc_the1 :::"Cn"::: ) (Set (Var "X"))))))) ; theorem :: CQC_THE1:10 (Bool "for" (Set (Var "Al")) "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 "Al")) ")" ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "p")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_cqc_the1 :::"Cn"::: ) (Set (Var "X"))))))) ; theorem :: CQC_THE1:11 (Bool "for" (Set (Var "Al")) "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 "Al")) ")" ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_cqc_the1 :::"Cn"::: ) (Set (Var "X")))) & (Bool (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_cqc_the1 :::"Cn"::: ) (Set (Var "X"))))) "holds" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k1_cqc_the1 :::"Cn"::: ) (Set (Var "X"))))))) ; theorem :: CQC_THE1:12 (Bool "for" (Set (Var "Al")) "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 "Al")) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "holds" (Bool (Set (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_cqc_the1 :::"Cn"::: ) (Set (Var "X")))))))) ; theorem :: CQC_THE1:13 (Bool "for" (Set (Var "Al")) "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 "Al")) ")" ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_cqc_the1 :::"Cn"::: ) (Set (Var "X")))) & (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 "q")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_cqc_the1 :::"Cn"::: ) (Set (Var "X")))))))) ; theorem :: CQC_THE1:14 (Bool "for" (Set (Var "Al")) "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 "Al")) ")" ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Set (Var "s")) ($#k13_cqc_lang :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")))) & (Bool (Set (Set (Var "s")) ($#k13_cqc_lang :::"."::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")))) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "s"))))) & (Bool (Set (Set (Var "s")) ($#k13_cqc_lang :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_cqc_the1 :::"Cn"::: ) (Set (Var "X"))))) "holds" (Bool (Set (Set (Var "s")) ($#k13_cqc_lang :::"."::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_cqc_the1 :::"Cn"::: ) (Set (Var "X")))))))) ; theorem :: CQC_THE1:15 (Bool "for" (Set (Var "Al")) "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 "Al")) ")" ) "holds" (Bool (Set ($#k1_cqc_the1 :::"Cn"::: ) (Set (Var "X"))) "is" ($#v1_cqc_the1 :::"being_a_theory"::: ) ))) ; theorem :: CQC_THE1:16 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "T")) "," (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")) ")" ) "st" (Bool (Bool (Set (Var "T")) "is" ($#v1_cqc_the1 :::"being_a_theory"::: ) ) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "T")))) "holds" (Bool (Set ($#k1_cqc_the1 :::"Cn"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Var "T"))))) ; theorem :: CQC_THE1:17 (Bool "for" (Set (Var "Al")) "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 "Al")) ")" ) "holds" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k1_cqc_the1 :::"Cn"::: ) (Set (Var "X")))))) ; theorem :: CQC_THE1:18 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")) ")" ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k1_cqc_the1 :::"Cn"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_cqc_the1 :::"Cn"::: ) (Set (Var "Y")))))) ; theorem :: CQC_THE1:19 (Bool "for" (Set (Var "Al")) "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 "Al")) ")" ) "holds" (Bool (Set ($#k1_cqc_the1 :::"Cn"::: ) (Set "(" ($#k1_cqc_the1 :::"Cn"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_cqc_the1 :::"Cn"::: ) (Set (Var "X")))))) ; theorem :: CQC_THE1:20 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")) ")" ) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v1_cqc_the1 :::"being_a_theory"::: ) ) "iff" (Bool (Set ($#k1_cqc_the1 :::"Cn"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set (Var "T"))) ")" ))) ; definitionfunc :::"Proof_Step_Kinds"::: -> ($#m1_hidden :::"set"::: ) equals :: CQC_THE1:def 3 "{" (Set (Var "k")) where k "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Num 9)) "}" ; end; :: deftheorem defines :::"Proof_Step_Kinds"::: CQC_THE1:def 3 : (Bool (Set ($#k2_cqc_the1 :::"Proof_Step_Kinds"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set (Var "k")) where k "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Num 9)) "}" ); registration cluster (Set ($#k2_cqc_the1 :::"Proof_Step_Kinds"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: CQC_THE1:21 (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_cqc_the1 :::"Proof_Step_Kinds"::: ) )) & (Bool (Num 1) ($#r2_hidden :::"in"::: ) (Set ($#k2_cqc_the1 :::"Proof_Step_Kinds"::: ) )) & (Bool (Num 2) ($#r2_hidden :::"in"::: ) (Set ($#k2_cqc_the1 :::"Proof_Step_Kinds"::: ) )) & (Bool (Num 3) ($#r2_hidden :::"in"::: ) (Set ($#k2_cqc_the1 :::"Proof_Step_Kinds"::: ) )) & (Bool (Num 4) ($#r2_hidden :::"in"::: ) (Set ($#k2_cqc_the1 :::"Proof_Step_Kinds"::: ) )) & (Bool (Num 5) ($#r2_hidden :::"in"::: ) (Set ($#k2_cqc_the1 :::"Proof_Step_Kinds"::: ) )) & (Bool (Num 6) ($#r2_hidden :::"in"::: ) (Set ($#k2_cqc_the1 :::"Proof_Step_Kinds"::: ) )) & (Bool (Num 7) ($#r2_hidden :::"in"::: ) (Set ($#k2_cqc_the1 :::"Proof_Step_Kinds"::: ) )) & (Bool (Num 8) ($#r2_hidden :::"in"::: ) (Set ($#k2_cqc_the1 :::"Proof_Step_Kinds"::: ) )) & (Bool (Num 9) ($#r2_hidden :::"in"::: ) (Set ($#k2_cqc_the1 :::"Proof_Step_Kinds"::: ) )) ")" ) ; theorem :: CQC_THE1:22 (Bool (Set ($#k2_cqc_the1 :::"Proof_Step_Kinds"::: ) ) "is" ($#v1_finset_1 :::"finite"::: ) ) ; theorem :: CQC_THE1:23 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")) ")" ) "," (Set ($#k2_cqc_the1 :::"Proof_Step_Kinds"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Bool "not" (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool (Bool "not" (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 1))) & (Bool (Bool "not" (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 2))) & (Bool (Bool "not" (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 3))) & (Bool (Bool "not" (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 4))) & (Bool (Bool "not" (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 5))) & (Bool (Bool "not" (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 6))) & (Bool (Bool "not" (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 7))) & (Bool (Bool "not" (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 8)))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 9))))) ; definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "PR" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "Al")) ")" ) "," (Set ($#k2_cqc_the1 :::"Proof_Step_Kinds"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ); let "n" be ($#m1_hidden :::"Nat":::); let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "Al")) ")" ); pred "PR" "," "n" :::"is_a_correct_step_wrt"::: "X" means :: CQC_THE1:def 4 (Bool (Set (Set "(" "PR" ($#k1_funct_1 :::"."::: ) "n" ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r2_hidden :::"in"::: ) "X") if (Bool (Set (Set "(" "PR" ($#k1_funct_1 :::"."::: ) "n" ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) (Bool (Set (Set "(" "PR" ($#k1_funct_1 :::"."::: ) "n" ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k5_cqc_lang :::"VERUM"::: ) "Al")) if (Bool (Set (Set "(" "PR" ($#k1_funct_1 :::"."::: ) "n" ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)) (Bool "ex" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) "Al") "st" (Bool (Set (Set "(" "PR" ($#k1_funct_1 :::"."::: ) "n" ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "p")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "p"))))) if (Bool (Set (Set "(" "PR" ($#k1_funct_1 :::"."::: ) "n" ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 2)) (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) "Al") "st" (Bool (Set (Set "(" "PR" ($#k1_funct_1 :::"."::: ) "n" ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" )))) if (Bool (Set (Set "(" "PR" ($#k1_funct_1 :::"."::: ) "n" ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 3)) (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) "Al") "st" (Bool (Set (Set "(" "PR" ($#k1_funct_1 :::"."::: ) "n" ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set "(" (Set (Var "q")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "r")) ")" ) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "r")) ")" ) ")" ) ")" )))) if (Bool (Set (Set "(" "PR" ($#k1_funct_1 :::"."::: ) "n" ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 4)) (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) "Al") "st" (Bool (Set (Set "(" "PR" ($#k1_funct_1 :::"."::: ) "n" ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "p")) ")" )))) if (Bool (Set (Set "(" "PR" ($#k1_funct_1 :::"."::: ) "n" ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 5)) (Bool "ex" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) "Al")(Bool "ex" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" "Al" "st" (Bool (Set (Set "(" "PR" ($#k1_funct_1 :::"."::: ) "n" ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "p")))))) if (Bool (Set (Set "(" "PR" ($#k1_funct_1 :::"."::: ) "n" ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 6)) (Bool "ex" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) "Al") "st" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) "n") & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i"))) & (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set "(" "PR" ($#k1_funct_1 :::"."::: ) (Set (Var "j")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) )) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set "(" "PR" ($#k1_funct_1 :::"."::: ) "n" ")" ) ($#k1_xtuple_0 :::"`1"::: ) )) & (Bool (Set (Set "(" "PR" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")))) ")" ))) if (Bool (Set (Set "(" "PR" ($#k1_funct_1 :::"."::: ) "n" ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 7)) (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) "Al")(Bool "ex" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" "Al" "st" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) "n") & (Bool (Set (Set "(" "PR" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")))) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p"))))) & (Bool (Set (Set "(" "PR" ($#k1_funct_1 :::"."::: ) "n" ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" ))) ")" )))) if (Bool (Set (Set "(" "PR" ($#k1_funct_1 :::"."::: ) "n" ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 8)) (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" "Al"(Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" "Al" "st" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) "n") & (Bool (Set (Set (Var "s")) ($#k13_cqc_lang :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) "Al")) & (Bool (Set (Set (Var "s")) ($#k13_cqc_lang :::"."::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) "Al")) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "s"))))) & (Bool (Set (Set (Var "s")) ($#k13_cqc_lang :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "PR" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) )) & (Bool (Set (Set (Var "s")) ($#k13_cqc_lang :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "PR" ($#k1_funct_1 :::"."::: ) "n" ")" ) ($#k1_xtuple_0 :::"`1"::: ) )) ")" )))) if (Bool (Set (Set "(" "PR" ($#k1_funct_1 :::"."::: ) "n" ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 9)) ; end; :: deftheorem defines :::"is_a_correct_step_wrt"::: CQC_THE1:def 4 : (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "PR")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")) ")" ) "," (Set ($#k2_cqc_the1 :::"Proof_Step_Kinds"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")) ")" ) "holds" (Bool "(" "(" (Bool (Bool (Set (Set "(" (Set (Var "PR")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "PR")) "," (Set (Var "n")) ($#r1_cqc_the1 :::"is_a_correct_step_wrt"::: ) (Set (Var "X"))) "iff" (Bool (Set (Set "(" (Set (Var "PR")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" ) ")" & "(" (Bool (Bool (Set (Set "(" (Set (Var "PR")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 1))) "implies" (Bool "(" (Bool (Set (Var "PR")) "," (Set (Var "n")) ($#r1_cqc_the1 :::"is_a_correct_step_wrt"::: ) (Set (Var "X"))) "iff" (Bool (Set (Set "(" (Set (Var "PR")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k5_cqc_lang :::"VERUM"::: ) (Set (Var "Al")))) ")" ) ")" & "(" (Bool (Bool (Set (Set "(" (Set (Var "PR")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 2))) "implies" (Bool "(" (Bool (Set (Var "PR")) "," (Set (Var "n")) ($#r1_cqc_the1 :::"is_a_correct_step_wrt"::: ) (Set (Var "X"))) "iff" (Bool "ex" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) "st" (Bool (Set (Set "(" (Set (Var "PR")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "p")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "p"))))) ")" ) ")" & "(" (Bool (Bool (Set (Set "(" (Set (Var "PR")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 3))) "implies" (Bool "(" (Bool (Set (Var "PR")) "," (Set (Var "n")) ($#r1_cqc_the1 :::"is_a_correct_step_wrt"::: ) (Set (Var "X"))) "iff" (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) "st" (Bool (Set (Set "(" (Set (Var "PR")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" )))) ")" ) ")" & "(" (Bool (Bool (Set (Set "(" (Set (Var "PR")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 4))) "implies" (Bool "(" (Bool (Set (Var "PR")) "," (Set (Var "n")) ($#r1_cqc_the1 :::"is_a_correct_step_wrt"::: ) (Set (Var "X"))) "iff" (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) "st" (Bool (Set (Set "(" (Set (Var "PR")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set "(" (Set (Var "q")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "r")) ")" ) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "r")) ")" ) ")" ) ")" )))) ")" ) ")" & "(" (Bool (Bool (Set (Set "(" (Set (Var "PR")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 5))) "implies" (Bool "(" (Bool (Set (Var "PR")) "," (Set (Var "n")) ($#r1_cqc_the1 :::"is_a_correct_step_wrt"::: ) (Set (Var "X"))) "iff" (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) "st" (Bool (Set (Set "(" (Set (Var "PR")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "p")) ")" )))) ")" ) ")" & "(" (Bool (Bool (Set (Set "(" (Set (Var "PR")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 6))) "implies" (Bool "(" (Bool (Set (Var "PR")) "," (Set (Var "n")) ($#r1_cqc_the1 :::"is_a_correct_step_wrt"::: ) (Set (Var "X"))) "iff" (Bool "ex" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")))(Bool "ex" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Set (Set "(" (Set (Var "PR")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "p")))))) ")" ) ")" & "(" (Bool (Bool (Set (Set "(" (Set (Var "PR")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 7))) "implies" (Bool "(" (Bool (Set (Var "PR")) "," (Set (Var "n")) ($#r1_cqc_the1 :::"is_a_correct_step_wrt"::: ) (Set (Var "X"))) "iff" (Bool "ex" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) "st" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i"))) & (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "PR")) ($#k1_funct_1 :::"."::: ) (Set (Var "j")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) )) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "PR")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) )) & (Bool (Set (Set "(" (Set (Var "PR")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")))) ")" ))) ")" ) ")" & "(" (Bool (Bool (Set (Set "(" (Set (Var "PR")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 8))) "implies" (Bool "(" (Bool (Set (Var "PR")) "," (Set (Var "n")) ($#r1_cqc_the1 :::"is_a_correct_step_wrt"::: ) (Set (Var "X"))) "iff" (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")))(Bool "ex" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) & (Bool (Set (Set "(" (Set (Var "PR")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")))) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "p"))))) & (Bool (Set (Set "(" (Set (Var "PR")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" ))) ")" )))) ")" ) ")" & "(" (Bool (Bool (Set (Set "(" (Set (Var "PR")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 9))) "implies" (Bool "(" (Bool (Set (Var "PR")) "," (Set (Var "n")) ($#r1_cqc_the1 :::"is_a_correct_step_wrt"::: ) (Set (Var "X"))) "iff" (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al"))(Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "Al")) "st" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) & (Bool (Set (Set (Var "s")) ($#k13_cqc_lang :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")))) & (Bool (Set (Set (Var "s")) ($#k13_cqc_lang :::"."::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")))) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "s"))))) & (Bool (Set (Set (Var "s")) ($#k13_cqc_lang :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "PR")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) )) & (Bool (Set (Set (Var "s")) ($#k13_cqc_lang :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "PR")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) )) ")" )))) ")" ) ")" ")" ))))); definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "Al")) ")" ); let "f" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "Al")) ")" ) "," (Set ($#k2_cqc_the1 :::"Proof_Step_Kinds"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ); pred "f" :::"is_a_proof_wrt"::: "X" means :: CQC_THE1:def 5 (Bool "(" (Bool "f" ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "f"))) "holds" (Bool "f" "," (Set (Var "n")) ($#r1_cqc_the1 :::"is_a_correct_step_wrt"::: ) "X") ")" ) ")" ); end; :: deftheorem defines :::"is_a_proof_wrt"::: CQC_THE1:def 5 : (Bool "for" (Set (Var "Al")) "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 "Al")) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")) ")" ) "," (Set ($#k2_cqc_the1 :::"Proof_Step_Kinds"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_cqc_the1 :::"is_a_proof_wrt"::: ) (Set (Var "X"))) "iff" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Var "f")) "," (Set (Var "n")) ($#r1_cqc_the1 :::"is_a_correct_step_wrt"::: ) (Set (Var "X"))) ")" ) ")" ) ")" )))); theorem :: CQC_THE1:24 (Bool "for" (Set (Var "Al")) "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 "Al")) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")) ")" ) "," (Set ($#k2_cqc_the1 :::"Proof_Step_Kinds"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r2_cqc_the1 :::"is_a_proof_wrt"::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))))) ; theorem :: CQC_THE1:25 (Bool "for" (Set (Var "Al")) "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 "Al")) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")) ")" ) "," (Set ($#k2_cqc_the1 :::"Proof_Step_Kinds"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r2_cqc_the1 :::"is_a_proof_wrt"::: ) (Set (Var "X")))) "holds" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))))) ; theorem :: CQC_THE1:26 (Bool "for" (Set (Var "Al")) "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 "Al")) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")) ")" ) "," (Set ($#k2_cqc_the1 :::"Proof_Step_Kinds"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" "not" (Bool (Set (Var "f")) ($#r2_cqc_the1 :::"is_a_proof_wrt"::: ) (Set (Var "X"))) "or" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)) "or" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 2)) "or" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 3)) "or" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 4)) "or" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 5)) "or" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Num 6)) ")" )))) ; theorem :: CQC_THE1:27 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")) ")" ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")) ")" ) "," (Set ($#k2_cqc_the1 :::"Proof_Step_Kinds"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Set (Var "f")) "," (Set (Var "n")) ($#r1_cqc_the1 :::"is_a_correct_step_wrt"::: ) (Set (Var "X"))) "iff" (Bool (Set (Set (Var "f")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "g"))) "," (Set (Var "n")) ($#r1_cqc_the1 :::"is_a_correct_step_wrt"::: ) (Set (Var "X"))) ")" ))))) ; theorem :: CQC_THE1:28 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")) ")" ) (Bool "for" (Set (Var "g")) "," (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")) ")" ) "," (Set ($#k2_cqc_the1 :::"Proof_Step_Kinds"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g")))) & (Bool (Set (Var "g")) "," (Set (Var "n")) ($#r1_cqc_the1 :::"is_a_correct_step_wrt"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "f")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "g"))) "," (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )) ($#r1_cqc_the1 :::"is_a_correct_step_wrt"::: ) (Set (Var "X"))))))) ; theorem :: CQC_THE1:29 (Bool "for" (Set (Var "Al")) "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 "Al")) ")" ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")) ")" ) "," (Set ($#k2_cqc_the1 :::"Proof_Step_Kinds"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r2_cqc_the1 :::"is_a_proof_wrt"::: ) (Set (Var "X"))) & (Bool (Set (Var "g")) ($#r2_cqc_the1 :::"is_a_proof_wrt"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "f")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "g"))) ($#r2_cqc_the1 :::"is_a_proof_wrt"::: ) (Set (Var "X")))))) ; theorem :: CQC_THE1:30 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")) ")" ) "," (Set ($#k2_cqc_the1 :::"Proof_Step_Kinds"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r2_cqc_the1 :::"is_a_proof_wrt"::: ) (Set (Var "X"))) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "f")) ($#r2_cqc_the1 :::"is_a_proof_wrt"::: ) (Set (Var "Y")))))) ; theorem :: CQC_THE1:31 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "l")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")) ")" ) "," (Set ($#k2_cqc_the1 :::"Proof_Step_Kinds"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r2_cqc_the1 :::"is_a_proof_wrt"::: ) (Set (Var "X"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "l"))) & (Bool (Set (Var "l")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "l")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_cqc_the1 :::"Cn"::: ) (Set (Var "X")))))))) ; definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "f" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "Al")) ")" ) "," (Set ($#k2_cqc_the1 :::"Proof_Step_Kinds"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ); assume (Bool (Set (Const "f")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ; func :::"Effect"::: "f" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) "Al") equals :: CQC_THE1:def 6 (Set (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) "f" ")" ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ); end; :: deftheorem defines :::"Effect"::: CQC_THE1:def 6 : (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")) ")" ) "," (Set ($#k2_cqc_the1 :::"Proof_Step_Kinds"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k3_cqc_the1 :::"Effect"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) )))); theorem :: CQC_THE1:32 (Bool "for" (Set (Var "Al")) "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 "Al")) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")) ")" ) "," (Set ($#k2_cqc_the1 :::"Proof_Step_Kinds"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r2_cqc_the1 :::"is_a_proof_wrt"::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k3_cqc_the1 :::"Effect"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_cqc_the1 :::"Cn"::: ) (Set (Var "X"))))))) ; theorem :: CQC_THE1:33 (Bool "for" (Set (Var "Al")) "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 "Al")) ")" ) "holds" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) "{" (Set (Var "F")) where F "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) : (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")) ")" ) "," (Set ($#k2_cqc_the1 :::"Proof_Step_Kinds"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool "(" (Bool (Set (Var "f")) ($#r2_cqc_the1 :::"is_a_proof_wrt"::: ) (Set (Var "X"))) & (Bool (Set ($#k3_cqc_the1 :::"Effect"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "F"))) ")" )) "}" ))) ; theorem :: CQC_THE1:34 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")) ")" ) "st" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) "{" (Set (Var "p")) where p "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) : (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")) ")" ) "," (Set ($#k2_cqc_the1 :::"Proof_Step_Kinds"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool "(" (Bool (Set (Var "f")) ($#r2_cqc_the1 :::"is_a_proof_wrt"::: ) (Set (Var "X"))) & (Bool (Set ($#k3_cqc_the1 :::"Effect"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))) ")" )) "}" )) "holds" (Bool (Set (Var "Y")) "is" ($#v1_cqc_the1 :::"being_a_theory"::: ) ))) ; theorem :: CQC_THE1:35 (Bool "for" (Set (Var "Al")) "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 "Al")) ")" ) "holds" (Bool "{" (Set (Var "p")) where p "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) : (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")) ")" ) "," (Set ($#k2_cqc_the1 :::"Proof_Step_Kinds"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool "(" (Bool (Set (Var "f")) ($#r2_cqc_the1 :::"is_a_proof_wrt"::: ) (Set (Var "X"))) & (Bool (Set ($#k3_cqc_the1 :::"Effect"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))) ")" )) "}" ($#r1_hidden :::"="::: ) (Set ($#k1_cqc_the1 :::"Cn"::: ) (Set (Var "X")))))) ; theorem :: CQC_THE1:36 (Bool "for" (Set (Var "Al")) "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 "Al")) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_cqc_the1 :::"Cn"::: ) (Set (Var "X")))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")) ")" ) "," (Set ($#k2_cqc_the1 :::"Proof_Step_Kinds"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool "(" (Bool (Set (Var "f")) ($#r2_cqc_the1 :::"is_a_proof_wrt"::: ) (Set (Var "X"))) & (Bool (Set ($#k3_cqc_the1 :::"Effect"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))) ")" )) ")" )))) ; theorem :: CQC_THE1:37 (Bool "for" (Set (Var "Al")) "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 "Al")) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_cqc_the1 :::"Cn"::: ) (Set (Var "X"))))) "holds" (Bool "ex" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")) ")" ) "st" (Bool "(" (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "Y")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_cqc_the1 :::"Cn"::: ) (Set (Var "Y")))) ")" ))))) ; definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; func :::"TAUT"::: "Al" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) "Al" ")" ) equals :: CQC_THE1:def 7 (Set ($#k1_cqc_the1 :::"Cn"::: ) (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) "Al" ")" ) ")" )); end; :: deftheorem defines :::"TAUT"::: CQC_THE1:def 7 : (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) "holds" (Bool (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "Al"))) ($#r1_hidden :::"="::: ) (Set ($#k1_cqc_the1 :::"Cn"::: ) (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")) ")" ) ")" )))); theorem :: CQC_THE1:38 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")) ")" ) "st" (Bool (Bool (Set (Var "T")) "is" ($#v1_cqc_the1 :::"being_a_theory"::: ) )) "holds" (Bool (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "Al"))) ($#r1_tarski :::"c="::: ) (Set (Var "T"))))) ; theorem :: CQC_THE1:39 (Bool "for" (Set (Var "Al")) "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 "Al")) ")" ) "holds" (Bool (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "Al"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_cqc_the1 :::"Cn"::: ) (Set (Var "X")))))) ; theorem :: CQC_THE1:40 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) "holds" (Bool (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "Al"))) "is" ($#v1_cqc_the1 :::"being_a_theory"::: ) )) ; theorem :: CQC_THE1:41 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) "holds" (Bool (Set ($#k5_cqc_lang :::"VERUM"::: ) (Set (Var "Al"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "Al"))))) ; theorem :: CQC_THE1:42 (Bool "for" (Set (Var "Al")) "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 "Al"))) "holds" (Bool (Set (Set "(" (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "p")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "Al")))))) ; theorem :: CQC_THE1:43 (Bool "for" (Set (Var "Al")) "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 "Al"))) "holds" (Bool (Set (Set (Var "p")) ($#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 "Al")))))) ; theorem :: CQC_THE1:44 (Bool "for" (Set (Var "Al")) "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 "Al"))) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set "(" (Set (Var "q")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "r")) ")" ) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "r")) ")" ) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "Al")))))) ; theorem :: CQC_THE1:45 (Bool "for" (Set (Var "Al")) "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 "Al"))) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "p")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "Al")))))) ; theorem :: CQC_THE1:46 (Bool "for" (Set (Var "Al")) "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 "Al"))) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "Al")))) & (Bool (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "Al"))))) "holds" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "Al")))))) ; theorem :: CQC_THE1:47 (Bool "for" (Set (Var "Al")) "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 "Al"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "holds" (Bool (Set (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "Al"))))))) ; theorem :: CQC_THE1:48 (Bool "for" (Set (Var "Al")) "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 "Al"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "Al")))) & (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 "q")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "Al"))))))) ; theorem :: CQC_THE1:49 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Set (Var "s")) ($#k13_cqc_lang :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")))) & (Bool (Set (Set (Var "s")) ($#k13_cqc_lang :::"."::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")))) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "s"))))) & (Bool (Set (Set (Var "s")) ($#k13_cqc_lang :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "Al"))))) "holds" (Bool (Set (Set (Var "s")) ($#k13_cqc_lang :::"."::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "Al"))))))) ; definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Const "Al")) ")" ); let "s" be ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Const "Al")); pred "X" :::"|-"::: "s" means :: CQC_THE1:def 8 (Bool "s" ($#r2_hidden :::"in"::: ) (Set ($#k1_cqc_the1 :::"Cn"::: ) "X")); end; :: deftheorem defines :::"|-"::: CQC_THE1:def 8 : (Bool "for" (Set (Var "Al")) "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 "Al")) ")" ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "Al")) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r3_cqc_the1 :::"|-"::: ) (Set (Var "s"))) "iff" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set ($#k1_cqc_the1 :::"Cn"::: ) (Set (Var "X")))) ")" )))); theorem :: CQC_THE1:50 (Bool "for" (Set (Var "Al")) "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 "Al")) ")" ) "holds" (Bool (Set (Var "X")) ($#r3_cqc_the1 :::"|-"::: ) (Set ($#k5_cqc_lang :::"VERUM"::: ) (Set (Var "Al")))))) ; theorem :: CQC_THE1:51 (Bool "for" (Set (Var "Al")) "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 "Al")) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) "holds" (Bool (Set (Var "X")) ($#r3_cqc_the1 :::"|-"::: ) (Set (Set "(" (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "p")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "p"))))))) ; theorem :: CQC_THE1:52 (Bool "for" (Set (Var "Al")) "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 "Al")) ")" ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) "holds" (Bool (Set (Var "X")) ($#r3_cqc_the1 :::"|-"::: ) (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" )))))) ; theorem :: CQC_THE1:53 (Bool "for" (Set (Var "Al")) "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 "Al")) ")" ) (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 "Al"))) "holds" (Bool (Set (Var "X")) ($#r3_cqc_the1 :::"|-"::: ) (Set (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set "(" (Set (Var "q")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "r")) ")" ) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "r")) ")" ) ")" ) ")" )))))) ; theorem :: CQC_THE1:54 (Bool "for" (Set (Var "Al")) "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 "Al")) ")" ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) "holds" (Bool (Set (Var "X")) ($#r3_cqc_the1 :::"|-"::: ) (Set (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "p")) ")" )))))) ; theorem :: CQC_THE1:55 (Bool "for" (Set (Var "Al")) "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 "Al")) ")" ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) "st" (Bool (Bool (Set (Var "X")) ($#r3_cqc_the1 :::"|-"::: ) (Set (Var "p"))) & (Bool (Set (Var "X")) ($#r3_cqc_the1 :::"|-"::: ) (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q"))))) "holds" (Bool (Set (Var "X")) ($#r3_cqc_the1 :::"|-"::: ) (Set (Var "q")))))) ; theorem :: CQC_THE1:56 (Bool "for" (Set (Var "Al")) "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 "Al")) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "holds" (Bool (Set (Var "X")) ($#r3_cqc_the1 :::"|-"::: ) (Set (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "p")))))))) ; theorem :: CQC_THE1:57 (Bool "for" (Set (Var "Al")) "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 "Al")) ")" ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Var "X")) ($#r3_cqc_the1 :::"|-"::: ) (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")))) & (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 (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "q")) ")" ")" ))))))) ; theorem :: CQC_THE1:58 (Bool "for" (Set (Var "Al")) "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 "Al")) ")" ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Set (Var "s")) ($#k13_cqc_lang :::"."::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")))) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "s"))))) & (Bool (Set (Var "X")) ($#r3_cqc_the1 :::"|-"::: ) (Set (Set (Var "s")) ($#k13_cqc_lang :::"."::: ) (Set (Var "x"))))) "holds" (Bool (Set (Var "X")) ($#r3_cqc_the1 :::"|-"::: ) (Set (Set (Var "s")) ($#k13_cqc_lang :::"."::: ) (Set (Var "y")))))))) ; definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "s" be ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Const "Al")); attr "s" is :::"valid"::: means :: CQC_THE1:def 9 (Bool (Set ($#k1_subset_1 :::"{}"::: ) (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) "Al" ")" )) ($#r3_cqc_the1 :::"|-"::: ) "s"); end; :: deftheorem defines :::"valid"::: CQC_THE1:def 9 : (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "Al")) "holds" (Bool "(" (Bool (Set (Var "s")) "is" ($#v2_cqc_the1 :::"valid"::: ) ) "iff" (Bool (Set ($#k1_subset_1 :::"{}"::: ) (Set "(" ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")) ")" )) ($#r3_cqc_the1 :::"|-"::: ) (Set (Var "s"))) ")" ))); definitionlet "Al" be ($#m1_qc_lang1 :::"QC-alphabet"::: ) ; let "s" be ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Const "Al")); redefine attr "s" is :::"valid"::: means :: CQC_THE1:def 10 (Bool "s" ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) "Al")); end; :: deftheorem defines :::"valid"::: CQC_THE1:def 10 : (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "Al")) "holds" (Bool "(" (Bool (Set (Var "s")) "is" ($#v2_cqc_the1 :::"valid"::: ) ) "iff" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set ($#k4_cqc_the1 :::"TAUT"::: ) (Set (Var "Al")))) ")" ))); theorem :: CQC_THE1:59 (Bool "for" (Set (Var "Al")) "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 "Al")) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al"))) "st" (Bool (Bool (Set (Var "p")) "is" ($#v2_cqc_the1 :::"valid"::: ) )) "holds" (Bool (Set (Var "X")) ($#r3_cqc_the1 :::"|-"::: ) (Set (Var "p")))))) ; theorem :: CQC_THE1:60 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) "holds" (Bool (Set ($#k5_cqc_lang :::"VERUM"::: ) (Set (Var "Al"))) "is" ($#v2_cqc_the1 :::"valid"::: ) )) ; theorem :: CQC_THE1:61 (Bool "for" (Set (Var "Al")) "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 "Al"))) "holds" (Bool (Set (Set "(" (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "p")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "p"))) "is" ($#v2_cqc_the1 :::"valid"::: ) ))) ; theorem :: CQC_THE1:62 (Bool "for" (Set (Var "Al")) "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 "Al"))) "holds" (Bool (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set (Var "p")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) ))) ; theorem :: CQC_THE1:63 (Bool "for" (Set (Var "Al")) "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 "Al"))) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set "(" (Set (Var "q")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "r")) ")" ) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" ($#k6_cqc_lang :::"'not'"::: ) (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "r")) ")" ) ")" ) ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) ))) ; theorem :: CQC_THE1:64 (Bool "for" (Set (Var "Al")) "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 "Al"))) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "q")) ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k7_cqc_lang :::"'&'"::: ) (Set (Var "p")) ")" )) "is" ($#v2_cqc_the1 :::"valid"::: ) ))) ; theorem :: CQC_THE1:65 (Bool "for" (Set (Var "Al")) "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 "Al"))) "st" (Bool (Bool (Set (Var "p")) "is" ($#v2_cqc_the1 :::"valid"::: ) ) & (Bool (Set (Set (Var "p")) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "q"))) "is" ($#v2_cqc_the1 :::"valid"::: ) )) "holds" (Bool (Set (Var "q")) "is" ($#v2_cqc_the1 :::"valid"::: ) ))) ; theorem :: CQC_THE1:66 (Bool "for" (Set (Var "Al")) "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 "Al"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "holds" (Bool (Set (Set "(" ($#k11_cqc_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ")" ) ($#k8_cqc_lang :::"=>"::: ) (Set (Var "p"))) "is" ($#v2_cqc_the1 :::"valid"::: ) )))) ; theorem :: CQC_THE1:67 (Bool "for" (Set (Var "Al")) "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 "Al"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "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 "p")))))) "holds" (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_THE1:68 (Bool "for" (Set (Var "Al")) "being" ($#m1_qc_lang1 :::"QC-alphabet"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"QC-formula":::) "of" (Set (Var "Al")) (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Bool (Set (Set (Var "s")) ($#k13_cqc_lang :::"."::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set ($#k3_cqc_lang :::"CQC-WFF"::: ) (Set (Var "Al")))) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_qc_lang1 :::"still_not-bound_in"::: ) (Set (Var "s"))))) & (Bool (Set (Set (Var "s")) ($#k13_cqc_lang :::"."::: ) (Set (Var "x"))) "is" ($#v2_cqc_the1 :::"valid"::: ) )) "holds" (Bool (Set (Set (Var "s")) ($#k13_cqc_lang :::"."::: ) (Set (Var "y"))) "is" ($#v2_cqc_the1 :::"valid"::: ) )))) ;