let s be State of SCM+FSA; :: thesis: 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; :: thesis: 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; :: thesis: 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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( 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)) ; :: thesis: 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 ;
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; :: thesis: verum