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 dI = len (maxPrefix (p,q));
set mP = maxPrefix (p,q);
set lmP = (maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>;
A4: now :: thesis: 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 . x
let x be object ; :: thesis: ( 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))*>) ; :: thesis: ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) . b1 = q . b1
reconsider 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;
per cases ( n <= len (maxPrefix (p,q)) or n = (len (maxPrefix (p,q))) + 1 ) by A7, NAT_1:8;
suppose A8: n <= len (maxPrefix (p,q)) ; :: thesis: ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) . b1 = q . b1
then n in dom (maxPrefix (p,q)) by A6, FINSEQ_3:25;
hence ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) . x = (maxPrefix (p,q)) . x by FINSEQ_1:def 7
.= q . x by A8, Th6 ;
:: thesis: verum
end;
suppose n = (len (maxPrefix (p,q))) + 1 ; :: thesis: ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) . b1 = q . b1
hence ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) . x = q . x by A3, FINSEQ_1:42; :: thesis: verum
end;
end;
end;
A9: now :: thesis: 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 . x
let x be object ; :: thesis: ( 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))*>) ; :: thesis: ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) . b1 = p . b1
reconsider 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;
per cases ( n <= len (maxPrefix (p,q)) or n = (len (maxPrefix (p,q))) + 1 ) by A12, NAT_1:8;
suppose A13: n <= len (maxPrefix (p,q)) ; :: thesis: ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) . b1 = p . b1
then n in dom (maxPrefix (p,q)) by A11, FINSEQ_3:25;
hence ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) . x = (maxPrefix (p,q)) . x by FINSEQ_1:def 7
.= p . x by A13, Th6 ;
:: thesis: verum
end;
suppose n = (len (maxPrefix (p,q))) + 1 ; :: thesis: ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) . b1 = p . b1
hence ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) . x = p . x by FINSEQ_1:42; :: thesis: verum
end;
end;
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; :: thesis: verum