let s be State of SCM+FSA; 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; 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; ( s . d <= 0 implies (IExec ((triv-times d),p,s)) . d = s . d )
set a = d;
assume A1:
s . d <= 0
; (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
;
verum