:: HENMODEL semantic presentation
:: Showing IDV graph ... (Click the Palm Trees again to close it)
theorem Th1: :: HENMODEL:1
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th2: :: HENMODEL:2
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: deftheorem Def1 defines min* HENMODEL:def 1 :
theorem Th3: :: HENMODEL:3
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: deftheorem Def2 defines |- HENMODEL:def 2 :
:: deftheorem Def3 defines Consistent HENMODEL:def 3 :
:: deftheorem Def4 defines Consistent HENMODEL:def 4 :
theorem Th4: :: HENMODEL:4
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th5: :: HENMODEL:5
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th6: :: HENMODEL:6
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th7: :: HENMODEL:7
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
Lm1:
for f, g being FinSequence holds Seg (len (f ^ g)) = (Seg (len f)) \/ (seq (len f),(len g))
by CALCUL_2:9;
Lm2:
for n, m being Nat holds Seg n misses seq n,m
by CALCUL_2:8;
theorem :: HENMODEL:8
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: HENMODEL:9
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: HENMODEL:10
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: HENMODEL:11
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th12: :: HENMODEL:12
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th13: :: HENMODEL:13
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: deftheorem defines HCar HENMODEL:def 5 :
:: deftheorem Def6 defines Henkin_interpretation HENMODEL:def 6 :
:: deftheorem defines valH HENMODEL:def 7 :
theorem Th14: :: HENMODEL:14
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th15: :: HENMODEL:15
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: HENMODEL:16
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: HENMODEL:17
:: Showing IDV graph ... (Click the Palm Tree again to close it) 