let s be State of SCM+FSA; :: thesis: 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; :: thesis: 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; :: thesis: ( 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; :: thesis: ( 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 ) ) ; :: thesis: S1[k + 1]
A5: now :: thesis: ( 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 ; :: thesis: ( ((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; :: thesis: (((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; :: thesis: verum
end;
hereby :: thesis: ( 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 ; :: thesis: ( (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; :: thesis: ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . (intloc 0) = 1
thus ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . (intloc 0) = 1 by A3, A12, Th8; :: thesis: verum
end;
A16: k < k + 1 by NAT_1:13;
assume A17: k + 1 <= s . d ; :: thesis: ( (((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; :: thesis: ((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; :: thesis: verum
end;
A18: S1[ 0 ]
proof
hereby :: thesis: ( 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 ; :: thesis: ( (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; :: thesis: ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0) . (intloc 0) = 1
thus ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))),p,s)) . 0) . (intloc 0) = 1 by Th6; :: thesis: verum
end;
assume 0 <= s . d ; :: thesis: ( (((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; :: thesis: ((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; :: thesis: 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 ; :: thesis: (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; :: thesis: verum