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 S1[ 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
A2: now :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; :: thesis: S1[k + 1]
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
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 b2,b3
let Q be Instruction-Sequence of SCM+FSA; :: thesis: ( t . a <= k + 1 implies while>0 (a,I) is_halting_onInit b1,b2 )
assume A4: t . a <= k + 1 ; :: thesis: while>0 (a,I) is_halting_onInit b1,b2
per cases ( t . a <> k + 1 or t . a = k + 1 ) ;
suppose A5: t . a = k + 1 ; :: thesis: while>0 (a,I) is_halting_onInit b1,b2
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;
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
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;
then Q +* (while>0 (a,I)) halts_on Initialized t by EXTPRO_1:29;
then Q +* (while>0 (a,I)) halts_on Initialized t ;
hence while>0 (a,I) is_halting_onInit t,Q ; :: thesis: verum
end;
end;
end;
hence S1[k + 1] ; :: thesis: verum
end;
A13: S1[ 0 ] by Lm6;
A14: for k being Nat holds S1[k] from NAT_1:sch 2(A13, A2);
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
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,b2
per cases ( t . a <= 0 or t . a > 0 ) ;
end;
end;
hence while>0 (a,I) is InitHalting by Th23; :: thesis: verum