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 SCM+FSA 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 SCM+FSA 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 SCM+FSA 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 SCM+FSA ; :: 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 D = Int-Locations \/ FinSeq-Locations ;
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