:: Full Trees
:: by Robert Milewski
::
:: Received February 25, 1998
:: Copyright (c) 1998-2012 Association of Mizar Users


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 *
proofend;

theorem Th2: :: BINTREE2:2
for T being binary Tree
for t being Element of T holds t is FinSequence of BOOLEAN
proofend;

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

theorem Th4: :: BINTREE2:4
for T being Tree st T = {0,1} * holds
Leaves T = {}
proofend;

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

theorem :: BINTREE2:6
for T being Tree st ( for t being Element of T holds succ t = {(t ^ <*0*>),(t ^ <*1*>)} ) holds
Leaves T = {}
proofend;

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

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*>)} )
proofend;

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} * &amp; D . {} = F2() &amp; ( 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]
proofend;

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} * &amp; D . {} = F2() &amp; ( for x being Node of D holds
( P1[D . x,D . (x ^ <*0*>)] &amp; 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]
proofend;

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
proofend;
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 ) &amp; ( 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
proofend;
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
proofend;
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
proofend;

theorem Th10: :: BINTREE2:10
for T being Tree st T = {0,1} * holds
for n being Nat holds 0* n in T -level n
proofend;

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

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
proofend;
end;

registration
cluster non empty Tree-like full for set ;
existence
 ex b1 being Tree st b1 is full
proofend;
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))
proofend;

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

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

theorem Th15: :: BINTREE2:15
for T being full Tree
for n being non empty Element of NAT holds (FinSeqLevel (n,T)) . 1 = 0* n
proofend;

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

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))
proofend;

theorem Th18: :: BINTREE2:18
for T being full Tree
for n being Element of NAT holds card (T -level n) = 2 to_power n
proofend;

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

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)
proofend;

theorem :: BINTREE2:21
for T being full Tree
for n being non empty Element of NAT holds rng (FinSeqLevel (n,T)) = T -level n
proofend;

theorem :: BINTREE2:22
for T being full Tree holds (FinSeqLevel (1,T)) . 1 = <*0*>
proofend;

theorem :: BINTREE2:23
for T being full Tree holds (FinSeqLevel (1,T)) . 2 = <*1*>
proofend;

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)*>
proofend;