let s be State of SCM+FSA; for p being Instruction-Sequence of SCM+FSA
for d being read-write Int-Location st 0 <= s . d holds
(IExec ((triv-times d),p,s)) . d = 0
let p be Instruction-Sequence of SCM+FSA; for d being read-write Int-Location st 0 <= s . d holds
(IExec ((triv-times d),p,s)) . d = 0
let d be read-write Int-Location; ( 0 <= s . d implies (IExec ((triv-times d),p,s)) . d = 0 )
set a = d;
set I1 = while=0 (d,(Macro (d := d)));
set i2 = SubFrom (d,(intloc 0));
set I = (while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)));
set au = 1 -stRWNotIn ({d} \/ (UsedILoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))));
set ST = StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s);
defpred S1[ Nat] means ( ( $1 < s . d implies ( (while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))) is_halting_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . $1,p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) & ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . $1) . (intloc 0) = 1 ) ) & ( $1 <= s . d implies ( (((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . $1) . d) + $1 = s . d & ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . $1) . (1 -stRWNotIn ({d} \/ (UsedILoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) = ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . $1) . d ) ) );
d in {d,(intloc 0)}
by TARSKI:def 2;
then
d in UsedIntLoc (SubFrom (d,(intloc 0)))
by SF_MASTR:14;
then
d in (UsedILoc (while=0 (d,(Macro (d := d))))) \/ (UsedIntLoc (SubFrom (d,(intloc 0))))
by XBOOLE_0:def 3;
then A1:
d in UsedILoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))
by SF_MASTR:30;
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 . d implies (
(while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))) is_halting_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k,
p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) &
((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k) . (intloc 0) = 1 ) )
and A4:
(
k <= s . d implies (
(((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k) . d) + k = s . d &
((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k) . (1 -stRWNotIn ({d} \/ (UsedILoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) = ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k) . d ) )
;
S1[k + 1]
A5:
now ( k < s . d implies ( ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k) . (1 -stRWNotIn ({d} \/ (UsedILoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) > 0 & (((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . d) + (k + 1) = s . d ) )assume A6:
k < s . d
;
( ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k) . (1 -stRWNotIn ({d} \/ (UsedILoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) > 0 & (((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . d) + (k + 1) = s . d )then A7:
((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k) . d <> 0
by A4;
then A8:
DataPart (IExec ((while=0 (d,(Macro (d := d)))),(p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))),((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k))) = DataPart ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k)
by A3, A6, SCMFSA9A:22;
while=0 (
d,
(Macro (d := d)))
is_halting_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k,
p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))
by A7, SCMFSA_9:18;
then A9:
while=0 (
d,
(Macro (d := d)))
is_halting_on Initialized ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k),
p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))
by A3, A6, SCMFSA8B:42;
A10:
k - k < (s . d) - k
by A6, XREAL_1:9;
hence
((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k) . (1 -stRWNotIn ({d} \/ (UsedILoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) > 0
by A4, A6;
(((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . d) + (k + 1) = s . d
(while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))) is_halting_on Initialized ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k),
p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))
by A3, A6, SCMFSA8B:42;
then
((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) | ((UsedILoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))) \/ FinSeq-Locations) = (IExec (((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),(p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))),((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k))) | ((UsedILoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))) \/ FinSeq-Locations)
by A3, A4, A6, A10, Th16;
then ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . d =
(IExec (((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),(p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))),((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k))) . d
by A1, SCMFSA_M:28
.=
(Exec ((SubFrom (d,(intloc 0))),(IExec ((while=0 (d,(Macro (d := d)))),(p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))),((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k))))) . d
by A9, SFMASTR1:11
.=
((IExec ((while=0 (d,(Macro (d := d)))),(p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))),((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k))) . d) - ((IExec ((while=0 (d,(Macro (d := d)))),(p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))),((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k))) . (intloc 0))
by SCMFSA_2:65
.=
(((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k) . d) - ((IExec ((while=0 (d,(Macro (d := d)))),(p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))),((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k))) . (intloc 0))
by A8, SCMFSA_M:2
.=
(((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k) . d) - 1
by A3, A6, A8, SCMFSA_M:2
;
hence
(((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . d) + (k + 1) = s . d
by A4, A6;
verum end;
hereby ( k + 1 <= s . d implies ( (((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . d) + (k + 1) = s . d & ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . (1 -stRWNotIn ({d} \/ (UsedILoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) = ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . d ) )
assume A11:
k + 1
< s . d
;
( (while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))) is_halting_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1),p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) & ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . (intloc 0) = 1 )then reconsider sa =
s . d as
Element of
NAT by INT_1:3;
A12:
k < sa
by A11, NAT_1:12;
then A13:
((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . (intloc 0) = 1
by A3, Th8;
A14:
((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . d <> 0
by A5, A11, A12;
while=0 (
d,
(Macro (d := d)))
is_halting_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1),
p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))
by A14, SCMFSA_9:18;
then A15:
while=0 (
d,
(Macro (d := d)))
is_halting_on Initialized ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)),
p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))
by A13, SCMFSA8B:42;
Macro (SubFrom (d,(intloc 0))) is_halting_on IExec (
(while=0 (d,(Macro (d := d)))),
(p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))),
((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1))),
p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))
by SCMFSA7B:19;
then
(while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))) is_halting_on Initialized ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)),
p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))
by A15, SFMASTR1:3;
hence
(while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))) is_halting_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1),
p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))
by A13, SCMFSA8B:42;
((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . (intloc 0) = 1thus
((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . (intloc 0) = 1
by A3, A12, Th8;
verum
end;
A16:
k < k + 1
by NAT_1:13;
assume A17:
k + 1
<= s . d
;
( (((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . d) + (k + 1) = s . d & ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . (1 -stRWNotIn ({d} \/ (UsedILoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) = ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . d )
hence
(((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . d) + (k + 1) = s . d
by A5, A16, XXREAL_0:2;
((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . (1 -stRWNotIn ({d} \/ (UsedILoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) = ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . d
((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . (1 -stRWNotIn ({d} \/ (UsedILoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) = (((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k) . d) - 1
by A3, A4, A5, A17, A16, Th8, XXREAL_0:2;
hence
((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . (1 -stRWNotIn ({d} \/ (UsedILoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) = ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . d
by A4, A5, A17, A16, XXREAL_0:2;
verum
end;
A18:
S1[ 0 ]
proof
hereby ( 0 <= s . d implies ( (((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0) . d) + 0 = s . d & ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0) . (1 -stRWNotIn ({d} \/ (UsedILoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) = ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0) . d ) )
assume
0 < s . d
;
( (while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))) is_halting_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0,p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) & ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0) . (intloc 0) = 1 )then A19:
((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0) . d <> 0
by Th9;
A20:
((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0) . (intloc 0) = 1
by Th6;
while=0 (
d,
(Macro (d := d)))
is_halting_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0,
p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))
by A19, SCMFSA_9:18;
then A21:
while=0 (
d,
(Macro (d := d)))
is_halting_on Initialized ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0),
p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))
by A20, SCMFSA8B:42;
Macro (SubFrom (d,(intloc 0))) is_halting_on IExec (
(while=0 (d,(Macro (d := d)))),
(p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))),
((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0)),
p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))
by SCMFSA7B:19;
then
(while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))) is_halting_on Initialized ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0),
p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))
by A21, SFMASTR1:3;
hence
(while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))) is_halting_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0,
p +* (times* (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))
by A20, SCMFSA8B:42;
((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0) . (intloc 0) = 1thus
((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0) . (intloc 0) = 1
by Th6;
verum
end;
assume
0 <= s . d
;
( (((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0) . d) + 0 = s . d & ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0) . (1 -stRWNotIn ({d} \/ (UsedILoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) = ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0) . d )
thus
(((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0) . d) + 0 = s . d
by Th9;
((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0) . (1 -stRWNotIn ({d} \/ (UsedILoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) = ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0) . d
((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0) . d = s . d
by Th9;
hence
((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0) . (1 -stRWNotIn ({d} \/ (UsedILoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) = ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0) . d
by Th7;
verum
end;
A22:
for k being Nat holds S1[k]
from NAT_1:sch 2(A18, A2);
A23:
ProperTimesBody d,(while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))),s,p
by A22;
assume
0 <= s . d
; (IExec ((triv-times d),p,s)) . d = 0
then reconsider k = s . d as Element of NAT by INT_1:3;
A24:
(((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k) . d) + k = s . d
by A22;
DataPart (IExec ((times (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))),p,s)) = DataPart ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . k)
by A23, Th19;
hence
(IExec ((triv-times d),p,s)) . d = 0
by A24, SCMFSA_M:2; verum