:: Joining of Decorated Trees
:: by Grzegorz Bancerek
::
:: Received October 8, 1993
:: Copyright (c) 1993-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 NUMBERS, TREES_2, SUBSET_1, RELAT_1, FINSEQ_1, FUNCT_1, TARSKI,
TREES_1, XXREAL_0, ARYTM_3, CARD_1, FUNCOP_1, XBOOLE_0, TREES_3,
ZFMISC_1, NAT_1, FINSEQ_2, TREES_A, ORDINAL4, FUNCT_6, FINSEQ_4, MCART_1,
PARTFUN1, TREES_4;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
NAT_1, RELAT_1, FUNCT_1, DOMAIN_1, FUNCOP_1, FUNCT_3, FINSEQ_1, FINSEQ_2,
TREES_1, TREES_2, FUNCT_6, TREES_3, XXREAL_0;
constructors BINOP_1, DOMAIN_1, XXREAL_0, XREAL_0, NAT_1, FUNCT_5, FINSEQ_2,
FUNCT_6, TREES_3, RELSET_1, NUMBERS;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, XREAL_0,
FINSEQ_1, TREES_2, TREES_3, CARD_1, FINSEQ_2, FUNCOP_1, TREES_1,
XTUPLE_0;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, FINSEQ_1, TREES_1, TREES_2;
equalities FINSEQ_1, TREES_2, FINSEQ_2, FUNCT_6;
expansions TARSKI, FINSEQ_1;
theorems TARSKI, ZFMISC_1, FINSEQ_1, NAT_1, FUNCT_1, FUNCT_2, FUNCOP_1,
FUNCT_6, FINSEQ_2, FINSEQ_3, TREES_1, TREES_2, TREES_3, RELAT_1,
XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, FUNCT_5, ORDINAL1, CARD_1;
schemes CLASSES1, FINSEQ_1, XBOOLE_0;
begin :: Joining of decorated trees
definition
let T be DecoratedTree;
mode Node of T is Element of dom T;
end;
reserve x, y, z for object,
i, j, n for Nat,
p, q, r for FinSequence,
v for FinSequence of NAT;
Lm1: now
let x be set, y;
let p be FinSequence of x;
assume y in dom p or y in dom p;
then A1: p.y in rng p by FUNCT_1:def 3;
rng p c= x by FINSEQ_1:def 4;
hence p.y in x by A1;
end;
definition
let T1, T2 be DecoratedTree;
redefine pred T1 = T2 means :: redefines = (FUNCT_1, redefinition) → = (RELAT_1, redefinition) → = (XBOOLE_0, redefinition) → = (HIDDEN, definition)
dom T1 = dom T2 & for p being Node of T1 holds T1.p = T2.p;
compatibility
proof
(for p being Node of T1 holds T1.p = T2.p) & dom T1 = dom T2 implies
for x being object st x in dom T1 holds T1.x = T2.x;
hence thesis by FUNCT_1:2;
end;
end;
theorem Th1:
for i,j being Nat
st elementary_tree i c= elementary_tree j holds i <= j
proof
let i,j be Nat;
assume that
A1: elementary_tree i c= elementary_tree j and
A2: i > j;
reconsider j as Element of NAT by ORDINAL1:def 12;
<*j*> in elementary_tree i by A2,TREES_1:28;
then A3: ex n being Nat st n < j & <*j*> = <*n*> by A1,TREES_1:30;
<*j*>.1 = j;
hence thesis by A3,FINSEQ_1:40;
end;
theorem Th2:
for i,j being Nat
st elementary_tree i = elementary_tree j holds i = j
proof
let i,j be Nat;
assume elementary_tree i = elementary_tree j;
then i <= j & i >= j by Th1;
hence thesis by XXREAL_0:1;
end;
Lm2: n < len p implies n+1 in dom p & p.(n+1) in rng p
proof
assume
A1: n < len p;
n >= 0 by NAT_1:2;
then A2: n+1 >= 0+1 by XREAL_1:7;
n+1 <= len p by A1,NAT_1:13;
then n+1 in dom p by A2,FINSEQ_3:25;
hence thesis by FUNCT_1:def 3;
end;
Lm3: now
let n; let x be set;
let p be FinSequence of x;
assume n < len p;
then A1: p.(n+1) in rng p by Lm2;
rng p c= x by FINSEQ_1:def 4;
hence p.(n+1) in x by A1;
end;
definition
let x be object;
func root-tree x -> DecoratedTree equals
(elementary_tree 0) --> x;
correctness;
end;
definition
let D be non empty set, d be Element of D;
redefine func root-tree d -> Element of FinTrees D; :: redefines root-tree (TREES_4, definition)
coherence
proof
dom ((elementary_tree 0) --> d) = elementary_tree 0;
hence thesis by TREES_3:def 8;
end;
end;
theorem Th3:
dom root-tree x = elementary_tree 0 & (root-tree x).{} = x
proof
{} in elementary_tree 0 by TARSKI:def 1,TREES_1:29;
hence thesis by FUNCOP_1:7;
end;
theorem
root-tree x = root-tree y implies x = y
proof
(root-tree x).{} = x by Th3;
hence thesis by Th3;
end;
theorem Th5:
for T being DecoratedTree st dom T = elementary_tree 0 holds
T = root-tree (T.{}) by TARSKI:def 1,TREES_1:29;
theorem
root-tree x = {[{},x]}
proof
thus root-tree x = [:{{}},{x}:] by FUNCOP_1:def 2,TREES_1:29
.= {[{},x]} by ZFMISC_1:29;
end;
definition
let x;
let p be FinSequence;
func x-flat_tree(p) -> DecoratedTree means
:
Def3: dom it = elementary_tree len p & it.{} = x &
for n st n < len p holds it.<*n*> = p.(n+1);
existence
proof
defpred X[object,object] means
$1 = {} & $2 = x or ex n st $1 = <*n*> & $2 = p.(n+1);
A1: for z being object st z in elementary_tree len p
ex y being object st X[z,y]
proof
let z be object;
assume z in elementary_tree len p;
then reconsider z as Element of elementary_tree len p;
reconsider z as FinSequence of NAT;
A2: z = {} or ex n st n < len p & z = <*n*> by TREES_1:30;
now
given n such that
A3: z = <*n*> and n < len p;
take y = p.(n+1),n;
thus z = <*n*> & y = p.(n+1) by A3;
end;
hence thesis by A2;
end;
consider f being Function such that
A4: dom f = elementary_tree len p & for y being object st y in
elementary_tree len p holds X[y,f.y] from CLASSES1:sch 1(A1);
reconsider f as DecoratedTree by A4,TREES_2:def 8;
take f;
thus dom f = elementary_tree len p by A4;
{} in dom f & for n st {} = <*n*> holds f.{} <> p.(n+1) by TREES_1:22;
hence f.{} = x by A4;
let n;
assume n < len p;
then <*n*> in dom f by A4,TREES_1:28;
then consider k being Nat such that
A5: <*n*> = <*k*> and
A6: f.<*n*> = p.(k+1) by A4;
k = <*n*>.1 by A5,FINSEQ_1:40
.= n;
hence thesis by A6;
end;
uniqueness
proof
let T1, T2 be DecoratedTree such that
A7: dom T1 = elementary_tree len p and
A8: T1.{} = x and
A9: for n st n < len p holds T1.<*n*> = p.(n+1) and
A10: dom T2 = elementary_tree len p and
A11: T2.{} = x and
A12: for n st n < len p holds T2.<*n*> = p.(n+1);
now
let x be object;
assume x in elementary_tree len p;
then reconsider x9 = x as Element of elementary_tree len p;
A13: x9 = {} or ex n st n < len p & x9 = <*n*> by TREES_1:30;
now
given n such that
A14: n < len p & x = <*n*>;
thus T1.x = p.(n+1) by A9,A14
.= T2.x by A12,A14;
end;
hence T1.x = T2.x by A8,A11,A13;
end;
hence thesis by A7,A10;
end;
end;
theorem
x-flat_tree p = y-flat_tree q implies x = y & p = q
proof
assume
A1: x-flat_tree p = y-flat_tree q;
(x-flat_tree p).{} = x by Def3;
hence x = y by A1,Def3;
A2: dom (x-flat_tree p) = elementary_tree len p & dom (y-flat_tree q) =
elementary_tree len q by Def3;
then A3: len p = len q by A1,Th2;
now
let i be Nat;
assume that
A4: i >= 1 and
A5: i <= len p;
consider n be Nat such that
A6: i = 1+n by A4,NAT_1:10;
A7: n in NAT & n < len p by A5,A6,NAT_1:13,ORDINAL1:def 12;
then p.i = (x-flat_tree p).<*n*> by A6,Def3;
hence p.i = q.i by A1,A3,A6,A7,Def3;
end;
hence thesis by A1,A2,Th2;
end;
theorem Th8:
for j being Element of NAT st j < i
holds (elementary_tree i)|<*j*> = elementary_tree 0
proof let j be Element of NAT;
set p = i |-> elementary_tree 0, T = tree(p);
assume
A1: j < i;
then A2: 1+j >= 1 & j+1 <= i by NAT_1:11,13;
len p = i by CARD_1:def 7;
then A3: elementary_tree i = T & T|<*j*> = p.(j+1) by A1,TREES_3:49,54;
j+1 in Seg i by A2;
hence thesis by A3,FUNCOP_1:7;
end;
theorem Th9:
for i being Element of NAT st i < len p
holds (x-flat_tree p)|<*i*> = root-tree (p.(i+1))
proof let i be Element of NAT;
reconsider t = {} as Element of (dom (x-flat_tree p))|<*i*> by TREES_1:22;
assume
A1: i < len p;
then A2: (x-flat_tree p).<*i*> = p.(i+1) by Def3;
A3: dom (x-flat_tree p) = elementary_tree len p by Def3;
(elementary_tree len p)|<*i*> = elementary_tree 0 by A1,Th8;
then
A4: dom ((x-flat_tree p)|<*i*>) = elementary_tree 0 by A3,TREES_2:def 10;
<*
i*>^t = <*i*> & ((x-flat_tree p)|<*i*>).t = (x-flat_tree p).(<*i*>^t) by
FINSEQ_1:34,TREES_2:def 10;
hence thesis by A2,A4,Th5;
end;
definition
let x be object, p such that
A1: p is DTree-yielding;
func x-tree(p) -> DecoratedTree means
: Def4:
( ex q being DTree-yielding FinSequence st p = q & dom it = tree(doms q)) &
it.{} = x &
for n being Nat st n < len p holds it|<*n*> = p.(n+1);
existence
proof
reconsider pp=p as Function-yielding FinSequence by A1;
A2: dom doms pp = dom p by A1,TREES_3:37;
reconsider q = doms pp as Tree-yielding FinSequence by A1;
defpred X[object,object] means $1 = {} & $2 = x or $1 <> {} &
ex n,r st $1 = <*n*>^r & $2 = p..(n+1,r);
A3: for y being object st y in tree(q) ex z being object st X[y,z]
proof
let y be object;
assume y in tree(q);
then reconsider s = y as Element of tree(q);
now
assume y <> {};
then consider w being (FinSequence of NAT),
n being Element of NAT such that
A4: s = <*n*>^w by FINSEQ_2:130;
reconsider w as FinSequence;
take z = p..(n+1,w);
thus y = {} & z = x or y <> {} &
ex n,r st y = <*n*>^r & z = p..(n+1,r) by A4;
end;
hence thesis;
end;
consider T being Function such that
A5: dom T = tree(q) & for y being object st y in tree(q) holds X[y,T.y]
from CLASSES1:sch 1(A3);
reconsider T as DecoratedTree by A5,TREES_2:def 8;
take T;
thus ex q being DTree-yielding FinSequence st p = q & dom T = tree(doms q)
by A1,A5;
{} in tree(q) by TREES_1:22;
hence T.{} = x by A5;
A6: len p = len q by A2,FINSEQ_3:29;
let n be Nat;
assume
A7: n < len p;
then A8: n+1 in dom p by Lm2;
then reconsider t = p.(n+1) as DecoratedTree by A1,TREES_3:24;
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
A9: dom t = q.(n+1) by A8,FUNCT_6:22;
A10: dom t = q.(n+1) by A8,FUNCT_6:22
.= (dom T)|<*nn*> by A5,A6,A7,TREES_3:49;
A11: (dom T)|<*n*> = dom (T|<*n*>) by TREES_2:def 10;
now
let r be FinSequence of NAT;
assume
A12: r in dom t;
then <*n*>^r in dom T by A5,A6,A7,A9,TREES_3:def 15;
then consider m being Nat, s being FinSequence such that
A13: <*n*>^r = <*m*>^s and
A14: T.(<*n*>^r) = p..(m+1,s) by A5;
A15: (<*n*>^r).1 = n & (<*m*>^s).1 = m by FINSEQ_1:41;
then m+1 in dom p & r = s by A7,A13,Lm2,FINSEQ_1:33;
then p..(m+1,s) = t.r by A12,A13,A15,FUNCT_5:38;
hence (T|<*n*>).r = t.r by A10,A12,A14,TREES_2:def 10;
end;
hence thesis by A10,A11,TREES_2:31;
end;
uniqueness
proof
let T1, T2 be DecoratedTree;
given q1 being DTree-yielding FinSequence such that
A16: p = q1 and
A17: dom T1 = tree(doms q1);
assume that
A18: T1.{} = x and
A19: for n being Nat st n < len p holds T1|<*n*> = p.(n+1);
given q2 being DTree-yielding FinSequence such that
A20: p = q2 & dom T2 = tree(doms q2);
assume that
A21: T2.{} = x and
A22: for n being Nat st n < len p holds T2|<*n*> = p.(n+1);
now
let q be FinSequence of NAT;
assume
A23: q in dom T1;
now
assume q <> {};
then consider s being FinSequence of NAT,
n being Element of NAT such that
A24: q = <*n*>^s by FINSEQ_2:130;
A25: <*n*> in dom T1 by A23,A24,TREES_1:21;
A26: n < len doms q1 by A17,A23,A24,TREES_3:48;
len doms q1 = len p by A16,TREES_3:38;
then A27: T1|<*n*> = p.(n+1) & T2|<*n*> = p.(n+1) by A19,A22,A26;
A28: s in (dom T1)|<*n*> by A23,A24,A25,TREES_1:def 6;
then T1.q = (T1|<*n*>).s by A24,TREES_2:def 10;
hence T1.q = T2.q by A16,A17,A20,A24,A27,A28,TREES_2:def 10;
end;
hence T1.q = T2.q by A18,A21;
end;
hence thesis by A16,A17,A20;
end;
end;
definition
let x be object;
let T be DecoratedTree;
func x-tree T -> DecoratedTree equals
x-tree <*T*>;
correctness;
end;
definition
let x be object;
let T1, T2 be DecoratedTree;
func x-tree (T1,T2) -> DecoratedTree equals
x-tree <*T1,T2*>;
correctness;
end;
theorem Th10:
for p being DTree-yielding FinSequence holds dom (x-tree(p)) = tree(doms p)
proof
let p be DTree-yielding FinSequence;
ex q being DTree-yielding FinSequence st
p = q & dom (x-tree(p)) = tree(doms q) by Def4;
hence thesis;
end;
theorem Th11:
for p being DTree-yielding FinSequence holds
y in dom (x-tree(p)) iff y = {} or
ex i being Nat, T being DecoratedTree, q being Node of T st
i < len p & T = p.(i+1) & y = <*i*>^q
proof
let p be DTree-yielding FinSequence;
A1: dom (x-tree p) = tree(doms p) by Th10;
A2: now
given i,q such that
A3: i < len doms p and
A4: q in (doms p).(i+1) and
A5: y = <*i*>^q;
len doms p = len p by TREES_3:38;
then A6: i+1 in dom p by A3,Lm2;
then reconsider T = p.(i+1) as DecoratedTree by TREES_3:24;
take i, T;
reconsider q as Node of T by A4,A6,FUNCT_6:22;
take q;
thus i < len p & T = p.(i+1) & y = <*i*>^q by A3,A5,TREES_3:38;
end;
now
given i being Nat, T being DecoratedTree, q being Node of T
such that
A7: i < len p and
A8: T = p.(i+1) and
A9: y = <*i*>^q;
reconsider q as FinSequence;
take i, q;
i+1 in dom p by A7,Lm2;
then (doms p).(i+1) = dom T by A8,FUNCT_6:22;
hence i < len doms p & q in (doms p).(i+1) & y = <*i*>^q by A7,A9,
TREES_3:38;
end;
hence thesis by A1,A2,TREES_3:def 15;
end;
theorem Th12:
for p being DTree-yielding FinSequence for i being Nat,
T being DecoratedTree, q being Node of T st i < len p &
T = p.(i+1) holds (x-tree p).(<*i*>^q) = T.q
proof
let p be DTree-yielding FinSequence, n be Nat,
T be DecoratedTree;
let q be Node of T;
assume
A1: n < len p & T = p.(n+1);
reconsider n as Element of NAT by ORDINAL1:def 12;
A2: <*n*>^q in dom (x-tree(p)) by Th11,A1;
then <*n*> in dom (x-tree(p)) by TREES_1:21;
then q in (dom (x-tree p))|<*n*> by A2,TREES_1:def 6;
then ((x-tree(p))|<*n*>).q = (x-tree(p)).(<*n*>^q) by TREES_2:def 10;
hence thesis by A1,Def4;
end;
theorem
for T being DecoratedTree holds dom (x-tree T) = ^dom T
proof
let T be DecoratedTree;
dom (x-tree <*T*>) = tree(doms <*T*>) & doms <*T*> = <*dom T*> by Th10,
FINSEQ_3:132;
hence thesis by TREES_3:def 16;
end;
theorem
for T1, T2 being DecoratedTree holds
dom (x-tree (T1,T2)) = tree(dom T1, dom T2)
proof
let T1, T2 be DecoratedTree;
dom
(x-tree <*T1,T2*>) = tree(doms <*T1,T2*>) & doms <*T1,T2*> = <*dom T1,
dom T2*> by Th10,FINSEQ_3:133;
hence thesis by TREES_3:def 17;
end;
theorem
for p,q being DTree-yielding FinSequence st x-tree p = y-tree q holds
x = y & p = q
proof
let p,q be DTree-yielding FinSequence;
assume
A1: x-tree p = y-tree q;
(x-tree p).{} = x by Def4;
hence x = y by A1,Def4;
dom (x-tree p) = tree(doms p) & dom (y-tree q) = tree(doms q) by Th10;
then A2: doms p = doms q by A1,TREES_3:50;
dom p = dom doms p & dom doms q = dom q by TREES_3:37;
then A3: len p = len q by A2,FINSEQ_3:29;
now
let i be Nat;
assume that
A4: i >= 1 and
A5: i <= len p;
consider n be Nat such that
A6: i = 1+n by A4,NAT_1:10;
reconsider n as Element of NAT by ORDINAL1:def 12;
A7: n < len p by A5,A6,NAT_1:13;
then p.i = (x-tree p)|<*n*> by A6,Def4;
hence p.i = q.i by A1,A3,A6,A7,Def4;
end;
hence thesis by A3;
end;
theorem
root-tree x = y-flat_tree p implies x = y & p = {}
proof
assume
A1: root-tree x = y-flat_tree p;
thus x = (root-tree x).{} by Th3
.= y by A1,Def3;
dom (y-flat_tree p) = elementary_tree len p by Def3;
hence thesis by A1,Th2;
end;
theorem
root-tree x = y-tree p & p is DTree-yielding implies x = y & p = {}
proof
assume that
A1: root-tree x = y-tree p and
A2: p is DTree-yielding;
reconsider p9 = p as DTree-yielding FinSequence by A2;
thus x = (root-tree x).{} by Th3
.= y by A1,A2,Def4;
dom (y-tree p) = tree(doms p9) by Th10;
then A3: doms p9 = {} by A1,TREES_3:50,52;
dom doms p9 = dom p by TREES_3:37;
hence thesis by A3;
end;
theorem
x-flat_tree p = y-tree q & q is DTree-yielding implies x = y &
len p = len q & for i st i in dom p holds q.i = root-tree (p.i)
proof
assume that
A1: x-flat_tree p = y-tree q and
A2: q is DTree-yielding;
reconsider q9 = q as DTree-yielding FinSequence by A2;
thus x = (x-flat_tree p).{} by Def3
.= y by A1,A2,Def4;
tree((len p)|->elementary_tree 0) = elementary_tree len p by TREES_3:54
.= dom (x-flat_tree p) by Def3
.= tree(doms q9) by A1,Th10;
then A3: (len p)|->elementary_tree 0 = doms q9 by TREES_3:50;
len doms q9 = len q by TREES_3:38;
thus
then A4: len p = len q by A3,CARD_1:def 7;
let i;
assume
A5: i in dom p;
then A6: i >= 1 by FINSEQ_3:25;
A7: i <= len p by A5,FINSEQ_3:25;
consider n being Nat such that
A8: i = 1+n by A6,NAT_1:10;
reconsider n as Element of NAT by ORDINAL1:def 12;
A9: n < len p by A7,A8,NAT_1:13;
then (x-flat_tree p)|<*n*> = root-tree (p.i) by A8,Th9;
hence thesis by A1,A2,A4,A8,A9,Def4;
end;
theorem
for p being DTree-yielding FinSequence, n being Nat,
q being FinSequence st <*n*>^q in dom (x-tree(p)) holds
(x-tree(p)).(<*n*>^q) = p..(n+1,q)
proof
let p be DTree-yielding FinSequence, n be Nat, q be FinSequence;
assume
A1: <*n*>^q in dom (x-tree(p));
then <*n*>^q is Node of (x-tree(p));
then reconsider q9 = q as FinSequence of NAT by FINSEQ_1:36;
reconsider n as Element of NAT by ORDINAL1:def 12;
A2: <*n*> in dom (x-tree p) by A1,TREES_1:21;
A3: <*n*>^q in tree(doms p) by A1,Th10;
A4: len doms p = len p by TREES_3:38;
A5: q9 in (dom (x-tree p))|<*n*> by A1,A2,TREES_1:def 6;
A6: n < len p by A3,A4,TREES_3:48;
A7: dom
((x-tree p)|<*n*>) = (dom (x-tree p))|<*n*> & ((x-tree(p))|<*n*>).q9 = (
x-tree(p)).(<*n*>^q) by A5,TREES_2:def 10;
n+1 in dom p & p.(n+1) = (x-tree(p))|<*n*> by A6,Def4,Lm2;
hence thesis by A5,A7,FUNCT_5:38;
end;
theorem
x-flat_tree({}) = root-tree x & x-tree({}) = root-tree x
proof
len {} = 0;
then A1: dom (x-flat_tree {}) = elementary_tree 0 by Def3;
now
let y be object;
assume y in elementary_tree 0;
then y = {} by TARSKI:def 1,TREES_1:29;
hence (x-flat_tree {}).y = x by Def3;
end;
hence x-flat_tree({}) = root-tree x by A1;
reconsider e = {} as DTree-yielding FinSequence;
A2: dom (x-tree {}) = tree(doms e) by Th10
.= elementary_tree 0 by FUNCT_6:23,TREES_3:52;
now
let y be object;
assume y in elementary_tree 0;
then y = {} by TARSKI:def 1,TREES_1:29;
hence (x-tree e).y = x by Def4;
end;
hence thesis by A2;
end;
theorem
x-flat_tree(<*y*>) =
((elementary_tree 1) --> x) with-replacement (<*0*>, root-tree y)
proof
set T = ((elementary_tree 1) --> x) with-replacement (<*0*>, root-tree y);
A1: dom (x-flat_tree <*y*>) = elementary_tree len <*y*> by Def3
.= elementary_tree 1 by FINSEQ_1:40;
A2: dom root-tree y = elementary_tree 0;
A3: dom ((elementary_tree 1) --> x) = elementary_tree 1 & <*0*> in
elementary_tree 1 by TARSKI:def 2,TREES_1:51;
then A4: dom T = elementary_tree 1 with-replacement (<*0*>, elementary_tree 0 )
by A2,TREES_2:def 11
.= elementary_tree 1 by TREES_3:58,67;
now
let z be object;
assume z in elementary_tree 1;
then A5: z = {} or z = <*0*> by TARSKI:def 2,TREES_1:51;
A6: {} in elementary_tree 1 by TARSKI:def 2,TREES_1:51;
A7: not <*0*> is_a_prefix_of {};
A8: len <*y*> = 1 by FINSEQ_1:40;
A9: <*y*>.1 = y & (x-flat_tree <*y*>).{} = x by Def3;
A10: T.{} = ((elementary_tree 1) --> x).{} by A3,A6,A7,TREES_3:45;
A11: (x-flat_tree <*y*>).<*0*> = <*y*>.(0+1) by A8,Def3;
T.<*0*> = (root-tree y).{} by A3,TREES_3:44;
hence
T.z = (x-flat_tree <*y*>).z by A5,A6,A9,A10,A11,Th3,FUNCOP_1:7;
end;
hence thesis by A1,A4;
end;
theorem
for T being DecoratedTree holds
x-tree(<*T*>) = ((elementary_tree 1) --> x) with-replacement (<*0*>, T)
proof
let T be DecoratedTree;
set D = ((elementary_tree 1) --> x) with-replacement (<*0*>, T);
set W = elementary_tree 1 with-replacement(<*0*>,dom T);
A1: dom (x-tree <*T*>) = tree(doms <*T*>) by Th10
.= tree(<*dom T*>) by FINSEQ_3:132
.= ^dom T by TREES_3:def 16
.= W by TREES_3:58;
A2: dom ((elementary_tree 1) --> x) = elementary_tree 1;
reconsider t1 = {}, t2 = <*0*> as Element of elementary_tree 1
by TARSKI:def 2,TREES_1:51;
t2 = t2;
then A3: dom D = W by A2,TREES_2:def 11;
A4: {} in dom T by TREES_1:22;
now
let y be object;
assume y in W;
then reconsider q = y as Element of W;
q
in elementary_tree 1 or ex v st v in dom T & q = t2^v by TREES_1:def 9;
then A5: q = {} or q = t2 & t2 = t2^t1 or
ex v st v in dom T & q = <*0*>^v by FINSEQ_1:34,TARSKI:def 2,TREES_1:51;
not t2 is_a_prefix_of t1;
then A6: D.{} = ((elementary_tree 1)-->x).t1 by A2,TREES_3:45
.= x
.= (x-tree <*T*>).{} by Def4;
now
given r being FinSequence of NAT such that
A7: r in dom T and
A8: q = <*0*>^r;
reconsider r as Node of T by A7;
q = t2^r by A8;
then A9: D.q = T.r by A2,TREES_3:46;
len <*T*> = 1 & <*T*>.(0+1) = T by FINSEQ_1:40;
then A10: (x-tree <*T*>)|t2 = T by Def4;
W|t2 = dom T by TREES_1:33;
hence D.q = (x-tree <*T*>).q by A1,A8,A9,A10,TREES_2:def 10;
end;
hence D.y = (x-tree <*T*>).y by A4,A5,A6;
end;
hence thesis by A1,A3;
end;
registration
let D be non empty set, d be Element of D, p be FinSequence of D;
cluster d-flat_tree(p) -> D-valued;
coherence
proof
set T = d-flat_tree(p);
rng T c= D
proof
let x be object;
assume x in rng T;
then consider y being object such that
A1: y in dom T and
A2: x = T.y by FUNCT_1:def 3;
reconsider y as Node of T by A1;
A3: dom T = elementary_tree len p by Def3;
A4: T.{} = d by Def3;
now
assume y <> {};
then consider n such that
A5: n < len p & y = <*n*> by A3,TREES_1:30;
A6: T.y = p.(n+1) & p.(n+1) in rng p by A5,Def3,Lm2;
rng p c= D by FINSEQ_1:def 4;
hence thesis by A2,A6;
end;
hence thesis by A2,A4;
end;
hence thesis by RELAT_1:def 19;
end;
end;
registration
let D be non empty set, F be non empty DTree-set of D;
let d be Element of D, p be FinSequence of F;
cluster d-tree(p) -> D-valued;
coherence
proof
set T = d-tree(p);
rng T c= D
proof
let x be object;
assume x in rng T;
then consider y being object such that
A1: y in dom T and
A2: x = T.y by FUNCT_1:def 3;
reconsider y as Node of T by A1;
A3: tree(doms p)-level 1 = {<*n*>: n < len doms p} by TREES_3:49;
A4: T.{} = d by Def4;
A5: tree(doms p) = dom T & len doms p = len p by Th10,TREES_3:38;
now
assume y <> {};
then consider q being FinSequence of NAT,
n being Element of NAT such that
A6: y = <*n*>^q by FINSEQ_2:130;
A7: <*n*> in dom T by A6,TREES_1:21;
A8: len <*n*> = 1 by FINSEQ_1:40;
A9: q in (dom T)|<*n*> by A6,A7,TREES_1:def 6;
A10: <*n*> in (dom T)-level 1 by A7,A8;
A11: dom (T|<*n*>) = (dom T)|<*n*> by TREES_2:def 10;
consider i such that
A12: <*n*> = <*i*> & i < len p by A3,A5,A10;
A13: <*n*>.1 = n & <*i*>.1 = i;
then A14: T|<*n*> = p.(n+1) by A12,Def4;
A15: p.(n+1) in rng p by A12,A13,Lm2;
rng p c= F by FINSEQ_1:def 4;
then reconsider t = p.(n+1) as Element of F by A15;
A16: t.q = x by A2,A6,A9,A14,TREES_2:def 10;
A17: t.q in rng t by A9,A11,A14,FUNCT_1:def 3;
rng t c= D by RELAT_1:def 19;
hence thesis by A16,A17;
end;
hence thesis by A2,A4;
end;
hence thesis by RELAT_1:def 19;
end;
end;
registration
let D be non empty set, d be Element of D, T be DecoratedTree of D;
cluster d-tree T -> D-valued;
coherence
proof
reconsider T as Element of Trees D by TREES_3:def 7;
reconsider t = <*T*> as Element of (Trees D)* by FINSEQ_1:def 11;
d-tree T = d-tree t;
hence thesis;
end;
end;
registration
let D be non empty set, d be Element of D, T1, T2 be DecoratedTree of D;
cluster d-tree(T1, T2) -> D-valued;
coherence
proof
reconsider T1, T2 as Element of Trees D by TREES_3:def 7;
<*T1,T2*> = <*T1 qua Element of Trees D qua non empty set*>^
<*T2 qua Element of Trees D qua non empty set*>;
then
reconsider t = <*T1,T2*> as Element of (Trees D)* by FINSEQ_1:def 11;
d-tree(T1, T2) = d-tree t;
hence thesis;
end;
end;
definition
let D be non empty set;
let p be FinSequence of FinTrees D;
redefine func doms p -> FinSequence of FinTrees; :: redefines doms (FUNCT_6, definition)
coherence
proof
A1: dom doms p = dom p by TREES_3:37;
A2: rng p c= FinTrees D by FINSEQ_1:def 4;
thus doms p is FinSequence of FinTrees
proof
let x be object;
assume x in rng doms p;
then consider y being object such that
A3: y in dom p and
A4: x = (doms p).y by A1,FUNCT_1:def 3;
reconsider T = p.y as DecoratedTree by A3,TREES_3:24;
T in rng p by A3,FUNCT_1:def 3;
then dom T in FinTrees by A2,TREES_3:def 2;
hence thesis by A3,A4,FUNCT_6:22;
end;
end;
end;
definition
let D be non empty set;
let d be Element of D, p be FinSequence of FinTrees D;
redefine func d-tree p -> Element of FinTrees D; :: redefines -tree (TREES_4, definition)
coherence
proof
dom (d-tree p) = tree(doms p) by Th10;
hence thesis by TREES_3:def 8;
end;
end;
definition
let D be non empty set, x be Subset of D;
redefine mode FinSequence of x -> FinSequence of D; :: redefines FinSequence (FINSEQ_1, definition)
coherence
proof
let p be FinSequence of x;
rng p c= x by FINSEQ_1:def 4;
hence rng p c= D by XBOOLE_1:1;
end;
end;
registration
let D be non empty constituted-DTrees set;
let X be Subset of D;
cluster -> DTree-yielding for FinSequence of X;
coherence;
end;
begin :: Expanding of decoreted tree by substitution
scheme ExpandTree{T1() -> Tree, T2() -> Tree, P[set]}: ex T being Tree st
for p holds p in T iff p in T1() or
ex q being Element of T1(), r being Element of T2() st P[q] & p = q^r
proof
defpred X[object] means $1 in T1() or
ex q being Element of T1(), r being Element of T2() st P[q] & $1 = q^r;
consider T being set such that
A1: for x being object holds x in T iff x in NAT* & X[x] from XBOOLE_0:sch 1;
set t = the Element of T1();
t in NAT* by FINSEQ_1:def 11;
then reconsider T as non empty set by A1;
T is Tree-like
proof
thus T c= NAT*
by A1;
thus
for p being FinSequence of NAT st p in T holds ProperPrefixes p c= T
proof
let p be FinSequence of NAT such that
A2: p in T;
let x be object;
assume x in ProperPrefixes p;
then consider q such that
A3: x = q and
A4: q is_a_proper_prefix_of p by TREES_1:def 2;
assume
A5: not thesis;
q is_a_prefix_of p by A4,XBOOLE_0:def 8;
then consider r such that
A6: p = q^r by TREES_1:1;
reconsider q,r as FinSequence of NAT by A6,FINSEQ_1:36;
q^r in T1() & q in NAT* & (q^r in T1() implies q in T1()) or
ex q being Element of T1(), r being Element of T2() st P[q] & p = q^r
by A1,A2,A6,FINSEQ_1:def 11,TREES_1:21;
then consider q9 being Element of T1(), r9 being Element of T2() such
that
A7: P[q9] and
A8: q^r = q9^r9 by A1,A3,A5,A6;
now
assume len q <= len q9;
then ex s being FinSequence st q^s = q9 by A8,FINSEQ_1:47;
then A9: q in T1() by TREES_1:21;
q in NAT* by FINSEQ_1:def 11;
hence contradiction by A1,A3,A5,A9;
end;
then consider s being FinSequence such that
A10: q9^s = q by A8,FINSEQ_1:47;
reconsider s as FinSequence of NAT by A10,FINSEQ_1:36;
q9^r9 = q9^(s^r) by A8,A10,FINSEQ_1:32;
then s^r = r9 by FINSEQ_1:33;
then q in NAT* & s is Element of T2() by FINSEQ_1:def 11,TREES_1:21;
hence thesis by A1,A3,A5,A7,A10;
end;
let p be FinSequence of NAT, k,n be Nat;
assume that
A11: p^<*k*> in T and
A12: n <= k;
A13: now
assume p^<*k*> in T1();
then A14: p^<*n*> in T1() by A12,TREES_1:def 3;
reconsider n as Element of NAT by ORDINAL1:def 12;
p^<*n*> in NAT* by FINSEQ_1:def 11;
hence thesis by A1,A14;
end;
now
assume
A15: not p^<*k*> in T1();
then consider q being Element of T1(), r being Element of T2() such that
A16: P[q] and
A17: p^<*k*> = q^r by A1,A11;
q^{} = q by FINSEQ_1:34;
then r <> {} by A15,A17;
then consider w being FinSequence, z such that
A18: r = w^<*z*> by FINSEQ_1:46;
reconsider w as FinSequence of NAT by A18,FINSEQ_1:36;
A19: p^<*k*> = q^w^<*z*> by A17,A18,FINSEQ_1:32;
A20: (
p^<*k*>).(len p+1) = k & (q^w^<*z*>).(len(q^w)+1) = z by FINSEQ_1:42;
A21: len <*k*> = 1 & len <*z*> = 1 by FINSEQ_1:40;
A22: len
(p^<*k*>) = len p+len <*k*> & len (q^w^<*z*>) = len (q^w)+len <*z*> by
FINSEQ_1:22;
then A23: p = q^w by A19,A20,A21,FINSEQ_1:33;
A24: w^<*n*> in T2() by A12,A18,A19,A20,A21,A22,TREES_1:def 3;
A25: p^<*n*> = q^(w^<*n*>) by A23,FINSEQ_1:32;
reconsider n as Element of NAT by ORDINAL1:def 12;
p^<*n*> in NAT* by FINSEQ_1:def 11;
hence thesis by A1,A16,A24,A25;
end;
hence thesis by A13;
end;
then reconsider T as Tree;
take T;
let p;
p is Element of T1() or
(ex q being Element of T1(), r being Element of T2() st P[q] & p = q^r)
implies p in NAT* by FINSEQ_1:def 11;
hence thesis by A1;
end;
definition
let T,T9 be DecoratedTree;
let x be set;
func (T,x) <- T9 -> DecoratedTree means
:
Def7: (for p holds p in dom it iff p in dom T or
ex q being Node of T, r being Node of T9 st
q in Leaves dom T & T.q = x & p = q^r) & (for p being Node of T st
not p in Leaves dom T or T.p <> x holds it.p = T.p) &
for p being Node of T, q being Node of T9 st
p in Leaves dom T & T.p = x holds it.(p^q) = T9.q;
existence
proof
defpred X[set] means $1 in Leaves dom T & T.$1 = x;
consider W being Tree such that
A1: p in W iff p in dom T or ex q being Node of T, r being Node of T9 st
X[q] & p = q^r from ExpandTree;
defpred X[object,object] means
$1 is Node of T & (not $1 in Leaves dom T or T.$1 <> x) & $2 = T.$1 or
ex p being Node of T, q being Node of T9 st
$1 = p^q & p in Leaves dom T & T.p = x & $2 = T9.q;
A2: for z being object st z in W ex y being object st X[z,y]
proof
let z be object;
assume z in W;
then reconsider w = z as Element of W;
A3: now
given q being Node of T, r being Node of T9 such that
A4: q in Leaves dom T & T.q = x & w = q^r;
take y = T9.r, q, r;
thus z = q^r & q in Leaves dom T & T.q = x & y = T9.r by A4;
end;
now
assume
A5: not ex q being Node of T, r being Node of T9 st
q in Leaves dom T & T.q = x & w = q^r;
take y = T.z;
thus z is Node of T by A1,A5;
reconsider w as Node of T by A1,A5;
reconsider e = {} as Node of T9 by TREES_1:22;
w^e = w by FINSEQ_1:34;
hence (not z in Leaves dom T or T.z <> x) & y = T.z by A5;
end;
hence thesis by A3;
end;
consider f being Function such that
A6: dom f = W &
for z being object st z in W holds X[z,f.z] from CLASSES1:sch 1(A2);
reconsider f as DecoratedTree by A6,TREES_2:def 8;
take f;
thus p in dom f iff p in dom T or
ex q being Node of T, r being Node of T9 st
q in Leaves dom T & T.q = x & p = q^r by A1,A6;
thus for p being Node of T st not p in Leaves dom T or T.p <> x holds
f.p = T.p
proof
let p be Node of T;
assume
A7: not p in Leaves dom T or T.p <> x;
A8: p in W by A1;
now
given p9 being Node of T, q being Node of T9 such that
A9: p = p9^q and
A10: p9 in Leaves dom T and
A11: T.p9 = x and f.p = T9.q;
p9
is_a_prefix_of p & not p9 is_a_proper_prefix_of p by A9,A10,TREES_1:1,def 5;
hence contradiction by A7,A10,A11,XBOOLE_0:def 8;
end;
hence thesis by A6,A8;
end;
let p be Node of T, q be Node of T9;
assume that
A12: p in Leaves dom T and
A13: T.p = x;
A14: p^q in W by A1,A12,A13;
now
assume p^q is Node of T;
then A15: not p is_a_proper_prefix_of p^q by A12,TREES_1:def 5;
p is_a_prefix_of p^q by TREES_1:1;
hence p = p^q by A15,XBOOLE_0:def 8;
end;
then consider p9 being Node of T, q9 being Node of T9 such that
A16: p^q = p9^q9 and
A17: p9 in Leaves dom T and T.p9 = x and
A18: f.(p^q) = T9.q9 by A6,A12,A13,A14;
now
let p,p9,q,q9 be FinSequence of NAT, T be Tree;
assume that
A19: p^q = p9^q9 and
A20: p in Leaves T & p9 in Leaves T and
A21: p <> p9;
now
assume len p <= len p9;
then ex r st p^r = p9 by A19,FINSEQ_1:47;
then p is_a_prefix_of p9 by TREES_1:1;
then p is_a_proper_prefix_of p9 by A21,XBOOLE_0:def 8;
hence contradiction by A20,TREES_1:def 5;
end;
then ex r st p9^r = p by A19,FINSEQ_1:47;
then p9 is_a_prefix_of p by TREES_1:1;
then p9 is_a_proper_prefix_of p by A21,XBOOLE_0:def 8;
hence contradiction by A20,TREES_1:def 5;
end;
then p = p9 by A12,A16,A17;
hence thesis by A16,A18,FINSEQ_1:33;
end;
uniqueness
proof
let T1, T2 be DecoratedTree such that
A22: p in dom T1 iff p in dom T or ex q being Node of T, r being Node of T9 st
q in Leaves dom T & T.q = x & p = q^r and
A23: for p being Node of T st
not p in Leaves dom T or T.p <> x holds T1.p = T.p and
A24: for p being Node of T, q being Node of T9 st
p in Leaves dom T & T.p = x holds T1.(p^q) = T9.q and
A25: p in dom T2 iff p in dom T or ex q being Node of T, r being Node of T9 st
q in Leaves dom T & T.q = x & p = q^r and
A26: for p being Node of T st
not p in Leaves dom T or T.p <> x holds T2.p = T.p and
A27: for p being Node of T, q being Node of T9 st
p in Leaves dom T & T.p = x holds T2.(p^q) = T9.q;
A28: dom T1 = dom T2
proof
let p be FinSequence of NAT;
p in dom T1 iff p in dom T or ex q being Node of T, r being Node of T9
st q in Leaves dom T & T.q = x & p = q^r by A22;
hence thesis by A25;
end;
reconsider p9 = {} as Node of T9 by TREES_1:22;
now
let y be object;
assume y in dom T1;
then reconsider p = y as Node of T1;
per cases by A22;
suppose
p in dom T;
then reconsider p as Node of T;
hereby per cases;
suppose
A29: p in Leaves dom T & T.p = x;
then A30: T1.(p^p9) = T9.p9 by A24;
p^p9 = p by FINSEQ_1:34;
hence T1.y = T2.y by A27,A29,A30;
end;
suppose
A31: not p in Leaves dom T or T.p <> x;
then T1.p = T.p by A23;
hence T1.y = T2.y by A26,A31;
end;
end;
end;
suppose
ex q being Node of T, r being Node of T9 st q in Leaves dom T &
T.q = x & p = q^r;
then consider q being Node of T, r being Node of T9 such that
A32: q in Leaves dom T & T.q = x & p = q^r;
thus T1.y = T9.r by A24,A32
.= T2.y by A27,A32;
end;
end;
hence thesis by A28;
end;
end;
registration
let D be non empty set;
let T,T9 be DecoratedTree of D;
let x be set;
cluster (T,x) <- T9 -> D-valued;
coherence
proof
rng ((T,x)<-T9) c= D
proof
let y be object;
assume y in rng ((T,x)<-T9);
then consider z being object such that
A1: z in dom ((T,x)<-T9) and
A2: y = ((T,x)<-T9).z by FUNCT_1:def 3;
reconsider z as Node of (T,x)<-T9 by A1;
reconsider p9 = {} as Node of T9 by TREES_1:22;
per cases by Def7;
suppose
z in dom T;
then reconsider p = z as Node of T;
hereby per cases;
suppose
p in Leaves dom T & T.p = x;
then A3: ((T,x)<-T9).(p^p9) = T9.p9 by Def7;
p^p9 = p by FINSEQ_1:34;
hence thesis by A2,A3;
end;
suppose
not p in Leaves dom T or T.p <> x;
then ((T,x)<-T9).p = T.p by Def7;
hence thesis by A2;
end;
end;
end;
suppose
ex q being Node of T, r being Node of T9 st q in Leaves dom T &
T.q = x & z = q^r;
then consider q being Node of T, r being Node of T9 such that
A4: q in Leaves dom T & T.q = x & z = q^r;
((T,x)<-T9).z = T9.r by A4,Def7;
hence thesis by A2;
end;
end;
hence thesis by RELAT_1:def 19;
end;
end;
reserve T,T9 for DecoratedTree,
x,y for set;
theorem
not x in rng T or not x in Leaves T implies (T,x) <- T9 = T
proof
A1: Leaves T c= rng T by RELAT_1:111;
assume not x in rng T or not x in Leaves T;
then A2: not x in Leaves T by A1;
thus
A3: dom ((T,x) <- T9) = dom T
proof
let p be FinSequence of NAT;
p in dom (T,x) <- T9 iff p in dom T or
ex q being Node of T, r being Node of T9 st
q in Leaves dom T & T.q = x & p = q^r by Def7;
hence thesis by A2,FUNCT_1:def 6;
end;
let p be Node of (T,x) <- T9;
reconsider p9 = p as Node of T by A3;
p9 in Leaves dom T implies T.p9 in Leaves T by FUNCT_1:def 6;
hence thesis by A2,Def7;
end;
begin :: Double decoreted trees
reserve D1, D2 for non empty set,
T for DecoratedTree of D1,D2,
d1 for Element of D1,
d2 for Element of D2,
F for non empty DTree-set of D1,D2,
F1 for non empty (DTree-set of D1),
F2 for non empty DTree-set of D2;
theorem Th24:
for D1, D2, T holds dom T`1 = dom T & dom T`2 = dom T
proof
let D1, D2, T;
A1: T`1 = pr1(D1,D2)*T & T`2 = pr2(D1,D2)*T by TREES_3:def 12,def 13;
A2: rng T c= [:D1,D2:] & dom pr1(D1,D2) = [:D1,D2:] by FUNCT_2:def 1
,RELAT_1:def 19;
dom pr2(D1,D2) = [:D1,D2:] by FUNCT_2:def 1;
hence thesis by A1,A2,RELAT_1:27;
end;
theorem Th25:
(root-tree [d1,d2])`1 = root-tree d1 & (root-tree [d1,d2])`2 = root-tree d2
proof reconsider r = {} as Node of root-tree [d1,d2] by TREES_1:22;
A1: dom (root-tree [d1,d2])`1 = dom root-tree [d1,d2] by Th24;
A2: dom (root-tree [d1,d2])`2 = dom root-tree [d1,d2] by Th24;
A3: (root-tree [d1,d2]).r = [d1,d2];
A4: [d1,d2]`1 = d1;
A5: [d1,d2]`2 = d2;
thus (root-tree [d1,d2])`1 = root-tree ((root-tree [d1,d2])`1.r) by A1,Th5
.= root-tree d1 by A3,A4,TREES_3:39;
thus (root-tree [d1,d2])`2 = root-tree ((root-tree [d1,d2])`2.r) by A2,Th5
.= root-tree d2 by A3,A5,TREES_3:39;
end;
theorem
<:root-tree x, root-tree y:> = root-tree [x,y]
proof reconsider x9 = x as Element of {x} by TARSKI:def 1;
reconsider y9 = y as Element of {y} by TARSKI:def 1;
(root-tree [x9,y9])`1 = root-tree x & (root-tree [x9,y9])`2 = root-tree y
by Th25;
hence thesis by TREES_3:40;
end;
theorem Th27:
for D1,D2, d1,d2, F,F1
for p being FinSequence of F, p1 being FinSequence of F1 st dom p1 = dom p &
for i st i in dom p for T st T = p.i holds p1.i = T`1
holds ([d1,d2]-tree p)`1 = d1-tree p1
proof
let D1,D2, d1,d2, F,F1;
let p be FinSequence of F, p1 be FinSequence of F1 such that
A1: dom p1 = dom p and
A2: for i st i in dom p for T st T = p.i holds p1.i = T`1;
set W = [d1,d2]-tree p, W1 = d1-tree p1;
A3: len doms p = len p by TREES_3:38;
A4: len doms p1 = len p1 by TREES_3:38;
A5: len p = len p1 by A1,FINSEQ_3:29;
then A6: dom doms p = dom doms p1 by A3,A4,FINSEQ_3:29;
A7: dom doms p = dom p by A3,FINSEQ_3:29;
now
let i be Nat;
assume
A8: i in dom p;
then reconsider T = p.i as Element of F by Lm1;
A9: p1.i = T`1 by A2,A8;
A10: (doms p).i = dom T by A8,FUNCT_6:22;
(doms p1).i = dom T`1 by A1,A8,A9,FUNCT_6:22;
hence (doms p).i = (doms p1).i by A10,Th24;
end;
then A11: doms p = doms p1 by A6,A7,FINSEQ_1:13;
dom W`1 = dom W by Th24
.= tree(doms p) by Th10;
hence dom W`1 = dom W1 by A11,Th10;
let x be Node of W`1;
reconsider a = x as Node of W by Th24;
A12: W`1.x = (W.a)`1 by TREES_3:39;
per cases;
suppose
x = {};
then W.x = [d1,d2] & W1.x = d1 by Def4;
hence thesis by A12;
end;
suppose
x <> {};
then consider n being Nat, T being DecoratedTree,
q being Node of T such that
A13: n < len p and
A14: T = p.(n+1) and
A15: a = <*n*>^q by Th11;
reconsider T as Element of F by A13,A14,Lm3;
reconsider q as Node of T`1 by Th24;
A16: p1.(n+1) = T`1 by A2,A13,A14,Lm2;
A17: W.a = T.q by A13,A14,A15,Th12;
W1.a = T`1.q by A5,A13,A15,A16,Th12;
hence thesis by A12,A17,TREES_3:39;
end;
end;
theorem Th28:
for D1,D2, d1,d2, F,F2
for p being FinSequence of F, p2 being FinSequence of F2 st dom p2 = dom p &
for i st i in dom p for T st T = p.i holds p2.i = T`2
holds ([d1,d2]-tree p)`2 = d2-tree p2
proof
let D1,D2, d1,d2, F,F2;
let p be FinSequence of F, p2 be FinSequence of F2 such that
A1: dom p2 = dom p and
A2: for i st i in dom p for T st T = p.i holds p2.i = T`2;
set W = [d1,d2]-tree p, W2 = d2-tree p2;
A3: len doms p = len p by TREES_3:38;
A4: len doms p2 = len p2 by TREES_3:38;
A5: len p = len p2 by A1,FINSEQ_3:29;
then A6: dom doms p = dom doms p2 by A3,A4,FINSEQ_3:29;
A7: dom doms p = dom p by A3,FINSEQ_3:29;
now
let i be Nat;
assume
A8: i in dom p;
then reconsider T = p.i as Element of F by Lm1;
A9: p2.i = T`2 by A2,A8;
A10: (doms p).i = dom T by A8,FUNCT_6:22;
(doms p2).i = dom T`2 by A1,A8,A9,FUNCT_6:22;
hence (doms p).i = (doms p2).i by A10,Th24;
end;
then A11: doms p = doms p2 by A6,A7,FINSEQ_1:13;
dom W`2 = dom W by Th24
.= tree(doms p) by Th10;
hence dom W`2 = dom W2 by A11,Th10;
let x be Node of W`2;
reconsider a = x as Node of W by Th24;
A12: W`2.x = (W.a)`2 by TREES_3:39;
per cases;
suppose
x = {};
then W.x = [d1,d2] & W2.x = d2 by Def4;
hence thesis by A12;
end;
suppose
x <> {};
then consider n being Nat, T being DecoratedTree,
q being Node of T such that
A13: n < len p and
A14: T = p.(n+1) and
A15: a = <*n*>^q by Th11;
reconsider T as Element of F by A13,A14,Lm3;
reconsider q as Node of T`2 by Th24;
A16: p2.(n+1) = T`2 by A2,A13,A14,Lm2;
A17: W.a = T.q by A13,A14,A15,Th12;
W2.a = T`2.q by A5,A13,A15,A16,Th12;
hence thesis by A12,A17,TREES_3:39;
end;
end;
theorem Th29:
for D1,D2, d1,d2, F for p being FinSequence of F
ex p1 being FinSequence of Trees D1 st dom p1 = dom p &
(for i st i in dom p ex T being Element of F st T = p.i & p1.i = T`1) &
([d1,d2]-tree p)`1 = d1-tree p1
proof
let D1,D2, d1,d2, F;
let p be FinSequence of F;
A1: Seg len p = dom p by FINSEQ_1:def 3;
defpred X[set,set] means ex T being Element of F st T = p.$1 & $2 = T`1;
A2: for i be Nat st i in Seg len p ex x being Element of Trees D1 st X[i,x]
proof
let i be Nat;
assume i in Seg len p;
then reconsider T = p.i as Element of F by A1,Lm1;
reconsider y = T`1 as Element of Trees D1 by TREES_3:def 7;
take y, T;
thus thesis;
end;
consider p1 being FinSequence of Trees D1 such that
A3: dom p1 = Seg len p & for i be Nat st i in Seg len p holds X[i,p1.i]
from FINSEQ_1:sch 5(A2);
take p1;
thus
A4: dom p1 = dom p by A3,FINSEQ_1:def 3;
hence for i st i in dom p
ex T being Element of F st T = p.i & p1.i = T`1 by A3;
now
let i;
assume i in dom p;
then ex T being Element of F st T = p.i & p1.i = T`1 by A3,A4;
hence for T st T = p.i holds p1.i = T`1;
end;
hence thesis by A4,Th27;
end;
theorem Th30:
for D1,D2, d1,d2, F for p being FinSequence of F
ex p2 being FinSequence of Trees D2 st dom p2 = dom p &
(for i st i in dom p ex T being Element of F st T = p.i & p2.i = T`2) &
([d1,d2]-tree p)`2 = d2-tree p2
proof
let D1,D2, d1,d2, F;
let p be FinSequence of F;
A1: Seg len p = dom p by FINSEQ_1:def 3;
defpred X[Nat,set] means ex T being Element of F st T = p.$1 & $2 = T`2;
A2: for i be Nat st i in Seg len p ex x being Element of Trees D2 st X[i,x]
proof
let i be Nat;
assume i in Seg len p;
then reconsider T = p.i as Element of F by A1,Lm1;
reconsider y = T`2 as Element of Trees D2 by TREES_3:def 7;
take y, T;
thus thesis;
end;
consider p2 being FinSequence of Trees D2 such that
A3: dom p2 = Seg len p & for i be Nat st i in Seg len p holds X[i,p2.i]
from FINSEQ_1:sch 5(A2);
take p2;
thus
A4: dom p2 = dom p by A3,FINSEQ_1:def 3;
hence for i st i in dom p
ex T being Element of F st T = p.i & p2.i = T`2 by A3;
now
let i;
assume i in dom p;
then ex T being Element of F st T = p.i & p2.i = T`2 by A3,A4;
hence for T st T = p.i holds p2.i = T`2;
end;
hence thesis by A4,Th28;
end;
theorem
for D1,D2, d1,d2 for p being FinSequence of FinTrees [:D1,D2:]
ex p1 being FinSequence of FinTrees D1 st dom p1 = dom p &
(for i st i in dom p ex T being Element of FinTrees [:D1,D2:] st
T = p.i & p1.i = T`1) & ([d1,d2]-tree p)`1 = d1-tree p1
proof
let D1,D2, d1,d2;
let p be FinSequence of FinTrees [:D1,D2:];
consider p1 being FinSequence of Trees D1 such that
A1: dom
p1 = dom p & for i st i in dom p ex T being Element of FinTrees [:D1,D2
:] st T = p.i & p1.i = T`1 and
A2: ([d1,d2]-tree p)`1 = d1-tree p1 by Th29;
rng p1 c= FinTrees D1
proof
let x be object;
assume x in rng p1;
then consider y being object such that
A3: y in dom p1 and
A4: x = p1.y by FUNCT_1:def 3;
reconsider y as Nat by A3;
consider T being Element of FinTrees [:D1,D2:] such that
T = p.y and
A5: p1.y = T`1 by A1,A3;
dom T`1 = dom T by Th24;
hence thesis by A4,A5,TREES_3:def 8;
end;
then p1 is FinSequence of FinTrees D1 by FINSEQ_1:def 4;
hence thesis by A1,A2;
end;
theorem
for D1,D2, d1,d2 for p being FinSequence of FinTrees [:D1,D2:]
ex p2 being FinSequence of FinTrees D2 st dom p2 = dom p &
(for i st i in dom p ex T being Element of FinTrees [:D1,D2:] st
T = p.i & p2.i = T`2) & ([d1,d2]-tree p)`2 = d2-tree p2
proof
let D1,D2, d1,d2;
let p be FinSequence of FinTrees [:D1,D2:];
consider p2 being FinSequence of Trees D2 such that
A1: dom
p2 = dom p & for i st i in dom p ex T being Element of FinTrees [:D1,D2
:] st T = p.i & p2.i = T`2 and
A2: ([d1,d2]-tree p)`2 = d2-tree p2 by Th30;
rng p2 c= FinTrees D2
proof
let x be object;
assume x in rng p2;
then consider y being object such that
A3: y in dom p2 and
A4: x = p2.y by FUNCT_1:def 3;
reconsider y as Nat by A3;
consider T being Element of FinTrees [:D1,D2:] such that
T = p.y and
A5: p2.y = T`2 by A1,A3;
dom T`2 = dom T by Th24;
hence thesis by A4,A5,TREES_3:def 8;
end;
then p2 is FinSequence of FinTrees D2 by FINSEQ_1:def 4;
hence thesis by A1,A2;
end;