let s be State of SCM+FSA; for a being read-write Int-Location
for bb, cc being Int-Location
for I being MacroInstruction of SCM+FSA
for p being Instruction-Sequence of SCM+FSA st s . (intloc 0) = 1 holds
for aux being read-write Int-Location st aux = 1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I)) holds
DataPart (IExec (((((aux := cc) ";" (SubFrom (aux,bb))) ";" (AddTo (aux,(intloc 0)))) ";" (a := bb)),p,s)) = DataPart ((s +* (aux,(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb)))
let a be read-write Int-Location; for bb, cc being Int-Location
for I being MacroInstruction of SCM+FSA
for p being Instruction-Sequence of SCM+FSA st s . (intloc 0) = 1 holds
for aux being read-write Int-Location st aux = 1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I)) holds
DataPart (IExec (((((aux := cc) ";" (SubFrom (aux,bb))) ";" (AddTo (aux,(intloc 0)))) ";" (a := bb)),p,s)) = DataPart ((s +* (aux,(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb)))
let bb, cc be Int-Location; for I being MacroInstruction of SCM+FSA
for p being Instruction-Sequence of SCM+FSA st s . (intloc 0) = 1 holds
for aux being read-write Int-Location st aux = 1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I)) holds
DataPart (IExec (((((aux := cc) ";" (SubFrom (aux,bb))) ";" (AddTo (aux,(intloc 0)))) ";" (a := bb)),p,s)) = DataPart ((s +* (aux,(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb)))
let I be MacroInstruction of SCM+FSA ; for p being Instruction-Sequence of SCM+FSA st s . (intloc 0) = 1 holds
for aux being read-write Int-Location st aux = 1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I)) holds
DataPart (IExec (((((aux := cc) ";" (SubFrom (aux,bb))) ";" (AddTo (aux,(intloc 0)))) ";" (a := bb)),p,s)) = DataPart ((s +* (aux,(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb)))
let p be Instruction-Sequence of SCM+FSA; ( s . (intloc 0) = 1 implies for aux being read-write Int-Location st aux = 1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I)) holds
DataPart (IExec (((((aux := cc) ";" (SubFrom (aux,bb))) ";" (AddTo (aux,(intloc 0)))) ";" (a := bb)),p,s)) = DataPart ((s +* (aux,(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))) )
assume A1:
s . (intloc 0) = 1
; for aux being read-write Int-Location st aux = 1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I)) holds
DataPart (IExec (((((aux := cc) ";" (SubFrom (aux,bb))) ";" (AddTo (aux,(intloc 0)))) ";" (a := bb)),p,s)) = DataPart ((s +* (aux,(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb)))
( cc = intloc 0 or cc is read-write )
by SCMFSA_M:def 2;
then A2:
(Initialized s) . cc = s . cc
by A1, SCMFSA_M:9, SCMFSA_M:37;
set i3 = a := bb;
let aux be read-write Int-Location; ( aux = 1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I)) implies DataPart (IExec (((((aux := cc) ";" (SubFrom (aux,bb))) ";" (AddTo (aux,(intloc 0)))) ";" (a := bb)),p,s)) = DataPart ((s +* (aux,(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))) )
assume A3:
aux = 1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))
; DataPart (IExec (((((aux := cc) ";" (SubFrom (aux,bb))) ";" (AddTo (aux,(intloc 0)))) ";" (a := bb)),p,s)) = DataPart ((s +* (aux,(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb)))
bb in {a,bb,cc}
by ENUMSET1:def 1;
then
bb in {a,bb,cc} \/ (UsedILoc I)
by XBOOLE_0:def 3;
then A4:
bb <> aux
by A3, SCMFSA_M:25;
set s2 = (s +* (aux,(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb));
A5:
aux in dom s
by SCMFSA_2:42;
a in {a,bb,cc}
by ENUMSET1:def 1;
then
a in {a,bb,cc} \/ (UsedILoc I)
by XBOOLE_0:def 3;
then A6:
a <> aux
by A3, SCMFSA_M:25;
then A7: ((s +* (aux,(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))) . aux =
(s +* (aux,(((s . cc) - (s . bb)) + 1))) . aux
by FUNCT_7:32
.=
((s . cc) - (s . bb)) + 1
by A5, FUNCT_7:31
;
set i2 = AddTo (aux,(intloc 0));
set i1 = SubFrom (aux,bb);
set i0 = aux := cc;
set s1 = IExec (((((aux := cc) ";" (SubFrom (aux,bb))) ";" (AddTo (aux,(intloc 0)))) ";" (a := bb)),p,s);
A8: (IExec (((aux := cc) ";" (SubFrom (aux,bb))),p,s)) . (intloc 0) =
(Exec ((SubFrom (aux,bb)),(Exec ((aux := cc),(Initialized s))))) . (intloc 0)
by SCMFSA6C:8
.=
(Exec ((aux := cc),(Initialized s))) . (intloc 0)
by SCMFSA_2:65
.=
(Initialized s) . (intloc 0)
by SCMFSA_2:63
.=
1
by SCMFSA_M:9
;
A9:
a in dom (s +* (aux,(((s . cc) - (s . bb)) + 1)))
by SCMFSA_2:42;
( bb = intloc 0 or bb is read-write )
by SCMFSA_M:def 2;
then A10:
(Initialized s) . bb = s . bb
by A1, SCMFSA_M:9, SCMFSA_M:37;
A11: (IExec (((((aux := cc) ";" (SubFrom (aux,bb))) ";" (AddTo (aux,(intloc 0)))) ";" (a := bb)),p,s)) . a =
(Exec ((a := bb),(IExec ((((aux := cc) ";" (SubFrom (aux,bb))) ";" (AddTo (aux,(intloc 0)))),p,s)))) . a
by SCMFSA6C:6
.=
(IExec ((((aux := cc) ";" (SubFrom (aux,bb))) ";" (AddTo (aux,(intloc 0)))),p,s)) . bb
by SCMFSA_2:63
.=
(Exec ((AddTo (aux,(intloc 0))),(IExec (((aux := cc) ";" (SubFrom (aux,bb))),p,s)))) . bb
by SCMFSA6C:6
.=
(IExec (((aux := cc) ";" (SubFrom (aux,bb))),p,s)) . bb
by A4, SCMFSA_2:64
.=
(Exec ((SubFrom (aux,bb)),(Exec ((aux := cc),(Initialized s))))) . bb
by SCMFSA6C:8
.=
(Exec ((aux := cc),(Initialized s))) . bb
by A4, SCMFSA_2:65
.=
s . bb
by A4, A10, SCMFSA_2:63
;
A12: (IExec (((((aux := cc) ";" (SubFrom (aux,bb))) ";" (AddTo (aux,(intloc 0)))) ";" (a := bb)),p,s)) . aux =
(Exec ((a := bb),(IExec ((((aux := cc) ";" (SubFrom (aux,bb))) ";" (AddTo (aux,(intloc 0)))),p,s)))) . aux
by SCMFSA6C:6
.=
(IExec ((((aux := cc) ";" (SubFrom (aux,bb))) ";" (AddTo (aux,(intloc 0)))),p,s)) . aux
by A6, SCMFSA_2:63
.=
(Exec ((AddTo (aux,(intloc 0))),(IExec (((aux := cc) ";" (SubFrom (aux,bb))),p,s)))) . aux
by SCMFSA6C:6
.=
((IExec (((aux := cc) ";" (SubFrom (aux,bb))),p,s)) . aux) + 1
by A8, SCMFSA_2:64
.=
((Exec ((SubFrom (aux,bb)),(Exec ((aux := cc),(Initialized s))))) . aux) + 1
by SCMFSA6C:8
.=
(((Exec ((aux := cc),(Initialized s))) . aux) - ((Exec ((aux := cc),(Initialized s))) . bb)) + 1
by SCMFSA_2:65
.=
(((Initialized s) . cc) - ((Exec ((aux := cc),(Initialized s))) . bb)) + 1
by SCMFSA_2:63
.=
((s . cc) - (s . bb)) + 1
by A4, A2, A10, SCMFSA_2:63
;
now ( ( for x being Int-Location holds (IExec (((((aux := cc) ";" (SubFrom (aux,bb))) ";" (AddTo (aux,(intloc 0)))) ";" (a := bb)),p,s)) . x = ((s +* (aux,(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))) . x ) & ( for x being FinSeq-Location holds (IExec (((((aux := cc) ";" (SubFrom (aux,bb))) ";" (AddTo (aux,(intloc 0)))) ";" (a := bb)),p,s)) . x = ((s +* (aux,(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))) . x ) )hereby for x being FinSeq-Location holds (IExec (((((aux := cc) ";" (SubFrom (aux,bb))) ";" (AddTo (aux,(intloc 0)))) ";" (a := bb)),p,s)) . x = ((s +* (aux,(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))) . x
let x be
Int-Location;
(IExec (((((aux := cc) ";" (SubFrom (aux,bb))) ";" (AddTo (aux,(intloc 0)))) ";" (a := bb)),p,s)) . b1 = ((s +* (aux,(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))) . b1per cases
( x = a or x = aux or ( x <> aux & x <> a ) )
;
suppose A13:
(
x <> aux &
x <> a )
;
(IExec (((((aux := cc) ";" (SubFrom (aux,bb))) ";" (AddTo (aux,(intloc 0)))) ";" (a := bb)),p,s)) . b1 = ((s +* (aux,(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))) . b1then A14:
((s +* (aux,(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))) . x =
(s +* (aux,(((s . cc) - (s . bb)) + 1))) . x
by FUNCT_7:32
.=
s . x
by A13, FUNCT_7:32
;
A15:
(
x = intloc 0 or
x is
read-write )
by SCMFSA_M:def 2;
(IExec (((((aux := cc) ";" (SubFrom (aux,bb))) ";" (AddTo (aux,(intloc 0)))) ";" (a := bb)),p,s)) . x =
(Exec ((a := bb),(IExec ((((aux := cc) ";" (SubFrom (aux,bb))) ";" (AddTo (aux,(intloc 0)))),p,s)))) . x
by SCMFSA6C:6
.=
(IExec ((((aux := cc) ";" (SubFrom (aux,bb))) ";" (AddTo (aux,(intloc 0)))),p,s)) . x
by A13, SCMFSA_2:63
.=
(Exec ((AddTo (aux,(intloc 0))),(IExec (((aux := cc) ";" (SubFrom (aux,bb))),p,s)))) . x
by SCMFSA6C:6
.=
(IExec (((aux := cc) ";" (SubFrom (aux,bb))),p,s)) . x
by A13, SCMFSA_2:64
.=
(Exec ((SubFrom (aux,bb)),(Exec ((aux := cc),(Initialized s))))) . x
by SCMFSA6C:8
.=
(Exec ((aux := cc),(Initialized s))) . x
by A13, SCMFSA_2:65
.=
(Initialized s) . x
by A13, SCMFSA_2:63
.=
s . x
by A1, A15, SCMFSA_M:9, SCMFSA_M:37
;
hence
(IExec (((((aux := cc) ";" (SubFrom (aux,bb))) ";" (AddTo (aux,(intloc 0)))) ";" (a := bb)),p,s)) . x = ((s +* (aux,(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))) . x
by A14;
verum end;
end; let x be
FinSeq-Location ;
(IExec (((((aux := cc) ";" (SubFrom (aux,bb))) ";" (AddTo (aux,(intloc 0)))) ";" (a := bb)),p,s)) . x = ((s +* (aux,(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))) . xthus (IExec (((((aux := cc) ";" (SubFrom (aux,bb))) ";" (AddTo (aux,(intloc 0)))) ";" (a := bb)),p,s)) . x =
(Exec ((a := bb),(IExec ((((aux := cc) ";" (SubFrom (aux,bb))) ";" (AddTo (aux,(intloc 0)))),p,s)))) . x
by SCMFSA6C:7
.=
(IExec ((((aux := cc) ";" (SubFrom (aux,bb))) ";" (AddTo (aux,(intloc 0)))),p,s)) . x
by SCMFSA_2:63
.=
(Exec ((AddTo (aux,(intloc 0))),(IExec (((aux := cc) ";" (SubFrom (aux,bb))),p,s)))) . x
by SCMFSA6C:7
.=
(IExec (((aux := cc) ";" (SubFrom (aux,bb))),p,s)) . x
by SCMFSA_2:64
.=
(Exec ((SubFrom (aux,bb)),(Exec ((aux := cc),(Initialized s))))) . x
by SCMFSA6C:9
.=
(Exec ((aux := cc),(Initialized s))) . x
by SCMFSA_2:65
.=
(Initialized s) . x
by SCMFSA_2:63
.=
s . x
by SCMFSA_M:37
.=
(s +* (aux,(((s . cc) - (s . bb)) + 1))) . x
by FUNCT_7:32, SCMFSA_2:58
.=
((s +* (aux,(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))) . x
by FUNCT_7:32, SCMFSA_2:58
;
verum
hence
DataPart (IExec (((((aux := cc) ";" (SubFrom (aux,bb))) ";" (AddTo (aux,(intloc 0)))) ";" (a := bb)),p,s)) = DataPart ((s +* (aux,(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb)))
by SCMFSA_M:2; verum