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} \/ (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)))),p,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)))),p,s)) . $1,p +* (times* (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 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)))),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} \/ (UsedIntLoc ((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 (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:30;
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)))),p,s)) . k,p +* (times* (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 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)))),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} \/ (UsedIntLoc ((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: S₁[k + 1]

A5: now

assume A6: k < s . d ; :: thesis: ( ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),p,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)))),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;
A9: while=0 (d,(Macro (d := d))) is_closed_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 A10: while=0 (d,(Macro (d := d))) is_closed_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, Th4;
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 A11: 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, A9, Th5;
A12: 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} \/ (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)))),p,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)))),p,s)) . k),p +* (times* (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))))) & (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, Th5;
then ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),p,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)))),(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))) | ((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)))),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, Th7
.= (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 A10, A11, 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, SCMFSA6A:7
.= (((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),p,s)) . k) . d) - 1 by A3, A6, A8, SCMFSA6A:7 ;
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} \/ (UsedIntLoc ((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 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)))),p,s)) . (k + 1),p +* (times* (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 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)))),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;
A14: k < sa by A13, NAT_1:12;
then A15: ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),p,s)) . (k + 1)) . (intloc 0) = 1 by A3, Th12;
A16: ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),p,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)))),p,s)) . (k + 1),p +* (times* (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))))) by SCMFSA_9:18;
A18: Macro (SubFrom (d,(intloc 0))) is_closed_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:18;
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 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)))),p,s)) . (k + 1)),p +* (times* (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))))) 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)))),p,s)) . (k + 1)),p +* (times* (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))))) 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)))),p,s)) . (k + 1)),p +* (times* (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))))) by A19, A18, SFMASTR1:2;
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)))),p,s)) . (k + 1),p +* (times* (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))))) 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)))),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 )
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 A19, A20, A18, 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 A15, A21, Th5; :: 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, 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)))),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} \/ (UsedIntLoc ((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, A22, XXREAL_0:2; :: thesis: ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),p,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)))),p,s)) . (k + 1)) . d
((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),p,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)))),p,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)))),p,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)))),p,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)))),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} \/ (UsedIntLoc ((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_closed_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)))))) & (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 A25: ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),p,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)))),p,s)) . 0,p +* (times* (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))))) by SCMFSA_9:18;
A27: Macro (SubFrom (d,(intloc 0))) is_closed_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:18;
A28: ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),p,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)))),p,s)) . 0,p +* (times* (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 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)))),p,s)) . 0),p +* (times* (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 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)))),p,s)) . 0),p +* (times* (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 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)))),p,s)) . 0),p +* (times* (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))))) by A29, A27, SFMASTR1:2;
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)))),p,s)) . 0,p +* (times* (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 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)))),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 )
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 A29, A30, A27, 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 A28, A31, Th5; :: 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 Th10; :: 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} \/ (UsedIntLoc ((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 Th13; :: thesis: ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),p,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)))),p,s)) . 0) . d
((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),p,s)) . 0) . d = s . d by Th13;
hence ((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),p,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)))),p,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,p

proof

let k be Element of NAT ; :: according to SFMASTR2:def 4 :: 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)))),p,s)) . k,p +* (times* (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 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)))),p,s)) . k,p +* (times* (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))))) ) )
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)))),p,s)) . k,p +* (times* (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 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)))),p,s)) . k,p +* (times* (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))))) ) ) by A32; :: thesis: verum

end;

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;
A34: (((StepTimes (d,((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))),p,s)) . k) . d) + k = s . d by A32;
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 A33, Th23;
hence (IExec ((triv-times d),p,s)) . d = 0 by A34, SCMFSA6A:7; :: thesis: verum