let s be State of SCM+FSA; :: thesis: for a being read-write Int-Location
for bb, cc being Int-Location
for Ig being good Program of {INT,(INT *)} st s . (intloc 0) = 1 & ProperForUpBody a,bb,cc,Ig,s holds
for k being Element of NAT st k <= ((s . cc) - (s . bb)) + 1 holds
( ((StepForUp (a,bb,cc,Ig,s)) . k) . (intloc 0) = 1 & ( not Ig destroys a implies ( ((StepForUp (a,bb,cc,Ig,s)) . k) . a = k + (s . bb) & ((StepForUp (a,bb,cc,Ig,s)) . k) . a <= (s . cc) + 1 ) ) & (((StepForUp (a,bb,cc,Ig,s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)))) + k = ((s . cc) - (s . bb)) + 1 )
let a be read-write Int-Location ; :: thesis: for bb, cc being Int-Location
for Ig being good Program of {INT,(INT *)} st s . (intloc 0) = 1 & ProperForUpBody a,bb,cc,Ig,s holds
for k being Element of NAT st k <= ((s . cc) - (s . bb)) + 1 holds
( ((StepForUp (a,bb,cc,Ig,s)) . k) . (intloc 0) = 1 & ( not Ig destroys a implies ( ((StepForUp (a,bb,cc,Ig,s)) . k) . a = k + (s . bb) & ((StepForUp (a,bb,cc,Ig,s)) . k) . a <= (s . cc) + 1 ) ) & (((StepForUp (a,bb,cc,Ig,s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)))) + k = ((s . cc) - (s . bb)) + 1 )
let bb, cc be Int-Location ; :: thesis: for Ig being good Program of {INT,(INT *)} st s . (intloc 0) = 1 & ProperForUpBody a,bb,cc,Ig,s holds
for k being Element of NAT st k <= ((s . cc) - (s . bb)) + 1 holds
( ((StepForUp (a,bb,cc,Ig,s)) . k) . (intloc 0) = 1 & ( not Ig destroys a implies ( ((StepForUp (a,bb,cc,Ig,s)) . k) . a = k + (s . bb) & ((StepForUp (a,bb,cc,Ig,s)) . k) . a <= (s . cc) + 1 ) ) & (((StepForUp (a,bb,cc,Ig,s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)))) + k = ((s . cc) - (s . bb)) + 1 )
let Ig be good Program of {INT,(INT *)}; :: thesis: ( s . (intloc 0) = 1 & ProperForUpBody a,bb,cc,Ig,s implies for k being Element of NAT st k <= ((s . cc) - (s . bb)) + 1 holds
( ((StepForUp (a,bb,cc,Ig,s)) . k) . (intloc 0) = 1 & ( not Ig destroys a implies ( ((StepForUp (a,bb,cc,Ig,s)) . k) . a = k + (s . bb) & ((StepForUp (a,bb,cc,Ig,s)) . k) . a <= (s . cc) + 1 ) ) & (((StepForUp (a,bb,cc,Ig,s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)))) + k = ((s . cc) - (s . bb)) + 1 ) )
set I = Ig;
assume that
A1: s . (intloc 0) = 1 and
A2: ProperForUpBody a,bb,cc,Ig,s ; :: thesis: for k being Element of NAT st k <= ((s . cc) - (s . bb)) + 1 holds
( ((StepForUp (a,bb,cc,Ig,s)) . k) . (intloc 0) = 1 & ( not Ig destroys a implies ( ((StepForUp (a,bb,cc,Ig,s)) . k) . a = k + (s . bb) & ((StepForUp (a,bb,cc,Ig,s)) . k) . a <= (s . cc) + 1 ) ) & (((StepForUp (a,bb,cc,Ig,s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)))) + k = ((s . cc) - (s . bb)) + 1 )
set scb1 = ((s . cc) - (s . bb)) + 1;
set aux = 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig));
set SF = StepForUp (a,bb,cc,Ig,s);
set IB = (Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)));
set s2 = (s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb));
set SW2 = StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))));
A3: (Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0))) = Ig ';' ((AddTo (a,(intloc 0))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))) by SCMFSA6A:70;
defpred S₁[ Nat] means ( $1 <= ((s . cc) - (s . bb)) + 1 implies ( ((StepForUp (a,bb,cc,Ig,s)) . $1) . (intloc 0) = 1 & ( not Ig destroys a implies ( ((StepForUp (a,bb,cc,Ig,s)) . $1) . a = $1 + (s . bb) & ((StepForUp (a,bb,cc,Ig,s)) . $1) . a <= (s . cc) + 1 ) ) & (((StepForUp (a,bb,cc,Ig,s)) . $1) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)))) + $1 = ((s . cc) - (s . bb)) + 1 ) );
a in {a,bb,cc} by ENUMSET1:def 1;
then a in {a,bb,cc} \/ (UsedIntLoc Ig) by XBOOLE_0:def 3;
then A4: 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)) <> a by SFMASTR1:21;
A5: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: S₁[k] ; :: thesis: S₁[k + 1]
thus S₁[k + 1] :: thesis: verum

proof

A7: not 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)) in UsedIntLoc Ig

proof

assume 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)) in UsedIntLoc Ig ; :: thesis: contradiction
then 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)) in {a,bb,cc} \/ (UsedIntLoc Ig) by XBOOLE_0:def 3;
hence contradiction by SFMASTR1:21; :: thesis: verum

end;

set k1 = k + 1;
assume A8: k + 1 <= ((s . cc) - (s . bb)) + 1 ; :: thesis: ( ((StepForUp (a,bb,cc,Ig,s)) . (k + 1)) . (intloc 0) = 1 & ( not Ig destroys a implies ( ((StepForUp (a,bb,cc,Ig,s)) . (k + 1)) . a = (k + 1) + (s . bb) & ((StepForUp (a,bb,cc,Ig,s)) . (k + 1)) . a <= (s . cc) + 1 ) ) & (((StepForUp (a,bb,cc,Ig,s)) . (k + 1)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)))) + (k + 1) = ((s . cc) - (s . bb)) + 1 )
A9: k < k + 1 by XREAL_1:31;
then A10: ((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) > 0 by A6, A8, XREAL_1:10, XXREAL_0:2;
A11: k < ((s . cc) - (s . bb)) + 1 by A8, A9, XXREAL_0:2;
then A12: Ig is_closed_on (StepForUp (a,bb,cc,Ig,s)) . k by A2, Def7;
then A13: Ig is_closed_on Initialized ((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k) by A6, A8, A9, SFMASTR2:4, XXREAL_0:2;
A14: Ig is_halting_on (StepForUp (a,bb,cc,Ig,s)) . k by A2, A11, Def7;
then A15: Ig is_halting_on Initialized ((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k) by A6, A8, A9, A12, SFMASTR2:5, XXREAL_0:2;
thus ((StepForUp (a,bb,cc,Ig,s)) . (k + 1)) . (intloc 0) = 1 by A6, A8, A9, A12, A14, Th24, XXREAL_0:2; :: thesis: ( ( not Ig destroys a implies ( ((StepForUp (a,bb,cc,Ig,s)) . (k + 1)) . a = (k + 1) + (s . bb) & ((StepForUp (a,bb,cc,Ig,s)) . (k + 1)) . a <= (s . cc) + 1 ) ) & (((StepForUp (a,bb,cc,Ig,s)) . (k + 1)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)))) + (k + 1) = ((s . cc) - (s . bb)) + 1 )
A16: (AddTo (a,(intloc 0))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0))) is_closed_on IExec (Ig,((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k)) by SCMFSA7B:24;
then A17: (Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0))) is_closed_on Initialized ((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k) by A3, A13, A15, SFMASTR1:3;
(AddTo (a,(intloc 0))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0))) is_halting_on IExec (Ig,((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k)) by SCMFSA7B:25;
then (Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0))) is_halting_on Initialized ((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k) by A3, A13, A15, A16, SFMASTR1:4;
then A18: DataPart ((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . (k + 1)) = DataPart (IExec (((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k))) by A6, A8, A9, A10, A17, SCMFSA9A:38, XXREAL_0:2;

hereby :: thesis: (((StepForUp (a,bb,cc,Ig,s)) . (k + 1)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)))) + (k + 1) = ((s . cc) - (s . bb)) + 1

assume A19: not Ig destroys a ; :: thesis: ( ((StepForUp (a,bb,cc,Ig,s)) . (k + 1)) . a = (k + 1) + (s . bb) & ((StepForUp (a,bb,cc,Ig,s)) . (k + 1)) . a <= (s . cc) + 1 )
A20: (IExec (((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k))) . a = (IExec (((AddTo (a,(intloc 0))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),(IExec (Ig,((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k))))) . a by A3, A13, A15, SFMASTR1:8
.= (Exec ((SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0))),(Exec ((AddTo (a,(intloc 0))),(Initialized (IExec (Ig,((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k)))))))) . a by SCMFSA6C:9
.= (Exec ((AddTo (a,(intloc 0))),(Initialized (IExec (Ig,((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k)))))) . a by A4, SCMFSA_2:91
.= ((Initialized (IExec (Ig,((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k)))) . a) + ((Initialized (IExec (Ig,((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k)))) . (intloc 0)) by SCMFSA_2:90
.= ((Initialized (IExec (Ig,((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k)))) . a) + 1 by SCMFSA6C:3
.= ((IExec (Ig,((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k))) . a) + 1 by SCMFSA6C:3
.= ((Initialized ((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k)) . a) + 1 by A13, A15, A19, Th7
.= (((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k) . a) + 1 by SCMFSA6C:3 ;
hence ((StepForUp (a,bb,cc,Ig,s)) . (k + 1)) . a = (k + 1) + (s . bb) by A6, A8, A9, A18, A19, SCMFSA6A:38, XXREAL_0:2; :: thesis: ((StepForUp (a,bb,cc,Ig,s)) . (k + 1)) . a <= (s . cc) + 1
(k + 1) + (s . bb) <= (((s . cc) + 1) - (s . bb)) + (s . bb) by A8, XREAL_1:8;
hence ((StepForUp (a,bb,cc,Ig,s)) . (k + 1)) . a <= (s . cc) + 1 by A6, A8, A9, A18, A19, A20, SCMFSA6A:38, XXREAL_0:2; :: thesis: verum

end;

(IExec (((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k))) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) = (IExec (((AddTo (a,(intloc 0))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),(IExec (Ig,((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k))))) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) by A3, A13, A15, SFMASTR1:8
.= (Exec ((SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0))),(Exec ((AddTo (a,(intloc 0))),(Initialized (IExec (Ig,((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k)))))))) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) by SCMFSA6C:9
.= ((Exec ((AddTo (a,(intloc 0))),(Initialized (IExec (Ig,((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k)))))) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)))) - ((Exec ((AddTo (a,(intloc 0))),(Initialized (IExec (Ig,((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k)))))) . (intloc 0)) by SCMFSA_2:91
.= ((Exec ((AddTo (a,(intloc 0))),(Initialized (IExec (Ig,((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k)))))) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)))) - ((Initialized (IExec (Ig,((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k)))) . (intloc 0)) by SCMFSA_2:90
.= ((Exec ((AddTo (a,(intloc 0))),(Initialized (IExec (Ig,((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k)))))) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)))) - 1 by SCMFSA6C:3
.= ((Initialized (IExec (Ig,((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k)))) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)))) - 1 by A4, SCMFSA_2:90
.= ((IExec (Ig,((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k))) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)))) - 1 by SCMFSA6C:3
.= ((Initialized ((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)))) - 1 by A13, A15, A7, Th7, SFMASTR1:1
.= (((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)))) - 1 by SCMFSA6C:3 ;
hence (((StepForUp (a,bb,cc,Ig,s)) . (k + 1)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)))) + (k + 1) = ((((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)))) - 1) + (k + 1) by A18, SCMFSA6A:38
.= ((s . cc) - (s . bb)) + 1 by A6, A8, A9, XXREAL_0:2 ;
:: thesis: verum

end;

end;

A21: a in dom (s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) by SCMFSA_2:66;
A22: 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)) in dom s by SCMFSA_2:66;
A23: S₁[ 0 ]

proof

assume A24: 0 <= ((s . cc) - (s . bb)) + 1 ; :: thesis: ( ((StepForUp (a,bb,cc,Ig,s)) . 0) . (intloc 0) = 1 & ( not Ig destroys a implies ( ((StepForUp (a,bb,cc,Ig,s)) . 0) . a = 0 + (s . bb) & ((StepForUp (a,bb,cc,Ig,s)) . 0) . a <= (s . cc) + 1 ) ) & (((StepForUp (a,bb,cc,Ig,s)) . 0) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)))) + 0 = ((s . cc) - (s . bb)) + 1 )
A25: (StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . 0 = (s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb)) by SCMFSA_9:def 5;
hence ((StepForUp (a,bb,cc,Ig,s)) . 0) . (intloc 0) = (s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) . (intloc 0) by FUNCT_7:34
.= 1 by A1, FUNCT_7:34 ;
:: thesis: ( ( not Ig destroys a implies ( ((StepForUp (a,bb,cc,Ig,s)) . 0) . a = 0 + (s . bb) & ((StepForUp (a,bb,cc,Ig,s)) . 0) . a <= (s . cc) + 1 ) ) & (((StepForUp (a,bb,cc,Ig,s)) . 0) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)))) + 0 = ((s . cc) - (s . bb)) + 1 )

hereby :: thesis: (((StepForUp (a,bb,cc,Ig,s)) . 0) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)))) + 0 = ((s . cc) - (s . bb)) + 1

assume not Ig destroys a ; :: thesis: ( ((StepForUp (a,bb,cc,Ig,s)) . 0) . a = 0 + (s . bb) & ((StepForUp (a,bb,cc,Ig,s)) . 0) . a <= (s . cc) + 1 )
thus ((StepForUp (a,bb,cc,Ig,s)) . 0) . a = 0 + (s . bb) by A21, A25, FUNCT_7:33; :: thesis: ((StepForUp (a,bb,cc,Ig,s)) . 0) . a <= (s . cc) + 1
0 + (s . bb) <= (((s . cc) + 1) - (s . bb)) + (s . bb) by A24, XREAL_1:8;
hence ((StepForUp (a,bb,cc,Ig,s)) . 0) . a <= (s . cc) + 1 by A21, A25, FUNCT_7:33; :: thesis: verum

end;

thus (((StepForUp (a,bb,cc,Ig,s)) . 0) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)))) + 0 = (s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) by A4, A25, FUNCT_7:34
.= ((s . cc) - (s . bb)) + 1 by A22, FUNCT_7:33 ; :: thesis: verum

end;

thus for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A23, A5); :: thesis: verum