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 (Computation (s +* ((while>0 a,Ig) +* (Start-At (insloc 0 )))),(LifeSpan (s +* ((while>0 a,Ig) +* (Start-At (insloc 0 )))))) = 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
(StepWhile>0 a,Ig,s) . i <> (StepWhile>0 a,Ig,s) . j

let i, j be Element of NAT ; :: thesis:
assume A9: ( i < j & i <= K & j <= K ) ; :: thesis:
then A10: i < K by XXREAL_0:2;
assume A11: (StepWhile>0 a,Ig,s) . i = (StepWhile>0 a,Ig,s) . j ; :: thesis:
defpred S₁[ Element of NAT ] means ( i < $1 & $1 <= j implies f . ((StepWhile>0 a,Ig,s) . $1) < f . ((StepWhile>0 a,Ig,s) . i) );
A12: S₁[ 0 ] ;
A13: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

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

per cases by A16, XXREAL_0:1;

suppose A17: i = k ; :: thesis:

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

end;

suppose A18: i < k ; :: thesis:

A19: k < j by A15, NAT_1:13;

assume ((StepWhile>0 a,Ig,s) . k) . a <= 0 ; :: thesis:
then K <= k by A6;
hence contradiction by A9, A19, 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 A14, A15, A18, NAT_1:13, XXREAL_0:2; :: thesis:

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A12, A13);
hence contradiction by A9, A11; :: thesis:

end;

let i, j be Element of NAT ; :: thesis:
assume A21: ( i < j & i <= K & j <= K ) ; :: thesis:

per cases by A21, XXREAL_0:1;

suppose A22: 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, A22, SCMFSA6A:38;
hence contradiction by A6, A21, A22; :: thesis:

end;

suppose A23: j < K ; :: thesis:

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

let k be Element of NAT ; :: thesis:
assume that
A26: ( j + k <= K implies DataPart ((StepWhile>0 a,Ig,s) . (i + k)) = DataPart ((StepWhile>0 a,Ig,s) . (j + k)) ) and
A27: j + (k + 1) <= K ; :: thesis:
A28: ( j + k < (j + k) + 1 & (j + k) + 1 <= K ) by A27, XREAL_1:31;
then A29: j + k < K by XXREAL_0:2;
A30: ((StepWhile>0 a,Ig,s) . (j + k)) . (intloc 0 ) = 1 by A1, A2, Th39;
A31: ((StepWhile>0 a,Ig,s) . (j + k)) . a > 0 by A6, A29;
then A32: Ig is_closed_on (StepWhile>0 a,Ig,s) . (j + k) by A2, Def4;
then A33: Ig is_closed_on Initialize ((StepWhile>0 a,Ig,s) . (j + k)) by A30, Lm7;
A34: Ig is_halting_on (StepWhile>0 a,Ig,s) . (j + k) by A2, A31, Def4;
then A35: Ig is_halting_on Initialize ((StepWhile>0 a,Ig,s) . (j + k)) by A30, A32, Lm8;
A36: ((StepWhile>0 a,Ig,s) . (i + k)) . (intloc 0 ) = 1 by A1, A2, Th39;
A37: ((StepWhile>0 a,Ig,s) . (i + k)) . a > 0

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

end;

then A39: Ig is_closed_on (StepWhile>0 a,Ig,s) . (i + k) by A2, Def4;
then A40: Ig is_closed_on Initialize ((StepWhile>0 a,Ig,s) . (i + k)) by A36, Lm7;
Ig is_halting_on (StepWhile>0 a,Ig,s) . (i + k) by A2, A37, Def4;
then A41: Ig is_halting_on Initialize ((StepWhile>0 a,Ig,s) . (i + k)) by A36, A39, 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 A36, A37, A40, A41, Th38
.= DataPart (IExec Ig,((StepWhile>0 a,Ig,s) . (j + k))) by A26, A28, A30, A32, A34, SCMFSA8C:46, XXREAL_0:2
.= DataPart ((StepWhile>0 a,Ig,s) . ((j + k) + 1)) by A30, A31, A33, A35, Th38
.= DataPart ((StepWhile>0 a,Ig,s) . (j + (k + 1))) ; :: thesis:

end;

A42: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A24, A25);
consider p being Element of NAT such that
A43: K = j + p and
1 <= p by A23, FSM_1:1;
A44: DataPart ((StepWhile>0 a,Ig,s) . (i + p)) = DataPart ((StepWhile>0 a,Ig,s) . K) by A42, A43;
A45: i + p < K by A21, A43, XREAL_1:8;
((StepWhile>0 a,Ig,s) . (i + p)) . a <= 0 by A5, A44, SCMFSA6A:38;
hence contradiction by A6, A45; :: thesis:

end;

given i, j being Element of NAT such that A46: i <> j and
A47: i <= ExitsAtWhile>0 a,Ig,s and
A48: j <= ExitsAtWhile>0 a,Ig,s and
A49: ( (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 A46, XXREAL_0:1;
hence contradiction by A4, A8, A20, A47, A48, A49; :: thesis: