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 )
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 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;
A9: now :: thesis: not m div 2 = n div 2
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;
A12: W . n = (W .edgeSeq()) . (n div 2) by A4, A5, 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;
assume A13: for m, n being even Element of NAT st 1 <= m & m < n & n <= len W holds
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
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;
now :: thesis: x1 = x2
per cases ( 2 * m < 2 * n or 2 * m = 2 * n or 2 * m > 2 * n ) by XXREAL_0:1;
suppose 2 * m < 2 * n ; :: thesis: x1 = x2
hence x1 = x2 by A13, A20, A26, A25; :: thesis: verum
end;
suppose 2 * m = 2 * n ; :: thesis: x1 = x2
hence x1 = x2 ; :: thesis: verum
end;
suppose 2 * m > 2 * n ; :: thesis: x1 = x2
hence x1 = x2 by A13, A20, A24, A22; :: thesis: verum
end;
end;
end;
hence x1 = x2 ; :: thesis: verum
end;
then W .edgeSeq() is one-to-one by FUNCT_1:def 4;
hence W is Trail-like ; :: thesis: verum