let x, y be object ; :: thesis: for E being non empty set
for u being Element of E ^omega
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 st P . 1 = [x,u] & P . (len P) = [y,(<%> E)] holds
len P <= (len u) + 1
let E be non empty set ; :: thesis: for u being Element of E ^omega
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 st P . 1 = [x,u] & P . (len P) = [y,(<%> E)] holds
len P <= (len u) + 1
let u be Element of E ^omega ; :: thesis: 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 st P . 1 = [x,u] & P . (len P) = [y,(<%> E)] holds
len P <= (len u) + 1
let F be Subset of (E ^omega); :: thesis: 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 st P . 1 = [x,u] & P . (len P) = [y,(<%> E)] holds
len P <= (len u) + 1
let TS be non empty transition-system over F; :: thesis: ( not <%> E in rng (dom the Tran of TS) implies for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,(<%> E)] holds
len P <= (len u) + 1 )
defpred S₁[ Nat] means for P being RedSequence of ==>.-relation TS
for u being Element of E ^omega
for x being object st len u = $1 & P . 1 = [x,u] & P . (len P) = [y,(<%> E)] holds
len P <= (len u) + 1;
assume A1: not <%> E in rng (dom the Tran of TS) ; :: thesis: for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,(<%> E)] holds
len P <= (len u) + 1

A2: now :: thesis: for k being Nat st ( for n being Nat st n < k holds
S₁[n] ) holds
S₁[k]

let k be Nat; :: thesis: ( ( for n being Nat st n < k holds
S₁[n] ) implies S₁[k] )
assume A3: for n being Nat st n < k holds
S₁[n] ; :: thesis: S₁[k]

now :: thesis: for P being RedSequence of ==>.-relation TS
for u being Element of E ^omega
for x being object st len u = k & P . 1 = [x,u] & P . (len P) = [y,(<%> E)] holds
len P <= (len u) + 1

let P be RedSequence of ==>.-relation TS; :: thesis: for u being Element of E ^omega
for x being object st len u = k & P . 1 = [x,u] & P . (len P) = [y,(<%> E)] holds
len b₃ <= (len b₄) + 1
let u be Element of E ^omega ; :: thesis: for x being object st len u = k & P . 1 = [x,u] & P . (len P) = [y,(<%> E)] holds
len b₂ <= (len b₃) + 1
let x be object ; :: thesis: ( len u = k & P . 1 = [x,u] & P . (len P) = [y,(<%> E)] implies len b₁ <= (len b₂) + 1 )
assume that
A4: len u = k and
A5: P . 1 = [x,u] and
A6: P . (len P) = [y,(<%> E)] ; :: thesis: len b₁ <= (len b₂) + 1

per cases ( len u < 1 or len u >= 1 ) ;

suppose len u < 1 ; :: thesis: len b₁ <= (len b₂) + 1

then u = <%> E by NAT_1:25;
then len P = 1 by A1, A5, A6, Th60;
hence len P <= (len u) + 1 by NAT_1:25; :: thesis: verum

end;

suppose A7: len u >= 1 ; :: thesis: len b₁ <= (len b₂) + 1

A8: len P <> 1

proof

assume len P = 1 ; :: thesis: contradiction
then u = <%> E by A5, A6, XTUPLE_0:1;
hence contradiction by A7; :: thesis: verum

end;

then consider P9 being RedSequence of ==>.-relation TS such that
A9: <*(P . 1)*> ^ P9 = P and
A10: (len P9) + 1 = len P by Th5, NAT_1:25;
A11: len P > 1 by A8, NAT_1:25;
then len P >= 1 + 1 by NAT_1:13;
then A12: 1 + 1 in dom P by FINSEQ_3:25;
A13: 1 in dom P by A11, FINSEQ_3:25;
then A14: P . (1 + 1) = [((P . (1 + 1)) `1),((P . (1 + 1)) `2)] by A12, Th48;
then A15: [[x,u],[((P . (1 + 1)) `1),((P . (1 + 1)) `2)]] in ==>.-relation TS by A5, A13, A12, REWRITE1:def 2;
then reconsider u1 = (P . (1 + 1)) `2 as Element of E ^omega by Th32;
A16: ( len <*(P . 1)*> = 1 & len P9 >= 1 ) by FINSEQ_1:39, NAT_1:25;
then A17: P9 . 1 = [((P . (1 + 1)) `1),u1] by A9, A14, FINSEQ_1:65;
x,u ==>. (P . (1 + 1)) `1 ,u1,TS by A15, Def4;
then consider v being Element of E ^omega such that
A18: ( x,v -->. (P . (1 + 1)) `1 ,TS & u = v ^ u1 ) ;
( v <> <%> E & len u = (len u1) + (len v) ) by A1, A18, Th15, AFINSQ_1:17;
then A19: (len u) - 0 > ((len u1) + (len v)) - (len v) by XREAL_1:15;
then A20: (len u1) + 1 <= len u by NAT_1:13;
P9 . (len P9) = [y,(<%> E)] by A6, A9, A10, A16, FINSEQ_1:65;
then len P9 <= (len u1) + 1 by A3, A4, A19, A17;
then len P9 <= len u by A20, XXREAL_0:2;
hence len P <= (len u) + 1 by A10, XREAL_1:6; :: thesis: verum

end;

end;

end;

hence S₁[k] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 4(A2);
hence for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,(<%> E)] holds
len P <= (len u) + 1 ; :: thesis: verum