let E be non empty set ; for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS
for k, l being Nat st k in dom P & l in dom P & k < l holds
(P . k) `2 <> (P . l) `2
let F be Subset of (E ^omega); for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS
for k, l being Nat st k in dom P & l in dom P & k < l holds
(P . k) `2 <> (P . l) `2
let TS be non empty transition-system over F; ( not <%> E in rng (dom the Tran of TS) implies for P being RedSequence of ==>.-relation TS
for k, l being Nat st k in dom P & l in dom P & k < l holds
(P . k) `2 <> (P . l) `2 )
defpred S1[ Nat] means for P being RedSequence of ==>.-relation TS
for k, l being Nat st len P = $1 & k in dom P & l in dom P & k < l holds
(P . k) `2 <> (P . l) `2 ;
assume A1:
not <%> E in rng (dom the Tran of TS)
; for P being RedSequence of ==>.-relation TS
for k, l being Nat st k in dom P & l in dom P & k < l holds
(P . k) `2 <> (P . l) `2
A2:
now for i being Nat st S1[i] holds
S1[i + 1]let i be
Nat;
( S1[i] implies S1[i + 1] )assume A3:
S1[
i]
;
S1[i + 1]now for P being RedSequence of ==>.-relation TS
for k, l being Nat st len P = i + 1 & k in dom P & l in dom P & k < l holds
(P . k) `2 <> (P . l) `2 let P be
RedSequence of
==>.-relation TS;
for k, l being Nat st len P = i + 1 & k in dom P & l in dom P & k < l holds
(b3 . b4) `2 <> (b3 . b5) `2 let k,
l be
Nat;
( len P = i + 1 & k in dom P & l in dom P & k < l implies (b1 . b2) `2 <> (b1 . b3) `2 )assume that A4:
len P = i + 1
and A5:
k in dom P
and A6:
l in dom P
and A7:
k < l
;
(b1 . b2) `2 <> (b1 . b3) `2 A8:
i < len P
by A4, NAT_1:13;
A9:
k <= len P
by A5, FINSEQ_3:25;
A10:
1
<= k
by A5, FINSEQ_3:25;
A11:
1
<= l
by A6, FINSEQ_3:25;
A12:
l <= len P
by A6, FINSEQ_3:25;
per cases
( ( k = 1 & l = len P ) or ( k <> 1 & l = len P ) or l <> len P )
;
suppose A13:
(
k <> 1 &
l = len P )
;
(b1 . b2) `2 <> (b1 . b3) `2 reconsider k1 =
k - 1 as
Nat by A10, NAT_1:21;
A14:
k > 1
by A10, A13, XXREAL_0:1;
then
k1 > 1
- 1
by XREAL_1:9;
then A15:
k1 >= 0 + 1
by NAT_1:13;
reconsider l1 =
l - 1 as
Nat by A11, NAT_1:21;
A16:
k1 < l1
by A7, XREAL_1:9;
A17:
l > 1
by A7, A10, A11, XXREAL_0:1;
then consider Q being
RedSequence of
==>.-relation TS such that A18:
<*(P . 1)*> ^ Q = P
and A19:
(len Q) + 1
= len P
by A13, Th5;
l1 > 1
- 1
by A17, XREAL_1:9;
then A20:
l1 >= 0 + 1
by NAT_1:13;
k1 <= ((len Q) + 1) - 1
by A9, A19, XREAL_1:9;
then A21:
k1 in dom Q
by A15, FINSEQ_3:25;
A22:
len <*(P . 1)*> = 1
by FINSEQ_1:40;
then A23:
P . l = Q . l1
by A12, A17, A18, FINSEQ_1:24;
l1 <= ((len Q) + 1) - 1
by A12, A19, XREAL_1:9;
then A24:
l1 in dom Q
by A20, FINSEQ_3:25;
P . k = Q . k1
by A9, A14, A18, A22, FINSEQ_1:24;
hence
(P . k) `2 <> (P . l) `2
by A3, A4, A19, A21, A24, A16, A23;
verum end; suppose A25:
l <> len P
;
(b1 . b2) `2 <> (b1 . b3) `2
k < i + 1
by A4, A7, A12, XXREAL_0:2;
then A26:
k <= i
by NAT_1:13;
then reconsider Q =
P | i as
RedSequence of
==>.-relation TS by A10, REWRITE2:3, XXREAL_0:2;
A27:
P . k = Q . k
by A26, FINSEQ_3:112;
l < i + 1
by A4, A12, A25, XXREAL_0:1;
then A28:
l <= i
by NAT_1:13;
then A29:
P . l = Q . l
by FINSEQ_3:112;
k <= len Q
by A8, A26, FINSEQ_1:59;
then A30:
k in dom Q
by A10, FINSEQ_3:25;
l <= len Q
by A8, A28, FINSEQ_1:59;
then A31:
l in dom Q
by A11, FINSEQ_3:25;
len Q = i
by A8, FINSEQ_1:59;
hence
(P . k) `2 <> (P . l) `2
by A3, A7, A30, A31, A27, A29;
verum end; end; hence
S1[
i + 1]
;
verum end;
A32:
S1[ 0 ]
;
A33:
for i being Nat holds S1[i]
from NAT_1:sch 2(A32, A2);
let P be RedSequence of ==>.-relation TS; for k, l being Nat st k in dom P & l in dom P & k < l holds
(P . k) `2 <> (P . l) `2
let k, l be Nat; ( k in dom P & l in dom P & k < l implies (P . k) `2 <> (P . l) `2 )
assume A34:
( k in dom P & l in dom P & k < l )
; (P . k) `2 <> (P . l) `2
len P = len P
;
hence
(P . k) `2 <> (P . l) `2
by A33, A34; verum