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 ((),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 ((),p,s)) . d = s . d

let d be read-write Int-Location; :: thesis: ( s . d <= 0 implies (IExec ((),p,s)) . d = s . d )
set a = d;
assume A1: s . d <= 0 ; :: thesis: (IExec ((),p,s)) . d = s . d
set I = (while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,()));
set au = 1 -stRWNotIn ({d} \/ (UsedILoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,())))));
reconsider WH = while>0 ((1 -stRWNotIn ({d} \/ (UsedILoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,())))))),(((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,()))) ";" (SubFrom ((1 -stRWNotIn ({d} \/ (UsedILoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,())))))),())))) as MacroInstruction of SCM+FSA ;
set s1 = Exec (((1 -stRWNotIn ({d} \/ (UsedILoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,())))))) := d),());
A2: (Exec (((1 -stRWNotIn ({d} \/ (UsedILoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,())))))) := d),())) . (1 -stRWNotIn ({d} \/ (UsedILoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,())))))) = () . 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,())))) by XBOOLE_0:def 3;
then A3: 1 -stRWNotIn ({d} \/ (UsedILoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,()))))) <> d by SCMFSA_M:25;
(Exec (((1 -stRWNotIn ({d} \/ (UsedILoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,())))))) := d),())) . () = () . () 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,())))))) := d),())))) = DataPart (Exec (((1 -stRWNotIn ({d} \/ (UsedILoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,())))))) := d),())) by ;
A5: Exec (((1 -stRWNotIn ({d} \/ (UsedILoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,())))))) := d),()) = IExec ((Macro ((1 -stRWNotIn ({d} \/ (UsedILoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,())))))) := 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,())))))) := d)),p,s),p by ;
hence (IExec ((),p,s)) . d = (IExec (WH,p,(Exec (((1 -stRWNotIn ({d} \/ (UsedILoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,())))))) := d),())))) . d by
.= (Exec (((1 -stRWNotIn ({d} \/ (UsedILoc ((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,())))))) := d),())) . d by
.= () . d by
.= s . d by SCMFSA_M:37 ;
:: thesis: verum