:: Sets and Functions of Trees and Joining Operations of Trees
:: by Grzegorz Bancerek
::
:: Received November 27, 1992
:: Copyright (c) 1992 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 b₁ being set st
for x being set holds
( x in b₁ iff x is Tree )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being set holds
( x in b₁ iff x is Tree ) ) & ( for x being set holds
( x in b₂ iff x is Tree ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines Trees TREES_3:def 1 :
for b₁ being set holds
( b₁ = Trees iff for x being set holds
( x in b₁ 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 b₁ being Subset of Trees st
for x being set holds
( x in b₁ iff x is finite Tree )

proof end;

uniqueness
for b₁, b₂ being Subset of Trees st ( for x being set holds
( x in b₁ iff x is finite Tree ) ) & ( for x being set holds
( x in b₂ iff x is finite Tree ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines FinTrees TREES_3:def 2 :
for b₁ being Subset of Trees holds
( b₁ = FinTrees iff for x being set holds
( x in b₁ 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 set ;
coherence
for b₁ being set st b₁ is empty holds
( b₁ is constituted-Trees & b₁ is constituted-FinTrees & b₁ is constituted-DTrees )

proof end;

end;

theorem :: TREES_3:12

canceled;

theorem Th13: :: TREES_3:13

for x being set holds
( {x} is constituted-Trees iff x is Tree )

proof end;

theorem Th14: :: TREES_3:14

for x being set holds
( {x} is constituted-FinTrees iff x is finite Tree )

proof end;

theorem Th15: :: TREES_3:15

for x being set holds
( {x} is constituted-DTrees iff x is DecoratedTree )

proof end;

theorem Th16: :: TREES_3:16

for x, y being set holds
( {x,y} is constituted-Trees iff ( x is Tree & y is Tree ) )

proof end;

theorem Th17: :: TREES_3:17

for x, y being set holds
( {x,y} is constituted-FinTrees iff ( x is finite Tree & y is finite Tree ) )

proof end;

theorem Th18: :: TREES_3:18

for x, y being set holds
( {x,y} is constituted-DTrees iff ( x is DecoratedTree & y is DecoratedTree ) )

proof end;

theorem :: TREES_3:19

for X, Y being set st X is constituted-Trees & Y c= X holds
Y is constituted-Trees

proof end;

theorem :: TREES_3:20

for X, Y being set st X is constituted-FinTrees & Y c= X holds
Y is constituted-FinTrees

proof end;

theorem :: TREES_3:21

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 set ;
existence
ex b₁ being set st
( b₁ is finite & b₁ is constituted-Trees & b₁ is constituted-FinTrees & not b₁ is empty )

proof end;

cluster non empty finite constituted-DTrees set ;
existence
ex b₁ being set st
( b₁ is finite & b₁ is constituted-DTrees & not b₁ is empty )

proof end;

end;

registration

cluster constituted-FinTrees -> constituted-Trees set ;
coherence
for b₁ being set st b₁ is constituted-FinTrees holds
b₁ is constituted-Trees

proof end;

end;

registration

let X be constituted-Trees set ;
cluster -> constituted-Trees Element of bool X;
coherence
for b₁ being Subset of X holds b₁ is constituted-Trees

proof end;

end;

registration

let X be constituted-FinTrees set ;
cluster -> constituted-FinTrees Element of bool X;
coherence
for b₁ being Subset of X holds b₁ is constituted-FinTrees

proof end;

end;

registration

let X be constituted-DTrees set ;
cluster -> constituted-DTrees Element of bool X;
coherence
for b₁ being Subset of X holds b₁ is constituted-DTrees

proof end;

end;

registration

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

end;

registration

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

end;

registration

let D be non empty constituted-DTrees set ;
cluster -> Relation-like Function-like Element of D;
coherence
for b₁ being Element of D holds
( b₁ is Function-like & b₁ is Relation-like ) by Def5;

end;

registration

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

end;

registration

cluster Trees -> constituted-Trees ;
coherence
Trees is constituted-Trees

proof end;

end;

registration

cluster non empty constituted-Trees constituted-FinTrees Element of bool Trees;
existence
ex b₁ being Subset of Trees st
( b₁ is constituted-FinTrees & not b₁ is empty )

proof end;

end;

registration

cluster FinTrees -> constituted-FinTrees ;
coherence
FinTrees is constituted-FinTrees

proof end;

end;

definition

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

proof end;

end;

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

registration

let D be non empty set ;
cluster -> constituted-DTrees DTree-set of D;
coherence
for b₁ being DTree-set of D holds b₁ is constituted-DTrees

proof end;

end;

registration

let D be non empty set ;
cluster non empty finite constituted-DTrees DTree-set of D;
existence
ex b₁ being DTree-set of D st
( b₁ is finite & not b₁ is empty )

proof end;

end;

registration

let D be non empty set ;
let E be non empty DTree-set of D;
cluster -> D -valued Element of E;
coherence
for b₁ being Element of E holds b₁ 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 Element of bool [:T,D:];
coherence
for b₁ being Function of T,D holds b₁ 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 b₁ being DTree-set of D st
for T being DecoratedTree of D holds T in b₁

proof end;

uniqueness
for b₁, b₂ being DTree-set of D st ( for T being DecoratedTree of D holds T in b₁ ) & ( for T being DecoratedTree of D holds T in b₂ ) holds
b₁ = b₂

proof end;

end;

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

registration

let D be non empty set ;
cluster Trees D -> non empty ;
coherence
not Trees D is empty by Def7;

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 b₁ being DTree-set of D st
for T being DecoratedTree of D holds
( dom T is finite iff T in b₁ )

proof end;

uniqueness
for b₁, b₂ being DTree-set of D st ( for T being DecoratedTree of D holds
( dom T is finite iff T in b₁ ) ) & ( for T being DecoratedTree of D holds
( dom T is finite iff T in b₂ ) ) holds
b₁ = b₂

proof end;

end;

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

registration

let D be non empty set ;
cluster FinTrees D -> non empty ;
coherence
not FinTrees D is empty

proof end;

end;

theorem :: TREES_3:22

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 set ;
coherence
for b₁ being Function st b₁ is empty holds
( b₁ is Tree-yielding & b₁ is FinTree-yielding & b₁ is DTree-yielding )

proof end;

end;

theorem :: TREES_3:23

canceled;

theorem Th24: :: TREES_3:24

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:25

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 Th26: :: TREES_3:26

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 Th27: :: TREES_3:27

for p, q being FinSequence holds
( ( p is Tree-yielding & q is Tree-yielding ) iff p ^ q is Tree-yielding )

proof end;

theorem Th28: :: TREES_3:28

for p, q being FinSequence holds
( ( p is FinTree-yielding & q is FinTree-yielding ) iff p ^ q is FinTree-yielding )

proof end;

theorem Th29: :: TREES_3:29

for p, q being FinSequence holds
( ( p is DTree-yielding & q is DTree-yielding ) iff p ^ q is DTree-yielding )

proof end;

theorem Th30: :: TREES_3:30

for x being set holds
( <*x*> is Tree-yielding iff x is Tree )

proof end;

theorem Th31: :: TREES_3:31

for x being set holds
( <*x*> is FinTree-yielding iff x is finite Tree )

proof end;

theorem Th32: :: TREES_3:32

for x being set holds
( <*x*> is DTree-yielding iff x is DecoratedTree )

proof end;

theorem Th33: :: TREES_3:33

for x, y being set holds
( <*x,y*> is Tree-yielding iff ( x is Tree & y is Tree ) )

proof end;

theorem Th34: :: TREES_3:34

for x, y being set holds
( <*x,y*> is FinTree-yielding iff ( x is finite Tree & y is finite Tree ) )

proof end;

theorem Th35: :: TREES_3:35

for x, y being set holds
( <*x,y*> is DTree-yielding iff ( x is DecoratedTree & y is DecoratedTree ) )

proof end;

theorem Th36: :: TREES_3:36

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 Th37: :: TREES_3:37

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 Th38: :: TREES_3:38

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 Function-like non empty finite FinSequence-like FinSubsequence-like Tree-yielding FinTree-yielding set ;
existence
ex b₁ being FinSequence st
( b₁ is Tree-yielding & b₁ is FinTree-yielding & not b₁ is empty )

proof end;

cluster Relation-like Function-like non empty finite FinSequence-like FinSubsequence-like DTree-yielding set ;
existence
ex b₁ being FinSequence st
( b₁ is DTree-yielding & not b₁ is empty )

proof end;

end;

registration

cluster Relation-like Function-like non empty Tree-yielding FinTree-yielding set ;
existence
ex b₁ being Function st
( b₁ is Tree-yielding & b₁ is FinTree-yielding & not b₁ is empty )

proof end;

cluster Relation-like Function-like non empty DTree-yielding set ;
existence
ex b₁ being Function st
( b₁ is DTree-yielding & not b₁ is empty )

proof end;

end;

registration

cluster Relation-like Function-like FinTree-yielding -> Tree-yielding set ;
coherence
for b₁ being Function st b₁ is FinTree-yielding holds
b₁ is Tree-yielding

proof end;

end;

registration

let D be non empty constituted-Trees set ;
cluster -> Tree-yielding FinSequence of D;
coherence
for b₁ being FinSequence of D holds b₁ 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 Th27;

end;

registration

let D be non empty constituted-FinTrees set ;
cluster -> FinTree-yielding FinSequence of D;
coherence
for b₁ being FinSequence of D holds b₁ 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 Th28;

end;

registration

let D be non empty constituted-DTrees set ;
cluster -> DTree-yielding FinSequence of D;
coherence
for b₁ being FinSequence of D holds b₁ 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 Th29;

end;

registration

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

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 Th31;
let S be finite Tree;
cluster <*T,S*> -> FinTree-yielding ;
coherence
<*T,S*> is FinTree-yielding by Th34;

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 Th32;
let S be DecoratedTree;
cluster <*T,S*> -> non empty DTree-yielding ;
coherence
( <*T,S*> is DTree-yielding & not <*T,S*> is empty ) by Th35;

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 Th39: :: TREES_3:39

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:40

for p being DTree-yielding FinSequence holds len (doms p) = len p

proof end;

Lm3: 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 Th41: :: TREES_3:41

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:42

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 b₁ being Element of S holds b₁ 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 b₁ being Leaf of T holds b₁ is Element of Leaves T by TREES_1:def 10;

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 b₁ being Tree st
for t being Element of b₁ 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 b₂ being Tree holds
( b₂ is T-Substitution of T iff for t being Element of b₂ 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 T-Substitution of T;
existence
ex b₁ being T-Substitution of T st b₁ 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:43

for T being Tree holds T is T-Substitution of 0

proof end;

theorem :: TREES_3:44

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;

Lm4: 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:45

canceled;

theorem :: TREES_3:46

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:47

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:48

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:49

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 ) by TREES_1:49;

end;

theorem Th50: :: TREES_3:50

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 A1: 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 b₁ being Tree st
for x being set holds
( x in b₁ 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 b₁, b₂ being Tree st ( for x being set holds
( x in b₁ 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 b₂ 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
b₁ = b₂

proof end;

end;

:: deftheorem Def15 defines tree TREES_3:def 15 :
for p being FinSequence st p is Tree-yielding holds
for b₂ being Tree holds
( b₂ = tree p iff for x being set holds
( x in b₂ 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:51

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 Th52: :: TREES_3:52

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:53

for p, q being Tree-yielding FinSequence st tree p = tree q holds
p = q

proof end;

theorem Th54: :: TREES_3:54

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 Th55: :: TREES_3:55

tree {} = elementary_tree 0

proof end;

theorem Th56: :: TREES_3:56

for p being FinSequence st p is Tree-yielding holds
elementary_tree (len p) c= tree p

proof end;

theorem Th57: :: TREES_3:57

for i being Element of NAT holds elementary_tree i = tree (i |-> (elementary_tree 0))

proof end;

theorem Th58: :: TREES_3:58

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:59

for p being Tree-yielding FinSequence holds tree (p ^ <*(elementary_tree 0)*>) = (tree p) \/ (elementary_tree ((len p) + 1))

proof end;

theorem Th60: :: TREES_3:60

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:61

for T being Tree holds ^ T = (elementary_tree 1) with-replacement (<*0*>,T)

proof end;

theorem :: TREES_3:62

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 Th63: :: TREES_3:63

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 Th64: :: TREES_3:64

for T being Tree
for p being FinSequence holds
( p in T iff <*0*> ^ p in ^ T )

proof end;

theorem :: TREES_3:65

for T being Tree holds elementary_tree 1 c= ^ T

proof end;

theorem :: TREES_3:66

for T1, T2 being Tree st T1 c= T2 holds
^ T1 c= ^ T2

proof end;

theorem :: TREES_3:67

for T1, T2 being Tree st ^ T1 = ^ T2 holds
T1 = T2

proof end;

theorem :: TREES_3:68

for T being Tree holds (^ T) | <*0*> = T

proof end;

theorem :: TREES_3:69

for T1, T2 being Tree holds (^ T1) with-replacement (<*0*>,T2) = ^ T2

proof end;

theorem :: TREES_3:70

^ (elementary_tree 0) = elementary_tree 1

proof end;

theorem Th71: :: TREES_3:71

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 Th72: :: TREES_3:72

for T1, T2 being Tree
for p being FinSequence holds
( p in T1 iff <*0*> ^ p in tree (T1,T2) )

proof end;

theorem Th73: :: TREES_3:73

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:74

for T1, T2 being Tree holds elementary_tree 2 c= tree (T1,T2)

proof end;

theorem :: TREES_3:75

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:76

for T1, T2, W1, W2 being Tree st tree (T1,T2) = tree (W1,W2) holds
( T1 = W1 & T2 = W2 )

proof end;

theorem :: TREES_3:77

for T1, T2 being Tree holds
( (tree (T1,T2)) | <*0*> = T1 & (tree (T1,T2)) | <*1*> = T2 )

proof end;

theorem :: TREES_3:78

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:79

tree ((elementary_tree 0),(elementary_tree 0)) = elementary_tree 2

proof end;

theorem Th80: :: TREES_3:80

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 Th81: :: TREES_3:81

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 Th82: :: TREES_3:82

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:83

for T being finite Tree holds height (^ T) = (height T) + 1

proof end;

theorem :: TREES_3:84

for T1, T2 being finite Tree holds height (tree (T1,T2)) = (max ((height T1),(height T2))) + 1

proof end;

begin

registration

let D be non empty set ;
let t be Element of FinTrees D;
cluster proj1 t -> finite ;
coherence
dom t is finite by Def8;

end;

definition

let p be FinSequence;
assume A1: p is DTree-yielding ;
defpred S₁[ 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 b₁ being FinSequence st
( dom b₁ = dom p & ( for i being Element of NAT st i in dom p holds
ex T being DecoratedTree st
( T = p . i & b₁ . i = T . {} ) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence st dom b₁ = dom p & ( for i being Element of NAT st i in dom p holds
ex T being DecoratedTree st
( T = p . i & b₁ . i = T . {} ) ) & dom b₂ = dom p & ( for i being Element of NAT st i in dom p holds
ex T being DecoratedTree st
( T = p . i & b₂ . i = T . {} ) ) holds
b₁ = b₂

proof end;

end;

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