let G be _Graph; :: thesis: for W1, W2 being Walk of G st W1 .first() = W2 .first() holds
len (maxPrefix (W1,W2)) is odd
let W1, W2 be Walk of G; :: thesis: ( W1 .first() = W2 .first() implies len (maxPrefix (W1,W2)) is odd )
assume that
A1: W1 .first() = W2 .first() and
A2: len (maxPrefix (W1,W2)) is even ; :: thesis: contradiction
set dI = len (maxPrefix (W1,W2));
reconsider dIp = (len (maxPrefix (W1,W2))) - 1 as odd Element of NAT by A1, A2, Th5, INT_1:5;
A3: dIp < len (maxPrefix (W1,W2)) by XREAL_1:146;
set mP = maxPrefix (W1,W2);
set lmP = (maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>;
A4: len ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) = (len (maxPrefix (W1,W2))) + 1 by FINSEQ_2:16;
A5: now :: thesis: for x being object st x in dom ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) holds
((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) . x = W1 . x
let x be object ; :: thesis: ( x in dom ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) implies ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) . b1 = W1 . b1 )
assume A6: x in dom ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) ; :: thesis: ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) . b1 = W1 . b1
reconsider n = x as Nat by A6;
A7: 1 <= n by A6, FINSEQ_3:25;
n <= len ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) by A6, FINSEQ_3:25;
then A8: n <= (len (maxPrefix (W1,W2))) + 1 by FINSEQ_2:16;
per cases ( n <= len (maxPrefix (W1,W2)) or n = (len (maxPrefix (W1,W2))) + 1 ) by A8, NAT_1:8;
suppose A9: n <= len (maxPrefix (W1,W2)) ; :: thesis: ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) . b1 = W1 . b1
then n in dom (maxPrefix (W1,W2)) by A7, FINSEQ_3:25;
hence ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) . x = (maxPrefix (W1,W2)) . x by FINSEQ_1:def 7
.= W1 . x by A9, Th6 ;
:: thesis: verum
end;
suppose n = (len (maxPrefix (W1,W2))) + 1 ; :: thesis: ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) . b1 = W1 . b1
hence ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) . x = W1 . x by FINSEQ_1:42; :: thesis: verum
end;
end;
end;
A10: len (maxPrefix (W1,W2)) = dIp + 1 ;
A11: len (maxPrefix (W1,W2)) <= len W2 by Th3;
then dIp < len W2 by XREAL_1:146, XXREAL_0:2;
then A12: W2 . (len (maxPrefix (W1,W2))) Joins W2 . dIp,W2 . (dIp + 2),G by A10, GLIB_001:def 3;
A13: len (maxPrefix (W1,W2)) <= len W1 by Th3;
then dIp < len W1 by XREAL_1:146, XXREAL_0:2;
then A14: W1 . (len (maxPrefix (W1,W2))) Joins W1 . dIp,W1 . (dIp + 2),G by A10, GLIB_001:def 3;
W1 . (len (maxPrefix (W1,W2))) = W2 . (len (maxPrefix (W1,W2))) by Th7;
then A15: ( ( W1 . dIp = W2 . dIp & W1 . (dIp + 2) = W2 . (dIp + 2) ) or ( W1 . dIp = W2 . (dIp + 2) & W1 . (dIp + 2) = W2 . dIp ) ) by A14, A12, GLIB_000:15;
A16: now :: thesis: for x being object st x in dom ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) holds
((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) . x = W2 . x
let x be object ; :: thesis: ( x in dom ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) implies ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) . b1 = W2 . b1 )
assume A17: x in dom ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) ; :: thesis: ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) . b1 = W2 . b1
reconsider n = x as Nat by A17;
A18: 1 <= n by A17, FINSEQ_3:25;
n <= len ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) by A17, FINSEQ_3:25;
then A19: n <= (len (maxPrefix (W1,W2))) + 1 by FINSEQ_2:16;
per cases ( n <= len (maxPrefix (W1,W2)) or n = (len (maxPrefix (W1,W2))) + 1 ) by A19, NAT_1:8;
suppose A20: n <= len (maxPrefix (W1,W2)) ; :: thesis: ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) . b1 = W2 . b1
then n in dom (maxPrefix (W1,W2)) by A18, FINSEQ_3:25;
hence ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) . x = (maxPrefix (W1,W2)) . x by FINSEQ_1:def 7
.= W2 . x by A20, Th6 ;
:: thesis: verum
end;
suppose A21: n = (len (maxPrefix (W1,W2))) + 1 ; :: thesis: ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) . b1 = W2 . b1
hence ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) . x = W1 . ((len (maxPrefix (W1,W2))) + 1) by FINSEQ_1:42
.= W2 . x by A3, A15, A21, Th7 ;
:: thesis: verum
end;
end;
end;
len (maxPrefix (W1,W2)) < len W2 by A2, A11, XXREAL_0:1;
then len ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) <= len W2 by A4, NAT_1:13;
then dom ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) c= dom W2 by FINSEQ_3:30;
then A22: (maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*> c= W2 by A16, GRFUNC_1:2;
len (maxPrefix (W1,W2)) < len W1 by A2, A13, XXREAL_0:1;
then len ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) <= len W1 by A4, NAT_1:13;
then dom ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) c= dom W1 by FINSEQ_3:30;
then (maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*> c= W1 by A5, GRFUNC_1:2;
then (maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*> c= maxPrefix (W1,W2) by A22, Def1;
then len ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) <= len (maxPrefix (W1,W2)) by FINSEQ_1:63;
then (len (maxPrefix (W1,W2))) + 1 <= len (maxPrefix (W1,W2)) by FINSEQ_2:16;
hence contradiction by NAT_1:13; :: thesis: verum