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 ((StepForUp (a,bb,cc,Ig,s)) . k) . (intloc 0) = 1 & Ig is_closed_on (StepForUp (a,bb,cc,Ig,s)) . k & Ig is_halting_on (StepForUp (a,bb,cc,Ig,s)) . k holds
((StepForUp (a,bb,cc,Ig,s)) . (k + 1)) . (intloc 0) = 1
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 ((StepForUp (a,bb,cc,Ig,s)) . k) . (intloc 0) = 1 & Ig is_closed_on (StepForUp (a,bb,cc,Ig,s)) . k & Ig is_halting_on (StepForUp (a,bb,cc,Ig,s)) . k holds
((StepForUp (a,bb,cc,Ig,s)) . (k + 1)) . (intloc 0) = 1
let bb, cc be Int-Location ; :: thesis: for Ig being good Program of {INT,(INT *)}
for k being Element of NAT st ((StepForUp (a,bb,cc,Ig,s)) . k) . (intloc 0) = 1 & Ig is_closed_on (StepForUp (a,bb,cc,Ig,s)) . k & Ig is_halting_on (StepForUp (a,bb,cc,Ig,s)) . k holds
((StepForUp (a,bb,cc,Ig,s)) . (k + 1)) . (intloc 0) = 1
let Ig be good Program of {INT,(INT *)}; :: thesis: for k being Element of NAT st ((StepForUp (a,bb,cc,Ig,s)) . k) . (intloc 0) = 1 & Ig is_closed_on (StepForUp (a,bb,cc,Ig,s)) . k & Ig is_halting_on (StepForUp (a,bb,cc,Ig,s)) . k holds
((StepForUp (a,bb,cc,Ig,s)) . (k + 1)) . (intloc 0) = 1
let k be Element of NAT ; :: thesis: ( ((StepForUp (a,bb,cc,Ig,s)) . k) . (intloc 0) = 1 & Ig is_closed_on (StepForUp (a,bb,cc,Ig,s)) . k & Ig is_halting_on (StepForUp (a,bb,cc,Ig,s)) . k implies ((StepForUp (a,bb,cc,Ig,s)) . (k + 1)) . (intloc 0) = 1 )
set I = Ig;
assume that
A1: ((StepForUp (a,bb,cc,Ig,s)) . k) . (intloc 0) = 1 and
A2: ( Ig is_closed_on (StepForUp (a,bb,cc,Ig,s)) . k & Ig is_halting_on (StepForUp (a,bb,cc,Ig,s)) . k ) ; :: thesis: ((StepForUp (a,bb,cc,Ig,s)) . (k + 1)) . (intloc 0) = 1
set aux = 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig));
set IB = (Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)));
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;

per cases ( ((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 or ((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 ) ;

suppose ((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: ((StepForUp (a,bb,cc,Ig,s)) . (k + 1)) . (intloc 0) = 1

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 ((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 SCMFSA9A:37;
hence ((StepForUp (a,bb,cc,Ig,s)) . (k + 1)) . (intloc 0) = 1 by A1, SCMFSA6A:38; :: thesis: verum

end;

suppose 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) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) > 0 ; :: thesis: ((StepForUp (a,bb,cc,Ig,s)) . (k + 1)) . (intloc 0) = 1

A5: ( 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) & 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 A1, A2, SFMASTR2:5;
A6: (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 ( (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 A3, A5, SCMFSA7B:25, SFMASTR1:3;
then A7: 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 A1, A3, A4, A5, A6, SCMFSA9A:38, SFMASTR1:4;
(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))) . (intloc 0) = (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))))) . (intloc 0) by A3, A5, 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)))))))) . (intloc 0) 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)))))) . (intloc 0) by 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)))) . (intloc 0) by SCMFSA_2:90
.= 1 by SCMFSA6C:3 ;
hence ((StepForUp (a,bb,cc,Ig,s)) . (k + 1)) . (intloc 0) = 1 by A7, SCMFSA6A:38; :: thesis: verum

end;

end;