let s be State of SCM+FSA; :: thesis: for a being read-write Int-Location
for bb, cc being Int-Location
for k being Nat
for p being Instruction-Sequence of SCM+FSA
for Ig being really-closed good MacroInstruction 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} \/ (UsedILoc Ig)) \/ FinSeq-Locations) = (IExec ((Ig ";" (AddTo (a,(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepForUp (a,bb,cc,Ig,p,s)) . k))) | (({a,bb,cc} \/ (UsedILoc Ig)) \/ FinSeq-Locations)
let a be read-write Int-Location; :: thesis: for bb, cc being Int-Location
for k being Nat
for p being Instruction-Sequence of SCM+FSA
for Ig being really-closed good MacroInstruction 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} \/ (UsedILoc Ig)) \/ FinSeq-Locations) = (IExec ((Ig ";" (AddTo (a,(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepForUp (a,bb,cc,Ig,p,s)) . k))) | (({a,bb,cc} \/ (UsedILoc Ig)) \/ FinSeq-Locations)
let bb, cc be Int-Location; :: thesis: for k being Nat
for p being Instruction-Sequence of SCM+FSA
for Ig being really-closed good MacroInstruction 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} \/ (UsedILoc Ig)) \/ FinSeq-Locations) = (IExec ((Ig ";" (AddTo (a,(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepForUp (a,bb,cc,Ig,p,s)) . k))) | (({a,bb,cc} \/ (UsedILoc Ig)) \/ FinSeq-Locations)
let k be Nat; :: thesis: for p being Instruction-Sequence of SCM+FSA
for Ig being really-closed good MacroInstruction 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} \/ (UsedILoc Ig)) \/ FinSeq-Locations) = (IExec ((Ig ";" (AddTo (a,(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepForUp (a,bb,cc,Ig,p,s)) . k))) | (({a,bb,cc} \/ (UsedILoc Ig)) \/ FinSeq-Locations)
let p be Instruction-Sequence of SCM+FSA; :: thesis: for Ig being really-closed good MacroInstruction 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} \/ (UsedILoc Ig)) \/ FinSeq-Locations) = (IExec ((Ig ";" (AddTo (a,(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepForUp (a,bb,cc,Ig,p,s)) . k))) | (({a,bb,cc} \/ (UsedILoc Ig)) \/ FinSeq-Locations)
let Ig be really-closed good MacroInstruction 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} \/ (UsedILoc Ig)) \/ FinSeq-Locations) = (IExec ((Ig ";" (AddTo (a,(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepForUp (a,bb,cc,Ig,p,s)) . k))) | (({a,bb,cc} \/ (UsedILoc 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} \/ (UsedILoc Ig)) \/ FinSeq-Locations) = (IExec ((Ig ";" (AddTo (a,(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepForUp (a,bb,cc,Ig,p,s)) . k))) | (({a,bb,cc} \/ (UsedILoc Ig)) \/ FinSeq-Locations)
set FL = FinSeq-Locations ;
set I = Ig;
set aux = 1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig));
set SF = StepForUp (a,bb,cc,Ig,p,s);
set IB = (Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)));
set s2 = (s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb));
set p2 = p;
set SW2 = StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))));
A4: ((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k) . (intloc 0) = 1 by A1, A2, A3, Th17;
set scb1 = ((s . cc) - (s . bb)) + 1;
A5: (((StepForUp (a,bb,cc,Ig,p,s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig)))) + k = ((s . cc) - (s . bb)) + 1 by A1, A2, A3, Th17;
A6: ((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))) > 0

proof

assume ((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))) <= 0 ; :: thesis: contradiction
then (((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc 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} \/ (UsedILoc Ig))),(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k));
set IB1 = Ig ";" (AddTo (a,(intloc 0)));
set Iloc = {a,bb,cc} \/ (UsedILoc Ig);
set S1 = IExec ((Ig ";" (AddTo (a,(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k));
Ig is_halting_on (StepForUp (a,bb,cc,Ig,p,s)) . k,p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))))) by A2, A3;
then A7: Ig is_halting_on Initialized ((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k),p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))))) by A4, SCMFSA8B:42;
Macro (AddTo (a,(intloc 0))) is_halting_on IExec (Ig,(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k)),p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))))) by SCMFSA7B:19;
then A8: Ig ";" (AddTo (a,(intloc 0))) is_halting_on Initialized ((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k),p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))))) by A7, SFMASTR1:3;

now :: thesis: ( ( for x being Int-Location st x in {a,bb,cc} \/ (UsedILoc Ig) holds
(IExec ((Ig ";" (AddTo (a,(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k))) . x = (IExec (((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k))) . x ) & ( for x being FinSeq-Location holds (IExec ((Ig ";" (AddTo (a,(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k))) . x = (IExec (((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k))) . x ) )

hereby :: thesis: for x being FinSeq-Location holds (IExec ((Ig ";" (AddTo (a,(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k))) . x = (IExec (((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k))) . x

let x be Int-Location; :: thesis: ( x in {a,bb,cc} \/ (UsedILoc Ig) implies (IExec ((Ig ";" (AddTo (a,(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k))) . x = (IExec (((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k))) . x )
assume x in {a,bb,cc} \/ (UsedILoc Ig) ; :: thesis: (IExec ((Ig ";" (AddTo (a,(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k))) . x = (IExec (((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k))) . x
then A9: x <> 1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig)) by SCMFSA_M:25;
(IExec (((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k))) . x = (Exec ((SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))),(IExec ((Ig ";" (AddTo (a,(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k))))) . x by A8, SFMASTR1:11
.= (IExec ((Ig ";" (AddTo (a,(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k))) . x by A9, SCMFSA_2:65 ;
hence (IExec ((Ig ";" (AddTo (a,(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k))) . x = (IExec (((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc 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} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k))) . x = (IExec (((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k))) . x
(IExec (((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k))) . x = (Exec ((SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))),(IExec ((Ig ";" (AddTo (a,(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k))))) . x by A8, SFMASTR1:12
.= (IExec ((Ig ";" (AddTo (a,(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc 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} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k))) . x = (IExec (((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k))) . x ; :: thesis: verum

end;

then A10: (IExec ((Ig ";" (AddTo (a,(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k))) | (({a,bb,cc} \/ (UsedILoc Ig)) \/ FinSeq-Locations) = (IExec (((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k))) | (({a,bb,cc} \/ (UsedILoc Ig)) \/ FinSeq-Locations) by SCMFSA_M:28;
A11: (Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))) = Ig ";" ((AddTo (a,(intloc 0))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))) by SCMFSA6A:28;
(AddTo (a,(intloc 0))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))) is_halting_on IExec (Ig,(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k)),p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))))) by SCMFSA7B:19;
then DataPart ((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . (k + 1)) = DataPart (IExec (((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k))) by A4, A6, A7, A11, SCMFSA9A:32, SFMASTR1:3;
hence ((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) | (({a,bb,cc} \/ (UsedILoc Ig)) \/ FinSeq-Locations) = (IExec ((Ig ";" (AddTo (a,(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepForUp (a,bb,cc,Ig,p,s)) . k))) | (({a,bb,cc} \/ (UsedILoc Ig)) \/ FinSeq-Locations) by A10, RELAT_1:153, SCMFSA_2:100, XBOOLE_1:9; :: thesis: verum