set f = U -concatenation ;
set D = U * ;
defpred S1[ set ] means $1 is FinSequence of U;
defpred S2[] means for p1, q1, p2, q2 being U -valued FinSequence st p1 in X & p2 in X & p1 ^ q1 = p2 ^ q2 holds
( p1 = p2 & q1 = q2 );
thus
( X is U -prefix implies S2[] )
( ( for p1, q1, p2, q2 being U -valued FinSequence st p1 in X & p2 in X & p1 ^ q1 = p2 ^ q2 holds
( p1 = p2 & q1 = q2 ) ) implies X is U -prefix )proof
assume
X is
U -prefix
;
S2[]
then B2:
X is
U -concatenation -unambiguous
by DefPrefix;
let p1,
q1,
p2,
q2 be
U -valued FinSequence;
( p1 in X & p2 in X & p1 ^ q1 = p2 ^ q2 implies ( p1 = p2 & q1 = q2 ) )
Z0:
(
S1[
p1] &
S1[
p2] &
S1[
q1] &
S1[
q2] )
by Lm45;
assume Z:
(
p1 in X &
p2 in X )
;
( not p1 ^ q1 = p2 ^ q2 or ( p1 = p2 & q1 = q2 ) )
(
q1 in U * &
q2 in U * &
p1 in U * &
p2 in U * )
by Z0, FINSEQ_1:def 11;
then B1:
(
p1 in X /\ (U *) &
p2 in X /\ (U *) &
q1 in U * &
q2 in U * )
by Z0, XBOOLE_0:def 4, Z;
assume
p1 ^ q1 = p2 ^ q2
;
( p1 = p2 & q1 = q2 )
then (U -concatenation) . (
p1,
q1) =
p2 ^ q2
by Th4
.=
(U -concatenation) . (
p2,
q2)
by Th4
;
hence
(
p1 = p2 &
q1 = q2 )
by B2, DefUnambiguous2, B1;
verum
end;
assume B3:
S2[]
; X is U -prefix
now let x1,
x2,
d1,
d2 be
set ;
( x1 in X /\ (U *) & x2 in X /\ (U *) & d1 in U * & d2 in U * & (U -concatenation) . (x1,d1) = (U -concatenation) . (x2,d2) implies ( x1 = x2 & d1 = d2 ) )assume C0:
(
x1 in X /\ (U *) &
x2 in X /\ (U *) &
d1 in U * &
d2 in U * )
;
( (U -concatenation) . (x1,d1) = (U -concatenation) . (x2,d2) implies ( x1 = x2 & d1 = d2 ) )then reconsider x11 =
x1,
x22 =
x2,
d11 =
d1,
d22 =
d2 as
Element of
U * ;
assume
(U -concatenation) . (
x1,
d1)
= (U -concatenation) . (
x2,
d2)
;
( x1 = x2 & d1 = d2 )then x11 ^ d11 =
(U -concatenation) . (
x22,
d22)
by Th4
.=
x22 ^ d22
by Th4
;
hence
(
x1 = x2 &
d1 = d2 )
by B3, C0;
verum end;
then
X is U -concatenation -unambiguous
by DefUnambiguous2;
hence
X is U -prefix
by DefPrefix; verum