let s be State of SCM+FSA ; :: thesis:
let a be read-write Int-Location ; :: thesis:
let Ig be good Program of SCM+FSA ; :: thesis:
set I = Ig;
assume that
A1: s . (intloc 0 ) = 1 and
A2: ProperBodyWhile>0 a,Ig,s and
A3: WithVariantWhile>0 a,Ig,s ; :: thesis:
set SW = StepWhile>0 a,Ig,s;
consider K being Element of NAT such that
A4: ExitsAtWhile>0 a,Ig,s = K and
A5: ((StepWhile>0 a,Ig,s) . K) . a <= 0 and
A6: for i being Element of NAT st ((StepWhile>0 a,Ig,s) . i) . a <= 0 holds
K <= i and
DataPart (Comput (ProgramPart (s +* ((while>0 a,Ig) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,Ig) +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (s +* ((while>0 a,Ig) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,Ig) +* (Start-At 0 ,SCM+FSA ))))) = DataPart ((StepWhile>0 a,Ig,s) . K) by A2, A3, Def6;
consider f being Function of (product the Object-Kind of SCM+FSA ),NAT such that
A7: for k being Element of NAT holds
( f . ((StepWhile>0 a,Ig,s) . (k + 1)) < f . ((StepWhile>0 a,Ig,s) . k) or ((StepWhile>0 a,Ig,s) . k) . a <= 0 ) by A3, Def5;
A8: for i, j being Element of NAT st i < j & i <= K & j <= K holds
DataPart ((StepWhile>0 a,Ig,s) . i) <> DataPart ((StepWhile>0 a,Ig,s) . j)

let i, j be Element of NAT ; :: thesis:
assume that
A9: i < j and
i <= K and
A10: j <= K ; :: thesis:

per cases by A10, XXREAL_0:1;

suppose A11: j = K ; :: thesis:

assume DataPart ((StepWhile>0 a,Ig,s) . i) = DataPart ((StepWhile>0 a,Ig,s) . j) ; :: thesis:
then ((StepWhile>0 a,Ig,s) . i) . a <= 0 by A5, A11, SCMFSA6A:38;
hence contradiction by A6, A9, A11; :: thesis:

end;

suppose A12: j < K ; :: thesis:

defpred S₁[ Nat] means ( j + $1 <= K implies DataPart ((StepWhile>0 a,Ig,s) . (i + $1)) = DataPart ((StepWhile>0 a,Ig,s) . (j + $1)) );
A13: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

let k be Element of NAT ; :: thesis:
assume that
A14: ( j + k <= K implies DataPart ((StepWhile>0 a,Ig,s) . (i + k)) = DataPart ((StepWhile>0 a,Ig,s) . (j + k)) ) and
A15: j + (k + 1) <= K ; :: thesis:
A16: ((StepWhile>0 a,Ig,s) . (j + k)) . (intloc 0 ) = 1 by A1, A2, Th39;
A17: j + k < (j + k) + 1 by XREAL_1:31;
then A18: j + k < K by A15, XXREAL_0:2;
then A19: ((StepWhile>0 a,Ig,s) . (j + k)) . a > 0 by A6;
then A20: Ig is_closed_on (StepWhile>0 a,Ig,s) . (j + k) by A2, Def4;
then A21: Ig is_closed_on Initialized ((StepWhile>0 a,Ig,s) . (j + k)) by A16, Lm7;
A22: Ig is_halting_on (StepWhile>0 a,Ig,s) . (j + k) by A2, A19, Def4;
then A23: Ig is_halting_on Initialized ((StepWhile>0 a,Ig,s) . (j + k)) by A16, A20, Lm8;
A24: ((StepWhile>0 a,Ig,s) . (i + k)) . (intloc 0 ) = 1 by A1, A2, Th39;
A25: ((StepWhile>0 a,Ig,s) . (i + k)) . a > 0

assume not ((StepWhile>0 a,Ig,s) . (i + k)) . a > 0 ; :: thesis:
then A26: K <= i + k by A6;
i + k < j + k by A9, XREAL_1:8;
hence contradiction by A18, A26, XXREAL_0:2; :: thesis:

end;

then A27: Ig is_closed_on (StepWhile>0 a,Ig,s) . (i + k) by A2, Def4;
then A28: Ig is_closed_on Initialized ((StepWhile>0 a,Ig,s) . (i + k)) by A24, Lm7;
Ig is_halting_on (StepWhile>0 a,Ig,s) . (i + k) by A2, A25, Def4;
then A29: Ig is_halting_on Initialized ((StepWhile>0 a,Ig,s) . (i + k)) by A24, A27, Lm8;
thus DataPart ((StepWhile>0 a,Ig,s) . (i + (k + 1))) = DataPart ((StepWhile>0 a,Ig,s) . ((i + k) + 1))
.= DataPart (IExec Ig,((StepWhile>0 a,Ig,s) . (i + k))) by A24, A25, A28, A29, Th38
.= DataPart (IExec Ig,((StepWhile>0 a,Ig,s) . (j + k))) by A14, A15, A17, A16, A20, A22, SCMFSA8C:46, XXREAL_0:2
.= DataPart ((StepWhile>0 a,Ig,s) . ((j + k) + 1)) by A16, A19, A21, A23, Th38
.= DataPart ((StepWhile>0 a,Ig,s) . (j + (k + 1))) ; :: thesis:

end;

consider p being Element of NAT such that
A30: K = j + p and
1 <= p by A12, FINSEQ_4:99;
assume DataPart ((StepWhile>0 a,Ig,s) . i) = DataPart ((StepWhile>0 a,Ig,s) . j) ; :: thesis:
then A31: S₁[ 0 ] ;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A31, A13);
then DataPart ((StepWhile>0 a,Ig,s) . (i + p)) = DataPart ((StepWhile>0 a,Ig,s) . K) by A30;
then A32: ((StepWhile>0 a,Ig,s) . (i + p)) . a <= 0 by A5, SCMFSA6A:38;
i + p < K by A9, A30, XREAL_1:8;
hence contradiction by A6, A32; :: thesis:

end;

end;

end;

A33: for i, j being Element of NAT st i < j & i <= K & j <= K holds
(StepWhile>0 a,Ig,s) . i <> (StepWhile>0 a,Ig,s) . j

let i, j be Element of NAT ; :: thesis:
assume that
A34: i < j and
i <= K and
A35: j <= K ; :: thesis:
defpred S₁[ Nat] means ( i < $1 & $1 <= j implies f . ((StepWhile>0 a,Ig,s) . $1) < f . ((StepWhile>0 a,Ig,s) . i) );
A36: i < K by A34, A35, XXREAL_0:2;
A37: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

let k be Element of NAT ; :: thesis:
assume that
A38: ( i < k & k <= j implies f . ((StepWhile>0 a,Ig,s) . k) < f . ((StepWhile>0 a,Ig,s) . i) ) and
A39: i < k + 1 and
A40: k + 1 <= j ; :: thesis:
A41: i <= k by A39, NAT_1:13;

per cases by A41, XXREAL_0:1;

suppose A42: i = k ; :: thesis:

not ((StepWhile>0 a,Ig,s) . i) . a <= 0 by A6, A36;
hence f . ((StepWhile>0 a,Ig,s) . (k + 1)) < f . ((StepWhile>0 a,Ig,s) . i) by A7, A42; :: thesis:

end;

suppose A43: i < k ; :: thesis:

A44: k < j by A40, NAT_1:13;

assume ((StepWhile>0 a,Ig,s) . k) . a <= 0 ; :: thesis:
then K <= k by A6;
hence contradiction by A35, A44, XXREAL_0:2; :: thesis:

end;

then f . ((StepWhile>0 a,Ig,s) . (k + 1)) < f . ((StepWhile>0 a,Ig,s) . k) by A7;
hence f . ((StepWhile>0 a,Ig,s) . (k + 1)) < f . ((StepWhile>0 a,Ig,s) . i) by A38, A40, A43, NAT_1:13, XXREAL_0:2; :: thesis:

end;

end;

end;

assume A45: (StepWhile>0 a,Ig,s) . i = (StepWhile>0 a,Ig,s) . j ; :: thesis:
A46: S₁[ 0 ] ;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A46, A37);
hence contradiction by A34, A45; :: thesis:

end;

given i, j being Element of NAT such that A47: i <> j and
A48: ( i <= ExitsAtWhile>0 a,Ig,s & j <= ExitsAtWhile>0 a,Ig,s & ( (StepWhile>0 a,Ig,s) . i = (StepWhile>0 a,Ig,s) . j or DataPart ((StepWhile>0 a,Ig,s) . i) = DataPart ((StepWhile>0 a,Ig,s) . j) ) ) ; :: thesis:
( i < j or j < i ) by A47, XXREAL_0:1;
hence contradiction by A4, A33, A8, A48; :: thesis: