:: Replacement of Subtrees in a Tree
:: by Oleg Okhotnikov
::
:: Received October 1, 1995
:: Copyright (c) 1995-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies TREES_1, FINSEQ_1, NUMBERS, SUBSET_1, ORDINAL4, XBOOLE_0, TARSKI,
RELAT_1, XXREAL_0, ARYTM_3, TREES_2, FUNCT_1, TREES_A, NAT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0,
NAT_1, RELAT_1, FUNCT_1, FINSEQ_1, TREES_1, TREES_2;
constructors XXREAL_0, NAT_1, MEMBERED, TREES_2, RELSET_1, FINSEQ_2;
registrations XBOOLE_0, RELSET_1, MEMBERED, FINSEQ_1, TREES_2, XXREAL_0;
requirements NUMERALS, BOOLE, SUBSET;
definitions TARSKI, XBOOLE_0, TREES_1, TREES_2, RELAT_1;
expansions TARSKI, XBOOLE_0, TREES_1;
theorems TARSKI, FUNCT_1, FINSEQ_1, TREES_1, TREES_2, XBOOLE_0, XBOOLE_1,
RELAT_1, CARD_2;
schemes TREES_2;
begin
reserve T, T1 for Tree,
P for AntiChain_of_Prefixes of T,
p1 for FinSequence,
p, q, r, s, p9 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 p is_a_prefix_of s^r & s is_a_prefix_of p^q by TREES_1:1;
hence thesis by A1,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 P9 = P as Subset of T by TREES_1:def 11;
now
let x be object;
assume
A2: x in P9;
then reconsider x9 = x as FinSequence by TREES_1:def 10;
reconsider x9 as Element of T by A2;
now
let p such that
A3: p in P;
per cases;
suppose p <> x9;
then not p,x9 are_c=-comparable by A2,A3,TREES_1:def 10;
hence not p is_a_proper_prefix_of x9;
end;
suppose p = x9;
hence not p is_a_proper_prefix_of x9;
end;
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};
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 be object;
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 3;
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 3;
thus ProperPrefixes q c= X
proof
let x be object;
assume
A12: x in ProperPrefixes q;
then consider p1 such that
A13: x = p1 and
A14: p1 is_a_proper_prefix_of q by TREES_1:def 2;
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
A15: p in P;
ex t st q = t & for p st p in P holds not p
is_a_proper_prefix_of t by A10;
hence thesis by A14,A15,XBOOLE_1:56;
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 3;
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 and
A17: p in P by A4;
thus ProperPrefixes q c= X
proof
let x be object;
assume
A18: x in ProperPrefixes q;
then reconsider r = x as FinSequence by TREES_1:11;
r is_a_proper_prefix_of p^s by A16,A18,TREES_1:12;
then r is_a_prefix_of p^s;
then consider r1 being FinSequence such that
A19: p^s = r^r1 by TREES_1:1;
A20: now
assume len p <= len r;
then consider r2 being FinSequence such that
A21: p^r2 = r by A19,FINSEQ_1:47;
p^s = p^(r2^r1) by A19,A21,FINSEQ_1:32;
then s = r2^r1 by FINSEQ_1:33;
then s|(dom r2) = r2 by FINSEQ_1:21;
then A22: s|Seg(len r2) = r2 by FINSEQ_1:def 3;
then reconsider r2 as FinSequence of NAT by FINSEQ_1:18;
r2 is_a_prefix_of s by A22;
then reconsider r2 as Element of T1 by TREES_1:20;
r = p^r2 by A21;
then r in { w^v where w is Element of T,
v is Element of T1 : w in P } by A17;
hence r in X by A4,XBOOLE_0:def 3;
end;
now
assume len r <= len p;
then ex r2 being FinSequence st r^r2 = p by A19,FINSEQ_1:47;
then p|(dom r) = r by FINSEQ_1:21;
then A23: p|Seg(len r) = r by FINSEQ_1:def 3;
then reconsider r3 = r as FinSequence of NAT by FINSEQ_1:18;
A24: r3 is_a_prefix_of p by A23;
then reconsider r3 as Element of T by TREES_1:20;
for p9 st p9 in P holds not p9 is_a_proper_prefix_of r3
proof
let p9;
assume
A25: p9 in P;
assume
A26: p9 is_a_proper_prefix_of r3;
then p9 is_a_prefix_of r3;
then p9 is_a_prefix_of p by A24; then
A27: p,p9 are_c=-comparable;
per cases;
suppose p<>p9;
hence contradiction by A17,A25,A27,TREES_1:def 10;
end;
suppose p=p9;
hence contradiction by A24,A26,XBOOLE_0:def 8;
end;
end;
then r3 in { t : for p9 st p9 in P holds
not p9 is_a_proper_prefix_of t };
hence r in X by XBOOLE_0:def 3;
end;
hence thesis by A20;
end;
end;
hence thesis by A8,A9,XBOOLE_0:def 3;
end;
let q,k,n such that
A28: q^<*k*> in X and
A29: n <= k;
A30: now
assume
A31: 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 A29,TREES_1:def 3;
now
let p such that
A32: p in P;
assume p is_a_proper_prefix_of u;
then
A33: p is_a_prefix_of q by TREES_1:9;
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 by A31;
hence contradiction by A32,A33,TREES_1:8;
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 3;
end;
now
assume q^<*k*> in Z;
then consider p being Element of T, s being Element of T1 such that
A34: q^<*k*> = p^s and
A35: p in P by A4;
A36: now
assume len q <= len p;
then consider r being FinSequence such that
A37: q^r = p by A34,FINSEQ_1:47;
q^<*k*> = q^(r^s) by A34,A37,FINSEQ_1:32;
then A38: <*k*> = r^s by FINSEQ_1:33;
A39: now
assume
A40: r = <*k*>;
then reconsider s9 = q^<*n*> as Element of T by A29,A37,
TREES_1:def 3;
now
let p9 such that
A41: p9 in P;
assume
A42: p9 is_a_proper_prefix_of s9;
A43: len p = len q + len <*k*> by A37,A40,FINSEQ_1:22
.= len q + 1 by FINSEQ_1:40
.= len q + len <*n*> by FINSEQ_1:40
.= len s9 by FINSEQ_1:22;
per cases;
suppose p9 = p;
hence contradiction by A42,A43,CARD_2:102;
end;
suppose
A44: p9 <> p;
q is_a_prefix_of p & p9 is_a_prefix_of q
by A37,A42,TREES_1:1,9;
then p9 is_a_prefix_of p;
then p,p9 are_c=-comparable;
hence contradiction by A35,A41,A44,TREES_1:def 10;
end;
end;
hence q^<*n*> in { t : for p st p in P holds
not p is_a_proper_prefix_of t };
end;
now
assume that
A45: s = <*k*> and
A46: r = {};
s = <*>NAT^s by FINSEQ_1:34;
then <*>NAT^<*n*> in T1 by A29,A45,TREES_1:def 3;
then reconsider t = <*n*> as Element of T1 by FINSEQ_1:34;
q^<*n*> = p^t by A37,A46,FINSEQ_1:34;
hence q^<*n*> in Z by A4,A35;
end;
hence q^<*n*> in X by A38,A39,FINSEQ_1:88,XBOOLE_0:def 3;
end;
now
assume len p <= len q;
then consider r being FinSequence such that
A47: p^r = q by A34,FINSEQ_1:47;
p^(r^<*k*>) = p^s by A34,A47,FINSEQ_1:32;
then A48: r^<*k*> = s by FINSEQ_1:33;
then s|dom r = r by FINSEQ_1:21;
then s|Seg len r = r by FINSEQ_1:def 3;
then reconsider r as FinSequence of NAT by FINSEQ_1:18;
reconsider t = r^<*n*> as Element of T1 by A29,A48,TREES_1:def 3;
q^<*n*> = p^t by A47,FINSEQ_1:32;
then q^<*n*> in { p9^v where p9 is Element of T,
v is Element of T1 : p9 in P } by A35;
hence q^<*n*> in X by A4,XBOOLE_0:def 3;
end;
hence q^<*n*> in X by A36;
end;
hence q^<*n*> in X by A28,A30,XBOOLE_0:def 3;
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
A49: q in X;
A50: 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 A49,A50,XBOOLE_0:def 3;
end;
assume
A51: (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;
A52: (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
A53: p in P & r in T1 & q = p^r;
P c= T by TREES_1:def 11;
hence q in Z by A4,A53;
end;
hence thesis by A51,A52,XBOOLE_0:def 3;
end;
uniqueness
proof
let S1,S2 be Tree such that
A54: 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
A55: 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
A56: 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 A54,A56;
hence thesis by A55;
end;
assume
A57: 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 A55,A57;
hence thesis by A54;
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 object;
assume
A2: x in tree(T,P,T1);
then reconsider q = x as FinSequence of NAT by TREES_1:19;
A3: now
given p,r such that
A4: p in P & r in T1 & q = p^r;
P c= T by TREES_1:def 11;
hence x in { p9^s where p9 is Element of T,
s is Element of T1 : p9 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 3;
end;
let x be object 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 3;
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 object;
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 t9 being Element of T such that
A1: x = t9 and
A2: for p st p in P holds not p is_a_prefix_of t9;
for p st p in P holds not p is_a_proper_prefix_of t9 by A2;
hence thesis 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 object;
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 11;
then consider t9 being Element of T such that
A2: t9 = x by A1;
now
let p such that
A3: p in P;
per cases;
suppose t9 = p;
hence not p is_a_proper_prefix_of t9;
end;
suppose t9 <> p;
then not t9, p are_c=-comparable by A1,A2,A3,TREES_1:def 10;
hence not p is_a_proper_prefix_of t9;
end;
end;
hence thesis by A2;
end;
hence thesis;
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 object;
assume
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} \
{t1 where t1 is Element of T :
for p st p in P holds not p is_a_prefix_of t1};
then A2: x in {t1 where t1 is Element of T : for p st p in P holds not p
is_a_proper_prefix_of t1};
A3: 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 A1,XBOOLE_0:def 5;
assume
A4: 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 t9 being Element of T such that
A5: x = t9 and
A6: for p st p in P holds not p is_a_proper_prefix_of t9 by A2;
now
let p;
assume
A7: p in P;
then A8: not p is_a_proper_prefix_of t9 by A6;
per cases by A8;
suppose
not p is_a_prefix_of t9;
hence not p is_a_prefix_of t9;
end;
suppose
p = t9;
hence not p is_a_prefix_of t9 by A4,A5,A7;
end;
end;
hence thesis by A5;
end;
hence contradiction by A3;
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;
let x be object;
assume
A9: x in P;
A10: 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 ex t9 being Element of T st x = t9 & for p st p in P
holds not p is_a_prefix_of t9;
hence contradiction by A9;
end;
hence thesis by A9,A10,XBOOLE_0:def 5;
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 object;
assume
A1: x in P;
P c= T by TREES_1:def 11;
then consider q being Element of T such that
A2: q = x by A1;
<*> NAT in T1 by TREES_1:22;
then consider s9 being Element of T1 such that
A3: s9 = <*> NAT;
q = q^s9 by A3,FINSEQ_1:34;
thus
then x in { p^s where p is Element of T, s is Element of T1 : p in P }
by A1,A2;
end;
hence thesis;
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 object;
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;
end;
suppose
A5: not x in P;
now per cases by A3,XBOOLE_0:def 3;
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 5;
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;
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;
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;
end;
hence thesis by XBOOLE_0:def 3;
end;
thus thesis by A2,Th3,XBOOLE_1:9;
end;
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:22;
p = q^r by A2,A3,FINSEQ_1:34;
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 6;
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 6;
A7: now
assume that p^x in T and
A8: for r st r in P holds not r is_a_proper_prefix_of p^x;
A9: not p is_a_proper_prefix_of p^x by A1,A8;
p is_a_prefix_of p^x by TREES_1:1;
then p^x = p by A9
.= p^<*>NAT by FINSEQ_1:34;
then x = {} by FINSEQ_1:33;
hence thesis by TREES_1:22;
end;
now
given s,r such that
A10: s in P and
A11: r in T1 and
A12: p^x = s^r;
now
assume s <> p;
then not s,p are_c=-comparable by A1,A10,TREES_1:def 10;
hence contradiction by A12,Th1;
end;
hence thesis by A11,A12,FINSEQ_1:33;
end;
hence thesis by A1,A6,A7,Def1;
end;
end;
registration
let T;
cluster non empty for AntiChain_of_Prefixes of T;
existence
proof
set w = the Element of T;
consider X being set such that
A1: X = {w};
A2: X is AntiChain_of_Prefixes-like by A1,TREES_1:36;
X c= T
proof
let x be object;
assume x in X;
then x = w by A1,TARSKI:def 1;
hence thesis;
end;
then reconsider X as AntiChain_of_Prefixes of T by A2,TREES_1:def 11;
take X;
thus thesis by A1;
end;
end;
definition
let T;
let t be Element of T;
redefine func {t} -> AntiChain_of_Prefixes of T; :: redefines { (TARSKI, definition)
correctness by TREES_1:39;
end;
theorem Th9:
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 thesis by A1,A2,Def1,TREES_1:def 9;
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 thesis by A5,A6,Def1,TREES_1:def 9;
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 3;
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 TREES_2:sch 6(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 that
A11: q in dom D1 and
A12: D1.q <> D2.q;
thus contradiction
proof
per cases by A7,A8,A11;
suppose
A13: 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
A14: for p st p in P holds not p is_a_prefix_of q & D2.q = T.q;
consider x being object such that
A15: x in P by A1,XBOOLE_0:def 1;
P c= dom T by TREES_1:def 11;
then reconsider x as Element of dom T by A15;
A16: ex p9 st p9 = x;
then D1.q = T.q by A13,A15;
hence contradiction by A12,A14,A15,A16;
end;
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
A17: p2 in P and r2 in dom T1 and
A18: q = p2^r2 and D2.q = T1.r2;
not p2 is_a_prefix_of q by A13,A17;
hence contradiction by A18,TREES_1:1;
end;
end;
hence contradiction;
end;
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
A19: p1 in P and r1 in dom T1 and
A20: q = p1^r1 and
A21: 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 A19;
hence contradiction by A20,TREES_1:1;
end;
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
A22: p2 in P and r2 in dom T1 and
A23: q = p2^r2 and
A24: D2.q = T1.r2;
now
assume
A25: p1 <> p2;
p1,p2 are_c=-comparable by A20,A23,Th1;
hence contradiction by A19,A22,A25,TREES_1:def 10;
end;
hence contradiction by A12,A20,A21,A23,A24,FINSEQ_1:33;
end;
end;
hence contradiction;
end;
end;
end;
hence thesis by A7,A9,TREES_2:31;
end;
end;
theorem Th10:
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 Th11:
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 11;
hence thesis by A1,TREES_2:def 11;
end;
theorem Th12:
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 that
A2: q in dom tree(T,P,T1) and
A3: q in {t1 where t1 is Element of dom T : for p st p in P holds not p
is_a_prefix_of t1};
A4: ex t9 being Element of dom T st t9 = q & for p st p in P
holds not p is_a_prefix_of t9 by A3;
per cases by A2,Th10;
suppose
A5: for p st p in P holds not p is_a_prefix_of q & tree(T,P,T1).q = T.q;
consider x being object such that
A6: x in P by A1,XBOOLE_0:def 1;
P c= dom T by TREES_1:def 11;
then reconsider x as Element of dom T by A6;
ex p9 st p9 = x;
hence thesis by A5,A6;
end;
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 and r in dom T1 and
A8: q = p^r and tree(T,P,T1).q = T1.r;
not p is_a_prefix_of q by A4,A7;
hence thesis by A8,TREES_1:1;
end;
end;
theorem Th13:
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 that
A2: q in dom (T with-replacement (p,T1)) and
A3: q in {t1 where t1 is Element of dom T : not p is_a_prefix_of t1};
per cases by A1,A2,Th11;
suppose
not p is_a_prefix_of q & T with-replacement (p,T1).q = T.q;
hence thesis;
end;
suppose
A4: ex r st r in dom T1 & q = p^r & T with-replacement (p,T1).q = T1.r;
ex t9 being Element of dom T st q = t9 & not p is_a_prefix_of t9 by A3;
hence thesis by A4,TREES_1:1;
end;
end;
theorem Th14:
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 p9 being Element of dom T, r being Element of dom T1 st
q = p9^r & p9 in P & tree(T,P,T1).q = T1.r
proof
let q;
assume that
A1: q in dom tree(T,P,T1) and
A2: q in {p^s where p is Element of dom T, s is Element of dom T1 : p in P};
per cases by A1,Th10;
suppose
A3: for p st p in P holds not p is_a_prefix_of q & tree(T,P,T1).q = T.q;
consider p9 being Element of dom T, r being Element of dom T1 such that
A4: q= p9^r and
A5: p9 in P by A2;
tree(T,P,T1).q = T1.r by A4,TREES_1:1,A3,A5;
hence thesis by A4,A5;
end;
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
A6: p in P and
A7: r in dom T1 and
A8: q = p^r and
A9: tree(T,P,T1).q = T1.r;
consider p9 being Element of dom T, r9 being Element of dom T1 such that
A10: q = p9^r9 and
A11: p9 in P by A2;
now
assume
A12: p <> p9;
p,p9 are_c=-comparable by A8,A10,Th1;
hence contradiction by A6,A11,A12,TREES_1:def 10;
end;
hence thesis by A6,A7,A8,A9;
end;
end;
theorem Th15:
p in dom T implies for q st q in dom (T with-replacement (p,T1)) &
q in the set of all p^s where s is Element of dom T1
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 that
A2: q in dom (T with-replacement (p,T1)) and
A3: q in the set of all p^s where s is Element of dom T1;
per cases by A1,A2,Th11;
suppose
A4: not p is_a_prefix_of q & T with-replacement (p,T1).q = T.q;
ex r being Element of dom T1 st q = p^r by A3;
hence thesis by A4,TREES_1:1;
end;
suppose
ex r st r in dom T1 & q = p^r & T with-replacement (p,T1).q = T1.r;
hence thesis;
end;
end;
theorem
tree(T,{t},T1) = T with-replacement (t,T1)
proof
A1: dom tree(T,{t},T1) = tree(dom T,{t},dom T1) by Def2
.= dom T with-replacement (t,dom T1) by Th9
.= dom (T with-replacement (t,T1)) by TREES_2:def 11;
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 3;
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 t9 being Element of dom T such that
A6: q = t9 and
A7: for p st p in {t} holds not p is_a_prefix_of t9;
consider p such that
A8: p = t;
p in {t} by A8,TARSKI:def 1;
then A9: not p is_a_prefix_of t9 by A7;
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 A8,Th13;
hence thesis by A1,A2,A5,A6,A9,Th12;
end;
suppose
A10: q in { p9^s where p9 is Element of dom T,
s is Element of dom T1 : p9 in {t} };
then consider p being Element of dom T, r being Element of dom T1
such that
A11: q = p^r and
A12: p in {t};
A13: q in the set of all p^s where s is Element of dom T1 by A11;
consider p1 being Element of dom T, r1 being Element of dom T1 such that
A14: q = p1^r1 and
A15: p1 in {t} and
A16: tree(T,{t},T1).q = T1.r1 by A2,A10,Th14;
A17: p1 = t by A15,TARSKI:def 1;
A18: p = t by A12,TARSKI:def 1;
then ex r2 being Element of dom T1 st q = p^r2 & (T
with-replacement (p,T1)).q = T1.r2 by A1,A2,A13,Th15;
hence thesis by A14,A16,A17,A18,FINSEQ_1:33;
end;
end;
hence thesis by A1,TREES_2:31;
end;
reserve D for non empty set,
T,T1 for DecoratedTree of D,
P for non empty AntiChain_of_Prefixes of dom T;
registration
let D,T,P,T1;
cluster tree(T,P,T1) -> D-valued;
coherence
proof
set T2 = tree(T,P,T1);
let y be object;
assume y in rng T2;
then consider x being object such that
A2: x in dom T2 and
A3: y = T2.x by FUNCT_1:def 3;
x is Element of dom T2 by A2;
then reconsider q = x as FinSequence of NAT;
dom T2 = tree(dom T,P,dom T1) by 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 Th7;
per cases by A2,A4,XBOOLE_0:def 3;
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 A2,Th12;
now
ex t9 being Element of dom T st q = t9 & for p st p in P
holds not p is_a_prefix_of t9 by A5;
hence q in dom T;
end; then
A7: y in rng T by A3,A6,FUNCT_1:def 3;
rng T c= D by RELAT_1:def 19;
hence thesis by A7;
end;
suppose q in { p^s where p is Element of dom T,
s is Element of dom T1 : p in P };
then 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 A2,Th14;
hence thesis by A3;
end;
end;
end;