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

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 Nat st p in D * holds
p | (Seg n) in D *

proof end;

theorem Th2: :: BINTREE2:2

for T being binary Tree
for t being Element of T holds t is FinSequence of BOOLEAN

proof end;

definition

let T be binary Tree;
:: original: Element
redefine mode Element of T -> FinSequence of BOOLEAN ;
coherence
for b₁ being Element of T holds b₁ is FinSequence of BOOLEAN by Th2;

end;

theorem Th3: :: BINTREE2:3

for T being Tree st T = {0,1} * holds
T is binary

proof end;

theorem Th4: :: BINTREE2:4

for T being Tree st T = {0,1} * holds
Leaves T = {}

proof end;

theorem :: BINTREE2:5

for T being binary Tree
for n being Nat
for t being Element of T st t in T -level n holds
t is Element of n -tuples_on BOOLEAN

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

scheme :: BINTREE2:sch 1
DecoratedBinTreeEx{ F₁() -> non empty set , F₂() -> Element of F₁(), P₁[ object , object , object ] } :

ex D being binary DecoratedTree of F₁() st
( dom D = {0,1} * & D . {} = F₂() & ( for x being Node of D holds P₁[D . x,D . (x ^ <*0*>),D . (x ^ <*1*>)] ) )

provided

A1: for a being Element of F₁() ex b, c being Element of F₁() st P₁[a,b,c]

proof end;

scheme :: BINTREE2:sch 2
DecoratedBinTreeEx1{ F₁() -> non empty set , F₂() -> Element of F₁(), P₁[ object , object ], P₂[ object , object ] } :

ex D being binary DecoratedTree of F₁() st
( dom D = {0,1} * & D . {} = F₂() & ( for x being Node of D holds
( P₁[D . x,D . (x ^ <*0*>)] & P₂[D . x,D . (x ^ <*1*>)] ) ) )

provided

A1: for a being Element of F₁() ex b being Element of F₁() st P₁[a,b] and
A2: for a being Element of F₁() ex b being Element of F₁() st P₂[a,b]

proof 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 zero 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 b₁ 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
b₁ . t = (Absval F) + 1

proof end;

uniqueness
for b₁, b₂ 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
b₁ . 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
b₂ . t = (Absval F) + 1 ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines NumberOnLevel BINTREE2:def 1 :
for T being binary Tree
for n being non zero Nat
for b₃ being Function of (T -level n),NAT holds
( b₃ = 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
b₃ . t = (Absval F) + 1 );

registration

let T be binary Tree;
let n be non zero Nat;

cluster NumberOnLevel (n,T) -> one-to-one ;

coherence
NumberOnLevel (n,T) is one-to-one

proof end;

end;

definition

let T be Tree;

attr T 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 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 end;

theorem Th11: :: BINTREE2:11

for T being Tree st T = {0,1} * holds
for n being non zero Nat
for y being Element of n -tuples_on BOOLEAN holds y in T -level n

proof end;

registration

let T be binary Tree;
let n be Nat;

cluster T -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 b₁ being Tree st b₁ is full holds
b₁ is binary by Th3;

end;

registration

cluster non empty Tree-like full for set ;

existence
ex b₁ being Tree st b₁ is full by Th9, Def2;

end;

theorem Th12: :: BINTREE2:12

for T being full Tree
for n being non zero Nat holds Seg (2 to_power n) c= rng (NumberOnLevel (n,T))

proof end;

definition

let T be full Tree;
let n be non zero 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 end;

end;

:: deftheorem defines FinSeqLevel BINTREE2:def 3 :
for T being full Tree
for n being non zero Nat holds FinSeqLevel (n,T) = (NumberOnLevel (n,T)) " ;

registration

let T be full Tree;
let n be non zero 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 zero Nat holds (NumberOnLevel (n,T)) . (0* n) = 1

proof end;

theorem Th14: :: BINTREE2:14

for T being full Tree
for n being non zero 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 end;

theorem Th15: :: BINTREE2:15

for T being full Tree
for n being non zero Nat holds (FinSeqLevel (n,T)) . 1 = 0* n

proof end;

theorem Th16: :: BINTREE2:16

for T being full Tree
for n being non zero 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 end;

theorem Th17: :: BINTREE2:17

for T being full Tree
for n being non zero Nat
for i being Nat st i in Seg (2 to_power n) holds
(FinSeqLevel (n,T)) . i = Rev (n -BinarySequence (i -' 1))

proof end;

theorem Th18: :: BINTREE2:18

for T being full Tree
for n being Nat holds card (T -level n) = 2 to_power n

proof end;

theorem Th19: :: BINTREE2:19

for T being full Tree
for n being non zero Nat holds len (FinSeqLevel (n,T)) = 2 to_power n

proof end;

theorem Th20: :: BINTREE2:20

for T being full Tree
for n being non zero Nat holds dom (FinSeqLevel (n,T)) = Seg (2 to_power n)

proof end;

theorem :: BINTREE2:21

for T being full Tree
for n being non zero Nat holds rng (FinSeqLevel (n,T)) = T -level n

proof end;

theorem :: BINTREE2:22

for T being full Tree holds (FinSeqLevel (1,T)) . 1 = <*0*>

proof end;

theorem :: BINTREE2:23

for T being full Tree holds (FinSeqLevel (1,T)) . 2 = <*1*>

proof end;

theorem :: BINTREE2:24

for T being full Tree
for n, i being non zero 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 end;