let s be State of SCM+FSA; for a being read-write Int-Location
for bb, cc being Int-Location
for I being Program of {INT,(INT *)} st s . (intloc 0) = 1 holds
for aux being read-write Int-Location st aux = 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)) holds
DataPart (IExec (((((aux := cc) ';' (SubFrom (aux,bb))) ';' (AddTo (aux,(intloc 0)))) ';' (a := bb)),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 Program of {INT,(INT *)} st s . (intloc 0) = 1 holds
for aux being read-write Int-Location st aux = 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)) holds
DataPart (IExec (((((aux := cc) ';' (SubFrom (aux,bb))) ';' (AddTo (aux,(intloc 0)))) ';' (a := bb)),s)) = DataPart ((s +* (aux,(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb)))
let bb, cc be Int-Location ; for I being Program of {INT,(INT *)} st s . (intloc 0) = 1 holds
for aux being read-write Int-Location st aux = 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)) holds
DataPart (IExec (((((aux := cc) ';' (SubFrom (aux,bb))) ';' (AddTo (aux,(intloc 0)))) ';' (a := bb)),s)) = DataPart ((s +* (aux,(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb)))
let I be Program of {INT,(INT *)}; ( s . (intloc 0) = 1 implies for aux being read-write Int-Location st aux = 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)) holds
DataPart (IExec (((((aux := cc) ';' (SubFrom (aux,bb))) ';' (AddTo (aux,(intloc 0)))) ';' (a := bb)),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} \/ (UsedIntLoc I)) holds
DataPart (IExec (((((aux := cc) ';' (SubFrom (aux,bb))) ';' (AddTo (aux,(intloc 0)))) ';' (a := bb)),s)) = DataPart ((s +* (aux,(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb)))
( cc = intloc 0 or not cc is read-only )
by SF_MASTR:def 5;
then A2:
(Initialized s) . cc = s . cc
by A1, SCMFSA6C:3;
set i3 = a := bb;
let aux be read-write Int-Location ; ( aux = 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)) implies DataPart (IExec (((((aux := cc) ';' (SubFrom (aux,bb))) ';' (AddTo (aux,(intloc 0)))) ';' (a := bb)),s)) = DataPart ((s +* (aux,(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))) )
assume A3:
aux = 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))
; DataPart (IExec (((((aux := cc) ';' (SubFrom (aux,bb))) ';' (AddTo (aux,(intloc 0)))) ';' (a := bb)),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} \/ (UsedIntLoc I)
by XBOOLE_0:def 3;
then A4:
bb <> aux
by A3, SFMASTR1:21;
set s2 = (s +* (aux,(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb));
A5:
aux in dom s
by SCMFSA_2:66;
a in {a,bb,cc}
by ENUMSET1:def 1;
then
a in {a,bb,cc} \/ (UsedIntLoc I)
by XBOOLE_0:def 3;
then A6:
a <> aux
by A3, SFMASTR1:21;
then A7: ((s +* (aux,(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))) . aux =
(s +* (aux,(((s . cc) - (s . bb)) + 1))) . aux
by FUNCT_7:34
.=
((s . cc) - (s . bb)) + 1
by A5, FUNCT_7:33
;
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)),s);
A8: (IExec (((aux := cc) ';' (SubFrom (aux,bb))),s)) . (intloc 0) =
(Exec ((SubFrom (aux,bb)),(Exec ((aux := cc),(Initialized s))))) . (intloc 0)
by SCMFSA6C:9
.=
(Exec ((aux := cc),(Initialized s))) . (intloc 0)
by SCMFSA_2:91
.=
(Initialized s) . (intloc 0)
by SCMFSA_2:89
.=
1
by SCMFSA6C:3
;
A9:
a in dom (s +* (aux,(((s . cc) - (s . bb)) + 1)))
by SCMFSA_2:66;
( bb = intloc 0 or not bb is read-only )
by SF_MASTR:def 5;
then A10:
(Initialized s) . bb = s . bb
by A1, SCMFSA6C:3;
A11: (IExec (((((aux := cc) ';' (SubFrom (aux,bb))) ';' (AddTo (aux,(intloc 0)))) ';' (a := bb)),s)) . a =
(Exec ((a := bb),(IExec ((((aux := cc) ';' (SubFrom (aux,bb))) ';' (AddTo (aux,(intloc 0)))),s)))) . a
by SCMFSA6C:7
.=
(IExec ((((aux := cc) ';' (SubFrom (aux,bb))) ';' (AddTo (aux,(intloc 0)))),s)) . bb
by SCMFSA_2:89
.=
(Exec ((AddTo (aux,(intloc 0))),(IExec (((aux := cc) ';' (SubFrom (aux,bb))),s)))) . bb
by SCMFSA6C:7
.=
(IExec (((aux := cc) ';' (SubFrom (aux,bb))),s)) . bb
by A4, SCMFSA_2:90
.=
(Exec ((SubFrom (aux,bb)),(Exec ((aux := cc),(Initialized s))))) . bb
by SCMFSA6C:9
.=
(Exec ((aux := cc),(Initialized s))) . bb
by A4, SCMFSA_2:91
.=
s . bb
by A4, A10, SCMFSA_2:89
;
A12: (IExec (((((aux := cc) ';' (SubFrom (aux,bb))) ';' (AddTo (aux,(intloc 0)))) ';' (a := bb)),s)) . aux =
(Exec ((a := bb),(IExec ((((aux := cc) ';' (SubFrom (aux,bb))) ';' (AddTo (aux,(intloc 0)))),s)))) . aux
by SCMFSA6C:7
.=
(IExec ((((aux := cc) ';' (SubFrom (aux,bb))) ';' (AddTo (aux,(intloc 0)))),s)) . aux
by A6, SCMFSA_2:89
.=
(Exec ((AddTo (aux,(intloc 0))),(IExec (((aux := cc) ';' (SubFrom (aux,bb))),s)))) . aux
by SCMFSA6C:7
.=
((IExec (((aux := cc) ';' (SubFrom (aux,bb))),s)) . aux) + 1
by A8, SCMFSA_2:90
.=
((Exec ((SubFrom (aux,bb)),(Exec ((aux := cc),(Initialized s))))) . aux) + 1
by SCMFSA6C:9
.=
(((Exec ((aux := cc),(Initialized s))) . aux) - ((Exec ((aux := cc),(Initialized s))) . bb)) + 1
by SCMFSA_2:91
.=
(((Initialized s) . cc) - ((Exec ((aux := cc),(Initialized s))) . bb)) + 1
by SCMFSA_2:89
.=
((s . cc) - (s . bb)) + 1
by A4, A2, A10, SCMFSA_2:89
;
now hereby for x being FinSeq-Location holds (IExec (((((aux := cc) ';' (SubFrom (aux,bb))) ';' (AddTo (aux,(intloc 0)))) ';' (a := bb)),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)),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)),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:34
.=
s . x
by A13, FUNCT_7:34
;
A15:
(
x = intloc 0 or not
x is
read-only )
by SF_MASTR:def 5;
(IExec (((((aux := cc) ';' (SubFrom (aux,bb))) ';' (AddTo (aux,(intloc 0)))) ';' (a := bb)),s)) . x =
(Exec ((a := bb),(IExec ((((aux := cc) ';' (SubFrom (aux,bb))) ';' (AddTo (aux,(intloc 0)))),s)))) . x
by SCMFSA6C:7
.=
(IExec ((((aux := cc) ';' (SubFrom (aux,bb))) ';' (AddTo (aux,(intloc 0)))),s)) . x
by A13, SCMFSA_2:89
.=
(Exec ((AddTo (aux,(intloc 0))),(IExec (((aux := cc) ';' (SubFrom (aux,bb))),s)))) . x
by SCMFSA6C:7
.=
(IExec (((aux := cc) ';' (SubFrom (aux,bb))),s)) . x
by A13, SCMFSA_2:90
.=
(Exec ((SubFrom (aux,bb)),(Exec ((aux := cc),(Initialized s))))) . x
by SCMFSA6C:9
.=
(Exec ((aux := cc),(Initialized s))) . x
by A13, SCMFSA_2:91
.=
(Initialized s) . x
by A13, SCMFSA_2:89
.=
s . x
by A1, A15, SCMFSA6C:3
;
hence
(IExec (((((aux := cc) ';' (SubFrom (aux,bb))) ';' (AddTo (aux,(intloc 0)))) ';' (a := bb)),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)),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)),s)) . x =
(Exec ((a := bb),(IExec ((((aux := cc) ';' (SubFrom (aux,bb))) ';' (AddTo (aux,(intloc 0)))),s)))) . x
by SCMFSA6C:8
.=
(IExec ((((aux := cc) ';' (SubFrom (aux,bb))) ';' (AddTo (aux,(intloc 0)))),s)) . x
by SCMFSA_2:89
.=
(Exec ((AddTo (aux,(intloc 0))),(IExec (((aux := cc) ';' (SubFrom (aux,bb))),s)))) . x
by SCMFSA6C:8
.=
(IExec (((aux := cc) ';' (SubFrom (aux,bb))),s)) . x
by SCMFSA_2:90
.=
(Exec ((SubFrom (aux,bb)),(Exec ((aux := cc),(Initialized s))))) . x
by SCMFSA6C:10
.=
(Exec ((aux := cc),(Initialized s))) . x
by SCMFSA_2:91
.=
(Initialized s) . x
by SCMFSA_2:89
.=
s . x
by SCMFSA6C:3
.=
(s +* (aux,(((s . cc) - (s . bb)) + 1))) . x
by FUNCT_7:34, SCMFSA_2:83
.=
((s +* (aux,(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))) . x
by FUNCT_7:34, SCMFSA_2:83
;
verum
hence
DataPart (IExec (((((aux := cc) ';' (SubFrom (aux,bb))) ';' (AddTo (aux,(intloc 0)))) ';' (a := bb)),s)) = DataPart ((s +* (aux,(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb)))
by SCMFSA6A:38; verum