let p be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA
for a being read-write Int-Location
for Ig being good really-closed MacroInstruction of SCM+FSA st s . (intloc 0) = 1 & ProperBodyWhile>0 a,Ig,s,p & WithVariantWhile>0 a,Ig,s,p holds
for i, j being Nat st i <> j & i <= ExitsAtWhile>0 (a,Ig,p,s) & j <= ExitsAtWhile>0 (a,Ig,p,s) holds
( (StepWhile>0 (a,Ig,p,s)) . i <> (StepWhile>0 (a,Ig,p,s)) . j & DataPart ((StepWhile>0 (a,Ig,p,s)) . i) <> DataPart ((StepWhile>0 (a,Ig,p,s)) . j) )
let s be State of SCM+FSA; :: thesis: for a being read-write Int-Location
for Ig being good really-closed MacroInstruction of SCM+FSA st s . (intloc 0) = 1 & ProperBodyWhile>0 a,Ig,s,p & WithVariantWhile>0 a,Ig,s,p holds
for i, j being Nat st i <> j & i <= ExitsAtWhile>0 (a,Ig,p,s) & j <= ExitsAtWhile>0 (a,Ig,p,s) holds
( (StepWhile>0 (a,Ig,p,s)) . i <> (StepWhile>0 (a,Ig,p,s)) . j & DataPart ((StepWhile>0 (a,Ig,p,s)) . i) <> DataPart ((StepWhile>0 (a,Ig,p,s)) . j) )
let a be read-write Int-Location; :: thesis: for Ig being good really-closed MacroInstruction of SCM+FSA st s . (intloc 0) = 1 & ProperBodyWhile>0 a,Ig,s,p & WithVariantWhile>0 a,Ig,s,p holds
for i, j being Nat st i <> j & i <= ExitsAtWhile>0 (a,Ig,p,s) & j <= ExitsAtWhile>0 (a,Ig,p,s) holds
( (StepWhile>0 (a,Ig,p,s)) . i <> (StepWhile>0 (a,Ig,p,s)) . j & DataPart ((StepWhile>0 (a,Ig,p,s)) . i) <> DataPart ((StepWhile>0 (a,Ig,p,s)) . j) )
let Ig be good really-closed MacroInstruction of SCM+FSA ; :: thesis: ( s . (intloc 0) = 1 & ProperBodyWhile>0 a,Ig,s,p & WithVariantWhile>0 a,Ig,s,p implies for i, j being Nat st i <> j & i <= ExitsAtWhile>0 (a,Ig,p,s) & j <= ExitsAtWhile>0 (a,Ig,p,s) holds
( (StepWhile>0 (a,Ig,p,s)) . i <> (StepWhile>0 (a,Ig,p,s)) . j & DataPart ((StepWhile>0 (a,Ig,p,s)) . i) <> DataPart ((StepWhile>0 (a,Ig,p,s)) . j) ) )
set I = Ig;
assume that
A1: s . (intloc 0) = 1 and
A2: ProperBodyWhile>0 a,Ig,s,p and
A3: WithVariantWhile>0 a,Ig,s,p ; :: thesis: for i, j being Nat st i <> j & i <= ExitsAtWhile>0 (a,Ig,p,s) & j <= ExitsAtWhile>0 (a,Ig,p,s) holds
( (StepWhile>0 (a,Ig,p,s)) . i <> (StepWhile>0 (a,Ig,p,s)) . j & DataPart ((StepWhile>0 (a,Ig,p,s)) . i) <> DataPart ((StepWhile>0 (a,Ig,p,s)) . j) )
set SW = StepWhile>0 (a,Ig,p,s);
set PW = p +* (while>0 (a,Ig));
consider K being Nat such that
A4: ExitsAtWhile>0 (a,Ig,p,s) = K and
A5: ((StepWhile>0 (a,Ig,p,s)) . K) . a <= 0 and
A6: for i being Nat st ((StepWhile>0 (a,Ig,p,s)) . i) . a <= 0 holds
K <= i and
DataPart (Comput ((p +* (while>0 (a,Ig))),(Initialize s),(LifeSpan ((p +* (while>0 (a,Ig))),(s +* (Start-At (0,SCM+FSA))))))) = DataPart ((StepWhile>0 (a,Ig,p,s)) . K) by A2, A3, Def6;
consider f being Function of (product (the_Values_of SCM+FSA)),NAT such that
A7: for k being Nat holds
( f . ((StepWhile>0 (a,Ig,p,s)) . (k + 1)) < f . ((StepWhile>0 (a,Ig,p,s)) . k) or ((StepWhile>0 (a,Ig,p,s)) . k) . a <= 0 ) by A3;
A8: for i, j being Nat st i < j & i <= K & j <= K holds
DataPart ((StepWhile>0 (a,Ig,p,s)) . i) <> DataPart ((StepWhile>0 (a,Ig,p,s)) . j)
proof
let i, j be Nat; :: thesis: ( i < j & i <= K & j <= K implies DataPart ((StepWhile>0 (a,Ig,p,s)) . i) <> DataPart ((StepWhile>0 (a,Ig,p,s)) . j) )
assume that
A9: i < j and
i <= K and
A10: j <= K ; :: thesis: DataPart ((StepWhile>0 (a,Ig,p,s)) . i) <> DataPart ((StepWhile>0 (a,Ig,p,s)) . j)
per cases ( j = K or j < K ) by A10, XXREAL_0:1;
suppose A11: j = K ; :: thesis: DataPart ((StepWhile>0 (a,Ig,p,s)) . i) <> DataPart ((StepWhile>0 (a,Ig,p,s)) . j)
assume DataPart ((StepWhile>0 (a,Ig,p,s)) . i) = DataPart ((StepWhile>0 (a,Ig,p,s)) . j) ; :: thesis: contradiction
then ((StepWhile>0 (a,Ig,p,s)) . i) . a <= 0 by A5, A11, SCMFSA_M:2;
hence contradiction by A6, A9, A11; :: thesis: verum
end;
suppose A12: j < K ; :: thesis: DataPart ((StepWhile>0 (a,Ig,p,s)) . i) <> DataPart ((StepWhile>0 (a,Ig,p,s)) . j)
defpred S1[ Nat] means ( j + $1 <= K implies DataPart ((StepWhile>0 (a,Ig,p,s)) . (i + $1)) = DataPart ((StepWhile>0 (a,Ig,p,s)) . (j + $1)) );
A13: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume that
A14: ( j + k <= K implies DataPart ((StepWhile>0 (a,Ig,p,s)) . (i + k)) = DataPart ((StepWhile>0 (a,Ig,p,s)) . (j + k)) ) and
A15: j + (k + 1) <= K ; :: thesis: DataPart ((StepWhile>0 (a,Ig,p,s)) . (i + (k + 1))) = DataPart ((StepWhile>0 (a,Ig,p,s)) . (j + (k + 1)))
A16: ((StepWhile>0 (a,Ig,p,s)) . (j + k)) . (intloc 0) = 1 by A1, A2, Th33;
A17: j + k < (j + k) + 1 by XREAL_1:29;
then A18: j + k < K by A15, XXREAL_0:2;
then A19: ((StepWhile>0 (a,Ig,p,s)) . (j + k)) . a > 0 by A6;
A20: Ig is_halting_on (StepWhile>0 (a,Ig,p,s)) . (j + k),p +* (while>0 (a,Ig)) by A2, A19;
then A21: Ig is_halting_on Initialized ((StepWhile>0 (a,Ig,p,s)) . (j + k)),p +* (while>0 (a,Ig)) by A16, Lm7;
A22: ((StepWhile>0 (a,Ig,p,s)) . (i + k)) . (intloc 0) = 1 by A1, A2, Th33;
A23: ((StepWhile>0 (a,Ig,p,s)) . (i + k)) . a > 0
proof
assume not ((StepWhile>0 (a,Ig,p,s)) . (i + k)) . a > 0 ; :: thesis: contradiction
then A24: K <= i + k by A6;
i + k < j + k by A9, XREAL_1:6;
hence contradiction by A18, A24, XXREAL_0:2; :: thesis: verum
end;
Ig is_halting_on (StepWhile>0 (a,Ig,p,s)) . (i + k),p +* (while>0 (a,Ig)) by A2, A23;
then A25: Ig is_halting_on Initialized ((StepWhile>0 (a,Ig,p,s)) . (i + k)),p +* (while>0 (a,Ig)) by A22, Lm7;
thus DataPart ((StepWhile>0 (a,Ig,p,s)) . (i + (k + 1))) = DataPart ((StepWhile>0 (a,Ig,p,s)) . ((i + k) + 1))
.= DataPart (IExec (Ig,(p +* (while>0 (a,Ig))),((StepWhile>0 (a,Ig,p,s)) . (i + k)))) by A22, A23, A25, Th32
.= DataPart (IExec (Ig,(p +* (while>0 (a,Ig))),((StepWhile>0 (a,Ig,p,s)) . (j + k)))) by A14, A15, A17, A16, A20, SCMFSA8C:20, XXREAL_0:2
.= DataPart ((StepWhile>0 (a,Ig,p,s)) . ((j + k) + 1)) by A16, A19, A21, Th32
.= DataPart ((StepWhile>0 (a,Ig,p,s)) . (j + (k + 1))) ; :: thesis: verum
end;
consider p being Element of NAT such that
A26: K = j + p and
1 <= p by A12, FINSEQ_4:84;
assume DataPart ((StepWhile>0 (a,Ig,p,s)) . i) = DataPart ((StepWhile>0 (a,Ig,p,s)) . j) ; :: thesis: contradiction
then A27: S1[ 0 ] ;
for k being Nat holds S1[k] from NAT_1:sch 2(A27, A13);
then DataPart ((StepWhile>0 (a,Ig,p,s)) . (i + p)) = DataPart ((StepWhile>0 (a,Ig,p,s)) . K) by A26;
then A28: ((StepWhile>0 (a,Ig,p,s)) . (i + p)) . a <= 0 by A5, SCMFSA_M:2;
i + p < K by A9, A26, XREAL_1:6;
hence contradiction by A6, A28; :: thesis: verum
end;
end;
end;
A29: for i, j being Nat st i < j & i <= K & j <= K holds
(StepWhile>0 (a,Ig,p,s)) . i <> (StepWhile>0 (a,Ig,p,s)) . j
proof
let i, j be Nat; :: thesis: ( i < j & i <= K & j <= K implies (StepWhile>0 (a,Ig,p,s)) . i <> (StepWhile>0 (a,Ig,p,s)) . j )
assume that
A30: i < j and
i <= K and
A31: j <= K ; :: thesis: (StepWhile>0 (a,Ig,p,s)) . i <> (StepWhile>0 (a,Ig,p,s)) . j
defpred S1[ Nat] means ( i < $1 & $1 <= j implies f . ((StepWhile>0 (a,Ig,p,s)) . $1) < f . ((StepWhile>0 (a,Ig,p,s)) . i) );
A32: i < K by A30, A31, XXREAL_0:2;
A33: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume that
A34: ( i < k & k <= j implies f . ((StepWhile>0 (a,Ig,p,s)) . k) < f . ((StepWhile>0 (a,Ig,p,s)) . i) ) and
A35: i < k + 1 and
A36: k + 1 <= j ; :: thesis: f . ((StepWhile>0 (a,Ig,p,s)) . (k + 1)) < f . ((StepWhile>0 (a,Ig,p,s)) . i)
A37: i <= k by A35, NAT_1:13;
per cases ( i = k or i < k ) by A37, XXREAL_0:1;
suppose A38: i = k ; :: thesis: f . ((StepWhile>0 (a,Ig,p,s)) . (k + 1)) < f . ((StepWhile>0 (a,Ig,p,s)) . i)
not ((StepWhile>0 (a,Ig,p,s)) . i) . a <= 0 by A6, A32;
hence f . ((StepWhile>0 (a,Ig,p,s)) . (k + 1)) < f . ((StepWhile>0 (a,Ig,p,s)) . i) by A7, A38; :: thesis: verum
end;
suppose A39: i < k ; :: thesis: f . ((StepWhile>0 (a,Ig,p,s)) . (k + 1)) < f . ((StepWhile>0 (a,Ig,p,s)) . i)
A40: k < j by A36, NAT_1:13;
now :: thesis: not ((StepWhile>0 (a,Ig,p,s)) . k) . a <= 0
assume ((StepWhile>0 (a,Ig,p,s)) . k) . a <= 0 ; :: thesis: contradiction
then K <= k by A6;
hence contradiction by A31, A40, XXREAL_0:2; :: thesis: verum
end;
then f . ((StepWhile>0 (a,Ig,p,s)) . (k + 1)) < f . ((StepWhile>0 (a,Ig,p,s)) . k) by A7;
hence f . ((StepWhile>0 (a,Ig,p,s)) . (k + 1)) < f . ((StepWhile>0 (a,Ig,p,s)) . i) by A34, A36, A39, NAT_1:13, XXREAL_0:2; :: thesis: verum
end;
end;
end;
assume A41: (StepWhile>0 (a,Ig,p,s)) . i = (StepWhile>0 (a,Ig,p,s)) . j ; :: thesis: contradiction
A42: S1[ 0 ] ;
for k being Nat holds S1[k] from NAT_1:sch 2(A42, A33);
 hence contradiction by A30, A41; :: thesis: verum
end;
given i, j being Nat such that A43: i <> j and
A44: ( i <= ExitsAtWhile>0 (a,Ig,p,s) & j <= ExitsAtWhile>0 (a,Ig,p,s) & ( (StepWhile>0 (a,Ig,p,s)) . i = (StepWhile>0 (a,Ig,p,s)) . j or DataPart ((StepWhile>0 (a,Ig,p,s)) . i) = DataPart ((StepWhile>0 (a,Ig,p,s)) . j) ) ) ; :: thesis: contradiction
( i < j or j < i ) by A43, XXREAL_0:1;
hence contradiction by A4, A29, A8, A44; :: thesis: verum