let E be non empty set ; :: thesis: for u being Element of E ^omega

for TS being non empty transition-system over (Lex E) \/ {(<%> E)}

for R being RedSequence of ==>.-relation TS st (R . 1) `2 = u & (R . (len R)) `2 = <%> E holds

len R > len u

let u be Element of E ^omega ; :: thesis: for TS being non empty transition-system over (Lex E) \/ {(<%> E)}

for R being RedSequence of ==>.-relation TS st (R . 1) `2 = u & (R . (len R)) `2 = <%> E holds

len R > len u

let TS be non empty transition-system over (Lex E) \/ {(<%> E)}; :: thesis: for R being RedSequence of ==>.-relation TS st (R . 1) `2 = u & (R . (len R)) `2 = <%> E holds

len R > len u

defpred S_{1}[ Nat] means for R being RedSequence of ==>.-relation TS

for u being Element of E ^omega st len R = $1 & (R . 1) `2 = u & (R . (len R)) `2 = <%> E holds

len R > len u;

_{1}[ 0 ]
;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A14, A1);

hence for R being RedSequence of ==>.-relation TS st (R . 1) `2 = u & (R . (len R)) `2 = <%> E holds

len R > len u ; :: thesis: verum

for TS being non empty transition-system over (Lex E) \/ {(<%> E)}

for R being RedSequence of ==>.-relation TS st (R . 1) `2 = u & (R . (len R)) `2 = <%> E holds

len R > len u

let u be Element of E ^omega ; :: thesis: for TS being non empty transition-system over (Lex E) \/ {(<%> E)}

for R being RedSequence of ==>.-relation TS st (R . 1) `2 = u & (R . (len R)) `2 = <%> E holds

len R > len u

let TS be non empty transition-system over (Lex E) \/ {(<%> E)}; :: thesis: for R being RedSequence of ==>.-relation TS st (R . 1) `2 = u & (R . (len R)) `2 = <%> E holds

len R > len u

defpred S

for u being Element of E ^omega st len R = $1 & (R . 1) `2 = u & (R . (len R)) `2 = <%> E holds

len R > len u;

A1: now :: thesis: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

A14:
SS

let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A2: S_{1}[k]
; :: thesis: S_{1}[k + 1]

_{1}[k + 1]
; :: thesis: verum

end;assume A2: S

now :: thesis: for R being RedSequence of ==>.-relation TS

for u being Element of E ^omega st len R = k + 1 & (R . 1) `2 = u & (R . (len R)) `2 = <%> E holds

len R > len u

hence
Sfor u being Element of E ^omega st len R = k + 1 & (R . 1) `2 = u & (R . (len R)) `2 = <%> E holds

len R > len u

let R be RedSequence of ==>.-relation TS; :: thesis: for u being Element of E ^omega st len R = k + 1 & (R . 1) `2 = u & (R . (len R)) `2 = <%> E holds

len b_{2} > len b_{3}

let u be Element of E ^omega ; :: thesis: ( len R = k + 1 & (R . 1) `2 = u & (R . (len R)) `2 = <%> E implies len b_{1} > len b_{2} )

assume that

A3: len R = k + 1 and

A4: (R . 1) `2 = u and

A5: (R . (len R)) `2 = <%> E ; :: thesis: len b_{1} > len b_{2}

end;len b

let u be Element of E ^omega ; :: thesis: ( len R = k + 1 & (R . 1) `2 = u & (R . (len R)) `2 = <%> E implies len b

assume that

A3: len R = k + 1 and

A4: (R . 1) `2 = u and

A5: (R . (len R)) `2 = <%> E ; :: thesis: len b

per cases
( len u = 0 or len u > 0 )
;

end;

suppose A6:
len u > 0
; :: thesis: len b_{1} > len b_{2}

then consider e being Element of E, u1 being Element of E ^omega such that

A7: u = <%e%> ^ u1 by Th7;

len R <> 1 by A4, A5, A6;

then consider R9 being RedSequence of ==>.-relation TS such that

A8: <*(R . 1)*> ^ R9 = R and

A9: (len R9) + 1 = len R by NAT_1:25, REWRITE3:5;

A10: (len R9) + 0 < k + 1 by A3, A9, XREAL_1:6;

A11: len R9 >= 0 + 1 by NAT_1:8;

then len R9 in dom R9 by FINSEQ_3:25;

then A12: (R9 . (len R9)) `2 = <%> E by A5, A8, A9, REWRITE3:1;

1 in dom R9 by A11, FINSEQ_3:25;

then A13: (<*(R . 1)*> ^ R9) . (1 + 1) = R9 . 1 by REWRITE3:1;

end;A7: u = <%e%> ^ u1 by Th7;

len R <> 1 by A4, A5, A6;

then consider R9 being RedSequence of ==>.-relation TS such that

A8: <*(R . 1)*> ^ R9 = R and

A9: (len R9) + 1 = len R by NAT_1:25, REWRITE3:5;

A10: (len R9) + 0 < k + 1 by A3, A9, XREAL_1:6;

A11: len R9 >= 0 + 1 by NAT_1:8;

then len R9 in dom R9 by FINSEQ_3:25;

then A12: (R9 . (len R9)) `2 = <%> E by A5, A8, A9, REWRITE3:1;

1 in dom R9 by A11, FINSEQ_3:25;

then A13: (<*(R . 1)*> ^ R9) . (1 + 1) = R9 . 1 by REWRITE3:1;

for k being Nat holds S

hence for R being RedSequence of ==>.-relation TS st (R . 1) `2 = u & (R . (len R)) `2 = <%> E holds

len R > len u ; :: thesis: verum