let G be _Graph; :: thesis: for W being Walk of G holds

( W is Trail-like iff for m, n being even Element of NAT st 1 <= m & m < n & n <= len W holds

W . m <> W . n )

let W be Walk of G; :: thesis: ( W is Trail-like iff for m, n being even Element of NAT st 1 <= m & m < n & n <= len W holds

W . m <> W . n )

W . m <> W . n ; :: thesis: W is Trail-like

hence W is Trail-like ; :: thesis: verum

( W is Trail-like iff for m, n being even Element of NAT st 1 <= m & m < n & n <= len W holds

W . m <> W . n )

let W be Walk of G; :: thesis: ( W is Trail-like iff for m, n being even Element of NAT st 1 <= m & m < n & n <= len W holds

W . m <> W . n )

hereby :: thesis: ( ( for m, n being even Element of NAT st 1 <= m & m < n & n <= len W holds

W . m <> W . n ) implies W is Trail-like )

assume A13:
for m, n being even Element of NAT st 1 <= m & m < n & n <= len W holds W . m <> W . n ) implies W is Trail-like )

assume
W is Trail-like
; :: thesis: for m, n being even Element of NAT st 1 <= m & m < n & n <= len W holds

W . m <> W . n

then A1: W .edgeSeq() is one-to-one ;

let m, n be even Element of NAT ; :: thesis: ( 1 <= m & m < n & n <= len W implies W . m <> W . n )

assume that

A2: 1 <= m and

A3: m < n and

A4: n <= len W ; :: thesis: W . m <> W . n

A5: 1 <= n by A2, A3, XXREAL_0:2;

then A6: n div 2 in dom (W .edgeSeq()) by A4, Lm40;

A7: m <= len W by A3, A4, XXREAL_0:2;

then A8: W . m = (W .edgeSeq()) . (m div 2) by A2, Lm40;

m div 2 in dom (W .edgeSeq()) by A2, A7, Lm40;

hence W . m <> W . n by A1, A8, A6, A12, A9, FUNCT_1:def 4; :: thesis: verum

end;W . m <> W . n

then A1: W .edgeSeq() is one-to-one ;

let m, n be even Element of NAT ; :: thesis: ( 1 <= m & m < n & n <= len W implies W . m <> W . n )

assume that

A2: 1 <= m and

A3: m < n and

A4: n <= len W ; :: thesis: W . m <> W . n

A5: 1 <= n by A2, A3, XXREAL_0:2;

then A6: n div 2 in dom (W .edgeSeq()) by A4, Lm40;

A7: m <= len W by A3, A4, XXREAL_0:2;

then A8: W . m = (W .edgeSeq()) . (m div 2) by A2, Lm40;

A9: now :: thesis: not m div 2 = n div 2

A12:
W . n = (W .edgeSeq()) . (n div 2)
by A4, A5, Lm40;
2 divides m
by PEPIN:22;

then A10: 2 * (m div 2) = m by NAT_D:3;

A11: 2 divides n by PEPIN:22;

assume m div 2 = n div 2 ; :: thesis: contradiction

hence contradiction by A3, A11, A10, NAT_D:3; :: thesis: verum

end;then A10: 2 * (m div 2) = m by NAT_D:3;

A11: 2 divides n by PEPIN:22;

assume m div 2 = n div 2 ; :: thesis: contradiction

hence contradiction by A3, A11, A10, NAT_D:3; :: thesis: verum

m div 2 in dom (W .edgeSeq()) by A2, A7, Lm40;

hence W . m <> W . n by A1, A8, A6, A12, A9, FUNCT_1:def 4; :: thesis: verum

W . m <> W . n ; :: thesis: W is Trail-like

now :: thesis: for x1, x2 being object st x1 in dom (W .edgeSeq()) & x2 in dom (W .edgeSeq()) & (W .edgeSeq()) . x1 = (W .edgeSeq()) . x2 holds

x1 = x2

then
W .edgeSeq() is one-to-one
by FUNCT_1:def 4;x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom (W .edgeSeq()) & x2 in dom (W .edgeSeq()) & (W .edgeSeq()) . x1 = (W .edgeSeq()) . x2 implies x1 = x2 )

assume that

A14: x1 in dom (W .edgeSeq()) and

A15: x2 in dom (W .edgeSeq()) and

A16: (W .edgeSeq()) . x1 = (W .edgeSeq()) . x2 ; :: thesis: x1 = x2

reconsider m = x1, n = x2 as Element of NAT by A14, A15;

A17: m <= len (W .edgeSeq()) by A14, FINSEQ_3:25;

1 <= m by A14, FINSEQ_3:25;

then A18: (W .edgeSeq()) . x1 = W . (2 * m) by A17, Def15;

A19: n <= len (W .edgeSeq()) by A15, FINSEQ_3:25;

1 <= n by A15, FINSEQ_3:25;

then A20: W . (2 * m) = W . (2 * n) by A16, A18, A19, Def15;

A21: 2 * n in dom W by A15, Lm41;

then A22: 1 <= 2 * n by FINSEQ_3:25;

A23: 2 * m in dom W by A14, Lm41;

then A24: 2 * m <= len W by FINSEQ_3:25;

A25: 2 * n <= len W by A21, FINSEQ_3:25;

A26: 1 <= 2 * m by A23, FINSEQ_3:25;

end;assume that

A14: x1 in dom (W .edgeSeq()) and

A15: x2 in dom (W .edgeSeq()) and

A16: (W .edgeSeq()) . x1 = (W .edgeSeq()) . x2 ; :: thesis: x1 = x2

reconsider m = x1, n = x2 as Element of NAT by A14, A15;

A17: m <= len (W .edgeSeq()) by A14, FINSEQ_3:25;

1 <= m by A14, FINSEQ_3:25;

then A18: (W .edgeSeq()) . x1 = W . (2 * m) by A17, Def15;

A19: n <= len (W .edgeSeq()) by A15, FINSEQ_3:25;

1 <= n by A15, FINSEQ_3:25;

then A20: W . (2 * m) = W . (2 * n) by A16, A18, A19, Def15;

A21: 2 * n in dom W by A15, Lm41;

then A22: 1 <= 2 * n by FINSEQ_3:25;

A23: 2 * m in dom W by A14, Lm41;

then A24: 2 * m <= len W by FINSEQ_3:25;

A25: 2 * n <= len W by A21, FINSEQ_3:25;

A26: 1 <= 2 * m by A23, FINSEQ_3:25;

now :: thesis: x1 = x2end;

hence
x1 = x2
; :: thesis: verumhence W is Trail-like ; :: thesis: verum