let G be non-multi _Graph; :: thesis: for W1, W2 being Walk of G st W1 .first() = W2 .first() & not W1 is_a_prefix_of W2 & not W2 is_a_prefix_of W1 holds
W1 . ((len (maxPrefix (W1,W2))) + 2) <> W2 . ((len (maxPrefix (W1,W2))) + 2)
let W1, W2 be Walk of G; :: thesis: ( W1 .first() = W2 .first() & not W1 is_a_prefix_of W2 & not W2 is_a_prefix_of W1 implies W1 . ((len (maxPrefix (W1,W2))) + 2) <> W2 . ((len (maxPrefix (W1,W2))) + 2) )
assume that
A1: W1 .first() = W2 .first() and
A2: not W1 c= W2 and
A3: not W2 c= W1 and
A4: W1 . ((len (maxPrefix (W1,W2))) + 2) = W2 . ((len (maxPrefix (W1,W2))) + 2) ; :: thesis: contradiction
set dI = len (maxPrefix (W1,W2));
A5: len (maxPrefix (W1,W2)) is odd by A1, Th22;
len (maxPrefix (W1,W2)) < len W1 by A2, Th8;
then A6: W1 . ((len (maxPrefix (W1,W2))) + 1) Joins W1 . (len (maxPrefix (W1,W2))),W1 . ((len (maxPrefix (W1,W2))) + 2),G by A5, GLIB_001:def 3;
A7: W1 . (len (maxPrefix (W1,W2))) = W2 . (len (maxPrefix (W1,W2))) by Th7;
len (maxPrefix (W1,W2)) < len W2 by A3, Th8;
then A8: W2 . ((len (maxPrefix (W1,W2))) + 1) Joins W2 . (len (maxPrefix (W1,W2))),W2 . ((len (maxPrefix (W1,W2))) + 2),G by A5, GLIB_001:def 3;
W1 . ((len (maxPrefix (W1,W2))) + 1) <> W2 . ((len (maxPrefix (W1,W2))) + 1) by A2, A3, Th9;
hence contradiction by A4, A7, A6, A8, GLIB_000:def 20; :: thesis: verum