let s be State of SCM+FSA; 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; 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; 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; 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 ; ( 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
; ( ( 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 for f being FinSeq-Location holds (IExec ((for-up (a,bb,cc,I)),p,s)) . f = s . f
let x be
Int-Location;
( 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)
;
(IExec ((for-up (a,bb,cc,I)),p,s)) . x = s . x
x in {a,bb,cc} \/ (UsedILoc I)
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
;
verum
end;
let x be FinSeq-Location ; (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
; verum