let s be State of SCM+FSA ; :: thesis: for a being read-write Int-Location
for bb, cc being Int-Location
for I being Program of SCM+FSA 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 ; :: thesis: for bb, cc being Int-Location
for I being Program of SCM+FSA 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 ; :: thesis: for I being Program of SCM+FSA 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 SCM+FSA ; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: ( 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)) ; :: thesis: 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 :: thesis: 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 ; :: thesis: (IExec ((((aux := cc) ';' (SubFrom aux,bb)) ';' (AddTo aux,(intloc 0 ))) ';' (a := bb)),s) . b₁ = ((s +* aux,(((s . cc) - (s . bb)) + 1)) +* a,(s . bb)) . b₁

per cases ( x = a or x = aux or ( x <> aux & x <> a ) ) ;

suppose x = a ; :: thesis: (IExec ((((aux := cc) ';' (SubFrom aux,bb)) ';' (AddTo aux,(intloc 0 ))) ';' (a := bb)),s) . b₁ = ((s +* aux,(((s . cc) - (s . bb)) + 1)) +* a,(s . bb)) . b₁

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 A11, A9, FUNCT_7:33; :: thesis: verum

end;

suppose x = aux ; :: thesis: (IExec ((((aux := cc) ';' (SubFrom aux,bb)) ';' (AddTo aux,(intloc 0 ))) ';' (a := bb)),s) . b₁ = ((s +* aux,(((s . cc) - (s . bb)) + 1)) +* a,(s . bb)) . b₁

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 A12, A7; :: thesis: verum

end;

suppose A13: ( x <> aux & x <> a ) ; :: thesis: (IExec ((((aux := cc) ';' (SubFrom aux,bb)) ';' (AddTo aux,(intloc 0 ))) ';' (a := bb)),s) . b₁ = ((s +* aux,(((s . cc) - (s . bb)) + 1)) +* a,(s . bb)) . b₁

then 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; :: thesis: verum

end;

end;

end;

let x be FinSeq-Location ; :: thesis: (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
thus (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 ; :: thesis: verum

end;

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; :: thesis: verum