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 SCM+FSA 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 destroysdestroy 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 SCM+FSA 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 destroysdestroy 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 SCM+FSA 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 destroysdestroy 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 SCM+FSA ; :: 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 destroysdestroy 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 D = Int-Locations \/ FinSeq-Locations ;
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 destroysdestroy 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 destroysdestroy 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 destroysdestroy 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 destroysdestroy 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 destroysdestroy 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 destroysdestroy 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 destroysdestroy 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 destroysdestroy 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