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;
assume that
A1: s . (intloc 0 ) = 1 and
A2: 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 )
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₁[ Element of NAT ] means ( ((StepForUp a,bb,cc,Ig,s) . $1) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) > 0 implies $1 < ((s . cc) - (s . bb)) + 1 );
A3: 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)) in dom s by SCMFSA_2:66;
a in {a,bb,cc} by ENUMSET1:def 1;
then a in {a,bb,cc} \/ (UsedIntLoc Ig) by XBOOLE_0:def 3;
then A4: 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)) <> a by SFMASTR1:21;
A5: S₁[ 0 ]

proof

assume A6: ((StepForUp a,bb,cc,Ig,s) . 0 ) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) > 0 ; :: thesis: 0 < ((s . cc) - (s . bb)) + 1
(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 ((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 A4, FUNCT_7:34
.= ((s . cc) - (s . bb)) + 1 by A3, FUNCT_7:33 ;
hence 0 < ((s . cc) - (s . bb)) + 1 by A6; :: thesis: verum

end;

A7: 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
A8: S₁[k] and
A9: ((StepForUp a,bb,cc,Ig,s) . (k + 1)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) > 0 ; :: thesis: k + 1 < ((s . cc) - (s . bb)) + 1
A10: ((StepForUp a,bb,cc,Ig,s) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) > 0

proof

assume A11: ((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 A9, A11, SCMFSA6A:38; :: thesis: verum

end;

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

end;

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