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
for k being Element of NAT
for p being Instruction-Sequence of SCM+FSA st s . (intloc 0) = 1 & ProperForUpBody a,bb,cc,Ig,s,p & k < ((s . cc) - (s . bb)) + 1 holds
((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) | (({a,bb,cc} \/ (UsedIntLoc Ig)) \/ FinSeq-Locations) = (IExec ((Ig ';' (AddTo (a,(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0))))))),((StepForUp (a,bb,cc,Ig,p,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
for k being Element of NAT
for p being Instruction-Sequence of SCM+FSA st s . (intloc 0) = 1 & ProperForUpBody a,bb,cc,Ig,s,p & k < ((s . cc) - (s . bb)) + 1 holds
((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) | (({a,bb,cc} \/ (UsedIntLoc Ig)) \/ FinSeq-Locations) = (IExec ((Ig ';' (AddTo (a,(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0))))))),((StepForUp (a,bb,cc,Ig,p,s)) . k))) | (({a,bb,cc} \/ (UsedIntLoc Ig)) \/ FinSeq-Locations)
let bb, cc be Int-Location ; :: thesis: for Ig being good Program of
for k being Element of NAT
for p being Instruction-Sequence of SCM+FSA st s . (intloc 0) = 1 & ProperForUpBody a,bb,cc,Ig,s,p & k < ((s . cc) - (s . bb)) + 1 holds
((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) | (({a,bb,cc} \/ (UsedIntLoc Ig)) \/ FinSeq-Locations) = (IExec ((Ig ';' (AddTo (a,(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0))))))),((StepForUp (a,bb,cc,Ig,p,s)) . k))) | (({a,bb,cc} \/ (UsedIntLoc Ig)) \/ FinSeq-Locations)
let Ig be good Program of ; :: thesis: for k being Element of NAT
for p being Instruction-Sequence of SCM+FSA st s . (intloc 0) = 1 & ProperForUpBody a,bb,cc,Ig,s,p & k < ((s . cc) - (s . bb)) + 1 holds
((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) | (({a,bb,cc} \/ (UsedIntLoc Ig)) \/ FinSeq-Locations) = (IExec ((Ig ';' (AddTo (a,(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0))))))),((StepForUp (a,bb,cc,Ig,p,s)) . k))) | (({a,bb,cc} \/ (UsedIntLoc Ig)) \/ FinSeq-Locations)
let k be Element of NAT ; :: thesis: for p being Instruction-Sequence of SCM+FSA st s . (intloc 0) = 1 & ProperForUpBody a,bb,cc,Ig,s,p & k < ((s . cc) - (s . bb)) + 1 holds
((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) | (({a,bb,cc} \/ (UsedIntLoc Ig)) \/ FinSeq-Locations) = (IExec ((Ig ';' (AddTo (a,(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0))))))),((StepForUp (a,bb,cc,Ig,p,s)) . k))) | (({a,bb,cc} \/ (UsedIntLoc Ig)) \/ FinSeq-Locations)
let p be Instruction-Sequence of SCM+FSA; :: thesis: ( s . (intloc 0) = 1 & ProperForUpBody a,bb,cc,Ig,s,p & k < ((s . cc) - (s . bb)) + 1 implies ((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) | (({a,bb,cc} \/ (UsedIntLoc Ig)) \/ FinSeq-Locations) = (IExec ((Ig ';' (AddTo (a,(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0))))))),((StepForUp (a,bb,cc,Ig,p,s)) . k))) | (({a,bb,cc} \/ (UsedIntLoc Ig)) \/ FinSeq-Locations) )
assume that
A1: s . (intloc 0) = 1 and
A2: ProperForUpBody a,bb,cc,Ig,s,p and
A3: k < ((s . cc) - (s . bb)) + 1 ; :: thesis: ((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) | (({a,bb,cc} \/ (UsedIntLoc Ig)) \/ FinSeq-Locations) = (IExec ((Ig ';' (AddTo (a,(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0))))))),((StepForUp (a,bb,cc,Ig,p,s)) . k))) | (({a,bb,cc} \/ (UsedIntLoc Ig)) \/ FinSeq-Locations)
set FL = FinSeq-Locations ;
set I = Ig;
set aux = 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig));
set SF = StepForUp (a,bb,cc,Ig,p,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 p2 = p;
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)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))));
StepForUp (a,bb,cc,Ig,p,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)))),p,((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)))),p,((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,p,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)))),p,((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)))),p,((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)))),p,((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:8;
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)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((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)))),p,((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)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((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)))),p,((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,(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((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)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k)),p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))))) by SCMFSA7B:18;
A8: Ig is_closed_on (StepForUp (a,bb,cc,Ig,p,s)) . k,p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))))) 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)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k),p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))))) by A4, SFMASTR2:4;
Ig is_halting_on (StepForUp (a,bb,cc,Ig,p,s)) . k,p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))))) 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)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k),p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))))) by A8, A4, SFMASTR2:5;
Macro (AddTo (a,(intloc 0))) is_halting_on IExec (Ig,(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((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)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k)),p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))))) by SCMFSA7B:19;
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)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k),p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))))) by A9, A10, A7, SFMASTR1:3;

now

hereby :: thesis: for x being FinSeq-Location holds (IExec ((Ig ';' (AddTo (a,(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((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)))),p,((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)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((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)))),p,((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)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((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)))),p,((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)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((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)))),p,((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)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((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)))),p,((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)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((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)))),p,((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:20;
(IExec (((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((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)))),p,((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)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((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)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k))))) . x by A9, A10, A7, A11, SFMASTR1:2, SFMASTR1:11
.= (IExec ((Ig ';' (AddTo (a,(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((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)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k))) . x by A12, SCMFSA_2:65 ;
hence (IExec ((Ig ';' (AddTo (a,(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((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)))),p,((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)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((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)))),p,((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)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((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)))),p,((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)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((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)))),p,((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)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((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)))),p,((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)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((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)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k))))) . x by A9, A10, A7, A11, SFMASTR1:2, SFMASTR1:12
.= (IExec ((Ig ';' (AddTo (a,(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((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)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k))) . x by SCMFSA_2:65 ;
hence (IExec ((Ig ';' (AddTo (a,(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((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)))),p,((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)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((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)))),p,((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)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((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)))),p,((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)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((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)))),p,((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,(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((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)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k)),p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))))) ) by SCMFSA6A:28, SCMFSA7B:18;
then ( (AddTo (a,(intloc 0))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0))) is_halting_on IExec (Ig,(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((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)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k)),p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((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))) 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)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k),p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))))) ) by A9, A10, SCMFSA7B:19, SFMASTR1:2;
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)))),p,((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)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((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)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k))) by A4, A6, A9, A10, A14, SCMFSA9A:32, SFMASTR1:3;
hence ((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) | (({a,bb,cc} \/ (UsedIntLoc Ig)) \/ FinSeq-Locations) = (IExec ((Ig ';' (AddTo (a,(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0))))))),((StepForUp (a,bb,cc,Ig,p,s)) . k))) | (({a,bb,cc} \/ (UsedIntLoc Ig)) \/ FinSeq-Locations) by A13, RELAT_1:153, SCMFSA_2:100, XBOOLE_1:9; :: thesis: verum