let I be InitHalting good really-closed MacroInstruction of SCM+FSA ; :: thesis: for a being read-write Int-Location st ex f being Function of (product (the_Values_of SCM+FSA)),INT st

for s, t being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA holds

( ( f . s > 0 implies f . (IExec (I,P,s)) < f . s ) & ( DataPart s = DataPart t implies f . s = f . t ) & ( f . s <= 0 implies s . a <= 0 ) & ( s . a <= 0 implies f . s <= 0 ) ) holds

while>0 (a,I) is InitHalting

let a be read-write Int-Location; :: thesis: ( ex f being Function of (product (the_Values_of SCM+FSA)),INT st

for s, t being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA holds

( ( f . s > 0 implies f . (IExec (I,P,s)) < f . s ) & ( DataPart s = DataPart t implies f . s = f . t ) & ( f . s <= 0 implies s . a <= 0 ) & ( s . a <= 0 implies f . s <= 0 ) ) implies while>0 (a,I) is InitHalting )

set D = Data-Locations ;

given f being Function of (product (the_Values_of SCM+FSA)),INT such that A1: for s, t being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA holds

( ( f . s > 0 implies f . (IExec (I,P,s)) < f . s ) & ( DataPart s = DataPart t implies f . s = f . t ) & ( f . s <= 0 implies s . a <= 0 ) & ( s . a <= 0 implies f . s <= 0 ) ) ; :: thesis: while>0 (a,I) is InitHalting

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

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

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

_{1}[ 0 ]
_{1}[k]
from NAT_1:sch 2(A14, A2);

for s, t being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA holds

( ( f . s > 0 implies f . (IExec (I,P,s)) < f . s ) & ( DataPart s = DataPart t implies f . s = f . t ) & ( f . s <= 0 implies s . a <= 0 ) & ( s . a <= 0 implies f . s <= 0 ) ) holds

while>0 (a,I) is InitHalting

let a be read-write Int-Location; :: thesis: ( ex f being Function of (product (the_Values_of SCM+FSA)),INT st

for s, t being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA holds

( ( f . s > 0 implies f . (IExec (I,P,s)) < f . s ) & ( DataPart s = DataPart t implies f . s = f . t ) & ( f . s <= 0 implies s . a <= 0 ) & ( s . a <= 0 implies f . s <= 0 ) ) implies while>0 (a,I) is InitHalting )

set D = Data-Locations ;

given f being Function of (product (the_Values_of SCM+FSA)),INT such that A1: for s, t being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA holds

( ( f . s > 0 implies f . (IExec (I,P,s)) < f . s ) & ( DataPart s = DataPart t implies f . s = f . t ) & ( f . s <= 0 implies s . a <= 0 ) & ( s . a <= 0 implies f . s <= 0 ) ) ; :: thesis: while>0 (a,I) is InitHalting

defpred S

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

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

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

S_{1}[k + 1]

A14:
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 f . t <= k + 1 holds

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

hence
Sfor Q being Instruction-Sequence of SCM+FSA st f . t <= 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 f . t <= k + 1 holds

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

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

assume A4: f . t <= 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: ( f . t <= k + 1 implies while>0 (a,I) is_halting_onInit b

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

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

end;

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

then
f . t < 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:
f . t = 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 It = Comput ((Q +* I),(Initialized t),(LifeSpan ((Q +* I),(Initialized t))));

A6: I is_halting_onInit t,Q by SCM_HALT:26;

then A7: Q +* I halts_on Initialized t ;

A8: not t . a <= 0 by A1, A5;

then A9: 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 A6, SCM_HALT:74;

then A10: (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 SCM_HALT:9 ;

DataPart (Comput ((Q +* (while>0 (a,I))),(Initialized t),((LifeSpan ((Q +* I),(Initialized t))) + 2))) = DataPart (Result ((Q +* I),(Initialized t))) by A9, A7, EXTPRO_1:23

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

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

then f . (Comput ((Q +* (while>0 (a,I))),(Initialized t),((LifeSpan ((Q +* I),(Initialized t))) + 2))) = f . (IExec (I,Q,t)) by A1;

then f . (Comput ((Q +* (while>0 (a,I))),(Initialized t),((LifeSpan ((Q +* I),(Initialized t))) + 2))) < 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 A11: (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 A8, A6, SCM_HALT:74;

then A12: 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 A10, SCMFSA_M:8;

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 It = Comput ((Q +* I),(Initialized t),(LifeSpan ((Q +* I),(Initialized t))));

A6: I is_halting_onInit t,Q by SCM_HALT:26;

then A7: Q +* I halts_on Initialized t ;

A8: not t . a <= 0 by A1, A5;

then A9: 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 A6, SCM_HALT:74;

then A10: (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 SCM_HALT:9 ;

DataPart (Comput ((Q +* (while>0 (a,I))),(Initialized t),((LifeSpan ((Q +* I),(Initialized t))) + 2))) = DataPart (Result ((Q +* I),(Initialized t))) by A9, A7, EXTPRO_1:23

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

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

then f . (Comput ((Q +* (while>0 (a,I))),(Initialized t),((LifeSpan ((Q +* I),(Initialized t))) + 2))) = f . (IExec (I,Q,t)) by A1;

then f . (Comput ((Q +* (while>0 (a,I))),(Initialized t),((LifeSpan ((Q +* I),(Initialized t))) + 2))) < 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 A11: (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 A8, A6, SCM_HALT:74;

then A12: 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 A10, 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

A13: 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 A12, A11;

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 A13, EXTPRO_1:4; :: thesis: verum

end;A13: 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 A12, A11;

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 A13, EXTPRO_1:4; :: thesis: verum

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

proof

A15:
for k being Nat holds S
let t be State of SCM+FSA; :: thesis: for Q being Instruction-Sequence of SCM+FSA st f . t <= 0 holds

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

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

assume f . t <= 0 ; :: thesis: while>0 (a,I) is_halting_onInit t,Q

then t . a <= 0 by A1;

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

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

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

assume f . t <= 0 ; :: thesis: while>0 (a,I) is_halting_onInit t,Q

then t . a <= 0 by A1;

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

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 SCM_HALT:26; :: 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
( f . t <= 0 or f . t > 0 )
;

end;

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

then
t . a <= 0
by A1;

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

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

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

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

S_{1}[n]
by A15;

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