let s be State of SCM+FSA; :: thesis: for d being read-write Int-Location st s . d <= 0 holds
(IExec ((triv-times d),s)) . d = s . d
let d be read-write Int-Location ; :: thesis: ( s . d <= 0 implies (IExec ((triv-times d),s)) . d = s . d )
set a = d;
assume A1: s . d <= 0 ; :: thesis: (IExec ((triv-times d),s)) . d = s . d
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 WH = while>0 ((1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))))))),(((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))))))),(intloc 0)))));
set s1 = Exec (((1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))))))) := d),(Initialized s));
A2: (Exec (((1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))))))) := d),(Initialized s))) . (1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))))))) = (Initialized s) . d by SCMFSA_2:89
.= s . d by SCMFSA6C:3 ;
d in {d} by TARSKI:def 1;
then d in {d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))))) by XBOOLE_0:def 3;
then A3: 1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))))) <> d by SFMASTR1:21;
(Exec (((1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))))))) := d),(Initialized s))) . (intloc 0) = (Initialized s) . (intloc 0) by SCMFSA_2:89
.= 1 by SCMFSA6C:3 ;
then A4: DataPart (IExec ((while>0 ((1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))))))),(((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))))))),(intloc 0)))))),(Exec (((1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))))))) := d),(Initialized s))))) = DataPart (Exec (((1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))))))) := d),(Initialized s))) by A1, A2, SCMFSA9A:41;
A5: Exec (((1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))))))) := d),(Initialized s)) = IExec ((Macro ((1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))))))) := d)),s) by SCMFSA6C:6;
then ( while>0 ((1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))))))),(((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))))))),(intloc 0))))) is_closed_on IExec ((Macro ((1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))))))) := d)),s) & while>0 ((1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))))))),(((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))))))),(intloc 0))))) is_halting_on IExec ((Macro ((1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))))))) := d)),s) ) by A1, A2, SCMFSA_9:43;
hence (IExec ((triv-times d),s)) . d = (IExec ((while>0 ((1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))))))),(((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))))))),(intloc 0)))))),(Exec (((1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))))))) := d),(Initialized s))))) . d by A5, SFMASTR1:15
.= (Exec (((1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))))))) := d),(Initialized s))) . d by A4, SCMFSA6A:38
.= (Initialized s) . d by A3, SCMFSA_2:89
.= s . d by SCMFSA6C:3 ;
:: thesis: verum