Copyright (c) 1995 Association of Mizar Users
environ
vocabulary TREES_1, FINSEQ_1, ZFMISC_1, BOOLE, TREES_3, RELAT_1, TREES_2,
FUNCT_1;
notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XREAL_0, NAT_1, RELAT_1,
FUNCT_1, FINSEQ_1, TREES_1, TREES_2;
constructors NAT_1, TREES_2, XREAL_0, MEMBERED;
clusters SUBSET_1, TREES_2, RELSET_1, ARYTM_3, XBOOLE_0, MEMBERED;
requirements NUMERALS, BOOLE, SUBSET;
definitions TARSKI, XBOOLE_0, TREES_1, TREES_2;
theorems TARSKI, FUNCT_1, FINSEQ_1, RLVECT_1, TREES_1, TREES_2, XBOOLE_0,
XBOOLE_1;
schemes TREES_2;
begin
reserve T, T1 for Tree,
P for AntiChain_of_Prefixes of T,
p1 for FinSequence,
p, q, r, s, p' for FinSequence of NAT,
x, Z for set,
t for Element of T,
k, n for Nat;
theorem Th1:
for p,q,r,s being FinSequence st p^q = s^r holds p,s are_c=-comparable
proof let p,q,r,s be FinSequence;
assume A1: p^q = s^r;
then A2: p is_a_prefix_of s^r by TREES_1:8;
s is_a_prefix_of p^q by A1,TREES_1:8;
hence p,s are_c=-comparable by A1,A2,TREES_2:1;
end;
definition let T,T1;
let P such that
A1: P<>{};
func tree(T,P,T1) -> Tree means :Def1:
q in it iff
(q in T & for p st p in P holds not p is_a_proper_prefix_of q)
or ex p,r st p in P & r in T1 & q = p^r;
existence
proof
reconsider P' = P as Subset of T by TREES_1:def 14;
now let x; assume A2: x in P';
then reconsider x' = x as FinSequence by TREES_1:def 13;
reconsider x' as Element of T by A2;
now let p such that A3: p in P;
per cases;
suppose p <> x';
then not p,x' are_c=-comparable by A2,A3,TREES_1:def 13;
hence not p is_a_proper_prefix_of x' by XBOOLE_1:104;
suppose p = x';
hence not p is_a_proper_prefix_of x';
end;
hence x in {t : for p st p in P holds not p is_a_proper_prefix_of t};
end;
then P c= {t : for p st p in P holds not p is_a_proper_prefix_of t}
by TARSKI:def 3;
then reconsider Y = {t : for p st p in P holds not p is_a_proper_prefix_of
t}
as non empty set by A1,XBOOLE_1:3;
consider Z such that A4:
Z = {p^s where p is Element of T, s is Element of T1 : p in P};
reconsider X = Y \/ Z as non empty set;
A5: x in {t : for p st p in P holds not p is_a_proper_prefix_of t} implies
x is FinSequence of NAT & x in NAT* & x in T
proof assume
x in {t : for p st p in P holds not p is_a_proper_prefix_of t};
then A6: ex t st x = t & for p st p in P holds not p is_a_proper_prefix_of
t;
hence x is FinSequence of NAT;
thus thesis by A6,FINSEQ_1:def 11;
end;
X is Tree-like
proof
thus X c= NAT*
proof let x; assume x in X;
then A7: x in {t : for p st p in P holds not p is_a_proper_prefix_of t
} or
x in {p^s where p is Element of T, s is Element of T1 : p in P}
by A4,XBOOLE_0:def 2;
now assume
x in {p^s where p is Element of T, s is Element of T1 : p in P}
;
then ex p being Element of T st ex s being Element of T1 st
x = p^s & p in P;
hence x is FinSequence of NAT;
end;
hence thesis by A5,A7,FINSEQ_1:def 11;
end;
thus for q st q in X holds ProperPrefixes q c= X
proof let q such that A8: q in X;
A9: now assume
A10: q in {t : for p st p in P holds not p is_a_proper_prefix_of
t};
then ex t st q = t &
for p st p in P holds not p is_a_proper_prefix_of t;
then A11: ProperPrefixes q c= T by TREES_1:def 5;
thus ProperPrefixes q c= X
proof let x; assume
A12: x in ProperPrefixes q;
then consider p1 such that
A13: x = p1 & p1 is_a_proper_prefix_of q by TREES_1:def 4;
reconsider p1 as Element of T by A11,A12,A13;
for p st p in P holds not p is_a_proper_prefix_of p1
proof let p such that A14: p in P;
consider t such that A15: q = t & for p st p in P holds
not p is_a_proper_prefix_of t by A10;
q = t & not p is_a_proper_prefix_of t by A14,A15;
hence not p is_a_proper_prefix_of p1 by A13,TREES_1:27;
end;
then x in { s1 where s1 is Element of T : for p st p in P
holds
not p is_a_proper_prefix_of s1 } by A13;
hence thesis by XBOOLE_0:def 2;
end;
end;
now assume q in Z;
then consider p being Element of T, s being Element of T1 such
that
A16: q = p^s & p in P by A4;
thus ProperPrefixes q c= X
proof let x; assume
A17: x in ProperPrefixes q;
then reconsider r = x as FinSequence by TREES_1:35;
r is_a_proper_prefix_of p^s by A16,A17,TREES_1:36;
then r is_a_prefix_of p^s & r <> p^s by XBOOLE_0:def 8;
then consider r1 being FinSequence such that
A18: p^s = r^r1 by TREES_1:8;
A19: now assume len p <= len r;
then consider r2 being FinSequence such that
A20: p^r2 = r by A18,FINSEQ_1:64;
p^s = p^(r2^r1) by A18,A20,FINSEQ_1:45;
then s = r2^r1 by FINSEQ_1:46;
then s|(dom r2) = r2 by RLVECT_1:105;
then A21: s|Seg(len r2) = r2 by FINSEQ_1:def 3;
then reconsider r2 as FinSequence of NAT by FINSEQ_1:23;
r2 is_a_prefix_of s & s in T1 by A21,TREES_1:def 1;
then reconsider r2 as Element of T1 by TREES_1:45;
r = p^r2 by A20;
then r in { w^v where w is Element of T,
v is Element of T1 : w in P } by A16;
hence r in X by A4,XBOOLE_0:def 2;
end;
now assume len r <= len p;
then ex r2 being FinSequence st
r^r2 = p by A18,FINSEQ_1:64;
then p|(dom r) = r by RLVECT_1:105;
then A22: p|Seg(len r) = r by FINSEQ_1:def 3;
then reconsider r3 = r as FinSequence of NAT by FINSEQ_1:23
;
A23: r3 is_a_prefix_of p by A22,TREES_1:def 1;
then reconsider r3 as Element of T by TREES_1:45;
for p' st p' in P holds not p' is_a_proper_prefix_of r3
proof let p'; assume A24: p' in P;
assume A25: p' is_a_proper_prefix_of r3;
then p' is_a_prefix_of r3 by XBOOLE_0:def 8;
then p' is_a_prefix_of p by A23,XBOOLE_1:1;
then A26: p,p' are_c=-comparable by XBOOLE_0:def 9;
per cases;
suppose p<>p';
hence contradiction by A16,A24,A26,TREES_1:def 13;
suppose p=p';
hence contradiction by A23,A25,TREES_1:28;
end;
then r3 in { t : for p' st p' in P holds
not p' is_a_proper_prefix_of t };
hence r in X by XBOOLE_0:def 2;
end;
hence thesis by A19;
end;
end;
hence thesis by A8,A9,XBOOLE_0:def 2;
end;
let q,k,n such that
A27: q^<*k*> in X & n <= k;
A28: now assume A29: q^<*k*> in
{ t : for p st p in P holds not p is_a_proper_prefix_of t };
then ex s being Element of T st
q^<*k*> = s & for p st p in P holds not p is_a_proper_prefix_of s;
then reconsider u = q^<*n*> as Element of T by A27,TREES_1:def 5;
now let p such that A30: p in P; assume p is_a_proper_prefix_of u;
then A31: p is_a_prefix_of q by TREES_1:32;
consider s being Element of T such that A32:
q^<*k*> = s & for p st p in P holds
not p is_a_proper_prefix_of s by A29;
not p is_a_proper_prefix_of s by A30,A32;
hence contradiction by A31,A32,TREES_1:31;
end;
then q^<*n*> in {t : for p st p in P holds not p
is_a_proper_prefix_of t};
hence q^<*n*> in X by XBOOLE_0:def 2;
end;
now assume q^<*k*> in Z;
then consider p being Element of T, s being Element of T1 such that
A33: q^<*k*> = p^s & p in P by A4;
A34: now assume len q <= len p;
then consider r being FinSequence such that
A35: q^r = p by A33,FINSEQ_1:64;
q^<*k*> = q^(r^s) by A33,A35,FINSEQ_1:45;
then A36: <*k*> = r^s by FINSEQ_1:46;
A37: now assume
A38: r = <*k*>;
then reconsider s' = q^<*n*> as Element of T by A27,A35,TREES_1:
def 5;
now let p' such that A39: p' in P;
assume A40: p' is_a_proper_prefix_of s';
then A41: p' is_a_prefix_of s' & p' <> s' by XBOOLE_0:def 8;
A42: len p = len q + len <*k*> by A35,A38,FINSEQ_1:35
.= len q + 1 by FINSEQ_1:57
.= len q + len <*n*> by FINSEQ_1:57
.= len s' by FINSEQ_1:35;
per cases;
suppose p' = p;
hence contradiction by A41,A42,TREES_1:15;
suppose A43: p' <> p;
A44: q is_a_prefix_of p by A35,TREES_1:8;
p' is_a_prefix_of q by A40,TREES_1:32;
then p' is_a_prefix_of p by A44,XBOOLE_1:1;
then p,p' are_c=-comparable by XBOOLE_0:def 9;
hence contradiction by A33,A39,A43,TREES_1:def 13;
end;
hence q^<*n*> in { t : for p st p in P holds
not p is_a_proper_prefix_of t };
end;
now assume
A45: s = <*k*> & r = {};
s = <*>NAT^s & s in T1 & {} = <*> NAT
by FINSEQ_1:47;
then <*>NAT^<*n*> in T1 by A27,A45,TREES_1:def 5;
then reconsider t = <*n*> as Element of T1 by FINSEQ_1:47;
q^<*n*> = p^t by A35,A45,FINSEQ_1:47; hence q^<*n*> in
Z by A4,A33;
end;
hence q^<*n*> in X by A36,A37,TREES_1:6,XBOOLE_0:def 2;
end;
now assume len p <= len q;
then consider r being FinSequence such that
A46: p^r = q by A33,FINSEQ_1:64;
p^(r^<*k*>) = p^s by A33,A46,FINSEQ_1:45;
then A47: r^<*k*> = s & s in T1 by FINSEQ_1:46;
then s|dom r = r by RLVECT_1:105;
then s|Seg len r = r by FINSEQ_1:def 3;
then reconsider r as FinSequence of NAT by FINSEQ_1:23;
reconsider t = r^<*n*> as Element of T1 by A27,A47,TREES_1:def 5;
q^<*n*> = p^t by A46,FINSEQ_1:45;
then q^<*n*> in { p'^v where p' is Element of T,
v is Element of T1 : p' in P } by A33;
hence q^<*n*> in X by A4,XBOOLE_0:def 2;
end;
hence q^<*n*> in X by A34;
end;
hence q^<*n*> in X by A27,A28,XBOOLE_0:def 2;
end;
then reconsider X as Tree;
take X; let q;
thus q in X implies
(q in T & for p st p in P holds not p is_a_proper_prefix_of q)
or ex p,r st p in P & r in T1 & q = p^r
proof assume A48: q in X;
A49: now assume q in Y;
then ex s being Element of T st q = s &
for p st p in P holds not p is_a_proper_prefix_of s;
hence thesis;
end;
now assume q in Z;
then ex p being Element of T st ex s being Element of T1 st
q = p^s & p in P by A4;
hence ex p,r st p in P & r in T1 & q = p^r;
end;
hence thesis by A48,A49,XBOOLE_0:def 2;
end;
assume
A50: (q in T & for p st p in P holds not p is_a_proper_prefix_of q)
or ex p,r st p in P & r in T1 & q = p^r;
A51: (q in T & for p st p in P holds not p is_a_proper_prefix_of q) implies
q in {t : for p st p in P holds not p is_a_proper_prefix_of t};
now given p,r such that
A52: p in P & r in T1 & q = p^r; P c= T by TREES_1:def 14;
hence q in Z by A4,A52;
end;
hence thesis by A50,A51,XBOOLE_0:def 2;
end;
uniqueness
proof let S1,S2 be Tree such that
A53: q in S1 iff (q in T & for p st p in
P holds not p is_a_proper_prefix_of q)
or ex p,r st p in P & r in T1 & q = p^r and
A54: q in S2 iff (q in T & for p st p in
P holds not p is_a_proper_prefix_of q)
or ex p,r st p in P & r in T1 & q = p^r;
let x be FinSequence of NAT;
thus x in S1 implies x in S2
proof assume
A55: x in S1;
reconsider q = x as FinSequence of NAT;
(q in T & for p st p in P holds not p is_a_proper_prefix_of q)
or ex p,r st p in P & r in T1 & q = p^r by A53,A55;
hence thesis by A54;
end;
assume
A56: x in S2;
reconsider q = x as FinSequence of NAT;
(q in T & for p st p in P holds not p is_a_proper_prefix_of q)
or ex p,r st p in P & r in T1 & q = p^r by A54,A56;
hence thesis by A53;
end;
end;
theorem Th2:
P <> {} implies tree(T,P,T1) =
{t1 where t1 is Element of T :
for p st p in P holds not p is_a_proper_prefix_of t1}
\/ { p^s where p is Element of T, s is Element of T1 : p in P }
proof assume A1: P <> {};
thus tree(T,P,T1) c=
{t : for p st p in P holds not p is_a_proper_prefix_of t} \/
{ p^s where p is Element of T, s is Element of T1 : p in P }
proof let x be set; assume
A2: x in tree(T,P,T1);
then reconsider q = x as FinSequence of NAT by TREES_1:44;
A3: now given p,r such that
A4: p in P & r in T1 & q = p^r; P c= T by TREES_1:def 14;
hence x in { p'^s where p' is Element of T,
s is Element of T1 : p' in P } by A4;
end;
q in T & (for p st p in P holds not p is_a_proper_prefix_of q) implies
x in { t : for p st p in P holds not p is_a_proper_prefix_of t };
hence thesis by A1,A2,A3,Def1,XBOOLE_0:def 2;
end;
let x be set such that
A5:x in { t : for p st p in P holds not p is_a_proper_prefix_of t } \/
{ p^s where p is Element of T, s is Element of T1 : p in P };
A6:now assume x in { p^s where p is Element of T, s is Element of T1 : p in
P };
then ex p being Element of T st
ex s being Element of T1 st x = p^s & p in P;
hence thesis by Def1;
end;
now assume x in { t : for p st p in P holds not p is_a_proper_prefix_of t
}
;
then ex t st x = t & for p st p in P holds not p is_a_proper_prefix_of t;
hence thesis by A1,Def1;
end;
hence thesis by A5,A6,XBOOLE_0:def 2;
end;
theorem Th3:
{t1 where t1 is Element of T :
for p st p in P holds not p is_a_prefix_of t1} c=
{t1 where t1 is Element of T :
for p st p in P holds not p is_a_proper_prefix_of t1}
proof
let x be set; assume
x in {t1 where t1 is Element of T :
for p st p in P holds not p is_a_prefix_of t1};
then consider t' being Element of T such that A1: x = t' &
for p st p in P holds not p is_a_prefix_of t';
now let p; assume p in P; then not p is_a_prefix_of t' by A1;
hence not p is_a_proper_prefix_of t' by XBOOLE_0:def 8;
end;
hence x in {t1 where t1 is Element of T :
for p st p in P holds not p is_a_proper_prefix_of t1} by A1;
end;
theorem Th4:
P c= {t1 where t1 is Element of T :
for p st p in P holds not p is_a_proper_prefix_of t1}
proof let x be set; assume A1: x in P;
ex t1 being Element of T st x = t1 &
for p st p in P holds not p is_a_proper_prefix_of t1
proof
P c= T by TREES_1:def 14;
then consider t' being Element of T such that A2: t' = x by A1;
now let p such that A3: p in P;
per cases;
suppose t' = p;
hence not p is_a_proper_prefix_of t';
suppose t' <> p;
then not t', p are_c=-comparable by A1,A2,A3,TREES_1:def 13;
hence not p is_a_proper_prefix_of t' by XBOOLE_1:104;
end;
hence thesis by A2;
end;
hence x in {t1 where t1 is Element of T :
for p st p in P holds not p is_a_proper_prefix_of t1};
end;
theorem Th5:
{t1 where t1 is Element of T :
for p st p in P holds not p is_a_proper_prefix_of t1} \
{t1 where t1 is Element of T :
for p st p in P holds not p is_a_prefix_of t1} = P
proof
now let x be set; assume
x in {t1 where t1 is Element of T :
for p st p in P holds not p is_a_proper_prefix_of t1} \
{t1 where t1 is Element of T :
for p st p in P holds not p is_a_prefix_of t1};
then A1: x in {t1 where t1 is Element of T :
for p st p in P holds not p is_a_proper_prefix_of t1} &
not x in {t1 where t1 is Element of T :
for p st p in P holds not p is_a_prefix_of t1} by XBOOLE_0:def 4;
assume A2: not x in P;
ex t1 being Element of T st x = t1 &
for p st p in P holds not p is_a_prefix_of t1
proof
consider t' being Element of T such that A3: x = t' &
for p st p in P holds not p is_a_proper_prefix_of t' by A1;
now let p; assume A4: p in P;
then A5: not p is_a_proper_prefix_of t' by A3;
per cases by A5,XBOOLE_0:def 8;
suppose not p is_a_prefix_of t';
hence not p is_a_prefix_of t';
suppose p = t';
hence not p is_a_prefix_of t' by A2,A3,A4;
end;
hence thesis by A3;
end;
hence contradiction by A1;
end;
hence {t1 where t1 is Element of T :
for p st p in P holds not p is_a_proper_prefix_of t1} \
{t1 where t1 is Element of T :
for p st p in P holds not p is_a_prefix_of t1} c= P by TARSKI:def 3;
let x be set; assume A6: x in P;
A7: P c= {t1 where t1 is Element of T :
for p st p in P holds not p is_a_proper_prefix_of t1} by Th4;
not x in {t1 where t1 is Element of T :
for p st p in P holds not p is_a_prefix_of t1}
proof assume x in {t1 where t1 is Element of T :
for p st p in P holds not p is_a_prefix_of t1};
then consider t' being Element of T such that A8: x = t' &
for p st p in P holds not p is_a_prefix_of t';
thus contradiction by A6,A8;
end;
hence x in {t1 where t1 is Element of T :
for p st p in P holds not p is_a_proper_prefix_of t1} \
{t1 where t1 is Element of T :
for p st p in P holds not p is_a_prefix_of t1} by A6,A7,XBOOLE_0:def 4;
end;
theorem Th6:
for T, T1, P holds
P c= { p^s where p is Element of T, s is Element of T1 : p in P }
proof let T, T1, P;
now let x be set; assume A1: x in P;
P c= T by TREES_1:def 14;
then consider q being Element of T such that A2: q = x by A1; <*> NAT in
T1 by TREES_1:47;
then consider s' being Element of T1 such that A3: s' = <*> NAT;
q = q^s' by A3,FINSEQ_1:47;
hence x in { p^s where p is Element of T, s is Element of T1 : p in P }
by A1,A2;
end;
hence P c= { p^s where p is Element of T, s is Element of T1 : p in P }
by TARSKI:def 3;
end;
theorem Th7:
P <> {} implies tree(T,P,T1) =
{t1 where t1 is Element of T :
for p st p in P holds not p is_a_prefix_of t1}
\/ { p^s where p is Element of T, s is Element of T1 : p in P }
proof
assume A1: P <> {};
then A2:tree(T,P,T1) = {t1 where t1 is Element of T :
for p st p in P holds not p is_a_proper_prefix_of t1}
\/ { p^s where p is Element of T, s is Element of T1 : p in P } by Th2;
thus tree(T,P,T1) c= {t1 where t1 is Element of T :
for p st p in P holds not p is_a_prefix_of t1}
\/ { p^s where p is Element of T, s is Element of T1 : p in P }
proof let x be set; assume x in tree(T,P,T1);
then A3: x in {t1 where t1 is Element of T :
for p st p in P holds not p is_a_proper_prefix_of t1}
\/ { p^s where p is Element of T, s is Element of T1 : p in P } by A1,
Th2;
now per cases;
suppose A4: x in P;
P c= { p^s where p is Element of T, s is Element of T1 : p in P }
by Th6;
hence x in {t1 where t1 is Element of T :
for p st p in P holds not p is_a_prefix_of t1}
or x in { p^s where p is Element of T, s is Element of T1 : p in P }
by A4;
suppose A5: not x in P;
now per cases by A3,XBOOLE_0:def 2;
suppose A6: x in {t1 where t1 is Element of T :
for p st p in P holds not p is_a_proper_prefix_of t1};
x in {t1 where t1 is Element of T :
for p st p in P holds not p is_a_prefix_of t1}
proof
assume A7: not x in {t1 where t1 is Element of T :
for p st p in P holds not p is_a_prefix_of t1};
{t1 where t1 is Element of T :
for p st p in P holds not p is_a_proper_prefix_of t1} \
{t1 where t1 is Element of T :
for p st p in P holds not p is_a_prefix_of t1} = P by Th5;
hence contradiction by A5,A6,A7,XBOOLE_0:def 4;
end;
hence x in {t1 where t1 is Element of T :
for p st p in P holds not p is_a_prefix_of t1} or
x in { p^s where p is Element of T, s is Element of T1 : p in P };
suppose
x in { p^s where p is Element of T, s is Element of T1 : p in P }
;
hence x in {t1 where t1 is Element of T :
for p st p in P holds not p is_a_prefix_of t1} or
x in { p^s where p is Element of T, s is Element of T1 : p in P };
end;
hence x in {t1 where t1 is Element of T :
for p st p in P holds not p is_a_prefix_of t1}
or x in { p^s where p is Element of T, s is Element of T1 : p in P };
end;
hence x in {t1 where t1 is Element of T :
for p st p in P holds not p is_a_prefix_of t1}
\/ { p^s where p is Element of T, s is Element of T1 : p in P }
by XBOOLE_0:def 2;
end;
{t1 where t1 is Element of T :
for p st p in P holds not p is_a_prefix_of t1} c=
{t1 where t1 is Element of T :
for p st p in P holds not p is_a_proper_prefix_of t1} by Th3;
hence {t1 where t1 is Element of T :
for p st p in P holds not p is_a_prefix_of t1}
\/ { p^s where p is Element of T, s is Element of T1 : p in P }
c= tree(T,P,T1) by A2,XBOOLE_1:9;
end;
canceled;
theorem
p in P implies T1 = tree(T,P,T1)|p
proof
assume
A1: p in P;
ex q,r st q in P & r in T1 & p = q^r
proof
consider q such that A2: q = p; consider r such that A3: r = <*> NAT; A4:
r in T1 by A3,TREES_1:47; p = q^r by A2,A3,FINSEQ_1:47;
hence thesis by A1,A2,A4;
end;
then A5: p in tree(T,P,T1) by Def1;
let x be FinSequence of NAT;
thus x in T1 implies x in tree(T,P,T1)|p
proof assume
x in T1;
then p^x in tree(T,P,T1) by A1,Def1;
hence thesis by A5,TREES_1:def 9;
end;
thus x in tree(T,P,T1)|p implies x in T1
proof
assume
x in tree(T,P,T1)|p;
then A6: p^x in tree(T,P,T1) by A5,TREES_1:def 9;
A7: now assume
p^x in T & for r st r in P holds not r is_a_proper_prefix_of p^x;
then A8: not p is_a_proper_prefix_of p^x by A1;
p is_a_prefix_of p^x by TREES_1:8;
then p^x = p by A8,XBOOLE_0:def 8 .= p^<*>NAT by FINSEQ_1:47;
then x = {} by FINSEQ_1:46;
hence x in T1 by TREES_1:47;
end;
now given s,r such that
A9: s in P & r in T1 & p^x = s^r;
now assume s <> p;
then not s,p are_c=-comparable by A1,A9,TREES_1:def 13;
hence contradiction by A9,Th1;
end;
hence x in T1 by A9,FINSEQ_1:46;
end;
hence thesis by A1,A6,A7,Def1;
end;
end;
definition let T;
cluster non empty AntiChain_of_Prefixes of T;
existence
proof
consider w being Element of T;
consider X being set such that A1: X = {w};
A2: X is AntiChain_of_Prefixes-like by A1,TREES_1:70;
X c= T
proof let x be set; assume x in X; then x = w by A1,TARSKI:def 1;
hence x in T;
end;
then reconsider X as AntiChain_of_Prefixes of T by A2,TREES_1:def 14;
take X;
thus thesis by A1;
end;
end;
definition let T; let t be Element of T;
redefine func {t} -> non empty AntiChain_of_Prefixes of T;
correctness by TREES_1:74;
end;
theorem Th10:
tree(T,{t},T1) = T with-replacement (t,T1)
proof
let p;
thus p in tree(T,{t},T1) implies p in T with-replacement (t,T1)
proof
assume A1: p in tree(T,{t},T1);
A2: now assume A3:
p in T & for s st s in {t} holds not s is_a_proper_prefix_of p;
t in {t} by TARSKI:def 1;
hence p in T & not t is_a_proper_prefix_of p by A3;
end;
now given s such that A4: ex r st s in {t} & r in T1 & p = s^r;
s = t by A4,TARSKI:def 1;
hence ex r st r in T1 & p = t^r by A4;
end;
hence p in T with-replacement (t,T1) by A1,A2,Def1,TREES_1:def 12;
end;
assume A5: p in T with-replacement (t,T1);
A6:p in T & not t is_a_proper_prefix_of p implies
p in T & for s st s in {t} holds not s is_a_proper_prefix_of p
by TARSKI:def 1;
now assume A7: ex r st r in T1 & p = t^r;
thus ex s,r st s in {t} & r in T1 & p = s^r
proof
take t; t in {t} by TARSKI:def 1;
hence thesis by A7;
end;
end;
hence p in tree(T,{t},T1) by A5,A6,Def1,TREES_1:def 12;
end;
reserve T,T1 for DecoratedTree,
P for AntiChain_of_Prefixes of dom T,
t for Element of dom T,
p1, p2, r1, r2 for FinSequence of NAT;
definition let T,P,T1;
assume
A1: P<>{};
func tree(T,P,T1) -> DecoratedTree means :Def2:
dom it = tree(dom T, P, dom T1) &
for q st q in tree(dom T, P, dom T1) holds
(for p st p in P holds not p is_a_prefix_of q & it.q = T.q)
or ex p,r st p in P & r in dom T1 & q = p^r & it.q = T1.r;
existence
proof
defpred X[FinSequence,set] means
(for p st p in P holds not p is_a_prefix_of $1 & $2 = T.$1) or
ex p,r st p in P & r in dom T1 & $1 = p^r & $2 = T1.r;
A2: for q st q in tree(dom T,P,dom T1) ex x st X[q,x]
proof let q; assume q in tree(dom T, P, dom T1);
then A3: q in {t where t is Element of dom T :
for p st p in P holds not p is_a_prefix_of t}
\/ { p^s where p is Element of dom T,
s is Element of dom T1 : p in P } by A1,Th7;
A4: now assume q in {t where t is Element of dom T :
for p st p in P holds not p is_a_prefix_of t};
then consider t such that A5: q = t &
for p st p in P holds not p is_a_prefix_of t;
take x = T.t;
for p st p in P holds not p is_a_prefix_of q & x = T.q by A5;
hence thesis;
end;
now assume q in { p^s where p is Element of dom T,
s is Element of dom T1 : p in P };
then consider p being Element of dom T, s being Element of dom T1
such that A6: q = p^s & p in P;
take x = T1.s;
(for p st p in P holds not p is_a_prefix_of q & x = T.q) or
ex p,r st p in P & r in dom T1 & q = p^r & x = T1.r by A6;
hence thesis;
end;
hence thesis by A3,A4,XBOOLE_0:def 2;
end;
thus ex T0 being DecoratedTree st dom T0 = tree(dom T, P, dom T1) &
for p st p in tree(dom T, P, dom T1) holds X[p,T0.p]
from DTreeEx(A2);
end;
uniqueness
proof let D1,D2 be DecoratedTree such that
A7: dom D1 = tree(dom T,P,dom T1) and
A8: for q st q in tree(dom T,P,dom T1) holds
(for p st p in P holds not p is_a_prefix_of q & D1.q = T.q) or
ex p,r st p in P & r in dom T1 & q = p^r & D1.q = T1.r and
A9: dom D2 = tree(dom T,P,dom T1) and
A10: for q st q in tree(dom T,P,dom T1) holds
(for p st p in P holds not p is_a_prefix_of q & D2.q = T.q) or
ex p,r st p in P & r in dom T1 & q = p^r & D2.q = T1.r;
now let q; assume
A11: q in dom D1 & D1.q <> D2.q;
thus contradiction
proof
per cases by A7,A8,A11;
suppose A12: for p st p in P holds
not p is_a_prefix_of q & D1.q = T.q;
now
per cases by A7,A10,A11;
suppose A13: for p st p in P holds
not p is_a_prefix_of q & D2.q = T.q;
consider x being set such that A14: x in P by A1,XBOOLE_0:def
1;
P c= dom T by TREES_1:def 14;
then reconsider x as Element of dom T by A14;
consider p' such that A15: p' = x;
D1.q = T.q by A12,A14,A15;
hence contradiction by A11,A13,A14,A15;
suppose ex p,r st p in P & r in dom T1 & q = p^r & D2.q = T1.r
;
then consider p2,r2 such that
A16: p2 in P & r2 in dom T1 & q = p2^r2 & D2.q = T1.r2;
not p2 is_a_prefix_of q by A12,A16;
hence contradiction by A16,TREES_1:8;
end;
hence contradiction;
suppose ex p,r st p in P & r in dom T1 & q = p^r & D1.q = T1.r;
then consider p1,r1 such that
A17: p1 in P & r1 in dom T1 & q = p1^r1 & D1.q = T1.r1;
now
per cases by A7,A10,A11;
suppose for p st p in P holds
not p is_a_prefix_of q & D2.q = T.q;
then not p1 is_a_prefix_of q by A17;
hence contradiction by A17,TREES_1:8;
suppose ex p,r st p in P & r in dom T1 & q = p^r & D2.q = T1.r
;
then consider p2,r2 such that
A18: p2 in P & r2 in dom T1 & q = p2^r2 & D2.q = T1.r2;
now assume A19: p1 <> p2;
p1,p2 are_c=-comparable by A17,A18,Th1;
hence contradiction by A17,A18,A19,TREES_1:def 13;
end;
hence contradiction by A11,A17,A18,FINSEQ_1:46;
end;
hence contradiction;
end;
end;
hence thesis by A7,A9,TREES_2:33;
end;
end;
canceled 2;
theorem Th13:
P<>{} implies for q st q in dom tree(T,P,T1) holds
(for p st p in P holds not p is_a_prefix_of q & tree(T,P,T1).q = T.q)
or ex p,r st p in P & r in dom T1 & q = p^r & tree(T,P,T1).q = T1.r
proof assume A1: P<>{}; let q; assume q in dom tree(T,P,T1);
then q in tree(dom T,P,dom T1) by A1,Def2;
hence thesis by Def2;
end;
theorem Th14:
p in dom T implies for q st q in dom (T with-replacement (p,T1)) holds
(not p is_a_prefix_of q & T with-replacement (p,T1).q = T.q)
or ex r st r in dom T1 & q = p^r & T with-replacement (p,T1).q = T1.r
proof assume A1: p in dom T; let q;
assume q in dom (T with-replacement (p,T1));
then q in dom T with-replacement (p,dom T1) by A1,TREES_2:def 12;
hence thesis by A1,TREES_2:def 12;
end;
theorem Th15:
P<>{} implies for q st q in dom tree(T,P,T1) &
q in {t1 where t1 is Element of dom T :
for p st p in P holds not p is_a_prefix_of t1}
holds tree(T,P,T1).q = T.q
proof assume A1: P<>{}; let q; assume A2: q in dom tree(T,P,T1) &
q in {t1 where t1 is Element of dom T :
for p st p in P holds not p is_a_prefix_of t1};
then consider t' being Element of dom T such that A3: t' = q &
for p st p in P holds not p is_a_prefix_of t';
per cases by A2,Th13;
suppose
A4: for p st p in P holds not p is_a_prefix_of q & tree(T,P,T1).q = T.q;
consider x being set such that A5: x in P by A1,XBOOLE_0:def 1;
P c= dom T by TREES_1:def 14;
then reconsider x as Element of dom T by A5;
consider p' such that A6: p' = x;
thus tree(T,P,T1).q = T.q by A4,A5,A6;
suppose ex p,r st p in P & r in dom T1 & q = p^r & tree(T,P,T1).q = T1.r;
then consider p,r such that A7: p in P & r in dom T1 & q = p^r &
tree(T,P,T1).q = T1.r;
not p is_a_prefix_of q by A3,A7;
hence tree(T,P,T1).q = T.q by A7,TREES_1:8;
end;
theorem Th16:
p in dom T implies for q st q in dom (T with-replacement (p,T1)) &
q in {t1 where t1 is Element of dom T : not p is_a_prefix_of t1}
holds T with-replacement (p,T1).q = T.q
proof assume A1: p in dom T;
let q; assume A2: q in dom (T with-replacement (p,T1)) &
q in {t1 where t1 is Element of dom T : not p is_a_prefix_of t1};
per cases by A1,A2,Th14;
suppose not p is_a_prefix_of q & T with-replacement (p,T1).q = T.q;
hence T with-replacement (p,T1).q = T.q;
suppose ex r st r in dom T1 & q = p^r &
T with-replacement (p,T1).q = T1.r;
then consider r such that
A3: r in dom T1 & q = p^r & T with-replacement (p,T1).q = T1.r;
consider t' being Element of dom T such that A4: q = t' &
not p is_a_prefix_of t' by A2;
thus T with-replacement (p,T1).q = T.q by A3,A4,TREES_1:8;
end;
theorem Th17:
for q st q in dom tree(T,P,T1) &
q in {p^s where p is Element of dom T, s is Element of dom T1 : p in P}
holds ex p' being Element of dom T, r being Element of dom T1 st
q = p'^r & p' in P & tree(T,P,T1).q = T1.r
proof let q; assume A1: q in dom tree(T,P,T1) &
q in {p^s where p is Element of dom T, s is Element of dom T1 : p in P};
per cases by A1,Th13;
suppose
A2: for p st p in P holds not p is_a_prefix_of q & tree(T,P,T1).q = T.q;
consider p' being Element of dom T, r being Element of dom T1
such that A3: q= p'^r & p' in P by A1;
now assume tree(T,P,T1).q <> T1.r;
not p' is_a_prefix_of q by A2,A3;
hence contradiction by A3,TREES_1:8;
end;
hence ex p' being Element of dom T, r being Element of dom T1 st
q = p'^r & p' in P & tree(T,P,T1).q = T1.r by A3;
suppose
ex p,r st p in P & r in dom T1 & q = p^r & tree(T,P,T1).q = T1.r;
then consider p,r such that
A4: p in P & r in dom T1 & q = p^r & tree(T,P,T1).q = T1.r;
consider p' being Element of dom T, r' being Element of dom T1
such that A5: q = p'^r' & p' in P by A1;
now assume A6: p <> p';
p,p' are_c=-comparable by A4,A5,Th1;
hence contradiction by A4,A5,A6,TREES_1:def 13;
end;
hence ex p' being Element of dom T, r being Element of dom T1 st
q = p'^r & p' in P & tree(T,P,T1).q = T1.r by A4;
end;
theorem Th18:
p in dom T implies for q st q in dom (T with-replacement (p,T1)) &
q in {p^s where s is Element of dom T1 : s = s}
holds ex r being Element of dom T1 st
q = p^r & T with-replacement (p,T1).q = T1.r
proof assume A1: p in dom T; let q;
assume A2: q in dom (T with-replacement (p,T1)) &
q in {p^s where s is Element of dom T1 : s = s};
per cases by A1,A2,Th14;
suppose A3: not p is_a_prefix_of q & T with-replacement (p,T1).q = T.q;
consider r being Element of dom T1 such that A4: q = p^r & r = r by A2;
thus ex r being Element of dom T1 st q = p^r &
T with-replacement (p,T1).q = T1.r by A3,A4,TREES_1:8;
suppose ex r st r in dom T1 & q = p^r & T with-replacement (p,T1).q = T1.r
;
hence ex r being Element of dom T1 st q = p^r &
T with-replacement (p,T1).q = T1.r;
end;
theorem
tree(T,{t},T1) = T with-replacement (t,T1)
proof
A1:dom tree(T,{t},T1) = dom (T with-replacement (t,T1))
proof
dom tree(T,{t},T1) = tree(dom T,{t},dom T1) by Def2
.= dom T with-replacement (t,dom T1) by Th10
.= dom (T with-replacement (t,T1)) by TREES_2:def 12;
hence thesis;
end;
for q st q in dom tree(T,{t},T1) holds tree(T,{t},T1).q =
T with-replacement (t,T1).q
proof let q; assume A2: q in dom tree(T,{t},T1);
then A3: q in tree(dom T,{t},dom T1) by Def2;
A4: tree(dom T,{t},dom T1) =
{t1 where t1 is Element of dom T :
for p st p in {t} holds not p is_a_prefix_of t1} \/
{ p^s where p is Element of dom T, s is Element of dom T1 : p in {t} }
by Th7;
per cases by A3,A4,XBOOLE_0:def 2;
suppose A5: q in {t1 where t1 is Element of dom T :
for p st p in {t} holds not p is_a_prefix_of t1};
then consider t' being Element of dom T such that A6: q = t' &
for p st p in {t} holds not p is_a_prefix_of t';
consider p such that A7: p = t; p in {t} by A7,TARSKI:def 1;
then A8: not p is_a_prefix_of t' by A6;
q in dom (T with-replacement (t,T1)) &
q in {t1 where t1 is Element of dom T : not p is_a_prefix_of t1}
implies T with-replacement (t,T1).q = T.q by A7,Th16;
hence tree(T,{t},T1).q = T with-replacement (t,T1).q by A1,A2,A5,A6,A8,
Th15;
suppose A9: q in { p'^s where p' is Element of dom T,
s is Element of dom T1 : p' in {t} };
then consider p being Element of dom T, r being Element of dom T1
such that A10: q = p^r & p in {t};
A11: q in { p^s where s is Element of dom T1 : s = s } by A10;
consider p1 being Element of dom T, r1 being Element of dom T1
such that A12: q = p1^r1 & p1 in {t} & tree(T,{t},T1).q = T1.r1 by A2,
A9,Th17;
A13: p1 = t & p = t by A10,A12,TARSKI:def 1;
then consider r2 being Element of dom T1
such that A14: q = p^r2 & (T with-replacement (p,T1)).q = T1.r2
by A1,A2,A11,Th18;
thus tree(T,{t},T1).q = T with-replacement (t,T1).q by A12,A13,A14,
FINSEQ_1:46;
end;
hence tree(T,{t},T1) = T with-replacement (t,T1) by A1,TREES_2:33;
end;
reserve D for non empty set,
T,T1 for DecoratedTree of D,
P for AntiChain_of_Prefixes of dom T;
definition let D,T,P,T1;
assume
A1: P<>{};
func tree(T,P,T1) -> DecoratedTree of D equals
tree(T,P,T1);
coherence
proof
consider T2 being DecoratedTree such that A2: T2 = tree(T,P,T1);
T2 is ParametrizedSubset of D
proof
thus rng T2 c= D
proof let y be set; assume y in rng T2;
then consider x being set such that
A3: x in dom T2 & y = T2.x by FUNCT_1:def 5;
x is Element of dom T2 by A3;
then reconsider q = x as FinSequence of NAT;
dom T2 = tree(dom T,P,dom T1) by A1,A2,Def2;
then A4: dom T2 = {t1 where t1 is Element of dom T :
for p st p in P holds not p is_a_prefix_of t1}
\/ { p^s where p is Element of dom T,
s is Element of dom T1 : p in P } by A1,Th7;
per cases by A3,A4,XBOOLE_0:def 2;
suppose A5: q in {t1 where t1 is Element of dom T :
for p st p in P holds not p is_a_prefix_of t1};
then A6: tree(T,P,T1).q = T.q by A1,A2,A3,Th15;
now
consider t' being Element of dom T such that A7: q = t' &
for p st p in P holds not p is_a_prefix_of t' by A5;
thus q in dom T by A7;
end;
then A8: y in rng T by A2,A3,A6,FUNCT_1:def 5;
rng T c= D by TREES_2:def 9;
hence y in D by A8;
suppose q in { p^s where p is Element of dom T,
s is Element of dom T1 : p in P };
then consider p being Element of dom T,r being Element of dom
T1
such that A9: q = p^r & p in P &
tree(T,P,T1).q = T1.r by A2,A3,Th17;
thus y in D by A2,A3,A9;
end;
end;
hence thesis by A2;
end;
end;