let s be State of SCM+FSA; :: thesis: for p being Instruction-Sequence of SCM+FSA
for d being read-write Int-Location st s . d <= 0 holds
(IExec ((triv-times d),p,s)) . d = s . d
let p be Instruction-Sequence of SCM+FSA; :: thesis: for d being read-write Int-Location st s . d <= 0 holds
(IExec ((triv-times d),p,s)) . d = s . d
let d be read-write Int-Location ; :: thesis: ( s . d <= 0 implies (IExec ((triv-times d),p,s)) . d = s . d )
set a = d;
assume A1: s . d <= 0 ; :: thesis: (IExec ((triv-times d),p,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:63
.= 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:20;
(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:63
.= 1 by SCMFSA6A:38 ;
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)))))),p,(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:35;
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)),p,s) by SCMFSA6C:5;
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)),p,s),p & 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)),p,s),p ) by A1, A2, SCMFSA_9:38;
hence (IExec ((triv-times d),p,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)))))),p,(Exec (((1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))))))) := d),(Initialized s))))) . d by A5, SFMASTR1:14
.= (Exec (((1 -stRWNotIn ({d} \/ (UsedIntLoc ((while=0 (d,(Macro (d := d)))) ';' (SubFrom (d,(intloc 0))))))) := d),(Initialized s))) . d by A4, SCMFSA6A:7
.= (Initialized s) . d by A3, SCMFSA_2:63
.= s . d by SCMFSA6C:3 ;
:: thesis: verum