let p, q be FinSequence; :: thesis: ( not p is_a_prefix_of q & not q is_a_prefix_of p implies p . ((len (maxPrefix p,q)) + 1) <> q . ((len (maxPrefix p,q)) + 1) )
assume that
A1: not p c= q and
A2: not q c= p and
A3: p . ((len (maxPrefix p,q)) + 1) = q . ((len (maxPrefix p,q)) + 1) ; :: thesis: contradiction
set mP = maxPrefix p,q;
set dI = len (maxPrefix p,q);
set lmP = (maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>;
A4: len ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) = (len (maxPrefix p,q)) + 1 by FINSEQ_2:19;
len (maxPrefix p,q) < len p by A1, Th8;
then len ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) <= len p by A4, NAT_1:13;
then A5: dom ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) c= dom p by FINSEQ_3:32;

now

let x be set ; :: thesis: ( x in dom ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) implies ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) . b₁ = p . b₁ )
assume A6: x in dom ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) ; :: thesis: ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) . b₁ = p . b₁
x is Element of NAT by A6;
then reconsider n = x as Nat ;
A7: 1 <= n by A6, FINSEQ_3:27;
n <= len ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) by A6, FINSEQ_3:27;
then A8: n <= (len (maxPrefix p,q)) + 1 by FINSEQ_2:19;

per cases ( n <= len (maxPrefix p,q) or n = (len (maxPrefix p,q)) + 1 ) by A8, NAT_1:8;

suppose A9: n <= len (maxPrefix p,q) ; :: thesis: ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) . b₁ = p . b₁

then n in dom (maxPrefix p,q) by A7, FINSEQ_3:27;
hence ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) . x = (maxPrefix p,q) . x by FINSEQ_1:def 7
.= p . x by A9, Th6 ;
:: thesis: verum

end;

suppose n = (len (maxPrefix p,q)) + 1 ; :: thesis: ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) . b₁ = p . b₁

hence ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) . x = p . x by FINSEQ_1:59; :: thesis: verum

end;

end;

end;

then A10: (maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*> c= p by A5, GRFUNC_1:8;
len (maxPrefix p,q) < len q by A2, Th8;
then len ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) <= len q by A4, NAT_1:13;
then A11: dom ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) c= dom q by FINSEQ_3:32;

now

let x be set ; :: thesis: ( x in dom ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) implies ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) . b₁ = q . b₁ )
assume A12: x in dom ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) ; :: thesis: ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) . b₁ = q . b₁
x is Element of NAT by A12;
then reconsider n = x as Nat ;
A13: 1 <= n by A12, FINSEQ_3:27;
n <= len ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) by A12, FINSEQ_3:27;
then A14: n <= (len (maxPrefix p,q)) + 1 by FINSEQ_2:19;

per cases ( n <= len (maxPrefix p,q) or n = (len (maxPrefix p,q)) + 1 ) by A14, NAT_1:8;

suppose A15: n <= len (maxPrefix p,q) ; :: thesis: ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) . b₁ = q . b₁

then n in dom (maxPrefix p,q) by A13, FINSEQ_3:27;
hence ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) . x = (maxPrefix p,q) . x by FINSEQ_1:def 7
.= q . x by A15, Th6 ;
:: thesis: verum

end;

suppose n = (len (maxPrefix p,q)) + 1 ; :: thesis: ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) . b₁ = q . b₁

hence ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) . x = q . x by A3, FINSEQ_1:59; :: thesis: verum

end;

end;

end;

then (maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*> c= q by A11, GRFUNC_1:8;
then (maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*> c= maxPrefix p,q by A10, Def1;
then len ((maxPrefix p,q) ^ <*(p . ((len (maxPrefix p,q)) + 1))*>) <= len (maxPrefix p,q) by FINSEQ_1:84;
then (len (maxPrefix p,q)) + 1 <= len (maxPrefix p,q) by FINSEQ_2:19;
hence contradiction by NAT_1:13; :: thesis: verum