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

existence

ex b_{1} being set st

for x being set holds

( x in b_{1} iff x is Tree )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff x is Tree ) ) & ( for x being set holds

( x in b_{2} iff x is Tree ) ) holds

b_{1} = b_{2}

end;
ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def1 defines Trees TREES_3:def 1 :

for b_{1} being set holds

( b_{1} = Trees iff for x being set holds

( x in b_{1} iff x is Tree ) );

for b

( b

( x in b

definition

ex b_{1} being Subset of Trees st

for x being set holds

( x in b_{1} iff x is finite Tree )

for b_{1}, b_{2} being Subset of Trees st ( for x being set holds

( x in b_{1} iff x is finite Tree ) ) & ( for x being set holds

( x in b_{2} iff x is finite Tree ) ) holds

b_{1} = b_{2}
end;

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 for x being set holds

( x in it iff x is finite Tree );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def2 defines FinTrees TREES_3:def 2 :

for b_{1} being Subset of Trees holds

( b_{1} = FinTrees iff for x being set holds

( x in b_{1} iff x is finite Tree ) );

for b

( b

( x in b

definition

let IT be set ;

end;
attr IT is constituted-Trees means :Def3: :: TREES_3:def 3

for x being set st x in IT holds

x is Tree;

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;

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;

for x being set st x in IT holds

x is DecoratedTree;

:: 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 );

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 );

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 );

for IT being set holds

( IT is constituted-DTrees iff for x being set st x in IT holds

x is DecoratedTree );

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 )

( ( 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

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 )

( 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 )

( ( 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

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 )

( 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 )

( ( 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

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 )

( X /\ Y is constituted-DTrees & Y /\ X is constituted-DTrees & X \ Y is constituted-DTrees )

proof end;

registration

coherence

for b_{1} being set st b_{1} is empty holds

( b_{1} is constituted-Trees & b_{1} is constituted-FinTrees & b_{1} is constituted-DTrees )

end;
for b

( b

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 ) )

( {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 ) )

( {x,y} is constituted-DTrees iff ( x is DecoratedTree & y is DecoratedTree ) )

proof end;

registration

existence

ex b_{1} being set st

( b_{1} is finite & b_{1} is constituted-Trees & b_{1} is constituted-FinTrees & not b_{1} is empty )

ex b_{1} being set st

( b_{1} is finite & b_{1} is constituted-DTrees & not b_{1} is empty )

end;
ex b

( b

proof end;

existence ex b

( b

proof end;

registration

coherence

for b_{1} being set st b_{1} is constituted-FinTrees holds

b_{1} is constituted-Trees

end;
for b

b

proof end;

registration

let X be constituted-Trees set ;

coherence

for b_{1} being Subset of X holds b_{1} is constituted-Trees

end;
coherence

for b

proof end;

registration

let X be constituted-FinTrees set ;

coherence

for b_{1} being Subset of X holds b_{1} is constituted-FinTrees

end;
coherence

for b

proof end;

registration

let X be constituted-DTrees set ;

coherence

for b_{1} being Subset of X holds b_{1} is constituted-DTrees

end;
coherence

for b

proof end;

registration

let D be non empty constituted-Trees set ;

coherence

for b_{1} being Element of D holds

( not b_{1} is empty & b_{1} is Tree-like )
by Def3;

end;
coherence

for b

( not b

registration

let D be non empty constituted-FinTrees set ;

coherence

for b_{1} being Element of D holds b_{1} is finite
by Def4;

end;
coherence

for b

registration
end;

registration

let D be non empty constituted-DTrees set ;

coherence

for b_{1} being Element of D holds b_{1} is DecoratedTree-like
by Def5;

end;
coherence

for b

registration
end;

registration
end;

registration

existence

ex b_{1} being Subset of Trees st

( b_{1} is constituted-FinTrees & not b_{1} is empty )

end;
ex b

( b

proof end;

definition

let D be non empty set ;

ex b_{1} being non empty set st

for x being set st x in b_{1} holds

x is DecoratedTree of D

end;
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 for x being set st x in it holds

x is DecoratedTree of D;

ex b

for x being set st x in b

x is DecoratedTree of D

proof end;

:: deftheorem Def6 defines DTree-set TREES_3:def 6 :

for D, b_{2} being non empty set holds

( b_{2} is DTree-set of D iff for x being set st x in b_{2} holds

x is DecoratedTree of D );

for D, b

( b

x is DecoratedTree of D );

registration

let D be non empty set ;

coherence

for b_{1} being DTree-set of D holds b_{1} is constituted-DTrees

end;
coherence

for b

proof end;

registration

let D be non empty set ;

existence

ex b_{1} being DTree-set of D st

( b_{1} is finite & not b_{1} is empty )

end;
existence

ex b

( b

proof end;

registration

let D be non empty set ;

let E be non empty DTree-set of D;

coherence

for b_{1} being Element of E holds b_{1} is D -valued
by Def6;

end;
let E be non empty DTree-set of D;

coherence

for b

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

end;
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;

registration

let T be Tree;

let D be non empty set ;

coherence

for b_{1} being Function of T,D holds b_{1} is DecoratedTree-like

end;
let D be non empty set ;

coherence

for b

proof end;

definition

let D be non empty set ;

ex b_{1} being DTree-set of D st

for T being DecoratedTree of D holds T in b_{1}

for b_{1}, b_{2} being DTree-set of D st ( for T being DecoratedTree of D holds T in b_{1} ) & ( for T being DecoratedTree of D holds T in b_{2} ) holds

b_{1} = b_{2}

end;
func Trees D -> DTree-set of D means :Def7: :: TREES_3:def 7

for T being DecoratedTree of D holds T in it;

existence for T being DecoratedTree of D holds T in it;

ex b

for T being DecoratedTree of D holds T in b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def7 defines Trees TREES_3:def 7 :

for D being non empty set

for b_{2} being DTree-set of D holds

( b_{2} = Trees D iff for T being DecoratedTree of D holds T in b_{2} );

for D being non empty set

for b

( b

registration
end;

definition

let D be non empty set ;

ex b_{1} being DTree-set of D st

for T being DecoratedTree of D holds

( dom T is finite iff T in b_{1} )

for b_{1}, b_{2} being DTree-set of D st ( for T being DecoratedTree of D holds

( dom T is finite iff T in b_{1} ) ) & ( for T being DecoratedTree of D holds

( dom T is finite iff T in b_{2} ) ) holds

b_{1} = b_{2}

end;
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 for T being DecoratedTree of D holds

( dom T is finite iff T in it );

ex b

for T being DecoratedTree of D holds

( dom T is finite iff T in b

proof end;

uniqueness for b

( dom T is finite iff T in b

( dom T is finite iff T in b

b

proof end;

:: deftheorem Def8 defines FinTrees TREES_3:def 8 :

for D being non empty set

for b_{2} being DTree-set of D holds

( b_{2} = FinTrees D iff for T being DecoratedTree of D holds

( dom T is finite iff T in b_{2} ) );

for D being non empty set

for b

( b

( dom T is finite iff T in b

begin

:: deftheorem Def9 defines Tree-yielding TREES_3:def 9 :

for IT being Function holds

( IT is Tree-yielding iff rng IT is constituted-Trees );

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 );

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 );

for IT being Function holds

( IT is DTree-yielding iff rng IT is constituted-DTrees );

registration

for b_{1} being Function st b_{1} is empty holds

( b_{1} is Tree-yielding & b_{1} is FinTree-yielding & b_{1} is DTree-yielding )
end;

cluster Relation-like Function-like empty -> Tree-yielding FinTree-yielding DTree-yielding for set ;

coherence for b

( b

proof 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 )

( 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 )

( 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 )

( 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 )

( ( 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 )

( ( 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 )

( ( p is DTree-yielding & q is DTree-yielding ) iff p ^ q is DTree-yielding )

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 ) )

( <*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 ) )

( <*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 )

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 )

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 )

for i being Element of NAT st i <> 0 holds

( i |-> x is DTree-yielding iff x is DecoratedTree )

proof end;

registration

ex b_{1} being FinSequence st

( b_{1} is Tree-yielding & b_{1} is FinTree-yielding & not b_{1} is empty )

ex b_{1} being FinSequence st

( b_{1} is DTree-yielding & not b_{1} is empty )
end;

cluster Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like Tree-yielding FinTree-yielding for set ;

existence ex b

( b

proof end;

cluster Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like DTree-yielding for set ;

existence ex b

( b

proof end;

registration

existence

ex b_{1} being Function st

( b_{1} is Tree-yielding & b_{1} is FinTree-yielding & not b_{1} is empty )

ex b_{1} being Function st

( b_{1} is DTree-yielding & not b_{1} is empty )

end;
ex b

( b

proof end;

existence ex b

( b

proof end;

registration

coherence

for b_{1} being Function st b_{1} is FinTree-yielding holds

b_{1} is Tree-yielding

end;
for b

b

proof end;

registration

let D be non empty constituted-Trees set ;

coherence

for b_{1} being FinSequence of D holds b_{1} is Tree-yielding

end;
coherence

for b

proof end;

registration

let D be non empty constituted-FinTrees set ;

coherence

for b_{1} being FinSequence of D holds b_{1} is FinTree-yielding

end;
coherence

for b

proof end;

registration
end;

registration

let D be non empty constituted-DTrees set ;

coherence

for b_{1} being FinSequence of D holds b_{1} is DTree-yielding

end;
coherence

for b

proof end;

registration
end;

registration

let T be Tree;

coherence

( <*T*> is Tree-yielding & not <*T*> is empty ) by Th28;

let S be Tree;

coherence

( <*T,S*> is Tree-yielding & not <*T,S*> is empty ) by Th31;

end;
coherence

( <*T*> is Tree-yielding & not <*T*> is empty ) by Th28;

let S be Tree;

coherence

( <*T,S*> is Tree-yielding & not <*T,S*> is empty ) by Th31;

registration
end;

registration

let T be finite Tree;

coherence

<*T*> is FinTree-yielding by Th29;

let S be finite Tree;

coherence

<*T,S*> is FinTree-yielding by Th32;

end;
coherence

<*T*> is FinTree-yielding by Th29;

let S be finite Tree;

coherence

<*T,S*> is FinTree-yielding by Th32;

registration
end;

registration

let T be DecoratedTree;

coherence

( <*T*> is DTree-yielding & not <*T*> is empty ) by Th30;

let S be DecoratedTree;

coherence

( <*T,S*> is DTree-yielding & not <*T,S*> is empty ) by Th33;

end;
coherence

( <*T*> is DTree-yielding & not <*T*> is empty ) by Th30;

let S be DecoratedTree;

coherence

( <*T,S*> is DTree-yielding & not <*T,S*> is empty ) by Th33;

registration
end;

registration

let p be DTree-yielding FinSequence;

coherence

( doms p is Tree-yielding & doms p is FinSequence-like )

end;
coherence

( doms p is Tree-yielding & doms p is FinSequence-like )

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;
mode DecoratedTree of D,E is DecoratedTree of [:D,E:];

mode DTree-set of D,E is DTree-set of [:D,E:];

registration

let D1, D2 be non empty set ;

let T1 be DecoratedTree of D1;

let T2 be DecoratedTree of D2;

coherence

<:T1,T2:> is [:D1,D2:] -valued

end;
let T1 be DecoratedTree of D1;

let T2 be DecoratedTree of D2;

coherence

<:T1,T2:> is [:D1,D2:] -valued

proof end;

registration

let D, E be non empty set ;

let T be DecoratedTree of D;

let f be Function of D,E;

coherence

f * T is DecoratedTree-like

end;
let T be DecoratedTree of D;

let f be Function of D,E;

coherence

f * T is DecoratedTree-like

proof 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

redefine func pr2 (D1,D2) -> Function of [:D1,D2:],D2;

coherence

pr2 (D1,D2) is Function of [:D1,D2:],D2

end;
:: 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: pr2redefine func pr2 (D1,D2) -> Function of [:D1,D2:],D2;

coherence

pr2 (D1,D2) is Function of [:D1,D2:],D2

proof end;

definition

let D1, D2 be non empty set ;

let T be DecoratedTree of D1,D2;

correctness

coherence

(pr1 (D1,D2)) * T is DecoratedTree of D1;

;

correctness

coherence

(pr2 (D1,D2)) * T is DecoratedTree of D2;

;

end;
let T be DecoratedTree of D1,D2;

correctness

coherence

(pr1 (D1,D2)) * T is DecoratedTree of D1;

;

correctness

coherence

(pr2 (D1,D2)) * T is DecoratedTree of D2;

;

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

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;

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 )

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;

registration
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_{1} being Element of S holds b_{1} is Element of T

end;
let S be non empty Subset of T;

:: original: Element

redefine mode Element of S -> Element of T;

coherence

for b

proof end;

definition

let T be finite Tree;

:: original: Leaf

redefine mode Leaf of T -> Element of Leaves T;

coherence

for b_{1} being Leaf of T holds b_{1} is Element of Leaves T
by TREES_1:def 7;

end;
:: original: Leaf

redefine mode Leaf of T -> Element of Leaves T;

coherence

for b

definition

let T be finite Tree;

ex b_{1} being Tree st

for t being Element of b_{1} holds

( t in T or ex l being Leaf of T st l is_a_proper_prefix_of t )

end;
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 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 );

ex b

for t being Element of b

( t in T or ex l being Leaf of T st l is_a_proper_prefix_of t )

proof end;

:: deftheorem Def14 defines T-Substitution TREES_3:def 14 :

for T being finite Tree

for b_{2} being Tree holds

( b_{2} is T-Substitution of T iff for t being Element of b_{2} holds

( t in T or ex l being Leaf of T st l is_a_proper_prefix_of t ) );

for T being finite Tree

for b

( b

( 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

end;
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;

registration
end;

definition
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

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)

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 . {}

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

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

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;

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 ) )

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 ;

ex b_{1} being Tree st

for x being set holds

( x in b_{1} 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 b_{1}, b_{2} being Tree st ( for x being set holds

( x in b_{1} 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_{2} 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_{1} = b_{2}

end;
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 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 ) ) );

ex b

for x being set holds

( x in b

( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) ) )

proof end;

uniqueness for b

( x in b

( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) ) ) ) & ( for x being set holds

( x in b

( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) ) ) ) holds

b

proof end;

:: deftheorem Def15 defines tree TREES_3:def 15 :

for p being FinSequence st p is Tree-yielding holds

for b_{2} being Tree holds

( b_{2} = tree p iff for x being set holds

( x in b_{2} 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 p being FinSequence st p is Tree-yielding holds

for b

( b

( x in b

( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) ) ) );

:: deftheorem defines tree TREES_3:def 17 :

for T1, T2 being Tree holds tree (T1,T2) = tree <*T1,T2*>;

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) ) )

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) ) )

( (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 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) )

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

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)

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)

for T1, T2 being Tree holds tree ((p ^ <*T1*>) ^ q) = (tree ((p ^ <*T2*>) ^ q)) with-replacement (<*(len p)*>,T1)

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
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 ) ) )

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 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 ) ) ) )

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

( (tree (T1,T2)) with-replacement (<*0*>,T) = tree (T,T2) & (tree (T1,T2)) with-replacement (<*1*>,T) = tree (T1,T) )

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

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

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

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;

begin

:: from DTCONSTR

registration
end;

definition

let p be FinSequence;

assume B1: p is DTree-yielding ;

defpred S_{1}[ Nat, set ] means ex T being DecoratedTree st

( T = p . $1 & $2 = T . {} );

ex b_{1} being FinSequence st

( dom b_{1} = dom p & ( for i being Element of NAT st i in dom p holds

ex T being DecoratedTree st

( T = p . i & b_{1} . i = T . {} ) ) )

for b_{1}, b_{2} being FinSequence st dom b_{1} = dom p & ( for i being Element of NAT st i in dom p holds

ex T being DecoratedTree st

( T = p . i & b_{1} . i = T . {} ) ) & dom b_{2} = dom p & ( for i being Element of NAT st i in dom p holds

ex T being DecoratedTree st

( T = p . i & b_{2} . i = T . {} ) ) holds

b_{1} = b_{2}

end;
assume B1: p is DTree-yielding ;

defpred S

( 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 ( 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 . {} ) ) );

ex b

( dom b

ex T being DecoratedTree st

( T = p . i & b

proof end;

uniqueness for b

ex T being DecoratedTree st

( T = p . i & b

ex T being DecoratedTree st

( T = p . i & b

b

proof end;

:: deftheorem defines roots TREES_3:def 18 :

for p being FinSequence st p is DTree-yielding holds

for b_{2} being FinSequence holds

( b_{2} = roots p iff ( dom b_{2} = dom p & ( for i being Element of NAT st i in dom p holds

ex T being DecoratedTree st

( T = p . i & b_{2} . i = T . {} ) ) ) );

for p being FinSequence st p is DTree-yielding holds

for b

( b

ex T being DecoratedTree st

( T = p . i & b