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