let G be simple _Graph; :: thesis: for W1, W2 being Walk of G
for k being odd Nat st k <= len W1 & k <= len W2 & ( for j being odd Nat st j <= k holds
W1 . j = W2 . j ) holds
for j being Nat st 1 <= j & j <= k holds
W1 . j = W2 . j
let W1, W2 be Walk of G; :: thesis: for k being odd Nat st k <= len W1 & k <= len W2 & ( for j being odd Nat st j <= k holds
W1 . j = W2 . j ) holds
for j being Nat st 1 <= j & j <= k holds
W1 . j = W2 . j
let k be odd Nat; :: thesis: ( k <= len W1 & k <= len W2 & ( for j being odd Nat st j <= k holds
W1 . j = W2 . j ) implies for j being Nat st 1 <= j & j <= k holds
W1 . j = W2 . j )
assume that
A1: k <= len W1 and
A2: k <= len W2 and
A3: for j being odd Nat st j <= k holds
W1 . j = W2 . j ; :: thesis: for j being Nat st 1 <= j & j <= k holds
W1 . j = W2 . j
let j be Nat; :: thesis: ( 1 <= j & j <= k implies W1 . j = W2 . j )
assume that
A4: 1 <= j and
A5: j <= k ; :: thesis: W1 . j = W2 . j
per cases ( j is odd or j is even ) ;
suppose j is odd ; :: thesis: W1 . j = W2 . j
hence W1 . j = W2 . j by A3, A5; :: thesis: verum
end;
suppose j is even ; :: thesis: W1 . j = W2 . j
then reconsider j9 = j as even Nat ;
1 - 1 <= j - 1 by A4, XREAL_1:9;
then reconsider j1 = j9 - 1 as odd Element of NAT by INT_1:3;
A6: j1 < j by XREAL_1:44;
j <= len W1 by A1, A5, XXREAL_0:2;
then j1 < len W1 by A6, XXREAL_0:2;
then A7: W1 . (j1 + 1) Joins W1 . j1,W1 . (j1 + 2),G by GLIB_001:def 3;
j1 + 1 < k by A5, XXREAL_0:1;
then (j1 + 1) + 1 <= k by NAT_1:13;
then A8: W1 . (j1 + 2) = W2 . (j1 + 2) by A3;
j <= len W2 by A2, A5, XXREAL_0:2;
then j1 < len W2 by A6, XXREAL_0:2;
then A9: W2 . (j1 + 1) Joins W2 . j1,W2 . (j1 + 2),G by GLIB_001:def 3;
W1 . j1 = W2 . j1 by A3, A5, A6, XXREAL_0:2;
hence W1 . j = W2 . j by A7, A9, A8, GLIB_000:def 20; :: thesis: verum
end;
end;