let s be State of SCM+FSA; for p being Instruction-Sequence of SCM+FSA
for a being Int-Location
for J being really-closed good MacroInstruction of SCM+FSA st ProperTimesBody a,J,s,p holds
for k being Nat st k <= s . a holds
((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1
let p be Instruction-Sequence of SCM+FSA; for a being Int-Location
for J being really-closed good MacroInstruction of SCM+FSA st ProperTimesBody a,J,s,p holds
for k being Nat st k <= s . a holds
((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1
let a be Int-Location; for J being really-closed good MacroInstruction of SCM+FSA st ProperTimesBody a,J,s,p holds
for k being Nat st k <= s . a holds
((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1
let J be really-closed good MacroInstruction of SCM+FSA ; ( ProperTimesBody a,J,s,p implies for k being Nat st k <= s . a holds
((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 )
set I = J;
set ST = StepTimes (a,J,p,s);
set au = 1 -stRWNotIn ({a} \/ (UsedILoc J));
set Is = Initialized s;
defpred S1[ Nat] means ( $1 <= s . a implies ((StepTimes (a,J,p,s)) . $1) . (intloc 0) = 1 );
assume A1:
ProperTimesBody a,J,s,p
; for k being Nat st k <= s . a holds
((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1
A2:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume that A3:
(
k <= s . a implies
((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 )
and A4:
k + 1
<= s . a
;
((StepTimes (a,J,p,s)) . (k + 1)) . (intloc 0) = 1
reconsider sa =
s . a as
Element of
NAT by A4, INT_1:3;
A5:
k < sa
by A4, NAT_1:13;
then
J is_halting_on (StepTimes (a,J,p,s)) . k,
p +* (times* (a,J))
by A1;
hence
((StepTimes (a,J,p,s)) . (k + 1)) . (intloc 0) = 1
by A3, A5, Th8;
verum
end;
A6:
S1[ 0 ]
thus
for k being Nat holds S1[k]
from NAT_1:sch 2(A6, A2); verum