:: TREES_3 semantic presentation

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

proof end;

definition

func Trees -> set means :Def1: :: TREES_3:def 1
for x being set holds
( x in it iff x is Tree );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines Trees TREES_3:def 1 :

registration

cluster Trees -> non empty ;
coherence

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines FinTrees TREES_3:def 2 :

registration

cluster FinTrees -> non empty ;
coherence

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 :

:: deftheorem Def4 defines constituted-FinTrees TREES_3:def 4 :

:: deftheorem Def5 defines constituted-DTrees TREES_3:def 5 :

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;

theorem Th12: :: TREES_3:12

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

proof end;

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

proof end;

cluster non empty finite constituted-DTrees set ;
existence

proof end;

end;

registration

cluster constituted-FinTrees -> constituted-Trees set ;
coherence

proof end;

end;

registration

let X be constituted-Trees set ;
cluster -> constituted-Trees Element of bool X;
coherence

proof end;

end;

registration

let X be constituted-FinTrees set ;
cluster -> constituted-Trees constituted-FinTrees Element of bool X;
coherence

proof end;

end;

registration

let X be constituted-DTrees set ;
cluster -> constituted-DTrees Element of bool X;
coherence

proof end;

end;

definition

let D be non empty constituted-Trees set ;
:: original: Element
redefine mode Element of D -> Tree;
coherence by Def3;

end;

definition

let D be non empty constituted-FinTrees set ;
:: original: Element
redefine mode Element of D -> finite Tree;
coherence by Def4;

end;

definition

let D be non empty constituted-DTrees set ;
:: original: Element
redefine mode Element of D -> DecoratedTree;
coherence by Def5;

end;

registration

cluster Trees -> non empty constituted-Trees ;
coherence

proof end;

end;

registration

cluster non empty constituted-Trees constituted-FinTrees Element of bool Trees ;
existence

proof end;

end;

registration

cluster FinTrees -> non empty constituted-Trees constituted-FinTrees ;
coherence

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

proof end;

end;

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

registration

let D be non empty set ;
cluster -> constituted-DTrees DTree-set of D;
coherence

proof end;

end;

registration

let D be non empty set ;
cluster non empty finite constituted-DTrees DTree-set of D;
existence

proof end;

end;

definition

let D be non empty set ;
let E be non empty DTree-set of D;
:: original: Element
redefine mode Element of E -> DecoratedTree of D;
coherence 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

proof end;

:: original: Relation
redefine mode Relation of T,D -> ParametrizedSubset of D;
coherence

proof end;

end;

registration

let T be Tree;
let D be non empty set ;
cluster -> DecoratedTree-like Relation of T,D;
coherence

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines Trees TREES_3:def 7 :

registration

let D be non empty set ;
cluster Trees D -> non empty constituted-DTrees ;
coherence 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines FinTrees TREES_3:def 8 :

registration

let D be non empty set ;
cluster FinTrees D -> non empty constituted-DTrees ;
coherence

proof end;

end;

theorem :: TREES_3:22

for D being non empty set holds FinTrees D c= Trees D

proof end;

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 :

:: deftheorem Def10 defines FinTree-yielding TREES_3:def 10 :

:: deftheorem Def11 defines DTree-yielding TREES_3:def 11 :

theorem Th23: :: TREES_3:23

( {} is Tree-yielding & {} is FinTree-yielding & {} is DTree-yielding )

proof end;

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 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 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 Nat st i <> 0 holds
( i |-> x is DTree-yielding iff x is DecoratedTree )

proof end;

registration

cluster non empty Tree-yielding FinTree-yielding set ;
existence

proof end;

cluster non empty DTree-yielding set ;
existence

proof end;

end;

registration

cluster non empty Tree-yielding FinTree-yielding set ;
existence

proof end;

cluster non empty DTree-yielding set ;
existence

proof end;

end;

registration

cluster FinTree-yielding -> Tree-yielding set ;
coherence

proof end;

end;

registration

let D be non empty constituted-Trees set ;
cluster -> Tree-yielding FinSequence of D;
coherence

proof end;

end;

registration

let p, q be Tree-yielding FinSequence;
cluster p ^ q -> Tree-yielding ;
coherence by Th27;

end;

registration

let D be non empty constituted-FinTrees set ;
cluster -> Tree-yielding FinTree-yielding FinSequence of D;
coherence

proof end;

end;

registration

let p, q be FinTree-yielding FinSequence;
cluster p ^ q -> Tree-yielding FinTree-yielding ;
coherence by Th28;

end;

registration

let D be non empty constituted-DTrees set ;
cluster -> DTree-yielding FinSequence of D;
coherence

proof end;

end;

registration

let p, q be DTree-yielding FinSequence;
cluster p ^ q -> DTree-yielding ;
coherence by Th29;

end;

Lm2: for x, y being set holds
( not <*x*> is empty & not <*x,y*> is empty )

proof end;

registration

let T be Tree;
cluster <*T*> -> non empty Tree-yielding ;
coherence by Th30;
let S be Tree;
cluster <*T,S*> -> non empty Tree-yielding ;
coherence by Lm2, Th33;

end;

registration

let n be Nat;
let T be Tree;
cluster n |-> T -> Tree-yielding ;
coherence

proof end;

end;

registration

let T be finite Tree;
cluster <*T*> -> Tree-yielding FinTree-yielding ;
coherence by Th31;
let S be finite Tree;
cluster <*T,S*> -> non empty Tree-yielding FinTree-yielding ;
coherence by Th34;

end;

registration

let n be Nat;
let T be finite Tree;
cluster n |-> T -> Tree-yielding FinTree-yielding ;
coherence

proof end;

end;

registration

let T be DecoratedTree;
cluster <*T*> -> non empty DTree-yielding ;
coherence by Th32;
let S be DecoratedTree;
cluster <*T,S*> -> non empty DTree-yielding ;
coherence by Lm2, Th35;

end;

registration

let n be Nat;
let T be DecoratedTree;
cluster n |-> T -> DTree-yielding ;
coherence

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

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;

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

proof end;

end;

definition

let D1, D2 be non empty set ;
let T1 be DecoratedTree of D1;
let T2 be DecoratedTree of D2;
:: original: <:
redefine func <:T1,T2:> -> DecoratedTree of D1,D2;
coherence

proof end;

end;

definition

let D, E be non empty set ;
let T be DecoratedTree of D;
let f be Function of D,E;
:: original: *
redefine func f * T -> DecoratedTree of E;
coherence

proof end;

end;

definition

let D1, D2 be non empty set ;
:: original: pr1
redefine func pr1 D1,D2 -> Function of [:D1,D2:],D1;
coherence

proof end;

:: original: pr2
redefine func pr2 D1,D2 -> Function of [:D1,D2:],D2;
coherence

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 ;
func T `2 -> DecoratedTree of D2 equals :: TREES_3:def 13
(pr2 D1,D2) * T;
correctness ;

end;

:: deftheorem defines `1 TREES_3:def 12 :

:: deftheorem defines `2 TREES_3:def 13 :

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

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

proof end;

end;

definition

let T be finite Tree;
:: original: Leaf
redefine mode Leaf of T -> Element of Leaves T;
coherence 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

proof end;

end;

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

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

proof end;

end;

registration

let T be finite Tree;
cluster finite T-Substitution of T;
existence

proof end;

end;

definition

let n be 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 Nat st <*n*> in T1 holds
T1 | <*n*> = T2 | <*n*> ) holds
T1 c= T2

proof end;

Lm4: for n being Nat
for p being FinSequence st n < len p holds
( n + 1 in dom p & p . (n + 1) in rng p )

proof end;

theorem :: TREES_3:45

canceled;

theorem :: TREES_3:46

for T, T' being Tree
for p being FinSequence of NAT st p in Leaves T holds
T c= T with-replacement p,T'

proof end;

theorem :: TREES_3:47

for T, T' being DecoratedTree
for p being Element of dom T holds (T with-replacement p,T') . p = T' . {}

proof end;

theorem :: TREES_3:48

for T, T' being DecoratedTree
for p, q being Element of dom T st not p is_a_prefix_of q holds
(T with-replacement p,T') . q = T . q

proof end;

theorem :: TREES_3:49

for T, T' being DecoratedTree
for p being Element of dom T
for q being Element of dom T' holds (T with-replacement p,T') . (p ^ q) = T' . q

proof end;

registration

let T1, T2 be Tree;
cluster T1 \/ T2 -> non empty Tree-like ;
coherence 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 Nat ex q being FinSequence st
( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def15 defines tree TREES_3:def 15 :

definition

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

end;

:: deftheorem defines ^ TREES_3:def 16 :

definition

let T1, T2 be Tree;
func tree T1,T2 -> Tree equals :: TREES_3:def 17
tree <*T1,T2*>;
correctness ;

end;

:: deftheorem defines tree TREES_3:def 17 :

theorem :: TREES_3:51

for n being 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 Nat : n < len p } & ( for n being 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 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

proof end;

end;

registration

let T be finite Tree;
cluster ^ T -> finite ;
coherence ;

end;

registration

let T1, T2 be finite Tree;
cluster tree T1,T2 -> finite ;
coherence ;

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 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 t' being finite Tree st t' in rng w holds
height t' <= 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;

registration

let D be non empty set ;
let t be Element of FinTrees D;
cluster dom t -> finite ;
coherence 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 Nat st i in dom p holds
ex T being DecoratedTree st
( T = p . i & it . i = T . {} ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defines roots TREES_3:def 18 :