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 SCM+FSA
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 SCM+FSA
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 SCM+FSA
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 SCM+FSA ; :: 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 D = Int-Locations \/ FinSeq-Locations ;
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),(Initialize s))) . (intloc 0 ) by SCMFSA6C:9
.= (Exec ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) := cc),(Initialize s)) . (intloc 0 ) by SCMFSA_2:91
.= (Initialize s) . (intloc 0 ) by SCMFSA_2:89
.= 1 by SCMFSA6C:3 ;
then A6: DataPart (Initialize (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 ))),(Initialize (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 ))),(Initialize (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 )), Initialize (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 ))),(Initialize (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 ))),(Initialize (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 )), Initialize (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 ))),(Initialize (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 ))),(Initialize (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 ))),(Initialize (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 ((Initialize (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 )))),((Initialize (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 ((Initialize (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 ))),(Initialize (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 ))),(Initialize (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 ))),(Initialize (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 ))),(Initialize (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 ))),(Initialize (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 ))),(Initialize (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