:: by Grzegorz Bancerek

::

:: Received October 8, 1993

:: Copyright (c) 1993-2019 Association of Mizar Users

Lm1: now :: thesis: for x being set

for y being object

for p being FinSequence of x st ( y in dom p or y in dom p ) holds

p . y in x

for y being object

for p being FinSequence of x st ( y in dom p or y in dom p ) holds

p . y in x

let x be set ; :: thesis: for y being object

for p being FinSequence of x st ( y in dom p or y in dom p ) holds

p . y in x

let y be object ; :: thesis: for p being FinSequence of x st ( y in dom p or y in dom p ) holds

p . y in x

let p be FinSequence of x; :: thesis: ( ( y in dom p or y in dom p ) implies p . y in x )

assume ( y in dom p or y in dom p ) ; :: thesis: p . y in x

then A1: p . y in rng p by FUNCT_1:def 3;

rng p c= x by FINSEQ_1:def 4;

hence p . y in x by A1; :: thesis: verum

end;
for p being FinSequence of x st ( y in dom p or y in dom p ) holds

p . y in x

let y be object ; :: thesis: for p being FinSequence of x st ( y in dom p or y in dom p ) holds

p . y in x

let p be FinSequence of x; :: thesis: ( ( y in dom p or y in dom p ) implies p . y in x )

assume ( y in dom p or y in dom p ) ; :: thesis: p . y in x

then A1: p . y in rng p by FUNCT_1:def 3;

rng p c= x by FINSEQ_1:def 4;

hence p . y in x by A1; :: thesis: verum

definition

let T1, T2 be DecoratedTree;

( T1 = T2 iff ( dom T1 = dom T2 & ( for p being Node of T1 holds T1 . p = T2 . p ) ) )

end;
redefine pred T1 = T2 means :: TREES_4:def 1

( dom T1 = dom T2 & ( for p being Node of T1 holds T1 . p = T2 . p ) );

compatibility ( dom T1 = dom T2 & ( for p being Node of T1 holds T1 . p = T2 . p ) );

( T1 = T2 iff ( dom T1 = dom T2 & ( for p being Node of T1 holds T1 . p = T2 . p ) ) )

proof end;

:: deftheorem defines = TREES_4:def 1 :

for T1, T2 being DecoratedTree holds

( T1 = T2 iff ( dom T1 = dom T2 & ( for p being Node of T1 holds T1 . p = T2 . p ) ) );

for T1, T2 being DecoratedTree holds

( T1 = T2 iff ( dom T1 = dom T2 & ( for p being Node of T1 holds T1 . p = T2 . p ) ) );

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

Lm3: now :: thesis: for n being Nat

for x being set

for p being FinSequence of x st n < len p holds

p . (n + 1) in x

for x being set

for p being FinSequence of x st n < len p holds

p . (n + 1) in x

let n be Nat; :: thesis: for x being set

for p being FinSequence of x st n < len p holds

p . (n + 1) in x

let x be set ; :: thesis: for p being FinSequence of x st n < len p holds

p . (n + 1) in x

let p be FinSequence of x; :: thesis: ( n < len p implies p . (n + 1) in x )

assume n < len p ; :: thesis: p . (n + 1) in x

then A1: p . (n + 1) in rng p by Lm2;

rng p c= x by FINSEQ_1:def 4;

hence p . (n + 1) in x by A1; :: thesis: verum

end;
for p being FinSequence of x st n < len p holds

p . (n + 1) in x

let x be set ; :: thesis: for p being FinSequence of x st n < len p holds

p . (n + 1) in x

let p be FinSequence of x; :: thesis: ( n < len p implies p . (n + 1) in x )

assume n < len p ; :: thesis: p . (n + 1) in x

then A1: p . (n + 1) in rng p by Lm2;

rng p c= x by FINSEQ_1:def 4;

hence p . (n + 1) in x by A1; :: thesis: verum

definition
end;

:: deftheorem defines root-tree TREES_4:def 2 :

for x being object holds root-tree x = (elementary_tree 0) --> x;

for x being object holds root-tree x = (elementary_tree 0) --> x;

definition

let D be non empty set ;

let d be Element of D;

:: original: root-tree

redefine func root-tree d -> Element of FinTrees D;

coherence

root-tree d is Element of FinTrees D

end;
let d be Element of D;

:: original: root-tree

redefine func root-tree d -> Element of FinTrees D;

coherence

root-tree d is Element of FinTrees D

proof end;

definition

let x be object ;

let p be FinSequence;

ex b_{1} being DecoratedTree st

( dom b_{1} = elementary_tree (len p) & b_{1} . {} = x & ( for n being Nat st n < len p holds

b_{1} . <*n*> = p . (n + 1) ) )

for b_{1}, b_{2} being DecoratedTree st dom b_{1} = elementary_tree (len p) & b_{1} . {} = x & ( for n being Nat st n < len p holds

b_{1} . <*n*> = p . (n + 1) ) & dom b_{2} = elementary_tree (len p) & b_{2} . {} = x & ( for n being Nat st n < len p holds

b_{2} . <*n*> = p . (n + 1) ) holds

b_{1} = b_{2}

end;
let p be FinSequence;

func x -flat_tree p -> DecoratedTree means :Def3: :: TREES_4:def 3

( dom it = elementary_tree (len p) & it . {} = x & ( for n being Nat st n < len p holds

it . <*n*> = p . (n + 1) ) );

existence ( dom it = elementary_tree (len p) & it . {} = x & ( for n being Nat st n < len p holds

it . <*n*> = p . (n + 1) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def3 defines -flat_tree TREES_4:def 3 :

for x being object

for p being FinSequence

for b_{3} being DecoratedTree holds

( b_{3} = x -flat_tree p iff ( dom b_{3} = elementary_tree (len p) & b_{3} . {} = x & ( for n being Nat st n < len p holds

b_{3} . <*n*> = p . (n + 1) ) ) );

for x being object

for p being FinSequence

for b

( b

b

theorem :: TREES_4:7

for x, y being object

for p, q being FinSequence st x -flat_tree p = y -flat_tree q holds

( x = y & p = q )

for p, q being FinSequence st x -flat_tree p = y -flat_tree q holds

( x = y & p = q )

proof end;

theorem Th8: :: TREES_4:8

for i being Nat

for j being Element of NAT st j < i holds

(elementary_tree i) | <*j*> = elementary_tree 0

for j being Element of NAT st j < i holds

(elementary_tree i) | <*j*> = elementary_tree 0

proof end;

theorem Th9: :: TREES_4:9

for x being object

for p being FinSequence

for i being Element of NAT st i < len p holds

(x -flat_tree p) | <*i*> = root-tree (p . (i + 1))

for p being FinSequence

for i being Element of NAT st i < len p holds

(x -flat_tree p) | <*i*> = root-tree (p . (i + 1))

proof end;

definition

let x be object ;

let p be FinSequence;

assume A1: p is DTree-yielding ;

ex b_{1} being DecoratedTree st

( ex q being DTree-yielding FinSequence st

( p = q & dom b_{1} = tree (doms q) ) & b_{1} . {} = x & ( for n being Nat st n < len p holds

b_{1} | <*n*> = p . (n + 1) ) )

for b_{1}, b_{2} being DecoratedTree st ex q being DTree-yielding FinSequence st

( p = q & dom b_{1} = tree (doms q) ) & b_{1} . {} = x & ( for n being Nat st n < len p holds

b_{1} | <*n*> = p . (n + 1) ) & ex q being DTree-yielding FinSequence st

( p = q & dom b_{2} = tree (doms q) ) & b_{2} . {} = x & ( for n being Nat st n < len p holds

b_{2} | <*n*> = p . (n + 1) ) holds

b_{1} = b_{2}

end;
let p be FinSequence;

assume A1: p is DTree-yielding ;

func x -tree p -> DecoratedTree means :Def4: :: TREES_4:def 4

( ex q being DTree-yielding FinSequence st

( p = q & dom it = tree (doms q) ) & it . {} = x & ( for n being Nat st n < len p holds

it | <*n*> = p . (n + 1) ) );

existence ( ex q being DTree-yielding FinSequence st

( p = q & dom it = tree (doms q) ) & it . {} = x & ( for n being Nat st n < len p holds

it | <*n*> = p . (n + 1) ) );

ex b

( ex q being DTree-yielding FinSequence st

( p = q & dom b

b

proof end;

uniqueness for b

( p = q & dom b

b

( p = q & dom b

b

b

proof end;

:: deftheorem Def4 defines -tree TREES_4:def 4 :

for x being object

for p being FinSequence st p is DTree-yielding holds

for b_{3} being DecoratedTree holds

( b_{3} = x -tree p iff ( ex q being DTree-yielding FinSequence st

( p = q & dom b_{3} = tree (doms q) ) & b_{3} . {} = x & ( for n being Nat st n < len p holds

b_{3} | <*n*> = p . (n + 1) ) ) );

for x being object

for p being FinSequence st p is DTree-yielding holds

for b

( b

( p = q & dom b

b

definition
end;

:: deftheorem defines -tree TREES_4:def 5 :

for x being object

for T being DecoratedTree holds x -tree T = x -tree <*T*>;

for x being object

for T being DecoratedTree holds x -tree T = x -tree <*T*>;

definition

let x be object ;

let T1, T2 be DecoratedTree;

correctness

coherence

x -tree <*T1,T2*> is DecoratedTree;

;

end;
let T1, T2 be DecoratedTree;

correctness

coherence

x -tree <*T1,T2*> is DecoratedTree;

;

:: deftheorem defines -tree TREES_4:def 6 :

for x being object

for T1, T2 being DecoratedTree holds x -tree (T1,T2) = x -tree <*T1,T2*>;

for x being object

for T1, T2 being DecoratedTree holds x -tree (T1,T2) = x -tree <*T1,T2*>;

theorem Th11: :: TREES_4:11

for x, y being object

for p being DTree-yielding FinSequence holds

( y in dom (x -tree p) iff ( y = {} or ex i being Nat ex T being DecoratedTree ex q being Node of T st

( i < len p & T = p . (i + 1) & y = <*i*> ^ q ) ) )

for p being DTree-yielding FinSequence holds

( y in dom (x -tree p) iff ( y = {} or ex i being Nat ex T being DecoratedTree ex q being Node of T st

( i < len p & T = p . (i + 1) & y = <*i*> ^ q ) ) )

proof end;

theorem Th12: :: TREES_4:12

for x being object

for p being DTree-yielding FinSequence

for i being Nat

for T being DecoratedTree

for q being Node of T st i < len p & T = p . (i + 1) holds

(x -tree p) . (<*i*> ^ q) = T . q

for p being DTree-yielding FinSequence

for i being Nat

for T being DecoratedTree

for q being Node of T st i < len p & T = p . (i + 1) holds

(x -tree p) . (<*i*> ^ q) = T . q

proof end;

theorem :: TREES_4:14

for x being object

for T1, T2 being DecoratedTree holds dom (x -tree (T1,T2)) = tree ((dom T1),(dom T2))

for T1, T2 being DecoratedTree holds dom (x -tree (T1,T2)) = tree ((dom T1),(dom T2))

proof end;

theorem :: TREES_4:15

for x, y being object

for p, q being DTree-yielding FinSequence st x -tree p = y -tree q holds

( x = y & p = q )

for p, q being DTree-yielding FinSequence st x -tree p = y -tree q holds

( x = y & p = q )

proof end;

theorem :: TREES_4:16

for x, y being object

for p being FinSequence st root-tree x = y -flat_tree p holds

( x = y & p = {} )

for p being FinSequence st root-tree x = y -flat_tree p holds

( x = y & p = {} )

proof end;

theorem :: TREES_4:17

for x, y being object

for p being FinSequence st root-tree x = y -tree p & p is DTree-yielding holds

( x = y & p = {} )

for p being FinSequence st root-tree x = y -tree p & p is DTree-yielding holds

( x = y & p = {} )

proof end;

theorem :: TREES_4:18

for x, y being object

for p, q being FinSequence st x -flat_tree p = y -tree q & q is DTree-yielding holds

( x = y & len p = len q & ( for i being Nat st i in dom p holds

q . i = root-tree (p . i) ) )

for p, q being FinSequence st x -flat_tree p = y -tree q & q is DTree-yielding holds

( x = y & len p = len q & ( for i being Nat st i in dom p holds

q . i = root-tree (p . i) ) )

proof end;

theorem :: TREES_4:19

for x being object

for p being DTree-yielding FinSequence

for n being Nat

for q being FinSequence st <*n*> ^ q in dom (x -tree p) holds

(x -tree p) . (<*n*> ^ q) = p .. ((n + 1),q)

for p being DTree-yielding FinSequence

for n being Nat

for q being FinSequence st <*n*> ^ q in dom (x -tree p) holds

(x -tree p) . (<*n*> ^ q) = p .. ((n + 1),q)

proof end;

theorem :: TREES_4:21

for x, y being object holds x -flat_tree <*y*> = ((elementary_tree 1) --> x) with-replacement (<*0*>,(root-tree y))

proof end;

theorem :: TREES_4:22

for x being object

for T being DecoratedTree holds x -tree <*T*> = ((elementary_tree 1) --> x) with-replacement (<*0*>,T)

for T being DecoratedTree holds x -tree <*T*> = ((elementary_tree 1) --> x) with-replacement (<*0*>,T)

proof end;

registration

let D be non empty set ;

let d be Element of D;

let p be FinSequence of D;

coherence

d -flat_tree p is D -valued

end;
let d be Element of D;

let p be FinSequence of D;

coherence

d -flat_tree p is D -valued

proof end;

registration

let D be non empty set ;

let F be non empty DTree-set of D;

let d be Element of D;

let p be FinSequence of F;

coherence

d -tree p is D -valued

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

let d be Element of D;

let p be FinSequence of F;

coherence

d -tree p is D -valued

proof end;

registration

let D be non empty set ;

let d be Element of D;

let T be DecoratedTree of D;

coherence

d -tree T is D -valued

end;
let d be Element of D;

let T be DecoratedTree of D;

coherence

d -tree T is D -valued

proof end;

registration

let D be non empty set ;

let d be Element of D;

let T1, T2 be DecoratedTree of D;

coherence

d -tree (T1,T2) is D -valued

end;
let d be Element of D;

let T1, T2 be DecoratedTree of D;

coherence

d -tree (T1,T2) is D -valued

proof end;

definition

let D be non empty set ;

let p be FinSequence of FinTrees D;

:: original: doms

redefine func doms p -> FinSequence of FinTrees ;

coherence

doms p is FinSequence of FinTrees

end;
let p be FinSequence of FinTrees D;

:: original: doms

redefine func doms p -> FinSequence of FinTrees ;

coherence

doms p is FinSequence of FinTrees

proof end;

definition

let D be non empty set ;

let d be Element of D;

let p be FinSequence of FinTrees D;

:: original: -tree

redefine func d -tree p -> Element of FinTrees D;

coherence

d -tree p is Element of FinTrees D

end;
let d be Element of D;

let p be FinSequence of FinTrees D;

:: original: -tree

redefine func d -tree p -> Element of FinTrees D;

coherence

d -tree p is Element of FinTrees D

proof end;

definition

let D be non empty set ;

let x be Subset of D;

:: original: FinSequence

redefine mode FinSequence of x -> FinSequence of D;

coherence

for b_{1} being FinSequence of x holds b_{1} is FinSequence of D

end;
let x be Subset of D;

:: original: FinSequence

redefine mode FinSequence of x -> FinSequence of D;

coherence

for b

proof end;

registration

let D be non empty constituted-DTrees set ;

let X be Subset of D;

coherence

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

end;
let X be Subset of D;

coherence

for b

definition

let T, T9 be DecoratedTree;

let x be set ;

ex b_{1} being DecoratedTree st

( ( for p being FinSequence holds

( p in dom b_{1} iff ( p in dom T or ex q being Node of T ex r being Node of T9 st

( q in Leaves (dom T) & T . q = x & p = q ^ r ) ) ) ) & ( for p being Node of T st ( not p in Leaves (dom T) or T . p <> x ) holds

b_{1} . p = T . p ) & ( for p being Node of T

for q being Node of T9 st p in Leaves (dom T) & T . p = x holds

b_{1} . (p ^ q) = T9 . q ) )

for b_{1}, b_{2} being DecoratedTree st ( for p being FinSequence holds

( p in dom b_{1} iff ( p in dom T or ex q being Node of T ex r being Node of T9 st

( q in Leaves (dom T) & T . q = x & p = q ^ r ) ) ) ) & ( for p being Node of T st ( not p in Leaves (dom T) or T . p <> x ) holds

b_{1} . p = T . p ) & ( for p being Node of T

for q being Node of T9 st p in Leaves (dom T) & T . p = x holds

b_{1} . (p ^ q) = T9 . q ) & ( for p being FinSequence holds

( p in dom b_{2} iff ( p in dom T or ex q being Node of T ex r being Node of T9 st

( q in Leaves (dom T) & T . q = x & p = q ^ r ) ) ) ) & ( for p being Node of T st ( not p in Leaves (dom T) or T . p <> x ) holds

b_{2} . p = T . p ) & ( for p being Node of T

for q being Node of T9 st p in Leaves (dom T) & T . p = x holds

b_{2} . (p ^ q) = T9 . q ) holds

b_{1} = b_{2}

end;
let x be set ;

func (T,x) <- T9 -> DecoratedTree means :Def7: :: TREES_4:def 7

( ( for p being FinSequence holds

( p in dom it iff ( p in dom T or ex q being Node of T ex r being Node of T9 st

( q in Leaves (dom T) & T . q = x & p = q ^ r ) ) ) ) & ( for p being Node of T st ( not p in Leaves (dom T) or T . p <> x ) holds

it . p = T . p ) & ( for p being Node of T

for q being Node of T9 st p in Leaves (dom T) & T . p = x holds

it . (p ^ q) = T9 . q ) );

existence ( ( for p being FinSequence holds

( p in dom it iff ( p in dom T or ex q being Node of T ex r being Node of T9 st

( q in Leaves (dom T) & T . q = x & p = q ^ r ) ) ) ) & ( for p being Node of T st ( not p in Leaves (dom T) or T . p <> x ) holds

it . p = T . p ) & ( for p being Node of T

for q being Node of T9 st p in Leaves (dom T) & T . p = x holds

it . (p ^ q) = T9 . q ) );

ex b

( ( for p being FinSequence holds

( p in dom b

( q in Leaves (dom T) & T . q = x & p = q ^ r ) ) ) ) & ( for p being Node of T st ( not p in Leaves (dom T) or T . p <> x ) holds

b

for q being Node of T9 st p in Leaves (dom T) & T . p = x holds

b

proof end;

uniqueness for b

( p in dom b

( q in Leaves (dom T) & T . q = x & p = q ^ r ) ) ) ) & ( for p being Node of T st ( not p in Leaves (dom T) or T . p <> x ) holds

b

for q being Node of T9 st p in Leaves (dom T) & T . p = x holds

b

( p in dom b

( q in Leaves (dom T) & T . q = x & p = q ^ r ) ) ) ) & ( for p being Node of T st ( not p in Leaves (dom T) or T . p <> x ) holds

b

for q being Node of T9 st p in Leaves (dom T) & T . p = x holds

b

b

proof end;

:: deftheorem Def7 defines <- TREES_4:def 7 :

for T, T9 being DecoratedTree

for x being set

for b_{4} being DecoratedTree holds

( b_{4} = (T,x) <- T9 iff ( ( for p being FinSequence holds

( p in dom b_{4} iff ( p in dom T or ex q being Node of T ex r being Node of T9 st

( q in Leaves (dom T) & T . q = x & p = q ^ r ) ) ) ) & ( for p being Node of T st ( not p in Leaves (dom T) or T . p <> x ) holds

b_{4} . p = T . p ) & ( for p being Node of T

for q being Node of T9 st p in Leaves (dom T) & T . p = x holds

b_{4} . (p ^ q) = T9 . q ) ) );

for T, T9 being DecoratedTree

for x being set

for b

( b

( p in dom b

( q in Leaves (dom T) & T . q = x & p = q ^ r ) ) ) ) & ( for p being Node of T st ( not p in Leaves (dom T) or T . p <> x ) holds

b

for q being Node of T9 st p in Leaves (dom T) & T . p = x holds

b

registration

let D be non empty set ;

let T, T9 be DecoratedTree of D;

let x be set ;

coherence

(T,x) <- T9 is D -valued

end;
let T, T9 be DecoratedTree of D;

let x be set ;

coherence

(T,x) <- T9 is D -valued

proof end;

theorem :: TREES_4:23

for T, T9 being DecoratedTree

for x being set st ( not x in rng T or not x in Leaves T ) holds

(T,x) <- T9 = T

for x being set st ( not x in rng T or not x in Leaves T ) holds

(T,x) <- T9 = T

proof end;

theorem Th24: :: TREES_4:24

for D1, D2 being non empty set

for T being DecoratedTree of D1,D2 holds

( dom (T `1) = dom T & dom (T `2) = dom T )

for T being DecoratedTree of D1,D2 holds

( dom (T `1) = dom T & dom (T `2) = dom T )

proof end;

theorem Th25: :: TREES_4:25

for D1, D2 being non empty set

for d1 being Element of D1

for d2 being Element of D2 holds

( (root-tree [d1,d2]) `1 = root-tree d1 & (root-tree [d1,d2]) `2 = root-tree d2 )

for d1 being Element of D1

for d2 being Element of D2 holds

( (root-tree [d1,d2]) `1 = root-tree d1 & (root-tree [d1,d2]) `2 = root-tree d2 )

proof end;

theorem Th27: :: TREES_4:27

for D1, D2 being non empty set

for d1 being Element of D1

for d2 being Element of D2

for F being non empty DTree-set of D1,D2

for F1 being non empty DTree-set of D1

for p being FinSequence of F

for p1 being FinSequence of F1 st dom p1 = dom p & ( for i being Nat st i in dom p holds

for T being DecoratedTree of D1,D2 st T = p . i holds

p1 . i = T `1 ) holds

([d1,d2] -tree p) `1 = d1 -tree p1

for d1 being Element of D1

for d2 being Element of D2

for F being non empty DTree-set of D1,D2

for F1 being non empty DTree-set of D1

for p being FinSequence of F

for p1 being FinSequence of F1 st dom p1 = dom p & ( for i being Nat st i in dom p holds

for T being DecoratedTree of D1,D2 st T = p . i holds

p1 . i = T `1 ) holds

([d1,d2] -tree p) `1 = d1 -tree p1

proof end;

theorem Th28: :: TREES_4:28

for D1, D2 being non empty set

for d1 being Element of D1

for d2 being Element of D2

for F being non empty DTree-set of D1,D2

for F2 being non empty DTree-set of D2

for p being FinSequence of F

for p2 being FinSequence of F2 st dom p2 = dom p & ( for i being Nat st i in dom p holds

for T being DecoratedTree of D1,D2 st T = p . i holds

p2 . i = T `2 ) holds

([d1,d2] -tree p) `2 = d2 -tree p2

for d1 being Element of D1

for d2 being Element of D2

for F being non empty DTree-set of D1,D2

for F2 being non empty DTree-set of D2

for p being FinSequence of F

for p2 being FinSequence of F2 st dom p2 = dom p & ( for i being Nat st i in dom p holds

for T being DecoratedTree of D1,D2 st T = p . i holds

p2 . i = T `2 ) holds

([d1,d2] -tree p) `2 = d2 -tree p2

proof end;

theorem Th29: :: TREES_4:29

for D1, D2 being non empty set

for d1 being Element of D1

for d2 being Element of D2

for F being non empty DTree-set of D1,D2

for p being FinSequence of F ex p1 being FinSequence of Trees D1 st

( dom p1 = dom p & ( for i being Nat st i in dom p holds

ex T being Element of F st

( T = p . i & p1 . i = T `1 ) ) & ([d1,d2] -tree p) `1 = d1 -tree p1 )

for d1 being Element of D1

for d2 being Element of D2

for F being non empty DTree-set of D1,D2

for p being FinSequence of F ex p1 being FinSequence of Trees D1 st

( dom p1 = dom p & ( for i being Nat st i in dom p holds

ex T being Element of F st

( T = p . i & p1 . i = T `1 ) ) & ([d1,d2] -tree p) `1 = d1 -tree p1 )

proof end;

theorem Th30: :: TREES_4:30

for D1, D2 being non empty set

for d1 being Element of D1

for d2 being Element of D2

for F being non empty DTree-set of D1,D2

for p being FinSequence of F ex p2 being FinSequence of Trees D2 st

( dom p2 = dom p & ( for i being Nat st i in dom p holds

ex T being Element of F st

( T = p . i & p2 . i = T `2 ) ) & ([d1,d2] -tree p) `2 = d2 -tree p2 )

for d1 being Element of D1

for d2 being Element of D2

for F being non empty DTree-set of D1,D2

for p being FinSequence of F ex p2 being FinSequence of Trees D2 st

( dom p2 = dom p & ( for i being Nat st i in dom p holds

ex T being Element of F st

( T = p . i & p2 . i = T `2 ) ) & ([d1,d2] -tree p) `2 = d2 -tree p2 )

proof end;

theorem :: TREES_4:31

for D1, D2 being non empty set

for d1 being Element of D1

for d2 being Element of D2

for p being FinSequence of FinTrees [:D1,D2:] ex p1 being FinSequence of FinTrees D1 st

( dom p1 = dom p & ( for i being Nat st i in dom p holds

ex T being Element of FinTrees [:D1,D2:] st

( T = p . i & p1 . i = T `1 ) ) & ([d1,d2] -tree p) `1 = d1 -tree p1 )

for d1 being Element of D1

for d2 being Element of D2

for p being FinSequence of FinTrees [:D1,D2:] ex p1 being FinSequence of FinTrees D1 st

( dom p1 = dom p & ( for i being Nat st i in dom p holds

ex T being Element of FinTrees [:D1,D2:] st

( T = p . i & p1 . i = T `1 ) ) & ([d1,d2] -tree p) `1 = d1 -tree p1 )

proof end;

theorem :: TREES_4:32

for D1, D2 being non empty set

for d1 being Element of D1

for d2 being Element of D2

for p being FinSequence of FinTrees [:D1,D2:] ex p2 being FinSequence of FinTrees D2 st

( dom p2 = dom p & ( for i being Nat st i in dom p holds

ex T being Element of FinTrees [:D1,D2:] st

( T = p . i & p2 . i = T `2 ) ) & ([d1,d2] -tree p) `2 = d2 -tree p2 )

for d1 being Element of D1

for d2 being Element of D2

for p being FinSequence of FinTrees [:D1,D2:] ex p2 being FinSequence of FinTrees D2 st

( dom p2 = dom p & ( for i being Nat st i in dom p holds

ex T being Element of FinTrees [:D1,D2:] st

( T = p . i & p2 . i = T `2 ) ) & ([d1,d2] -tree p) `2 = d2 -tree p2 )

proof end;