let s be State of SCM+FSA; :: thesis: for a being read-write Int-Location
for cc, bb being Int-Location
for Ig being good Program of {INT,(INT *)}
for k being Element of NAT st s . (intloc 0) = 1 & k = ((s . cc) - (s . bb)) + 1 & ( ProperForUpBody a,bb,cc,Ig,s or Ig is parahalting ) holds
DataPart (IExec ((for-up (a,bb,cc,Ig)),s)) = DataPart ((StepForUp (a,bb,cc,Ig,s)) . k)
let a be read-write Int-Location ; :: thesis: for cc, bb being Int-Location
for Ig being good Program of {INT,(INT *)}
for k being Element of NAT st s . (intloc 0) = 1 & k = ((s . cc) - (s . bb)) + 1 & ( ProperForUpBody a,bb,cc,Ig,s or Ig is parahalting ) holds
DataPart (IExec ((for-up (a,bb,cc,Ig)),s)) = DataPart ((StepForUp (a,bb,cc,Ig,s)) . k)
let cc, bb be Int-Location ; :: thesis: for Ig being good Program of {INT,(INT *)}
for k being Element of NAT st s . (intloc 0) = 1 & k = ((s . cc) - (s . bb)) + 1 & ( ProperForUpBody a,bb,cc,Ig,s or Ig is parahalting ) holds
DataPart (IExec ((for-up (a,bb,cc,Ig)),s)) = DataPart ((StepForUp (a,bb,cc,Ig,s)) . k)
let Ig be good Program of {INT,(INT *)}; :: thesis: for k being Element of NAT st s . (intloc 0) = 1 & k = ((s . cc) - (s . bb)) + 1 & ( ProperForUpBody a,bb,cc,Ig,s or Ig is parahalting ) holds
DataPart (IExec ((for-up (a,bb,cc,Ig)),s)) = DataPart ((StepForUp (a,bb,cc,Ig,s)) . k)
let k be Element of NAT ; :: thesis: ( s . (intloc 0) = 1 & k = ((s . cc) - (s . bb)) + 1 & ( ProperForUpBody a,bb,cc,Ig,s or Ig is parahalting ) implies DataPart (IExec ((for-up (a,bb,cc,Ig)),s)) = DataPart ((StepForUp (a,bb,cc,Ig,s)) . k) )
set SAt = Start-At (0,SCM+FSA);
set I = Ig;
assume that
A1: s . (intloc 0) = 1 and
A2: k = ((s . cc) - (s . bb)) + 1 and
A3: ( ProperForUpBody a,bb,cc,Ig,s or Ig is parahalting ) ; :: thesis: DataPart (IExec ((for-up (a,bb,cc,Ig)),s)) = DataPart ((StepForUp (a,bb,cc,Ig,s)) . k)
set scb1 = ((s . cc) - (s . bb)) + 1;
set SF = StepForUp (a,bb,cc,Ig,s);
A4: ProperForUpBody a,bb,cc,Ig,s by A3, Th23;
set i3 = a := bb;
set aux = 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig));
set i0 = (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc;
set i1 = SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),bb);
set i2 = AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0));
set IB = (Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)));
set I03 = ((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))) ';' (a := bb);
set s1 = IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))) ';' (a := bb)),s);
A5: (IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))) ';' (a := bb)),s)) . (intloc 0) = (Exec ((a := bb),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),s)))) . (intloc 0) by SCMFSA6C:7
.= (IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),s)) . (intloc 0) by SCMFSA_2:89
.= (Exec ((AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0))),(IExec ((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),bb))),s)))) . (intloc 0) by SCMFSA6C:7
.= (IExec ((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),bb))),s)) . (intloc 0) by SCMFSA_2:90
.= (Exec ((SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),bb)),(Exec (((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc),(Initialized s))))) . (intloc 0) by SCMFSA6C:9
.= (Exec (((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc),(Initialized s))) . (intloc 0) by SCMFSA_2:91
.= (Initialized s) . (intloc 0) by SCMFSA_2:89
.= 1 by SCMFSA6C:3 ;
then A6: DataPart (Initialized (IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))) ';' (a := bb)),s))) = DataPart (IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))) ';' (a := bb)),s)) by SCMFSA8C:27;
set Ex1 = ExitsAtWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),(Initialized (IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))) ';' (a := bb)),s))));
set SW1 = StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),(Initialized (IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))) ';' (a := bb)),s))));
A7: ProperBodyWhile>0 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)),(Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0))), IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))) ';' (a := bb)),s) by A1, A3, Lm1;
then A8: ProperBodyWhile>0 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)),(Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0))), Initialized (IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))) ';' (a := bb)),s)) by A6, SCMFSA9A:44;
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))));
A9: DataPart (IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))) ';' (a := bb)),s)) = DataPart ((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))) by A1, Th22;
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)))),(Initialized (IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))) ';' (a := bb)),s))))) . k) = 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 A6, A8, SCMFSA9A:40;
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)))),(Initialized (IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))) ';' (a := bb)),s))))) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc 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 SCMFSA6A:38;
A11: WithVariantWhile>0 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)),(Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0))), IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))) ';' (a := bb)),s) by A1, A3, Lm1;
then A12: WithVariantWhile>0 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)),(Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0))), Initialized (IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))) ';' (a := bb)),s)) by A5, A6, A7, SCMFSA9A:47;
then consider K being Element of NAT such that
A13: ExitsAtWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),(Initialized (IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))) ';' (a := bb)),s)))) = K and
A14: ((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),(Initialized (IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))) ';' (a := bb)),s))))) . K) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) <= 0 and
A15: for i being Element of NAT st ((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),(Initialized (IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))) ';' (a := bb)),s))))) . i) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) <= 0 holds
K <= i and
DataPart (Comput ((ProgramPart ((Initialized (IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))) ';' (a := bb)),s))) +* ((while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),((Initialized (IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))) ';' (a := bb)),s))) +* ((while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))))) +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart ((Initialized (IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))) ';' (a := bb)),s))) +* ((while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))))) +* (Start-At (0,SCM+FSA))))),((Initialized (IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))) ';' (a := bb)),s))) +* ((while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))))) +* (Start-At (0,SCM+FSA)))))))) = 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)))),(Initialized (IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))) ';' (a := bb)),s))))) . K) by A8, SCMFSA9A:def 6;
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)))),(Initialized (IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))) ';' (a := bb)),s))))) . K) = 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 A6, A8, A9, SCMFSA9A:40;
then A16: ((StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),(Initialized (IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))) ';' (a := bb)),s))))) . K) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc 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 SCMFSA6A:38;

A17: now

assume A18: K < ((s . cc) - (s . bb)) + 1 ; :: thesis: contradiction
then (((StepForUp (a,bb,cc,Ig,s)) . K) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)))) + K < 0 + (((s . cc) - (s . bb)) + 1) by A14, A16, XREAL_1:10;
hence contradiction by A1, A4, A18, Th25; :: thesis: verum

end;

(((StepForUp (a,bb,cc,Ig,s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)))) + k = ((s . cc) - (s . bb)) + 1 by A1, A2, A4, Th25;
then K <= k by A2, A15, A10;
then A19: ExitsAtWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),(Initialized (IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))) ';' (a := bb)),s)))) = k by A2, A13, A17, XXREAL_0:1;
set MI = for-up (a,bb,cc,Ig);
set I4 = while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))));
( while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0))))) is_halting_on IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))) ';' (a := bb)),s) & while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0))))) is_closed_on IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))) ';' (a := bb)),s) ) by A7, A11, SCMFSA9A:33;
hence DataPart (IExec ((for-up (a,bb,cc,Ig)),s)) = DataPart (IExec ((while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))))),(IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))) ';' (a := bb)),s)))) by SFMASTR1:10
.= 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)))),(Initialized (IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))) ';' (a := bb)),s))))) . (ExitsAtWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),((Ig ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))),(Initialized (IExec ((((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(intloc 0)))) ';' (a := bb)),s)))))) by A8, A12, SCMFSA9A:42
.= DataPart ((StepForUp (a,bb,cc,Ig,s)) . k) by A6, A8, A9, A19, SCMFSA9A:40 ;
:: thesis: verum