let I be Program of SCM+FSA; :: thesis: for a being read-write Int-Location
for s being State of SCM+FSA st ex f being Function of (product the Object-Kind of SCM+FSA),NAT st
for k being Element of NAT holds
( ( f . ((StepWhile>0 (a,s,I)) . k) <> 0 implies ( f . ((StepWhile>0 (a,s,I)) . (k + 1)) < f . ((StepWhile>0 (a,s,I)) . k) & I is_closed_onInit (StepWhile>0 (a,s,I)) . k & I is_halting_onInit (StepWhile>0 (a,s,I)) . k ) ) & ((StepWhile>0 (a,s,I)) . (k + 1)) . (intloc 0) = 1 & ( f . ((StepWhile>0 (a,s,I)) . k) = 0 implies ((StepWhile>0 (a,s,I)) . k) . a <= 0 ) & ( ((StepWhile>0 (a,s,I)) . k) . a <= 0 implies f . ((StepWhile>0 (a,s,I)) . k) = 0 ) ) holds
( while>0 (a,I) is_halting_onInit s & while>0 (a,I) is_closed_onInit s )
let a be read-write Int-Location ; :: thesis: for s being State of SCM+FSA st ex f being Function of (product the Object-Kind of SCM+FSA),NAT st
for k being Element of NAT holds
( ( f . ((StepWhile>0 (a,s,I)) . k) <> 0 implies ( f . ((StepWhile>0 (a,s,I)) . (k + 1)) < f . ((StepWhile>0 (a,s,I)) . k) & I is_closed_onInit (StepWhile>0 (a,s,I)) . k & I is_halting_onInit (StepWhile>0 (a,s,I)) . k ) ) & ((StepWhile>0 (a,s,I)) . (k + 1)) . (intloc 0) = 1 & ( f . ((StepWhile>0 (a,s,I)) . k) = 0 implies ((StepWhile>0 (a,s,I)) . k) . a <= 0 ) & ( ((StepWhile>0 (a,s,I)) . k) . a <= 0 implies f . ((StepWhile>0 (a,s,I)) . k) = 0 ) ) holds
( while>0 (a,I) is_halting_onInit s & while>0 (a,I) is_closed_onInit s )
let s be State of SCM+FSA; :: thesis: ( ex f being Function of (product the Object-Kind of SCM+FSA),NAT st
for k being Element of NAT holds
( ( f . ((StepWhile>0 (a,s,I)) . k) <> 0 implies ( f . ((StepWhile>0 (a,s,I)) . (k + 1)) < f . ((StepWhile>0 (a,s,I)) . k) & I is_closed_onInit (StepWhile>0 (a,s,I)) . k & I is_halting_onInit (StepWhile>0 (a,s,I)) . k ) ) & ((StepWhile>0 (a,s,I)) . (k + 1)) . (intloc 0) = 1 & ( f . ((StepWhile>0 (a,s,I)) . k) = 0 implies ((StepWhile>0 (a,s,I)) . k) . a <= 0 ) & ( ((StepWhile>0 (a,s,I)) . k) . a <= 0 implies f . ((StepWhile>0 (a,s,I)) . k) = 0 ) ) implies ( while>0 (a,I) is_halting_onInit s & while>0 (a,I) is_closed_onInit s ) )
set D = Int-Locations \/ FinSeq-Locations;
given f being Function of (product the Object-Kind of SCM+FSA),NAT such that A1: for k being Element of NAT holds
( ( f . ((StepWhile>0 (a,s,I)) . k) <> 0 implies ( f . ((StepWhile>0 (a,s,I)) . (k + 1)) < f . ((StepWhile>0 (a,s,I)) . k) & I is_closed_onInit (StepWhile>0 (a,s,I)) . k & I is_halting_onInit (StepWhile>0 (a,s,I)) . k ) ) & ((StepWhile>0 (a,s,I)) . (k + 1)) . (intloc 0) = 1 & ( f . ((StepWhile>0 (a,s,I)) . k) = 0 implies ((StepWhile>0 (a,s,I)) . k) . a <= 0 ) & ( ((StepWhile>0 (a,s,I)) . k) . a <= 0 implies f . ((StepWhile>0 (a,s,I)) . k) = 0 ) ) ; :: thesis: ( while>0 (a,I) is_halting_onInit s & while>0 (a,I) is_closed_onInit s )
set IniI = Initialized I;
set Iwhile = Initialized (while>0 (a,I));
set s1 = s +* (Initialized (while>0 (a,I)));
A2: IC SCM+FSA in dom (Initialized (while>0 (a,I))) by SCMFSA6A:24;
deffunc H₁( Nat) -> Element of NAT = f . ((StepWhile>0 (a,s,I)) . $1);
A3: for k being Nat holds
( H₁(k + 1) < H₁(k) or H₁(k) = 0 )

proof

let k be Nat; :: thesis: ( H₁(k + 1) < H₁(k) or H₁(k) = 0 )
k in NAT by ORDINAL1:def 13;
hence ( H₁(k + 1) < H₁(k) or H₁(k) = 0 ) by A1; :: thesis: verum

end;

consider m being Nat such that
A4: H₁(m) = 0 and
A5: for n being Nat st H₁(n) = 0 holds
m <= n from NAT_1:sch 17(A3);
reconsider m = m as Element of NAT by ORDINAL1:def 13;
defpred S₁[ Element of NAT ] means ( $1 + 1 <= m implies ex k being Element of NAT st (StepWhile>0 (a,s,I)) . ($1 + 1) = Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),k) );
A6: S₁[ 0 ]

proof

assume 0 + 1 <= m ; :: thesis: ex k being Element of NAT st (StepWhile>0 (a,s,I)) . (0 + 1) = Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),k)
take n = (LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3; :: thesis: (StepWhile>0 (a,s,I)) . (0 + 1) = Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),n)
thus (StepWhile>0 (a,s,I)) . (0 + 1) = Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),n) by Th26; :: thesis: verum

end;

A7: now

let i be Element of NAT ; :: thesis: ( i < m implies ( I is_closed_onInit (StepWhile>0 (a,s,I)) . i & I is_halting_onInit (StepWhile>0 (a,s,I)) . i ) )
assume i < m ; :: thesis: ( I is_closed_onInit (StepWhile>0 (a,s,I)) . i & I is_halting_onInit (StepWhile>0 (a,s,I)) . i )
then H₁(i) <> 0 by A5;
hence ( I is_closed_onInit (StepWhile>0 (a,s,I)) . i & I is_halting_onInit (StepWhile>0 (a,s,I)) . i ) by A1; :: thesis: verum

end;

A8: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A9: S₁[k] ; :: thesis: S₁[k + 1]

now

set sk = (StepWhile>0 (a,s,I)) . k;
set sk1 = (StepWhile>0 (a,s,I)) . (k + 1);
assume A10: (k + 1) + 1 <= m ; :: thesis: ex m being Element of NAT st (StepWhile>0 (a,s,I)) . ((k + 1) + 1) = Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),m)
(k + 1) + 0 < (k + 1) + 1 by XREAL_1:8;
then consider n being Element of NAT such that
A11: (StepWhile>0 (a,s,I)) . (k + 1) = Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),n) by A9, A10, XXREAL_0:2;
A12: ((StepWhile>0 (a,s,I)) . (k + 1)) . (intloc 0) = 1 by A1;
k + 0 < k + (1 + 1) by XREAL_1:8;
then A13: k < m by A10, XXREAL_0:2;
then A14: I is_halting_onInit (StepWhile>0 (a,s,I)) . k by A7;
H₁(k) <> 0 by A5, A13;
then A15: ((StepWhile>0 (a,s,I)) . k) . a > 0 by A1;
take m = n + ((LifeSpan ((ProgramPart (((StepWhile>0 (a,s,I)) . (k + 1)) +* (Initialized I))),(((StepWhile>0 (a,s,I)) . (k + 1)) +* (Initialized I)))) + 3); :: thesis: (StepWhile>0 (a,s,I)) . ((k + 1) + 1) = Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),m)
A16: (StepWhile>0 (a,s,I)) . (k + 1) = Comput ((ProgramPart (((StepWhile>0 (a,s,I)) . k) +* (Initialized (while>0 (a,I))))),(((StepWhile>0 (a,s,I)) . k) +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (((StepWhile>0 (a,s,I)) . k) +* (Initialized I))),(((StepWhile>0 (a,s,I)) . k) +* (Initialized I)))) + 3)) by Def1;
I is_closed_onInit (StepWhile>0 (a,s,I)) . k by A7, A13;
then IC ((StepWhile>0 (a,s,I)) . (k + 1)) = 0 by A16, A14, A15, Th19;
hence (StepWhile>0 (a,s,I)) . ((k + 1) + 1) = Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),m) by A11, A12, Th27; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

A17: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A6, A8);

now

per cases ( m = 0 or m <> 0 ) ;

suppose m = 0 ; :: thesis: ( while>0 (a,I) is_halting_onInit s & while>0 (a,I) is_closed_onInit s )

then ((StepWhile>0 (a,s,I)) . 0) . a <= 0 by A1, A4;
then s . a <= 0 by Def1;
hence ( while>0 (a,I) is_halting_onInit s & while>0 (a,I) is_closed_onInit s ) by Th16; :: thesis: verum

end;

suppose A18: m <> 0 ; :: thesis: ( while>0 (a,I) is_halting_onInit s & while>0 (a,I) is_closed_onInit s )

then consider i being Nat such that
A19: m = i + 1 by NAT_1:6;
reconsider i = i as Element of NAT by ORDINAL1:def 13;
set si = (StepWhile>0 (a,s,I)) . i;
set sm = (StepWhile>0 (a,s,I)) . m;
set sm1 = ((StepWhile>0 (a,s,I)) . m) +* (Initialized (while>0 (a,I)));
set sm2 = ((StepWhile>0 (a,s,I)) . m) +* (Initialize (while>0 (a,I)));
A20: i < m by A19, XREAL_1:31;
then A21: I is_closed_onInit (StepWhile>0 (a,s,I)) . i by A7;
i < m by A19, NAT_1:13;
then H₁(i) <> 0 by A5;
then A22: ((StepWhile>0 (a,s,I)) . i) . a > 0 by A1;
A23: I is_halting_onInit (StepWhile>0 (a,s,I)) . i by A7, A20;
(StepWhile>0 (a,s,I)) . m = Comput ((ProgramPart (((StepWhile>0 (a,s,I)) . i) +* (Initialized (while>0 (a,I))))),(((StepWhile>0 (a,s,I)) . i) +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (((StepWhile>0 (a,s,I)) . i) +* (Initialized I))),(((StepWhile>0 (a,s,I)) . i) +* (Initialized I)))) + 3)) by A19, Def1;
then A24: IC ((StepWhile>0 (a,s,I)) . m) = 0 by A21, A23, A22, Th19;
((StepWhile>0 (a,s,I)) . (i + 1)) . (intloc 0) = 1 by A1;
then A25: ((StepWhile>0 (a,s,I)) . m) +* (Initialized (while>0 (a,I))) = ((StepWhile>0 (a,s,I)) . m) +* (Initialize (while>0 (a,I))) by A19, SCMFSA8C:18;
then A26: IC (((StepWhile>0 (a,s,I)) . m) +* (Initialize (while>0 (a,I)))) = (Initialized (while>0 (a,I))) . (IC SCM+FSA) by A2, FUNCT_4:14
.= IC ((StepWhile>0 (a,s,I)) . m) by A24, SCMFSA6A:46 ;
set p = (LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3;
A27: DataPart (((StepWhile>0 (a,s,I)) . m) +* (Initialize (while>0 (a,I)))) = DataPart ((StepWhile>0 (a,s,I)) . m) by SCMFSA8A:11;
m = i + 1 by A19;
then consider n being Element of NAT such that
A28: (StepWhile>0 (a,s,I)) . m = Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),n) by A17;
ProgramPart ((StepWhile>0 (a,s,I)) . m) = ProgramPart (s +* (Initialized (while>0 (a,I)))) by A28, AMI_1:123;
then B29: ProgramPart (((StepWhile>0 (a,s,I)) . m) +* (Initialize (while>0 (a,I)))) = ProgramPart ((StepWhile>0 (a,s,I)) . m) by A25, FUNCT_4:100;
then A29: ((StepWhile>0 (a,s,I)) . m) +* (Initialized (while>0 (a,I))) = (StepWhile>0 (a,s,I)) . m by A25, A26, A27, SCMFSA_9:29;
A30: ((StepWhile>0 (a,s,I)) . m) . a <= 0 by A1, A4;
then while>0 (a,I) is_halting_onInit (StepWhile>0 (a,s,I)) . m by Th16;
then ProgramPart (((StepWhile>0 (a,s,I)) . m) +* (Initialized (while>0 (a,I)))) halts_on ((StepWhile>0 (a,s,I)) . m) +* (Initialized (while>0 (a,I))) by SCM_HALT:def 5;
then consider j being Element of NAT such that
A31: CurInstr ((ProgramPart ((StepWhile>0 (a,s,I)) . m)),(Comput ((ProgramPart ((StepWhile>0 (a,s,I)) . m)),((StepWhile>0 (a,s,I)) . m),j))) = halt SCM+FSA by A29, EXTPRO_1:30;
T: ProgramPart (s +* (Initialized (while>0 (a,I)))) = ProgramPart (Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),n)) by AMI_1:123;
x: Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),(j + n)) = Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),n)),j) by EXTPRO_1:5;
ProgramPart (s +* (Initialized (while>0 (a,I)))) halts_on s +* (Initialized (while>0 (a,I))) by A28, A31, x, T, EXTPRO_1:30;
hence while>0 (a,I) is_halting_onInit s by SCM_HALT:def 5; :: thesis: while>0 (a,I) is_closed_onInit s

now

let q be Element of NAT ; :: thesis: IC (Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),b₁)) in dom (while>0 (a,I))

per cases ( q <= (LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3 or q > (LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3 ) ;

suppose A32: q <= (LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3 ; :: thesis: IC (Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),b₁)) in dom (while>0 (a,I))

A33: (StepWhile>0 (a,s,I)) . 0 = s by Def1;
then A34: I is_halting_onInit s by A7, A18;
H₁( 0 ) <> 0 by A5, A18;
then A35: s . a > 0 by A1, A33;
I is_closed_onInit s by A7, A18, A33;
hence IC (Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),q)) in dom (while>0 (a,I)) by A32, A35, A34, Th19; :: thesis: verum

end;

suppose A36: q > (LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3 ; :: thesis: IC (Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),b₁)) in dom (while>0 (a,I))

A37: now

take k = (LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3; :: thesis: ( (StepWhile>0 (a,s,I)) . 1 = Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),k) & k <= q )
thus ( (StepWhile>0 (a,s,I)) . 1 = Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),k) & k <= q ) by A36, Th26; :: thesis: verum

end;

defpred S₂[ Nat] means ( $1 <= m & $1 <> 0 & ex k being Element of NAT st
( (StepWhile>0 (a,s,I)) . $1 = Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),k) & k <= q ) );
A38: for i being Nat st S₂[i] holds
i <= m ;
0 + 1 < m + 1 by A18, XREAL_1:8;
then 1 <= m by NAT_1:13;
then A39: ex t being Nat st S₂[t] by A37;
consider t being Nat such that
A40: ( S₂[t] & ( for i being Nat st S₂[i] holds
i <= t ) ) from NAT_1:sch 6(A38, A39);
reconsider t = t as Element of NAT by ORDINAL1:def 13;

now

per cases ( t = m or t <> m ) ;

suppose t = m ; :: thesis: IC (Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),q)) in dom (while>0 (a,I))

then consider r being Element of NAT such that
A41: (StepWhile>0 (a,s,I)) . m = Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),r) and
A42: r <= q by A40;
consider x being Nat such that
A43: q = r + x by A42, NAT_1:10;
A44: while>0 (a,I) is_closed_onInit (StepWhile>0 (a,s,I)) . m by A30, Th16;
reconsider x = x as Element of NAT by ORDINAL1:def 13;
T: ProgramPart (s +* (Initialized (while>0 (a,I)))) = ProgramPart (((StepWhile>0 (a,s,I)) . m) +* (Initialized (while>0 (a,I)))) by B29, A41, A25, AMI_1:123;
Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),q) = Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(((StepWhile>0 (a,s,I)) . m) +* (Initialized (while>0 (a,I)))),x) by A29, A41, A43, EXTPRO_1:5;
hence IC (Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),q)) in dom (while>0 (a,I)) by A44, T, SCM_HALT:def 4; :: thesis: verum

end;

suppose A45: t <> m ; :: thesis: IC (Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),q)) in dom (while>0 (a,I))

set Dt = (StepWhile>0 (a,s,I)) . t;
A46: t < m by A40, A45, XXREAL_0:1;
then A47: I is_closed_onInit (StepWhile>0 (a,s,I)) . t by A7;
A48: I is_halting_onInit (StepWhile>0 (a,s,I)) . t by A7, A46;
consider y being Nat such that
A49: t = y + 1 by A40, NAT_1:6;
reconsider y = y as Element of NAT by ORDINAL1:def 13;
t = y + 1 by A49;
then A50: ((StepWhile>0 (a,s,I)) . t) . (intloc 0) = 1 by A1;
H₁(t) <> 0 by A5, A46;
then A51: ((StepWhile>0 (a,s,I)) . t) . a > 0 by A1;
consider z being Element of NAT such that
A52: (StepWhile>0 (a,s,I)) . t = Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),z) and
A53: z <= q by A40;
set z2 = z + ((LifeSpan ((ProgramPart (((StepWhile>0 (a,s,I)) . t) +* (Initialized I))),(((StepWhile>0 (a,s,I)) . t) +* (Initialized I)))) + 3);
consider w being Nat such that
A54: q = z + w by A53, NAT_1:10;
set Dy = (StepWhile>0 (a,s,I)) . y;
y + 0 < t by A49, XREAL_1:8;
then A55: y < m by A40, XXREAL_0:2;
then A56: I is_closed_onInit (StepWhile>0 (a,s,I)) . y by A7;
H₁(y) <> 0 by A5, A55;
then A57: ((StepWhile>0 (a,s,I)) . y) . a > 0 by A1;
A58: I is_halting_onInit (StepWhile>0 (a,s,I)) . y by A7, A55;
reconsider w = w as Element of NAT by ORDINAL1:def 13;
(StepWhile>0 (a,s,I)) . t = Comput ((ProgramPart (((StepWhile>0 (a,s,I)) . y) +* (Initialized (while>0 (a,I))))),(((StepWhile>0 (a,s,I)) . y) +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (((StepWhile>0 (a,s,I)) . y) +* (Initialized I))),(((StepWhile>0 (a,s,I)) . y) +* (Initialized I)))) + 3)) by A49, Def1;
then A59: IC ((StepWhile>0 (a,s,I)) . t) = 0 by A56, A58, A57, Th19;
X: (StepWhile>0 (a,s,I)) . t = ((StepWhile>0 (a,s,I)) . t) +* (Initialized (while>0 (a,I))) by A50, A52, A59, Th27;

now

assume A60: z + ((LifeSpan ((ProgramPart (((StepWhile>0 (a,s,I)) . t) +* (Initialized I))),(((StepWhile>0 (a,s,I)) . t) +* (Initialized I)))) + 3) <= q ; :: thesis: contradiction

A61: now

take k = z + ((LifeSpan ((ProgramPart (((StepWhile>0 (a,s,I)) . t) +* (Initialized I))),(((StepWhile>0 (a,s,I)) . t) +* (Initialized I)))) + 3); :: thesis: ( (StepWhile>0 (a,s,I)) . (t + 1) = Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),k) & k <= q )
thus ( (StepWhile>0 (a,s,I)) . (t + 1) = Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),k) & k <= q ) by A50, A52, A59, A60, Th27; :: thesis: verum

end;

t + 1 <= m by A46, NAT_1:13;
hence contradiction by A40, A61, XREAL_1:31; :: thesis: verum

end;

then A62: w < (LifeSpan ((ProgramPart (((StepWhile>0 (a,s,I)) . t) +* (Initialized I))),(((StepWhile>0 (a,s,I)) . t) +* (Initialized I)))) + 3 by A54, XREAL_1:8;
Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),q) = Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),((StepWhile>0 (a,s,I)) . t),w) by A52, A54, EXTPRO_1:5
.= Comput ((ProgramPart (((StepWhile>0 (a,s,I)) . t) +* (Initialized (while>0 (a,I))))),(((StepWhile>0 (a,s,I)) . t) +* (Initialized (while>0 (a,I)))),w) by X, A52, AMI_1:123 ;
hence IC (Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),q)) in dom (while>0 (a,I)) by A62, A47, A48, A51, Th19; :: thesis: verum

end;

end;

end;

hence IC (Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),q)) in dom (while>0 (a,I)) ; :: thesis: verum

end;

end;

end;

hence while>0 (a,I) is_closed_onInit s by SCM_HALT:def 4; :: thesis: verum

end;

end;

end;

hence ( while>0 (a,I) is_halting_onInit s & while>0 (a,I) is_closed_onInit s ) ; :: thesis: verum