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 & 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 SCM+FSA 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 SCM+FSA 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 SCM+FSA ; :: 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 ) ) )
set D = Int-Locations \/ FinSeq-Locations ;
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: (Initialize 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),(Initialize s))) . (intloc 0 ) by SCMFSA6C:9
.= (Exec ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc),(Initialize s)) . (intloc 0 ) by SCMFSA_2:91
.= (Initialize 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: (Initialize 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),(Initialize s))) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)))) + 1 by SCMFSA6C:9
.= (((Exec ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc),(Initialize s)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)))) - ((Exec ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc),(Initialize s)) . bb)) + 1 by SCMFSA_2:91
.= (((Initialize s) . cc) - ((Exec ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc),(Initialize 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