let s be State of SCM+FSA; :: thesis: for a being read-write Int-Location
for bb, cc being Int-Location
for p being Instruction-Sequence of SCM+FSA
for I being really-closed MacroInstruction of SCM+FSA st s . (intloc 0) = 1 & s . bb > s . cc holds
( ( for x being Int-Location st x <> a & x in {bb,cc} \/ (UsedILoc I) holds
(IExec ((for-up (a,bb,cc,I)),p,s)) . x = s . x ) & ( for f being FinSeq-Location holds (IExec ((for-up (a,bb,cc,I)),p,s)) . f = s . f ) )
let a be read-write Int-Location; :: thesis: for bb, cc being Int-Location
for p being Instruction-Sequence of SCM+FSA
for I being really-closed MacroInstruction of SCM+FSA st s . (intloc 0) = 1 & s . bb > s . cc holds
( ( for x being Int-Location st x <> a & x in {bb,cc} \/ (UsedILoc I) holds
(IExec ((for-up (a,bb,cc,I)),p,s)) . x = s . x ) & ( for f being FinSeq-Location holds (IExec ((for-up (a,bb,cc,I)),p,s)) . f = s . f ) )
let bb, cc be Int-Location; :: thesis: for p being Instruction-Sequence of SCM+FSA
for I being really-closed MacroInstruction of SCM+FSA st s . (intloc 0) = 1 & s . bb > s . cc holds
( ( for x being Int-Location st x <> a & x in {bb,cc} \/ (UsedILoc I) holds
(IExec ((for-up (a,bb,cc,I)),p,s)) . x = s . x ) & ( for f being FinSeq-Location holds (IExec ((for-up (a,bb,cc,I)),p,s)) . f = s . f ) )
let p be Instruction-Sequence of SCM+FSA; :: thesis: for I being really-closed MacroInstruction of SCM+FSA st s . (intloc 0) = 1 & s . bb > s . cc holds
( ( for x being Int-Location st x <> a & x in {bb,cc} \/ (UsedILoc I) holds
(IExec ((for-up (a,bb,cc,I)),p,s)) . x = s . x ) & ( for f being FinSeq-Location holds (IExec ((for-up (a,bb,cc,I)),p,s)) . f = s . f ) )
let I be really-closed MacroInstruction of SCM+FSA ; :: thesis: ( s . (intloc 0) = 1 & s . bb > s . cc implies ( ( for x being Int-Location st x <> a & x in {bb,cc} \/ (UsedILoc I) holds
(IExec ((for-up (a,bb,cc,I)),p,s)) . x = s . x ) & ( for f being FinSeq-Location holds (IExec ((for-up (a,bb,cc,I)),p,s)) . f = s . f ) ) )
assume that
A1: s . (intloc 0) = 1 and
A2: s . bb > s . cc ; :: thesis: ( ( for x being Int-Location st x <> a & x in {bb,cc} \/ (UsedILoc I) holds
(IExec ((for-up (a,bb,cc,I)),p,s)) . x = s . x ) & ( for f being FinSeq-Location holds (IExec ((for-up (a,bb,cc,I)),p,s)) . f = s . f ) )
( cc = intloc 0 or cc is read-write ) by SCMFSA_M:def 2;
then A3: (Initialized s) . cc = s . cc by A1, SCMFSA_M:9, SCMFSA_M:37;
set MI = for-up (a,bb,cc,I);
set i3 = a := bb;
set aux = 1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I));
set i0 = (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))) := cc;
set i1 = SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),bb);
set i2 = AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),(intloc 0));
set IB = (I ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),(intloc 0)));
set I4 = while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),((I ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),(intloc 0)))));
set I03 = ((((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))) := cc) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),bb))) ";" (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),(intloc 0)))) ";" (a := bb);
set s1 = IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))) := cc) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),bb))) ";" (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),(intloc 0)))) ";" (a := bb)),p,s);
set p1 = p;
set s2 = (s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb));
A4: (IExec ((((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))) := cc) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),bb))),p,s)) . (intloc 0) = (Exec ((SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),bb)),(Exec (((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))) := cc),(Initialized s))))) . (intloc 0) by SCMFSA6C:8
.= (Exec (((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))) := cc),(Initialized s))) . (intloc 0) by SCMFSA_2:65
.= (Initialized s) . (intloc 0) by SCMFSA_2:63
.= 1 by SCMFSA_M:9 ;
( bb = intloc 0 or bb is read-write ) by SCMFSA_M:def 2;
then A5: (Initialized s) . bb = s . bb by A1, SCMFSA_M:9, SCMFSA_M:37;
A6: (IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))) := cc) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),bb))) ";" (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),(intloc 0)))) ";" (a := bb)),p,s)) . (intloc 0) = (Exec ((a := bb),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))) := cc) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),bb))) ";" (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),(intloc 0)))),p,s)))) . (intloc 0) by SCMFSA6C:6
.= (IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))) := cc) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),bb))) ";" (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),(intloc 0)))),p,s)) . (intloc 0) by SCMFSA_2:63
.= (Exec ((AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),(intloc 0))),(IExec ((((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))) := cc) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),bb))),p,s)))) . (intloc 0) by SCMFSA6C:6
.= 1 by A4, SCMFSA_2:64 ;
(s . bb) - (s . bb) > (s . cc) - (s . bb) by A2, XREAL_1:9;
then (s . cc) - (s . bb) <= - 1 by INT_1:8;
then A7: ((s . cc) - (s . bb)) + 1 <= (- 1) + 1 by XREAL_1:6;
set s3 = IExec ((for-up (a,bb,cc,I)),p,s);
a in {a,bb,cc} by ENUMSET1:def 1;
then a in {a,bb,cc} \/ (UsedILoc I) by XBOOLE_0:def 3;
then A8: a <> 1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I)) by SCMFSA_M:25;
bb in {a,bb,cc} by ENUMSET1:def 1;
then bb in {a,bb,cc} \/ (UsedILoc I) by XBOOLE_0:def 3;
then A9: bb <> 1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I)) by SCMFSA_M:25;
A10: (IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))) := cc) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),bb))) ";" (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),(intloc 0)))) ";" (a := bb)),p,s)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))) = (Exec ((a := bb),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))) := cc) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),bb))) ";" (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),(intloc 0)))),p,s)))) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))) by SCMFSA6C:6
.= (IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))) := cc) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),bb))) ";" (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),(intloc 0)))),p,s)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))) by A8, SCMFSA_2:63
.= (Exec ((AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),(intloc 0))),(IExec ((((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))) := cc) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),bb))),p,s)))) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))) by SCMFSA6C:6
.= ((IExec ((((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))) := cc) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),bb))),p,s)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I)))) + 1 by A4, SCMFSA_2:64
.= ((Exec ((SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),bb)),(Exec (((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))) := cc),(Initialized s))))) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I)))) + 1 by SCMFSA6C:8
.= (((Exec (((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))) := cc),(Initialized s))) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I)))) - ((Exec (((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))) := cc),(Initialized s))) . bb)) + 1 by SCMFSA_2:65
.= (((Initialized s) . cc) - ((Exec (((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))) := cc),(Initialized s))) . bb)) + 1 by SCMFSA_2:63
.= ((s . cc) - (s . bb)) + 1 by A9, A3, A5, SCMFSA_2:63 ;
then while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),((I ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),(intloc 0))))) is_halting_on IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))) := cc) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),bb))) ";" (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),(intloc 0)))) ";" (a := bb)),p,s),p by A7, SCMFSA_9:38;
then A11: DataPart (IExec ((for-up (a,bb,cc,I)),p,s)) = DataPart (IExec ((while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),((I ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),(intloc 0)))))),p,(IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))) := cc) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),bb))) ";" (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),(intloc 0)))) ";" (a := bb)),p,s)))) by SFMASTR1:9
.= DataPart (IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))) := cc) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),bb))) ";" (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),(intloc 0)))) ";" (a := bb)),p,s)) by A10, A7, A6, SCMFSA9A:35
.= DataPart ((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))) by A1, Th14 ;

hereby :: thesis: for f being FinSeq-Location holds (IExec ((for-up (a,bb,cc,I)),p,s)) . f = s . f

let x be Int-Location; :: thesis: ( x <> a & x in {bb,cc} \/ (UsedILoc I) implies (IExec ((for-up (a,bb,cc,I)),p,s)) . x = s . x )
assume that
A12: x <> a and
A13: x in {bb,cc} \/ (UsedILoc I) ; :: thesis: (IExec ((for-up (a,bb,cc,I)),p,s)) . x = s . x
x in {a,bb,cc} \/ (UsedILoc I)

proof

per cases ( x in {bb,cc} or x in UsedILoc I ) by A13, XBOOLE_0:def 3;

suppose x in {bb,cc} ; :: thesis: x in {a,bb,cc} \/ (UsedILoc I)

then ( x = bb or x = cc ) by TARSKI:def 2;
then x in {a,bb,cc} by ENUMSET1:def 1;
hence x in {a,bb,cc} \/ (UsedILoc I) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose x in UsedILoc I ; :: thesis: x in {a,bb,cc} \/ (UsedILoc I)

hence x in {a,bb,cc} \/ (UsedILoc I) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

then A14: x <> 1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I)) by SCMFSA_M:25;
thus (IExec ((for-up (a,bb,cc,I)),p,s)) . x = ((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))) . x by A11, SCMFSA_M:2
.= (s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),(((s . cc) - (s . bb)) + 1))) . x by A12, FUNCT_7:32
.= s . x by A14, FUNCT_7:32 ; :: thesis: verum

end;

let x be FinSeq-Location ; :: thesis: (IExec ((for-up (a,bb,cc,I)),p,s)) . x = s . x
thus (IExec ((for-up (a,bb,cc,I)),p,s)) . x = ((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))) . x by A11, SCMFSA_M:2
.= (s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),(((s . cc) - (s . bb)) + 1))) . x by FUNCT_7:32, SCMFSA_2:58
.= s . x by FUNCT_7:32, SCMFSA_2:58 ; :: thesis: verum