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