:: Sets and Functions of Trees and Joining Operations of Trees
:: by Grzegorz Bancerek
::
:: Received November 27, 1992
:: Copyright (c) 1992-2012 Association of Mizar Users


begin

Lm1: for n being Element of NAT
for p, q being FinSequence st 1 <= n & n <= len p holds
(p ^ q) . n = p . n

proof end;

begin

definition
func Trees -> set means :Def1: :: TREES_3:def 1
for x being set holds
( x in it iff x is Tree );
existence
ex b1 being set st
for x being set holds
( x in b1 iff x is Tree )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff x is Tree ) ) & ( for x being set holds
( x in b2 iff x is Tree ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Trees TREES_3:def 1 :
for b1 being set holds
( b1 = Trees iff for x being set holds
( x in b1 iff x is Tree ) );

registration
cluster Trees -> non empty ;
coherence
not Trees is empty
proof end;
end;

definition
func FinTrees -> Subset of Trees means :Def2: :: TREES_3:def 2
for x being set holds
( x in it iff x is finite Tree );
existence
ex b1 being Subset of Trees st
for x being set holds
( x in b1 iff x is finite Tree )
proof end;
uniqueness
for b1, b2 being Subset of Trees st ( for x being set holds
( x in b1 iff x is finite Tree ) ) & ( for x being set holds
( x in b2 iff x is finite Tree ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines FinTrees TREES_3:def 2 :
for b1 being Subset of Trees holds
( b1 = FinTrees iff for x being set holds
( x in b1 iff x is finite Tree ) );

registration
cluster FinTrees -> non empty ;
coherence
not FinTrees is empty
proof end;
end;

definition
let IT be set ;
attr IT is constituted-Trees means :Def3: :: TREES_3:def 3
for x being set st x in IT holds
x is Tree;
attr IT is constituted-FinTrees means :Def4: :: TREES_3:def 4
for x being set st x in IT holds
x is finite Tree;
attr IT is constituted-DTrees means :Def5: :: TREES_3:def 5
for x being set st x in IT holds
x is DecoratedTree;
end;

:: deftheorem Def3 defines constituted-Trees TREES_3:def 3 :
for IT being set holds
( IT is constituted-Trees iff for x being set st x in IT holds
x is Tree );

:: deftheorem Def4 defines constituted-FinTrees TREES_3:def 4 :
for IT being set holds
( IT is constituted-FinTrees iff for x being set st x in IT holds
x is finite Tree );

:: deftheorem Def5 defines constituted-DTrees TREES_3:def 5 :
for IT being set holds
( IT is constituted-DTrees iff for x being set st x in IT holds
x is DecoratedTree );

theorem :: TREES_3:1
for X being set holds
( X is constituted-Trees iff X c= Trees )
proof end;

theorem :: TREES_3:2
for X being set holds
( X is constituted-FinTrees iff X c= FinTrees )
proof end;

theorem Th3: :: TREES_3:3
for X, Y being set holds
( ( X is constituted-Trees & Y is constituted-Trees ) iff X \/ Y is constituted-Trees )
proof end;

theorem :: TREES_3:4
for X, Y being set st X is constituted-Trees & Y is constituted-Trees holds
X \+\ Y is constituted-Trees
proof end;

theorem :: TREES_3:5
for X, Y being set st X is constituted-Trees holds
( X /\ Y is constituted-Trees & Y /\ X is constituted-Trees & X \ Y is constituted-Trees )
proof end;

theorem Th6: :: TREES_3:6
for X, Y being set holds
( ( X is constituted-FinTrees & Y is constituted-FinTrees ) iff X \/ Y is constituted-FinTrees )
proof end;

theorem :: TREES_3:7
for X, Y being set st X is constituted-FinTrees & Y is constituted-FinTrees holds
X \+\ Y is constituted-FinTrees
proof end;

theorem :: TREES_3:8
for X, Y being set st X is constituted-FinTrees holds
( X /\ Y is constituted-FinTrees & Y /\ X is constituted-FinTrees & X \ Y is constituted-FinTrees )
proof end;

theorem Th9: :: TREES_3:9
for X, Y being set holds
( ( X is constituted-DTrees & Y is constituted-DTrees ) iff X \/ Y is constituted-DTrees )
proof end;

theorem :: TREES_3:10
for X, Y being set st X is constituted-DTrees & Y is constituted-DTrees holds
X \+\ Y is constituted-DTrees
proof end;

theorem :: TREES_3:11
for X, Y being set st X is constituted-DTrees holds
( X /\ Y is constituted-DTrees & Y /\ X is constituted-DTrees & X \ Y is constituted-DTrees )
proof end;

registration
cluster empty -> constituted-Trees constituted-FinTrees constituted-DTrees for set ;
coherence
for b1 being set st b1 is empty holds
( b1 is constituted-Trees & b1 is constituted-FinTrees & b1 is constituted-DTrees )
proof end;
end;

theorem Th12: :: TREES_3:12
for x being set holds
( {x} is constituted-Trees iff x is Tree )
proof end;

theorem Th13: :: TREES_3:13
for x being set holds
( {x} is constituted-FinTrees iff x is finite Tree )
proof end;

theorem Th14: :: TREES_3:14
for x being set holds
( {x} is constituted-DTrees iff x is DecoratedTree )
proof end;

theorem Th15: :: TREES_3:15
for x, y being set holds
( {x,y} is constituted-Trees iff ( x is Tree & y is Tree ) )
proof end;

theorem Th16: :: TREES_3:16
for x, y being set holds
( {x,y} is constituted-FinTrees iff ( x is finite Tree & y is finite Tree ) )
proof end;

theorem Th17: :: TREES_3:17
for x, y being set holds
( {x,y} is constituted-DTrees iff ( x is DecoratedTree & y is DecoratedTree ) )
proof end;

theorem :: TREES_3:18
for X, Y being set st X is constituted-Trees & Y c= X holds
Y is constituted-Trees
proof end;

theorem :: TREES_3:19
for X, Y being set st X is constituted-FinTrees & Y c= X holds
Y is constituted-FinTrees
proof end;

theorem :: TREES_3:20
for X, Y being set st X is constituted-DTrees & Y c= X holds
Y is constituted-DTrees
proof end;

registration
cluster non empty finite constituted-Trees constituted-FinTrees for set ;
existence
ex b1 being set st
( b1 is finite & b1 is constituted-Trees & b1 is constituted-FinTrees & not b1 is empty )
proof end;
cluster non empty finite constituted-DTrees for set ;
existence
ex b1 being set st
( b1 is finite & b1 is constituted-DTrees & not b1 is empty )
proof end;
end;

registration
cluster constituted-FinTrees -> constituted-Trees for set ;
coherence
for b1 being set st b1 is constituted-FinTrees holds
b1 is constituted-Trees
proof end;
end;

registration
let X be constituted-Trees set ;
cluster -> constituted-Trees for Element of bool X;
coherence
for b1 being Subset of X holds b1 is constituted-Trees
proof end;
end;

registration
let X be constituted-FinTrees set ;
cluster -> constituted-FinTrees for Element of bool X;
coherence
for b1 being Subset of X holds b1 is constituted-FinTrees
proof end;
end;

registration
let X be constituted-DTrees set ;
cluster -> constituted-DTrees for Element of bool X;
coherence
for b1 being Subset of X holds b1 is constituted-DTrees
proof end;
end;

registration
let D be non empty constituted-Trees set ;
cluster -> non empty Tree-like for Element of D;
coherence
for b1 being Element of D holds
( not b1 is empty & b1 is Tree-like )
by Def3;
end;

registration
let D be non empty constituted-FinTrees set ;
cluster -> finite for Element of D;
coherence
for b1 being Element of D holds b1 is finite
by Def4;
end;

registration
cluster constituted-DTrees -> functional for set ;
coherence
for b1 being set st b1 is constituted-DTrees holds
b1 is functional
proof end;
end;

registration
let D be non empty constituted-DTrees set ;
cluster -> DecoratedTree-like for Element of D;
coherence
for b1 being Element of D holds b1 is DecoratedTree-like
by Def5;
end;

registration
cluster Trees -> constituted-Trees ;
coherence
Trees is constituted-Trees
proof end;
end;

registration
cluster FinTrees -> constituted-FinTrees ;
coherence
FinTrees is constituted-FinTrees
proof end;
end;

registration
cluster non empty constituted-Trees constituted-FinTrees for Element of bool Trees;
existence
ex b1 being Subset of Trees st
( b1 is constituted-FinTrees & not b1 is empty )
proof end;
end;

definition
let D be non empty set ;
mode DTree-set of D -> non empty set means :Def6: :: TREES_3:def 6
for x being set st x in it holds
x is DecoratedTree of D;
existence
ex b1 being non empty set st
for x being set st x in b1 holds
x is DecoratedTree of D
proof end;
end;

:: deftheorem Def6 defines DTree-set TREES_3:def 6 :
for D, b2 being non empty set holds
( b2 is DTree-set of D iff for x being set st x in b2 holds
x is DecoratedTree of D );

registration
let D be non empty set ;
cluster -> constituted-DTrees for DTree-set of D;
coherence
for b1 being DTree-set of D holds b1 is constituted-DTrees
proof end;
end;

registration
let D be non empty set ;
cluster functional non empty finite constituted-DTrees for DTree-set of D;
existence
ex b1 being DTree-set of D st
( b1 is finite & not b1 is empty )
proof end;
end;

registration
let D be non empty set ;
let E be non empty DTree-set of D;
cluster -> D -valued for Element of E;
coherence
for b1 being Element of E holds b1 is D -valued
by Def6;
end;

definition
let T be Tree;
let D be non empty set ;
:: original: Funcs
redefine func Funcs (T,D) -> non empty DTree-set of D;
coherence
Funcs (T,D) is non empty DTree-set of D
proof end;
end;

registration
let T be Tree;
let D be non empty set ;
cluster Function-like quasi_total -> DecoratedTree-like for Element of bool [:T,D:];
coherence
for b1 being Function of T,D holds b1 is DecoratedTree-like
proof end;
end;

definition
let D be non empty set ;
func Trees D -> DTree-set of D means :Def7: :: TREES_3:def 7
for T being DecoratedTree of D holds T in it;
existence
ex b1 being DTree-set of D st
for T being DecoratedTree of D holds T in b1
proof end;
uniqueness
for b1, b2 being DTree-set of D st ( for T being DecoratedTree of D holds T in b1 ) & ( for T being DecoratedTree of D holds T in b2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines Trees TREES_3:def 7 :
for D being non empty set
for b2 being DTree-set of D holds
( b2 = Trees D iff for T being DecoratedTree of D holds T in b2 );

registration
let D be non empty set ;
cluster Trees D -> non empty ;
coherence
not Trees D is empty
;
end;

definition
let D be non empty set ;
func FinTrees D -> DTree-set of D means :Def8: :: TREES_3:def 8
for T being DecoratedTree of D holds
( dom T is finite iff T in it );
existence
ex b1 being DTree-set of D st
for T being DecoratedTree of D holds
( dom T is finite iff T in b1 )
proof end;
uniqueness
for b1, b2 being DTree-set of D st ( for T being DecoratedTree of D holds
( dom T is finite iff T in b1 ) ) & ( for T being DecoratedTree of D holds
( dom T is finite iff T in b2 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines FinTrees TREES_3:def 8 :
for D being non empty set
for b2 being DTree-set of D holds
( b2 = FinTrees D iff for T being DecoratedTree of D holds
( dom T is finite iff T in b2 ) );

theorem :: TREES_3:21
for D being non empty set holds FinTrees D c= Trees D
proof end;

begin

definition
let IT be Function;
attr IT is Tree-yielding means :Def9: :: TREES_3:def 9
rng IT is constituted-Trees ;
attr IT is FinTree-yielding means :Def10: :: TREES_3:def 10
rng IT is constituted-FinTrees ;
attr IT is DTree-yielding means :Def11: :: TREES_3:def 11
rng IT is constituted-DTrees ;
end;

:: deftheorem Def9 defines Tree-yielding TREES_3:def 9 :
for IT being Function holds
( IT is Tree-yielding iff rng IT is constituted-Trees );

:: deftheorem Def10 defines FinTree-yielding TREES_3:def 10 :
for IT being Function holds
( IT is FinTree-yielding iff rng IT is constituted-FinTrees );

:: deftheorem Def11 defines DTree-yielding TREES_3:def 11 :
for IT being Function holds
( IT is DTree-yielding iff rng IT is constituted-DTrees );

registration
cluster Relation-like Function-like empty -> Tree-yielding FinTree-yielding DTree-yielding for set ;
coherence
for b1 being Function st b1 is empty holds
( b1 is Tree-yielding & b1 is FinTree-yielding & b1 is DTree-yielding )
proof end;
end;

theorem Th22: :: TREES_3:22
for f being Function holds
( f is Tree-yielding iff for x being set st x in dom f holds
f . x is Tree )
proof end;

theorem :: TREES_3:23
for f being Function holds
( f is FinTree-yielding iff for x being set st x in dom f holds
f . x is finite Tree )
proof end;

theorem Th24: :: TREES_3:24
for f being Function holds
( f is DTree-yielding iff for x being set st x in dom f holds
f . x is DecoratedTree )
proof end;

theorem Th25: :: TREES_3:25
for p, q being FinSequence holds
( ( p is Tree-yielding & q is Tree-yielding ) iff p ^ q is Tree-yielding )
proof end;

theorem Th26: :: TREES_3:26
for p, q being FinSequence holds
( ( p is FinTree-yielding & q is FinTree-yielding ) iff p ^ q is FinTree-yielding )
proof end;

theorem Th27: :: TREES_3:27
for p, q being FinSequence holds
( ( p is DTree-yielding & q is DTree-yielding ) iff p ^ q is DTree-yielding )
proof end;

theorem Th28: :: TREES_3:28
for x being set holds
( <*x*> is Tree-yielding iff x is Tree )
proof end;

theorem Th29: :: TREES_3:29
for x being set holds
( <*x*> is FinTree-yielding iff x is finite Tree )
proof end;

theorem Th30: :: TREES_3:30
for x being set holds
( <*x*> is DTree-yielding iff x is DecoratedTree )
proof end;

theorem Th31: :: TREES_3:31
for x, y being set holds
( <*x,y*> is Tree-yielding iff ( x is Tree & y is Tree ) )
proof end;

theorem Th32: :: TREES_3:32
for x, y being set holds
( <*x,y*> is FinTree-yielding iff ( x is finite Tree & y is finite Tree ) )
proof end;

theorem Th33: :: TREES_3:33
for x, y being set holds
( <*x,y*> is DTree-yielding iff ( x is DecoratedTree & y is DecoratedTree ) )
proof end;

theorem Th34: :: TREES_3:34
for x being set
for i being Element of NAT st i <> 0 holds
( i |-> x is Tree-yielding iff x is Tree )
proof end;

theorem Th35: :: TREES_3:35
for x being set
for i being Element of NAT st i <> 0 holds
( i |-> x is FinTree-yielding iff x is finite Tree )
proof end;

theorem Th36: :: TREES_3:36
for x being set
for i being Element of NAT st i <> 0 holds
( i |-> x is DTree-yielding iff x is DecoratedTree )
proof end;

registration
cluster Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like Tree-yielding FinTree-yielding for set ;
existence
ex b1 being FinSequence st
( b1 is Tree-yielding & b1 is FinTree-yielding & not b1 is empty )
proof end;
cluster Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like DTree-yielding for set ;
existence
ex b1 being FinSequence st
( b1 is DTree-yielding & not b1 is empty )
proof end;
end;

registration
cluster Relation-like Function-like non empty Tree-yielding FinTree-yielding for set ;
existence
ex b1 being Function st
( b1 is Tree-yielding & b1 is FinTree-yielding & not b1 is empty )
proof end;
cluster Relation-like Function-like non empty DTree-yielding for set ;
existence
ex b1 being Function st
( b1 is DTree-yielding & not b1 is empty )
proof end;
end;

registration
cluster Relation-like Function-like FinTree-yielding -> Tree-yielding for set ;
coherence
for b1 being Function st b1 is FinTree-yielding holds
b1 is Tree-yielding
proof end;
end;

registration
let D be non empty constituted-Trees set ;
cluster -> Tree-yielding for FinSequence of D;
coherence
for b1 being FinSequence of D holds b1 is Tree-yielding
proof end;
end;

registration
let p, q be Tree-yielding FinSequence;
cluster p ^ q -> Tree-yielding ;
coherence
p ^ q is Tree-yielding
by Th25;
end;

registration
let D be non empty constituted-FinTrees set ;
cluster -> FinTree-yielding for FinSequence of D;
coherence
for b1 being FinSequence of D holds b1 is FinTree-yielding
proof end;
end;

registration
let p, q be FinTree-yielding FinSequence;
cluster p ^ q -> FinTree-yielding ;
coherence
p ^ q is FinTree-yielding
by Th26;
end;

registration
let D be non empty constituted-DTrees set ;
cluster -> DTree-yielding for FinSequence of D;
coherence
for b1 being FinSequence of D holds b1 is DTree-yielding
proof end;
end;

registration
let p, q be DTree-yielding FinSequence;
cluster p ^ q -> DTree-yielding ;
coherence
p ^ q is DTree-yielding
by Th27;
end;

registration
let T be Tree;
cluster <*T*> -> non empty Tree-yielding ;
coherence
( <*T*> is Tree-yielding & not <*T*> is empty )
by Th28;
let S be Tree;
cluster <*T,S*> -> non empty Tree-yielding ;
coherence
( <*T,S*> is Tree-yielding & not <*T,S*> is empty )
by Th31;
end;

registration
let n be Element of NAT ;
let T be Tree;
cluster n |-> T -> Tree-yielding ;
coherence
n |-> T is Tree-yielding
proof end;
end;

registration
let T be finite Tree;
cluster <*T*> -> FinTree-yielding ;
coherence
<*T*> is FinTree-yielding
by Th29;
let S be finite Tree;
cluster <*T,S*> -> FinTree-yielding ;
coherence
<*T,S*> is FinTree-yielding
by Th32;
end;

registration
let n be Element of NAT ;
let T be finite Tree;
cluster n |-> T -> FinTree-yielding ;
coherence
n |-> T is FinTree-yielding
proof end;
end;

registration
let T be DecoratedTree;
cluster <*T*> -> non empty DTree-yielding ;
coherence
( <*T*> is DTree-yielding & not <*T*> is empty )
by Th30;
let S be DecoratedTree;
cluster <*T,S*> -> non empty DTree-yielding ;
coherence
( <*T,S*> is DTree-yielding & not <*T,S*> is empty )
by Th33;
end;

registration
let n be Element of NAT ;
let T be DecoratedTree;
cluster n |-> T -> DTree-yielding ;
coherence
n |-> T is DTree-yielding
proof end;
end;

theorem Th37: :: TREES_3:37
for f being DTree-yielding Function holds
( dom (doms f) = dom f & doms f is Tree-yielding )
proof end;

registration
let p be DTree-yielding FinSequence;
cluster doms p -> FinSequence-like Tree-yielding ;
coherence
( doms p is Tree-yielding & doms p is FinSequence-like )
proof end;
end;

theorem :: TREES_3:38
for p being DTree-yielding FinSequence holds len (doms p) = len p
proof end;

Lm2: for D being non empty set
for T being DecoratedTree of D holds T is Function of (dom T),D

proof end;

begin

definition
let D, E be non empty set ;
mode DecoratedTree of D,E is DecoratedTree of [:D,E:];
mode DTree-set of D,E is DTree-set of [:D,E:];
end;

registration
let T1, T2 be DecoratedTree;
cluster <:T1,T2:> -> DecoratedTree-like ;
coherence
<:T1,T2:> is DecoratedTree-like
proof end;
end;

registration
let D1, D2 be non empty set ;
let T1 be DecoratedTree of D1;
let T2 be DecoratedTree of D2;
cluster <:T1,T2:> -> [:D1,D2:] -valued ;
coherence
<:T1,T2:> is [:D1,D2:] -valued
proof end;
end;

registration
let D, E be non empty set ;
let T be DecoratedTree of D;
let f be Function of D,E;
cluster T * f -> DecoratedTree-like ;
coherence
f * T is DecoratedTree-like
proof end;
end;

definition
let D1, D2 be non empty set ;
:: original: pr1
redefine func pr1 (D1,D2) -> Function of [:D1,D2:],D1;
coherence
pr1 (D1,D2) is Function of [:D1,D2:],D1
proof end;
:: original: pr2
redefine func pr2 (D1,D2) -> Function of [:D1,D2:],D2;
coherence
pr2 (D1,D2) is Function of [:D1,D2:],D2
proof end;
end;

definition
let D1, D2 be non empty set ;
let T be DecoratedTree of D1,D2;
func T `1 -> DecoratedTree of D1 equals :: TREES_3:def 12
(pr1 (D1,D2)) * T;
correctness
coherence
(pr1 (D1,D2)) * T is DecoratedTree of D1
;
;
func T `2 -> DecoratedTree of D2 equals :: TREES_3:def 13
(pr2 (D1,D2)) * T;
correctness
coherence
(pr2 (D1,D2)) * T is DecoratedTree of D2
;
;
end;

:: deftheorem defines `1 TREES_3:def 12 :
for D1, D2 being non empty set
for T being DecoratedTree of D1,D2 holds T `1 = (pr1 (D1,D2)) * T;

:: deftheorem defines `2 TREES_3:def 13 :
for D1, D2 being non empty set
for T being DecoratedTree of D1,D2 holds T `2 = (pr2 (D1,D2)) * T;

theorem Th39: :: TREES_3:39
for D1, D2 being non empty set
for T being DecoratedTree of D1,D2
for t being Element of dom T holds
( (T . t) `1 = (T `1) . t & (T `2) . t = (T . t) `2 )
proof end;

theorem :: TREES_3:40
for D1, D2 being non empty set
for T being DecoratedTree of D1,D2 holds <:(T `1),(T `2):> = T
proof end;

registration
let T be finite Tree;
cluster Leaves T -> non empty finite ;
coherence
( Leaves T is finite & not Leaves T is empty )
proof end;
end;

definition
let T be Tree;
let S be non empty Subset of T;
:: original: Element
redefine mode Element of S -> Element of T;
coherence
for b1 being Element of S holds b1 is Element of T
proof end;
end;

definition
let T be finite Tree;
:: original: Leaf
redefine mode Leaf of T -> Element of Leaves T;
coherence
for b1 being Leaf of T holds b1 is Element of Leaves T
by TREES_1:def 7;
end;

definition
let T be finite Tree;
mode T-Substitution of T -> Tree means :Def14: :: TREES_3:def 14
for t being Element of it holds
( t in T or ex l being Leaf of T st l is_a_proper_prefix_of t );
existence
ex b1 being Tree st
for t being Element of b1 holds
( t in T or ex l being Leaf of T st l is_a_proper_prefix_of t )
proof end;
end;

:: deftheorem Def14 defines T-Substitution TREES_3:def 14 :
for T being finite Tree
for b2 being Tree holds
( b2 is T-Substitution of T iff for t being Element of b2 holds
( t in T or ex l being Leaf of T st l is_a_proper_prefix_of t ) );

definition
let T be finite Tree;
let t be Leaf of T;
let S be Tree;
:: original: with-replacement
redefine func T with-replacement (t,S) -> T-Substitution of T;
coherence
T with-replacement (t,S) is T-Substitution of T
proof end;
end;

registration
let T be finite Tree;
cluster non empty finite Tree-like for T-Substitution of T;
existence
ex b1 being T-Substitution of T st b1 is finite
proof end;
end;

definition
let n be Element of NAT ;
mode T-Substitution of n is T-Substitution of elementary_tree n;
end;

theorem :: TREES_3:41
for T being Tree holds T is T-Substitution of 0
proof end;

theorem :: TREES_3:42
for T1, T2 being Tree st T1 -level 1 c= T2 -level 1 & ( for n being Element of NAT st <*n*> in T1 holds
T1 | <*n*> = T2 | <*n*> ) holds
T1 c= T2
proof end;

Lm3: for n being Element of NAT
for p being FinSequence st n < len p holds
( n + 1 in dom p & p . (n + 1) in rng p )

proof end;

begin

theorem :: TREES_3:43
for T, T9 being Tree
for p being FinSequence of NAT st p in Leaves T holds
T c= T with-replacement (p,T9)
proof end;

theorem :: TREES_3:44
for T, T9 being DecoratedTree
for p being Element of dom T holds (T with-replacement (p,T9)) . p = T9 . {}
proof end;

theorem :: TREES_3:45
for T, T9 being DecoratedTree
for p, q being Element of dom T st not p is_a_prefix_of q holds
(T with-replacement (p,T9)) . q = T . q
proof end;

theorem :: TREES_3:46
for T, T9 being DecoratedTree
for p being Element of dom T
for q being Element of dom T9 holds (T with-replacement (p,T9)) . (p ^ q) = T9 . q
proof end;

registration
let T1, T2 be Tree;
cluster T1 \/ T2 -> non empty Tree-like ;
coherence
( not T1 \/ T2 is empty & T1 \/ T2 is Tree-like )
;
end;

theorem Th47: :: TREES_3:47
for T1, T2 being Tree
for p being Element of T1 \/ T2 holds
( ( p in T1 & p in T2 implies (T1 \/ T2) | p = (T1 | p) \/ (T2 | p) ) & ( not p in T1 implies (T1 \/ T2) | p = T2 | p ) & ( not p in T2 implies (T1 \/ T2) | p = T1 | p ) )
proof end;

definition
let p be FinSequence;
assume B1: p is Tree-yielding ;
func tree p -> Tree means :Def15: :: TREES_3:def 15
for x being set holds
( x in it iff ( x = {} or ex n being Element of NAT ex q being FinSequence st
( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) ) );
existence
ex b1 being Tree st
for x being set holds
( x in b1 iff ( x = {} or ex n being Element of NAT ex q being FinSequence st
( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) ) )
proof end;
uniqueness
for b1, b2 being Tree st ( for x being set holds
( x in b1 iff ( x = {} or ex n being Element of NAT ex q being FinSequence st
( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) ) ) ) & ( for x being set holds
( x in b2 iff ( x = {} or ex n being Element of NAT ex q being FinSequence st
( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def15 defines tree TREES_3:def 15 :
for p being FinSequence st p is Tree-yielding holds
for b2 being Tree holds
( b2 = tree p iff for x being set holds
( x in b2 iff ( x = {} or ex n being Element of NAT ex q being FinSequence st
( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) ) ) );

definition
let T be Tree;
func ^ T -> Tree equals :: TREES_3:def 16
tree <*T*>;
correctness
coherence
tree <*T*> is Tree
;
;
end;

:: deftheorem defines ^ TREES_3:def 16 :
for T being Tree holds ^ T = tree <*T*>;

definition
let T1, T2 be Tree;
func tree (T1,T2) -> Tree equals :: TREES_3:def 17
tree <*T1,T2*>;
correctness
coherence
tree <*T1,T2*> is Tree
;
;
end;

:: deftheorem defines tree TREES_3:def 17 :
for T1, T2 being Tree holds tree (T1,T2) = tree <*T1,T2*>;

theorem :: TREES_3:48
for n being Element of NAT
for p, q being FinSequence st p is Tree-yielding holds
( <*n*> ^ q in tree p iff ( n < len p & q in p . (n + 1) ) )
proof end;

theorem Th49: :: TREES_3:49
for p being FinSequence st p is Tree-yielding holds
( (tree p) -level 1 = { <*n*> where n is Element of NAT : n < len p } & ( for n being Element of NAT st n < len p holds
(tree p) | <*n*> = p . (n + 1) ) )
proof end;

theorem :: TREES_3:50
for p, q being Tree-yielding FinSequence st tree p = tree q holds
p = q
proof end;

theorem Th51: :: TREES_3:51
for p being FinSequence
for p1, p2 being Tree-yielding FinSequence
for T being Tree holds
( p in T iff <*(len p1)*> ^ p in tree ((p1 ^ <*T*>) ^ p2) )
proof end;

theorem Th52: :: TREES_3:52
tree {} = elementary_tree 0
proof end;

theorem Th53: :: TREES_3:53
for p being FinSequence st p is Tree-yielding holds
elementary_tree (len p) c= tree p
proof end;

theorem Th54: :: TREES_3:54
for i being Element of NAT holds elementary_tree i = tree (i |-> (elementary_tree 0))
proof end;

theorem Th55: :: TREES_3:55
for T being Tree
for p being Tree-yielding FinSequence holds tree (p ^ <*T*>) = ((tree p) \/ (elementary_tree ((len p) + 1))) with-replacement (<*(len p)*>,T)
proof end;

theorem :: TREES_3:56
for p being Tree-yielding FinSequence holds tree (p ^ <*(elementary_tree 0)*>) = (tree p) \/ (elementary_tree ((len p) + 1))
proof end;

theorem Th57: :: TREES_3:57
for p, q being Tree-yielding FinSequence
for T1, T2 being Tree holds tree ((p ^ <*T1*>) ^ q) = (tree ((p ^ <*T2*>) ^ q)) with-replacement (<*(len p)*>,T1)
proof end;

theorem :: TREES_3:58
for T being Tree holds ^ T = (elementary_tree 1) with-replacement (<*0*>,T)
proof end;

theorem :: TREES_3:59
for T1, T2 being Tree holds tree (T1,T2) = ((elementary_tree 2) with-replacement (<*0*>,T1)) with-replacement (<*1*>,T2)
proof end;

registration
let p be FinTree-yielding FinSequence;
cluster tree p -> finite ;
coherence
tree p is finite
proof end;
end;

registration
let T be finite Tree;
cluster ^ T -> finite ;
coherence
^ T is finite
;
end;

registration
let T1, T2 be finite Tree;
cluster tree (T1,T2) -> finite ;
coherence
tree (T1,T2) is finite
;
end;

theorem Th60: :: TREES_3:60
for T being Tree
for x being set holds
( x in ^ T iff ( x = {} or ex p being FinSequence st
( p in T & x = <*0*> ^ p ) ) )
proof end;

theorem Th61: :: TREES_3:61
for T being Tree
for p being FinSequence holds
( p in T iff <*0*> ^ p in ^ T )
proof end;

theorem :: TREES_3:62
for T being Tree holds elementary_tree 1 c= ^ T
proof end;

theorem :: TREES_3:63
for T1, T2 being Tree st T1 c= T2 holds
^ T1 c= ^ T2
proof end;

theorem :: TREES_3:64
for T1, T2 being Tree st ^ T1 = ^ T2 holds
T1 = T2
proof end;

theorem :: TREES_3:65
for T being Tree holds (^ T) | <*0*> = T
proof end;

theorem :: TREES_3:66
for T1, T2 being Tree holds (^ T1) with-replacement (<*0*>,T2) = ^ T2
proof end;

theorem :: TREES_3:67
^ (elementary_tree 0) = elementary_tree 1
proof end;

theorem Th68: :: TREES_3:68
for T1, T2 being Tree
for x being set holds
( x in tree (T1,T2) iff ( x = {} or ex p being FinSequence st
( ( p in T1 & x = <*0*> ^ p ) or ( p in T2 & x = <*1*> ^ p ) ) ) )
proof end;

theorem Th69: :: TREES_3:69
for T1, T2 being Tree
for p being FinSequence holds
( p in T1 iff <*0*> ^ p in tree (T1,T2) )
proof end;

theorem Th70: :: TREES_3:70
for T1, T2 being Tree
for p being FinSequence holds
( p in T2 iff <*1*> ^ p in tree (T1,T2) )
proof end;

theorem :: TREES_3:71
for T1, T2 being Tree holds elementary_tree 2 c= tree (T1,T2)
proof end;

theorem :: TREES_3:72
for T1, T2, W1, W2 being Tree st T1 c= W1 & T2 c= W2 holds
tree (T1,T2) c= tree (W1,W2)
proof end;

theorem :: TREES_3:73
for T1, T2, W1, W2 being Tree st tree (T1,T2) = tree (W1,W2) holds
( T1 = W1 & T2 = W2 )
proof end;

theorem :: TREES_3:74
for T1, T2 being Tree holds
( (tree (T1,T2)) | <*0*> = T1 & (tree (T1,T2)) | <*1*> = T2 )
proof end;

theorem :: TREES_3:75
for T, T1, T2 being Tree holds
( (tree (T1,T2)) with-replacement (<*0*>,T) = tree (T,T2) & (tree (T1,T2)) with-replacement (<*1*>,T) = tree (T1,T) )
proof end;

theorem :: TREES_3:76
tree ((elementary_tree 0),(elementary_tree 0)) = elementary_tree 2
proof end;

theorem Th77: :: TREES_3:77
for n being Element of NAT
for w being FinTree-yielding FinSequence st ( for t being finite Tree st t in rng w holds
height t <= n ) holds
height (tree w) <= n + 1
proof end;

theorem Th78: :: TREES_3:78
for w being FinTree-yielding FinSequence
for t being finite Tree st t in rng w holds
height (tree w) > height t
proof end;

theorem Th79: :: TREES_3:79
for w being FinTree-yielding FinSequence
for t being finite Tree st t in rng w & ( for t9 being finite Tree st t9 in rng w holds
height t9 <= height t ) holds
height (tree w) = (height t) + 1
proof end;

theorem :: TREES_3:80
for T being finite Tree holds height (^ T) = (height T) + 1
proof end;

theorem :: TREES_3:81
for T1, T2 being finite Tree holds height (tree (T1,T2)) = (max ((height T1),(height T2))) + 1
proof end;

begin

:: from DTCONSTR
registration
let D be non empty set ;
let t be Element of FinTrees D;
cluster dom t -> finite ;
coherence
dom t is finite
by Def8;
end;

definition
let p be FinSequence;
assume B1: p is DTree-yielding ;
defpred S1[ Nat, set ] means ex T being DecoratedTree st
( T = p . $1 & $2 = T . {} );
func roots p -> FinSequence means :: TREES_3:def 18
( dom it = dom p & ( for i being Element of NAT st i in dom p holds
ex T being DecoratedTree st
( T = p . i & it . i = T . {} ) ) );
existence
ex b1 being FinSequence st
( dom b1 = dom p & ( for i being Element of NAT st i in dom p holds
ex T being DecoratedTree st
( T = p . i & b1 . i = T . {} ) ) )
proof end;
uniqueness
for b1, b2 being FinSequence st dom b1 = dom p & ( for i being Element of NAT st i in dom p holds
ex T being DecoratedTree st
( T = p . i & b1 . i = T . {} ) ) & dom b2 = dom p & ( for i being Element of NAT st i in dom p holds
ex T being DecoratedTree st
( T = p . i & b2 . i = T . {} ) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines roots TREES_3:def 18 :
for p being FinSequence st p is DTree-yielding holds
for b2 being FinSequence holds
( b2 = roots p iff ( dom b2 = dom p & ( for i being Element of NAT st i in dom p holds
ex T being DecoratedTree st
( T = p . i & b2 . i = T . {} ) ) ) );