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
for k being Element of NAT
for p being Instruction-Sequence of SCM+FSA st s . (intloc 0) = 1 & k = ((s . cc) - (s . bb)) + 1 & ( ProperForUpBody a,bb,cc,Ig,s,p or Ig is parahalting ) holds
DataPart (IExec ((for-up (a,bb,cc,Ig)),p,s)) = DataPart ((StepForUp (a,bb,cc,Ig,p,s)) . k)
let a be read-write Int-Location ; :: thesis: for cc, bb 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 & k = ((s . cc) - (s . bb)) + 1 & ( ProperForUpBody a,bb,cc,Ig,s,p or Ig is parahalting ) holds
DataPart (IExec ((for-up (a,bb,cc,Ig)),p,s)) = DataPart ((StepForUp (a,bb,cc,Ig,p,s)) . k)
let cc, bb 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 & k = ((s . cc) - (s . bb)) + 1 & ( ProperForUpBody a,bb,cc,Ig,s,p or Ig is parahalting ) holds
DataPart (IExec ((for-up (a,bb,cc,Ig)),p,s)) = DataPart ((StepForUp (a,bb,cc,Ig,p,s)) . k)
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 & k = ((s . cc) - (s . bb)) + 1 & ( ProperForUpBody a,bb,cc,Ig,s,p or Ig is parahalting ) holds
DataPart (IExec ((for-up (a,bb,cc,Ig)),p,s)) = DataPart ((StepForUp (a,bb,cc,Ig,p,s)) . k)
let k be Element of NAT ; :: thesis: for p being Instruction-Sequence of SCM+FSA st s . (intloc 0) = 1 & k = ((s . cc) - (s . bb)) + 1 & ( ProperForUpBody a,bb,cc,Ig,s,p or Ig is parahalting ) holds
DataPart (IExec ((for-up (a,bb,cc,Ig)),p,s)) = DataPart ((StepForUp (a,bb,cc,Ig,p,s)) . k)
let p be Instruction-Sequence of SCM+FSA; :: thesis: ( s . (intloc 0) = 1 & k = ((s . cc) - (s . bb)) + 1 & ( ProperForUpBody a,bb,cc,Ig,s,p or Ig is parahalting ) implies DataPart (IExec ((for-up (a,bb,cc,Ig)),p,s)) = DataPart ((StepForUp (a,bb,cc,Ig,p,s)) . k) )
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,p or Ig is parahalting ) ; :: thesis: DataPart (IExec ((for-up (a,bb,cc,Ig)),p,s)) = DataPart ((StepForUp (a,bb,cc,Ig,p,s)) . k)
set scb1 = ((s . cc) - (s . bb)) + 1;
set SF = StepForUp (a,bb,cc,Ig,p,s);
A4: ProperForUpBody a,bb,cc,Ig,s,p 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)),p,s);
set p1 = p;
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)),p,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)))),p,s)))) . (intloc 0) by SCMFSA6C:6
.= (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)))),p,s)) . (intloc 0) by SCMFSA_2:63
.= (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))),p,s)))) . (intloc 0) by SCMFSA6C:6
.= (IExec ((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),bb))),p,s)) . (intloc 0) by SCMFSA_2:64
.= (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:8
.= (Exec (((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc),(Initialized s))) . (intloc 0) by SCMFSA_2:65
.= (Initialized s) . (intloc 0) by SCMFSA_2:63
.= 1 by SCMFSA6A:38 ;
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)),p,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)),p,s)) by SCMFSA8C:7;
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)))),p,(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)),p,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)))),p,(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)),p,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)),p,s),p 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)),p,s)),p by A6, SCMFSA9A:38;
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))));
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)),p,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)))),p,(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)),p,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)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . k) by A6, A8, SCMFSA9A:34;
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)))),p,(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)),p,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)))),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))) by SCMFSA6A:7;
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)),p,s),p 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)),p,s)),p by A5, A6, A7, SCMFSA9A:41;
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)))),p,(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)),p,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)))),p,(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)),p,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)))),p,(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)),p,s))))) . i) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) <= 0 holds
K <= i ) & DataPart (Comput ((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))))))),(Initialize (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)),p,s)))),(LifeSpan ((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))))))),(Initialize (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)),p,s)))))))) = 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,(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)),p,s))))) . K) ) by A12, 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)))),p,(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)),p,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)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . K) by A6, A8, A9, SCMFSA9A:34;
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)))),p,(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)),p,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)))),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))) by SCMFSA6A:7;

A17: now

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

end;

(((StepForUp (a,bb,cc,Ig,p,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)))),p,(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)),p,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)),p,s),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))))) 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)),p,s),p ) by A7, A11, SCMFSA9A:27;
hence DataPart (IExec ((for-up (a,bb,cc,Ig)),p,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)))))),p,(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)),p,s)))) by SFMASTR1:9
.= 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,(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)),p,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)))),p,(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)),p,s)))))) by A8, A12, SCMFSA9A:36
.= DataPart ((StepForUp (a,bb,cc,Ig,p,s)) . k) by A6, A8, A9, A19, SCMFSA9A:34 ;
:: thesis: verum