:: GOEDELCP  semantic presentation begin  registration
cluster   ($#v4_card_3 :::"countable"::: )    for    ($#m1_qc_lang1 :::"QC-alphabet"::: )  ; 
end; 





























































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")) ")" ); attr "X" is  :::"negation_faithful":::  means :: GOEDELCP:def 1 (Bool  "for" (Set (Var "p")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  "Al")  "holds"  (Bool  "("  (Bool "X"  ($#r1_henmodel :::"|-"::: )  (Set (Var "p"))) "or" (Bool "X"  ($#r1_henmodel :::"|-"::: )  (Set   ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p"))))  ")" )); end; 





:: deftheorem    defines :::"negation_faithful"::: GOEDELCP:def 1 :  (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  "("  (Bool (Set (Var "X")) "is"   ($#v1_goedelcp :::"negation_faithful"::: )  ) "iff" (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 "X"))  ($#r1_henmodel :::"|-"::: )  (Set (Var "p"))) "or" (Bool (Set (Var "X"))  ($#r1_henmodel :::"|-"::: )  (Set   ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p"))))  ")" ))  ")" ))); 
 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")) ")" ); attr "X" is  :::"with_examples":::  means :: GOEDELCP:def 2 (Bool  "for" (Set (Var "x")) "being"   ($#m2_subset_1 :::"bound_QC-variable":::) "of" "Al"  (Bool  "for" (Set (Var "p")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  "Al") (Bool  "ex" (Set (Var "y")) "being"   ($#m2_subset_1 :::"bound_QC-variable":::) "of" "Al" "st" (Bool "X"  ($#r1_henmodel :::"|-"::: )  (Set (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set  "("  ($#k12_cqc_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set (Var "p")) ")"  ")" ) ")" )  ($#k9_cqc_lang :::"'or'"::: )  (Set  "(" (Set (Var "p"))  ($#k4_substut2 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")"  ")" )))))); end; 





:: deftheorem    defines :::"with_examples"::: GOEDELCP:def 2 :  (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  "("  (Bool (Set (Var "X")) "is"   ($#v2_goedelcp :::"with_examples"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "being"   ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al"))  (Bool  "for" (Set (Var "p")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al"))) (Bool  "ex" (Set (Var "y")) "being"   ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Set (Var "X"))  ($#r1_henmodel :::"|-"::: )  (Set (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set  "("  ($#k12_cqc_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set (Var "p")) ")"  ")" ) ")" )  ($#k9_cqc_lang :::"'or'"::: )  (Set  "(" (Set (Var "p"))  ($#k4_substut2 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")"  ")" ))))))  ")" ))); 
 
theorem :: GOEDELCP:1 (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 "CX")) "being"   ($#v1_henmodel :::"Consistent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al")) ")" )  "st" (Bool (Bool (Set (Var "CX")) "is"   ($#v1_goedelcp :::"negation_faithful"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "CX"))  ($#r1_henmodel :::"|-"::: )  (Set (Var "p"))) "iff" (Bool (Bool  "not" (Set (Var "CX"))  ($#r1_henmodel :::"|-"::: )  (Set   ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p")))))  ")" )))) ; 
 
theorem :: GOEDELCP:2 (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 "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al")))  "st" (Bool (Bool   ($#r4_calcul_1 :::"|-"::: )  (Set (Set (Var "f"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  "(" (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k9_cqc_lang :::"'or'"::: )  (Set (Var "q")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ))) & (Bool   ($#r4_calcul_1 :::"|-"::: )  (Set (Set (Var "f"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) )))) "holds"  (Bool   ($#r4_calcul_1 :::"|-"::: )  (Set (Set (Var "f"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "q")) ($#k12_finseq_1 :::"*>"::: ) )))))) ; 
 
theorem :: GOEDELCP:3 (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"))  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v2_goedelcp :::"with_examples"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "X"))  ($#r1_henmodel :::"|-"::: )  (Set   ($#k12_cqc_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set (Var "p")) ")" )) "iff" (Bool  "ex" (Set (Var "y")) "being"   ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Set (Var "X"))  ($#r1_henmodel :::"|-"::: )  (Set (Set (Var "p"))  ($#k4_substut2 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))  ")" ))))) ; 
 
theorem :: GOEDELCP:4 (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 "CX")) "being"   ($#v1_henmodel :::"Consistent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al")) ")" )  (Bool  "for" (Set (Var "JH")) "being"    ($#m1_henmodel :::"Henkin_interpretation"::: )   "of" (Set (Var "CX"))  "st" (Bool  "("  (Bool (Bool (Set (Var "CX")) "is"   ($#v1_goedelcp :::"negation_faithful"::: )  ) & (Bool (Set (Var "CX")) "is"   ($#v2_goedelcp :::"with_examples"::: )  )) "implies" (Bool  "("  (Bool (Set (Var "JH")) "," (Set   ($#k3_henmodel :::"valH"::: )  (Set (Var "Al")))  ($#r1_valuat_1 :::"|="::: )  (Set (Var "p"))) "iff" (Bool (Set (Var "CX"))  ($#r1_henmodel :::"|-"::: )  (Set (Var "p")))  ")" )  ")"  & (Bool (Set (Var "CX")) "is"   ($#v1_goedelcp :::"negation_faithful"::: )  ) & (Bool (Set (Var "CX")) "is"   ($#v2_goedelcp :::"with_examples"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "JH")) "," (Set   ($#k3_henmodel :::"valH"::: )  (Set (Var "Al")))  ($#r1_valuat_1 :::"|="::: )  (Set   ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p")))) "iff" (Bool (Set (Var "CX"))  ($#r1_henmodel :::"|-"::: )  (Set   ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p"))))  ")" ))))) ; 
 
theorem :: GOEDELCP:5 (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 "f1")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al")))  "st" (Bool (Bool   ($#r4_calcul_1 :::"|-"::: )  (Set (Set (Var "f1"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) ))) & (Bool   ($#r4_calcul_1 :::"|-"::: )  (Set (Set (Var "f1"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "q")) ($#k12_finseq_1 :::"*>"::: ) )))) "holds"  (Bool   ($#r4_calcul_1 :::"|-"::: )  (Set (Set (Var "f1"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  "(" (Set (Var "p"))  ($#k7_cqc_lang :::"'&'"::: )  (Set (Var "q")) ")" ) ($#k12_finseq_1 :::"*>"::: ) )))))) ; 
 
theorem :: GOEDELCP: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")) ")" )  (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  "("  (Bool  "("  (Bool (Set (Var "X"))  ($#r1_henmodel :::"|-"::: )  (Set (Var "p"))) & (Bool (Set (Var "X"))  ($#r1_henmodel :::"|-"::: )  (Set (Var "q")))  ")" ) "iff" (Bool (Set (Var "X"))  ($#r1_henmodel :::"|-"::: )  (Set (Set (Var "p"))  ($#k7_cqc_lang :::"'&'"::: )  (Set (Var "q"))))  ")" )))) ; 
 
theorem :: GOEDELCP:7 (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 "CX")) "being"   ($#v1_henmodel :::"Consistent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al")) ")" )  (Bool  "for" (Set (Var "JH")) "being"    ($#m1_henmodel :::"Henkin_interpretation"::: )   "of" (Set (Var "CX"))  "st" (Bool  "("  (Bool (Bool (Set (Var "CX")) "is"   ($#v1_goedelcp :::"negation_faithful"::: )  ) & (Bool (Set (Var "CX")) "is"   ($#v2_goedelcp :::"with_examples"::: )  )) "implies" (Bool  "("  (Bool (Set (Var "JH")) "," (Set   ($#k3_henmodel :::"valH"::: )  (Set (Var "Al")))  ($#r1_valuat_1 :::"|="::: )  (Set (Var "p"))) "iff" (Bool (Set (Var "CX"))  ($#r1_henmodel :::"|-"::: )  (Set (Var "p")))  ")" )  ")"  &  "("  (Bool (Bool (Set (Var "CX")) "is"   ($#v1_goedelcp :::"negation_faithful"::: )  ) & (Bool (Set (Var "CX")) "is"   ($#v2_goedelcp :::"with_examples"::: )  )) "implies" (Bool  "("  (Bool (Set (Var "JH")) "," (Set   ($#k3_henmodel :::"valH"::: )  (Set (Var "Al")))  ($#r1_valuat_1 :::"|="::: )  (Set (Var "q"))) "iff" (Bool (Set (Var "CX"))  ($#r1_henmodel :::"|-"::: )  (Set (Var "q")))  ")" )  ")"  & (Bool (Set (Var "CX")) "is"   ($#v1_goedelcp :::"negation_faithful"::: )  ) & (Bool (Set (Var "CX")) "is"   ($#v2_goedelcp :::"with_examples"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "JH")) "," (Set   ($#k3_henmodel :::"valH"::: )  (Set (Var "Al")))  ($#r1_valuat_1 :::"|="::: )  (Set (Set (Var "p"))  ($#k7_cqc_lang :::"'&'"::: )  (Set (Var "q")))) "iff" (Bool (Set (Var "CX"))  ($#r1_henmodel :::"|-"::: )  (Set (Set (Var "p"))  ($#k7_cqc_lang :::"'&'"::: )  (Set (Var "q"))))  ")" ))))) ; 
 
theorem :: GOEDELCP:8 (Bool  "for" (Set (Var "Al")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "CX")) "being"   ($#v1_henmodel :::"Consistent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al")) ")" )  (Bool  "for" (Set (Var "JH")) "being"    ($#m1_henmodel :::"Henkin_interpretation"::: )   "of" (Set (Var "CX"))  (Bool  "for" (Set (Var "p")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al")))  "st" (Bool (Bool (Set   ($#k7_cqc_sim1 :::"QuantNbr"::: )  (Set (Var "p")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "CX")) "is"   ($#v1_goedelcp :::"negation_faithful"::: )  ) & (Bool (Set (Var "CX")) "is"   ($#v2_goedelcp :::"with_examples"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "JH")) "," (Set   ($#k3_henmodel :::"valH"::: )  (Set (Var "Al")))  ($#r1_valuat_1 :::"|="::: )  (Set (Var "p"))) "iff" (Bool (Set (Var "CX"))  ($#r1_henmodel :::"|-"::: )  (Set (Var "p")))  ")" ))))) ; 
 
theorem :: GOEDELCP:9 (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"))  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "J")) "being"    ($#m1_valuat_1 :::"interpretation"::: )   "of" (Set (Var "Al")) "," (Set (Var "A"))  (Bool  "for" (Set (Var "v")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k2_valuat_1 :::"Valuations_in"::: )   "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "J")) "," (Set (Var "v"))  ($#r1_valuat_1 :::"|="::: )  (Set   ($#k12_cqc_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set (Var "p")) ")" )) "iff" (Bool  "ex" (Set (Var "a")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A")) "st" (Bool (Set (Var "J")) "," (Set (Set (Var "v"))  ($#k1_sublemma :::"."::: )  (Set  "(" (Set (Var "x"))  ($#k12_sublemma :::"|"::: )  (Set (Var "a")) ")" ))  ($#r1_valuat_1 :::"|="::: )  (Set (Var "p"))))  ")" ))))))) ; 
 
theorem :: GOEDELCP:10 (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"))  (Bool  "for" (Set (Var "CX")) "being"   ($#v1_henmodel :::"Consistent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al")) ")" )  (Bool  "for" (Set (Var "JH")) "being"    ($#m1_henmodel :::"Henkin_interpretation"::: )   "of" (Set (Var "CX")) "holds"   (Bool  "("  (Bool (Set (Var "JH")) "," (Set   ($#k3_henmodel :::"valH"::: )  (Set (Var "Al")))  ($#r1_valuat_1 :::"|="::: )  (Set   ($#k12_cqc_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set (Var "p")) ")" )) "iff" (Bool  "ex" (Set (Var "y")) "being"   ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Set (Var "JH")) "," (Set   ($#k3_henmodel :::"valH"::: )  (Set (Var "Al")))  ($#r1_valuat_1 :::"|="::: )  (Set (Set (Var "p"))  ($#k4_substut2 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))  ")" )))))) ; 
 
theorem :: GOEDELCP:11 (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"))  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "J")) "being"    ($#m1_valuat_1 :::"interpretation"::: )   "of" (Set (Var "Al")) "," (Set (Var "A"))  (Bool  "for" (Set (Var "v")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k2_valuat_1 :::"Valuations_in"::: )   "(" (Set (Var "Al")) "," (Set (Var "A")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "J")) "," (Set (Var "v"))  ($#r1_valuat_1 :::"|="::: )  (Set   ($#k6_cqc_lang :::"'not'"::: )  (Set  "("  ($#k12_cqc_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p")) ")" ) ")"  ")" ))) "iff" (Bool (Set (Var "J")) "," (Set (Var "v"))  ($#r1_valuat_1 :::"|="::: )  (Set   ($#k11_cqc_lang :::"All"::: )   "(" (Set (Var "x")) "," (Set (Var "p")) ")" ))  ")" ))))))) ; 
 
theorem :: GOEDELCP: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  "("  (Bool (Set (Var "X"))  ($#r1_henmodel :::"|-"::: )  (Set   ($#k6_cqc_lang :::"'not'"::: )  (Set  "("  ($#k12_cqc_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p")) ")" ) ")"  ")" ))) "iff" (Bool (Set (Var "X"))  ($#r1_henmodel :::"|-"::: )  (Set   ($#k11_cqc_lang :::"All"::: )   "(" (Set (Var "x")) "," (Set (Var "p")) ")" ))  ")" ))))) ; 
 
theorem :: GOEDELCP:13 (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   ($#k7_cqc_sim1 :::"QuantNbr"::: )  (Set  "("  ($#k12_cqc_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set (Var "p")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k7_cqc_sim1 :::"QuantNbr"::: )  (Set (Var "p")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1)))))) ; 
 
theorem :: GOEDELCP:14 (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")) "," (Set (Var "y")) "being"   ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "holds"  (Bool (Set   ($#k7_cqc_sim1 :::"QuantNbr"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k7_cqc_sim1 :::"QuantNbr"::: )  (Set  "(" (Set (Var "p"))  ($#k4_substut2 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")"  ")" )))))) ; 
 










theorem :: GOEDELCP:15 (Bool  "for" (Set (Var "Al")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "CX")) "being"   ($#v1_henmodel :::"Consistent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al")) ")" )  (Bool  "for" (Set (Var "JH")) "being"    ($#m1_henmodel :::"Henkin_interpretation"::: )   "of" (Set (Var "CX"))  (Bool  "for" (Set (Var "p")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al")))  "st" (Bool (Bool (Set   ($#k7_cqc_sim1 :::"QuantNbr"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Var "CX")) "is"   ($#v1_goedelcp :::"negation_faithful"::: )  ) & (Bool (Set (Var "CX")) "is"   ($#v2_goedelcp :::"with_examples"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "JH")) "," (Set   ($#k3_henmodel :::"valH"::: )  (Set (Var "Al")))  ($#r1_valuat_1 :::"|="::: )  (Set (Var "p"))) "iff" (Bool (Set (Var "CX"))  ($#r1_henmodel :::"|-"::: )  (Set (Var "p")))  ")" ))))) ; 
 
theorem :: GOEDELCP:16 (Bool  "for" (Set (Var "Al")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "CX")) "being"   ($#v1_henmodel :::"Consistent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al")) ")" )  (Bool  "for" (Set (Var "JH")) "being"    ($#m1_henmodel :::"Henkin_interpretation"::: )   "of" (Set (Var "CX"))  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool  "("   "for" (Set (Var "p")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al")))  "st" (Bool (Bool (Set   ($#k7_cqc_sim1 :::"QuantNbr"::: )  (Set (Var "p")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Var "CX")) "is"   ($#v1_goedelcp :::"negation_faithful"::: )  ) & (Bool (Set (Var "CX")) "is"   ($#v2_goedelcp :::"with_examples"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "JH")) "," (Set   ($#k3_henmodel :::"valH"::: )  (Set (Var "Al")))  ($#r1_valuat_1 :::"|="::: )  (Set (Var "p"))) "iff" (Bool (Set (Var "CX"))  ($#r1_henmodel :::"|-"::: )  (Set (Var "p")))  ")" )  ")" )) "holds"  (Bool  "for" (Set (Var "p")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al")))  "st" (Bool (Bool (Set   ($#k7_cqc_sim1 :::"QuantNbr"::: )  (Set (Var "p")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1))) & (Bool (Set (Var "CX")) "is"   ($#v1_goedelcp :::"negation_faithful"::: )  ) & (Bool (Set (Var "CX")) "is"   ($#v2_goedelcp :::"with_examples"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "JH")) "," (Set   ($#k3_henmodel :::"valH"::: )  (Set (Var "Al")))  ($#r1_valuat_1 :::"|="::: )  (Set (Var "p"))) "iff" (Bool (Set (Var "CX"))  ($#r1_henmodel :::"|-"::: )  (Set (Var "p")))  ")" )))))) ; 
 
theorem :: GOEDELCP:17 (Bool  "for" (Set (Var "Al")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "CX")) "being"   ($#v1_henmodel :::"Consistent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al")) ")" )  (Bool  "for" (Set (Var "JH")) "being"    ($#m1_henmodel :::"Henkin_interpretation"::: )   "of" (Set (Var "CX"))  (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 "CX")) "is"   ($#v1_goedelcp :::"negation_faithful"::: )  ) & (Bool (Set (Var "CX")) "is"   ($#v2_goedelcp :::"with_examples"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "JH")) "," (Set   ($#k3_henmodel :::"valH"::: )  (Set (Var "Al")))  ($#r1_valuat_1 :::"|="::: )  (Set (Var "p"))) "iff" (Bool (Set (Var "CX"))  ($#r1_henmodel :::"|-"::: )  (Set (Var "p")))  ")" ))))) ; 
 begin  
theorem :: GOEDELCP:18 (Bool  "for" (Set (Var "Al")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    "st" (Bool (Bool (Set (Var "Al")) "is"   ($#v4_card_3 :::"countable"::: )  )) "holds"  (Bool (Set   ($#k9_qc_lang1 :::"QC-WFF"::: )  (Set (Var "Al"))) "is"   ($#v4_card_3 :::"countable"::: )  )) ; 
 definitionlet "Al" be    ($#m1_qc_lang1 :::"QC-alphabet"::: )  ; func  :::"ExCl"::: "Al" ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_cqc_lang :::"CQC-WFF"::: )  "Al" ")" ) means :: GOEDELCP:def 3 (Bool  "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "ex" (Set (Var "x")) "being"   ($#m2_subset_1 :::"bound_QC-variable":::) "of" "Al"(Bool  "ex" (Set (Var "p")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  "Al") "st" (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k12_cqc_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set (Var "p")) ")" ))))  ")" )); end; 





:: deftheorem    defines :::"ExCl"::: GOEDELCP:def 3 :  (Bool  "for" (Set (Var "Al")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_goedelcp :::"ExCl"::: )  (Set (Var "Al")))) "iff" (Bool  "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "b2"))) "iff" (Bool  "ex" (Set (Var "x")) "being"   ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al"))(Bool  "ex" (Set (Var "p")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al"))) "st" (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k12_cqc_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set (Var "p")) ")" ))))  ")" ))  ")" ))); 
 
theorem :: GOEDELCP:19 (Bool  "for" (Set (Var "Al")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    "st" (Bool (Bool (Set (Var "Al")) "is"   ($#v4_card_3 :::"countable"::: )  )) "holds"  (Bool (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al"))) "is"   ($#v4_card_3 :::"countable"::: )  )) ; 
 
theorem :: GOEDELCP:20 (Bool  "for" (Set (Var "Al")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    "st" (Bool (Bool (Set (Var "Al")) "is"   ($#v4_card_3 :::"countable"::: )  )) "holds"  (Bool  "("  (Bool (Bool  "not" (Set   ($#k1_goedelcp :::"ExCl"::: )  (Set (Var "Al"))) "is"   ($#v1_xboole_0 :::"empty"::: )  )) & (Bool (Set   ($#k1_goedelcp :::"ExCl"::: )  (Set (Var "Al"))) "is"   ($#v4_card_3 :::"countable"::: )  )  ")" )) ; 
 definitionlet "Al" be    ($#m1_qc_lang1 :::"QC-alphabet"::: )  ; let "p" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k9_qc_lang1 :::"QC-WFF"::: )  (Set (Const "Al"))); assume 
(Bool (Set (Const "p")) "is"   ($#v4_qc_lang2 :::"existential"::: )  )
 ; func  :::"Ex-bound_in"::: "p" ->   ($#m2_subset_1 :::"bound_QC-variable":::) "of" "Al" means :: GOEDELCP:def 4 (Bool  "ex" (Set (Var "q")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k9_qc_lang1 :::"QC-WFF"::: )  "Al") "st" (Bool "p"  ($#r1_hidden :::"="::: )  (Set   ($#k5_qc_lang2 :::"Ex"::: )   "(" it "," (Set (Var "q")) ")" ))); end; 







:: deftheorem    defines :::"Ex-bound_in"::: GOEDELCP:def 4 :  (Bool  "for" (Set (Var "Al")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k9_qc_lang1 :::"QC-WFF"::: )  (Set (Var "Al")))  "st" (Bool (Bool (Set (Var "p")) "is"   ($#v4_qc_lang2 :::"existential"::: )  )) "holds"  (Bool  "for" (Set (Var "b3")) "being"   ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_goedelcp :::"Ex-bound_in"::: )  (Set (Var "p")))) "iff" (Bool  "ex" (Set (Var "q")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k9_qc_lang1 :::"QC-WFF"::: )  (Set (Var "Al"))) "st" (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_qc_lang2 :::"Ex"::: )   "(" (Set (Var "b3")) "," (Set (Var "q")) ")" )))  ")" )))); 
 definitionlet "Al" be    ($#m1_qc_lang1 :::"QC-alphabet"::: )  ; let "p" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Const "Al"))); assume 
(Bool (Set (Const "p")) "is"   ($#v4_qc_lang2 :::"existential"::: )  )
 ; func  :::"Ex-the_scope_of"::: "p" ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  "Al") means :: GOEDELCP:def 5 (Bool  "ex" (Set (Var "x")) "being"   ($#m2_subset_1 :::"bound_QC-variable":::) "of" "Al" "st" (Bool "p"  ($#r1_hidden :::"="::: )  (Set   ($#k12_cqc_lang :::"Ex"::: )   "(" (Set (Var "x")) "," it ")" ))); end; 







:: deftheorem    defines :::"Ex-the_scope_of"::: GOEDELCP:def 5 :  (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")))  "st" (Bool (Bool (Set (Var "p")) "is"   ($#v4_qc_lang2 :::"existential"::: )  )) "holds"  (Bool  "for" (Set (Var "b3")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al"))) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_goedelcp :::"Ex-the_scope_of"::: )  (Set (Var "p")))) "iff" (Bool  "ex" (Set (Var "x")) "being"   ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set   ($#k12_cqc_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set (Var "b3")) ")" )))  ")" )))); 
 definitionlet "Al" be    ($#m1_qc_lang1 :::"QC-alphabet"::: )  ; let "F" be   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  "("  ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Const "Al")) ")" ); let "a" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); func  :::"bound_in":::  "(" "F" "," "a" ")"  ->   ($#m2_subset_1 :::"bound_QC-variable":::) "of" "Al" means :: GOEDELCP:def 6 (Bool  "for" (Set (Var "p")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  "Al")  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set "F"  ($#k3_funct_2 :::"."::: )  "a"))) "holds"  (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k2_goedelcp :::"Ex-bound_in"::: )  (Set (Var "p"))))); end; 







:: deftheorem    defines :::"bound_in"::: GOEDELCP:def 6 :  (Bool  "for" (Set (Var "Al")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  "("  ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al")) ")" )  (Bool  "for" (Set (Var "a")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "b4")) "being"   ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_goedelcp :::"bound_in"::: )   "(" (Set (Var "F")) "," (Set (Var "a")) ")" )) "iff" (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"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a"))))) "holds"  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_goedelcp :::"Ex-bound_in"::: )  (Set (Var "p")))))  ")" ))))); 
 definitionlet "Al" be    ($#m1_qc_lang1 :::"QC-alphabet"::: )  ; let "F" be   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  "("  ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Const "Al")) ")" ); let "a" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); func  :::"the_scope_of":::  "(" "F" "," "a" ")"  ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  "Al") means :: GOEDELCP:def 7 (Bool  "for" (Set (Var "p")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  "Al")  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set "F"  ($#k3_funct_2 :::"."::: )  "a"))) "holds"  (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k3_goedelcp :::"Ex-the_scope_of"::: )  (Set (Var "p"))))); end; 







:: deftheorem    defines :::"the_scope_of"::: GOEDELCP:def 7 :  (Bool  "for" (Set (Var "Al")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  "("  ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al")) ")" )  (Bool  "for" (Set (Var "a")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "b4")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al"))) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_goedelcp :::"the_scope_of"::: )   "(" (Set (Var "F")) "," (Set (Var "a")) ")" )) "iff" (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"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a"))))) "holds"  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_goedelcp :::"Ex-the_scope_of"::: )  (Set (Var "p")))))  ")" ))))); 
 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  :::"still_not-bound_in"::: "X" ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_qc_lang1 :::"bound_QC-variables"::: )  "Al" ")" ) equals :: GOEDELCP:def 8 (Set   ($#k3_tarski :::"union"::: )   "{"  (Set  "("  ($#k24_qc_lang1 :::"still_not-bound_in"::: )  (Set (Var "p")) ")" ) where p "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  "Al") : (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  "X")  "}"  ); end; 






:: deftheorem    defines :::"still_not-bound_in"::: GOEDELCP: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")) ")" ) "holds"  (Bool (Set   ($#k6_goedelcp :::"still_not-bound_in"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )   "{"  (Set  "("  ($#k24_qc_lang1 :::"still_not-bound_in"::: )  (Set (Var "p")) ")" ) where p "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al"))) : (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))  "}"  )))); 
 
theorem :: GOEDELCP:21 (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 (Var "X")))) "holds"  (Bool (Set (Var "X"))  ($#r1_henmodel :::"|-"::: )  (Set (Var "p")))))) ; 
 
theorem :: GOEDELCP:22 (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  "("  (Bool (Set   ($#k2_goedelcp :::"Ex-bound_in"::: )  (Set  "("  ($#k12_cqc_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set (Var "p")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "x"))) & (Bool (Set   ($#k3_goedelcp :::"Ex-the_scope_of"::: )  (Set  "("  ($#k12_cqc_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set (Var "p")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "p")))  ")" )))) ; 
 
theorem :: GOEDELCP:23 (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_henmodel :::"|-"::: )  (Set   ($#k5_cqc_lang :::"VERUM"::: )  (Set (Var "Al")))))) ; 
 
theorem :: GOEDELCP: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")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r1_henmodel :::"|-"::: )  (Set   ($#k6_cqc_lang :::"'not'"::: )  (Set  "("  ($#k5_cqc_lang :::"VERUM"::: )  (Set (Var "Al")) ")" ))) "iff" (Bool (Set (Var "X")) "is"   ($#v1_henmodel :::"Inconsistent"::: )  )  ")" ))) ; 
 








theorem :: GOEDELCP:25 (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 "f")) "," (Set (Var "g")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al")))  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))) & (Bool   ($#r4_calcul_1 :::"|-"::: )  (Set (Set (Var "f"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) )))) "holds"  (Bool   ($#r4_calcul_1 :::"|-"::: )  (Set (Set  "(" (Set  "(" (Set  "("  ($#k1_calcul_1 :::"Ant"::: )  (Set (Var "f")) ")" )  ($#k8_finseq_1 :::"^"::: )  (Set (Var "g")) ")" )  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  "("  ($#k2_calcul_1 :::"Suc"::: )  (Set (Var "f")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ")" )  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) )))))) ; 
 
theorem :: GOEDELCP:26 (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   ($#k6_goedelcp :::"still_not-bound_in"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k24_qc_lang1 :::"still_not-bound_in"::: )  (Set (Var "p")))))) ; 
 
theorem :: GOEDELCP:27 (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")) ")" ) "holds"  (Bool (Set   ($#k6_goedelcp :::"still_not-bound_in"::: )  (Set  "(" (Set (Var "X"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "Y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k6_goedelcp :::"still_not-bound_in"::: )  (Set (Var "X")) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k6_goedelcp :::"still_not-bound_in"::: )  (Set (Var "Y")) ")" ))))) ; 
 
theorem :: GOEDELCP:28 (Bool  "for" (Set (Var "Al")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_qc_lang1 :::"bound_QC-variables"::: )  (Set (Var "Al")) ")" )  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v1_finset_1 :::"finite"::: )  )) "holds"  (Bool  "ex" (Set (Var "x")) "being"   ($#m2_subset_1 :::"bound_QC-variable":::) "of" (Set (Var "Al")) "st" (Bool (Bool  "not" (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))))))) ; 
 
theorem :: GOEDELCP:29 (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   ($#k6_goedelcp :::"still_not-bound_in"::: )  (Set (Var "X")))  ($#r1_tarski :::"c="::: )  (Set   ($#k6_goedelcp :::"still_not-bound_in"::: )  (Set (Var "Y")))))) ; 
 
theorem :: GOEDELCP:30 (Bool  "for" (Set (Var "Al")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al"))) "holds"  (Bool (Set   ($#k6_goedelcp :::"still_not-bound_in"::: )  (Set  "("  ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_calcul_1 :::"still_not-bound_in"::: )  (Set (Var "f")))))) ; 
 
theorem :: GOEDELCP:31 (Bool  "for" (Set (Var "Al")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "CX")) "being"   ($#v1_henmodel :::"Consistent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al")) ")" )  "st" (Bool (Bool (Set (Var "Al")) "is"   ($#v4_card_3 :::"countable"::: )  ) & (Bool (Set   ($#k6_goedelcp :::"still_not-bound_in"::: )  (Set (Var "CX"))) "is"   ($#v1_finset_1 :::"finite"::: )  )) "holds"  (Bool  "ex" (Set (Var "CY")) "being"   ($#v1_henmodel :::"Consistent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al")) ")" ) "st"  (Bool  "("  (Bool (Set (Var "CX"))  ($#r1_tarski :::"c="::: )  (Set (Var "CY"))) & (Bool (Set (Var "CY")) "is"   ($#v2_goedelcp :::"with_examples"::: )  )  ")" )))) ; 
 
theorem :: GOEDELCP:32 (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 "p")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al")))  "st" (Bool (Bool (Set (Var "X"))  ($#r1_henmodel :::"|-"::: )  (Set (Var "p"))) & (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))) "holds"  (Bool (Set (Var "Y"))  ($#r1_henmodel :::"|-"::: )  (Set (Var "p")))))) ; 
 




theorem :: GOEDELCP:33 (Bool  "for" (Set (Var "Al")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "CX")) "being"   ($#v1_henmodel :::"Consistent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al")) ")" )  "st" (Bool (Bool (Set (Var "Al")) "is"   ($#v4_card_3 :::"countable"::: )  ) & (Bool (Set (Var "CX")) "is"   ($#v2_goedelcp :::"with_examples"::: )  )) "holds"  (Bool  "ex" (Set (Var "CY")) "being"   ($#v1_henmodel :::"Consistent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al")) ")" ) "st"  (Bool  "("  (Bool (Set (Var "CX"))  ($#r1_tarski :::"c="::: )  (Set (Var "CY"))) & (Bool (Set (Var "CY")) "is"   ($#v1_goedelcp :::"negation_faithful"::: )  ) & (Bool (Set (Var "CY")) "is"   ($#v2_goedelcp :::"with_examples"::: )  )  ")" )))) ; 
 









theorem :: GOEDELCP:34 (Bool  "for" (Set (Var "Al")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "CX")) "being"   ($#v1_henmodel :::"Consistent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al")) ")" )  "st" (Bool (Bool (Set (Var "Al")) "is"   ($#v4_card_3 :::"countable"::: )  ) & (Bool (Set   ($#k6_goedelcp :::"still_not-bound_in"::: )  (Set (Var "CX"))) "is"   ($#v1_finset_1 :::"finite"::: )  )) "holds"  (Bool  "ex" (Set (Var "CZ")) "being"   ($#v1_henmodel :::"Consistent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al")) ")" )(Bool  "ex" (Set (Var "JH1")) "being"    ($#m1_henmodel :::"Henkin_interpretation"::: )   "of" (Set (Var "CZ")) "st" (Bool (Set (Var "JH1")) "," (Set   ($#k3_henmodel :::"valH"::: )  (Set (Var "Al")))  ($#r6_calcul_1 :::"|="::: )  (Set (Var "CX"))))))) ; 
 begin  
theorem :: GOEDELCP:35 (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 "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "J")) "being"    ($#m1_valuat_1 :::"interpretation"::: )   "of" (Set (Var "Al")) "," (Set (Var "A"))  (Bool  "for" (Set (Var "v")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k2_valuat_1 :::"Valuations_in"::: )   "(" (Set (Var "Al")) "," (Set (Var "A")) ")" )  "st" (Bool (Bool (Set (Var "J")) "," (Set (Var "v"))  ($#r6_calcul_1 :::"|="::: )  (Set (Var "X"))) & (Bool (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "J")) "," (Set (Var "v"))  ($#r6_calcul_1 :::"|="::: )  (Set (Var "Y")))))))) ; 
 
theorem :: GOEDELCP: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")))  "st" (Bool (Bool (Set   ($#k6_goedelcp :::"still_not-bound_in"::: )  (Set (Var "X"))) "is"   ($#v1_finset_1 :::"finite"::: )  )) "holds"  (Bool (Set   ($#k6_goedelcp :::"still_not-bound_in"::: )  (Set  "(" (Set (Var "X"))  ($#k4_subset_1 :::"\/"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) ) ")" )) "is"   ($#v1_finset_1 :::"finite"::: )  )))) ; 
 
theorem :: GOEDELCP: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")))  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "J")) "being"    ($#m1_valuat_1 :::"interpretation"::: )   "of" (Set (Var "Al")) "," (Set (Var "A"))  (Bool  "for" (Set (Var "v")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k2_valuat_1 :::"Valuations_in"::: )   "(" (Set (Var "Al")) "," (Set (Var "A")) ")" )  "st" (Bool (Bool (Set (Var "X"))  ($#r7_calcul_1 :::"|="::: )  (Set (Var "p")))) "holds"  (Bool  "not" (Bool (Set (Var "J")) "," (Set (Var "v"))  ($#r6_calcul_1 :::"|="::: )  (Set (Set (Var "X"))  ($#k4_subset_1 :::"\/"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p")) ")" ) ($#k6_domain_1 :::"}"::: ) )))))))))) ; 
 
theorem :: GOEDELCP:38 (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 "Al")) "is"   ($#v4_card_3 :::"countable"::: )  ) & (Bool (Set   ($#k6_goedelcp :::"still_not-bound_in"::: )  (Set (Var "X"))) "is"   ($#v1_finset_1 :::"finite"::: )  ) & (Bool (Set (Var "X"))  ($#r7_calcul_1 :::"|="::: )  (Set (Var "p")))) "holds"  (Bool (Set (Var "X"))  ($#r1_henmodel :::"|-"::: )  (Set (Var "p")))))) ;