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