:: TREES_3 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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
ex b1 being set st
for x being set holds
( x in b1 iff x is Tree )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff x is Tree ) ) & ( for x being set holds
( x in b2 iff x is Tree ) ) holds
b1 = b2
proof end;
end;

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

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

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

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

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

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

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

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

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

theorem :: TREES_3:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds
( X is constituted-Trees iff X c= Trees )
proof end;

theorem :: TREES_3:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds
( X is constituted-FinTrees iff X c= FinTrees )
proof end;

theorem Th3: :: TREES_3:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( {} is constituted-Trees & {} is constituted-FinTrees & {} is constituted-DTrees )
proof end;

theorem Th13: :: TREES_3:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set holds
( {x} is constituted-Trees iff x is Tree )
proof end;

theorem Th14: :: TREES_3:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set holds
( {x} is constituted-FinTrees iff x is finite Tree )
proof end;

theorem Th15: :: TREES_3:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set holds
( {x} is constituted-DTrees iff x is DecoratedTree )
proof end;

theorem Th16: :: TREES_3:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being set holds
( {x,y} is constituted-DTrees iff ( x is DecoratedTree & y is DecoratedTree ) )
proof end;

theorem :: TREES_3:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set st X is constituted-Trees & Y c= X holds
Y is constituted-Trees
proof end;

theorem :: TREES_3:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set st X is constituted-FinTrees & Y c= X holds
Y is constituted-FinTrees
proof end;

theorem :: TREES_3:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 b1 being set st
( b1 is finite & b1 is constituted-Trees & b1 is constituted-FinTrees & not b1 is empty )
proof end;
cluster non empty finite constituted-DTrees set ;
existence
ex b1 being set st
( b1 is finite & b1 is constituted-DTrees & not b1 is empty )
proof end;
end;

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

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

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

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

definition
let D be non empty constituted-Trees set ;
:: original: Element
redefine mode Element of D -> Tree;
coherence
for b1 being Element of D holds b1 is Tree
by Def3;
end;

definition
let D be non empty constituted-FinTrees set ;
:: original: Element
redefine mode Element of D -> finite Tree;
coherence
for b1 being Element of D holds b1 is finite Tree
by Def4;
end;

definition
let D be non empty constituted-DTrees set ;
:: original: Element
redefine mode Element of D -> DecoratedTree;
coherence
for b1 being Element of D holds b1 is DecoratedTree
by Def5;
end;

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

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

registration
cluster FinTrees -> non empty constituted-Trees 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 b1 being set st
for x being set st x in b1 holds
x is DecoratedTree of D
proof end;
end;

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

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

registration
let D be non empty set ;
cluster non empty finite constituted-DTrees DTree-set of D;
existence
ex b1 being DTree-set of D st
( b1 is finite & not b1 is empty )
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
for b1 being Element of E holds b1 is DecoratedTree of D
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;
:: original: Relation
redefine mode Relation of T,D -> ParametrizedSubset of D;
coherence
for b1 being Relation of T,D holds b1 is ParametrizedSubset of D
proof end;
end;

registration
let T be Tree;
let D be non empty set ;
cluster -> DecoratedTree-like Relation of T,D;
coherence
for b1 being Function of T,D holds b1 is DecoratedTree-like
proof end;
end;

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

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

registration
let D be non empty set ;
cluster Trees D -> non empty constituted-DTrees ;
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 b1 being DTree-set of D st
for T being DecoratedTree of D holds
( dom T is finite iff T in b1 )
proof end;
uniqueness
for b1, b2 being DTree-set of D st ( for T being DecoratedTree of D holds
( dom T is finite iff T in b1 ) ) & ( for T being DecoratedTree of D holds
( dom T is finite iff T in b2 ) ) holds
b1 = b2
proof end;
end;

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

registration
let D be non empty set ;
cluster FinTrees D -> non empty constituted-DTrees ;
coherence
not FinTrees D is empty
proof end;
end;

theorem :: TREES_3:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 :
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 );

theorem Th23: :: TREES_3:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( {} is Tree-yielding & {} is FinTree-yielding & {} is DTree-yielding )
proof end;

theorem Th24: :: TREES_3:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set holds
( <*x*> is Tree-yielding iff x is Tree )
proof end;

theorem Th31: :: TREES_3:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set holds
( <*x*> is FinTree-yielding iff x is finite Tree )
proof end;

theorem Th32: :: TREES_3:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set holds
( <*x*> is DTree-yielding iff x is DecoratedTree )
proof end;

theorem Th33: :: TREES_3:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
ex b1 being FinSequence st
( b1 is Tree-yielding & b1 is FinTree-yielding & not b1 is empty )
proof end;
cluster non empty DTree-yielding set ;
existence
ex b1 being FinSequence st
( b1 is DTree-yielding & not b1 is empty )
proof end;
end;

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

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

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

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

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

registration
let p, q be FinTree-yielding FinSequence;
cluster p ^ q -> Tree-yielding 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 b1 being FinSequence of D holds b1 is DTree-yielding
proof end;
end;

registration
let p, q be DTree-yielding FinSequence;
cluster p ^ q -> DTree-yielding ;
coherence
p ^ q is DTree-yielding
by 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
( <*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 Lm2, Th33;
end;

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

registration
let n be Nat;
let T be finite Tree;
cluster n |-> T -> Tree-yielding 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 Lm2, Th35;
end;

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

theorem Th39: :: TREES_3:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
<:T1,T2:> is DecoratedTree-like
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
<:T1,T2:> is DecoratedTree of D1,D2
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
T * f is DecoratedTree of E
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D1, D2 being non empty set
for T being DecoratedTree of D1,D2 holds <:(T `1 ),(T `2 ):> = T
proof end;

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

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

definition
let T be finite Tree;
:: original: Leaf
redefine mode Leaf of T -> Element of Leaves T;
coherence
for b1 being Leaf of T holds b1 is Element of Leaves T
by TREES_1:def 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 b1 being Tree st
for t being Element of b1 holds
( t in T or ex l being Leaf of T st l is_a_proper_prefix_of t )
proof end;
end;

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

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

registration
let T be finite Tree;
cluster finite T-Substitution of T;
existence
ex b1 being T-Substitution of T st b1 is finite
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being Tree holds T is T-Substitution of 0
proof end;

theorem :: TREES_3:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TREES_3:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
( not T1 \/ T2 is empty & T1 \/ T2 is Tree-like )
by TREES_1:49;
end;

theorem Th50: :: TREES_3:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
ex b1 being Tree st
for x being set holds
( x in b1 iff ( x = {} or ex n being Nat ex q being FinSequence st
( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) ) )
proof end;
uniqueness
for b1, b2 being Tree st ( for x being set holds
( x in b1 iff ( x = {} or ex n being Nat ex q being FinSequence st
( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) ) ) ) & ( for x being set holds
( x in b2 iff ( x = {} or ex n being Nat ex q being FinSequence st
( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def15 defines tree TREES_3:def 15 :
for p being FinSequence st p is Tree-yielding holds
for b2 being Tree holds
( b2 = tree p iff for x being set holds
( x in b2 iff ( x = {} or ex n being 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Tree-yielding FinSequence st tree p = tree q holds
p = q
proof end;

theorem Th54: :: TREES_3:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
tree {} = elementary_tree 0
proof end;

theorem Th56: :: TREES_3:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSequence st p is Tree-yielding holds
elementary_tree (len p) c= tree p
proof end;

theorem Th57: :: TREES_3:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat holds elementary_tree i = tree (i |-> (elementary_tree 0))
proof end;

theorem Th58: :: TREES_3:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being Tree holds ^ T = (elementary_tree 1) with-replacement <*0*>,T
proof end;

theorem :: TREES_3:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being Tree
for p being FinSequence holds
( p in T iff <*0*> ^ p in ^ T )
proof end;

theorem :: TREES_3:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being Tree holds elementary_tree 1 c= ^ T
proof end;

theorem :: TREES_3:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T1, T2 being Tree st T1 c= T2 holds
^ T1 c= ^ T2
proof end;

theorem :: TREES_3:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T1, T2 being Tree st ^ T1 = ^ T2 holds
T1 = T2
proof end;

theorem :: TREES_3:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being Tree holds (^ T) | <*0*> = T
proof end;

theorem :: TREES_3:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T1, T2 being Tree holds (^ T1) with-replacement <*0*>,T2 = ^ T2
proof end;

theorem :: TREES_3:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
^ (elementary_tree 0) = elementary_tree 1
proof end;

theorem Th71: :: TREES_3:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T1, T2 being Tree holds elementary_tree 2 c= tree T1,T2
proof end;

theorem :: TREES_3:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T1, T2 being Tree holds
( (tree T1,T2) | <*0*> = T1 & (tree T1,T2) | <*1*> = T2 )
proof end;

theorem :: TREES_3:78  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
tree (elementary_tree 0),(elementary_tree 0) = elementary_tree 2
proof end;

theorem Th80: :: TREES_3:80  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being finite Tree holds height (^ T) = (height T) + 1
proof end;

theorem :: TREES_3:84  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
dom t is finite
by Def8;
end;

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

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