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 *)} st s . (intloc 0) = 1 & ProperForUpBody a,bb,cc,Ig,s holds
for k being Element of NAT holds
( ((StepForUp (a,bb,cc,Ig,s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) > 0 iff k < ((s . cc) - (s . bb)) + 1 )
let a be read-write Int-Location ; :: thesis: for bb, cc being Int-Location
for Ig being good Program of {INT,(INT *)} st s . (intloc 0) = 1 & ProperForUpBody a,bb,cc,Ig,s holds
for k being Element of NAT holds
( ((StepForUp (a,bb,cc,Ig,s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) > 0 iff k < ((s . cc) - (s . bb)) + 1 )
let bb, cc be Int-Location ; :: thesis: for Ig being good Program of {INT,(INT *)} st s . (intloc 0) = 1 & ProperForUpBody a,bb,cc,Ig,s holds
for k being Element of NAT holds
( ((StepForUp (a,bb,cc,Ig,s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) > 0 iff k < ((s . cc) - (s . bb)) + 1 )
let Ig be good Program of {INT,(INT *)}; :: thesis: ( s . (intloc 0) = 1 & ProperForUpBody a,bb,cc,Ig,s implies for k being Element of NAT holds
( ((StepForUp (a,bb,cc,Ig,s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) > 0 iff k < ((s . cc) - (s . bb)) + 1 ) )
set I = Ig;
set SF = StepForUp (a,bb,cc,Ig,s);
set aux = 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig));
set s2 = (s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb));
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))));
set scb1 = ((s . cc) - (s . bb)) + 1;
defpred S₁[ Nat] means ( ((StepForUp (a,bb,cc,Ig,s)) . $1) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) > 0 implies $1 < ((s . cc) - (s . bb)) + 1 );
assume A1: ( s . (intloc 0) = 1 & ProperForUpBody a,bb,cc,Ig,s ) ; :: thesis: for k being Element of NAT holds
( ((StepForUp (a,bb,cc,Ig,s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) > 0 iff k < ((s . cc) - (s . bb)) + 1 )
A2: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume that
A3: S₁[k] and
A4: ((StepForUp (a,bb,cc,Ig,s)) . (k + 1)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) > 0 ; :: thesis: k + 1 < ((s . cc) - (s . bb)) + 1
A5: ((StepForUp (a,bb,cc,Ig,s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) > 0

proof

assume A6: ((StepForUp (a,bb,cc,Ig,s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) <= 0 ; :: thesis: contradiction
then DataPart ((StepForUp (a,bb,cc,Ig,s)) . (k + 1)) = DataPart ((StepForUp (a,bb,cc,Ig,s)) . k) by SCMFSA9A:37;
hence contradiction by A4, A6, SCMFSA6A:38; :: thesis: verum

end;

then reconsider scb1 = ((s . cc) - (s . bb)) + 1 as Element of NAT by A3, INT_1:16;
assume k + 1 >= ((s . cc) - (s . bb)) + 1 ; :: thesis: contradiction
then A7: (((StepForUp (a,bb,cc,Ig,s)) . (k + 1)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)))) + (k + 1) > 0 + scb1 by A4, XREAL_1:10;
k + 1 <= scb1 by A3, A5, NAT_1:13;
hence contradiction by A1, A7, Th25; :: thesis: verum

end;

let k be Element of NAT ; :: thesis: ( ((StepForUp (a,bb,cc,Ig,s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) > 0 iff k < ((s . cc) - (s . bb)) + 1 )
a in {a,bb,cc} by ENUMSET1:def 1;
then a in {a,bb,cc} \/ (UsedIntLoc Ig) by XBOOLE_0:def 3;
then A8: 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)) <> a by SFMASTR1:21;
A9: 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)) in dom s by SCMFSA_2:66;
A10: S₁[ 0 ]

proof

(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))))) . 0 = (s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb)) by SCMFSA_9:def 5;
then A11: ((StepForUp (a,bb,cc,Ig,s)) . 0) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) = (s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))),(((s . cc) - (s . bb)) + 1))) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) by A8, FUNCT_7:34
.= ((s . cc) - (s . bb)) + 1 by A9, FUNCT_7:33 ;
assume ((StepForUp (a,bb,cc,Ig,s)) . 0) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) > 0 ; :: thesis: 0 < ((s . cc) - (s . bb)) + 1
hence 0 < ((s . cc) - (s . bb)) + 1 by A11; :: thesis: verum

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A10, A2);
hence S₁[k] ; :: thesis: ( k < ((s . cc) - (s . bb)) + 1 implies ((StepForUp (a,bb,cc,Ig,s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) > 0 )
assume A12: k < ((s . cc) - (s . bb)) + 1 ; :: thesis: ((StepForUp (a,bb,cc,Ig,s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) > 0
then A13: k - k < (((s . cc) - (s . bb)) + 1) - k by XREAL_1:11;
(((StepForUp (a,bb,cc,Ig,s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)))) + k = ((s . cc) - (s . bb)) + 1 by A1, A12, Th25;
hence ((StepForUp (a,bb,cc,Ig,s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) > 0 by A13; :: thesis: verum