:: BINTREE2 semantic presentation begin Lm1: for D being set for p, q being FinSequence of D holds p ^ q is FinSequence of D ; Lm2: for D being non empty set for x being Element of D holds <*x*> is FinSequence of D ; theorem Th1: :: BINTREE2:1 for D being set for p being FinSequence for n being Element of NAT st p in D * holds p | (Seg n) in D * proof let D be set ; ::_thesis: for p being FinSequence for n being Element of NAT st p in D * holds p | (Seg n) in D * let p be FinSequence; ::_thesis: for n being Element of NAT st p in D * holds p | (Seg n) in D * let n be Element of NAT ; ::_thesis: ( p in D * implies p | (Seg n) in D * ) assume p in D * ; ::_thesis: p | (Seg n) in D * then p is FinSequence of D by FINSEQ_1:def_11; then p | (Seg n) is FinSequence of D by FINSEQ_1:18; hence p | (Seg n) in D * by FINSEQ_1:def_11; ::_thesis: verum end; theorem Th2: :: BINTREE2:2 for T being binary Tree for t being Element of T holds t is FinSequence of BOOLEAN proof let T be binary Tree; ::_thesis: for t being Element of T holds t is FinSequence of BOOLEAN let t be Element of T; ::_thesis: t is FinSequence of BOOLEAN defpred S1[ FinSequence] means ( \$1 is Element of T implies rng \$1 c= BOOLEAN ); A1: for p being FinSequence of NAT for x being Element of NAT st S1[p] holds S1[p ^ <*x*>] proof let p be FinSequence of NAT ; ::_thesis: for x being Element of NAT st S1[p] holds S1[p ^ <*x*>] let x be Element of NAT ; ::_thesis: ( S1[p] implies S1[p ^ <*x*>] ) assume A2: S1[p] ; ::_thesis: S1[p ^ <*x*>] assume A3: p ^ <*x*> is Element of T ; ::_thesis: rng (p ^ <*x*>) c= BOOLEAN then reconsider p1 = p as Element of T by TREES_1:21; p ^ <*x*> in { (p ^ <*n*>) where n is Element of NAT : p ^ <*n*> in T } by A3; then A4: p ^ <*x*> in succ p1 by TREES_2:def_5; then not p in Leaves T by BINTREE1:3; then succ p1 = {(p ^ <*0*>),(p ^ <*1*>)} by BINTREE1:def_2; then ( p ^ <*x*> = p ^ <*0*> or p ^ <*x*> = p ^ <*1*> ) by A4, TARSKI:def_2; then ( x = 0 or x = 1 ) by FINSEQ_2:17; then A5: x in {0,1} by TARSKI:def_2; A6: {x} c= BOOLEAN proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in {x} or z in BOOLEAN ) assume z in {x} ; ::_thesis: z in BOOLEAN hence z in BOOLEAN by A5, TARSKI:def_1; ::_thesis: verum end; rng <*x*> = {x} by FINSEQ_1:38; then (rng p) \/ (rng <*x*>) c= BOOLEAN by A2, A3, A6, TREES_1:21, XBOOLE_1:8; hence rng (p ^ <*x*>) c= BOOLEAN by FINSEQ_1:31; ::_thesis: verum end; A7: S1[ <*> NAT] by XBOOLE_1:2; for p being FinSequence of NAT holds S1[p] from FINSEQ_2:sch_2(A7, A1); then rng t c= BOOLEAN ; hence t is FinSequence of BOOLEAN by FINSEQ_1:def_4; ::_thesis: verum end; definition let T be binary Tree; :: original: Element redefine mode Element of T -> FinSequence of BOOLEAN ; coherence for b1 being Element of T holds b1 is FinSequence of BOOLEAN by Th2; end; theorem Th3: :: BINTREE2:3 for T being Tree st T = {0,1} * holds T is binary proof let T be Tree; ::_thesis: ( T = {0,1} * implies T is binary ) assume A1: T = {0,1} * ; ::_thesis: T is binary now__::_thesis:_for_t_being_Element_of_T_st_not_t_in_Leaves_T_holds_ succ_t_=_{(t_^_<*0*>),(t_^_<*1*>)} let t be Element of T; ::_thesis: ( not t in Leaves T implies succ t = {(t ^ <*0*>),(t ^ <*1*>)} ) assume not t in Leaves T ; ::_thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)} { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in T } = {(t ^ <*0*>),(t ^ <*1*>)} proof thus { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in T } c= {(t ^ <*0*>),(t ^ <*1*>)} :: according to XBOOLE_0:def_10 ::_thesis: {(t ^ <*0*>),(t ^ <*1*>)} c= { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in T } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in T } or x in {(t ^ <*0*>),(t ^ <*1*>)} ) assume x in { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in T } ; ::_thesis: x in {(t ^ <*0*>),(t ^ <*1*>)} then consider n being Element of NAT such that A2: x = t ^ <*n*> and A3: t ^ <*n*> in T ; reconsider tn = t ^ <*n*> as FinSequence of {0,1} by A1, A3, FINSEQ_1:def_11; (len t) + 1 in Seg ((len t) + 1) by FINSEQ_1:4; then (len t) + 1 in Seg (len tn) by FINSEQ_2:16; then (len t) + 1 in dom tn by FINSEQ_1:def_3; then tn /. ((len t) + 1) = (t ^ <*n*>) . ((len t) + 1) by PARTFUN1:def_6 .= n by FINSEQ_1:42 ; then ( n = 0 or n = 1 ) by TARSKI:def_2; hence x in {(t ^ <*0*>),(t ^ <*1*>)} by A2, TARSKI:def_2; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(t ^ <*0*>),(t ^ <*1*>)} or x in { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in T } ) A4: t is FinSequence of {0,1} by A1, FINSEQ_1:def_11; rng <*1*> c= {0,1} proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng <*1*> or z in {0,1} ) assume z in rng <*1*> ; ::_thesis: z in {0,1} then z in {1} by FINSEQ_1:38; then z = 1 by TARSKI:def_1; hence z in {0,1} by TARSKI:def_2; ::_thesis: verum end; then <*1*> is FinSequence of {0,1} by FINSEQ_1:def_4; then t ^ <*1*> is FinSequence of {0,1} by A4, Lm1; then A5: t ^ <*1*> in T by A1, FINSEQ_1:def_11; assume x in {(t ^ <*0*>),(t ^ <*1*>)} ; ::_thesis: x in { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in T } then A6: ( x = t ^ <*0*> or x = t ^ <*1*> ) by TARSKI:def_2; rng <*0*> c= {0,1} proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng <*0*> or z in {0,1} ) assume z in rng <*0*> ; ::_thesis: z in {0,1} then z in {0} by FINSEQ_1:38; then z = 0 by TARSKI:def_1; hence z in {0,1} by TARSKI:def_2; ::_thesis: verum end; then <*0*> is FinSequence of {0,1} by FINSEQ_1:def_4; then t ^ <*0*> is FinSequence of {0,1} by A4, Lm1; then t ^ <*0*> in T by A1, FINSEQ_1:def_11; hence x in { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in T } by A5, A6; ::_thesis: verum end; hence succ t = {(t ^ <*0*>),(t ^ <*1*>)} by TREES_2:def_5; ::_thesis: verum end; hence T is binary by BINTREE1:def_2; ::_thesis: verum end; theorem Th4: :: BINTREE2:4 for T being Tree st T = {0,1} * holds Leaves T = {} proof A1: {0} c= BOOLEAN proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in {0} or z in BOOLEAN ) assume z in {0} ; ::_thesis: z in BOOLEAN then z = FALSE by TARSKI:def_1; hence z in BOOLEAN ; ::_thesis: verum end; let T be Tree; ::_thesis: ( T = {0,1} * implies Leaves T = {} ) assume A2: T = {0,1} * ; ::_thesis: Leaves T = {} assume Leaves T <> {} ; ::_thesis: contradiction then consider x being set such that A3: x in Leaves T by XBOOLE_0:def_1; reconsider x1 = x as Element of T by A3; T is binary by A2, Th3; then A4: x1 is FinSequence of BOOLEAN by Th2; then reconsider x1 = x as FinSequence of NAT ; set y1 = x1 ^ <*0*>; 0 in {0} by TARSKI:def_1; then <*0*> is FinSequence of BOOLEAN by A1, Lm2; then x1 ^ <*0*> is FinSequence of BOOLEAN by A4, Lm1; then A5: x1 ^ <*0*> in T by A2, FINSEQ_1:def_11; x1 is_a_proper_prefix_of x1 ^ <*0*> by TREES_1:8; hence contradiction by A3, A5, TREES_1:def_5; ::_thesis: verum end; theorem :: BINTREE2:5 for T being binary Tree for n being Element of NAT for t being Element of T st t in T -level n holds t is Element of n -tuples_on BOOLEAN proof let T be binary Tree; ::_thesis: for n being Element of NAT for t being Element of T st t in T -level n holds t is Element of n -tuples_on BOOLEAN let n be Element of NAT ; ::_thesis: for t being Element of T st t in T -level n holds t is Element of n -tuples_on BOOLEAN let t be Element of T; ::_thesis: ( t in T -level n implies t is Element of n -tuples_on BOOLEAN ) assume t in T -level n ; ::_thesis: t is Element of n -tuples_on BOOLEAN then t in { w where w is Element of T : len w = n } by TREES_2:def_6; then ex t2 being Element of T st ( t2 = t & len t2 = n ) ; hence t is Element of n -tuples_on BOOLEAN by FINSEQ_2:92; ::_thesis: verum end; theorem :: BINTREE2:6 for T being Tree st ( for t being Element of T holds succ t = {(t ^ <*0*>),(t ^ <*1*>)} ) holds Leaves T = {} proof let T be Tree; ::_thesis: ( ( for t being Element of T holds succ t = {(t ^ <*0*>),(t ^ <*1*>)} ) implies Leaves T = {} ) assume A1: for t being Element of T holds succ t = {(t ^ <*0*>),(t ^ <*1*>)} ; ::_thesis: Leaves T = {} assume Leaves T <> {} ; ::_thesis: contradiction then consider x being set such that A2: x in Leaves T by XBOOLE_0:def_1; reconsider t = x as Element of T by A2; succ t = {(t ^ <*0*>),(t ^ <*1*>)} by A1; hence contradiction by A2, BINTREE1:3; ::_thesis: verum end; theorem Th7: :: BINTREE2:7 for T being Tree st ( for t being Element of T holds succ t = {(t ^ <*0*>),(t ^ <*1*>)} ) holds T is binary proof let T be Tree; ::_thesis: ( ( for t being Element of T holds succ t = {(t ^ <*0*>),(t ^ <*1*>)} ) implies T is binary ) assume for t being Element of T holds succ t = {(t ^ <*0*>),(t ^ <*1*>)} ; ::_thesis: T is binary then for t being Element of T st not t in Leaves T holds succ t = {(t ^ <*0*>),(t ^ <*1*>)} ; hence T is binary by BINTREE1:def_2; ::_thesis: verum end; theorem Th8: :: BINTREE2:8 for T being Tree holds ( T = {0,1} * iff for t being Element of T holds succ t = {(t ^ <*0*>),(t ^ <*1*>)} ) proof let T be Tree; ::_thesis: ( T = {0,1} * iff for t being Element of T holds succ t = {(t ^ <*0*>),(t ^ <*1*>)} ) thus ( T = {0,1} * implies for t being Element of T holds succ t = {(t ^ <*0*>),(t ^ <*1*>)} ) ::_thesis: ( ( for t being Element of T holds succ t = {(t ^ <*0*>),(t ^ <*1*>)} ) implies T = {0,1} * ) proof assume A1: T = {0,1} * ; ::_thesis: for t being Element of T holds succ t = {(t ^ <*0*>),(t ^ <*1*>)} let t be Element of T; ::_thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)} ( T is binary & not t in Leaves T ) by A1, Th3, Th4; hence succ t = {(t ^ <*0*>),(t ^ <*1*>)} by BINTREE1:def_2; ::_thesis: verum end; assume A2: for t being Element of T holds succ t = {(t ^ <*0*>),(t ^ <*1*>)} ; ::_thesis: T = {0,1} * thus T = {0,1} * ::_thesis: verum proof thus T c= {0,1} * :: according to XBOOLE_0:def_10 ::_thesis: {0,1} * c= T proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in T or x in {0,1} * ) assume A3: x in T ; ::_thesis: x in {0,1} * T is binary by A2, Th7; then x is FinSequence of {0,1} by A3, Th2; hence x in {0,1} * by FINSEQ_1:def_11; ::_thesis: verum end; defpred S1[ FinSequence] means \$1 in T; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {0,1} * or x in T ) assume x in {0,1} * ; ::_thesis: x in T then A4: x is FinSequence of {0,1} by FINSEQ_1:def_11; A5: for p being FinSequence of {0,1} for n being Element of {0,1} st S1[p] holds S1[p ^ <*n*>] proof let p be FinSequence of {0,1}; ::_thesis: for n being Element of {0,1} st S1[p] holds S1[p ^ <*n*>] let n be Element of {0,1}; ::_thesis: ( S1[p] implies S1[p ^ <*n*>] ) A6: ( n = 0 or n = 1 ) by TARSKI:def_2; assume p in T ; ::_thesis: S1[p ^ <*n*>] then reconsider p1 = p as Element of T ; succ p1 = {(p1 ^ <*0*>),(p1 ^ <*1*>)} by A2; then p ^ <*n*> in succ p1 by A6, TARSKI:def_2; hence S1[p ^ <*n*>] ; ::_thesis: verum end; A7: S1[ <*> {0,1}] by TREES_1:22; for p being FinSequence of {0,1} holds S1[p] from FINSEQ_2:sch_2(A7, A5); hence x in T by A4; ::_thesis: verum end; end; scheme :: BINTREE2:sch 1 DecoratedBinTreeEx{ F1() -> non empty set , F2() -> Element of F1(), P1[ set , set , set ] } : ex D being binary DecoratedTree of F1() st ( dom D = {0,1} * & D . {} = F2() & ( for x being Node of D holds P1[D . x,D . (x ^ <*0*>),D . (x ^ <*1*>)] ) ) provided A1: for a being Element of F1() ex b, c being Element of F1() st P1[a,b,c] proof defpred S1[ set , set ] means ex b, c being Element of F1() st ( P1[\$1,b,c] & \$2 = [b,c] ); A2: for e being set st e in F1() holds ex u being set st ( u in [:F1(),F1():] & S1[e,u] ) proof let e be set ; ::_thesis: ( e in F1() implies ex u being set st ( u in [:F1(),F1():] & S1[e,u] ) ) assume e in F1() ; ::_thesis: ex u being set st ( u in [:F1(),F1():] & S1[e,u] ) then consider b, c being Element of F1() such that A3: P1[e,b,c] by A1; take u = [b,c]; ::_thesis: ( u in [:F1(),F1():] & S1[e,u] ) thus u in [:F1(),F1():] ; ::_thesis: S1[e,u] thus S1[e,u] by A3; ::_thesis: verum end; consider f being Function such that A4: dom f = F1() and A5: rng f c= [:F1(),F1():] and A6: for e being set st e in F1() holds S1[e,f . e] from FUNCT_1:sch_5(A2); deffunc H1( set ) -> set = IFEQ ((\$1 `2),0,((f . (\$1 `1)) `1),((f . (\$1 `1)) `2)); A7: for x being set st x in [:F1(),NAT:] holds H1(x) in F1() proof let x be set ; ::_thesis: ( x in [:F1(),NAT:] implies H1(x) in F1() ) assume x in [:F1(),NAT:] ; ::_thesis: H1(x) in F1() then x `1 in F1() by MCART_1:10; then A8: f . (x `1) in rng f by A4, FUNCT_1:def_3; then A9: (f . (x `1)) `2 in F1() by A5, MCART_1:10; A10: (f . (x `1)) `1 in F1() by A5, A8, MCART_1:10; now__::_thesis:_H1(x)_in_F1() percases ( x `2 = 0 or x `2 <> 0 ) ; suppose x `2 = 0 ; ::_thesis: H1(x) in F1() hence H1(x) in F1() by A10, FUNCOP_1:def_8; ::_thesis: verum end; suppose x `2 <> 0 ; ::_thesis: H1(x) in F1() hence H1(x) in F1() by A9, FUNCOP_1:def_8; ::_thesis: verum end; end; end; hence H1(x) in F1() ; ::_thesis: verum end; consider F being Function of [:F1(),NAT:],F1() such that A11: for x being set st x in [:F1(),NAT:] holds F . x = H1(x) from FUNCT_2:sch_2(A7); deffunc H2( set ) -> Element of NAT = 2; consider D being DecoratedTree of F1() such that A12: D . {} = F2() and A13: for d being Element of dom D holds ( succ d = { (d ^ <*k*>) where k is Element of NAT : k < H2(D . d) } & ( for n being Element of NAT st n < H2(D . d) holds D . (d ^ <*n*>) = F . ((D . d),n) ) ) from TREES_2:sch_9(); now__::_thesis:_for_t_being_Element_of_dom_D_st_not_t_in_Leaves_(dom_D)_holds_ succ_t_=_{(t_^_<*0*>),(t_^_<*1*>)} let t be Element of dom D; ::_thesis: ( not t in Leaves (dom D) implies succ t = {(t ^ <*0*>),(t ^ <*1*>)} ) assume not t in Leaves (dom D) ; ::_thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)} { (t ^ <*k*>) where k is Element of NAT : k < 2 } = {(t ^ <*0*>),(t ^ <*1*>)} proof thus { (t ^ <*k*>) where k is Element of NAT : k < 2 } c= {(t ^ <*0*>),(t ^ <*1*>)} :: according to XBOOLE_0:def_10 ::_thesis: {(t ^ <*0*>),(t ^ <*1*>)} c= { (t ^ <*k*>) where k is Element of NAT : k < 2 } proof let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in { (t ^ <*k*>) where k is Element of NAT : k < 2 } or v in {(t ^ <*0*>),(t ^ <*1*>)} ) assume v in { (t ^ <*k*>) where k is Element of NAT : k < 2 } ; ::_thesis: v in {(t ^ <*0*>),(t ^ <*1*>)} then consider k being Element of NAT such that A14: v = t ^ <*k*> and A15: k < 2 ; ( k = 0 or k = 1 ) by A15, NAT_1:23; hence v in {(t ^ <*0*>),(t ^ <*1*>)} by A14, TARSKI:def_2; ::_thesis: verum end; let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in {(t ^ <*0*>),(t ^ <*1*>)} or v in { (t ^ <*k*>) where k is Element of NAT : k < 2 } ) assume v in {(t ^ <*0*>),(t ^ <*1*>)} ; ::_thesis: v in { (t ^ <*k*>) where k is Element of NAT : k < 2 } then ( v = t ^ <*0*> or v = t ^ <*1*> ) by TARSKI:def_2; hence v in { (t ^ <*k*>) where k is Element of NAT : k < 2 } ; ::_thesis: verum end; hence succ t = {(t ^ <*0*>),(t ^ <*1*>)} by A13; ::_thesis: verum end; then dom D is binary by BINTREE1:def_2; then reconsider D = D as binary DecoratedTree of F1() by BINTREE1:def_3; take D ; ::_thesis: ( dom D = {0,1} * & D . {} = F2() & ( for x being Node of D holds P1[D . x,D . (x ^ <*0*>),D . (x ^ <*1*>)] ) ) now__::_thesis:_for_t_being_Element_of_dom_D_holds_succ_t_=_{(t_^_<*0*>),(t_^_<*1*>)} let t be Element of dom D; ::_thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)} { (t ^ <*k*>) where k is Element of NAT : k < 2 } = {(t ^ <*0*>),(t ^ <*1*>)} proof thus { (t ^ <*k*>) where k is Element of NAT : k < 2 } c= {(t ^ <*0*>),(t ^ <*1*>)} :: according to XBOOLE_0:def_10 ::_thesis: {(t ^ <*0*>),(t ^ <*1*>)} c= { (t ^ <*k*>) where k is Element of NAT : k < 2 } proof let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in { (t ^ <*k*>) where k is Element of NAT : k < 2 } or v in {(t ^ <*0*>),(t ^ <*1*>)} ) assume v in { (t ^ <*k*>) where k is Element of NAT : k < 2 } ; ::_thesis: v in {(t ^ <*0*>),(t ^ <*1*>)} then consider k being Element of NAT such that A16: v = t ^ <*k*> and A17: k < 2 ; ( k = 0 or k = 1 ) by A17, NAT_1:23; hence v in {(t ^ <*0*>),(t ^ <*1*>)} by A16, TARSKI:def_2; ::_thesis: verum end; let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in {(t ^ <*0*>),(t ^ <*1*>)} or v in { (t ^ <*k*>) where k is Element of NAT : k < 2 } ) assume v in {(t ^ <*0*>),(t ^ <*1*>)} ; ::_thesis: v in { (t ^ <*k*>) where k is Element of NAT : k < 2 } then ( v = t ^ <*0*> or v = t ^ <*1*> ) by TARSKI:def_2; hence v in { (t ^ <*k*>) where k is Element of NAT : k < 2 } ; ::_thesis: verum end; hence succ t = {(t ^ <*0*>),(t ^ <*1*>)} by A13; ::_thesis: verum end; hence dom D = {0,1} * by Th8; ::_thesis: ( D . {} = F2() & ( for x being Node of D holds P1[D . x,D . (x ^ <*0*>),D . (x ^ <*1*>)] ) ) thus D . {} = F2() by A12; ::_thesis: for x being Node of D holds P1[D . x,D . (x ^ <*0*>),D . (x ^ <*1*>)] let x be Node of D; ::_thesis: P1[D . x,D . (x ^ <*0*>),D . (x ^ <*1*>)] for e being set st e in F1() holds P1[e,F . (e,0),F . (e,1)] proof let e be set ; ::_thesis: ( e in F1() implies P1[e,F . (e,0),F . (e,1)] ) assume A18: e in F1() ; ::_thesis: P1[e,F . (e,0),F . (e,1)] then consider b, c being Element of F1() such that A19: P1[e,b,c] and A20: f . e = [b,c] by A6; [e,1] in [:F1(),NAT:] by A18, ZFMISC_1:87; then A21: F . [e,1] = IFEQ (([e,1] `2),0,((f . ([e,1] `1)) `1),((f . ([e,1] `1)) `2)) by A11 .= (f . ([e,1] `1)) `2 by FUNCOP_1:def_8 .= (f . e) `2 .= c by A20, MCART_1:7 ; [e,0] in [:F1(),NAT:] by A18, ZFMISC_1:87; then F . [e,0] = IFEQ (([e,0] `2),0,((f . ([e,0] `1)) `1),((f . ([e,0] `1)) `2)) by A11 .= (f . ([e,0] `1)) `1 by FUNCOP_1:def_8 .= (f . e) `1 .= b by A20, MCART_1:7 ; hence P1[e,F . (e,0),F . (e,1)] by A19, A21; ::_thesis: verum end; then P1[D . x,F . ((D . x),0),F . ((D . x),1)] ; then P1[D . x,D . (x ^ <*0*>),F . ((D . x),1)] by A13; hence P1[D . x,D . (x ^ <*0*>),D . (x ^ <*1*>)] by A13; ::_thesis: verum end; scheme :: BINTREE2:sch 2 DecoratedBinTreeEx1{ F1() -> non empty set , F2() -> Element of F1(), P1[ set , set ], P2[ set , set ] } : ex D being binary DecoratedTree of F1() st ( dom D = {0,1} * & D . {} = F2() & ( for x being Node of D holds ( P1[D . x,D . (x ^ <*0*>)] & P2[D . x,D . (x ^ <*1*>)] ) ) ) provided A1: for a being Element of F1() ex b being Element of F1() st P1[a,b] and A2: for a being Element of F1() ex b being Element of F1() st P2[a,b] proof deffunc H1( set ) -> Element of NAT = 2; defpred S1[ set , set ] means ( ( \$1 `2 = 0 implies P1[\$1 `1 ,\$2] ) & ( \$1 `2 = 1 implies P2[\$1 `1 ,\$2] ) ); A3: for e being set st e in [:F1(),NAT:] holds ex u being set st ( u in F1() & S1[e,u] ) proof let e be set ; ::_thesis: ( e in [:F1(),NAT:] implies ex u being set st ( u in F1() & S1[e,u] ) ) assume e in [:F1(),NAT:] ; ::_thesis: ex u being set st ( u in F1() & S1[e,u] ) then reconsider e1 = e `1 as Element of F1() by MCART_1:10; consider u1 being Element of F1() such that A4: P1[e1,u1] by A1; consider u2 being Element of F1() such that A5: P2[e1,u2] by A2; take u = IFEQ ((e `2),0,u1,u2); ::_thesis: ( u in F1() & S1[e,u] ) thus u in F1() ; ::_thesis: S1[e,u] thus ( e `2 = 0 implies P1[e `1 ,u] ) by A4, FUNCOP_1:def_8; ::_thesis: ( e `2 = 1 implies P2[e `1 ,u] ) thus ( e `2 = 1 implies P2[e `1 ,u] ) by A5, FUNCOP_1:def_8; ::_thesis: verum end; consider F being Function such that A6: ( dom F = [:F1(),NAT:] & rng F c= F1() ) and A7: for e being set st e in [:F1(),NAT:] holds S1[e,F . e] from FUNCT_1:sch_5(A3); reconsider F = F as Function of [:F1(),NAT:],F1() by A6, FUNCT_2:2; consider D being DecoratedTree of F1() such that A8: D . {} = F2() and A9: for d being Element of dom D holds ( succ d = { (d ^ <*k*>) where k is Element of NAT : k < H1(D . d) } & ( for n being Element of NAT st n < H1(D . d) holds D . (d ^ <*n*>) = F . ((D . d),n) ) ) from TREES_2:sch_9(); now__::_thesis:_for_t_being_Element_of_dom_D_st_not_t_in_Leaves_(dom_D)_holds_ succ_t_=_{(t_^_<*0*>),(t_^_<*1*>)} let t be Element of dom D; ::_thesis: ( not t in Leaves (dom D) implies succ t = {(t ^ <*0*>),(t ^ <*1*>)} ) assume not t in Leaves (dom D) ; ::_thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)} { (t ^ <*k*>) where k is Element of NAT : k < 2 } = {(t ^ <*0*>),(t ^ <*1*>)} proof thus { (t ^ <*k*>) where k is Element of NAT : k < 2 } c= {(t ^ <*0*>),(t ^ <*1*>)} :: according to XBOOLE_0:def_10 ::_thesis: {(t ^ <*0*>),(t ^ <*1*>)} c= { (t ^ <*k*>) where k is Element of NAT : k < 2 } proof let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in { (t ^ <*k*>) where k is Element of NAT : k < 2 } or v in {(t ^ <*0*>),(t ^ <*1*>)} ) assume v in { (t ^ <*k*>) where k is Element of NAT : k < 2 } ; ::_thesis: v in {(t ^ <*0*>),(t ^ <*1*>)} then consider k being Element of NAT such that A10: v = t ^ <*k*> and A11: k < 2 ; ( k = 0 or k = 1 ) by A11, NAT_1:23; hence v in {(t ^ <*0*>),(t ^ <*1*>)} by A10, TARSKI:def_2; ::_thesis: verum end; let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in {(t ^ <*0*>),(t ^ <*1*>)} or v in { (t ^ <*k*>) where k is Element of NAT : k < 2 } ) assume v in {(t ^ <*0*>),(t ^ <*1*>)} ; ::_thesis: v in { (t ^ <*k*>) where k is Element of NAT : k < 2 } then ( v = t ^ <*0*> or v = t ^ <*1*> ) by TARSKI:def_2; hence v in { (t ^ <*k*>) where k is Element of NAT : k < 2 } ; ::_thesis: verum end; hence succ t = {(t ^ <*0*>),(t ^ <*1*>)} by A9; ::_thesis: verum end; then dom D is binary by BINTREE1:def_2; then reconsider D = D as binary DecoratedTree of F1() by BINTREE1:def_3; take D ; ::_thesis: ( dom D = {0,1} * & D . {} = F2() & ( for x being Node of D holds ( P1[D . x,D . (x ^ <*0*>)] & P2[D . x,D . (x ^ <*1*>)] ) ) ) now__::_thesis:_for_t_being_Element_of_dom_D_holds_succ_t_=_{(t_^_<*0*>),(t_^_<*1*>)} let t be Element of dom D; ::_thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)} { (t ^ <*k*>) where k is Element of NAT : k < 2 } = {(t ^ <*0*>),(t ^ <*1*>)} proof thus { (t ^ <*k*>) where k is Element of NAT : k < 2 } c= {(t ^ <*0*>),(t ^ <*1*>)} :: according to XBOOLE_0:def_10 ::_thesis: {(t ^ <*0*>),(t ^ <*1*>)} c= { (t ^ <*k*>) where k is Element of NAT : k < 2 } proof let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in { (t ^ <*k*>) where k is Element of NAT : k < 2 } or v in {(t ^ <*0*>),(t ^ <*1*>)} ) assume v in { (t ^ <*k*>) where k is Element of NAT : k < 2 } ; ::_thesis: v in {(t ^ <*0*>),(t ^ <*1*>)} then consider k being Element of NAT such that A12: v = t ^ <*k*> and A13: k < 2 ; ( k = 0 or k = 1 ) by A13, NAT_1:23; hence v in {(t ^ <*0*>),(t ^ <*1*>)} by A12, TARSKI:def_2; ::_thesis: verum end; let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in {(t ^ <*0*>),(t ^ <*1*>)} or v in { (t ^ <*k*>) where k is Element of NAT : k < 2 } ) assume v in {(t ^ <*0*>),(t ^ <*1*>)} ; ::_thesis: v in { (t ^ <*k*>) where k is Element of NAT : k < 2 } then ( v = t ^ <*0*> or v = t ^ <*1*> ) by TARSKI:def_2; hence v in { (t ^ <*k*>) where k is Element of NAT : k < 2 } ; ::_thesis: verum end; hence succ t = {(t ^ <*0*>),(t ^ <*1*>)} by A9; ::_thesis: verum end; hence dom D = {0,1} * by Th8; ::_thesis: ( D . {} = F2() & ( for x being Node of D holds ( P1[D . x,D . (x ^ <*0*>)] & P2[D . x,D . (x ^ <*1*>)] ) ) ) thus D . {} = F2() by A8; ::_thesis: for x being Node of D holds ( P1[D . x,D . (x ^ <*0*>)] & P2[D . x,D . (x ^ <*1*>)] ) let x be Node of D; ::_thesis: ( P1[D . x,D . (x ^ <*0*>)] & P2[D . x,D . (x ^ <*1*>)] ) [(D . x),0] `2 = 0 ; then P1[[(D . x),0] `1 ,F . [(D . x),0]] by A7; then P1[D . x,F . ((D . x),0)] ; hence P1[D . x,D . (x ^ <*0*>)] by A9; ::_thesis: P2[D . x,D . (x ^ <*1*>)] [(D . x),1] `2 = 1 ; then P2[[(D . x),1] `1 ,F . [(D . x),1]] by A7; then P2[D . x,F . ((D . x),1)] ; hence P2[D . x,D . (x ^ <*1*>)] by A9; ::_thesis: verum end; Lm3: for D being non empty set for f being FinSequence of D holds Rev f is FinSequence of D ; definition let T be binary Tree; let n be non empty Nat; func NumberOnLevel (n,T) -> Function of (T -level n),NAT means :Def1: :: BINTREE2:def 1 for t being Element of T st t in T -level n holds for F being Element of n -tuples_on BOOLEAN st F = Rev t holds it . t = (Absval F) + 1; existence ex b1 being Function of (T -level n),NAT st for t being Element of T st t in T -level n holds for F being Element of n -tuples_on BOOLEAN st F = Rev t holds b1 . t = (Absval F) + 1 proof defpred S1[ set , set ] means ex t being Element of T st ( t = \$1 & ( for F being Tuple of n, BOOLEAN st F = Rev t holds \$2 = (Absval F) + 1 ) ); A1: for e being set st e in T -level n holds ex u being set st ( u in NAT & S1[e,u] ) proof let e be set ; ::_thesis: ( e in T -level n implies ex u being set st ( u in NAT & S1[e,u] ) ) assume e in T -level n ; ::_thesis: ex u being set st ( u in NAT & S1[e,u] ) then e in { w where w is Element of T : len w = n } by TREES_2:def_6; then consider t being Element of T such that A2: t = e and A3: len t = n ; len (Rev t) = n by A3, FINSEQ_5:def_3; then reconsider F1 = Rev t as Element of n -tuples_on BOOLEAN by FINSEQ_2:92; take u = (Absval F1) + 1; ::_thesis: ( u in NAT & S1[e,u] ) thus u in NAT ; ::_thesis: S1[e,u] take t ; ::_thesis: ( t = e & ( for F being Tuple of n, BOOLEAN st F = Rev t holds u = (Absval F) + 1 ) ) thus t = e by A2; ::_thesis: for F being Tuple of n, BOOLEAN st F = Rev t holds u = (Absval F) + 1 let F be Tuple of n, BOOLEAN ; ::_thesis: ( F = Rev t implies u = (Absval F) + 1 ) assume F = Rev t ; ::_thesis: u = (Absval F) + 1 hence u = (Absval F) + 1 ; ::_thesis: verum end; consider f being Function such that A4: ( dom f = T -level n & rng f c= NAT ) and A5: for e being set st e in T -level n holds S1[e,f . e] from FUNCT_1:sch_5(A1); reconsider f = f as Function of (T -level n),NAT by A4, FUNCT_2:2; take f ; ::_thesis: for t being Element of T st t in T -level n holds for F being Element of n -tuples_on BOOLEAN st F = Rev t holds f . t = (Absval F) + 1 let t be Element of T; ::_thesis: ( t in T -level n implies for F being Element of n -tuples_on BOOLEAN st F = Rev t holds f . t = (Absval F) + 1 ) assume t in T -level n ; ::_thesis: for F being Element of n -tuples_on BOOLEAN st F = Rev t holds f . t = (Absval F) + 1 then A6: ex t1 being Element of T st ( t1 = t & ( for F being Tuple of n, BOOLEAN st F = Rev t1 holds f . t = (Absval F) + 1 ) ) by A5; let F be Element of n -tuples_on BOOLEAN; ::_thesis: ( F = Rev t implies f . t = (Absval F) + 1 ) assume F = Rev t ; ::_thesis: f . t = (Absval F) + 1 hence f . t = (Absval F) + 1 by A6; ::_thesis: verum end; uniqueness for b1, b2 being Function of (T -level n),NAT st ( for t being Element of T st t in T -level n holds for F being Element of n -tuples_on BOOLEAN st F = Rev t holds b1 . t = (Absval F) + 1 ) & ( for t being Element of T st t in T -level n holds for F being Element of n -tuples_on BOOLEAN st F = Rev t holds b2 . t = (Absval F) + 1 ) holds b1 = b2 proof let f1, f2 be Function of (T -level n),NAT; ::_thesis: ( ( for t being Element of T st t in T -level n holds for F being Element of n -tuples_on BOOLEAN st F = Rev t holds f1 . t = (Absval F) + 1 ) & ( for t being Element of T st t in T -level n holds for F being Element of n -tuples_on BOOLEAN st F = Rev t holds f2 . t = (Absval F) + 1 ) implies f1 = f2 ) assume that A7: for t being Element of T st t in T -level n holds for F being Element of n -tuples_on BOOLEAN st F = Rev t holds f1 . t = (Absval F) + 1 and A8: for t being Element of T st t in T -level n holds for F being Element of n -tuples_on BOOLEAN st F = Rev t holds f2 . t = (Absval F) + 1 ; ::_thesis: f1 = f2 now__::_thesis:_for_x_being_set_st_x_in_T_-level_n_holds_ f1_._x_=_f2_._x let x be set ; ::_thesis: ( x in T -level n implies f1 . x = f2 . x ) assume A9: x in T -level n ; ::_thesis: f1 . x = f2 . x then x in { w where w is Element of T : len w = n } by TREES_2:def_6; then consider t being Element of T such that A10: t = x and A11: len t = n ; len (Rev t) = n by A11, FINSEQ_5:def_3; then reconsider F = Rev t as Element of n -tuples_on BOOLEAN by FINSEQ_2:92; thus f1 . x = (Absval F) + 1 by A7, A9, A10 .= f2 . x by A8, A9, A10 ; ::_thesis: verum end; hence f1 = f2 by FUNCT_2:12; ::_thesis: verum end; end; :: deftheorem Def1 defines NumberOnLevel BINTREE2:def_1_:_ for T being binary Tree for n being non empty Nat for b3 being Function of (T -level n),NAT holds ( b3 = NumberOnLevel (n,T) iff for t being Element of T st t in T -level n holds for F being Element of n -tuples_on BOOLEAN st F = Rev t holds b3 . t = (Absval F) + 1 ); registration let T be binary Tree; let n be non empty Element of NAT ; cluster NumberOnLevel (n,T) -> one-to-one ; coherence NumberOnLevel (n,T) is one-to-one proof now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_(NumberOnLevel_(n,T))_&_x2_in_dom_(NumberOnLevel_(n,T))_&_(NumberOnLevel_(n,T))_._x1_=_(NumberOnLevel_(n,T))_._x2_holds_ x1_=_x2 let x1, x2 be set ; ::_thesis: ( x1 in dom (NumberOnLevel (n,T)) & x2 in dom (NumberOnLevel (n,T)) & (NumberOnLevel (n,T)) . x1 = (NumberOnLevel (n,T)) . x2 implies x1 = x2 ) assume that A1: x1 in dom (NumberOnLevel (n,T)) and A2: x2 in dom (NumberOnLevel (n,T)) and A3: (NumberOnLevel (n,T)) . x1 = (NumberOnLevel (n,T)) . x2 ; ::_thesis: x1 = x2 A4: x1 in T -level n by A1, FUNCT_2:def_1; then x1 in { w where w is Element of T : len w = n } by TREES_2:def_6; then consider t1 being Element of T such that A5: t1 = x1 and A6: len t1 = n ; A7: x2 in T -level n by A2, FUNCT_2:def_1; then x2 in { w where w is Element of T : len w = n } by TREES_2:def_6; then consider t2 being Element of T such that A8: t2 = x2 and A9: len t2 = n ; len (Rev t2) = n by A9, FINSEQ_5:def_3; then reconsider F2 = Rev t2 as Element of n -tuples_on BOOLEAN by FINSEQ_2:92; len (Rev t1) = n by A6, FINSEQ_5:def_3; then reconsider F1 = Rev t1 as Element of n -tuples_on BOOLEAN by FINSEQ_2:92; (Absval F1) + 1 = (NumberOnLevel (n,T)) . x1 by A4, A5, Def1 .= (Absval F2) + 1 by A3, A7, A8, Def1 ; hence x1 = x2 by A5, A8, BINARI_3:2, BINARI_3:3; ::_thesis: verum end; hence NumberOnLevel (n,T) is one-to-one by FUNCT_1:def_4; ::_thesis: verum end; end; begin definition let T be Tree; attrT is full means :Def2: :: BINTREE2:def 2 T = {0,1} * ; end; :: deftheorem Def2 defines full BINTREE2:def_2_:_ for T being Tree holds ( T is full iff T = {0,1} * ); theorem Th9: :: BINTREE2:9 {0,1} * is Tree proof set X = {0,1} * ; A1: now__::_thesis:_for_p_being_FinSequence_of_NAT_st_p_in_{0,1}_*_holds_ ProperPrefixes_p_c=_{0,1}_* let p be FinSequence of NAT ; ::_thesis: ( p in {0,1} * implies ProperPrefixes p c= {0,1} * ) assume A2: p in {0,1} * ; ::_thesis: ProperPrefixes p c= {0,1} * thus ProperPrefixes p c= {0,1} * ::_thesis: verum proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in ProperPrefixes p or y in {0,1} * ) assume y in ProperPrefixes p ; ::_thesis: y in {0,1} * then consider q being FinSequence such that A3: y = q and A4: q is_a_proper_prefix_of p by TREES_1:def_2; q is_a_prefix_of p by A4, XBOOLE_0:def_8; then ex n being Element of NAT st q = p | (Seg n) by TREES_1:def_1; hence y in {0,1} * by A2, A3, Th1; ::_thesis: verum end; end; A5: now__::_thesis:_for_p_being_FinSequence_of_NAT_ for_k,_n_being_Element_of_NAT_st_p_^_<*k*>_in_{0,1}_*_&_n_<=_k_holds_ p_^_<*n*>_in_{0,1}_* let p be FinSequence of NAT ; ::_thesis: for k, n being Element of NAT st p ^ <*k*> in {0,1} * & n <= k holds p ^ <*n*> in {0,1} * let k, n be Element of NAT ; ::_thesis: ( p ^ <*k*> in {0,1} * & n <= k implies p ^ <*n*> in {0,1} * ) assume that A6: p ^ <*k*> in {0,1} * and A7: n <= k ; ::_thesis: p ^ <*n*> in {0,1} * A8: p ^ <*k*> is FinSequence of {0,1} by A6, FINSEQ_1:def_11; then reconsider kk = <*k*> as FinSequence of {0,1} by FINSEQ_1:36; 1 in Seg 1 by FINSEQ_1:3; then 1 in dom <*k*> by FINSEQ_1:38; then kk . 1 in {0,1} by FINSEQ_2:11; then A9: k in {0,1} by FINSEQ_1:40; now__::_thesis:_(_n_=_0_or_n_=_1_) percases ( k = 0 or k = 1 ) by A9, TARSKI:def_2; suppose k = 0 ; ::_thesis: ( n = 0 or n = 1 ) hence ( n = 0 or n = 1 ) by A7; ::_thesis: verum end; supposeA10: k = 1 ; ::_thesis: ( n = 0 or n = 1 ) ( n = 1 or n = 0 ) proof assume n <> 1 ; ::_thesis: n = 0 then n < 0 + 1 by A7, A10, XXREAL_0:1; hence n = 0 by NAT_1:13; ::_thesis: verum end; hence ( n = 0 or n = 1 ) ; ::_thesis: verum end; end; end; then n in {0,1} by TARSKI:def_2; then A11: <*n*> is FinSequence of {0,1} by Lm2; p is FinSequence of {0,1} by A8, FINSEQ_1:36; then p ^ <*n*> is FinSequence of {0,1} by A11, Lm1; hence p ^ <*n*> in {0,1} * by FINSEQ_1:def_11; ::_thesis: verum end; {0,1} * c= NAT * by FINSEQ_1:62; hence {0,1} * is Tree by A1, A5, TREES_1:def_3; ::_thesis: verum end; theorem Th10: :: BINTREE2:10 for T being Tree st T = {0,1} * holds for n being Nat holds 0* n in T -level n proof let T be Tree; ::_thesis: ( T = {0,1} * implies for n being Nat holds 0* n in T -level n ) assume A1: T = {0,1} * ; ::_thesis: for n being Nat holds 0* n in T -level n let n be Nat; ::_thesis: 0* n in T -level n ( len (0* n) = n & 0* n in T ) by A1, BINARI_3:4, CARD_1:def_7; then 0* n in { w where w is Element of T : len w = n } ; hence 0* n in T -level n by TREES_2:def_6; ::_thesis: verum end; theorem Th11: :: BINTREE2:11 for T being Tree st T = {0,1} * holds for n being non empty Element of NAT for y being Element of n -tuples_on BOOLEAN holds y in T -level n proof let T be Tree; ::_thesis: ( T = {0,1} * implies for n being non empty Element of NAT for y being Element of n -tuples_on BOOLEAN holds y in T -level n ) assume A1: T = {0,1} * ; ::_thesis: for n being non empty Element of NAT for y being Element of n -tuples_on BOOLEAN holds y in T -level n let n be non empty Element of NAT ; ::_thesis: for y being Element of n -tuples_on BOOLEAN holds y in T -level n let y be Element of n -tuples_on BOOLEAN; ::_thesis: y in T -level n y in { w where w is Element of T : len w = n } by A1; hence y in T -level n by TREES_2:def_6; ::_thesis: verum end; registration let T be binary Tree; let n be Element of NAT ; clusterT -level n -> finite ; coherence T -level n is finite by TREES_9:46; end; registration cluster non empty Tree-like full -> binary for set ; coherence for b1 being Tree st b1 is full holds b1 is binary proof let T be Tree; ::_thesis: ( T is full implies T is binary ) assume T is full ; ::_thesis: T is binary then T = {0,1} * by Def2; hence T is binary by Th3; ::_thesis: verum end; end; registration cluster non empty Tree-like full for set ; existence ex b1 being Tree st b1 is full proof reconsider T = {0,1} * as Tree by Th9; take T ; ::_thesis: T is full thus T is full by Def2; ::_thesis: verum end; end; theorem Th12: :: BINTREE2:12 for T being full Tree for n being non empty Nat holds Seg (2 to_power n) c= rng (NumberOnLevel (n,T)) proof let T be full Tree; ::_thesis: for n being non empty Nat holds Seg (2 to_power n) c= rng (NumberOnLevel (n,T)) let n be non empty Nat; ::_thesis: Seg (2 to_power n) c= rng (NumberOnLevel (n,T)) let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Seg (2 to_power n) or y in rng (NumberOnLevel (n,T)) ) assume y in Seg (2 to_power n) ; ::_thesis: y in rng (NumberOnLevel (n,T)) then y in { k where k is Element of NAT : ( 1 <= k & k <= 2 to_power n ) } by FINSEQ_1:def_1; then consider k being Element of NAT such that A1: k = y and A2: 1 <= k and A3: k <= 2 to_power n ; A4: k - 1 >= 1 - 1 by A2, XREAL_1:9; set t = Rev (n -BinarySequence (k -' 1)); A5: len (Rev (n -BinarySequence (k -' 1))) = len (n -BinarySequence (k -' 1)) by FINSEQ_5:def_3 .= n by CARD_1:def_7 ; then len (Rev (Rev (n -BinarySequence (k -' 1)))) = n by FINSEQ_5:def_3; then reconsider F = Rev (Rev (n -BinarySequence (k -' 1))) as Element of n -tuples_on BOOLEAN by FINSEQ_2:92; T = {0,1} * by Def2; then Rev (n -BinarySequence (k -' 1)) in T by FINSEQ_1:def_11; then Rev (n -BinarySequence (k -' 1)) in { w where w is Element of T : len w = n } by A5; then A6: Rev (n -BinarySequence (k -' 1)) in T -level n by TREES_2:def_6; then A7: Rev (n -BinarySequence (k -' 1)) in dom (NumberOnLevel (n,T)) by FUNCT_2:def_1; k < (2 to_power n) + 1 by A3, NAT_1:13; then k - 1 < 2 to_power n by XREAL_1:19; then A8: k -' 1 < 2 to_power n by A4, XREAL_0:def_2; (NumberOnLevel (n,T)) . (Rev (n -BinarySequence (k -' 1))) = (Absval F) + 1 by A6, Def1 .= (Absval (n -BinarySequence (k -' 1))) + 1 .= (k -' 1) + 1 by A8, BINARI_3:35 .= (k - 1) + 1 by A4, XREAL_0:def_2 .= y by A1 ; hence y in rng (NumberOnLevel (n,T)) by A7, FUNCT_1:def_3; ::_thesis: verum end; definition let T be full Tree; let n be non empty Nat; func FinSeqLevel (n,T) -> FinSequence of T -level n equals :: BINTREE2:def 3 (NumberOnLevel (n,T)) " ; coherence (NumberOnLevel (n,T)) " is FinSequence of T -level n proof reconsider k = n as non empty Element of NAT by ORDINAL1:def_12; T = {0,1} * by Def2; then A1: not T -level n is empty by Th10; for y being set holds ( y in Seg (2 to_power n) iff ex x being set st ( x in dom (NumberOnLevel (k,T)) & y = (NumberOnLevel (k,T)) . x ) ) proof let y be set ; ::_thesis: ( y in Seg (2 to_power n) iff ex x being set st ( x in dom (NumberOnLevel (k,T)) & y = (NumberOnLevel (k,T)) . x ) ) thus ( y in Seg (2 to_power n) implies ex x being set st ( x in dom (NumberOnLevel (k,T)) & y = (NumberOnLevel (k,T)) . x ) ) ::_thesis: ( ex x being set st ( x in dom (NumberOnLevel (k,T)) & y = (NumberOnLevel (k,T)) . x ) implies y in Seg (2 to_power n) ) proof assume A2: y in Seg (2 to_power n) ; ::_thesis: ex x being set st ( x in dom (NumberOnLevel (k,T)) & y = (NumberOnLevel (k,T)) . x ) take ((NumberOnLevel (n,T)) ") . y ; ::_thesis: ( ((NumberOnLevel (n,T)) ") . y in dom (NumberOnLevel (k,T)) & y = (NumberOnLevel (k,T)) . (((NumberOnLevel (n,T)) ") . y) ) Seg (2 to_power n) c= rng (NumberOnLevel (n,T)) by Th12; hence ( ((NumberOnLevel (n,T)) ") . y in dom (NumberOnLevel (k,T)) & y = (NumberOnLevel (k,T)) . (((NumberOnLevel (n,T)) ") . y) ) by A2, FUNCT_1:32; ::_thesis: verum end; given x being set such that A3: x in dom (NumberOnLevel (k,T)) and A4: y = (NumberOnLevel (k,T)) . x ; ::_thesis: y in Seg (2 to_power n) A5: x in T -level n by A3, FUNCT_2:def_1; then x in { t where t is Element of T : len t = n } by TREES_2:def_6; then consider t being Element of T such that A6: t = x and A7: len t = n ; len (Rev t) = n by A7, FINSEQ_5:def_3; then reconsider F = Rev t as Element of n -tuples_on BOOLEAN by FINSEQ_2:92; Absval F < 2 to_power n by BINARI_3:1; then A8: ( 1 <= (Absval F) + 1 & (Absval F) + 1 <= 2 to_power n ) by NAT_1:11, NAT_1:13; y = (Absval F) + 1 by A4, A5, A6, Def1; hence y in Seg (2 to_power n) by A8, FINSEQ_1:1; ::_thesis: verum end; then rng (NumberOnLevel (n,T)) = Seg (2 to_power n) by FUNCT_1:def_3; then A9: dom ((NumberOnLevel (k,T)) ") = Seg (2 to_power n) by FUNCT_1:33; rng ((NumberOnLevel (k,T)) ") = dom (NumberOnLevel (k,T)) by FUNCT_1:33 .= T -level n by FUNCT_2:def_1 ; then (NumberOnLevel (n,T)) " is Function of (Seg (2 to_power n)),(T -level n) by A9, FUNCT_2:2; hence (NumberOnLevel (n,T)) " is FinSequence of T -level n by A1, FINSEQ_2:25; ::_thesis: verum end; end; :: deftheorem defines FinSeqLevel BINTREE2:def_3_:_ for T being full Tree for n being non empty Nat holds FinSeqLevel (n,T) = (NumberOnLevel (n,T)) " ; registration let T be full Tree; let n be non empty Element of NAT ; cluster FinSeqLevel (n,T) -> one-to-one ; coherence FinSeqLevel (n,T) is one-to-one by FUNCT_1:40; end; theorem Th13: :: BINTREE2:13 for T being full Tree for n being non empty Element of NAT holds (NumberOnLevel (n,T)) . (0* n) = 1 proof let T be full Tree; ::_thesis: for n being non empty Element of NAT holds (NumberOnLevel (n,T)) . (0* n) = 1 let n be non empty Element of NAT ; ::_thesis: (NumberOnLevel (n,T)) . (0* n) = 1 A1: len (Rev (0* n)) = len (0* n) by FINSEQ_5:def_3 .= n by CARD_1:def_7 ; A2: T = {0,1} * by Def2; then 0* n is Element of T by BINARI_3:4; then Rev (0* n) is FinSequence of BOOLEAN by Lm3; then reconsider F = Rev (0* n) as Element of n -tuples_on BOOLEAN by A1, FINSEQ_2:92; 0* n in T -level n by A2, Th10; hence (NumberOnLevel (n,T)) . (0* n) = (Absval F) + 1 by Def1 .= 0 + 1 by BINARI_3:6, BINARI_3:8 .= 1 ; ::_thesis: verum end; theorem Th14: :: BINTREE2:14 for T being full Tree for n being non empty Element of NAT for y being Element of n -tuples_on BOOLEAN st y = 0* n holds (NumberOnLevel (n,T)) . ('not' y) = 2 to_power n proof let T be full Tree; ::_thesis: for n being non empty Element of NAT for y being Element of n -tuples_on BOOLEAN st y = 0* n holds (NumberOnLevel (n,T)) . ('not' y) = 2 to_power n let n be non empty Element of NAT ; ::_thesis: for y being Element of n -tuples_on BOOLEAN st y = 0* n holds (NumberOnLevel (n,T)) . ('not' y) = 2 to_power n let y be Element of n -tuples_on BOOLEAN; ::_thesis: ( y = 0* n implies (NumberOnLevel (n,T)) . ('not' y) = 2 to_power n ) assume A1: y = 0* n ; ::_thesis: (NumberOnLevel (n,T)) . ('not' y) = 2 to_power n then A2: Rev ('not' y) = 'not' y by BINARI_3:9; len (Rev ('not' y)) = len ('not' y) by FINSEQ_5:def_3 .= n by CARD_1:def_7 ; then reconsider F = Rev ('not' y) as Element of n -tuples_on BOOLEAN by FINSEQ_2:92; reconsider ny = 'not' y as Element of n -tuples_on BOOLEAN by FINSEQ_2:131; T = {0,1} * by Def2; then ny in T -level n by Th11; hence (NumberOnLevel (n,T)) . ('not' y) = (Absval F) + 1 by Def1 .= ((2 to_power n) - 1) + 1 by A1, A2, BINARI_3:7 .= 2 to_power n ; ::_thesis: verum end; theorem Th15: :: BINTREE2:15 for T being full Tree for n being non empty Element of NAT holds (FinSeqLevel (n,T)) . 1 = 0* n proof let T be full Tree; ::_thesis: for n being non empty Element of NAT holds (FinSeqLevel (n,T)) . 1 = 0* n let n be non empty Element of NAT ; ::_thesis: (FinSeqLevel (n,T)) . 1 = 0* n T = {0,1} * by Def2; then 0* n in T -level n by Th10; then A1: 0* n in dom (NumberOnLevel (n,T)) by FUNCT_2:def_1; 1 = (NumberOnLevel (n,T)) . (0* n) by Th13; hence (FinSeqLevel (n,T)) . 1 = 0* n by A1, FUNCT_1:32; ::_thesis: verum end; theorem Th16: :: BINTREE2:16 for T being full Tree for n being non empty Element of NAT for y being Element of n -tuples_on BOOLEAN st y = 0* n holds (FinSeqLevel (n,T)) . (2 to_power n) = 'not' y proof let T be full Tree; ::_thesis: for n being non empty Element of NAT for y being Element of n -tuples_on BOOLEAN st y = 0* n holds (FinSeqLevel (n,T)) . (2 to_power n) = 'not' y let n be non empty Element of NAT ; ::_thesis: for y being Element of n -tuples_on BOOLEAN st y = 0* n holds (FinSeqLevel (n,T)) . (2 to_power n) = 'not' y let y be Element of n -tuples_on BOOLEAN; ::_thesis: ( y = 0* n implies (FinSeqLevel (n,T)) . (2 to_power n) = 'not' y ) reconsider ny = 'not' y as Element of n -tuples_on BOOLEAN by FINSEQ_2:131; T = {0,1} * by Def2; then ny in T -level n by Th11; then A1: 'not' y in dom (NumberOnLevel (n,T)) by FUNCT_2:def_1; assume y = 0* n ; ::_thesis: (FinSeqLevel (n,T)) . (2 to_power n) = 'not' y then 2 to_power n = (NumberOnLevel (n,T)) . ('not' y) by Th14; hence (FinSeqLevel (n,T)) . (2 to_power n) = 'not' y by A1, FUNCT_1:32; ::_thesis: verum end; theorem Th17: :: BINTREE2:17 for T being full Tree for n being non empty Element of NAT for i being Element of NAT st i in Seg (2 to_power n) holds (FinSeqLevel (n,T)) . i = Rev (n -BinarySequence (i -' 1)) proof let T be full Tree; ::_thesis: for n being non empty Element of NAT for i being Element of NAT st i in Seg (2 to_power n) holds (FinSeqLevel (n,T)) . i = Rev (n -BinarySequence (i -' 1)) let n be non empty Element of NAT ; ::_thesis: for i being Element of NAT st i in Seg (2 to_power n) holds (FinSeqLevel (n,T)) . i = Rev (n -BinarySequence (i -' 1)) let i be Element of NAT ; ::_thesis: ( i in Seg (2 to_power n) implies (FinSeqLevel (n,T)) . i = Rev (n -BinarySequence (i -' 1)) ) reconsider nB = n -BinarySequence (i -' 1) as Element of n -tuples_on BOOLEAN by FINSEQ_2:131; assume A1: i in Seg (2 to_power n) ; ::_thesis: (FinSeqLevel (n,T)) . i = Rev (n -BinarySequence (i -' 1)) then A2: 1 <= i by FINSEQ_1:1; i <= 2 to_power n by A1, FINSEQ_1:1; then i < (2 to_power n) + 1 by NAT_1:13; then i - 1 < 2 to_power n by XREAL_1:19; then i -' 1 < 2 to_power n by A2, XREAL_1:233; then A3: (Absval nB) + 1 = (i -' 1) + 1 by BINARI_3:35 .= (i - 1) + 1 by A2, XREAL_1:233 .= i ; A4: len (Rev nB) = len nB by FINSEQ_5:def_3 .= n by CARD_1:def_7 ; then reconsider RnB = Rev nB as Element of n -tuples_on BOOLEAN by FINSEQ_2:92; RnB in {0,1} * by FINSEQ_1:def_11; then RnB is Element of T by Def2; then RnB in { t where t is Element of T : len t = n } by A4; then A5: RnB in T -level n by TREES_2:def_6; nB = Rev RnB ; then A6: (NumberOnLevel (n,T)) . RnB = (Absval nB) + 1 by A5, Def1; RnB in dom (NumberOnLevel (n,T)) by A5, FUNCT_2:def_1; hence (FinSeqLevel (n,T)) . i = Rev (n -BinarySequence (i -' 1)) by A6, A3, FUNCT_1:32; ::_thesis: verum end; theorem Th18: :: BINTREE2:18 for T being full Tree for n being Element of NAT holds card (T -level n) = 2 to_power n proof let T be full Tree; ::_thesis: for n being Element of NAT holds card (T -level n) = 2 to_power n defpred S1[ Element of NAT ] means card (T -level \$1) = 2 to_power \$1; A1: T = {0,1} * by Def2; A2: for n being Element of NAT st S1[n] holds S1[n + 1] proof defpred S2[ set , set ] means ex p being FinSequence st ( p = \$1 & \$2 = p ^ <*0*> ); let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) set Tn10 = { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 0 ) } ; set Tn11 = { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 1 ) } ; A3: (0* (n + 1)) . (n + 1) = 0 by FINSEQ_1:4, FUNCOP_1:7; ( len (0* (n + 1)) = n + 1 & 0* (n + 1) in T ) by A1, BINARI_3:4, CARD_1:def_7; then A4: 0* (n + 1) in { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 0 ) } by A3; A5: { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 1 ) } c= T -level (n + 1) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 1 ) } or x in T -level (n + 1) ) assume x in { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 1 ) } ; ::_thesis: x in T -level (n + 1) then consider p being Element of T such that A6: p = x and A7: len p = n + 1 and p . (n + 1) = 1 ; p in { w where w is Element of T : len w = n + 1 } by A7; hence x in T -level (n + 1) by A6, TREES_2:def_6; ::_thesis: verum end; rng <*1*> c= {0,1} proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng <*1*> or z in {0,1} ) assume z in rng <*1*> ; ::_thesis: z in {0,1} then z in {1} by FINSEQ_1:38; then z = 1 by TARSKI:def_1; hence z in {0,1} by TARSKI:def_2; ::_thesis: verum end; then A8: <*1*> is FinSequence of {0,1} by FINSEQ_1:def_4; defpred S3[ set , set ] means ex p being FinSequence st ( p = \$1 & \$2 = p ^ <*1*> ); A9: { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 0 ) } c= T -level (n + 1) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 0 ) } or x in T -level (n + 1) ) assume x in { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 0 ) } ; ::_thesis: x in T -level (n + 1) then consider p being Element of T such that A10: p = x and A11: len p = n + 1 and p . (n + 1) = 0 ; p in { w where w is Element of T : len w = n + 1 } by A11; hence x in T -level (n + 1) by A10, TREES_2:def_6; ::_thesis: verum end; 0* n in {0,1} * by BINARI_3:4; then 0* n is FinSequence of {0,1} by FINSEQ_1:def_11; then (0* n) ^ <*1*> is FinSequence of {0,1} by A8, Lm1; then A12: (0* n) ^ <*1*> in T by A1, FINSEQ_1:def_11; reconsider Tn = T -level n as non empty finite set by A1, Th10; assume A13: card (T -level n) = 2 to_power n ; ::_thesis: S1[n + 1] len (0* n) = n by CARD_1:def_7; then A14: ((0* n) ^ <*1*>) . (n + 1) = 1 by FINSEQ_1:42; len ((0* n) ^ <*1*>) = (len (0* n)) + 1 by FINSEQ_2:16 .= n + 1 by CARD_1:def_7 ; then (0* n) ^ <*1*> in { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 1 ) } by A12, A14; then reconsider Tn10 = { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 0 ) } , Tn11 = { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 1 ) } as non empty finite set by A4, A9, A5; A15: Tn10 \/ Tn11 c= T -level (n + 1) by A9, A5, XBOOLE_1:8; A16: for x being Element of Tn ex y being Element of Tn11 st S3[x,y] proof let x be Element of Tn; ::_thesis: ex y being Element of Tn11 st S3[x,y] x in T -level n ; then x in { w where w is Element of T : len w = n } by TREES_2:def_6; then consider p being Element of T such that A17: p = x and A18: len p = n ; set y = p ^ <*1*>; p ^ <*1*> is FinSequence of {0,1} by A8, Lm1; then A19: p ^ <*1*> in T by A1, FINSEQ_1:def_11; ( len (p ^ <*1*>) = n + 1 & (p ^ <*1*>) . (n + 1) = 1 ) by A18, FINSEQ_1:42, FINSEQ_2:16; then p ^ <*1*> in { t where t is Element of T : ( len t = n + 1 & t . (n + 1) = 1 ) } by A19; then reconsider y = p ^ <*1*> as Element of Tn11 ; take y ; ::_thesis: S3[x,y] take p ; ::_thesis: ( p = x & y = p ^ <*1*> ) thus ( p = x & y = p ^ <*1*> ) by A17; ::_thesis: verum end; consider f1 being Function of Tn,Tn11 such that A20: for x being Element of Tn holds S3[x,f1 . x] from FUNCT_2:sch_3(A16); now__::_thesis:_for_y_being_set_st_y_in_Tn11_holds_ ex_x_being_set_st_ (_x_in_Tn_&_y_=_f1_._x_) let y be set ; ::_thesis: ( y in Tn11 implies ex x being set st ( x in Tn & y = f1 . x ) ) assume y in Tn11 ; ::_thesis: ex x being set st ( x in Tn & y = f1 . x ) then consider t being Element of T such that A21: t = y and A22: len t = n + 1 and A23: t . (n + 1) = 1 ; consider p being FinSequence of BOOLEAN , d being Element of BOOLEAN such that A24: t = p ^ <*d*> by A22, FINSEQ_2:19; reconsider x = p as set ; take x = x; ::_thesis: ( x in Tn & y = f1 . x ) A25: (len p) + 1 = n + 1 by A22, A24, FINSEQ_2:16; p in T by A1, FINSEQ_1:def_11; then A26: p in { w where w is Element of T : len w = n } by A25; hence x in Tn by TREES_2:def_6; ::_thesis: y = f1 . x reconsider x9 = x as Element of Tn by A26, TREES_2:def_6; ex q being FinSequence st ( q = x9 & f1 . x9 = q ^ <*1*> ) by A20; hence y = f1 . x by A21, A23, A24, A25, FINSEQ_1:42; ::_thesis: verum end; then A27: rng f1 = Tn11 by FUNCT_2:10; A28: for x being Element of Tn ex y being Element of Tn10 st S2[x,y] proof let x be Element of Tn; ::_thesis: ex y being Element of Tn10 st S2[x,y] x in T -level n ; then x in { w where w is Element of T : len w = n } by TREES_2:def_6; then consider p being Element of T such that A29: p = x and A30: len p = n ; set y = p ^ <*0*>; rng <*0*> c= {0,1} proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng <*0*> or z in {0,1} ) assume z in rng <*0*> ; ::_thesis: z in {0,1} then z in {0} by FINSEQ_1:38; then z = 0 by TARSKI:def_1; hence z in {0,1} by TARSKI:def_2; ::_thesis: verum end; then <*0*> is FinSequence of {0,1} by FINSEQ_1:def_4; then p ^ <*0*> is FinSequence of {0,1} by Lm1; then A31: p ^ <*0*> in T by A1, FINSEQ_1:def_11; ( len (p ^ <*0*>) = n + 1 & (p ^ <*0*>) . (n + 1) = 0 ) by A30, FINSEQ_1:42, FINSEQ_2:16; then p ^ <*0*> in { t where t is Element of T : ( len t = n + 1 & t . (n + 1) = 0 ) } by A31; then reconsider y = p ^ <*0*> as Element of Tn10 ; take y ; ::_thesis: S2[x,y] take p ; ::_thesis: ( p = x & y = p ^ <*0*> ) thus ( p = x & y = p ^ <*0*> ) by A29; ::_thesis: verum end; consider f0 being Function of Tn,Tn10 such that A32: for x being Element of Tn holds S2[x,f0 . x] from FUNCT_2:sch_3(A28); now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_f1_&_x2_in_dom_f1_&_f1_._x1_=_f1_._x2_holds_ x1_=_x2 let x1, x2 be set ; ::_thesis: ( x1 in dom f1 & x2 in dom f1 & f1 . x1 = f1 . x2 implies x1 = x2 ) assume that A33: ( x1 in dom f1 & x2 in dom f1 ) and A34: f1 . x1 = f1 . x2 ; ::_thesis: x1 = x2 reconsider x19 = x1, x29 = x2 as Element of Tn by A33, FUNCT_2:def_1; ( ex p1 being FinSequence st ( p1 = x19 & f1 . x19 = p1 ^ <*1*> ) & ex p2 being FinSequence st ( p2 = x29 & f1 . x29 = p2 ^ <*1*> ) ) by A20; hence x1 = x2 by A34, FINSEQ_2:17; ::_thesis: verum end; then ( Tn c= dom f1 & f1 is one-to-one ) by FUNCT_1:def_4, FUNCT_2:def_1; then Tn,f1 .: Tn are_equipotent by CARD_1:33; then A35: Tn, rng f1 are_equipotent by RELSET_1:22; A36: T -level (n + 1) c= Tn10 \/ Tn11 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in T -level (n + 1) or x in Tn10 \/ Tn11 ) assume x in T -level (n + 1) ; ::_thesis: x in Tn10 \/ Tn11 then x in { w where w is Element of T : len w = n + 1 } by TREES_2:def_6; then consider p being Element of T such that A37: p = x and A38: len p = n + 1 ; ( x in Tn10 or x in Tn11 ) proof n + 1 in Seg (n + 1) by FINSEQ_1:4; then n + 1 in dom p by A38, FINSEQ_1:def_3; then p . (n + 1) in BOOLEAN by FINSEQ_2:11; then A39: ( p . (n + 1) = 0 or p . (n + 1) = 1 ) by TARSKI:def_2; assume not x in Tn10 ; ::_thesis: x in Tn11 hence x in Tn11 by A37, A38, A39; ::_thesis: verum end; hence x in Tn10 \/ Tn11 by XBOOLE_0:def_3; ::_thesis: verum end; now__::_thesis:_for_y_being_set_st_y_in_Tn10_holds_ ex_x_being_set_st_ (_x_in_Tn_&_y_=_f0_._x_) let y be set ; ::_thesis: ( y in Tn10 implies ex x being set st ( x in Tn & y = f0 . x ) ) assume y in Tn10 ; ::_thesis: ex x being set st ( x in Tn & y = f0 . x ) then consider t being Element of T such that A40: t = y and A41: len t = n + 1 and A42: t . (n + 1) = 0 ; consider p being FinSequence of BOOLEAN , d being Element of BOOLEAN such that A43: t = p ^ <*d*> by A41, FINSEQ_2:19; reconsider x = p as set ; take x = x; ::_thesis: ( x in Tn & y = f0 . x ) A44: (len p) + 1 = n + 1 by A41, A43, FINSEQ_2:16; p in T by A1, FINSEQ_1:def_11; then A45: p in { w where w is Element of T : len w = n } by A44; hence x in Tn by TREES_2:def_6; ::_thesis: y = f0 . x reconsider x9 = x as Element of Tn by A45, TREES_2:def_6; ex q being FinSequence st ( q = x9 & f0 . x9 = q ^ <*0*> ) by A32; hence y = f0 . x by A40, A42, A43, A44, FINSEQ_1:42; ::_thesis: verum end; then A46: rng f0 = Tn10 by FUNCT_2:10; now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_f0_&_x2_in_dom_f0_&_f0_._x1_=_f0_._x2_holds_ x1_=_x2 let x1, x2 be set ; ::_thesis: ( x1 in dom f0 & x2 in dom f0 & f0 . x1 = f0 . x2 implies x1 = x2 ) assume that A47: ( x1 in dom f0 & x2 in dom f0 ) and A48: f0 . x1 = f0 . x2 ; ::_thesis: x1 = x2 reconsider x19 = x1, x29 = x2 as Element of Tn by A47, FUNCT_2:def_1; ( ex p1 being FinSequence st ( p1 = x19 & f0 . x19 = p1 ^ <*0*> ) & ex p2 being FinSequence st ( p2 = x29 & f0 . x29 = p2 ^ <*0*> ) ) by A32; hence x1 = x2 by A48, FINSEQ_2:17; ::_thesis: verum end; then ( Tn c= dom f0 & f0 is one-to-one ) by FUNCT_1:def_4, FUNCT_2:def_1; then Tn,f0 .: Tn are_equipotent by CARD_1:33; then Tn, rng f0 are_equipotent by RELSET_1:22; then A49: card Tn = card Tn10 by A46, CARD_1:5; A50: Tn10 misses Tn11 proof assume Tn10 /\ Tn11 <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction then consider x being set such that A51: x in Tn10 /\ Tn11 by XBOOLE_0:def_1; x in Tn11 by A51, XBOOLE_0:def_4; then A52: ex p2 being Element of T st ( p2 = x & len p2 = n + 1 & p2 . (n + 1) = 1 ) ; x in Tn10 by A51, XBOOLE_0:def_4; then ex p1 being Element of T st ( p1 = x & len p1 = n + 1 & p1 . (n + 1) = 0 ) ; hence contradiction by A52; ::_thesis: verum end; thus 2 to_power (n + 1) = (2 to_power n) * (2 to_power 1) by POWER:27 .= 2 * (2 to_power n) by POWER:25 .= (card Tn) + (card Tn) by A13 .= (card Tn10) + (card Tn11) by A49, A35, A27, CARD_1:5 .= card (Tn10 \/ Tn11) by A50, CARD_2:40 .= card (T -level (n + 1)) by A15, A36, XBOOLE_0:def_10 ; ::_thesis: verum end; card (T -level 0) = card {{}} by TREES_9:44 .= 1 by CARD_1:30 .= 2 to_power 0 by POWER:24 ; then A53: S1[ 0 ] ; thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A53, A2); ::_thesis: verum end; theorem Th19: :: BINTREE2:19 for T being full Tree for n being non empty Element of NAT holds len (FinSeqLevel (n,T)) = 2 to_power n proof let T be full Tree; ::_thesis: for n being non empty Element of NAT holds len (FinSeqLevel (n,T)) = 2 to_power n let n be non empty Element of NAT ; ::_thesis: len (FinSeqLevel (n,T)) = 2 to_power n rng (FinSeqLevel (n,T)) = dom (NumberOnLevel (n,T)) by FUNCT_1:33 .= T -level n by FUNCT_2:def_1 ; then A1: dom (FinSeqLevel (n,T)),T -level n are_equipotent by WELLORD2:def_4; card (Seg (len (FinSeqLevel (n,T)))) = card (dom (FinSeqLevel (n,T))) by FINSEQ_1:def_3 .= card (T -level n) by A1, CARD_1:5 .= 2 to_power n by Th18 ; hence len (FinSeqLevel (n,T)) = 2 to_power n by FINSEQ_1:57; ::_thesis: verum end; theorem Th20: :: BINTREE2:20 for T being full Tree for n being non empty Element of NAT holds dom (FinSeqLevel (n,T)) = Seg (2 to_power n) proof let T be full Tree; ::_thesis: for n being non empty Element of NAT holds dom (FinSeqLevel (n,T)) = Seg (2 to_power n) let n be non empty Element of NAT ; ::_thesis: dom (FinSeqLevel (n,T)) = Seg (2 to_power n) thus dom (FinSeqLevel (n,T)) = Seg (len (FinSeqLevel (n,T))) by FINSEQ_1:def_3 .= Seg (2 to_power n) by Th19 ; ::_thesis: verum end; theorem :: BINTREE2:21 for T being full Tree for n being non empty Element of NAT holds rng (FinSeqLevel (n,T)) = T -level n proof let T be full Tree; ::_thesis: for n being non empty Element of NAT holds rng (FinSeqLevel (n,T)) = T -level n let n be non empty Element of NAT ; ::_thesis: rng (FinSeqLevel (n,T)) = T -level n reconsider Tln = T -level n as finite set ; T = {0,1} * by Def2; then not T -level n is empty by Th10; then reconsider p = FinSeqLevel (n,T) as Function of (dom (FinSeqLevel (n,T))),(T -level n) by FINSEQ_2:26; reconsider dp = dom p as finite set ; card dp = card (Seg (2 to_power n)) by Th20 .= 2 to_power n by FINSEQ_1:57 .= card Tln by Th18 ; hence rng (FinSeqLevel (n,T)) = T -level n by FINSEQ_4:63; ::_thesis: verum end; theorem :: BINTREE2:22 for T being full Tree holds (FinSeqLevel (1,T)) . 1 = <*0*> proof let T be full Tree; ::_thesis: (FinSeqLevel (1,T)) . 1 = <*0*> thus (FinSeqLevel (1,T)) . 1 = 0* 1 by Th15 .= <*0*> by FINSEQ_2:59 ; ::_thesis: verum end; theorem :: BINTREE2:23 for T being full Tree holds (FinSeqLevel (1,T)) . 2 = <*1*> proof let T be full Tree; ::_thesis: (FinSeqLevel (1,T)) . 2 = <*1*> A1: 0* 1 = <*FALSE*> by FINSEQ_2:59; reconsider t = <*FALSE*> as Element of 1 -tuples_on BOOLEAN by FINSEQ_2:131; thus (FinSeqLevel (1,T)) . 2 = (FinSeqLevel (1,T)) . (2 to_power 1) by POWER:25 .= 'not' t by A1, Th16 .= <*1*> by BINARI_3:14 ; ::_thesis: verum end; theorem :: BINTREE2:24 for T being full Tree for n, i being non empty Element of NAT st i <= 2 to_power (n + 1) holds for F being Element of n -tuples_on BOOLEAN st F = (FinSeqLevel (n,T)) . ((i + 1) div 2) holds (FinSeqLevel ((n + 1),T)) . i = F ^ <*((i + 1) mod 2)*> proof let T be full Tree; ::_thesis: for n, i being non empty Element of NAT st i <= 2 to_power (n + 1) holds for F being Element of n -tuples_on BOOLEAN st F = (FinSeqLevel (n,T)) . ((i + 1) div 2) holds (FinSeqLevel ((n + 1),T)) . i = F ^ <*((i + 1) mod 2)*> let n, i be non empty Element of NAT ; ::_thesis: ( i <= 2 to_power (n + 1) implies for F being Element of n -tuples_on BOOLEAN st F = (FinSeqLevel (n,T)) . ((i + 1) div 2) holds (FinSeqLevel ((n + 1),T)) . i = F ^ <*((i + 1) mod 2)*> ) assume A1: i <= 2 to_power (n + 1) ; ::_thesis: for F being Element of n -tuples_on BOOLEAN st F = (FinSeqLevel (n,T)) . ((i + 1) div 2) holds (FinSeqLevel ((n + 1),T)) . i = F ^ <*((i + 1) mod 2)*> A2: now__::_thesis:_(i_+_1)_mod_2_=_(i_-'_1)_mod_2 percases ( i -' 1 is odd or i -' 1 is even ) ; suppose i -' 1 is odd ; ::_thesis: (i + 1) mod 2 = (i -' 1) mod 2 then A3: (i -' 1) mod 2 = 1 by NAT_2:22; then ((i -' 1) + ((1 + 1) * 1)) mod 2 = 1 by NAT_D:21; then (((i -' 1) + 1) + 1) mod 2 = 1 ; hence (i + 1) mod 2 = (i -' 1) mod 2 by A3, NAT_1:14, XREAL_1:235; ::_thesis: verum end; suppose i -' 1 is even ; ::_thesis: (i + 1) mod 2 = (i -' 1) mod 2 then A4: (i -' 1) mod 2 = 0 by NAT_2:21; then ((i -' 1) + ((1 + 1) * 1)) mod 2 = 0 by NAT_D:21; then (((i -' 1) + 1) + 1) mod 2 = 0 ; hence (i + 1) mod 2 = (i -' 1) mod 2 by A4, NAT_1:14, XREAL_1:235; ::_thesis: verum end; end; end; let F be Element of n -tuples_on BOOLEAN; ::_thesis: ( F = (FinSeqLevel (n,T)) . ((i + 1) div 2) implies (FinSeqLevel ((n + 1),T)) . i = F ^ <*((i + 1) mod 2)*> ) assume A5: F = (FinSeqLevel (n,T)) . ((i + 1) div 2) ; ::_thesis: (FinSeqLevel ((n + 1),T)) . i = F ^ <*((i + 1) mod 2)*> A6: 1 <= i by NAT_1:14; then 1 + 1 <= i + 1 by XREAL_1:6; then A7: 1 <= (i + 1) div 2 by NAT_2:13; 2 to_power (n + 1) = (2 to_power n) * (2 to_power 1) by POWER:27 .= 2 * (2 to_power n) by POWER:25 ; then (i + 1) div 2 <= 2 to_power n by A1, NAT_2:25; then A8: (i + 1) div 2 in Seg (2 to_power n) by A7, FINSEQ_1:1; i + 1 >= 1 + 1 by A6, XREAL_1:6; then A9: 1 <= (i + 1) div 2 by NAT_2:13; A10: (i -' 1) div 2 = (((i -' 1) div 2) + 1) - 1 .= (((i -' 1) + (1 + 1)) div 2) - 1 by NAT_2:14 .= ((((i -' 1) + 1) + 1) div 2) - 1 .= ((i + 1) div 2) - 1 by NAT_1:14, XREAL_1:235 .= ((i + 1) div 2) -' 1 by A9, XREAL_1:233 ; i in Seg (2 to_power (n + 1)) by A1, A6, FINSEQ_1:1; hence (FinSeqLevel ((n + 1),T)) . i = Rev ((n + 1) -BinarySequence (i -' 1)) by Th17 .= Rev (<*((i -' 1) mod 2)*> ^ (n -BinarySequence ((i -' 1) div 2))) by BINARI_3:34 .= (Rev (n -BinarySequence (((i + 1) div 2) -' 1))) ^ <*((i + 1) mod 2)*> by A2, A10, FINSEQ_6:24 .= F ^ <*((i + 1) mod 2)*> by A5, A8, Th17 ; ::_thesis: verum end;