let s be State of SCM+FSA; :: thesis: for a being read-write Int-Location
for bb, cc being Int-Location
for p being Instruction-Sequence of SCM+FSA
for Ig being really-closed good MacroInstruction of SCM+FSA st s . (intloc 0) = 1 & ProperForUpBody a,bb,cc,Ig,s,p holds
for k being Nat holds
( ((StepForUp (a,bb,cc,Ig,p,s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))) > 0 iff k < ((s . cc) - (s . bb)) + 1 )
let a be read-write Int-Location; :: thesis: for bb, cc being Int-Location
for p being Instruction-Sequence of SCM+FSA
for Ig being really-closed good MacroInstruction of SCM+FSA st s . (intloc 0) = 1 & ProperForUpBody a,bb,cc,Ig,s,p holds
for k being Nat holds
( ((StepForUp (a,bb,cc,Ig,p,s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))) > 0 iff k < ((s . cc) - (s . bb)) + 1 )
let bb, cc be Int-Location; :: thesis: for p being Instruction-Sequence of SCM+FSA
for Ig being really-closed good MacroInstruction of SCM+FSA st s . (intloc 0) = 1 & ProperForUpBody a,bb,cc,Ig,s,p holds
for k being Nat holds
( ((StepForUp (a,bb,cc,Ig,p,s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))) > 0 iff k < ((s . cc) - (s . bb)) + 1 )
let p be Instruction-Sequence of SCM+FSA; :: thesis: for Ig being really-closed good MacroInstruction of SCM+FSA st s . (intloc 0) = 1 & ProperForUpBody a,bb,cc,Ig,s,p holds
for k being Nat holds
( ((StepForUp (a,bb,cc,Ig,p,s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))) > 0 iff k < ((s . cc) - (s . bb)) + 1 )
let Ig be really-closed good MacroInstruction of SCM+FSA ; :: thesis: ( s . (intloc 0) = 1 & ProperForUpBody a,bb,cc,Ig,s,p implies for k being Nat holds
( ((StepForUp (a,bb,cc,Ig,p,s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))) > 0 iff k < ((s . cc) - (s . bb)) + 1 ) )
set I = Ig;
set SF = StepForUp (a,bb,cc,Ig,p,s);
set aux = 1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig));
set s2 = (s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb));
set p2 = p;
set IB = (Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)));
set SW2 = StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc 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,p,s)) . $1) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))) > 0 implies $1 < ((s . cc) - (s . bb)) + 1 );
assume A1: ( s . (intloc 0) = 1 & ProperForUpBody a,bb,cc,Ig,s,p ) ; :: thesis: for k being Nat holds
( ((StepForUp (a,bb,cc,Ig,p,s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))) > 0 iff k < ((s . cc) - (s . bb)) + 1 )
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

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

proof

assume A6: ((StepForUp (a,bb,cc,Ig,p,s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))) <= 0 ; :: thesis: contradiction
then DataPart ((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) = DataPart ((StepForUp (a,bb,cc,Ig,p,s)) . k) by SCMFSA9A:31;
hence contradiction by A4, A6, SCMFSA_M:2; :: thesis: verum

end;

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

end;

let k be Nat; :: thesis: ( ((StepForUp (a,bb,cc,Ig,p,s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))) > 0 iff k < ((s . cc) - (s . bb)) + 1 )
a in {a,bb,cc} by ENUMSET1:def 1;
then a in {a,bb,cc} \/ (UsedILoc Ig) by XBOOLE_0:def 3;
then A8: 1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig)) <> a by SCMFSA_M:25;
A9: 1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig)) in dom s by SCMFSA_2:42;
A10: S₁[ 0 ]

proof

(StepWhile>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0)))),p,((s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb))))) . 0 = (s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) +* (a,(s . bb)) by SCMFSA_9:def 5;
then A11: ((StepForUp (a,bb,cc,Ig,p,s)) . 0) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))) = (s +* ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(((s . cc) - (s . bb)) + 1))) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))) by A8, FUNCT_7:32
.= ((s . cc) - (s . bb)) + 1 by A9, FUNCT_7:31 ;
assume ((StepForUp (a,bb,cc,Ig,p,s)) . 0) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))) > 0 ; :: thesis: 0 < ((s . cc) - (s . bb)) + 1
hence 0 < ((s . cc) - (s . bb)) + 1 by A11; :: thesis: verum

end;

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