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 {INT,(INT *)} st s . (intloc 0) = 1 & s . bb > s . cc holds
( ( for x being Int-Location st x <> a & x in {bb,cc} \/ (UsedIntLoc I) holds
(IExec ((for-up (a,bb,cc,I)),s)) . x = s . x ) & ( for f being FinSeq-Location holds (IExec ((for-up (a,bb,cc,I)),s)) . f = s . f ) )
let a be read-write Int-Location ; :: thesis: for bb, cc being Int-Location
for I being Program of {INT,(INT *)} st s . (intloc 0) = 1 & s . bb > s . cc holds
( ( for x being Int-Location st x <> a & x in {bb,cc} \/ (UsedIntLoc I) holds
(IExec ((for-up (a,bb,cc,I)),s)) . x = s . x ) & ( for f being FinSeq-Location holds (IExec ((for-up (a,bb,cc,I)),s)) . f = s . f ) )
let bb, cc be Int-Location ; :: thesis: for I being Program of {INT,(INT *)} st s . (intloc 0) = 1 & s . bb > s . cc holds
( ( for x being Int-Location st x <> a & x in {bb,cc} \/ (UsedIntLoc I) holds
(IExec ((for-up (a,bb,cc,I)),s)) . x = s . x ) & ( for f being FinSeq-Location holds (IExec ((for-up (a,bb,cc,I)),s)) . f = s . f ) )
let I be Program of {INT,(INT *)}; :: thesis: ( s . (intloc 0) = 1 & s . bb > s . cc implies ( ( for x being Int-Location st x <> a & x in {bb,cc} \/ (UsedIntLoc I) holds
(IExec ((for-up (a,bb,cc,I)),s)) . x = s . x ) & ( for f being FinSeq-Location holds (IExec ((for-up (a,bb,cc,I)),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} \/ (UsedIntLoc I) holds
(IExec ((for-up (a,bb,cc,I)),s)) . x = s . x ) & ( for f being FinSeq-Location holds (IExec ((for-up (a,bb,cc,I)),s)) . f = s . f ) )
( cc = intloc 0 or not cc is read-only ) by SF_MASTR:def 5;
then A3: (Initialized s) . cc = s . cc by A1, SCMFSA6C:3;
set MI = for-up (a,bb,cc,I);
set i3 = a := bb;
set aux = 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I));
set i0 = (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc;
set i1 = SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb);
set i2 = AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0));
set IB = (I ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)));
set I4 = while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))));
set I03 = ((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))) ';' (a := bb);
set s1 = IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))) ';' (a := bb)),s);
set s2 = (s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb));
A4: (IExec ((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb))),s)) . (intloc 0) = (Exec ((SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)),(Exec (((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc),(Initialized s))))) . (intloc 0) by SCMFSA6C:9
.= (Exec (((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc),(Initialized s))) . (intloc 0) by SCMFSA_2:91
.= (Initialized s) . (intloc 0) by SCMFSA_2:89
.= 1 by SCMFSA6C:3 ;
( bb = intloc 0 or not bb is read-only ) by SF_MASTR:def 5;
then A5: (Initialized s) . bb = s . bb by A1, SCMFSA6C:3;
A6: (IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))) ';' (a := bb)),s)) . (intloc 0) = (Exec ((a := bb),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))),s)))) . (intloc 0) by SCMFSA6C:7
.= (IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))),s)) . (intloc 0) by SCMFSA_2:89
.= (Exec ((AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec ((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb))),s)))) . (intloc 0) by SCMFSA6C:7
.= 1 by A4, SCMFSA_2:90 ;
(s . bb) - (s . bb) > (s . cc) - (s . bb) by A2, XREAL_1:11;
then (s . cc) - (s . bb) <= - 1 by INT_1:21;
then A7: ((s . cc) - (s . bb)) + 1 <= (- 1) + 1 by XREAL_1:8;
set s3 = IExec ((for-up (a,bb,cc,I)),s);
a in {a,bb,cc} by ENUMSET1:def 1;
then a in {a,bb,cc} \/ (UsedIntLoc I) by XBOOLE_0:def 3;
then A8: a <> 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)) by SFMASTR1:21;
bb in {a,bb,cc} by ENUMSET1:def 1;
then bb in {a,bb,cc} \/ (UsedIntLoc I) by XBOOLE_0:def 3;
then A9: bb <> 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)) by SFMASTR1:21;
A10: (IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))) ';' (a := bb)),s)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) = (Exec ((a := bb),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))),s)))) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) by SCMFSA6C:7
.= (IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))),s)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) by A8, SCMFSA_2:89
.= (Exec ((AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec ((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb))),s)))) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) by SCMFSA6C:7
.= ((IExec ((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb))),s)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)))) + 1 by A4, SCMFSA_2:90
.= ((Exec ((SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)),(Exec (((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc),(Initialized s))))) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)))) + 1 by SCMFSA6C:9
.= (((Exec (((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc),(Initialized s))) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)))) - ((Exec (((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc),(Initialized s))) . bb)) + 1 by SCMFSA_2:91
.= (((Initialized s) . cc) - ((Exec (((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc),(Initialized s))) . bb)) + 1 by SCMFSA_2:89
.= ((s . cc) - (s . bb)) + 1 by A9, A3, A5, SCMFSA_2:89 ;
then ( while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))))) is_halting_on IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))) ';' (a := bb)),s) & while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))))) is_closed_on IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))) ';' (a := bb)),s) ) by A7, SCMFSA_9:43;
then A11: DataPart (IExec ((for-up (a,bb,cc,I)),s)) = DataPart (IExec ((while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))))),(IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))) ';' (a := bb)),s)))) by SFMASTR1:10
.= DataPart (IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))) ';' (a := bb)),s)) by A10, A7, A6, SCMFSA9A:41
.= DataPart ((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))) by A1, Th22 ;

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

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

proof

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

suppose x in {bb,cc} ; :: thesis: x in {a,bb,cc} \/ (UsedIntLoc 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} \/ (UsedIntLoc I) by XBOOLE_0:def 3; :: thesis: verum

end;

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

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

end;

end;

end;

then A14: x <> 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)) by SFMASTR1:21;
thus (IExec ((for-up (a,bb,cc,I)),s)) . x = ((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))) . x by A11, SCMFSA6A:38
.= (s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1))) . x by A12, FUNCT_7:34
.= s . x by A14, FUNCT_7:34 ; :: thesis: verum

end;

let x be FinSeq-Location ; :: thesis: (IExec ((for-up (a,bb,cc,I)),s)) . x = s . x
thus (IExec ((for-up (a,bb,cc,I)),s)) . x = ((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))) . x by A11, SCMFSA6A:38
.= (s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1))) . x by FUNCT_7:34, SCMFSA_2:83
.= s . x by FUNCT_7:34, SCMFSA_2:83 ; :: thesis: verum