begin
theorem Th1:
theorem Th2:
theorem Th3:
:: deftheorem HENMODEL:def 1 :
canceled;
:: deftheorem Def2 defines |- HENMODEL:def 2 :
:: deftheorem Def3 defines Consistent HENMODEL:def 3 :
:: deftheorem Def4 defines Consistent HENMODEL:def 4 :
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
Lm1:
for f, g being FinSequence holds Seg (len (f ^ g)) = (Seg (len f)) \/ (seq (len f),(len g))
theorem
theorem
theorem
begin
theorem
begin
theorem Th12:
theorem Th13:
:: deftheorem defines HCar HENMODEL:def 5 :
:: deftheorem Def6 defines Henkin_interpretation HENMODEL:def 6 :
:: deftheorem defines valH HENMODEL:def 7 :
begin
theorem Th14:
theorem Th15:
theorem
theorem