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} \/ (UsedILoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))));
reconsider WH = while>0 ((1 -stRWNotIn ({d} \/ (UsedILoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))),(((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({d} \/ (UsedILoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))),(intloc 0))))) as MacroInstruction of SCM+FSA ;
set s1 = Exec (((1 -stRWNotIn ({d} \/ (UsedILoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) := d),(Initialized s));
A2: (Exec (((1 -stRWNotIn ({d} \/ (UsedILoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) := d),(Initialized s))) . (1 -stRWNotIn ({d} \/ (UsedILoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) = (Initialized s) . d by SCMFSA_2:63
.= s . d by SCMFSA_M:37 ;
d in {d} by TARSKI:def 1;
then d in {d} \/ (UsedILoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))) by XBOOLE_0:def 3;
then A3: 1 -stRWNotIn ({d} \/ (UsedILoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))))) <> d by SCMFSA_M:25;
(Exec (((1 -stRWNotIn ({d} \/ (UsedILoc ((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 SCMFSA_M:9 ;
then A4: DataPart (IExec (WH,p,(Exec (((1 -stRWNotIn ({d} \/ (UsedILoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) := d),(Initialized s))))) = DataPart (Exec (((1 -stRWNotIn ({d} \/ (UsedILoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) := d),(Initialized s))) by A1, A2, SCMFSA9A:35;
A5: Exec (((1 -stRWNotIn ({d} \/ (UsedILoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) := d),(Initialized s)) = IExec ((Macro ((1 -stRWNotIn ({d} \/ (UsedILoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) := d)),p,s) by SCMFSA6C:5;
then WH is_halting_on IExec ((Macro ((1 -stRWNotIn ({d} \/ (UsedILoc ((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 (WH,p,(Exec (((1 -stRWNotIn ({d} \/ (UsedILoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) := d),(Initialized s))))) . d by A5, SFMASTR1:14
.= (Exec (((1 -stRWNotIn ({d} \/ (UsedILoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))))) := d),(Initialized s))) . d by A4, SCMFSA_M:2
.= (Initialized s) . d by A3, SCMFSA_2:63
.= s . d by SCMFSA_M:37 ;
:: thesis: verum