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 *)}
for k being Element of NAT st s . (intloc 0) = 1 & ProperForUpBody a,bb,cc,Ig,s & k < ((s . cc) - (s . bb)) + 1 holds
((StepForUp (a,bb,cc,Ig,s)) . (k + 1)) | (({a,bb,cc} \/ (UsedIntLoc Ig)) \/ FinSeq-Locations) = (IExec ((Ig ';' (AddTo (a,(intloc 0)))),((StepForUp (a,bb,cc,Ig,s)) . k))) | (({a,bb,cc} \/ (UsedIntLoc Ig)) \/ FinSeq-Locations)
let a be read-write Int-Location ; :: thesis: for bb, cc being Int-Location
for Ig being good Program of {INT,(INT *)}
for k being Element of NAT st s . (intloc 0) = 1 & ProperForUpBody a,bb,cc,Ig,s & k < ((s . cc) - (s . bb)) + 1 holds
((StepForUp (a,bb,cc,Ig,s)) . (k + 1)) | (({a,bb,cc} \/ (UsedIntLoc Ig)) \/ FinSeq-Locations) = (IExec ((Ig ';' (AddTo (a,(intloc 0)))),((StepForUp (a,bb,cc,Ig,s)) . k))) | (({a,bb,cc} \/ (UsedIntLoc Ig)) \/ FinSeq-Locations)
let bb, cc be Int-Location ; :: thesis: for Ig being good Program of {INT,(INT *)}
for k being Element of NAT st s . (intloc 0) = 1 & ProperForUpBody a,bb,cc,Ig,s & k < ((s . cc) - (s . bb)) + 1 holds
((StepForUp (a,bb,cc,Ig,s)) . (k + 1)) | (({a,bb,cc} \/ (UsedIntLoc Ig)) \/ FinSeq-Locations) = (IExec ((Ig ';' (AddTo (a,(intloc 0)))),((StepForUp (a,bb,cc,Ig,s)) . k))) | (({a,bb,cc} \/ (UsedIntLoc Ig)) \/ FinSeq-Locations)
let Ig be good Program of {INT,(INT *)}; :: thesis: for k being Element of NAT st s . (intloc 0) = 1 & ProperForUpBody a,bb,cc,Ig,s & k < ((s . cc) - (s . bb)) + 1 holds
((StepForUp (a,bb,cc,Ig,s)) . (k + 1)) | (({a,bb,cc} \/ (UsedIntLoc Ig)) \/ FinSeq-Locations) = (IExec ((Ig ';' (AddTo (a,(intloc 0)))),((StepForUp (a,bb,cc,Ig,s)) . k))) | (({a,bb,cc} \/ (UsedIntLoc Ig)) \/ FinSeq-Locations)
let k be Element of NAT ; :: thesis: ( s . (intloc 0) = 1 & ProperForUpBody a,bb,cc,Ig,s & k < ((s . cc) - (s . bb)) + 1 implies ((StepForUp (a,bb,cc,Ig,s)) . (k + 1)) | (({a,bb,cc} \/ (UsedIntLoc Ig)) \/ FinSeq-Locations) = (IExec ((Ig ';' (AddTo (a,(intloc 0)))),((StepForUp (a,bb,cc,Ig,s)) . k))) | (({a,bb,cc} \/ (UsedIntLoc Ig)) \/ FinSeq-Locations) )
set FL = FinSeq-Locations ;
set I = Ig;
assume that
A1: s . (intloc 0) = 1 and
A2: ProperForUpBody a,bb,cc,Ig,s and
A3: k < ((s . cc) - (s . bb)) + 1 ; :: thesis: ((StepForUp (a,bb,cc,Ig,s)) . (k + 1)) | (({a,bb,cc} \/ (UsedIntLoc Ig)) \/ FinSeq-Locations) = (IExec ((Ig ';' (AddTo (a,(intloc 0)))),((StepForUp (a,bb,cc,Ig,s)) . k))) | (({a,bb,cc} \/ (UsedIntLoc Ig)) \/ FinSeq-Locations)
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))));
StepForUp (a,bb,cc,Ig,s) = 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)))) ;
then A4: ((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) = 1 by A1, A2, A3, Th25;
set scb1 = ((s . cc) - (s . bb)) + 1;
A5: (((StepForUp (a,bb,cc,Ig,s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)))) + k = ((s . cc) - (s . bb)) + 1 by A1, A2, A3, Th25;
A6: ((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

proof

assume ((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 ; :: thesis: contradiction
then (((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)))) + k < 0 + (((s . cc) - (s . bb)) + 1) by A3, XREAL_1:10;
hence contradiction by A5; :: thesis: verum

end;

set S2 = 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));
set IB1 = Ig ';' (AddTo (a,(intloc 0)));
set Iloc = {a,bb,cc} \/ (UsedIntLoc Ig);
set S1 = IExec ((Ig ';' (AddTo (a,(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));
A7: Macro (AddTo (a,(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;
A8: Ig is_closed_on (StepForUp (a,bb,cc,Ig,s)) . k by A2, A3, Def7;
then A9: 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 A4, SFMASTR2:4;
Ig is_halting_on (StepForUp (a,bb,cc,Ig,s)) . k by A2, A3, Def7;
then A10: 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 A8, A4, SFMASTR2:5;
Macro (AddTo (a,(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 A11: Ig ';' (AddTo (a,(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 A9, A10, A7, SFMASTR1:4;

now

hereby :: thesis: for x being FinSeq-Location holds (IExec ((Ig ';' (AddTo (a,(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))) . x = (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))) . x

let x be Int-Location ; :: thesis: ( x in {a,bb,cc} \/ (UsedIntLoc Ig) implies (IExec ((Ig ';' (AddTo (a,(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))) . x = (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))) . x )
assume x in {a,bb,cc} \/ (UsedIntLoc Ig) ; :: thesis: (IExec ((Ig ';' (AddTo (a,(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))) . x = (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))) . x
then A12: x <> 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)) by SFMASTR1:21;
(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))) . x = (Exec ((SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0))),(IExec ((Ig ';' (AddTo (a,(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))))) . x by A9, A10, A7, A11, SFMASTR1:3, SFMASTR1:12
.= (IExec ((Ig ';' (AddTo (a,(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))) . x by A12, SCMFSA_2:91 ;
hence (IExec ((Ig ';' (AddTo (a,(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))) . x = (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))) . x ; :: thesis: verum

end;

let x be FinSeq-Location ; :: thesis: (IExec ((Ig ';' (AddTo (a,(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))) . x = (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))) . x
(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))) . x = (Exec ((SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0))),(IExec ((Ig ';' (AddTo (a,(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))))) . x by A9, A10, A7, A11, SFMASTR1:3, SFMASTR1:13
.= (IExec ((Ig ';' (AddTo (a,(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))) . x by SCMFSA_2:91 ;
hence (IExec ((Ig ';' (AddTo (a,(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))) . x = (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))) . x ; :: thesis: verum

end;

then A13: (IExec ((Ig ';' (AddTo (a,(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,bb,cc} \/ (UsedIntLoc Ig)) \/ FinSeq-Locations) = (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,bb,cc} \/ (UsedIntLoc Ig)) \/ FinSeq-Locations) by SFMASTR2:7;
A14: ( (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)))) & (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 SCMFSA6A:70, SCMFSA7B:24;
then ( (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)) & (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 A9, A10, SCMFSA7B:25, SFMASTR1:3;
then 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 A4, A6, A9, A10, A14, SCMFSA9A:38, SFMASTR1:4;
hence ((StepForUp (a,bb,cc,Ig,s)) . (k + 1)) | (({a,bb,cc} \/ (UsedIntLoc Ig)) \/ FinSeq-Locations) = (IExec ((Ig ';' (AddTo (a,(intloc 0)))),((StepForUp (a,bb,cc,Ig,s)) . k))) | (({a,bb,cc} \/ (UsedIntLoc Ig)) \/ FinSeq-Locations) by A13, RELAT_1:188, SCMFSA_2:127, XBOOLE_1:9; :: thesis: verum