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