let s be State of SCM+FSA; :: thesis: for d being read-write Int-Location st 0 <= s . d holds
(IExec ((triv-times d),s)) . d = 0
let d be read-write Int-Location ; :: thesis: ( 0 <= s . d implies (IExec ((triv-times d),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} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))))));
set ST = StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s);
defpred S₁[ Nat] means ( ( $1 < s . d implies ( (while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))) is_closed_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . $1 & (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)))),s)) . $1 & ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . $1) . (intloc 0) = 1 ) ) & ( $1 <= s . d implies ( (((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . $1) . d) + $1 = s . d & ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . $1) . (1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))))))) = ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . $1) . d ) ) );
d in {d,(intloc 0)} by TARSKI:def 2;
then d in UsedIntLoc (SubFrom (d,(intloc 0))) by SF_MASTR:18;
then d in (UsedIntLoc (while=0 (d,(Macro (d := d))))) \/ (UsedIntLoc (SubFrom (d,(intloc 0)))) by XBOOLE_0:def 3;
then A1: d in UsedIntLoc ((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))) by SF_MASTR:34;
A2: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume that
A3: ( k < s . d implies ( (while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))) is_closed_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . k & (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)))),s)) . k & ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . k) . (intloc 0) = 1 ) ) and
A4: ( k <= s . d implies ( (((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . k) . d) + k = s . d & ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . k) . (1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))))))) = ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . k) . d ) ) ; :: thesis: S₁[k + 1]

A5: now

assume A6: k < s . d ; :: thesis: ( ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . k) . (1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))))))) > 0 & (((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . (k + 1)) . d) + (k + 1) = s . d )
then A7: ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . k) . d <> 0 by A4;
then A8: DataPart (IExec ((while=0 (d,(Macro (d := d)))),((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . k))) = DataPart ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . k) by A3, A6, SCMFSA9A:28;
A9: while=0 (d,(Macro (d := d))) is_closed_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . k by A7, SCMFSA_9:18;
then A10: while=0 (d,(Macro (d := d))) is_closed_on Initialized ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . k) by A3, A6, Th4;
while=0 (d,(Macro (d := d))) is_halting_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . k by A7, SCMFSA_9:18;
then A11: while=0 (d,(Macro (d := d))) is_halting_on Initialized ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . k) by A3, A6, A9, Th5;
A12: k - k < (s . d) - k by A6, XREAL_1:11;
hence ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . k) . (1 -stRWNotIn ({d} \/ (UsedIntLoc ((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)))),s)) . (k + 1)) . d) + (k + 1) = s . d
( (while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))) is_closed_on Initialized ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . k) & (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)))),s)) . k) ) by A3, A6, Th5;
then ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . (k + 1)) | ((UsedIntLoc ((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))))) \/ FinSeq-Locations) = (IExec (((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . k))) | ((UsedIntLoc ((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))))) \/ FinSeq-Locations) by A3, A4, A6, A12, Th20;
then ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . (k + 1)) . d = (IExec (((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . k))) . d by A1, Th7
.= (Exec ((SubFrom (d,(intloc 0))),(IExec ((while=0 (d,(Macro (d := d)))),((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . k))))) . d by A10, A11, SFMASTR1:12
.= ((IExec ((while=0 (d,(Macro (d := d)))),((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . k))) . d) - ((IExec ((while=0 (d,(Macro (d := d)))),((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . k))) . (intloc 0)) by SCMFSA_2:91
.= (((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . k) . d) - ((IExec ((while=0 (d,(Macro (d := d)))),((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . k))) . (intloc 0)) by A8, SCMFSA6A:38
.= (((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . k) . d) - 1 by A3, A6, A8, SCMFSA6A:38 ;
hence (((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),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)))),s)) . (k + 1)) . d) + (k + 1) = s . d & ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . (k + 1)) . (1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))))))) = ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . (k + 1)) . d ) )

assume A13: k + 1 < s . d ; :: thesis: ( (while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))) is_closed_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . (k + 1) & (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)))),s)) . (k + 1) & ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . (k + 1)) . (intloc 0) = 1 )
then reconsider sa = s . d as Element of NAT by INT_1:16;
A14: k < sa by A13, NAT_1:12;
then A15: ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . (k + 1)) . (intloc 0) = 1 by A3, Th12;
A16: ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . (k + 1)) . d <> 0 by A5, A13, A14;
then A17: while=0 (d,(Macro (d := d))) is_closed_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . (k + 1) by SCMFSA_9:18;
A18: Macro (SubFrom (d,(intloc 0))) is_closed_on IExec ((while=0 (d,(Macro (d := d)))),((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . (k + 1))) by SCMFSA7B:24;
while=0 (d,(Macro (d := d))) is_halting_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . (k + 1) by A16, SCMFSA_9:18;
then A19: while=0 (d,(Macro (d := d))) is_halting_on Initialized ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . (k + 1)) by A15, A17, Th5;
A20: while=0 (d,(Macro (d := d))) is_closed_on Initialized ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . (k + 1)) by A15, A17, Th4;
then A21: (while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))) is_closed_on Initialized ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . (k + 1)) by A19, A18, SFMASTR1:3;
hence (while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))) is_closed_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . (k + 1) by A15, Th4; :: 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)))),s)) . (k + 1) & ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . (k + 1)) . (intloc 0) = 1 )
Macro (SubFrom (d,(intloc 0))) is_halting_on IExec ((while=0 (d,(Macro (d := d)))),((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . (k + 1))) by SCMFSA7B:25;
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)))),s)) . (k + 1)) by A19, A20, A18, SFMASTR1:4;
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)))),s)) . (k + 1) by A15, A21, Th5; :: thesis: ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . (k + 1)) . (intloc 0) = 1
thus ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . (k + 1)) . (intloc 0) = 1 by A3, A14, Th12; :: thesis: verum

end;

A22: k < k + 1 by NAT_1:13;
assume A23: k + 1 <= s . d ; :: thesis: ( (((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . (k + 1)) . d) + (k + 1) = s . d & ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . (k + 1)) . (1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))))))) = ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . (k + 1)) . d )
hence (((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . (k + 1)) . d) + (k + 1) = s . d by A5, A22, XXREAL_0:2; :: thesis: ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . (k + 1)) . (1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))))))) = ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . (k + 1)) . d
((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . (k + 1)) . (1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))))))) = (((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . k) . d) - 1 by A3, A4, A5, A23, A22, Th12, XXREAL_0:2;
hence ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . (k + 1)) . (1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))))))) = ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . (k + 1)) . d by A4, A5, A23, A22, XXREAL_0:2; :: thesis: verum

end;

A24: S₁[ 0 ]

proof

hereby :: thesis: ( 0 <= s . d implies ( (((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . 0) . d) + 0 = s . d & ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . 0) . (1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))))))) = ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . 0) . d ) )

assume 0 < s . d ; :: thesis: ( (while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))) is_closed_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . 0 & (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)))),s)) . 0 & ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . 0) . (intloc 0) = 1 )
then A25: ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . 0) . d <> 0 by Th13;
then A26: while=0 (d,(Macro (d := d))) is_closed_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . 0 by SCMFSA_9:18;
A27: Macro (SubFrom (d,(intloc 0))) is_closed_on IExec ((while=0 (d,(Macro (d := d)))),((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . 0)) by SCMFSA7B:24;
A28: ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . 0) . (intloc 0) = 1 by Th10;
while=0 (d,(Macro (d := d))) is_halting_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . 0 by A25, SCMFSA_9:18;
then A29: while=0 (d,(Macro (d := d))) is_halting_on Initialized ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . 0) by A28, A26, Th5;
A30: while=0 (d,(Macro (d := d))) is_closed_on Initialized ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . 0) by A28, A26, Th4;
then A31: (while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))) is_closed_on Initialized ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . 0) by A29, A27, SFMASTR1:3;
hence (while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))) is_closed_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . 0 by A28, Th4; :: 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)))),s)) . 0 & ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . 0) . (intloc 0) = 1 )
Macro (SubFrom (d,(intloc 0))) is_halting_on IExec ((while=0 (d,(Macro (d := d)))),((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . 0)) by SCMFSA7B:25;
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)))),s)) . 0) by A29, A30, A27, SFMASTR1:4;
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)))),s)) . 0 by A28, A31, Th5; :: thesis: ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . 0) . (intloc 0) = 1
thus ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . 0) . (intloc 0) = 1 by Th10; :: thesis: verum

end;

assume 0 <= s . d ; :: thesis: ( (((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . 0) . d) + 0 = s . d & ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . 0) . (1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))))))) = ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . 0) . d )
thus (((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . 0) . d) + 0 = s . d by Th13; :: thesis: ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . 0) . (1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))))))) = ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . 0) . d
((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . 0) . d = s . d by Th13;
hence ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . 0) . (1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))))))) = ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . 0) . d by Th11; :: thesis: verum

end;

A32: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A24, A2);
A33: ProperTimesBody d,(while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))),s

proof

let k be Element of NAT ; :: according to SFMASTR2:def 3 :: thesis: ( k < s . d implies ( (while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))) is_closed_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . k & (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)))),s)) . k ) )
thus ( k < s . d implies ( (while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))) is_closed_on (StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . k & (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)))),s)) . k ) ) by A32; :: thesis: verum

end;

assume 0 <= s . d ; :: thesis: (IExec ((triv-times d),s)) . d = 0
then reconsider k = s . d as Element of NAT by INT_1:16;
A34: (((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . k) . d) + k = s . d by A32;
DataPart (IExec ((times (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))))),s)) = DataPart ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),s)) . k) by A33, Th23;
hence (IExec ((triv-times d),s)) . d = 0 by A34, SCMFSA6A:38; :: thesis: verum