:: TREES_3 semantic presentation
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
let n be Element of NAT ; ::_thesis: for p, q being FinSequence st 1 <= n & n <= len p holds
(p ^ q) . n = p . n
let p, q be FinSequence; ::_thesis: ( 1 <= n & n <= len p implies (p ^ q) . n = p . n )
assume that
A1: 1 <= n and
A2: n <= len p ; ::_thesis: (p ^ q) . n = p . n
n in dom p by A1, A2, FINSEQ_3:25;
hence (p ^ q) . n = p . n by FINSEQ_1:def_7; ::_thesis: verum
end;
begin
definition
func Trees -> set means :Def1: :: TREES_3:def 1
for x being set holds
( x in it iff x is Tree );
existence
ex b1 being set st
for x being set holds
( x in b1 iff x is Tree )
proof
set X = { T where T is Subset of (NAT *) : T is Tree } ;
take { T where T is Subset of (NAT *) : T is Tree } ; ::_thesis: for x being set holds
( x in { T where T is Subset of (NAT *) : T is Tree } iff x is Tree )
let x be set ; ::_thesis: ( x in { T where T is Subset of (NAT *) : T is Tree } iff x is Tree )
thus ( x in { T where T is Subset of (NAT *) : T is Tree } implies x is Tree ) ::_thesis: ( x is Tree implies x in { T where T is Subset of (NAT *) : T is Tree } )
proof
assume x in { T where T is Subset of (NAT *) : T is Tree } ; ::_thesis: x is Tree
then ex T being Subset of (NAT *) st
( x = T & T is Tree ) ;
hence x is Tree ; ::_thesis: verum
end;
assume x is Tree ; ::_thesis: x in { T where T is Subset of (NAT *) : T is Tree }
then reconsider T = x as Tree ;
T is Subset of (NAT *) by TREES_1:def_3;
hence x in { T where T is Subset of (NAT *) : T is Tree } ; ::_thesis: verum
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
defpred S1[ set ] means $1 is Tree;
let T1, T2 be set ; ::_thesis: ( ( for x being set holds
( x in T1 iff x is Tree ) ) & ( for x being set holds
( x in T2 iff x is Tree ) ) implies T1 = T2 )
assume that
A1: for x being set holds
( x in T1 iff S1[x] ) and
A2: for x being set holds
( x in T2 iff S1[x] ) ; ::_thesis: T1 = T2
thus T1 = T2 from XBOOLE_0:sch_2(A1, A2); ::_thesis: verum
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
set T = the Tree;
the Tree in Trees by Def1;
hence not Trees is empty ; ::_thesis: verum
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
set X = { T where T is Element of Trees : T is finite Tree } ;
{ T where T is Element of Trees : T is finite Tree } c= Trees
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { T where T is Element of Trees : T is finite Tree } or x in Trees )
assume x in { T where T is Element of Trees : T is finite Tree } ; ::_thesis: x in Trees
then ex T being Element of Trees st
( x = T & T is finite Tree ) ;
hence x in Trees ; ::_thesis: verum
end;
then reconsider X = { T where T is Element of Trees : T is finite Tree } as Subset of Trees ;
take X ; ::_thesis: for x being set holds
( x in X iff x is finite Tree )
let x be set ; ::_thesis: ( x in X iff x is finite Tree )
thus ( x in X implies x is finite Tree ) ::_thesis: ( x is finite Tree implies x in X )
proof
assume x in X ; ::_thesis: x is finite Tree
then ex T being Element of Trees st
( x = T & T is finite Tree ) ;
hence x is finite Tree ; ::_thesis: verum
end;
assume x is finite Tree ; ::_thesis: x in X
then reconsider T = x as finite Tree ;
T in Trees by Def1;
hence x in X ; ::_thesis: verum
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
defpred S1[ set ] means $1 is finite Tree;
let T1, T2 be Subset of Trees; ::_thesis: ( ( for x being set holds
( x in T1 iff x is finite Tree ) ) & ( for x being set holds
( x in T2 iff x is finite Tree ) ) implies T1 = T2 )
assume that
A1: for x being set holds
( x in T1 iff S1[x] ) and
A2: for x being set holds
( x in T2 iff S1[x] ) ; ::_thesis: T1 = T2
thus T1 = T2 from XBOOLE_0:sch_2(A1, A2); ::_thesis: verum
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
set T = the finite Tree;
the finite Tree in FinTrees by Def2;
hence not FinTrees is empty ; ::_thesis: verum
end;
end;
definition
let IT be set ;
attrIT is constituted-Trees means :Def3: :: TREES_3:def 3
for x being set st x in IT holds
x is Tree;
attrIT is constituted-FinTrees means :Def4: :: TREES_3:def 4
for x being set st x in IT holds
x is finite Tree;
attrIT is constituted-DTrees means :Def5: :: TREES_3:def 5
for x being set st x in IT holds
x is DecoratedTree;
end;
:: deftheorem Def3 defines constituted-Trees TREES_3:def_3_:_
for IT being set holds
( IT is constituted-Trees iff for x being set st x in IT holds
x is Tree );
:: deftheorem Def4 defines constituted-FinTrees TREES_3:def_4_:_
for IT being set holds
( IT is constituted-FinTrees iff for x being set st x in IT holds
x is finite Tree );
:: deftheorem Def5 defines constituted-DTrees TREES_3:def_5_:_
for IT being set holds
( IT is constituted-DTrees iff for x being set st x in IT holds
x is DecoratedTree );
theorem :: TREES_3:1
for X being set holds
( X is constituted-Trees iff X c= Trees )
proof
let X be set ; ::_thesis: ( X is constituted-Trees iff X c= Trees )
thus ( X is constituted-Trees implies X c= Trees ) ::_thesis: ( X c= Trees implies X is constituted-Trees )
proof
assume A1: for x being set st x in X holds
x is Tree ; :: according to TREES_3:def_3 ::_thesis: X c= Trees
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in Trees )
assume x in X ; ::_thesis: x in Trees
then x is Tree by A1;
hence x in Trees by Def1; ::_thesis: verum
end;
assume A2: X c= Trees ; ::_thesis: X is constituted-Trees
let x be set ; :: according to TREES_3:def_3 ::_thesis: ( x in X implies x is Tree )
assume x in X ; ::_thesis: x is Tree
hence x is Tree by A2, Def1; ::_thesis: verum
end;
theorem :: TREES_3:2
for X being set holds
( X is constituted-FinTrees iff X c= FinTrees )
proof
let X be set ; ::_thesis: ( X is constituted-FinTrees iff X c= FinTrees )
thus ( X is constituted-FinTrees implies X c= FinTrees ) ::_thesis: ( X c= FinTrees implies X is constituted-FinTrees )
proof
assume A1: for x being set st x in X holds
x is finite Tree ; :: according to TREES_3:def_4 ::_thesis: X c= FinTrees
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in FinTrees )
assume x in X ; ::_thesis: x in FinTrees
then x is finite Tree by A1;
hence x in FinTrees by Def2; ::_thesis: verum
end;
assume A2: X c= FinTrees ; ::_thesis: X is constituted-FinTrees
let x be set ; :: according to TREES_3:def_4 ::_thesis: ( x in X implies x is finite Tree )
assume x in X ; ::_thesis: x is finite Tree
hence x is finite Tree by A2, Def2; ::_thesis: verum
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
let X, Y be set ; ::_thesis: ( ( X is constituted-Trees & Y is constituted-Trees ) iff X \/ Y is constituted-Trees )
thus ( X is constituted-Trees & Y is constituted-Trees implies X \/ Y is constituted-Trees ) ::_thesis: ( X \/ Y is constituted-Trees implies ( X is constituted-Trees & Y is constituted-Trees ) )
proof
assume that
A1: for x being set st x in X holds
x is Tree and
A2: for x being set st x in Y holds
x is Tree ; :: according to TREES_3:def_3 ::_thesis: X \/ Y is constituted-Trees
let x be set ; :: according to TREES_3:def_3 ::_thesis: ( x in X \/ Y implies x is Tree )
assume x in X \/ Y ; ::_thesis: x is Tree
then ( x in X or x in Y ) by XBOOLE_0:def_3;
hence x is Tree by A1, A2; ::_thesis: verum
end;
assume A3: for x being set st x in X \/ Y holds
x is Tree ; :: according to TREES_3:def_3 ::_thesis: ( X is constituted-Trees & Y is constituted-Trees )
thus X is constituted-Trees ::_thesis: Y is constituted-Trees
proof
let x be set ; :: according to TREES_3:def_3 ::_thesis: ( x in X implies x is Tree )
assume x in X ; ::_thesis: x is Tree
then x in X \/ Y by XBOOLE_0:def_3;
hence x is Tree by A3; ::_thesis: verum
end;
let x be set ; :: according to TREES_3:def_3 ::_thesis: ( x in Y implies x is Tree )
assume x in Y ; ::_thesis: x is Tree
then x in X \/ Y by XBOOLE_0:def_3;
hence x is Tree by A3; ::_thesis: verum
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
let X, Y be set ; ::_thesis: ( X is constituted-Trees & Y is constituted-Trees implies X \+\ Y is constituted-Trees )
assume that
A1: for x being set st x in X holds
x is Tree and
A2: for x being set st x in Y holds
x is Tree ; :: according to TREES_3:def_3 ::_thesis: X \+\ Y is constituted-Trees
let x be set ; :: according to TREES_3:def_3 ::_thesis: ( x in X \+\ Y implies x is Tree )
assume x in X \+\ Y ; ::_thesis: x is Tree
then ( not x in X iff x in Y ) by XBOOLE_0:1;
hence x is Tree by A1, A2; ::_thesis: verum
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
let X, Y be set ; ::_thesis: ( X is constituted-Trees implies ( X /\ Y is constituted-Trees & Y /\ X is constituted-Trees & X \ Y is constituted-Trees ) )
assume A1: for x being set st x in X holds
x is Tree ; :: according to TREES_3:def_3 ::_thesis: ( X /\ Y is constituted-Trees & Y /\ X is constituted-Trees & X \ Y is constituted-Trees )
thus X /\ Y is constituted-Trees ::_thesis: ( Y /\ X is constituted-Trees & X \ Y is constituted-Trees )
proof
let x be set ; :: according to TREES_3:def_3 ::_thesis: ( x in X /\ Y implies x is Tree )
assume x in X /\ Y ; ::_thesis: x is Tree
then x in X by XBOOLE_0:def_4;
hence x is Tree by A1; ::_thesis: verum
end;
hence Y /\ X is constituted-Trees ; ::_thesis: X \ Y is constituted-Trees
let x be set ; :: according to TREES_3:def_3 ::_thesis: ( x in X \ Y implies x is Tree )
assume x in X \ Y ; ::_thesis: x is Tree
hence x is Tree by A1; ::_thesis: verum
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
let X, Y be set ; ::_thesis: ( ( X is constituted-FinTrees & Y is constituted-FinTrees ) iff X \/ Y is constituted-FinTrees )
thus ( X is constituted-FinTrees & Y is constituted-FinTrees implies X \/ Y is constituted-FinTrees ) ::_thesis: ( X \/ Y is constituted-FinTrees implies ( X is constituted-FinTrees & Y is constituted-FinTrees ) )
proof
assume that
A1: for x being set st x in X holds
x is finite Tree and
A2: for x being set st x in Y holds
x is finite Tree ; :: according to TREES_3:def_4 ::_thesis: X \/ Y is constituted-FinTrees
let x be set ; :: according to TREES_3:def_4 ::_thesis: ( x in X \/ Y implies x is finite Tree )
assume x in X \/ Y ; ::_thesis: x is finite Tree
then ( x in X or x in Y ) by XBOOLE_0:def_3;
hence x is finite Tree by A1, A2; ::_thesis: verum
end;
assume A3: for x being set st x in X \/ Y holds
x is finite Tree ; :: according to TREES_3:def_4 ::_thesis: ( X is constituted-FinTrees & Y is constituted-FinTrees )
thus X is constituted-FinTrees ::_thesis: Y is constituted-FinTrees
proof
let x be set ; :: according to TREES_3:def_4 ::_thesis: ( x in X implies x is finite Tree )
assume x in X ; ::_thesis: x is finite Tree
then x in X \/ Y by XBOOLE_0:def_3;
hence x is finite Tree by A3; ::_thesis: verum
end;
let x be set ; :: according to TREES_3:def_4 ::_thesis: ( x in Y implies x is finite Tree )
assume x in Y ; ::_thesis: x is finite Tree
then x in X \/ Y by XBOOLE_0:def_3;
hence x is finite Tree by A3; ::_thesis: verum
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
let X, Y be set ; ::_thesis: ( X is constituted-FinTrees & Y is constituted-FinTrees implies X \+\ Y is constituted-FinTrees )
assume that
A1: for x being set st x in X holds
x is finite Tree and
A2: for x being set st x in Y holds
x is finite Tree ; :: according to TREES_3:def_4 ::_thesis: X \+\ Y is constituted-FinTrees
let x be set ; :: according to TREES_3:def_4 ::_thesis: ( x in X \+\ Y implies x is finite Tree )
assume x in X \+\ Y ; ::_thesis: x is finite Tree
then ( not x in X iff x in Y ) by XBOOLE_0:1;
hence x is finite Tree by A1, A2; ::_thesis: verum
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
let X, Y be set ; ::_thesis: ( X is constituted-FinTrees implies ( X /\ Y is constituted-FinTrees & Y /\ X is constituted-FinTrees & X \ Y is constituted-FinTrees ) )
assume A1: for x being set st x in X holds
x is finite Tree ; :: according to TREES_3:def_4 ::_thesis: ( X /\ Y is constituted-FinTrees & Y /\ X is constituted-FinTrees & X \ Y is constituted-FinTrees )
thus X /\ Y is constituted-FinTrees ::_thesis: ( Y /\ X is constituted-FinTrees & X \ Y is constituted-FinTrees )
proof
let x be set ; :: according to TREES_3:def_4 ::_thesis: ( x in X /\ Y implies x is finite Tree )
assume x in X /\ Y ; ::_thesis: x is finite Tree
then x in X by XBOOLE_0:def_4;
hence x is finite Tree by A1; ::_thesis: verum
end;
hence Y /\ X is constituted-FinTrees ; ::_thesis: X \ Y is constituted-FinTrees
let x be set ; :: according to TREES_3:def_4 ::_thesis: ( x in X \ Y implies x is finite Tree )
assume x in X \ Y ; ::_thesis: x is finite Tree
hence x is finite Tree by A1; ::_thesis: verum
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
let X, Y be set ; ::_thesis: ( ( X is constituted-DTrees & Y is constituted-DTrees ) iff X \/ Y is constituted-DTrees )
thus ( X is constituted-DTrees & Y is constituted-DTrees implies X \/ Y is constituted-DTrees ) ::_thesis: ( X \/ Y is constituted-DTrees implies ( X is constituted-DTrees & Y is constituted-DTrees ) )
proof
assume that
A1: for x being set st x in X holds
x is DecoratedTree and
A2: for x being set st x in Y holds
x is DecoratedTree ; :: according to TREES_3:def_5 ::_thesis: X \/ Y is constituted-DTrees
let x be set ; :: according to TREES_3:def_5 ::_thesis: ( x in X \/ Y implies x is DecoratedTree )
assume x in X \/ Y ; ::_thesis: x is DecoratedTree
then ( x in X or x in Y ) by XBOOLE_0:def_3;
hence x is DecoratedTree by A1, A2; ::_thesis: verum
end;
assume A3: for x being set st x in X \/ Y holds
x is DecoratedTree ; :: according to TREES_3:def_5 ::_thesis: ( X is constituted-DTrees & Y is constituted-DTrees )
thus X is constituted-DTrees ::_thesis: Y is constituted-DTrees
proof
let x be set ; :: according to TREES_3:def_5 ::_thesis: ( x in X implies x is DecoratedTree )
assume x in X ; ::_thesis: x is DecoratedTree
then x in X \/ Y by XBOOLE_0:def_3;
hence x is DecoratedTree by A3; ::_thesis: verum
end;
let x be set ; :: according to TREES_3:def_5 ::_thesis: ( x in Y implies x is DecoratedTree )
assume x in Y ; ::_thesis: x is DecoratedTree
then x in X \/ Y by XBOOLE_0:def_3;
hence x is DecoratedTree by A3; ::_thesis: verum
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
let X, Y be set ; ::_thesis: ( X is constituted-DTrees & Y is constituted-DTrees implies X \+\ Y is constituted-DTrees )
assume that
A1: for x being set st x in X holds
x is DecoratedTree and
A2: for x being set st x in Y holds
x is DecoratedTree ; :: according to TREES_3:def_5 ::_thesis: X \+\ Y is constituted-DTrees
let x be set ; :: according to TREES_3:def_5 ::_thesis: ( x in X \+\ Y implies x is DecoratedTree )
assume x in X \+\ Y ; ::_thesis: x is DecoratedTree
then ( not x in X iff x in Y ) by XBOOLE_0:1;
hence x is DecoratedTree by A1, A2; ::_thesis: verum
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
let X, Y be set ; ::_thesis: ( X is constituted-DTrees implies ( X /\ Y is constituted-DTrees & Y /\ X is constituted-DTrees & X \ Y is constituted-DTrees ) )
assume A1: for x being set st x in X holds
x is DecoratedTree ; :: according to TREES_3:def_5 ::_thesis: ( X /\ Y is constituted-DTrees & Y /\ X is constituted-DTrees & X \ Y is constituted-DTrees )
thus X /\ Y is constituted-DTrees ::_thesis: ( Y /\ X is constituted-DTrees & X \ Y is constituted-DTrees )
proof
let x be set ; :: according to TREES_3:def_5 ::_thesis: ( x in X /\ Y implies x is DecoratedTree )
assume x in X /\ Y ; ::_thesis: x is DecoratedTree
then x in X by XBOOLE_0:def_4;
hence x is DecoratedTree by A1; ::_thesis: verum
end;
hence Y /\ X is constituted-DTrees ; ::_thesis: X \ Y is constituted-DTrees
let x be set ; :: according to TREES_3:def_5 ::_thesis: ( x in X \ Y implies x is DecoratedTree )
assume x in X \ Y ; ::_thesis: x is DecoratedTree
hence x is DecoratedTree by A1; ::_thesis: verum
end;
registration
cluster empty -> constituted-Trees constituted-FinTrees constituted-DTrees for set ;
coherence
for b1 being set st b1 is empty holds
( b1 is constituted-Trees & b1 is constituted-FinTrees & b1 is constituted-DTrees )
proof
let S be set ; ::_thesis: ( S is empty implies ( S is constituted-Trees & S is constituted-FinTrees & S is constituted-DTrees ) )
assume A1: S is empty ; ::_thesis: ( S is constituted-Trees & S is constituted-FinTrees & S is constituted-DTrees )
hence for x being set st x in S holds
x is Tree ; :: according to TREES_3:def_3 ::_thesis: ( S is constituted-FinTrees & S is constituted-DTrees )
thus for x being set st x in S holds
x is finite Tree by A1; :: according to TREES_3:def_4 ::_thesis: S is constituted-DTrees
thus for x being set st x in S holds
x is DecoratedTree by A1; :: according to TREES_3:def_5 ::_thesis: verum
end;
end;
theorem Th12: :: TREES_3:12
for x being set holds
( {x} is constituted-Trees iff x is Tree )
proof
let x be set ; ::_thesis: ( {x} is constituted-Trees iff x is Tree )
thus ( {x} is constituted-Trees implies x is Tree ) ::_thesis: ( x is Tree implies {x} is constituted-Trees )
proof
assume A1: for y being set st y in {x} holds
y is Tree ; :: according to TREES_3:def_3 ::_thesis: x is Tree
x in {x} by TARSKI:def_1;
hence x is Tree by A1; ::_thesis: verum
end;
assume A2: x is Tree ; ::_thesis: {x} is constituted-Trees
let y be set ; :: according to TREES_3:def_3 ::_thesis: ( y in {x} implies y is Tree )
thus ( y in {x} implies y is Tree ) by A2, TARSKI:def_1; ::_thesis: verum
end;
theorem Th13: :: TREES_3:13
for x being set holds
( {x} is constituted-FinTrees iff x is finite Tree )
proof
let x be set ; ::_thesis: ( {x} is constituted-FinTrees iff x is finite Tree )
thus ( {x} is constituted-FinTrees implies x is finite Tree ) ::_thesis: ( x is finite Tree implies {x} is constituted-FinTrees )
proof
assume A1: for y being set st y in {x} holds
y is finite Tree ; :: according to TREES_3:def_4 ::_thesis: x is finite Tree
x in {x} by TARSKI:def_1;
hence x is finite Tree by A1; ::_thesis: verum
end;
assume A2: x is finite Tree ; ::_thesis: {x} is constituted-FinTrees
let y be set ; :: according to TREES_3:def_4 ::_thesis: ( y in {x} implies y is finite Tree )
thus ( y in {x} implies y is finite Tree ) by A2, TARSKI:def_1; ::_thesis: verum
end;
theorem Th14: :: TREES_3:14
for x being set holds
( {x} is constituted-DTrees iff x is DecoratedTree )
proof
let x be set ; ::_thesis: ( {x} is constituted-DTrees iff x is DecoratedTree )
thus ( {x} is constituted-DTrees implies x is DecoratedTree ) ::_thesis: ( x is DecoratedTree implies {x} is constituted-DTrees )
proof
assume A1: for y being set st y in {x} holds
y is DecoratedTree ; :: according to TREES_3:def_5 ::_thesis: x is DecoratedTree
x in {x} by TARSKI:def_1;
hence x is DecoratedTree by A1; ::_thesis: verum
end;
assume A2: x is DecoratedTree ; ::_thesis: {x} is constituted-DTrees
let y be set ; :: according to TREES_3:def_5 ::_thesis: ( y in {x} implies y is DecoratedTree )
thus ( y in {x} implies y is DecoratedTree ) by A2, TARSKI:def_1; ::_thesis: verum
end;
theorem Th15: :: TREES_3:15
for x, y being set holds
( {x,y} is constituted-Trees iff ( x is Tree & y is Tree ) )
proof
let x, y be set ; ::_thesis: ( {x,y} is constituted-Trees iff ( x is Tree & y is Tree ) )
thus ( {x,y} is constituted-Trees implies ( x is Tree & y is Tree ) ) ::_thesis: ( x is Tree & y is Tree implies {x,y} is constituted-Trees )
proof
assume A1: for z being set st z in {x,y} holds
z is Tree ; :: according to TREES_3:def_3 ::_thesis: ( x is Tree & y is Tree )
A2: x in {x,y} by TARSKI:def_2;
y in {x,y} by TARSKI:def_2;
hence ( x is Tree & y is Tree ) by A1, A2; ::_thesis: verum
end;
assume that
A3: x is Tree and
A4: y is Tree ; ::_thesis: {x,y} is constituted-Trees
let z be set ; :: according to TREES_3:def_3 ::_thesis: ( z in {x,y} implies z is Tree )
thus ( z in {x,y} implies z is Tree ) by A3, A4, TARSKI:def_2; ::_thesis: verum
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 ) )
proof
let x, y be set ; ::_thesis: ( {x,y} is constituted-FinTrees iff ( x is finite Tree & y is finite Tree ) )
thus ( {x,y} is constituted-FinTrees implies ( x is finite Tree & y is finite Tree ) ) ::_thesis: ( x is finite Tree & y is finite Tree implies {x,y} is constituted-FinTrees )
proof
assume A1: for z being set st z in {x,y} holds
z is finite Tree ; :: according to TREES_3:def_4 ::_thesis: ( x is finite Tree & y is finite Tree )
A2: x in {x,y} by TARSKI:def_2;
y in {x,y} by TARSKI:def_2;
hence ( x is finite Tree & y is finite Tree ) by A1, A2; ::_thesis: verum
end;
assume that
A3: x is finite Tree and
A4: y is finite Tree ; ::_thesis: {x,y} is constituted-FinTrees
let z be set ; :: according to TREES_3:def_4 ::_thesis: ( z in {x,y} implies z is finite Tree )
thus ( z in {x,y} implies z is finite Tree ) by A3, A4, TARSKI:def_2; ::_thesis: verum
end;
theorem Th17: :: TREES_3:17
for x, y being set holds
( {x,y} is constituted-DTrees iff ( x is DecoratedTree & y is DecoratedTree ) )
proof
let x, y be set ; ::_thesis: ( {x,y} is constituted-DTrees iff ( x is DecoratedTree & y is DecoratedTree ) )
thus ( {x,y} is constituted-DTrees implies ( x is DecoratedTree & y is DecoratedTree ) ) ::_thesis: ( x is DecoratedTree & y is DecoratedTree implies {x,y} is constituted-DTrees )
proof
assume A1: for z being set st z in {x,y} holds
z is DecoratedTree ; :: according to TREES_3:def_5 ::_thesis: ( x is DecoratedTree & y is DecoratedTree )
A2: x in {x,y} by TARSKI:def_2;
y in {x,y} by TARSKI:def_2;
hence ( x is DecoratedTree & y is DecoratedTree ) by A1, A2; ::_thesis: verum
end;
assume that
A3: x is DecoratedTree and
A4: y is DecoratedTree ; ::_thesis: {x,y} is constituted-DTrees
let z be set ; :: according to TREES_3:def_5 ::_thesis: ( z in {x,y} implies z is DecoratedTree )
thus ( z in {x,y} implies z is DecoratedTree ) by A3, A4, TARSKI:def_2; ::_thesis: verum
end;
theorem :: TREES_3:18
for X, Y being set st X is constituted-Trees & Y c= X holds
Y is constituted-Trees
proof
let X, Y be set ; ::_thesis: ( X is constituted-Trees & Y c= X implies Y is constituted-Trees )
assume A1: for x being set st x in X holds
x is Tree ; :: according to TREES_3:def_3 ::_thesis: ( not Y c= X or Y is constituted-Trees )
assume A2: Y c= X ; ::_thesis: Y is constituted-Trees
let x be set ; :: according to TREES_3:def_3 ::_thesis: ( x in Y implies x is Tree )
assume x in Y ; ::_thesis: x is Tree
hence x is Tree by A1, A2; ::_thesis: verum
end;
theorem :: TREES_3:19
for X, Y being set st X is constituted-FinTrees & Y c= X holds
Y is constituted-FinTrees
proof
let X, Y be set ; ::_thesis: ( X is constituted-FinTrees & Y c= X implies Y is constituted-FinTrees )
assume A1: for x being set st x in X holds
x is finite Tree ; :: according to TREES_3:def_4 ::_thesis: ( not Y c= X or Y is constituted-FinTrees )
assume A2: Y c= X ; ::_thesis: Y is constituted-FinTrees
let x be set ; :: according to TREES_3:def_4 ::_thesis: ( x in Y implies x is finite Tree )
assume x in Y ; ::_thesis: x is finite Tree
hence x is finite Tree by A1, A2; ::_thesis: verum
end;
theorem :: TREES_3:20
for X, Y being set st X is constituted-DTrees & Y c= X holds
Y is constituted-DTrees
proof
let X, Y be set ; ::_thesis: ( X is constituted-DTrees & Y c= X implies Y is constituted-DTrees )
assume A1: for x being set st x in X holds
x is DecoratedTree ; :: according to TREES_3:def_5 ::_thesis: ( not Y c= X or Y is constituted-DTrees )
assume A2: Y c= X ; ::_thesis: Y is constituted-DTrees
let x be set ; :: according to TREES_3:def_5 ::_thesis: ( x in Y implies x is DecoratedTree )
assume x in Y ; ::_thesis: x is DecoratedTree
hence x is DecoratedTree by A1, A2; ::_thesis: verum
end;
registration
cluster non empty finite constituted-Trees constituted-FinTrees for set ;
existence
ex b1 being set st
( b1 is finite & b1 is constituted-Trees & b1 is constituted-FinTrees & not b1 is empty )
proof
set T = the finite Tree;
take { the finite Tree} ; ::_thesis: ( { the finite Tree} is finite & { the finite Tree} is constituted-Trees & { the finite Tree} is constituted-FinTrees & not { the finite Tree} is empty )
thus ( { the finite Tree} is finite & { the finite Tree} is constituted-Trees & { the finite Tree} is constituted-FinTrees & not { the finite Tree} is empty ) by Th12, Th13; ::_thesis: verum
end;
cluster non empty finite constituted-DTrees for set ;
existence
ex b1 being set st
( b1 is finite & b1 is constituted-DTrees & not b1 is empty )
proof
set T = the DecoratedTree;
take { the DecoratedTree} ; ::_thesis: ( { the DecoratedTree} is finite & { the DecoratedTree} is constituted-DTrees & not { the DecoratedTree} is empty )
thus ( { the DecoratedTree} is finite & { the DecoratedTree} is constituted-DTrees & not { the DecoratedTree} is empty ) by Th14; ::_thesis: verum
end;
end;
registration
cluster constituted-FinTrees -> constituted-Trees for set ;
coherence
for b1 being set st b1 is constituted-FinTrees holds
b1 is constituted-Trees
proof
let X be set ; ::_thesis: ( X is constituted-FinTrees implies X is constituted-Trees )
assume X is constituted-FinTrees ; ::_thesis: X is constituted-Trees
hence for x being set st x in X holds
x is Tree by Def4; :: according to TREES_3:def_3 ::_thesis: verum
end;
end;
registration
let X be constituted-Trees set ;
cluster -> constituted-Trees for Element of bool X;
coherence
for b1 being Subset of X holds b1 is constituted-Trees
proof
let Y be Subset of X; ::_thesis: Y is constituted-Trees
let x be set ; :: according to TREES_3:def_3 ::_thesis: ( x in Y implies x is Tree )
thus ( x in Y implies x is Tree ) by Def3; ::_thesis: verum
end;
end;
registration
let X be constituted-FinTrees set ;
cluster -> constituted-FinTrees for Element of bool X;
coherence
for b1 being Subset of X holds b1 is constituted-FinTrees
proof
let Y be Subset of X; ::_thesis: Y is constituted-FinTrees
let x be set ; :: according to TREES_3:def_4 ::_thesis: ( x in Y implies x is finite Tree )
thus ( x in Y implies x is finite Tree ) by Def4; ::_thesis: verum
end;
end;
registration
let X be constituted-DTrees set ;
cluster -> constituted-DTrees for Element of bool X;
coherence
for b1 being Subset of X holds b1 is constituted-DTrees
proof
let Y be Subset of X; ::_thesis: Y is constituted-DTrees
let x be set ; :: according to TREES_3:def_5 ::_thesis: ( x in Y implies x is DecoratedTree )
thus ( x in Y implies x is DecoratedTree ) by Def5; ::_thesis: verum
end;
end;
registration
let D be non empty constituted-Trees set ;
cluster -> non empty Tree-like for Element of D;
coherence
for b1 being Element of D holds
( not b1 is empty & b1 is Tree-like ) by Def3;
end;
registration
let D be non empty constituted-FinTrees set ;
cluster -> finite for Element of D;
coherence
for b1 being Element of D holds b1 is finite by Def4;
end;
registration
cluster constituted-DTrees -> functional for set ;
coherence
for b1 being set st b1 is constituted-DTrees holds
b1 is functional
proof
let X be set ; ::_thesis: ( X is constituted-DTrees implies X is functional )
assume A1: X is constituted-DTrees ; ::_thesis: X is functional
let x be set ; :: according to FUNCT_1:def_13 ::_thesis: ( not x in X or x is set )
thus ( not x in X or x is set ) by A1, Def5; ::_thesis: verum
end;
end;
registration
let D be non empty constituted-DTrees set ;
cluster -> DecoratedTree-like for Element of D;
coherence
for b1 being Element of D holds b1 is DecoratedTree-like by Def5;
end;
registration
cluster Trees -> constituted-Trees ;
coherence
Trees is constituted-Trees
proof
let x be set ; :: according to TREES_3:def_3 ::_thesis: ( x in Trees implies x is Tree )
thus ( x in Trees implies x is Tree ) by Def1; ::_thesis: verum
end;
end;
registration
cluster FinTrees -> constituted-FinTrees ;
coherence
FinTrees is constituted-FinTrees
proof
let x be set ; :: according to TREES_3:def_4 ::_thesis: ( x in FinTrees implies x is finite Tree )
thus ( x in FinTrees implies x is finite Tree ) by Def2; ::_thesis: verum
end;
end;
registration
cluster non empty constituted-Trees constituted-FinTrees for Element of bool Trees;
existence
ex b1 being Subset of Trees st
( b1 is constituted-FinTrees & not b1 is empty )
proof
take FinTrees ; ::_thesis: ( FinTrees is constituted-FinTrees & not FinTrees is empty )
thus ( FinTrees is constituted-FinTrees & not FinTrees is empty ) ; ::_thesis: verum
end;
end;
definition
let D be non empty set ;
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
ex b1 being non empty set st
for x being set st x in b1 holds
x is DecoratedTree of D
proof
take {((elementary_tree 0) --> the Element of D)} ; ::_thesis: for x being set st x in {((elementary_tree 0) --> the Element of D)} holds
x is DecoratedTree of D
thus for x being set st x in {((elementary_tree 0) --> the Element of D)} holds
x is DecoratedTree of D by TARSKI:def_1; ::_thesis: verum
end;
end;
:: deftheorem Def6 defines DTree-set TREES_3:def_6_:_
for D, b2 being non empty 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 for DTree-set of D;
coherence
for b1 being DTree-set of D holds b1 is constituted-DTrees
proof
let T be DTree-set of D; ::_thesis: T is constituted-DTrees
let x be set ; :: according to TREES_3:def_5 ::_thesis: ( x in T implies x is DecoratedTree )
thus ( x in T implies x is DecoratedTree ) by Def6; ::_thesis: verum
end;
end;
registration
let D be non empty set ;
cluster functional non empty finite constituted-DTrees for DTree-set of D;
existence
ex b1 being DTree-set of D st
( b1 is finite & not b1 is empty )
proof
set X = { the DecoratedTree of D};
{ the DecoratedTree of D} is constituted-DTrees
proof
let x be set ; :: according to TREES_3:def_5 ::_thesis: ( x in { the DecoratedTree of D} implies x is DecoratedTree )
thus ( x in { the DecoratedTree of D} implies x is DecoratedTree ) by TARSKI:def_1; ::_thesis: verum
end;
then reconsider X = { the DecoratedTree of D} as non empty constituted-DTrees set ;
X is DTree-set of D
proof
let x be set ; :: according to TREES_3:def_6 ::_thesis: ( x in X implies x is DecoratedTree of D )
thus ( x in X implies x is DecoratedTree of D ) by TARSKI:def_1; ::_thesis: verum
end;
then reconsider X = X as DTree-set of D ;
take X ; ::_thesis: ( X is finite & not X is empty )
thus ( X is finite & not X is empty ) ; ::_thesis: verum
end;
end;
registration
let D be non empty set ;
let E be non empty DTree-set of D;
cluster -> D -valued for Element of E;
coherence
for b1 being Element of E holds b1 is D -valued by Def6;
end;
definition
let T be Tree;
let D be non empty set ;
:: original: Funcs
redefine func Funcs (T,D) -> non empty DTree-set of D;
coherence
Funcs (T,D) is non empty DTree-set of D
proof
set F = Funcs (T,D);
Funcs (T,D) is constituted-DTrees
proof
let x be set ; :: according to TREES_3:def_5 ::_thesis: ( x in Funcs (T,D) implies x is DecoratedTree )
assume x in Funcs (T,D) ; ::_thesis: x is DecoratedTree
then ex f being Function st
( x = f & dom f = T & rng f c= D ) by FUNCT_2:def_2;
hence x is DecoratedTree by TREES_2:def_8; ::_thesis: verum
end;
then reconsider F = Funcs (T,D) as non empty constituted-DTrees set ;
F is DTree-set of D
proof
let x be set ; :: according to TREES_3:def_6 ::_thesis: ( x in F implies x is DecoratedTree of D )
assume x in F ; ::_thesis: x is DecoratedTree of D
then ex f being Function st
( x = f & dom f = T & rng f c= D ) by FUNCT_2:def_2;
hence x is DecoratedTree of D by RELAT_1:def_19, TREES_2:def_8; ::_thesis: verum
end;
then reconsider F = F as DTree-set of D ;
set d = the Function of T,D;
A1: dom the Function of T,D = T by FUNCT_2:def_1;
rng the Function of T,D c= D ;
then the Function of T,D in F by A1, FUNCT_2:def_2;
hence Funcs (T,D) is non empty DTree-set of D ; ::_thesis: verum
end;
end;
registration
let T be Tree;
let D be non empty set ;
cluster Function-like quasi_total -> DecoratedTree-like for Element of bool [:T,D:];
coherence
for b1 being Function of T,D holds b1 is DecoratedTree-like
proof
let f be Function of T,D; ::_thesis: f is DecoratedTree-like
thus dom f is Tree by FUNCT_2:def_1; :: according to TREES_2:def_8 ::_thesis: verum
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
set A = { (Funcs (T,D)) where T is Element of Trees : verum } ;
set TT = union { (Funcs (T,D)) where T is Element of Trees : verum } ;
set f = the Element of Trees --> the Element of D;
A1: the Element of Trees --> the Element of D in Funcs ( the Element of Trees ,D) by FUNCT_2:8;
A2: Funcs ( the Element of Trees ,D) in { (Funcs (T,D)) where T is Element of Trees : verum } ;
union { (Funcs (T,D)) where T is Element of Trees : verum } is constituted-DTrees
proof
let x be set ; :: according to TREES_3:def_5 ::_thesis: ( x in union { (Funcs (T,D)) where T is Element of Trees : verum } implies x is DecoratedTree )
assume x in union { (Funcs (T,D)) where T is Element of Trees : verum } ; ::_thesis: x is DecoratedTree
then consider X being set such that
A3: x in X and
A4: X in { (Funcs (T,D)) where T is Element of Trees : verum } by TARSKI:def_4;
ex T being Element of Trees st X = Funcs (T,D) by A4;
hence x is DecoratedTree by A3; ::_thesis: verum
end;
then reconsider TT = union { (Funcs (T,D)) where T is Element of Trees : verum } as non empty constituted-DTrees set by A2, A1, TARSKI:def_4;
TT is DTree-set of D
proof
let x be set ; :: according to TREES_3:def_6 ::_thesis: ( x in TT implies x is DecoratedTree of D )
assume x in TT ; ::_thesis: x is DecoratedTree of D
then consider X being set such that
A5: x in X and
A6: X in { (Funcs (T,D)) where T is Element of Trees : verum } by TARSKI:def_4;
ex T being Element of Trees st X = Funcs (T,D) by A6;
hence x is DecoratedTree of D by A5; ::_thesis: verum
end;
then reconsider TT = TT as DTree-set of D ;
take TT ; ::_thesis: for T being DecoratedTree of D holds T in TT
let T be DecoratedTree of D; ::_thesis: T in TT
reconsider t = dom T as Element of Trees by Def1;
rng T c= D ;
then A7: T in Funcs (t,D) by FUNCT_2:def_2;
Funcs (t,D) in { (Funcs (W,D)) where W is Element of Trees : verum } ;
hence T in TT by A7, TARSKI:def_4; ::_thesis: verum
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
let T1, T2 be DTree-set of D; ::_thesis: ( ( for T being DecoratedTree of D holds T in T1 ) & ( for T being DecoratedTree of D holds T in T2 ) implies T1 = T2 )
assume that
A8: for T being DecoratedTree of D holds T in T1 and
A9: for T being DecoratedTree of D holds T in T2 ; ::_thesis: T1 = T2
thus T1 c= T2 :: according to XBOOLE_0:def_10 ::_thesis: T2 c= T1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in T1 or x in T2 )
thus ( not x in T1 or x in T2 ) by A9; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in T2 or x in T1 )
thus ( not x in T2 or x in T1 ) by A8; ::_thesis: verum
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 ;
coherence
not Trees D is empty ;
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
defpred S1[ set ] means ex T being DecoratedTree of D st
( $1 = T & dom T is finite );
consider X being set such that
A1: for x being set holds
( x in X iff ( x in Trees D & S1[x] ) ) from XBOOLE_0:sch_1();
set T = the finite DecoratedTree of D;
A2: dom the finite DecoratedTree of D is finite ;
the finite DecoratedTree of D in Trees D by Def7;
then A3: not X is empty by A1, A2;
now__::_thesis:_for_x_being_set_st_x_in_X_holds_
x_is_DecoratedTree_of_D
let x be set ; ::_thesis: ( x in X implies x is DecoratedTree of D )
assume x in X ; ::_thesis: x is DecoratedTree of D
then x in Trees D by A1;
hence x is DecoratedTree of D ; ::_thesis: verum
end;
then reconsider X = X as DTree-set of D by A3, Def6;
take X ; ::_thesis: for T being DecoratedTree of D holds
( dom T is finite iff T in X )
let T be DecoratedTree of D; ::_thesis: ( dom T is finite iff T in X )
T in Trees D by Def7;
hence ( dom T is finite implies T in X ) by A1; ::_thesis: ( T in X implies dom T is finite )
assume T in X ; ::_thesis: dom T is finite
then ex t being DecoratedTree of D st
( T = t & dom t is finite ) by A1;
hence dom T is finite ; ::_thesis: verum
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
let T1, T2 be DTree-set of D; ::_thesis: ( ( for T being DecoratedTree of D holds
( dom T is finite iff T in T1 ) ) & ( for T being DecoratedTree of D holds
( dom T is finite iff T in T2 ) ) implies T1 = T2 )
assume that
A4: for T being DecoratedTree of D holds
( dom T is finite iff T in T1 ) and
A5: for T being DecoratedTree of D holds
( dom T is finite iff T in T2 ) ; ::_thesis: T1 = T2
thus T1 c= T2 :: according to XBOOLE_0:def_10 ::_thesis: T2 c= T1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in T1 or x in T2 )
assume A6: x in T1 ; ::_thesis: x in T2
then reconsider T = x as DecoratedTree of D ;
dom T is finite by A4, A6;
hence x in T2 by A5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in T2 or x in T1 )
assume A7: x in T2 ; ::_thesis: x in T1
then reconsider T = x as DecoratedTree of D ;
dom T is finite by A5, A7;
hence x in T1 by A4; ::_thesis: verum
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 ) );
theorem :: TREES_3:21
for D being non empty set holds FinTrees D c= Trees D
proof
let D be non empty set ; ::_thesis: FinTrees D c= Trees D
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in FinTrees D or x in Trees D )
thus ( not x in FinTrees D or x in Trees D ) by Def7; ::_thesis: verum
end;
begin
definition
let IT be Function;
attrIT is Tree-yielding means :Def9: :: TREES_3:def 9
rng IT is constituted-Trees ;
attrIT is FinTree-yielding means :Def10: :: TREES_3:def 10
rng IT is constituted-FinTrees ;
attrIT is DTree-yielding means :Def11: :: TREES_3:def 11
rng IT is constituted-DTrees ;
end;
:: deftheorem Def9 defines Tree-yielding TREES_3:def_9_:_
for IT being Function holds
( IT is Tree-yielding iff rng IT is constituted-Trees );
:: deftheorem Def10 defines FinTree-yielding TREES_3:def_10_:_
for IT being Function holds
( IT is FinTree-yielding iff rng IT is constituted-FinTrees );
:: deftheorem Def11 defines DTree-yielding TREES_3:def_11_:_
for IT being Function holds
( IT is DTree-yielding iff rng IT is constituted-DTrees );
registration
cluster Relation-like Function-like empty -> Tree-yielding FinTree-yielding DTree-yielding for set ;
coherence
for b1 being Function st b1 is empty holds
( b1 is Tree-yielding & b1 is FinTree-yielding & b1 is DTree-yielding )
proof
let F be Function; ::_thesis: ( F is empty implies ( F is Tree-yielding & F is FinTree-yielding & F is DTree-yielding ) )
assume A1: F is empty ; ::_thesis: ( F is Tree-yielding & F is FinTree-yielding & F is DTree-yielding )
hence rng F is constituted-Trees ; :: according to TREES_3:def_9 ::_thesis: ( F is FinTree-yielding & F is DTree-yielding )
thus rng F is constituted-FinTrees by A1; :: according to TREES_3:def_10 ::_thesis: F is DTree-yielding
thus rng F is constituted-DTrees by A1; :: according to TREES_3:def_11 ::_thesis: verum
end;
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 )
proof
let f be Function; ::_thesis: ( f is Tree-yielding iff for x being set st x in dom f holds
f . x is Tree )
thus ( f is Tree-yielding implies for x being set st x in dom f holds
f . x is Tree ) ::_thesis: ( ( for x being set st x in dom f holds
f . x is Tree ) implies f is Tree-yielding )
proof
assume A1: for x being set st x in rng f holds
x is Tree ; :: according to TREES_3:def_3,TREES_3:def_9 ::_thesis: for x being set st x in dom f holds
f . x is Tree
let x be set ; ::_thesis: ( x in dom f implies f . x is Tree )
assume x in dom f ; ::_thesis: f . x is Tree
then f . x in rng f by FUNCT_1:def_3;
hence f . x is Tree by A1; ::_thesis: verum
end;
assume A2: for x being set st x in dom f holds
f . x is Tree ; ::_thesis: f is Tree-yielding
let x be set ; :: according to TREES_3:def_3,TREES_3:def_9 ::_thesis: ( x in rng f implies x is Tree )
assume x in rng f ; ::_thesis: x is Tree
then ex y being set st
( y in dom f & x = f . y ) by FUNCT_1:def_3;
hence x is Tree by A2; ::_thesis: verum
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 )
proof
let f be Function; ::_thesis: ( f is FinTree-yielding iff for x being set st x in dom f holds
f . x is finite Tree )
thus ( f is FinTree-yielding implies for x being set st x in dom f holds
f . x is finite Tree ) ::_thesis: ( ( for x being set st x in dom f holds
f . x is finite Tree ) implies f is FinTree-yielding )
proof
assume A1: for x being set st x in rng f holds
x is finite Tree ; :: according to TREES_3:def_4,TREES_3:def_10 ::_thesis: for x being set st x in dom f holds
f . x is finite Tree
let x be set ; ::_thesis: ( x in dom f implies f . x is finite Tree )
assume x in dom f ; ::_thesis: f . x is finite Tree
then f . x in rng f by FUNCT_1:def_3;
hence f . x is finite Tree by A1; ::_thesis: verum
end;
assume A2: for x being set st x in dom f holds
f . x is finite Tree ; ::_thesis: f is FinTree-yielding
let x be set ; :: according to TREES_3:def_4,TREES_3:def_10 ::_thesis: ( x in rng f implies x is finite Tree )
assume x in rng f ; ::_thesis: x is finite Tree
then ex y being set st
( y in dom f & x = f . y ) by FUNCT_1:def_3;
hence x is finite Tree by A2; ::_thesis: verum
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 )
proof
let f be Function; ::_thesis: ( f is DTree-yielding iff for x being set st x in dom f holds
f . x is DecoratedTree )
thus ( f is DTree-yielding implies for x being set st x in dom f holds
f . x is DecoratedTree ) ::_thesis: ( ( for x being set st x in dom f holds
f . x is DecoratedTree ) implies f is DTree-yielding )
proof
assume A1: for x being set st x in rng f holds
x is DecoratedTree ; :: according to TREES_3:def_5,TREES_3:def_11 ::_thesis: for x being set st x in dom f holds
f . x is DecoratedTree
let x be set ; ::_thesis: ( x in dom f implies f . x is DecoratedTree )
assume x in dom f ; ::_thesis: f . x is DecoratedTree
then f . x in rng f by FUNCT_1:def_3;
hence f . x is DecoratedTree by A1; ::_thesis: verum
end;
assume A2: for x being set st x in dom f holds
f . x is DecoratedTree ; ::_thesis: f is DTree-yielding
let x be set ; :: according to TREES_3:def_5,TREES_3:def_11 ::_thesis: ( x in rng f implies x is DecoratedTree )
assume x in rng f ; ::_thesis: x is DecoratedTree
then ex y being set st
( y in dom f & x = f . y ) by FUNCT_1:def_3;
hence x is DecoratedTree by A2; ::_thesis: verum
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 )
proof
let p, q be FinSequence; ::_thesis: ( ( p is Tree-yielding & q is Tree-yielding ) iff p ^ q is Tree-yielding )
A1: rng (p ^ q) = (rng p) \/ (rng q) by FINSEQ_1:31;
thus ( p is Tree-yielding & q is Tree-yielding implies p ^ q is Tree-yielding ) ::_thesis: ( p ^ q is Tree-yielding implies ( p is Tree-yielding & q is Tree-yielding ) )
proof
assume that
A2: rng p is constituted-Trees and
A3: rng q is constituted-Trees ; :: according to TREES_3:def_9 ::_thesis: p ^ q is Tree-yielding
thus rng (p ^ q) is constituted-Trees by A1, A2, A3, Th3; :: according to TREES_3:def_9 ::_thesis: verum
end;
assume A4: rng (p ^ q) is constituted-Trees ; :: according to TREES_3:def_9 ::_thesis: ( p is Tree-yielding & q is Tree-yielding )
hence rng p is constituted-Trees by A1, Th3; :: according to TREES_3:def_9 ::_thesis: q is Tree-yielding
thus rng q is constituted-Trees by A1, A4, Th3; :: according to TREES_3:def_9 ::_thesis: verum
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 )
proof
let p, q be FinSequence; ::_thesis: ( ( p is FinTree-yielding & q is FinTree-yielding ) iff p ^ q is FinTree-yielding )
A1: rng (p ^ q) = (rng p) \/ (rng q) by FINSEQ_1:31;
thus ( p is FinTree-yielding & q is FinTree-yielding implies p ^ q is FinTree-yielding ) ::_thesis: ( p ^ q is FinTree-yielding implies ( p is FinTree-yielding & q is FinTree-yielding ) )
proof
assume that
A2: rng p is constituted-FinTrees and
A3: rng q is constituted-FinTrees ; :: according to TREES_3:def_10 ::_thesis: p ^ q is FinTree-yielding
thus rng (p ^ q) is constituted-FinTrees by A1, A2, A3, Th6; :: according to TREES_3:def_10 ::_thesis: verum
end;
assume A4: rng (p ^ q) is constituted-FinTrees ; :: according to TREES_3:def_10 ::_thesis: ( p is FinTree-yielding & q is FinTree-yielding )
hence rng p is constituted-FinTrees by A1, Th6; :: according to TREES_3:def_10 ::_thesis: q is FinTree-yielding
thus rng q is constituted-FinTrees by A1, A4, Th6; :: according to TREES_3:def_10 ::_thesis: verum
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 )
proof
let p, q be FinSequence; ::_thesis: ( ( p is DTree-yielding & q is DTree-yielding ) iff p ^ q is DTree-yielding )
A1: rng (p ^ q) = (rng p) \/ (rng q) by FINSEQ_1:31;
thus ( p is DTree-yielding & q is DTree-yielding implies p ^ q is DTree-yielding ) ::_thesis: ( p ^ q is DTree-yielding implies ( p is DTree-yielding & q is DTree-yielding ) )
proof
assume that
A2: rng p is constituted-DTrees and
A3: rng q is constituted-DTrees ; :: according to TREES_3:def_11 ::_thesis: p ^ q is DTree-yielding
thus rng (p ^ q) is constituted-DTrees by A1, A2, A3, Th9; :: according to TREES_3:def_11 ::_thesis: verum
end;
assume A4: rng (p ^ q) is constituted-DTrees ; :: according to TREES_3:def_11 ::_thesis: ( p is DTree-yielding & q is DTree-yielding )
hence rng p is constituted-DTrees by A1, Th9; :: according to TREES_3:def_11 ::_thesis: q is DTree-yielding
thus rng q is constituted-DTrees by A1, A4, Th9; :: according to TREES_3:def_11 ::_thesis: verum
end;
theorem Th28: :: TREES_3:28
for x being set holds
( <*x*> is Tree-yielding iff x is Tree )
proof
let x be set ; ::_thesis: ( <*x*> is Tree-yielding iff x is Tree )
A1: ( x is Tree iff {x} is constituted-Trees ) by Th12;
rng <*x*> = {x} by FINSEQ_1:39;
hence ( <*x*> is Tree-yielding iff x is Tree ) by A1, Def9; ::_thesis: verum
end;
theorem Th29: :: TREES_3:29
for x being set holds
( <*x*> is FinTree-yielding iff x is finite Tree )
proof
let x be set ; ::_thesis: ( <*x*> is FinTree-yielding iff x is finite Tree )
A1: ( x is finite Tree iff {x} is constituted-FinTrees ) by Th13;
rng <*x*> = {x} by FINSEQ_1:39;
hence ( <*x*> is FinTree-yielding iff x is finite Tree ) by A1, Def10; ::_thesis: verum
end;
theorem Th30: :: TREES_3:30
for x being set holds
( <*x*> is DTree-yielding iff x is DecoratedTree )
proof
let x be set ; ::_thesis: ( <*x*> is DTree-yielding iff x is DecoratedTree )
A1: ( x is DecoratedTree iff {x} is constituted-DTrees ) by Th14;
rng <*x*> = {x} by FINSEQ_1:39;
hence ( <*x*> is DTree-yielding iff x is DecoratedTree ) by A1, Def11; ::_thesis: verum
end;
theorem Th31: :: TREES_3:31
for x, y being set holds
( <*x,y*> is Tree-yielding iff ( x is Tree & y is Tree ) )
proof
let x, y be set ; ::_thesis: ( <*x,y*> is Tree-yielding iff ( x is Tree & y is Tree ) )
A1: ( ( x is Tree & y is Tree ) iff {x,y} is constituted-Trees ) by Th15;
rng <*x,y*> = {x,y} by FINSEQ_2:127;
hence ( <*x,y*> is Tree-yielding iff ( x is Tree & y is Tree ) ) by A1, Def9; ::_thesis: verum
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 ) )
proof
let x, y be set ; ::_thesis: ( <*x,y*> is FinTree-yielding iff ( x is finite Tree & y is finite Tree ) )
A1: ( ( x is finite Tree & y is finite Tree ) iff {x,y} is constituted-FinTrees ) by Th16;
rng <*x,y*> = {x,y} by FINSEQ_2:127;
hence ( <*x,y*> is FinTree-yielding iff ( x is finite Tree & y is finite Tree ) ) by A1, Def10; ::_thesis: verum
end;
theorem Th33: :: TREES_3:33
for x, y being set holds
( <*x,y*> is DTree-yielding iff ( x is DecoratedTree & y is DecoratedTree ) )
proof
let x, y be set ; ::_thesis: ( <*x,y*> is DTree-yielding iff ( x is DecoratedTree & y is DecoratedTree ) )
A1: ( ( x is DecoratedTree & y is DecoratedTree ) iff {x,y} is constituted-DTrees ) by Th17;
rng <*x,y*> = {x,y} by FINSEQ_2:127;
hence ( <*x,y*> is DTree-yielding iff ( x is DecoratedTree & y is DecoratedTree ) ) by A1, Def11; ::_thesis: verum
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 )
proof
let x be set ; ::_thesis: for i being Element of NAT st i <> 0 holds
( i |-> x is Tree-yielding iff x is Tree )
let i be Element of NAT ; ::_thesis: ( i <> 0 implies ( i |-> x is Tree-yielding iff x is Tree ) )
assume A1: i <> 0 ; ::_thesis: ( i |-> x is Tree-yielding iff x is Tree )
i |-> x = (Seg i) --> x by FINSEQ_2:def_2;
then rng (i |-> x) = {x} by A1, FUNCOP_1:8;
then ( x is Tree iff rng (i |-> x) is constituted-Trees ) by Th12;
hence ( i |-> x is Tree-yielding iff x is Tree ) by Def9; ::_thesis: verum
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 )
proof
let x be set ; ::_thesis: for i being Element of NAT st i <> 0 holds
( i |-> x is FinTree-yielding iff x is finite Tree )
let i be Element of NAT ; ::_thesis: ( i <> 0 implies ( i |-> x is FinTree-yielding iff x is finite Tree ) )
assume A1: i <> 0 ; ::_thesis: ( i |-> x is FinTree-yielding iff x is finite Tree )
i |-> x = (Seg i) --> x by FINSEQ_2:def_2;
then rng (i |-> x) = {x} by A1, FUNCOP_1:8;
then ( x is finite Tree iff rng (i |-> x) is constituted-FinTrees ) by Th13;
hence ( i |-> x is FinTree-yielding iff x is finite Tree ) by Def10; ::_thesis: verum
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 )
proof
let x be set ; ::_thesis: for i being Element of NAT st i <> 0 holds
( i |-> x is DTree-yielding iff x is DecoratedTree )
let i be Element of NAT ; ::_thesis: ( i <> 0 implies ( i |-> x is DTree-yielding iff x is DecoratedTree ) )
assume A1: i <> 0 ; ::_thesis: ( i |-> x is DTree-yielding iff x is DecoratedTree )
i |-> x = (Seg i) --> x by FINSEQ_2:def_2;
then rng (i |-> x) = {x} by A1, FUNCOP_1:8;
then ( x is DecoratedTree iff rng (i |-> x) is constituted-DTrees ) by Th14;
hence ( i |-> x is DTree-yielding iff x is DecoratedTree ) by Def11; ::_thesis: verum
end;
registration
cluster Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like Tree-yielding FinTree-yielding for set ;
existence
ex b1 being FinSequence st
( b1 is Tree-yielding & b1 is FinTree-yielding & not b1 is empty )
proof
set T = the finite Tree;
take <* the finite Tree*> ; ::_thesis: ( <* the finite Tree*> is Tree-yielding & <* the finite Tree*> is FinTree-yielding & not <* the finite Tree*> is empty )
thus ( <* the finite Tree*> is Tree-yielding & <* the finite Tree*> is FinTree-yielding & not <* the finite Tree*> is empty ) by Th28, Th29; ::_thesis: verum
end;
cluster Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like DTree-yielding for set ;
existence
ex b1 being FinSequence st
( b1 is DTree-yielding & not b1 is empty )
proof
set T = the DecoratedTree;
take <* the DecoratedTree*> ; ::_thesis: ( <* the DecoratedTree*> is DTree-yielding & not <* the DecoratedTree*> is empty )
thus ( <* the DecoratedTree*> is DTree-yielding & not <* the DecoratedTree*> is empty ) by Th30; ::_thesis: verum
end;
end;
registration
cluster Relation-like Function-like non empty Tree-yielding FinTree-yielding for set ;
existence
ex b1 being Function st
( b1 is Tree-yielding & b1 is FinTree-yielding & not b1 is empty )
proof
set p = the non empty Tree-yielding FinTree-yielding FinSequence;
take the non empty Tree-yielding FinTree-yielding FinSequence ; ::_thesis: ( the non empty Tree-yielding FinTree-yielding FinSequence is Tree-yielding & the non empty Tree-yielding FinTree-yielding FinSequence is FinTree-yielding & not the non empty Tree-yielding FinTree-yielding FinSequence is empty )
thus ( the non empty Tree-yielding FinTree-yielding FinSequence is Tree-yielding & the non empty Tree-yielding FinTree-yielding FinSequence is FinTree-yielding & not the non empty Tree-yielding FinTree-yielding FinSequence is empty ) ; ::_thesis: verum
end;
cluster Relation-like Function-like non empty DTree-yielding for set ;
existence
ex b1 being Function st
( b1 is DTree-yielding & not b1 is empty )
proof
set p = the non empty DTree-yielding FinSequence;
take the non empty DTree-yielding FinSequence ; ::_thesis: ( the non empty DTree-yielding FinSequence is DTree-yielding & not the non empty DTree-yielding FinSequence is empty )
thus ( the non empty DTree-yielding FinSequence is DTree-yielding & not the non empty DTree-yielding FinSequence is empty ) ; ::_thesis: verum
end;
end;
registration
cluster Relation-like Function-like FinTree-yielding -> Tree-yielding for set ;
coherence
for b1 being Function st b1 is FinTree-yielding holds
b1 is Tree-yielding
proof
let f be Function; ::_thesis: ( f is FinTree-yielding implies f is Tree-yielding )
assume f is FinTree-yielding ; ::_thesis: f is Tree-yielding
then rng f is constituted-FinTrees set by Def10;
hence rng f is constituted-Trees ; :: according to TREES_3:def_9 ::_thesis: verum
end;
end;
registration
let D be non empty constituted-Trees set ;
cluster -> Tree-yielding for FinSequence of D;
coherence
for b1 being FinSequence of D holds b1 is Tree-yielding
proof
let p be FinSequence of D; ::_thesis: p is Tree-yielding
let x be set ; :: according to TREES_3:def_3,TREES_3:def_9 ::_thesis: ( x in rng p implies x is Tree )
rng p c= D ;
hence ( x in rng p implies x is Tree ) ; ::_thesis: verum
end;
end;
registration
let p, q be Tree-yielding FinSequence;
clusterp ^ q -> Tree-yielding ;
coherence
p ^ q is Tree-yielding by Th25;
end;
registration
let D be non empty constituted-FinTrees set ;
cluster -> FinTree-yielding for FinSequence of D;
coherence
for b1 being FinSequence of D holds b1 is FinTree-yielding
proof
let p be FinSequence of D; ::_thesis: p is FinTree-yielding
let x be set ; :: according to TREES_3:def_4,TREES_3:def_10 ::_thesis: ( x in rng p implies x is finite Tree )
rng p c= D ;
hence ( x in rng p implies x is finite Tree ) ; ::_thesis: verum
end;
end;
registration
let p, q be FinTree-yielding FinSequence;
clusterp ^ q -> FinTree-yielding ;
coherence
p ^ q is FinTree-yielding by Th26;
end;
registration
let D be non empty constituted-DTrees set ;
cluster -> DTree-yielding for FinSequence of D;
coherence
for b1 being FinSequence of D holds b1 is DTree-yielding
proof
let p be FinSequence of D; ::_thesis: p is DTree-yielding
let x be set ; :: according to TREES_3:def_5,TREES_3:def_11 ::_thesis: ( x in rng p implies x is DecoratedTree )
rng p c= D ;
hence ( x in rng p implies x is DecoratedTree ) ; ::_thesis: verum
end;
end;
registration
let p, q be DTree-yielding FinSequence;
clusterp ^ q -> DTree-yielding ;
coherence
p ^ q is DTree-yielding by Th27;
end;
registration
let T be Tree;
cluster<*T*> -> non empty Tree-yielding ;
coherence
( <*T*> is Tree-yielding & not <*T*> is empty ) by Th28;
let S be Tree;
cluster<*T,S*> -> non empty Tree-yielding ;
coherence
( <*T,S*> is Tree-yielding & not <*T,S*> is empty ) by Th31;
end;
registration
let n be Element of NAT ;
let T be Tree;
clustern |-> T -> Tree-yielding ;
coherence
n |-> T is Tree-yielding
proof
0 |-> T = {} ;
hence n |-> T is Tree-yielding by Th34; ::_thesis: verum
end;
end;
registration
let T be finite Tree;
cluster<*T*> -> FinTree-yielding ;
coherence
<*T*> is FinTree-yielding by Th29;
let S be finite Tree;
cluster<*T,S*> -> FinTree-yielding ;
coherence
<*T,S*> is FinTree-yielding by Th32;
end;
registration
let n be Element of NAT ;
let T be finite Tree;
clustern |-> T -> FinTree-yielding ;
coherence
n |-> T is FinTree-yielding
proof
0 |-> T = {} ;
hence n |-> T is FinTree-yielding by Th35; ::_thesis: verum
end;
end;
registration
let T be DecoratedTree;
cluster<*T*> -> non empty DTree-yielding ;
coherence
( <*T*> is DTree-yielding & not <*T*> is empty ) by Th30;
let S be DecoratedTree;
cluster<*T,S*> -> non empty DTree-yielding ;
coherence
( <*T,S*> is DTree-yielding & not <*T,S*> is empty ) by Th33;
end;
registration
let n be Element of NAT ;
let T be DecoratedTree;
clustern |-> T -> DTree-yielding ;
coherence
n |-> T is DTree-yielding
proof
0 |-> T = {} ;
hence n |-> T is DTree-yielding by Th36; ::_thesis: verum
end;
end;
theorem Th37: :: TREES_3:37
for f being DTree-yielding Function holds
( dom (doms f) = dom f & doms f is Tree-yielding )
proof
let f be DTree-yielding Function; ::_thesis: ( dom (doms f) = dom f & doms f is Tree-yielding )
A1: dom (doms f) = f " (SubFuncs (rng f)) by FUNCT_6:def_2;
hence dom (doms f) c= dom f by RELAT_1:132; :: according to XBOOLE_0:def_10 ::_thesis: ( dom f c= dom (doms f) & doms f is Tree-yielding )
thus dom f c= dom (doms f) ::_thesis: doms f is Tree-yielding
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom f or x in dom (doms f) )
assume A2: x in dom f ; ::_thesis: x in dom (doms f)
then f . x is DecoratedTree by Th24;
hence x in dom (doms f) by A1, A2, FUNCT_6:19; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_dom_(doms_f)_holds_
(doms_f)_._x_is_Tree
let x be set ; ::_thesis: ( x in dom (doms f) implies (doms f) . x is Tree )
assume x in dom (doms f) ; ::_thesis: (doms f) . x is Tree
then A3: x in dom f by A1, FUNCT_6:19;
then reconsider g = f . x as DecoratedTree by Th24;
(doms f) . x = dom g by A3, FUNCT_6:22;
hence (doms f) . x is Tree ; ::_thesis: verum
end;
hence doms f is Tree-yielding by Th22; ::_thesis: verum
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
A1: dom (doms p) = dom p by Th37;
Seg (len p) = dom p by FINSEQ_1:def_3;
hence ( doms p is Tree-yielding & doms p is FinSequence-like ) by A1, Th37, FINSEQ_1:def_2; ::_thesis: verum
end;
end;
theorem :: TREES_3:38
for p being DTree-yielding FinSequence holds len (doms p) = len p
proof
let p be DTree-yielding FinSequence; ::_thesis: len (doms p) = len p
A1: dom p = dom (doms p) by Th37;
Seg (len p) = dom p by FINSEQ_1:def_3;
hence len (doms p) = len p by A1, FINSEQ_1:def_3; ::_thesis: verum
end;
Lm2: for D being non empty set
for T being DecoratedTree of D holds T is Function of (dom T),D
proof
let D be non empty set ; ::_thesis: for T being DecoratedTree of D holds T is Function of (dom T),D
let T be DecoratedTree of D; ::_thesis: T is Function of (dom T),D
rng T c= D ;
hence T is Function of (dom T),D by FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum
end;
begin
definition
let D, E be non empty set ;
mode DecoratedTree of D,E is DecoratedTree of [:D,E:];
mode DTree-set of D,E is DTree-set of [:D,E:];
end;
registration
let T1, T2 be DecoratedTree;
cluster<:T1,T2:> -> DecoratedTree-like ;
coherence
<:T1,T2:> is DecoratedTree-like
proof
dom <:T1,T2:> = (dom T1) /\ (dom T2) by FUNCT_3:def_7;
hence <:T1,T2:> is DecoratedTree-like by TREES_2:def_8; ::_thesis: verum
end;
end;
registration
let D1, D2 be non empty set ;
let T1 be DecoratedTree of D1;
let T2 be DecoratedTree of D2;
cluster<:T1,T2:> -> [:D1,D2:] -valued ;
coherence
<:T1,T2:> is [:D1,D2:] -valued
proof
A1: rng <:T1,T2:> c= [:(rng T1),(rng T2):] by FUNCT_3:51;
[:(rng T1),(rng T2):] c= [:D1,D2:] by ZFMISC_1:96;
then rng <:T1,T2:> c= [:D1,D2:] by A1, XBOOLE_1:1;
hence <:T1,T2:> is [:D1,D2:] -valued by RELAT_1:def_19; ::_thesis: verum
end;
end;
registration
let D, E be non empty set ;
let T be DecoratedTree of D;
let f be Function of D,E;
clusterT * f -> DecoratedTree-like ;
coherence
f * T is DecoratedTree-like
proof
reconsider g = T as Function of (dom T),D by Lm2;
reconsider fg = f * g as Function of (dom T),E ;
rng fg c= E ;
hence f * T is DecoratedTree-like ; ::_thesis: verum
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
thus pr1 (D1,D2) is Function of [:D1,D2:],D1 ; ::_thesis: verum
end;
:: original: pr2
redefine func pr2 (D1,D2) -> Function of [:D1,D2:],D2;
coherence
pr2 (D1,D2) is Function of [:D1,D2:],D2
proof
thus pr2 (D1,D2) is Function of [:D1,D2:],D2 ; ::_thesis: verum
end;
end;
definition
let D1, D2 be non empty set ;
let T be DecoratedTree of D1,D2;
funcT `1 -> DecoratedTree of D1 equals :: TREES_3:def 12
(pr1 (D1,D2)) * T;
correctness
coherence
(pr1 (D1,D2)) * T is DecoratedTree of D1;
;
funcT `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 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 )
proof
let D1, D2 be non empty set ; ::_thesis: 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 )
let T be DecoratedTree of D1,D2; ::_thesis: for t being Element of dom T holds
( (T . t) `1 = (T `1) . t & (T `2) . t = (T . t) `2 )
let t be Element of dom T; ::_thesis: ( (T . t) `1 = (T `1) . t & (T `2) . t = (T . t) `2 )
A1: dom (pr1 (D1,D2)) = [:D1,D2:] by FUNCT_2:def_1;
A2: dom (pr2 (D1,D2)) = [:D1,D2:] by FUNCT_2:def_1;
A3: rng T c= [:D1,D2:] ;
then A4: dom (T `1) = dom T by A1, RELAT_1:27;
A5: dom (T `2) = dom T by A2, A3, RELAT_1:27;
A6: T . t = [((T . t) `1),((T . t) `2)] by MCART_1:21;
then A7: (T `1) . t = (pr1 (D1,D2)) . (((T . t) `1),((T . t) `2)) by A4, FUNCT_1:12;
(T `2) . t = (pr2 (D1,D2)) . (((T . t) `1),((T . t) `2)) by A5, A6, FUNCT_1:12;
hence ( (T . t) `1 = (T `1) . t & (T `2) . t = (T . t) `2 ) by A7, FUNCT_3:def_4, FUNCT_3:def_5; ::_thesis: verum
end;
theorem :: TREES_3:40
for D1, D2 being non empty set
for T being DecoratedTree of D1,D2 holds <:(T `1),(T `2):> = T
proof
let D1, D2 be non empty set ; ::_thesis: for T being DecoratedTree of D1,D2 holds <:(T `1),(T `2):> = T
let T be DecoratedTree of D1,D2; ::_thesis: <:(T `1),(T `2):> = T
A1: dom (pr1 (D1,D2)) = [:D1,D2:] by FUNCT_2:def_1;
A2: dom (pr2 (D1,D2)) = [:D1,D2:] by FUNCT_2:def_1;
A3: rng T c= [:D1,D2:] ;
then A4: dom (T `1) = dom T by A1, RELAT_1:27;
A5: dom (T `2) = dom T by A2, A3, RELAT_1:27;
then A6: dom <:(T `1),(T `2):> = dom T by A4, FUNCT_3:50;
now__::_thesis:_for_x_being_set_st_x_in_dom_T_holds_
<:(T_`1),(T_`2):>_._x_=_T_._x
let x be set ; ::_thesis: ( x in dom T implies <:(T `1),(T `2):> . x = T . x )
assume x in dom T ; ::_thesis: <:(T `1),(T `2):> . x = T . x
then reconsider t = x as Element of dom T ;
thus <:(T `1),(T `2):> . x = [((T `1) . t),((T `2) . t)] by A4, A5, FUNCT_3:49
.= [((T . t) `1),((T `2) . t)] by Th39
.= [((T . t) `1),((T . t) `2)] by Th39
.= T . x by MCART_1:21 ; ::_thesis: verum
end;
hence <:(T `1),(T `2):> = T by A6, FUNCT_1:2; ::_thesis: verum
end;
registration
let T be finite Tree;
cluster Leaves T -> non empty finite ;
coherence
( Leaves T is finite & not Leaves T is empty )
proof
A1: T <> {} ;
defpred S1[ set , set ] means ex t1, t2 being Element of T st
( T = t1 & c2 = t2 & t2 is_a_prefix_of t1 );
A2: for x, y being set st S1[x,y] & S1[y,x] holds
x = y by XBOOLE_0:def_10;
A3: for x, y, z being set st S1[x,y] & S1[y,z] holds
S1[x,z] by XBOOLE_1:1;
consider x being set such that
A4: ( x in T & ( for y being set st y in T & y <> x holds
not S1[y,x] ) ) from CARD_2:sch_1(A1, A2, A3);
reconsider x = x as Element of T by A4;
now__::_thesis:_for_p_being_FinSequence_of_NAT_st_p_in_T_holds_
not_x_is_a_proper_prefix_of_p
let p be FinSequence of NAT ; ::_thesis: ( p in T implies not x is_a_proper_prefix_of p )
assume p in T ; ::_thesis: not x is_a_proper_prefix_of p
then reconsider t1 = p as Element of T ;
thus not x is_a_proper_prefix_of p ::_thesis: verum
proof
assume x is_a_prefix_of p ; :: according to XBOOLE_0:def_8 ::_thesis: x = p
then x = t1 by A4;
hence x = p ; ::_thesis: verum
end;
end;
hence ( Leaves T is finite & not Leaves T is empty ) by TREES_1:def_5; ::_thesis: verum
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
let t be Element of S; ::_thesis: t is Element of T
thus t is Element of T ; ::_thesis: verum
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_7;
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
take T ; ::_thesis: for t being Element of T holds
( t in T or ex l being Leaf of T st l is_a_proper_prefix_of t )
thus for t being Element of T holds
( t in T or ex l being Leaf of T st l is_a_proper_prefix_of t ) ; ::_thesis: verum
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 funcT with-replacement (t,S) -> T-Substitution of T;
coherence
T with-replacement (t,S) is T-Substitution of T
proof
let s be Element of T with-replacement (t,S); :: according to TREES_3:def_14 ::_thesis: ( s in T or ex l being Leaf of T st l is_a_proper_prefix_of s )
assume A1: not s in T ; ::_thesis: ex l being Leaf of T st l is_a_proper_prefix_of s
then consider t1 being FinSequence of NAT such that
t1 in S and
A2: s = t ^ t1 by TREES_1:def_9;
take t ; ::_thesis: t is_a_proper_prefix_of s
t ^ {} = t by FINSEQ_1:34;
then t1 <> {} by A1, A2;
hence t is_a_proper_prefix_of s by A2, TREES_1:10; ::_thesis: verum
end;
end;
registration
let T be finite Tree;
cluster non empty finite Tree-like for T-Substitution of T;
existence
ex b1 being T-Substitution of T st b1 is finite
proof
for t being Element of T holds
( t in T or ex l being Leaf of T st l is_a_proper_prefix_of t ) ;
then T is T-Substitution of T by Def14;
hence ex b1 being T-Substitution of T st b1 is finite ; ::_thesis: verum
end;
end;
definition
let n be Element of NAT ;
mode T-Substitution of n is T-Substitution of elementary_tree n;
end;
theorem :: TREES_3:41
for T being Tree holds T is T-Substitution of 0
proof
let T be Tree; ::_thesis: T is T-Substitution of 0
let t be Element of T; :: according to TREES_3:def_14 ::_thesis: ( t in elementary_tree 0 or ex l being Leaf of elementary_tree 0 st l is_a_proper_prefix_of t )
assume A1: not t in elementary_tree 0 ; ::_thesis: ex l being Leaf of elementary_tree 0 st l is_a_proper_prefix_of t
set l = the Leaf of elementary_tree 0;
take the Leaf of elementary_tree 0 ; ::_thesis: the Leaf of elementary_tree 0 is_a_proper_prefix_of t
A2: the Leaf of elementary_tree 0 = {} by TARSKI:def_1, TREES_1:29;
A3: t <> {} by A1, TARSKI:def_1, TREES_1:29;
{} is_a_prefix_of t by XBOOLE_1:2;
hence the Leaf of elementary_tree 0 is_a_proper_prefix_of t by A2, A3, XBOOLE_0:def_8; ::_thesis: verum
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
proof
let T1, T2 be Tree; ::_thesis: ( T1 -level 1 c= T2 -level 1 & ( for n being Element of NAT st <*n*> in T1 holds
T1 | <*n*> = T2 | <*n*> ) implies T1 c= T2 )
assume that
A1: T1 -level 1 c= T2 -level 1 and
A2: for n being Element of NAT st <*n*> in T1 holds
T1 | <*n*> = T2 | <*n*> ; ::_thesis: T1 c= T2
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in T1 or x in T2 )
assume x in T1 ; ::_thesis: x in T2
then reconsider t = x as Element of T1 ;
now__::_thesis:_(_t_<>_{}_implies_t_in_T2_)
assume t <> {} ; ::_thesis: t in T2
then consider p being FinSequence of NAT , n being Element of NAT such that
A3: t = <*n*> ^ p by FINSEQ_2:130;
A4: len <*n*> = 1 by FINSEQ_1:39;
reconsider n = n as Element of NAT ;
reconsider q = <*n*> as Element of T1 by A3, TREES_1:21;
A5: q in T1 -level 1 by A4;
then A6: q in T2 -level 1 by A1;
A7: p in T1 | q by A3, TREES_1:def_6;
T1 | <*n*> = T2 | <*n*> by A2, A5;
hence t in T2 by A3, A6, A7, TREES_1:def_6; ::_thesis: verum
end;
hence x in T2 by TREES_1:22; ::_thesis: verum
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
let n be Element of NAT ; ::_thesis: for p being FinSequence st n < len p holds
( n + 1 in dom p & p . (n + 1) in rng p )
let p be FinSequence; ::_thesis: ( n < len p implies ( n + 1 in dom p & p . (n + 1) in rng p ) )
assume A1: n < len p ; ::_thesis: ( n + 1 in dom p & p . (n + 1) in rng p )
A2: n + 1 >= 0 + 1 by NAT_1:13;
n + 1 <= len p by A1, NAT_1:13;
then n + 1 in dom p by A2, FINSEQ_3:25;
hence ( n + 1 in dom p & p . (n + 1) in rng p ) by FUNCT_1:def_3; ::_thesis: verum
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)
proof
let T, T9 be Tree; ::_thesis: for p being FinSequence of NAT st p in Leaves T holds
T c= T with-replacement (p,T9)
let p be FinSequence of NAT ; ::_thesis: ( p in Leaves T implies T c= T with-replacement (p,T9) )
assume A1: p in Leaves T ; ::_thesis: T c= T with-replacement (p,T9)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in T or x in T with-replacement (p,T9) )
assume x in T ; ::_thesis: x in T with-replacement (p,T9)
then reconsider t = x as Element of T ;
not p is_a_proper_prefix_of t by A1, TREES_1:def_5;
hence x in T with-replacement (p,T9) by A1, TREES_1:def_9; ::_thesis: verum
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 . {}
proof
let T, T9 be DecoratedTree; ::_thesis: for p being Element of dom T holds (T with-replacement (p,T9)) . p = T9 . {}
let p be Element of dom T; ::_thesis: (T with-replacement (p,T9)) . p = T9 . {}
p in (dom T) with-replacement (p,(dom T9)) by TREES_1:def_9;
then A1: ex r being FinSequence of NAT st
( r in dom T9 & p = p ^ r & (T with-replacement (p,T9)) . p = T9 . r ) by TREES_2:def_11;
p = p ^ {} by FINSEQ_1:34;
hence (T with-replacement (p,T9)) . p = T9 . {} by A1, FINSEQ_1:33; ::_thesis: verum
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
proof
let T, T9 be DecoratedTree; ::_thesis: 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
let p, q be Element of dom T; ::_thesis: ( not p is_a_prefix_of q implies (T with-replacement (p,T9)) . q = T . q )
assume A1: not p is_a_prefix_of q ; ::_thesis: (T with-replacement (p,T9)) . q = T . q
then A2: q in (dom T) with-replacement (p,(dom T9)) by TREES_2:7;
for r being FinSequence of NAT holds
( not r in dom T9 or not q = p ^ r or not (T with-replacement (p,T9)) . q = T9 . r ) by A1, TREES_1:1;
hence (T with-replacement (p,T9)) . q = T . q by A2, TREES_2:def_11; ::_thesis: verum
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
proof
let T, T9 be DecoratedTree; ::_thesis: for p being Element of dom T
for q being Element of dom T9 holds (T with-replacement (p,T9)) . (p ^ q) = T9 . q
let p be Element of dom T; ::_thesis: for q being Element of dom T9 holds (T with-replacement (p,T9)) . (p ^ q) = T9 . q
let q be Element of dom T9; ::_thesis: (T with-replacement (p,T9)) . (p ^ q) = T9 . q
A1: p is_a_prefix_of p ^ q by TREES_1:1;
p ^ q in (dom T) with-replacement (p,(dom T9)) by TREES_1:def_9;
then ex r being FinSequence of NAT st
( r in dom T9 & p ^ q = p ^ r & (T with-replacement (p,T9)) . (p ^ q) = T9 . r ) by A1, TREES_2:def_11;
hence (T with-replacement (p,T9)) . (p ^ q) = T9 . q by FINSEQ_1:33; ::_thesis: verum
end;
registration
let T1, T2 be Tree;
clusterT1 \/ T2 -> non empty Tree-like ;
coherence
( not T1 \/ T2 is empty & T1 \/ T2 is Tree-like ) ;
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 ) )
proof
let T1, T2 be Tree; ::_thesis: 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 ) )
let p be Element of T1 \/ T2; ::_thesis: ( ( 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 ) )
thus ( p in T1 & p in T2 implies (T1 \/ T2) | p = (T1 | p) \/ (T2 | p) ) ::_thesis: ( ( not p in T1 implies (T1 \/ T2) | p = T2 | p ) & ( not p in T2 implies (T1 \/ T2) | p = T1 | p ) )
proof
assume that
A1: p in T1 and
A2: p in T2 ; ::_thesis: (T1 \/ T2) | p = (T1 | p) \/ (T2 | p)
let q be FinSequence of NAT ; :: according to TREES_2:def_1 ::_thesis: ( ( not q in (T1 \/ T2) | p or q in (T1 | p) \/ (T2 | p) ) & ( not q in (T1 | p) \/ (T2 | p) or q in (T1 \/ T2) | p ) )
thus ( q in (T1 \/ T2) | p implies q in (T1 | p) \/ (T2 | p) ) ::_thesis: ( not q in (T1 | p) \/ (T2 | p) or q in (T1 \/ T2) | p )
proof
assume q in (T1 \/ T2) | p ; ::_thesis: q in (T1 | p) \/ (T2 | p)
then p ^ q in T1 \/ T2 by TREES_1:def_6;
then ( p ^ q in T1 or p ^ q in T2 ) by XBOOLE_0:def_3;
then ( q in T1 | p or q in T2 | p ) by A1, A2, TREES_1:def_6;
hence q in (T1 | p) \/ (T2 | p) by XBOOLE_0:def_3; ::_thesis: verum
end;
assume q in (T1 | p) \/ (T2 | p) ; ::_thesis: q in (T1 \/ T2) | p
then ( q in T1 | p or q in T2 | p ) by XBOOLE_0:def_3;
then ( p ^ q in T1 or p ^ q in T2 ) by A1, A2, TREES_1:def_6;
then p ^ q in T1 \/ T2 by XBOOLE_0:def_3;
hence q in (T1 \/ T2) | p by TREES_1:def_6; ::_thesis: verum
end;
for T1, T2 being Tree
for p being Element of T1 \/ T2 st not p in T1 holds
(T1 \/ T2) | p = T2 | p
proof
let T1, T2 be Tree; ::_thesis: for p being Element of T1 \/ T2 st not p in T1 holds
(T1 \/ T2) | p = T2 | p
let p be Element of T1 \/ T2; ::_thesis: ( not p in T1 implies (T1 \/ T2) | p = T2 | p )
assume A3: not p in T1 ; ::_thesis: (T1 \/ T2) | p = T2 | p
then A4: p in T2 by XBOOLE_0:def_3;
let q be FinSequence of NAT ; :: according to TREES_2:def_1 ::_thesis: ( ( not q in (T1 \/ T2) | p or q in T2 | p ) & ( not q in T2 | p or q in (T1 \/ T2) | p ) )
thus ( q in (T1 \/ T2) | p implies q in T2 | p ) ::_thesis: ( not q in T2 | p or q in (T1 \/ T2) | p )
proof
assume q in (T1 \/ T2) | p ; ::_thesis: q in T2 | p
then p ^ q in T1 \/ T2 by TREES_1:def_6;
then ( p ^ q in T1 or p ^ q in T2 ) by XBOOLE_0:def_3;
hence q in T2 | p by A3, A4, TREES_1:21, TREES_1:def_6; ::_thesis: verum
end;
assume q in T2 | p ; ::_thesis: q in (T1 \/ T2) | p
then p ^ q in T2 by A4, TREES_1:def_6;
then p ^ q in T1 \/ T2 by XBOOLE_0:def_3;
hence q in (T1 \/ T2) | p by TREES_1:def_6; ::_thesis: verum
end;
hence ( ( not p in T1 implies (T1 \/ T2) | p = T2 | p ) & ( not p in T2 implies (T1 \/ T2) | p = T1 | p ) ) ; ::_thesis: verum
end;
definition
let p be FinSequence;
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
ex b1 being Tree st
for x being set holds
( x in b1 iff ( x = {} or ex n being Element of NAT ex q being FinSequence st
( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) ) )
proof
defpred S1[ set ] means ( $1 = {} or ex n being Element of NAT ex q being FinSequence st
( n < len p & q in p . (n + 1) & $1 = <*n*> ^ q ) );
consider T being set such that
A1: for y being set holds
( y in T iff ( y in NAT * & S1[y] ) ) from XBOOLE_0:sch_1();
<*> NAT in NAT * by FINSEQ_1:def_11;
then reconsider T = T as non empty set by A1;
A2: rng p is constituted-Trees by B1, Def9;
A3: now__::_thesis:_for_n_being_Element_of_NAT_st_n_<_len_p_holds_
p_._(n_+_1)_is_Tree
let n be Element of NAT ; ::_thesis: ( n < len p implies p . (n + 1) is Tree )
assume n < len p ; ::_thesis: p . (n + 1) is Tree
then p . (n + 1) in rng p by Lm3;
hence p . (n + 1) is Tree by A2; ::_thesis: verum
end;
T is Tree-like
proof
thus T c= NAT * :: according to TREES_1:def_3 ::_thesis: ( ( for b1 being FinSequence of NAT holds
( not b1 in T or ProperPrefixes b1 c= T ) ) & ( for b1 being FinSequence of NAT
for b2, b3 being Element of NAT holds
( not b1 ^ <*b2*> in T or not b3 <= b2 or b1 ^ <*b3*> in T ) ) )
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in T or y in NAT * )
thus ( not y in T or y in NAT * ) by A1; ::_thesis: verum
end;
thus for w being FinSequence of NAT st w in T holds
ProperPrefixes w c= T ::_thesis: for b1 being FinSequence of NAT
for b2, b3 being Element of NAT holds
( not b1 ^ <*b2*> in T or not b3 <= b2 or b1 ^ <*b3*> in T )
proof
let w be FinSequence of NAT ; ::_thesis: ( w in T implies ProperPrefixes w c= T )
assume A4: w in T ; ::_thesis: ProperPrefixes w c= T
now__::_thesis:_(_w_<>_{}_implies_ProperPrefixes_w_c=_T_)
assume w <> {} ; ::_thesis: ProperPrefixes w c= T
then consider n being Element of NAT , q being FinSequence such that
A5: n < len p and
A6: q in p . (n + 1) and
A7: w = <*n*> ^ q by A1, A4;
reconsider q = q as FinSequence of NAT by A7, FINSEQ_1:36;
thus ProperPrefixes w c= T ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ProperPrefixes w or x in T )
assume x in ProperPrefixes w ; ::_thesis: x in T
then consider r being FinSequence such that
A8: x = r and
A9: r is_a_proper_prefix_of w by TREES_1:def_2;
r is_a_prefix_of w by A9, XBOOLE_0:def_8;
then consider k being Element of NAT such that
A10: r = w | (Seg k) by TREES_1:def_1;
rng r = w .: (Seg k) by A10, RELAT_1:115;
then reconsider r = r as FinSequence of NAT by FINSEQ_1:def_4;
A11: r in NAT * by FINSEQ_1:def_11;
now__::_thesis:_(_r_<>_{}_implies_x_in_T_)
assume r <> {} ; ::_thesis: x in T
then consider r1 being FinSequence of NAT , i being Element of NAT such that
A12: r = <*i*> ^ r1 by FINSEQ_2:130;
A13: dom <*i*> = Seg 1 by FINSEQ_1:38;
A14: 1 in Seg 1 by FINSEQ_1:2, TARSKI:def_1;
A15: Seg 1 c= dom r by A12, A13, FINSEQ_1:26;
A16: r . 1 = i by A12, FINSEQ_1:41;
A17: w . 1 = n by A7, FINSEQ_1:41;
A18: r . 1 = w . 1 by A10, A14, A15, FUNCT_1:47;
then A19: r1 is_a_proper_prefix_of q by A7, A9, A12, A16, A17, TREES_1:49;
A20: p . (n + 1) is Tree by A3, A5;
r1 is_a_prefix_of q by A19, XBOOLE_0:def_8;
then r1 in p . (n + 1) by A6, A20, TREES_1:20;
hence x in T by A1, A5, A8, A11, A12, A16, A17, A18; ::_thesis: verum
end;
hence x in T by A1, A8, A11; ::_thesis: verum
end;
end;
hence ProperPrefixes w c= T by TREES_1:15, XBOOLE_1:2; ::_thesis: verum
end;
let w be FinSequence of NAT ; ::_thesis: for b1, b2 being Element of NAT holds
( not w ^ <*b1*> in T or not b2 <= b1 or w ^ <*b2*> in T )
let k, n be Element of NAT ; ::_thesis: ( not w ^ <*k*> in T or not n <= k or w ^ <*n*> in T )
assume that
A21: w ^ <*k*> in T and
A22: n <= k ; ::_thesis: w ^ <*n*> in T
A23: now__::_thesis:_(_w_=_{}_implies_w_^_<*n*>_in_T_)
assume A24: w = {} ; ::_thesis: w ^ <*n*> in T
then <*k*> in T by A21, FINSEQ_1:34;
then consider m being Element of NAT , q being FinSequence such that
A25: m < len p and
q in p . (m + 1) and
A26: <*k*> = <*m*> ^ q by A1;
A27: <*k*> . 1 = k by FINSEQ_1:def_8;
(<*m*> ^ q) . 1 = m by FINSEQ_1:41;
then A28: n < len p by A22, A25, A26, A27, XXREAL_0:2;
then p . (n + 1) in rng p by Lm3;
then A29: {} in p . (n + 1) by A2, TREES_1:22;
A30: <*n*> ^ {} = <*n*> by FINSEQ_1:34;
A31: {} ^ <*n*> = <*n*> by FINSEQ_1:34;
<*n*> in NAT * by FINSEQ_1:def_11;
hence w ^ <*n*> in T by A1, A24, A28, A29, A30, A31; ::_thesis: verum
end;
now__::_thesis:_(_w_<>_{}_implies_w_^_<*n*>_in_T_)
assume w <> {} ; ::_thesis: w ^ <*n*> in T
then consider q being FinSequence of NAT , m being Element of NAT such that
A32: w = <*m*> ^ q by FINSEQ_2:130;
consider m9 being Element of NAT , r being FinSequence such that
A33: m9 < len p and
A34: r in p . (m9 + 1) and
A35: w ^ <*k*> = <*m9*> ^ r by A1, A21;
A36: w ^ <*k*> = <*m*> ^ (q ^ <*k*>) by A32, FINSEQ_1:32;
A37: w ^ <*n*> = <*m*> ^ (q ^ <*n*>) by A32, FINSEQ_1:32;
A38: (w ^ <*k*>) . 1 = m by A36, FINSEQ_1:41;
A39: (w ^ <*k*>) . 1 = m9 by A35, FINSEQ_1:41;
A40: <*m*> ^ (q ^ <*n*>) in NAT * by FINSEQ_1:def_11;
A41: r = q ^ <*k*> by A35, A36, A38, A39, FINSEQ_1:33;
p . (m + 1) in rng p by A33, A38, A39, Lm3;
then q ^ <*n*> in p . (m + 1) by A2, A22, A34, A38, A39, A41, TREES_1:def_3;
hence w ^ <*n*> in T by A1, A33, A37, A38, A39, A40; ::_thesis: verum
end;
hence w ^ <*n*> in T by A23; ::_thesis: verum
end;
then reconsider T = T as Tree ;
take T ; ::_thesis: for x being set holds
( x in T 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 ) ) )
let x be set ; ::_thesis: ( x in T 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 ) ) )
thus ( not x in T or x = {} or ex n being Element of NAT ex q being FinSequence st
( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) ) by A1; ::_thesis: ( ( x = {} or ex n being Element of NAT ex q being FinSequence st
( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) ) implies x in T )
assume A42: ( x = {} or ex n being Element of NAT ex q being FinSequence st
( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) ) ; ::_thesis: x in T
A43: now__::_thesis:_(_ex_n_being_Element_of_NAT_ex_q_being_FinSequence_st_
(_n_<_len_p_&_q_in_p_._(n_+_1)_&_x_=_<*n*>_^_q_)_implies_x_in_NAT_*_)
given n being Element of NAT , q being FinSequence such that A44: n < len p and
A45: q in p . (n + 1) and
A46: x = <*n*> ^ q ; ::_thesis: x in NAT *
reconsider T1 = p . (n + 1) as Tree by A3, A44;
reconsider q = q as Element of T1 by A45;
<*n*> ^ q in NAT * by FINSEQ_1:def_11;
hence x in NAT * by A46; ::_thesis: verum
end;
{} in NAT * by FINSEQ_1:49;
hence x in T by A1, A42, A43; ::_thesis: verum
end;
uniqueness
for b1, b2 being Tree st ( for x being set holds
( x in b1 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 b2 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
b1 = b2
proof
defpred S1[ set ] means ( $1 = {} or ex n being Element of NAT ex q being FinSequence st
( n < len p & q in p . (n + 1) & $1 = <*n*> ^ q ) );
let T1, T2 be Tree; ::_thesis: ( ( for x being set holds
( x in T1 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 T2 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 ) ) ) ) implies T1 = T2 )
assume that
A47: for x being set holds
( x in T1 iff S1[x] ) and
A48: for x being set holds
( x in T2 iff S1[x] ) ; ::_thesis: T1 = T2
thus T1 = T2 from XBOOLE_0:sch_2(A47, A48); ::_thesis: verum
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 Element of NAT ex q being FinSequence st
( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) ) ) );
definition
let T be Tree;
func ^ T -> Tree equals :: TREES_3:def 16
tree <*T*>;
correctness
coherence
tree <*T*> is Tree;
;
end;
:: deftheorem defines ^ TREES_3:def_16_:_
for T being Tree holds ^ T = tree <*T*>;
definition
let T1, T2 be Tree;
func tree (T1,T2) -> Tree equals :: TREES_3:def 17
tree <*T1,T2*>;
correctness
coherence
tree <*T1,T2*> is Tree;
;
end;
:: deftheorem defines tree TREES_3:def_17_:_
for T1, T2 being Tree holds tree (T1,T2) = tree <*T1,T2*>;
theorem :: TREES_3: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) ) )
proof
let n be Element of NAT ; ::_thesis: 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) ) )
let p, q be FinSequence; ::_thesis: ( p is Tree-yielding implies ( <*n*> ^ q in tree p iff ( n < len p & q in p . (n + 1) ) ) )
assume A1: p is Tree-yielding ; ::_thesis: ( <*n*> ^ q in tree p iff ( n < len p & q in p . (n + 1) ) )
thus ( <*n*> ^ q in tree p implies ( n < len p & q in p . (n + 1) ) ) ::_thesis: ( n < len p & q in p . (n + 1) implies <*n*> ^ q in tree p )
proof
assume <*n*> ^ q in tree p ; ::_thesis: ( n < len p & q in p . (n + 1) )
then consider k being Element of NAT , r being FinSequence such that
A2: k < len p and
A3: r in p . (k + 1) and
A4: <*n*> ^ q = <*k*> ^ r by A1, Def15;
A5: (<*n*> ^ q) . 1 = n by FINSEQ_1:41;
(<*k*> ^ r) . 1 = k by FINSEQ_1:41;
hence ( n < len p & q in p . (n + 1) ) by A2, A3, A4, A5, FINSEQ_1:33; ::_thesis: verum
end;
thus ( n < len p & q in p . (n + 1) implies <*n*> ^ q in tree p ) by A1, Def15; ::_thesis: verum
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) ) )
proof
let p be FinSequence; ::_thesis: ( p is Tree-yielding implies ( (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) ) ) )
set T = tree p;
assume A1: p is Tree-yielding ; ::_thesis: ( (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) ) )
then A2: rng p is constituted-Trees by Def9;
thus (tree p) -level 1 = { <*n*> where n is Element of NAT : n < len p } ::_thesis: for n being Element of NAT st n < len p holds
(tree p) | <*n*> = p . (n + 1)
proof
thus (tree p) -level 1 c= { <*n*> where n is Element of NAT : n < len p } :: according to XBOOLE_0:def_10 ::_thesis: { <*n*> where n is Element of NAT : n < len p } c= (tree p) -level 1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (tree p) -level 1 or x in { <*n*> where n is Element of NAT : n < len p } )
assume x in (tree p) -level 1 ; ::_thesis: x in { <*n*> where n is Element of NAT : n < len p }
then consider t being Element of tree p such that
A3: x = t and
A4: len t = 1 ;
A5: t = <*(t . 1)*> by A4, FINSEQ_1:40;
then consider n being Element of NAT , q being FinSequence such that
A6: n < len p and
q in p . (n + 1) and
A7: t = <*n*> ^ q by A1, Def15;
t = <*n*> by A5, A7, FINSEQ_1:88;
hence x in { <*n*> where n is Element of NAT : n < len p } by A3, A6; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { <*n*> where n is Element of NAT : n < len p } or x in (tree p) -level 1 )
assume x in { <*n*> where n is Element of NAT : n < len p } ; ::_thesis: x in (tree p) -level 1
then consider n being Element of NAT such that
A8: x = <*n*> and
A9: n < len p ;
p . (n + 1) in rng p by A9, Lm3;
then A10: {} in p . (n + 1) by A2, TREES_1:22;
<*n*> ^ {} = <*n*> by FINSEQ_1:34;
then reconsider t = <*n*> as Element of tree p by A1, A9, A10, Def15;
len t = 1 by FINSEQ_1:39;
hence x in (tree p) -level 1 by A8; ::_thesis: verum
end;
let n be Element of NAT ; ::_thesis: ( n < len p implies (tree p) | <*n*> = p . (n + 1) )
assume A11: n < len p ; ::_thesis: (tree p) | <*n*> = p . (n + 1)
then p . (n + 1) in rng p by Lm3;
then reconsider S = p . (n + 1) as Tree by A2;
A12: {} in S by TREES_1:22;
<*n*> ^ {} = <*n*> by FINSEQ_1:34;
then A13: <*n*> in tree p by A1, A11, A12, Def15;
(tree p) | <*n*> = S
proof
let r be FinSequence of NAT ; :: according to TREES_2:def_1 ::_thesis: ( ( not r in (tree p) | <*n*> or r in S ) & ( not r in S or r in (tree p) | <*n*> ) )
thus ( r in (tree p) | <*n*> implies r in S ) ::_thesis: ( not r in S or r in (tree p) | <*n*> )
proof
assume r in (tree p) | <*n*> ; ::_thesis: r in S
then <*n*> ^ r in tree p by A13, TREES_1:def_6;
then consider m being Element of NAT , q being FinSequence such that
m < len p and
A14: q in p . (m + 1) and
A15: <*n*> ^ r = <*m*> ^ q by A1, Def15;
A16: (<*n*> ^ r) . 1 = n by FINSEQ_1:41;
(<*m*> ^ q) . 1 = m by FINSEQ_1:41;
hence r in S by A14, A15, A16, FINSEQ_1:33; ::_thesis: verum
end;
assume r in S ; ::_thesis: r in (tree p) | <*n*>
then A17: <*n*> ^ r in tree p by A1, A11, Def15;
then <*n*> in tree p by TREES_1:21;
hence r in (tree p) | <*n*> by A17, TREES_1:def_6; ::_thesis: verum
end;
hence (tree p) | <*n*> = p . (n + 1) ; ::_thesis: verum
end;
theorem :: TREES_3:50
for p, q being Tree-yielding FinSequence st tree p = tree q holds
p = q
proof
let p, q be Tree-yielding FinSequence; ::_thesis: ( tree p = tree q implies p = q )
assume A1: tree p = tree q ; ::_thesis: p = q
A2: (tree p) -level 1 = { <*n*> where n is Element of NAT : n < len p } by Th49;
A3: (tree q) -level 1 = { <*k*> where k is Element of NAT : k < len q } by Th49;
A4: now__::_thesis:_for_n1,_n2_being_Element_of_NAT_st__{__<*i*>_where_i_is_Element_of_NAT_:_i_<_n1__}__=__{__<*k*>_where_k_is_Element_of_NAT_:_k_<_n2__}__holds_
not_n1_<_n2
let n1, n2 be Element of NAT ; ::_thesis: ( { <*i*> where i is Element of NAT : i < n1 } = { <*k*> where k is Element of NAT : k < n2 } implies not n1 < n2 )
assume ( { <*i*> where i is Element of NAT : i < n1 } = { <*k*> where k is Element of NAT : k < n2 } & n1 < n2 ) ; ::_thesis: contradiction
then <*n1*> in { <*i*> where i is Element of NAT : i < n1 } ;
then A5: ex i being Element of NAT st
( <*n1*> = <*i*> & i < n1 ) ;
<*n1*> . 1 = n1 by FINSEQ_1:40;
hence contradiction by A5, FINSEQ_1:40; ::_thesis: verum
end;
then A6: not len p < len q by A1, A2, A3;
A7: not len p > len q by A1, A2, A3, A4;
then A8: len p = len q by A6, XXREAL_0:1;
now__::_thesis:_for_i_being_Nat_st_i_>=_1_&_i_<=_len_p_holds_
p_._i_=_q_._i
let i be Nat; ::_thesis: ( i >= 1 & i <= len p implies p . i = q . i )
assume that
A9: i >= 1 and
A10: i <= len p ; ::_thesis: p . i = q . i
consider k being Nat such that
A11: i = 1 + k by A9, NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
A12: k < len p by A10, A11, NAT_1:13;
then p . i = (tree p) | <*k*> by A11, Th49;
hence p . i = q . i by A1, A8, A11, A12, Th49; ::_thesis: verum
end;
hence p = q by A6, A7, FINSEQ_1:14, XXREAL_0:1; ::_thesis: verum
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) )
proof
let p be FinSequence; ::_thesis: for p1, p2 being Tree-yielding FinSequence
for T being Tree holds
( p in T iff <*(len p1)*> ^ p in tree ((p1 ^ <*T*>) ^ p2) )
let p1, p2 be Tree-yielding FinSequence; ::_thesis: for T being Tree holds
( p in T iff <*(len p1)*> ^ p in tree ((p1 ^ <*T*>) ^ p2) )
let T be Tree; ::_thesis: ( p in T iff <*(len p1)*> ^ p in tree ((p1 ^ <*T*>) ^ p2) )
A1: len ((p1 ^ <*T*>) ^ p2) = (len (p1 ^ <*T*>)) + (len p2) by FINSEQ_1:22;
A2: len (p1 ^ <*T*>) = (len p1) + (len <*T*>) by FINSEQ_1:22;
A3: len <*T*> = 1 by FINSEQ_1:40;
A4: ((len p1) + 1) + (len p2) = ((len p1) + (len p2)) + 1 ;
len p1 <= (len p1) + (len p2) by NAT_1:11;
then A5: len p1 < len ((p1 ^ <*T*>) ^ p2) by A1, A2, A3, A4, NAT_1:13;
(len p1) + 1 >= 1 by NAT_1:11;
then (len p1) + 1 in dom (p1 ^ <*T*>) by A2, A3, FINSEQ_3:25;
then A6: ((p1 ^ <*T*>) ^ p2) . ((len p1) + 1) = (p1 ^ <*T*>) . ((len p1) + 1) by FINSEQ_1:def_7
.= T by FINSEQ_1:42 ;
hence ( p in T implies <*(len p1)*> ^ p in tree ((p1 ^ <*T*>) ^ p2) ) by A5, Def15; ::_thesis: ( <*(len p1)*> ^ p in tree ((p1 ^ <*T*>) ^ p2) implies p in T )
assume <*(len p1)*> ^ p in tree ((p1 ^ <*T*>) ^ p2) ; ::_thesis: p in T
then consider n being Element of NAT , q being FinSequence such that
n < len ((p1 ^ <*T*>) ^ p2) and
A7: q in ((p1 ^ <*T*>) ^ p2) . (n + 1) and
A8: <*(len p1)*> ^ p = <*n*> ^ q by Def15;
A9: (<*(len p1)*> ^ p) . 1 = len p1 by FINSEQ_1:41;
(<*n*> ^ q) . 1 = n by FINSEQ_1:41;
hence p in T by A6, A7, A8, A9, FINSEQ_1:33; ::_thesis: verum
end;
theorem Th52: :: TREES_3:52
tree {} = elementary_tree 0
proof
let p be FinSequence of NAT ; :: according to TREES_2:def_1 ::_thesis: ( ( not p in tree {} or p in elementary_tree 0 ) & ( not p in elementary_tree 0 or p in tree {} ) )
thus ( p in tree {} implies p in elementary_tree 0 ) ::_thesis: ( not p in elementary_tree 0 or p in tree {} )
proof
assume p in tree {} ; ::_thesis: p in elementary_tree 0
then A1: ( p = {} or ex n being Element of NAT ex q being FinSequence st
( n < len {} & q in {} . (n + 1) & p = <*n*> ^ q ) ) by Def15;
assume not p in elementary_tree 0 ; ::_thesis: contradiction
hence contradiction by A1, TARSKI:def_1, TREES_1:29; ::_thesis: verum
end;
assume p in elementary_tree 0 ; ::_thesis: p in tree {}
then p = {} by TARSKI:def_1, TREES_1:29;
hence p in tree {} by Def15; ::_thesis: verum
end;
theorem Th53: :: TREES_3:53
for p being FinSequence st p is Tree-yielding holds
elementary_tree (len p) c= tree p
proof
let p be FinSequence; ::_thesis: ( p is Tree-yielding implies elementary_tree (len p) c= tree p )
assume A1: p is Tree-yielding ; ::_thesis: elementary_tree (len p) c= tree p
then A2: rng p is constituted-Trees by Def9;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in elementary_tree (len p) or q in tree p )
assume q in elementary_tree (len p) ; ::_thesis: q in tree p
then ( q in { <*n*> where n is Element of NAT : n < len p } or q in {{}} ) by XBOOLE_0:def_3;
then A3: ( ex n being Element of NAT st
( q = <*n*> & n < len p ) or q = {} ) by TARSKI:def_1;
assume A4: not q in tree p ; ::_thesis: contradiction
then consider n being Element of NAT such that
A5: q = <*n*> and
A6: n < len p by A3, TREES_1:22;
p . (n + 1) in rng p by A6, Lm3;
then reconsider t = p . (n + 1) as Tree by A2;
A7: {} in t by TREES_1:22;
<*n*> ^ {} = q by A5, FINSEQ_1:34;
hence contradiction by A1, A4, A6, A7, Def15; ::_thesis: verum
end;
theorem Th54: :: TREES_3:54
for i being Element of NAT holds elementary_tree i = tree (i |-> (elementary_tree 0))
proof
let i be Element of NAT ; ::_thesis: elementary_tree i = tree (i |-> (elementary_tree 0))
set p = i |-> (elementary_tree 0);
let q be FinSequence of NAT ; :: according to TREES_2:def_1 ::_thesis: ( ( not q in elementary_tree i or q in tree (i |-> (elementary_tree 0)) ) & ( not q in tree (i |-> (elementary_tree 0)) or q in elementary_tree i ) )
A1: len (i |-> (elementary_tree 0)) = i by CARD_1:def_7;
then elementary_tree i c= tree (i |-> (elementary_tree 0)) by Th53;
hence ( q in elementary_tree i implies q in tree (i |-> (elementary_tree 0)) ) ; ::_thesis: ( not q in tree (i |-> (elementary_tree 0)) or q in elementary_tree i )
assume q in tree (i |-> (elementary_tree 0)) ; ::_thesis: q in elementary_tree i
then A2: ( q = {} or ex n being Element of NAT ex r being FinSequence st
( n < len (i |-> (elementary_tree 0)) & r in (i |-> (elementary_tree 0)) . (n + 1) & q = <*n*> ^ r ) ) by Def15;
now__::_thesis:_(_ex_n_being_Element_of_NAT_ex_r_being_FinSequence_st_
(_n_<_len_(i_|->_(elementary_tree_0))_&_r_in_(i_|->_(elementary_tree_0))_._(n_+_1)_&_q_=_<*n*>_^_r_)_implies_q_in_elementary_tree_i_)
given n being Element of NAT , r being FinSequence such that A3: n < len (i |-> (elementary_tree 0)) and
A4: r in (i |-> (elementary_tree 0)) . (n + 1) and
A5: q = <*n*> ^ r ; ::_thesis: q in elementary_tree i
i |-> (elementary_tree 0) = (Seg i) --> (elementary_tree 0) by FINSEQ_2:def_2;
then A6: rng (i |-> (elementary_tree 0)) c= {(elementary_tree 0)} by FUNCOP_1:13;
(i |-> (elementary_tree 0)) . (n + 1) in rng (i |-> (elementary_tree 0)) by A3, Lm3;
then (i |-> (elementary_tree 0)) . (n + 1) = elementary_tree 0 by A6, TARSKI:def_1;
then r = {} by A4, TARSKI:def_1, TREES_1:29;
then q = <*n*> by A5, FINSEQ_1:34;
hence q in elementary_tree i by A1, A3, TREES_1:28; ::_thesis: verum
end;
hence q in elementary_tree i by A2, TREES_1:22; ::_thesis: verum
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)
proof
let T be Tree; ::_thesis: for p being Tree-yielding FinSequence holds tree (p ^ <*T*>) = ((tree p) \/ (elementary_tree ((len p) + 1))) with-replacement (<*(len p)*>,T)
let p be Tree-yielding FinSequence; ::_thesis: tree (p ^ <*T*>) = ((tree p) \/ (elementary_tree ((len p) + 1))) with-replacement (<*(len p)*>,T)
set W1 = elementary_tree ((len p) + 1);
set W2 = (tree p) \/ (elementary_tree ((len p) + 1));
set W = ((tree p) \/ (elementary_tree ((len p) + 1))) with-replacement (<*(len p)*>,T);
len <*T*> = 1 by FINSEQ_1:40;
then A1: len (p ^ <*T*>) = (len p) + 1 by FINSEQ_1:22;
len p < (len p) + 1 by NAT_1:13;
then <*(len p)*> in elementary_tree ((len p) + 1) by TREES_1:28;
then A2: <*(len p)*> in (tree p) \/ (elementary_tree ((len p) + 1)) by XBOOLE_0:def_3;
let q be FinSequence of NAT ; :: according to TREES_2:def_1 ::_thesis: ( ( not q in tree (p ^ <*T*>) or q in ((tree p) \/ (elementary_tree ((len p) + 1))) with-replacement (<*(len p)*>,T) ) & ( not q in ((tree p) \/ (elementary_tree ((len p) + 1))) with-replacement (<*(len p)*>,T) or q in tree (p ^ <*T*>) ) )
thus ( q in tree (p ^ <*T*>) implies q in ((tree p) \/ (elementary_tree ((len p) + 1))) with-replacement (<*(len p)*>,T) ) ::_thesis: ( not q in ((tree p) \/ (elementary_tree ((len p) + 1))) with-replacement (<*(len p)*>,T) or q in tree (p ^ <*T*>) )
proof
assume q in tree (p ^ <*T*>) ; ::_thesis: q in ((tree p) \/ (elementary_tree ((len p) + 1))) with-replacement (<*(len p)*>,T)
then A3: ( q = {} or ex n being Element of NAT ex r being FinSequence st
( n < len (p ^ <*T*>) & r in (p ^ <*T*>) . (n + 1) & q = <*n*> ^ r ) ) by Def15;
now__::_thesis:_(_ex_n_being_Element_of_NAT_ex_r_being_FinSequence_st_
(_n_<_len_(p_^_<*T*>)_&_r_in_(p_^_<*T*>)_._(n_+_1)_&_q_=_<*n*>_^_r_)_implies_q_in_((tree_p)_\/_(elementary_tree_((len_p)_+_1)))_with-replacement_(<*(len_p)*>,T)_)
given n being Element of NAT , r being FinSequence such that A4: n < len (p ^ <*T*>) and
A5: r in (p ^ <*T*>) . (n + 1) and
A6: q = <*n*> ^ r ; ::_thesis: q in ((tree p) \/ (elementary_tree ((len p) + 1))) with-replacement (<*(len p)*>,T)
reconsider r = r as FinSequence of NAT by A6, FINSEQ_1:36;
A7: n <= len p by A1, A4, NAT_1:13;
A8: now__::_thesis:_(_n_<_len_p_implies_q_in_((tree_p)_\/_(elementary_tree_((len_p)_+_1)))_with-replacement_(<*(len_p)*>,T)_)
assume A9: n < len p ; ::_thesis: q in ((tree p) \/ (elementary_tree ((len p) + 1))) with-replacement (<*(len p)*>,T)
then n + 1 in dom p by Lm3;
then (p ^ <*T*>) . (n + 1) = p . (n + 1) by FINSEQ_1:def_7;
then q in tree p by A5, A6, A9, Def15;
then A10: q in (tree p) \/ (elementary_tree ((len p) + 1)) by XBOOLE_0:def_3;
not <*(len p)*> is_a_prefix_of <*n*> ^ r by A9, TREES_1:50;
then not <*(len p)*> is_a_proper_prefix_of <*n*> ^ r by XBOOLE_0:def_8;
hence q in ((tree p) \/ (elementary_tree ((len p) + 1))) with-replacement (<*(len p)*>,T) by A2, A6, A10, TREES_1:def_9; ::_thesis: verum
end;
now__::_thesis:_(_n_=_len_p_implies_q_in_((tree_p)_\/_(elementary_tree_((len_p)_+_1)))_with-replacement_(<*(len_p)*>,T)_)
assume A11: n = len p ; ::_thesis: q in ((tree p) \/ (elementary_tree ((len p) + 1))) with-replacement (<*(len p)*>,T)
then A12: (p ^ <*T*>) . (n + 1) = T by FINSEQ_1:42;
r = r ;
hence q in ((tree p) \/ (elementary_tree ((len p) + 1))) with-replacement (<*(len p)*>,T) by A2, A5, A6, A11, A12, TREES_1:def_9; ::_thesis: verum
end;
hence q in ((tree p) \/ (elementary_tree ((len p) + 1))) with-replacement (<*(len p)*>,T) by A7, A8, XXREAL_0:1; ::_thesis: verum
end;
hence q in ((tree p) \/ (elementary_tree ((len p) + 1))) with-replacement (<*(len p)*>,T) by A3, TREES_1:22; ::_thesis: verum
end;
assume A13: q in ((tree p) \/ (elementary_tree ((len p) + 1))) with-replacement (<*(len p)*>,T) ; ::_thesis: q in tree (p ^ <*T*>)
assume A14: not q in tree (p ^ <*T*>) ; ::_thesis: contradiction
A15: now__::_thesis:_for_r_being_FinSequence_of_NAT_holds_
(_not_r_in_T_or_not_q_=_<*(len_p)*>_^_r_)
given r being FinSequence of NAT such that A16: r in T and
A17: q = <*(len p)*> ^ r ; ::_thesis: contradiction
A18: len p < (len p) + 1 by NAT_1:13;
(p ^ <*T*>) . ((len p) + 1) = T by FINSEQ_1:42;
hence contradiction by A1, A14, A16, A17, A18, Def15; ::_thesis: verum
end;
now__::_thesis:_not_q_in_(tree_p)_\/_(elementary_tree_((len_p)_+_1))
assume q in (tree p) \/ (elementary_tree ((len p) + 1)) ; ::_thesis: contradiction
then A19: ( q in tree p or q in elementary_tree ((len p) + 1) ) by XBOOLE_0:def_3;
A20: now__::_thesis:_not_q_in_tree_p
assume q in tree p ; ::_thesis: contradiction
then ( ( q = {} & {} in tree (p ^ <*T*>) ) or ex n being Element of NAT ex r being FinSequence st
( n < len p & r in p . (n + 1) & q = <*n*> ^ r ) ) by Def15;
then consider n being Element of NAT , r being FinSequence such that
A21: n < len p and
A22: r in p . (n + 1) and
A23: q = <*n*> ^ r by A14;
n + 1 in dom p by A21, Lm3;
then A24: p . (n + 1) = (p ^ <*T*>) . (n + 1) by FINSEQ_1:def_7;
n < len (p ^ <*T*>) by A1, A21, NAT_1:13;
hence contradiction by A14, A22, A23, A24, Def15; ::_thesis: verum
end;
now__::_thesis:_q_in_tree_p
assume A25: not q in tree p ; ::_thesis: contradiction
then ( q = {} or ex n being Element of NAT st
( n < (len p) + 1 & q = <*n*> ) ) by A19, TREES_1:30;
then consider n being Element of NAT such that
A26: n < (len p) + 1 and
A27: q = <*n*> by A14, TREES_1:22;
A28: now__::_thesis:_(_n_<_len_p_implies_{}_in_p_._(n_+_1)_)
assume n < len p ; ::_thesis: {} in p . (n + 1)
then A29: p . (n + 1) in rng p by Lm3;
rng p is constituted-Trees by Def9;
hence {} in p . (n + 1) by A29, TREES_1:22; ::_thesis: verum
end;
A30: q = <*n*> ^ {} by A27, FINSEQ_1:34;
then A31: n >= len p by A25, A28, Def15;
n <= len p by A26, NAT_1:13;
then A32: len p = n by A31, XXREAL_0:1;
A33: n < n + 1 by NAT_1:13;
A34: (p ^ <*T*>) . ((len p) + 1) = T by FINSEQ_1:42;
{} in T by TREES_1:22;
hence contradiction by A1, A14, A30, A32, A33, A34, Def15; ::_thesis: verum
end;
hence contradiction by A20; ::_thesis: verum
end;
hence contradiction by A2, A13, A15, TREES_1:def_9; ::_thesis: verum
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
let p be Tree-yielding FinSequence; ::_thesis: tree (p ^ <*(elementary_tree 0)*>) = (tree p) \/ (elementary_tree ((len p) + 1))
len p < (len p) + 1 by NAT_1:13;
then A1: <*(len p)*> in elementary_tree ((len p) + 1) by TREES_1:28;
then A2: <*(len p)*> in (tree p) \/ (elementary_tree ((len p) + 1)) by XBOOLE_0:def_3;
{} in (elementary_tree ((len p) + 1)) | <*(len p)*> by TREES_1:22;
then A3: elementary_tree 0 c= (elementary_tree ((len p) + 1)) | <*(len p)*> by TREES_1:29, ZFMISC_1:31;
A4: (elementary_tree ((len p) + 1)) | <*(len p)*> c= elementary_tree 0
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (elementary_tree ((len p) + 1)) | <*(len p)*> or x in elementary_tree 0 )
assume x in (elementary_tree ((len p) + 1)) | <*(len p)*> ; ::_thesis: x in elementary_tree 0
then reconsider q = x as Element of (elementary_tree ((len p) + 1)) | <*(len p)*> ;
<*(len p)*> ^ q in elementary_tree ((len p) + 1) by A1, TREES_1:def_6;
then consider n being Element of NAT such that
n < (len p) + 1 and
A5: <*(len p)*> ^ q = <*n*> by TREES_1:30;
A6: len <*n*> = 1 by FINSEQ_1:40;
len <*(len p)*> = 1 by FINSEQ_1:40;
then 1 + (len q) = 1 + 0 by A5, A6, FINSEQ_1:22;
then x = {} ;
hence x in elementary_tree 0 by TREES_1:22; ::_thesis: verum
end;
now__::_thesis:_for_n_being_Element_of_NAT_
for_r_being_FinSequence_st_<*(len_p)*>_=_<*n*>_^_r_holds_
not_n_<_len_p
let n be Element of NAT ; ::_thesis: for r being FinSequence st <*(len p)*> = <*n*> ^ r holds
not n < len p
let r be FinSequence; ::_thesis: ( <*(len p)*> = <*n*> ^ r implies not n < len p )
assume <*(len p)*> = <*n*> ^ r ; ::_thesis: not n < len p
then n = <*(len p)*> . 1 by FINSEQ_1:41
.= len p by FINSEQ_1:40 ;
hence not n < len p ; ::_thesis: verum
end;
then for n being Element of NAT
for q being FinSequence holds
( not n < len p or not q in p . (n + 1) or not <*(len p)*> = <*n*> ^ q ) ;
then not <*(len p)*> in tree p by Def15;
then A7: ((tree p) \/ (elementary_tree ((len p) + 1))) | <*(len p)*> = (elementary_tree ((len p) + 1)) | <*(len p)*> by A2, Th47
.= elementary_tree 0 by A3, A4, XBOOLE_0:def_10 ;
thus tree (p ^ <*(elementary_tree 0)*>) = ((tree p) \/ (elementary_tree ((len p) + 1))) with-replacement (<*(len p)*>,(elementary_tree 0)) by Th55
.= (tree p) \/ (elementary_tree ((len p) + 1)) by A2, A7, TREES_2:6 ; ::_thesis: verum
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)
proof
let p, q be Tree-yielding FinSequence; ::_thesis: for T1, T2 being Tree holds tree ((p ^ <*T1*>) ^ q) = (tree ((p ^ <*T2*>) ^ q)) with-replacement (<*(len p)*>,T1)
let T1, T2 be Tree; ::_thesis: tree ((p ^ <*T1*>) ^ q) = (tree ((p ^ <*T2*>) ^ q)) with-replacement (<*(len p)*>,T1)
set w1 = (p ^ <*T1*>) ^ q;
set W1 = tree ((p ^ <*T1*>) ^ q);
set w2 = (p ^ <*T2*>) ^ q;
set W2 = tree ((p ^ <*T2*>) ^ q);
set W = (tree ((p ^ <*T2*>) ^ q)) with-replacement (<*(len p)*>,T1);
A1: len <*T1*> = 1 by FINSEQ_1:40;
A2: len <*T2*> = 1 by FINSEQ_1:40;
A3: len (p ^ <*T1*>) = (len p) + 1 by A1, FINSEQ_1:22;
A4: len ((p ^ <*T1*>) ^ q) = (len (p ^ <*T1*>)) + (len q) by FINSEQ_1:22;
A5: len (p ^ <*T2*>) = (len p) + 1 by A2, FINSEQ_1:22;
A6: len ((p ^ <*T2*>) ^ q) = (len (p ^ <*T2*>)) + (len q) by FINSEQ_1:22;
(len p) + 1 <= ((len p) + 1) + (len q) by NAT_1:11;
then A7: len p < ((len p) + 1) + (len q) by NAT_1:13;
then A8: ((p ^ <*T2*>) ^ q) . ((len p) + 1) in rng ((p ^ <*T2*>) ^ q) by A5, A6, Lm3;
rng ((p ^ <*T2*>) ^ q) is constituted-Trees by Def9;
then A9: {} in ((p ^ <*T2*>) ^ q) . ((len p) + 1) by A8, TREES_1:22;
<*(len p)*> ^ {} = <*(len p)*> by FINSEQ_1:34;
then A10: <*(len p)*> in tree ((p ^ <*T2*>) ^ q) by A5, A6, A7, A9, Def15;
let r be FinSequence of NAT ; :: according to TREES_2:def_1 ::_thesis: ( ( not r in tree ((p ^ <*T1*>) ^ q) or r in (tree ((p ^ <*T2*>) ^ q)) with-replacement (<*(len p)*>,T1) ) & ( not r in (tree ((p ^ <*T2*>) ^ q)) with-replacement (<*(len p)*>,T1) or r in tree ((p ^ <*T1*>) ^ q) ) )
thus ( r in tree ((p ^ <*T1*>) ^ q) implies r in (tree ((p ^ <*T2*>) ^ q)) with-replacement (<*(len p)*>,T1) ) ::_thesis: ( not r in (tree ((p ^ <*T2*>) ^ q)) with-replacement (<*(len p)*>,T1) or r in tree ((p ^ <*T1*>) ^ q) )
proof
assume r in tree ((p ^ <*T1*>) ^ q) ; ::_thesis: r in (tree ((p ^ <*T2*>) ^ q)) with-replacement (<*(len p)*>,T1)
then A11: ( r = {} or ex n being Element of NAT ex s being FinSequence st
( n < len ((p ^ <*T1*>) ^ q) & s in ((p ^ <*T1*>) ^ q) . (n + 1) & r = <*n*> ^ s ) ) by Def15;
now__::_thesis:_(_ex_n_being_Element_of_NAT_ex_s_being_FinSequence_st_
(_n_<_len_((p_^_<*T1*>)_^_q)_&_s_in_((p_^_<*T1*>)_^_q)_._(n_+_1)_&_r_=_<*n*>_^_s_)_implies_r_in_(tree_((p_^_<*T2*>)_^_q))_with-replacement_(<*(len_p)*>,T1)_)
given n being Element of NAT , s being FinSequence such that A12: n < len ((p ^ <*T1*>) ^ q) and
A13: s in ((p ^ <*T1*>) ^ q) . (n + 1) and
A14: r = <*n*> ^ s ; ::_thesis: r in (tree ((p ^ <*T2*>) ^ q)) with-replacement (<*(len p)*>,T1)
reconsider s = s as FinSequence of NAT by A14, FINSEQ_1:36;
A15: ( n <= len p or n >= (len p) + 1 ) by NAT_1:13;
A16: now__::_thesis:_(_n_<_len_p_implies_r_in_(tree_((p_^_<*T2*>)_^_q))_with-replacement_(<*(len_p)*>,T1)_)
assume A17: n < len p ; ::_thesis: r in (tree ((p ^ <*T2*>) ^ q)) with-replacement (<*(len p)*>,T1)
then A18: n + 1 in dom p by Lm3;
A19: dom p c= dom (p ^ <*T2*>) by FINSEQ_1:26;
A20: dom p c= dom (p ^ <*T1*>) by FINSEQ_1:26;
A21: (p ^ <*T2*>) . (n + 1) = p . (n + 1) by A18, FINSEQ_1:def_7;
A22: (p ^ <*T1*>) . (n + 1) = p . (n + 1) by A18, FINSEQ_1:def_7;
A23: ((p ^ <*T2*>) ^ q) . (n + 1) = p . (n + 1) by A18, A19, A21, FINSEQ_1:def_7;
((p ^ <*T1*>) ^ q) . (n + 1) = p . (n + 1) by A18, A20, A22, FINSEQ_1:def_7;
then A24: r in tree ((p ^ <*T2*>) ^ q) by A3, A4, A5, A6, A12, A13, A14, A23, Def15;
not <*(len p)*> is_a_prefix_of <*n*> ^ s by A17, TREES_1:50;
then not <*(len p)*> is_a_proper_prefix_of <*n*> ^ s by XBOOLE_0:def_8;
hence r in (tree ((p ^ <*T2*>) ^ q)) with-replacement (<*(len p)*>,T1) by A10, A14, A24, TREES_1:def_9; ::_thesis: verum
end;
A25: now__::_thesis:_(_n_=_len_p_implies_r_in_(tree_((p_^_<*T2*>)_^_q))_with-replacement_(<*(len_p)*>,T1)_)
assume A26: n = len p ; ::_thesis: r in (tree ((p ^ <*T2*>) ^ q)) with-replacement (<*(len p)*>,T1)
then A27: (p ^ <*T1*>) . (n + 1) = T1 by FINSEQ_1:42;
n < (len p) + 1 by A26, NAT_1:13;
then n + 1 in dom (p ^ <*T1*>) by A3, Lm3;
then A28: ((p ^ <*T1*>) ^ q) . (n + 1) = T1 by A27, FINSEQ_1:def_7;
s = s ;
hence r in (tree ((p ^ <*T2*>) ^ q)) with-replacement (<*(len p)*>,T1) by A10, A13, A14, A26, A28, TREES_1:def_9; ::_thesis: verum
end;
now__::_thesis:_(_n_>=_(len_p)_+_1_&_n_<_((len_p)_+_1)_+_(len_q)_implies_r_in_(tree_((p_^_<*T2*>)_^_q))_with-replacement_(<*(len_p)*>,T1)_)
assume that
A29: n >= (len p) + 1 and
A30: n < ((len p) + 1) + (len q) ; ::_thesis: r in (tree ((p ^ <*T2*>) ^ q)) with-replacement (<*(len p)*>,T1)
A31: n + 1 >= ((len p) + 1) + 1 by A29, XREAL_1:7;
A32: n + 1 <= ((len p) + 1) + (len q) by A30, NAT_1:13;
then A33: ((p ^ <*T1*>) ^ q) . (n + 1) = q . ((n + 1) - ((len p) + 1)) by A3, A31, FINSEQ_1:23;
((p ^ <*T2*>) ^ q) . (n + 1) = q . ((n + 1) - ((len p) + 1)) by A5, A31, A32, FINSEQ_1:23;
then A34: r in tree ((p ^ <*T2*>) ^ q) by A3, A4, A5, A6, A12, A13, A14, A33, Def15;
len p <> n by A29, NAT_1:13;
then not <*(len p)*> is_a_prefix_of <*n*> ^ s by TREES_1:50;
then not <*(len p)*> is_a_proper_prefix_of <*n*> ^ s by XBOOLE_0:def_8;
hence r in (tree ((p ^ <*T2*>) ^ q)) with-replacement (<*(len p)*>,T1) by A10, A14, A34, TREES_1:def_9; ::_thesis: verum
end;
hence r in (tree ((p ^ <*T2*>) ^ q)) with-replacement (<*(len p)*>,T1) by A3, A12, A15, A16, A25, FINSEQ_1:22, XXREAL_0:1; ::_thesis: verum
end;
hence r in (tree ((p ^ <*T2*>) ^ q)) with-replacement (<*(len p)*>,T1) by A11, TREES_1:22; ::_thesis: verum
end;
assume r in (tree ((p ^ <*T2*>) ^ q)) with-replacement (<*(len p)*>,T1) ; ::_thesis: r in tree ((p ^ <*T1*>) ^ q)
then A35: ( ( r in tree ((p ^ <*T2*>) ^ q) & not <*(len p)*> is_a_proper_prefix_of r ) or ex s being FinSequence of NAT st
( s in T1 & r = <*(len p)*> ^ s ) ) by A10, TREES_1:def_9;
assume A36: not r in tree ((p ^ <*T1*>) ^ q) ; ::_thesis: contradiction
then A37: r <> {} by Def15;
A38: (p ^ <*T1*>) . ((len p) + 1) = T1 by FINSEQ_1:42;
A39: len p < (len p) + 1 by NAT_1:13;
(len p) + 1 <= ((len p) + 1) + (len q) by NAT_1:11;
then A40: len p < len ((p ^ <*T2*>) ^ q) by A5, A6, NAT_1:13;
(len p) + 1 in dom (p ^ <*T1*>) by A3, A39, Lm3;
then A41: ((p ^ <*T1*>) ^ q) . ((len p) + 1) = T1 by A38, FINSEQ_1:def_7;
then consider n being Element of NAT , s being FinSequence such that
A42: n < len ((p ^ <*T2*>) ^ q) and
A43: s in ((p ^ <*T2*>) ^ q) . (n + 1) and
A44: r = <*n*> ^ s by A3, A4, A5, A6, A35, A36, A37, A40, Def15;
reconsider s = s as FinSequence of NAT by A44, FINSEQ_1:36;
A45: ( n = len p implies s = {} ) by A3, A4, A5, A6, A35, A36, A41, A42, A44, Def15, TREES_1:10;
{} in T1 by TREES_1:22;
then n <> len p by A3, A4, A5, A6, A36, A41, A42, A44, A45, Def15;
then ( n < len p or ( n > len p & 1 <= 1 ) ) by XXREAL_0:1;
then ( ( 1 <= 1 + n & 1 + n = n + 1 & n + 1 <= len p & (p ^ <*T1*>) ^ q = p ^ (<*T1*> ^ q) & (p ^ <*T2*>) ^ q = p ^ (<*T2*> ^ q) ) or ( (len p) + 1 < n + 1 & n + 1 <= len ((p ^ <*T1*>) ^ q) ) ) by A3, A4, A5, A6, A42, FINSEQ_1:32, NAT_1:11, NAT_1:13, XREAL_1:6;
then ( ( ((p ^ <*T1*>) ^ q) . (n + 1) = p . (n + 1) & ((p ^ <*T2*>) ^ q) . (n + 1) = p . (n + 1) ) or ( ((p ^ <*T1*>) ^ q) . (n + 1) = q . ((n + 1) - ((len p) + 1)) & ((p ^ <*T2*>) ^ q) . (n + 1) = q . ((n + 1) - ((len p) + 1)) ) ) by A3, A4, A5, A6, Lm1, FINSEQ_1:24;
hence contradiction by A3, A4, A5, A6, A36, A42, A43, A44, Def15; ::_thesis: verum
end;
theorem :: TREES_3:58
for T being Tree holds ^ T = (elementary_tree 1) with-replacement (<*0*>,T)
proof
let T be Tree; ::_thesis: ^ T = (elementary_tree 1) with-replacement (<*0*>,T)
let p be FinSequence of NAT ; :: according to TREES_2:def_1 ::_thesis: ( ( not p in ^ T or p in (elementary_tree 1) with-replacement (<*0*>,T) ) & ( not p in (elementary_tree 1) with-replacement (<*0*>,T) or p in ^ T ) )
A1: <*T*> . 1 = T by FINSEQ_1:40;
A2: len <*T*> = 1 by FINSEQ_1:40;
A3: 0 + 1 = 1 ;
A4: {} in T by TREES_1:22;
A5: <*0*> in elementary_tree 1 by TARSKI:def_2, TREES_1:51;
thus ( p in ^ T implies p in (elementary_tree 1) with-replacement (<*0*>,T) ) ::_thesis: ( not p in (elementary_tree 1) with-replacement (<*0*>,T) or p in ^ T )
proof
assume A6: p in ^ T ; ::_thesis: p in (elementary_tree 1) with-replacement (<*0*>,T)
now__::_thesis:_(_p_<>_{}_implies_p_in_(elementary_tree_1)_with-replacement_(<*0*>,T)_)
assume p <> {} ; ::_thesis: p in (elementary_tree 1) with-replacement (<*0*>,T)
then consider n being Element of NAT , q being FinSequence such that
A7: n < len <*T*> and
A8: q in <*T*> . (n + 1) and
A9: p = <*n*> ^ q by A6, Def15;
reconsider q = q as FinSequence of NAT by A9, FINSEQ_1:36;
A10: n = 0 by A2, A3, A7, NAT_1:13;
p = <*n*> ^ q by A9;
hence p in (elementary_tree 1) with-replacement (<*0*>,T) by A1, A5, A8, A10, TREES_1:def_9; ::_thesis: verum
end;
hence p in (elementary_tree 1) with-replacement (<*0*>,T) by TREES_1:22; ::_thesis: verum
end;
assume p in (elementary_tree 1) with-replacement (<*0*>,T) ; ::_thesis: p in ^ T
then A11: ( ( p in elementary_tree 1 & not <*0*> is_a_proper_prefix_of p ) or ex r being FinSequence of NAT st
( r in T & p = <*0*> ^ r ) ) by A5, TREES_1:def_9;
now__::_thesis:_(_p_in_elementary_tree_1_implies_p_in_^_T_)
assume p in elementary_tree 1 ; ::_thesis: p in ^ T
then ( p = {} or ( p = <*0*> & p ^ {} = p ) ) by FINSEQ_1:34, TARSKI:def_2, TREES_1:51;
hence p in ^ T by A1, A2, A3, A4, Def15; ::_thesis: verum
end;
hence p in ^ T by A1, A2, A3, A11, Def15; ::_thesis: verum
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
let T1, T2 be Tree; ::_thesis: tree (T1,T2) = ((elementary_tree 2) with-replacement (<*0*>,T1)) with-replacement (<*1*>,T2)
let p be FinSequence of NAT ; :: according to TREES_2:def_1 ::_thesis: ( ( not p in tree (T1,T2) or p in ((elementary_tree 2) with-replacement (<*0*>,T1)) with-replacement (<*1*>,T2) ) & ( not p in ((elementary_tree 2) with-replacement (<*0*>,T1)) with-replacement (<*1*>,T2) or p in tree (T1,T2) ) )
A1: <*T1,T2*> . 1 = T1 by FINSEQ_1:44;
A2: <*T1,T2*> . 2 = T2 by FINSEQ_1:44;
A3: len <*T1,T2*> = 2 by FINSEQ_1:44;
A4: 1 + 1 = 2 ;
A5: 0 + 1 = 1 ;
A6: {} in T1 by TREES_1:22;
A7: {} in T2 by TREES_1:22;
A8: <*0*> in elementary_tree 2 by ENUMSET1:def_1, TREES_1:53;
A9: <*1*> in elementary_tree 2 by ENUMSET1:def_1, TREES_1:53;
not <*0*> is_a_proper_prefix_of <*1*> by TREES_1:52;
then A10: <*1*> in (elementary_tree 2) with-replacement (<*0*>,T1) by A8, A9, TREES_1:def_9;
thus ( p in tree (T1,T2) implies p in ((elementary_tree 2) with-replacement (<*0*>,T1)) with-replacement (<*1*>,T2) ) ::_thesis: ( not p in ((elementary_tree 2) with-replacement (<*0*>,T1)) with-replacement (<*1*>,T2) or p in tree (T1,T2) )
proof
assume A11: p in tree (T1,T2) ; ::_thesis: p in ((elementary_tree 2) with-replacement (<*0*>,T1)) with-replacement (<*1*>,T2)
now__::_thesis:_(_p_<>_{}_implies_p_in_((elementary_tree_2)_with-replacement_(<*0*>,T1))_with-replacement_(<*1*>,T2)_)
assume p <> {} ; ::_thesis: p in ((elementary_tree 2) with-replacement (<*0*>,T1)) with-replacement (<*1*>,T2)
then consider n being Element of NAT , q being FinSequence such that
A12: n < len <*T1,T2*> and
A13: q in <*T1,T2*> . (n + 1) and
A14: p = <*n*> ^ q by A11, Def15;
reconsider q = q as FinSequence of NAT by A14, FINSEQ_1:36;
A15: not <*1*> is_a_prefix_of <*0*> ^ q by TREES_1:50;
A16: now__::_thesis:_(_n_=_0_implies_p_in_((elementary_tree_2)_with-replacement_(<*0*>,T1))_with-replacement_(<*1*>,T2)_)
assume A17: n = 0 ; ::_thesis: p in ((elementary_tree 2) with-replacement (<*0*>,T1)) with-replacement (<*1*>,T2)
then A18: not <*1*> is_a_proper_prefix_of <*n*> ^ q by A15, XBOOLE_0:def_8;
<*n*> ^ q in (elementary_tree 2) with-replacement (<*0*>,T1) by A1, A8, A13, A17, TREES_1:def_9;
hence p in ((elementary_tree 2) with-replacement (<*0*>,T1)) with-replacement (<*1*>,T2) by A10, A14, A18, TREES_1:def_9; ::_thesis: verum
end;
n <= 0 + 1 by A3, A4, A12, NAT_1:13;
then ( ( n = 1 & ( n = 1 implies <*n*> ^ q in ((elementary_tree 2) with-replacement (<*0*>,T1)) with-replacement (<*1*>,T2) ) ) or ( n >= 0 & n <= 0 ) ) by A2, A10, A13, NAT_1:8, TREES_1:def_9;
hence p in ((elementary_tree 2) with-replacement (<*0*>,T1)) with-replacement (<*1*>,T2) by A14, A16; ::_thesis: verum
end;
hence p in ((elementary_tree 2) with-replacement (<*0*>,T1)) with-replacement (<*1*>,T2) by TREES_1:22; ::_thesis: verum
end;
assume p in ((elementary_tree 2) with-replacement (<*0*>,T1)) with-replacement (<*1*>,T2) ; ::_thesis: p in tree (T1,T2)
then A19: ( ( p in (elementary_tree 2) with-replacement (<*0*>,T1) & not <*1*> is_a_proper_prefix_of p ) or ex r being FinSequence of NAT st
( r in T2 & p = <*1*> ^ r ) ) by A10, TREES_1:def_9;
now__::_thesis:_(_p_in_(elementary_tree_2)_with-replacement_(<*0*>,T1)_implies_p_in_tree_(T1,T2)_)
assume p in (elementary_tree 2) with-replacement (<*0*>,T1) ; ::_thesis: p in tree (T1,T2)
then A20: ( ( p in elementary_tree 2 & not <*0*> is_a_proper_prefix_of p ) or ex r being FinSequence of NAT st
( r in T1 & p = <*0*> ^ r ) ) by A8, TREES_1:def_9;
now__::_thesis:_(_p_in_elementary_tree_2_implies_p_in_tree_(T1,T2)_)
assume p in elementary_tree 2 ; ::_thesis: p in tree (T1,T2)
then A21: ( p = {} or p = <*0*> or p = <*1*> ) by ENUMSET1:def_1, TREES_1:53;
p ^ {} = p by FINSEQ_1:34;
hence p in tree (T1,T2) by A1, A2, A3, A4, A5, A6, A7, A21, Def15; ::_thesis: verum
end;
hence p in tree (T1,T2) by A1, A3, A5, A20, Def15; ::_thesis: verum
end;
hence p in tree (T1,T2) by A2, A3, A4, A19, Def15; ::_thesis: verum
end;
registration
let p be FinTree-yielding FinSequence;
cluster tree p -> finite ;
coherence
tree p is finite
proof
defpred S1[ set ] means for p being FinTree-yielding FinSequence st len p = p holds
tree p is finite Tree;
A1: S1[ 0 ]
proof
let p be FinTree-yielding FinSequence; ::_thesis: ( len p = 0 implies tree p is finite Tree )
assume len p = 0 ; ::_thesis: tree p is finite Tree
then p = {} ;
hence tree p is finite Tree by Th52; ::_thesis: verum
end;
A2: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A3: for p being FinTree-yielding FinSequence st len p = n holds
tree p is finite Tree ; ::_thesis: S1[n + 1]
let p be FinTree-yielding FinSequence; ::_thesis: ( len p = n + 1 implies tree p is finite Tree )
assume A4: len p = n + 1 ; ::_thesis: tree p is finite Tree
p <> {} by A4;
then consider q being FinSequence, x being set such that
A5: p = q ^ <*x*> by FINSEQ_1:46;
reconsider q = q as FinTree-yielding FinSequence by A5, Th26;
len <*x*> = 1 by FINSEQ_1:40;
then A6: len p = (len q) + 1 by A5, FINSEQ_1:22;
then tree q is finite by A3, A4;
then reconsider W = (tree q) \/ (elementary_tree (n + 1)) as finite Tree ;
<*x*> is FinTree-yielding by A5, Th26;
then reconsider x = x as finite Tree by Th29;
n < n + 1 by NAT_1:13;
then <*n*> in elementary_tree (n + 1) by TREES_1:28;
then reconsider r = <*n*> as Element of W by XBOOLE_0:def_3;
tree p = W with-replacement (r,x) by A4, A5, A6, Th55;
hence tree p is finite Tree ; ::_thesis: verum
end;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A1, A2);
then ( len p = len p implies tree p is finite ) ;
hence tree p is finite ; ::_thesis: verum
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 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 ) ) )
proof
let T be Tree; ::_thesis: for x being set holds
( x in ^ T iff ( x = {} or ex p being FinSequence st
( p in T & x = <*0*> ^ p ) ) )
let x be set ; ::_thesis: ( x in ^ T iff ( x = {} or ex p being FinSequence st
( p in T & x = <*0*> ^ p ) ) )
set p = <*T*>;
A1: len <*T*> = 1 by FINSEQ_1:40;
A2: <*T*> . 1 = T by FINSEQ_1:40;
thus ( x in ^ T & x <> {} implies ex p being FinSequence st
( p in T & x = <*0*> ^ p ) ) ::_thesis: ( ( x = {} or ex p being FinSequence st
( p in T & x = <*0*> ^ p ) ) implies x in ^ T )
proof
assume that
A3: x in ^ T and
A4: x <> {} ; ::_thesis: ex p being FinSequence st
( p in T & x = <*0*> ^ p )
consider n being Element of NAT , q being FinSequence such that
A5: n < len <*T*> and
A6: q in <*T*> . (n + 1) and
A7: x = <*n*> ^ q by A3, A4, Def15;
0 + 1 = 1 ;
then n = 0 by A1, A5, NAT_1:13;
hence ex p being FinSequence st
( p in T & x = <*0*> ^ p ) by A2, A6, A7; ::_thesis: verum
end;
0 < 0 + 1 ;
hence ( ( x = {} or ex p being FinSequence st
( p in T & x = <*0*> ^ p ) ) implies x in ^ T ) by A1, A2, Def15; ::_thesis: verum
end;
theorem Th61: :: TREES_3:61
for T being Tree
for p being FinSequence holds
( p in T iff <*0*> ^ p in ^ T )
proof
let T be Tree; ::_thesis: for p being FinSequence holds
( p in T iff <*0*> ^ p in ^ T )
let p be FinSequence; ::_thesis: ( p in T iff <*0*> ^ p in ^ T )
thus ( p in T implies <*0*> ^ p in ^ T ) by Th60; ::_thesis: ( <*0*> ^ p in ^ T implies p in T )
assume <*0*> ^ p in ^ T ; ::_thesis: p in T
then consider n being Element of NAT , q being FinSequence such that
n < len <*T*> and
A1: q in <*T*> . (n + 1) and
A2: <*0*> ^ p = <*n*> ^ q by Def15;
A3: (<*0*> ^ p) . 1 = 0 by FINSEQ_1:41;
A4: (<*n*> ^ q) . 1 = n by FINSEQ_1:41;
then p = q by A2, A3, FINSEQ_1:33;
hence p in T by A1, A2, A3, A4, FINSEQ_1:40; ::_thesis: verum
end;
theorem :: TREES_3:62
for T being Tree holds elementary_tree 1 c= ^ T
proof
let T be Tree; ::_thesis: elementary_tree 1 c= ^ T
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in elementary_tree 1 or x in ^ T )
assume x in elementary_tree 1 ; ::_thesis: x in ^ T
then reconsider p = x as Element of elementary_tree 1 ;
( p = {} or ( p = <*0*> & {} in T & <*0*> ^ {} = <*0*> ) ) by FINSEQ_1:34, TARSKI:def_2, TREES_1:22, TREES_1:51;
hence x in ^ T by Th60; ::_thesis: verum
end;
theorem :: TREES_3:63
for T1, T2 being Tree st T1 c= T2 holds
^ T1 c= ^ T2
proof
let T1, T2 be Tree; ::_thesis: ( T1 c= T2 implies ^ T1 c= ^ T2 )
assume A1: T1 c= T2 ; ::_thesis: ^ T1 c= ^ T2
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ^ T1 or x in ^ T2 )
assume x in ^ T1 ; ::_thesis: x in ^ T2
then reconsider p = x as Element of ^ T1 ;
( p = {} or ex q being FinSequence st
( q in T1 & p = <*0*> ^ q ) ) by Th60;
hence x in ^ T2 by A1, Th60; ::_thesis: verum
end;
theorem :: TREES_3:64
for T1, T2 being Tree st ^ T1 = ^ T2 holds
T1 = T2
proof
let T1, T2 be Tree; ::_thesis: ( ^ T1 = ^ T2 implies T1 = T2 )
assume A1: ^ T1 = ^ T2 ; ::_thesis: T1 = T2
let p be FinSequence of NAT ; :: according to TREES_2:def_1 ::_thesis: ( ( not p in T1 or p in T2 ) & ( not p in T2 or p in T1 ) )
( p in T1 iff <*0*> ^ p in ^ T1 ) by Th61;
hence ( ( not p in T1 or p in T2 ) & ( not p in T2 or p in T1 ) ) by A1, Th61; ::_thesis: verum
end;
theorem :: TREES_3:65
for T being Tree holds (^ T) | <*0*> = T
proof
let T be Tree; ::_thesis: (^ T) | <*0*> = T
set p = <*T*>;
A1: len <*T*> = 1 by FINSEQ_1:40;
A2: <*T*> . 1 = T by FINSEQ_1:40;
0 + 1 = 1 ;
hence (^ T) | <*0*> = T by A1, A2, Th49; ::_thesis: verum
end;
theorem :: TREES_3:66
for T1, T2 being Tree holds (^ T1) with-replacement (<*0*>,T2) = ^ T2
proof
let T1, T2 be Tree; ::_thesis: (^ T1) with-replacement (<*0*>,T2) = ^ T2
A1: len {} = 0 ;
A2: <*T1*> = {} ^ <*T1*> by FINSEQ_1:34;
A3: <*T2*> = {} ^ <*T2*> by FINSEQ_1:34;
A4: <*T1*> = <*T1*> ^ {} by FINSEQ_1:34;
<*T2*> = <*T2*> ^ {} by FINSEQ_1:34;
hence (^ T1) with-replacement (<*0*>,T2) = ^ T2 by A1, A2, A3, A4, Th57; ::_thesis: verum
end;
theorem :: TREES_3:67
^ (elementary_tree 0) = elementary_tree 1
proof
set T = elementary_tree 0;
thus ^ (elementary_tree 0) = tree (1 |-> (elementary_tree 0)) by FINSEQ_2:59
.= elementary_tree 1 by Th54 ; ::_thesis: verum
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 ) ) ) )
proof
let T1, T2 be Tree; ::_thesis: 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 ) ) ) )
let x be set ; ::_thesis: ( 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 ) ) ) )
set p = <*T1,T2*>;
A1: len <*T1,T2*> = 2 by FINSEQ_1:44;
A2: <*T1,T2*> . 1 = T1 by FINSEQ_1:44;
A3: <*T1,T2*> . 2 = T2 by FINSEQ_1:44;
thus ( x in tree (T1,T2) & x <> {} implies ex p being FinSequence st
( ( p in T1 & x = <*0*> ^ p ) or ( p in T2 & x = <*1*> ^ p ) ) ) ::_thesis: ( ( x = {} or ex p being FinSequence st
( ( p in T1 & x = <*0*> ^ p ) or ( p in T2 & x = <*1*> ^ p ) ) ) implies x in tree (T1,T2) )
proof
assume that
A4: x in tree (T1,T2) and
A5: x <> {} ; ::_thesis: ex p being FinSequence st
( ( p in T1 & x = <*0*> ^ p ) or ( p in T2 & x = <*1*> ^ p ) )
consider n being Element of NAT , q being FinSequence such that
A6: n < len <*T1,T2*> and
A7: q in <*T1,T2*> . (n + 1) and
A8: x = <*n*> ^ q by A4, A5, Def15;
1 + 1 = 2 ;
then n <= 1 by A1, A6, NAT_1:13;
then ( n = 1 or n < 0 + 1 ) by XXREAL_0:1;
then ( n = 1 or n = 0 ) by NAT_1:13;
hence ex p being FinSequence st
( ( p in T1 & x = <*0*> ^ p ) or ( p in T2 & x = <*1*> ^ p ) ) by A2, A3, A7, A8; ::_thesis: verum
end;
now__::_thesis:_(_ex_q_being_FinSequence_st_
(_(_q_in_T1_&_x_=_<*0*>_^_q_)_or_(_q_in_T2_&_x_=_<*1*>_^_q_)_)_implies_ex_n_being_Element_of_NAT_ex_q_being_FinSequence_st_
(_n_<_len_<*T1,T2*>_&_q_in_<*T1,T2*>_._(n_+_1)_&_x_=_<*n*>_^_q_)_)
given q being FinSequence such that A9: ( ( q in T1 & x = <*0*> ^ q ) or ( q in T2 & x = <*1*> ^ q ) ) ; ::_thesis: ex n being Element of NAT ex q being FinSequence st
( n < len <*T1,T2*> & q in <*T1,T2*> . (n + 1) & x = <*n*> ^ q )
( x = <*0*> ^ q or x <> <*0*> ^ q ) ;
then consider n being Element of NAT such that
A10: ( ( n = 0 & x = <*0*> ^ q ) or ( n = 1 & x <> <*0*> ^ q ) ) ;
take n = n; ::_thesis: ex q being FinSequence st
( n < len <*T1,T2*> & q in <*T1,T2*> . (n + 1) & x = <*n*> ^ q )
take q = q; ::_thesis: ( n < len <*T1,T2*> & q in <*T1,T2*> . (n + 1) & x = <*n*> ^ q )
thus n < len <*T1,T2*> by A1, A10; ::_thesis: ( q in <*T1,T2*> . (n + 1) & x = <*n*> ^ q )
(<*0*> ^ q) . 1 = 0 by FINSEQ_1:41;
hence ( q in <*T1,T2*> . (n + 1) & x = <*n*> ^ q ) by A9, A10, FINSEQ_1:41, FINSEQ_1:44; ::_thesis: verum
end;
hence ( ( x = {} or ex p being FinSequence st
( ( p in T1 & x = <*0*> ^ p ) or ( p in T2 & x = <*1*> ^ p ) ) ) implies x in tree (T1,T2) ) by Def15; ::_thesis: verum
end;
theorem Th69: :: TREES_3:69
for T1, T2 being Tree
for p being FinSequence holds
( p in T1 iff <*0*> ^ p in tree (T1,T2) )
proof
let T1, T2 be Tree; ::_thesis: for p being FinSequence holds
( p in T1 iff <*0*> ^ p in tree (T1,T2) )
A1: <*T1,T2*> = <*T1*> ^ <*T2*> by FINSEQ_1:def_9;
A2: <*T1*> = {} ^ <*T1*> by FINSEQ_1:34;
len {} = 0 ;
hence for p being FinSequence holds
( p in T1 iff <*0*> ^ p in tree (T1,T2) ) by A1, A2, Th51; ::_thesis: verum
end;
theorem Th70: :: TREES_3:70
for T1, T2 being Tree
for p being FinSequence holds
( p in T2 iff <*1*> ^ p in tree (T1,T2) )
proof
let T1, T2 be Tree; ::_thesis: for p being FinSequence holds
( p in T2 iff <*1*> ^ p in tree (T1,T2) )
A1: <*T1,T2*> = <*T1*> ^ <*T2*> by FINSEQ_1:def_9;
A2: len <*T1*> = 1 by FINSEQ_1:40;
<*T1,T2*> = <*T1,T2*> ^ {} by FINSEQ_1:34;
hence for p being FinSequence holds
( p in T2 iff <*1*> ^ p in tree (T1,T2) ) by A1, A2, Th51; ::_thesis: verum
end;
theorem :: TREES_3:71
for T1, T2 being Tree holds elementary_tree 2 c= tree (T1,T2)
proof
let T1, T2 be Tree; ::_thesis: elementary_tree 2 c= tree (T1,T2)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in elementary_tree 2 or x in tree (T1,T2) )
assume x in elementary_tree 2 ; ::_thesis: x in tree (T1,T2)
then reconsider p = x as Element of elementary_tree 2 ;
( p = {} or ( p = <*0*> & {} in T1 & <*0*> ^ {} = <*0*> ) or ( p = <*1*> & {} in T2 & <*1*> ^ {} = <*1*> ) ) by ENUMSET1:def_1, FINSEQ_1:34, TREES_1:22, TREES_1:53;
hence x in tree (T1,T2) by Th68; ::_thesis: verum
end;
theorem :: TREES_3:72
for T1, T2, W1, W2 being Tree st T1 c= W1 & T2 c= W2 holds
tree (T1,T2) c= tree (W1,W2)
proof
let T1, T2, W1, W2 be Tree; ::_thesis: ( T1 c= W1 & T2 c= W2 implies tree (T1,T2) c= tree (W1,W2) )
assume that
A1: T1 c= W1 and
A2: T2 c= W2 ; ::_thesis: tree (T1,T2) c= tree (W1,W2)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in tree (T1,T2) or x in tree (W1,W2) )
assume x in tree (T1,T2) ; ::_thesis: x in tree (W1,W2)
then reconsider p = x as Element of tree (T1,T2) ;
( p = {} or ex q being FinSequence st
( ( q in T1 & p = <*0*> ^ q ) or ( q in T2 & p = <*1*> ^ q ) ) ) by Th68;
hence x in tree (W1,W2) by A1, A2, Th68; ::_thesis: verum
end;
theorem :: TREES_3:73
for T1, T2, W1, W2 being Tree st tree (T1,T2) = tree (W1,W2) holds
( T1 = W1 & T2 = W2 )
proof
let T1, T2, W1, W2 be Tree; ::_thesis: ( tree (T1,T2) = tree (W1,W2) implies ( T1 = W1 & T2 = W2 ) )
assume A1: tree (T1,T2) = tree (W1,W2) ; ::_thesis: ( T1 = W1 & T2 = W2 )
now__::_thesis:_for_p_being_FinSequence_holds_
(_p_in_T1_iff_p_in_W1_)
let p be FinSequence; ::_thesis: ( p in T1 iff p in W1 )
( p in T1 iff <*0*> ^ p in tree (T1,T2) ) by Th69;
hence ( p in T1 iff p in W1 ) by A1, Th69; ::_thesis: verum
end;
hence for p being FinSequence of NAT holds
( p in T1 iff p in W1 ) ; :: according to TREES_2:def_1 ::_thesis: T2 = W2
let p be FinSequence of NAT ; :: according to TREES_2:def_1 ::_thesis: ( ( not p in T2 or p in W2 ) & ( not p in W2 or p in T2 ) )
( p in T2 iff <*1*> ^ p in tree (T1,T2) ) by Th70;
hence ( ( not p in T2 or p in W2 ) & ( not p in W2 or p in T2 ) ) by A1, Th70; ::_thesis: verum
end;
theorem :: TREES_3:74
for T1, T2 being Tree holds
( (tree (T1,T2)) | <*0*> = T1 & (tree (T1,T2)) | <*1*> = T2 )
proof
let T1, T2 be Tree; ::_thesis: ( (tree (T1,T2)) | <*0*> = T1 & (tree (T1,T2)) | <*1*> = T2 )
set p = <*T1,T2*>;
A1: len <*T1,T2*> = 2 by FINSEQ_1:44;
A2: <*T1,T2*> . 1 = T1 by FINSEQ_1:44;
A3: <*T1,T2*> . 2 = T2 by FINSEQ_1:44;
A4: 0 + 1 = 1 ;
1 + 1 = 2 ;
hence ( (tree (T1,T2)) | <*0*> = T1 & (tree (T1,T2)) | <*1*> = T2 ) by A1, A2, A3, A4, Th49; ::_thesis: verum
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) )
proof
let T, T1, T2 be Tree; ::_thesis: ( (tree (T1,T2)) with-replacement (<*0*>,T) = tree (T,T2) & (tree (T1,T2)) with-replacement (<*1*>,T) = tree (T1,T) )
A1: len {} = 0 ;
A2: <*T1*> = {} ^ <*T1*> by FINSEQ_1:34;
A3: <*T*> = {} ^ <*T*> by FINSEQ_1:34;
A4: <*T1,T2*> ^ {} = <*T1,T2*> by FINSEQ_1:34;
A5: <*T1,T*> ^ {} = <*T1,T*> by FINSEQ_1:34;
A6: len <*T1*> = 1 by FINSEQ_1:40;
A7: <*T1,T2*> = <*T1*> ^ <*T2*> by FINSEQ_1:def_9;
A8: <*T1,T*> = <*T1*> ^ <*T*> by FINSEQ_1:def_9;
<*T,T2*> = <*T*> ^ <*T2*> by FINSEQ_1:def_9;
hence ( (tree (T1,T2)) with-replacement (<*0*>,T) = tree (T,T2) & (tree (T1,T2)) with-replacement (<*1*>,T) = tree (T1,T) ) by A1, A2, A3, A4, A5, A6, A7, A8, Th57; ::_thesis: verum
end;
theorem :: TREES_3:76
tree ((elementary_tree 0),(elementary_tree 0)) = elementary_tree 2
proof
set T = elementary_tree 0;
thus tree ((elementary_tree 0),(elementary_tree 0)) = tree (2 |-> (elementary_tree 0)) by FINSEQ_2:61
.= elementary_tree 2 by Th54 ; ::_thesis: verum
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
proof
let n be Element of NAT ; ::_thesis: 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
let w be FinTree-yielding FinSequence; ::_thesis: ( ( for t being finite Tree st t in rng w holds
height t <= n ) implies height (tree w) <= n + 1 )
assume A1: for t being finite Tree st t in rng w holds
height t <= n ; ::_thesis: height (tree w) <= n + 1
consider p being FinSequence of NAT such that
A2: p in tree w and
A3: len p = height (tree w) by TREES_1:def_12;
A4: ( ( p = {} & len {} = 0 ) or ex n being Element of NAT ex q being FinSequence st
( n < len w & q in w . (n + 1) & p = <*n*> ^ q ) ) by A2, Def15;
now__::_thesis:_(_ex_k_being_Element_of_NAT_ex_q_being_FinSequence_st_
(_k_<_len_w_&_q_in_w_._(k_+_1)_&_p_=_<*k*>_^_q_)_implies_height_(tree_w)_<=_n_+_1_)
given k being Element of NAT , q being FinSequence such that A5: k < len w and
A6: q in w . (k + 1) and
A7: p = <*k*> ^ q ; ::_thesis: height (tree w) <= n + 1
A8: w . (k + 1) in rng w by A5, Lm3;
rng w is constituted-FinTrees by Def10;
then reconsider t = w . (k + 1) as finite Tree by A8;
reconsider q = q as FinSequence of NAT by A7, FINSEQ_1:36;
A9: len q <= height t by A6, TREES_1:def_12;
A10: height t <= n by A1, A5, Lm3;
A11: len <*k*> = 1 by FINSEQ_1:40;
A12: len q <= n by A9, A10, XXREAL_0:2;
len p = 1 + (len q) by A7, A11, FINSEQ_1:22;
hence height (tree w) <= n + 1 by A3, A12, XREAL_1:7; ::_thesis: verum
end;
hence height (tree w) <= n + 1 by A3, A4; ::_thesis: verum
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
proof
let w be FinTree-yielding FinSequence; ::_thesis: for t being finite Tree st t in rng w holds
height (tree w) > height t
let t be finite Tree; ::_thesis: ( t in rng w implies height (tree w) > height t )
assume t in rng w ; ::_thesis: height (tree w) > height t
then consider x being set such that
A1: x in dom w and
A2: t = w . x by FUNCT_1:def_3;
reconsider x = x as Element of NAT by A1;
A3: 1 <= x by A1, FINSEQ_3:25;
A4: len w >= x by A1, FINSEQ_3:25;
consider n being Nat such that
A5: x = 1 + n by A3, NAT_1:10;
reconsider n = n as Element of NAT by ORDINAL1:def_12;
A6: n < len w by A4, A5, NAT_1:13;
A7: {} in t by TREES_1:22;
A8: <*n*> ^ {} = <*n*> by FINSEQ_1:34;
A9: t = (tree w) | <*n*> by A2, A5, A6, Th49;
<*n*> in tree w by A2, A5, A6, A7, A8, Def15;
hence height (tree w) > height t by A9, TREES_1:48; ::_thesis: verum
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
proof
let w be FinTree-yielding FinSequence; ::_thesis: 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
let t be finite Tree; ::_thesis: ( t in rng w & ( for t9 being finite Tree st t9 in rng w holds
height t9 <= height t ) implies height (tree w) = (height t) + 1 )
assume that
A1: t in rng w and
A2: for t9 being finite Tree st t9 in rng w holds
height t9 <= height t ; ::_thesis: height (tree w) = (height t) + 1
A3: height (tree w) > height t by A1, Th78;
A4: height (tree w) <= (height t) + 1 by A2, Th77;
height (tree w) >= (height t) + 1 by A3, NAT_1:13;
hence height (tree w) = (height t) + 1 by A4, XXREAL_0:1; ::_thesis: verum
end;
theorem :: TREES_3:80
for T being finite Tree holds height (^ T) = (height T) + 1
proof
let T be finite Tree; ::_thesis: height (^ T) = (height T) + 1
set m = height T;
A1: rng <*T*> = {T} by FINSEQ_1:38;
A2: T in {T} by TARSKI:def_1;
for t being finite Tree st t in rng <*T*> holds
height t <= height T by A1, TARSKI:def_1;
hence height (^ T) = (height T) + 1 by A1, A2, Th79; ::_thesis: verum
end;
theorem :: TREES_3:81
for T1, T2 being finite Tree holds height (tree (T1,T2)) = (max ((height T1),(height T2))) + 1
proof
let T1, T2 be finite Tree; ::_thesis: height (tree (T1,T2)) = (max ((height T1),(height T2))) + 1
set m = max ((height T1),(height T2));
A1: rng <*T1,T2*> = {T1,T2} by FINSEQ_2:127;
A2: T1 in {T1,T2} by TARSKI:def_2;
A3: T2 in {T1,T2} by TARSKI:def_2;
A4: ( max ((height T1),(height T2)) = height T1 or max ((height T1),(height T2)) = height T2 ) by XXREAL_0:def_10;
now__::_thesis:_for_t_being_finite_Tree_st_t_in_rng_<*T1,T2*>_holds_
height_t_<=_max_((height_T1),(height_T2))
let t be finite Tree; ::_thesis: ( t in rng <*T1,T2*> implies height t <= max ((height T1),(height T2)) )
assume t in rng <*T1,T2*> ; ::_thesis: height t <= max ((height T1),(height T2))
then ( t = T1 or t = T2 ) by A1, TARSKI:def_2;
hence height t <= max ((height T1),(height T2)) by XXREAL_0:25; ::_thesis: verum
end;
hence height (tree (T1,T2)) = (max ((height T1),(height T2))) + 1 by A1, A2, A3, A4, Th79; ::_thesis: verum
end;
begin
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 B1: 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 Element of 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 Element of NAT st i in dom p holds
ex T being DecoratedTree st
( T = p . i & b1 . i = T . {} ) ) )
proof
A1: Seg (len p) = dom p by FINSEQ_1:def_3;
A2: for k being Nat st k in Seg (len p) holds
ex x being set st S1[k,x]
proof
let k be Nat; ::_thesis: ( k in Seg (len p) implies ex x being set st S1[k,x] )
assume k in Seg (len p) ; ::_thesis: ex x being set st S1[k,x]
then A3: p . k in rng p by A1, FUNCT_1:def_3;
rng p is constituted-DTrees by B1, Def11;
then reconsider T = p . k as DecoratedTree by A3;
take T . {} ; ::_thesis: S1[k,T . {}]
take T ; ::_thesis: ( T = p . k & T . {} = T . {} )
thus ( T = p . k & T . {} = T . {} ) ; ::_thesis: verum
end;
consider q being FinSequence such that
A4: ( dom q = Seg (len p) & ( for k being Nat st k in Seg (len p) holds
S1[k,q . k] ) ) from FINSEQ_1:sch_1(A2);
take q ; ::_thesis: ( dom q = dom p & ( for i being Element of NAT st i in dom p holds
ex T being DecoratedTree st
( T = p . i & q . i = T . {} ) ) )
thus dom q = dom p by A4, FINSEQ_1:def_3; ::_thesis: for i being Element of NAT st i in dom p holds
ex T being DecoratedTree st
( T = p . i & q . i = T . {} )
thus for i being Element of NAT st i in dom p holds
ex T being DecoratedTree st
( T = p . i & q . i = T . {} ) by A1, A4; ::_thesis: verum
end;
uniqueness
for b1, b2 being FinSequence st dom b1 = dom p & ( for i being Element of 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 Element of NAT st i in dom p holds
ex T being DecoratedTree st
( T = p . i & b2 . i = T . {} ) ) holds
b1 = b2
proof
let x1, x2 be FinSequence; ::_thesis: ( dom x1 = dom p & ( for i being Element of NAT st i in dom p holds
ex T being DecoratedTree st
( T = p . i & x1 . i = T . {} ) ) & dom x2 = dom p & ( for i being Element of NAT st i in dom p holds
ex T being DecoratedTree st
( T = p . i & x2 . i = T . {} ) ) implies x1 = x2 )
assume that
A5: dom x1 = dom p and
A6: for i being Element of NAT st i in dom p holds
S1[i,x1 . i] and
A7: dom x2 = dom p and
A8: for i being Element of NAT st i in dom p holds
S1[i,x2 . i] ; ::_thesis: x1 = x2
now__::_thesis:_for_k_being_Nat_st_k_in_dom_p_holds_
x1_._k_=_x2_._k
let k be Nat; ::_thesis: ( k in dom p implies x1 . k = x2 . k )
assume A9: k in dom p ; ::_thesis: x1 . k = x2 . k
then A10: S1[k,x1 . k] by A6;
S1[k,x2 . k] by A8, A9;
hence x1 . k = x2 . k by A10; ::_thesis: verum
end;
hence x1 = x2 by A5, A7, FINSEQ_1:13; ::_thesis: verum
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 Element of NAT st i in dom p holds
ex T being DecoratedTree st
( T = p . i & b2 . i = T . {} ) ) ) );