let p, q be FinSequence; ( 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)
; contradiction
set dI = len (maxPrefix (p,q));
set mP = maxPrefix (p,q);
set lmP = (maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>;
A4:
now for x being object st x in dom ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) holds
((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) . x = q . xlet x be
object ;
( x in dom ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) implies ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) . b1 = q . b1 )assume A5:
x in dom ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>)
;
((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) . b1 = q . b1reconsider n =
x as
Nat by A5;
A6:
1
<= n
by A5, FINSEQ_3:25;
n <= len ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>)
by A5, FINSEQ_3:25;
then A7:
n <= (len (maxPrefix (p,q))) + 1
by FINSEQ_2:16;
end;
A9:
now for x being object st x in dom ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) holds
((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) . x = p . xlet x be
object ;
( x in dom ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) implies ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) . b1 = p . b1 )assume A10:
x in dom ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>)
;
((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) . b1 = p . b1reconsider n =
x as
Nat by A10;
A11:
1
<= n
by A10, FINSEQ_3:25;
n <= len ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>)
by A10, FINSEQ_3:25;
then A12:
n <= (len (maxPrefix (p,q))) + 1
by FINSEQ_2:16;
end;
A14:
len ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) = (len (maxPrefix (p,q))) + 1
by FINSEQ_2:16;
len (maxPrefix (p,q)) < len q
by A2, Th8;
then
len ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) <= len q
by A14, NAT_1:13;
then
dom ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) c= dom q
by FINSEQ_3:30;
then A15:
(maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*> c= q
by A4, GRFUNC_1:2;
len (maxPrefix (p,q)) < len p
by A1, Th8;
then
len ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) <= len p
by A14, NAT_1:13;
then
dom ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) c= dom p
by FINSEQ_3:30;
then
(maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*> c= p
by A9, GRFUNC_1:2;
then
(maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*> c= maxPrefix (p,q)
by A15, Def1;
then
len ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) <= len (maxPrefix (p,q))
by FINSEQ_1:63;
then
(len (maxPrefix (p,q))) + 1 <= len (maxPrefix (p,q))
by FINSEQ_2:16;
hence
contradiction
by NAT_1:13; verum