let I be really-closed good InitHalting MacroInstruction of SCM+FSA ; :: thesis: for a being read-write Int-Location st ( for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA st s . a > 0 holds

(IExec (I,P,s)) . a < s . a ) holds

while>0 (a,I) is InitHalting

let a be read-write Int-Location; :: thesis: ( ( for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA st s . a > 0 holds

(IExec (I,P,s)) . a < s . a ) implies while>0 (a,I) is InitHalting )

set D = Data-Locations ;

defpred S_{1}[ Nat] means for t being State of SCM+FSA

for Q being Instruction-Sequence of SCM+FSA st t . a <= $1 holds

while>0 (a,I) is_halting_onInit t,Q;

assume A1: for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA st s . a > 0 holds

(IExec (I,P,s)) . a < s . a ; :: thesis: while>0 (a,I) is InitHalting

_{1}[ 0 ]
by Lm6;

A14: for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A13, A2);

for P being Instruction-Sequence of SCM+FSA st s . a > 0 holds

(IExec (I,P,s)) . a < s . a ) holds

while>0 (a,I) is InitHalting

let a be read-write Int-Location; :: thesis: ( ( for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA st s . a > 0 holds

(IExec (I,P,s)) . a < s . a ) implies while>0 (a,I) is InitHalting )

set D = Data-Locations ;

defpred S

for Q being Instruction-Sequence of SCM+FSA st t . a <= $1 holds

while>0 (a,I) is_halting_onInit t,Q;

assume A1: for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA st s . a > 0 holds

(IExec (I,P,s)) . a < s . a ; :: thesis: while>0 (a,I) is InitHalting

A2: now :: thesis: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

A13:
SS

let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A3: S_{1}[k]
; :: thesis: S_{1}[k + 1]

_{1}[k + 1]
; :: thesis: verum

end;assume A3: S

now :: thesis: for t being State of SCM+FSA

for Q being Instruction-Sequence of SCM+FSA st t . a <= k + 1 holds

while>0 (a,I) is_halting_onInit t,Q

hence
Sfor Q being Instruction-Sequence of SCM+FSA st t . a <= k + 1 holds

while>0 (a,I) is_halting_onInit t,Q

let t be State of SCM+FSA; :: thesis: for Q being Instruction-Sequence of SCM+FSA st t . a <= k + 1 holds

while>0 (a,I) is_halting_onInit b_{2},b_{3}

let Q be Instruction-Sequence of SCM+FSA; :: thesis: ( t . a <= k + 1 implies while>0 (a,I) is_halting_onInit b_{1},b_{2} )

assume A4: t . a <= k + 1 ; :: thesis: while>0 (a,I) is_halting_onInit b_{1},b_{2}

end;while>0 (a,I) is_halting_onInit b

let Q be Instruction-Sequence of SCM+FSA; :: thesis: ( t . a <= k + 1 implies while>0 (a,I) is_halting_onInit b

assume A4: t . a <= k + 1 ; :: thesis: while>0 (a,I) is_halting_onInit b

per cases
( t . a <> k + 1 or t . a = k + 1 )
;

end;

suppose
t . a <> k + 1
; :: thesis: while>0 (a,I) is_halting_onInit b_{1},b_{2}

then
t . a < k + 1
by A4, XXREAL_0:1;

hence while>0 (a,I) is_halting_onInit t,Q by A3, INT_1:7; :: thesis: verum

end;hence while>0 (a,I) is_halting_onInit t,Q by A3, INT_1:7; :: thesis: verum

suppose A5:
t . a = k + 1
; :: thesis: while>0 (a,I) is_halting_onInit b_{1},b_{2}

set l0 = intloc 0;

set tW0 = Initialized t;

set QW = Q +* (while>0 (a,I));

set t1 = Initialized t;

set Q1 = Q +* I;

set Wt = Comput ((Q +* (while>0 (a,I))),(Initialized t),((LifeSpan ((Q +* I),(Initialized t))) + 2));

set A = NAT ;

set It = Comput ((Q +* I),(Initialized t),(LifeSpan ((Q +* I),(Initialized t))));

A6: I is_halting_onInit t,Q by Th23;

then Q +* I halts_on Initialized t ;

then A7: Q +* I halts_on Initialized t ;

A8: DataPart (Comput ((Q +* (while>0 (a,I))),(Initialized t),((LifeSpan ((Q +* I),(Initialized t))) + 2))) = DataPart (Comput ((Q +* I),(Initialized t),(LifeSpan ((Q +* I),(Initialized t))))) by A5, A6, Lm7;

then A9: (Comput ((Q +* (while>0 (a,I))),(Initialized t),((LifeSpan ((Q +* I),(Initialized t))) + 2))) . (intloc 0) = (Comput ((Q +* I),(Initialized t),(LifeSpan ((Q +* I),(Initialized t))))) . (intloc 0) by SCMFSA_M:2

.= (Result ((Q +* I),(Initialized t))) . (intloc 0) by A7, EXTPRO_1:23

.= (Result ((Q +* I),(Initialized t))) . (intloc 0)

.= (IExec (I,Q,t)) . (intloc 0) by SCMFSA6B:def 1

.= 1 by Th7 ;

(Comput ((Q +* (while>0 (a,I))),(Initialized t),((LifeSpan ((Q +* I),(Initialized t))) + 2))) . a = (Comput ((Q +* I),(Initialized t),(LifeSpan ((Q +* I),(Initialized t))))) . a by A8, SCMFSA_M:2

.= (Result ((Q +* I),(Initialized t))) . a by A7, EXTPRO_1:23

.= (Result ((Q +* I),(Initialized t))) . a

.= (IExec (I,Q,t)) . a by SCMFSA6B:def 1 ;

then (Comput ((Q +* (while>0 (a,I))),(Initialized t),((LifeSpan ((Q +* I),(Initialized t))) + 2))) . a < k + 1 by A1, A5;

then while>0 (a,I) is_halting_onInit Comput ((Q +* (while>0 (a,I))),(Initialized t),((LifeSpan ((Q +* I),(Initialized t))) + 2)),Q +* (while>0 (a,I)) by A3, INT_1:7;

then (Q +* (while>0 (a,I))) +* (while>0 (a,I)) halts_on Initialized (Comput ((Q +* (while>0 (a,I))),(Initialized t),((LifeSpan ((Q +* I),(Initialized t))) + 2))) ;

then A10: (Q +* (while>0 (a,I))) +* (while>0 (a,I)) halts_on Initialized (Comput ((Q +* (while>0 (a,I))),(Initialized t),((LifeSpan ((Q +* I),(Initialized t))) + 2))) ;

IC (Comput ((Q +* (while>0 (a,I))),(Initialized t),((LifeSpan ((Q +* I),(Initialized t))) + 2))) = 0 by A5, A6, Lm7;

then A11: Initialized (Comput ((Q +* (while>0 (a,I))),(Initialized t),((LifeSpan ((Q +* I),(Initialized t))) + 2))) = Comput ((Q +* (while>0 (a,I))),(Initialized t),((LifeSpan ((Q +* I),(Initialized t))) + 2)) by A9, SCMFSA_M:8;

then Q +* (while>0 (a,I)) halts_on Initialized t ;

hence while>0 (a,I) is_halting_onInit t,Q ; :: thesis: verum

end;set tW0 = Initialized t;

set QW = Q +* (while>0 (a,I));

set t1 = Initialized t;

set Q1 = Q +* I;

set Wt = Comput ((Q +* (while>0 (a,I))),(Initialized t),((LifeSpan ((Q +* I),(Initialized t))) + 2));

set A = NAT ;

set It = Comput ((Q +* I),(Initialized t),(LifeSpan ((Q +* I),(Initialized t))));

A6: I is_halting_onInit t,Q by Th23;

then Q +* I halts_on Initialized t ;

then A7: Q +* I halts_on Initialized t ;

A8: DataPart (Comput ((Q +* (while>0 (a,I))),(Initialized t),((LifeSpan ((Q +* I),(Initialized t))) + 2))) = DataPart (Comput ((Q +* I),(Initialized t),(LifeSpan ((Q +* I),(Initialized t))))) by A5, A6, Lm7;

then A9: (Comput ((Q +* (while>0 (a,I))),(Initialized t),((LifeSpan ((Q +* I),(Initialized t))) + 2))) . (intloc 0) = (Comput ((Q +* I),(Initialized t),(LifeSpan ((Q +* I),(Initialized t))))) . (intloc 0) by SCMFSA_M:2

.= (Result ((Q +* I),(Initialized t))) . (intloc 0) by A7, EXTPRO_1:23

.= (Result ((Q +* I),(Initialized t))) . (intloc 0)

.= (IExec (I,Q,t)) . (intloc 0) by SCMFSA6B:def 1

.= 1 by Th7 ;

(Comput ((Q +* (while>0 (a,I))),(Initialized t),((LifeSpan ((Q +* I),(Initialized t))) + 2))) . a = (Comput ((Q +* I),(Initialized t),(LifeSpan ((Q +* I),(Initialized t))))) . a by A8, SCMFSA_M:2

.= (Result ((Q +* I),(Initialized t))) . a by A7, EXTPRO_1:23

.= (Result ((Q +* I),(Initialized t))) . a

.= (IExec (I,Q,t)) . a by SCMFSA6B:def 1 ;

then (Comput ((Q +* (while>0 (a,I))),(Initialized t),((LifeSpan ((Q +* I),(Initialized t))) + 2))) . a < k + 1 by A1, A5;

then while>0 (a,I) is_halting_onInit Comput ((Q +* (while>0 (a,I))),(Initialized t),((LifeSpan ((Q +* I),(Initialized t))) + 2)),Q +* (while>0 (a,I)) by A3, INT_1:7;

then (Q +* (while>0 (a,I))) +* (while>0 (a,I)) halts_on Initialized (Comput ((Q +* (while>0 (a,I))),(Initialized t),((LifeSpan ((Q +* I),(Initialized t))) + 2))) ;

then A10: (Q +* (while>0 (a,I))) +* (while>0 (a,I)) halts_on Initialized (Comput ((Q +* (while>0 (a,I))),(Initialized t),((LifeSpan ((Q +* I),(Initialized t))) + 2))) ;

IC (Comput ((Q +* (while>0 (a,I))),(Initialized t),((LifeSpan ((Q +* I),(Initialized t))) + 2))) = 0 by A5, A6, Lm7;

then A11: Initialized (Comput ((Q +* (while>0 (a,I))),(Initialized t),((LifeSpan ((Q +* I),(Initialized t))) + 2))) = Comput ((Q +* (while>0 (a,I))),(Initialized t),((LifeSpan ((Q +* I),(Initialized t))) + 2)) by A9, SCMFSA_M:8;

now :: thesis: ex mm being set st CurInstr ((Q +* (while>0 (a,I))),(Comput ((Q +* (while>0 (a,I))),(Initialized t),mm))) = halt SCM+FSA

then
Q +* (while>0 (a,I)) halts_on Initialized t
by EXTPRO_1:29;consider m being Nat such that

A12: CurInstr ((Q +* (while>0 (a,I))),(Comput ((Q +* (while>0 (a,I))),(Comput ((Q +* (while>0 (a,I))),(Initialized t),((LifeSpan ((Q +* I),(Initialized t))) + 2))),m))) = halt SCM+FSA by A11, A10;

take mm = ((LifeSpan ((Q +* I),(Initialized t))) + 2) + m; :: thesis: CurInstr ((Q +* (while>0 (a,I))),(Comput ((Q +* (while>0 (a,I))),(Initialized t),mm))) = halt SCM+FSA

thus CurInstr ((Q +* (while>0 (a,I))),(Comput ((Q +* (while>0 (a,I))),(Initialized t),mm))) = halt SCM+FSA by A12, EXTPRO_1:4; :: thesis: verum

end;A12: CurInstr ((Q +* (while>0 (a,I))),(Comput ((Q +* (while>0 (a,I))),(Comput ((Q +* (while>0 (a,I))),(Initialized t),((LifeSpan ((Q +* I),(Initialized t))) + 2))),m))) = halt SCM+FSA by A11, A10;

take mm = ((LifeSpan ((Q +* I),(Initialized t))) + 2) + m; :: thesis: CurInstr ((Q +* (while>0 (a,I))),(Comput ((Q +* (while>0 (a,I))),(Initialized t),mm))) = halt SCM+FSA

thus CurInstr ((Q +* (while>0 (a,I))),(Comput ((Q +* (while>0 (a,I))),(Initialized t),mm))) = halt SCM+FSA by A12, EXTPRO_1:4; :: thesis: verum

then Q +* (while>0 (a,I)) halts_on Initialized t ;

hence while>0 (a,I) is_halting_onInit t,Q ; :: thesis: verum

A14: for k being Nat holds S

now :: thesis: for t being State of SCM+FSA

for Q being Instruction-Sequence of SCM+FSA holds while>0 (a,I) is_halting_onInit t,Q

hence
while>0 (a,I) is InitHalting
by Th23; :: thesis: verumfor Q being Instruction-Sequence of SCM+FSA holds while>0 (a,I) is_halting_onInit t,Q

let t be State of SCM+FSA; :: thesis: for Q being Instruction-Sequence of SCM+FSA holds while>0 (a,I) is_halting_onInit Q,b_{2}

end;per cases
( t . a <= 0 or t . a > 0 )
;

end;

suppose
t . a <= 0
; :: thesis: for Q being Instruction-Sequence of SCM+FSA holds while>0 (a,I) is_halting_onInit Q,b_{2}

hence
for Q being Instruction-Sequence of SCM+FSA holds while>0 (a,I) is_halting_onInit t,Q
by Lm6; :: thesis: verum

end;suppose
t . a > 0
; :: thesis: for Q being Instruction-Sequence of SCM+FSA holds while>0 (a,I) is_halting_onInit Q,b_{2}

then reconsider n = t . a as Element of NAT by INT_1:3;

S_{1}[n]
by A14;

hence for Q being Instruction-Sequence of SCM+FSA holds while>0 (a,I) is_halting_onInit t,Q ; :: thesis: verum

end;S

hence for Q being Instruction-Sequence of SCM+FSA holds while>0 (a,I) is_halting_onInit t,Q ; :: thesis: verum