:: HENMODEL  semantic presentation begin  









































theorem :: HENMODEL:1 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "n")) "," (Set (Var "A"))  "st" (Bool (Bool  "ex" (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st" (Bool (Set   ($#k4_card_1 :::"succ"::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set (Var "n")))) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Var "A"))) & (Bool  "("   "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "m"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "m")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "m"))))  ")" )) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set  "("  ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")) ")" )))))) ; 
 
theorem :: HENMODEL:2 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "holds"   (Bool  "("  (Bool (Set   ($#k3_tarski :::"union"::: )  (Set (Var "A")))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool  "("   "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )    "holds"  (Bool  "("   "not" (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) "or" (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "A")))) "or" (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "A"))))  ")" )  ")" )  ")" )) ; 
 



theorem :: HENMODEL:3 (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "C"))  (Bool  "for" (Set (Var "X")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "m"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "m")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "n")))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "m"))))  ")" ) & (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set  "("  ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")) ")" )))) "holds"  (Bool  "ex" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st" (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "k")))))))) ; 
 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 "p" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Const "Al"))); pred "X" :::"|-"::: "p" means :: HENMODEL:def 1 (Bool  "ex" (Set (Var "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  "Al") "st"  (Bool  "("  (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")))  ($#r1_tarski :::"c="::: )  "X") & (Bool   ($#r4_calcul_1 :::"|-"::: )  (Set (Set (Var "f"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) "p" ($#k12_finseq_1 :::"*>"::: ) )))  ")" )); end; 






:: deftheorem    defines :::"|-"::: HENMODEL: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")) ")" )  (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"))) "iff" (Bool  "ex" (Set (Var "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al"))) "st"  (Bool  "("  (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")))  ($#r1_tarski :::"c="::: )  (Set (Var "X"))) & (Bool   ($#r4_calcul_1 :::"|-"::: )  (Set (Set (Var "f"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_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")) ")" ); attr "X" is  :::"Consistent":::  means :: HENMODEL:def 2 (Bool  "for" (Set (Var "p")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  "Al")  "holds"  (Bool  "("   "not" (Bool "X"  ($#r1_henmodel :::"|-"::: )  (Set (Var "p"))) "or"  "not" (Bool "X"  ($#r1_henmodel :::"|-"::: )  (Set   ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p"))))  ")" )); end; 





:: deftheorem    defines :::"Consistent"::: HENMODEL: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"   ($#v1_henmodel :::"Consistent"::: )  ) "iff" (Bool  "for" (Set (Var "p")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al")))  "holds"  (Bool  "("   "not" (Bool (Set (Var "X"))  ($#r1_henmodel :::"|-"::: )  (Set (Var "p"))) "or"  "not" (Bool (Set (Var "X"))  ($#r1_henmodel :::"|-"::: )  (Set   ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p"))))  ")" ))  ")" ))); 
 notationlet "Al" be    ($#m1_qc_lang1 :::"QC-alphabet"::: )  ; let "X" be   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Const "Al")) ")" ); antonym  :::"Inconsistent"::: "X" for  :::"Consistent"::: ; end; definitionlet "Al" be    ($#m1_qc_lang1 :::"QC-alphabet"::: )  ; let "f" be    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Const "Al"))); attr "f" is  :::"Consistent":::  means :: HENMODEL:def 3 (Bool  "for" (Set (Var "p")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  "Al")  "holds"  (Bool  "("   "not" (Bool   ($#r4_calcul_1 :::"|-"::: )  (Set "f"  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) ))) "or"  "not" (Bool   ($#r4_calcul_1 :::"|-"::: )  (Set "f"  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p")) ")" ) ($#k12_finseq_1 :::"*>"::: ) )))  ")" )); end; 





:: deftheorem    defines :::"Consistent"::: HENMODEL:def 3 :  (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  "("  (Bool (Set (Var "f")) "is"   ($#v2_henmodel :::"Consistent"::: )  ) "iff" (Bool  "for" (Set (Var "p")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al")))  "holds"  (Bool  "("   "not" (Bool   ($#r4_calcul_1 :::"|-"::: )  (Set (Set (Var "f"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) ))) "or"  "not" (Bool   ($#r4_calcul_1 :::"|-"::: )  (Set (Set (Var "f"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p")) ")" ) ($#k12_finseq_1 :::"*>"::: ) )))  ")" ))  ")" ))); 
 notationlet "Al" be    ($#m1_qc_lang1 :::"QC-alphabet"::: )  ; let "f" be    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Const "Al"))); antonym  :::"Inconsistent"::: "f" for  :::"Consistent"::: ; end; 
theorem :: HENMODEL:4 (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 "g")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al")))  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v1_henmodel :::"Consistent"::: )  ) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "g")))  ($#r1_tarski :::"c="::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "g")) "is"   ($#v2_henmodel :::"Consistent"::: )  )))) ; 
 
theorem :: HENMODEL: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")))  (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   ($#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 (Var "f"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "g")) ")" )  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) )))))) ; 
 
theorem :: HENMODEL: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  "("  (Bool (Set (Var "X")) "is"   ($#v1_henmodel :::"Inconsistent"::: )  ) "iff" (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"))  ($#r1_henmodel :::"|-"::: )  (Set (Var "p"))))  ")" ))) ; 
 
theorem :: HENMODEL: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")) ")" )  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v1_henmodel :::"Inconsistent"::: )  )) "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 "Y")) "is"   ($#v1_henmodel :::"Inconsistent"::: )  )  ")" )))) ; 
 
theorem :: HENMODEL: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")))  "st" (Bool (Bool (Set (Set (Var "X"))  ($#k4_subset_1 :::"\/"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) ))  ($#r1_henmodel :::"|-"::: )  (Set (Var "q")))) "holds"  (Bool  "ex" (Set (Var "g")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al"))) "st"  (Bool  "("  (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "g")))  ($#r1_tarski :::"c="::: )  (Set (Var "X"))) & (Bool   ($#r4_calcul_1 :::"|-"::: )  (Set (Set  "(" (Set (Var "g"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k12_finseq_1 :::"*>"::: ) ) ")" )  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "q")) ($#k12_finseq_1 :::"*>"::: ) )))  ")" ))))) ; 
 
theorem :: HENMODEL: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")) "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"))) "iff" (Bool (Set (Set (Var "X"))  ($#k4_subset_1 :::"\/"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p")) ")" ) ($#k6_domain_1 :::"}"::: ) )) "is"   ($#v1_henmodel :::"Inconsistent"::: )  )  ")" )))) ; 
 
theorem :: HENMODEL: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")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al"))) "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r1_henmodel :::"|-"::: )  (Set   ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p")))) "iff" (Bool (Set (Set (Var "X"))  ($#k4_subset_1 :::"\/"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) )) "is"   ($#v1_henmodel :::"Inconsistent"::: )  )  ")" )))) ; 
 begin  
theorem :: HENMODEL:11 (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  "("  ($#k9_setfam_1 :::"bool"::: )  (Set  "("  ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "Al")) ")" ) ")" )  "st" (Bool (Bool  "("   "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "m"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "m")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "n"))) "is"   ($#v1_henmodel :::"Consistent"::: )  ) & (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "n")))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "m"))))  ")" )  ")" )) "holds"  (Bool (Set   ($#k5_setfam_1 :::"union"::: )  (Set  "("  ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")) ")" )) "is"   ($#v1_henmodel :::"Consistent"::: )  ))) ; 
 begin  









theorem :: HENMODEL: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 "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X")) "is"   ($#v1_henmodel :::"Inconsistent"::: )  )) "holds"  (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  "not" (Set (Var "J")) "," (Set (Var "v"))  ($#r6_calcul_1 :::"|="::: )  (Set (Var "X"))))))))) ; 
 
theorem :: HENMODEL:13 (Bool  "for" (Set (Var "Al")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )   "holds"  (Bool (Set  ($#k6_domain_1 :::"{"::: ) (Set  "("  ($#k5_cqc_lang :::"VERUM"::: )  (Set (Var "Al")) ")" ) ($#k6_domain_1 :::"}"::: ) ) "is"   ($#v1_henmodel :::"Consistent"::: )  )) ; 
 registrationlet "Al" be    ($#m1_qc_lang1 :::"QC-alphabet"::: )  ; 
cluster   ($#v1_henmodel :::"Consistent"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "("  ($#k3_cqc_lang :::"CQC-WFF"::: )  "Al" ")" )); 
end; 





definitionlet "Al" be    ($#m1_qc_lang1 :::"QC-alphabet"::: )  ; func  :::"HCar"::: "Al" ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   equals :: HENMODEL:def 4 (Set   ($#k3_qc_lang1 :::"bound_QC-variables"::: )  "Al"); end; 





:: deftheorem    defines :::"HCar"::: HENMODEL:def 4 :  (Bool  "for" (Set (Var "Al")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )   "holds"  (Bool (Set   ($#k1_henmodel :::"HCar"::: )  (Set (Var "Al")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_qc_lang1 :::"bound_QC-variables"::: )  (Set (Var "Al"))))); 
 definitionlet "Al" be    ($#m1_qc_lang1 :::"QC-alphabet"::: )  ; let "P" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k6_qc_lang1 :::"QC-pred_symbols"::: )  (Set (Const "Al"))); let "ll" be   ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set   ($#k7_qc_lang1 :::"the_arity_of"::: )  (Set (Const "P"))) "," (Set (Const "Al")); :: original: :::"!"::: redefine func "P" :::"!"::: "ll" ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  "Al"); end; definitionlet "Al" be    ($#m1_qc_lang1 :::"QC-alphabet"::: )  ; let "CX" be   ($#v1_henmodel :::"Consistent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Const "Al")) ")" ); mode  :::"Henkin_interpretation":::  "of" "CX" ->    ($#m1_valuat_1 :::"interpretation"::: )   "of" "Al" "," (Set   ($#k1_henmodel :::"HCar"::: )  "Al") means :: HENMODEL:def 5 (Bool  "for" (Set (Var "P")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k6_qc_lang1 :::"QC-pred_symbols"::: )  "Al")  (Bool  "for" (Set (Var "r")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k3_margrel1 :::"relations_on"::: )  (Set  "("  ($#k1_henmodel :::"HCar"::: )  "Al" ")" ))  "st" (Bool (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "P")))  ($#r1_margrel1 :::"="::: )  (Set (Var "r")))) "holds"  (Bool  "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "r"))) "iff" (Bool  "ex" (Set (Var "ll")) "being"   ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set   ($#k7_qc_lang1 :::"the_arity_of"::: )  (Set (Var "P"))) "," "Al" "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "ll"))) & (Bool "CX"  ($#r1_henmodel :::"|-"::: )  (Set (Set (Var "P"))  ($#k2_henmodel :::"!"::: )  (Set (Var "ll"))))  ")" ))  ")" )))); end; 






:: deftheorem    defines :::"Henkin_interpretation"::: HENMODEL:def 5 :  (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 "b3")) "being"    ($#m1_valuat_1 :::"interpretation"::: )   "of" (Set (Var "Al")) "," (Set   ($#k1_henmodel :::"HCar"::: )  (Set (Var "Al"))) "holds"   (Bool  "("  (Bool (Set (Var "b3")) "is"    ($#m1_henmodel :::"Henkin_interpretation"::: )   "of" (Set (Var "CX"))) "iff" (Bool  "for" (Set (Var "P")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k6_qc_lang1 :::"QC-pred_symbols"::: )  (Set (Var "Al")))  (Bool  "for" (Set (Var "r")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k3_margrel1 :::"relations_on"::: )  (Set  "("  ($#k1_henmodel :::"HCar"::: )  (Set (Var "Al")) ")" ))  "st" (Bool (Bool (Set (Set (Var "b3"))  ($#k3_funct_2 :::"."::: )  (Set (Var "P")))  ($#r1_margrel1 :::"="::: )  (Set (Var "r")))) "holds"  (Bool  "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "r"))) "iff" (Bool  "ex" (Set (Var "ll")) "being"   ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set   ($#k7_qc_lang1 :::"the_arity_of"::: )  (Set (Var "P"))) "," (Set (Var "Al")) "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "ll"))) & (Bool (Set (Var "CX"))  ($#r1_henmodel :::"|-"::: )  (Set (Set (Var "P"))  ($#k2_henmodel :::"!"::: )  (Set (Var "ll"))))  ")" ))  ")" ))))  ")" )))); 
 definitionlet "Al" be    ($#m1_qc_lang1 :::"QC-alphabet"::: )  ; func  :::"valH"::: "Al" ->    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k2_valuat_1 :::"Valuations_in"::: )   "(" "Al" "," (Set  "("  ($#k1_henmodel :::"HCar"::: )  "Al" ")" ) ")" ) equals :: HENMODEL:def 6 (Set   ($#k11_cqc_sim1 :::"id"::: )  (Set  "("  ($#k3_qc_lang1 :::"bound_QC-variables"::: )  "Al" ")" )); end; 





:: deftheorem    defines :::"valH"::: HENMODEL:def 6 :  (Bool  "for" (Set (Var "Al")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )   "holds"  (Bool (Set   ($#k3_henmodel :::"valH"::: )  (Set (Var "Al")))  ($#r1_hidden :::"="::: )  (Set   ($#k11_cqc_sim1 :::"id"::: )  (Set  "("  ($#k3_qc_lang1 :::"bound_QC-variables"::: )  (Set (Var "Al")) ")" )))); 
 begin  



theorem :: HENMODEL:14 (Bool  "for" (Set (Var "Al")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "ll")) "being"   ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (Set (Var "Al")) "holds"  (Bool (Set (Set  "("  ($#k3_henmodel :::"valH"::: )  (Set (Var "Al")) ")" )  ($#k4_valuat_1 :::"*'"::: )  (Set (Var "ll")))  ($#r1_hidden :::"="::: )  (Set (Var "ll")))))) ; 
 
theorem :: HENMODEL:15 (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   ($#r4_calcul_1 :::"|-"::: )  (Set (Set (Var "f"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  "("  ($#k5_cqc_lang :::"VERUM"::: )  (Set (Var "Al")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ))))) ; 
 
theorem :: HENMODEL: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")) "holds"   (Bool  "("  (Bool (Set (Var "JH")) "," (Set   ($#k3_henmodel :::"valH"::: )  (Set (Var "Al")))  ($#r1_valuat_1 :::"|="::: )  (Set   ($#k5_cqc_lang :::"VERUM"::: )  (Set (Var "Al")))) "iff" (Bool (Set (Var "CX"))  ($#r1_henmodel :::"|-"::: )  (Set   ($#k5_cqc_lang :::"VERUM"::: )  (Set (Var "Al"))))  ")" )))) ; 
 
theorem :: HENMODEL:17 (Bool  "for" (Set (Var "Al")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "P")) "being"   ($#m2_subset_1 :::"QC-pred_symbol":::) "of" (Set (Var "k")) "," (Set (Var "Al"))  (Bool  "for" (Set (Var "ll")) "being"   ($#m2_finseq_1 :::"CQC-variable_list":::) "of" (Set (Var "k")) "," (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 (Set (Var "P"))  ($#k4_cqc_lang :::"!"::: )  (Set (Var "ll")))) "iff" (Bool (Set (Var "CX"))  ($#r1_henmodel :::"|-"::: )  (Set (Set (Var "P"))  ($#k4_cqc_lang :::"!"::: )  (Set (Var "ll"))))  ")" ))))))) ;