:: BINTREE2 semantic presentation

theorem Th1: :: BINTREE2:1

for b₁ being set
for b₂ being FinSequence
for b₃ being Nat st b₂ in b₁ * holds
b₂ | (Seg b₃) in b₁ *

proof end;

theorem Th2: :: BINTREE2:2

for b₁ being binary Tree
for b₂ being Element of b₁ holds b₂ is FinSequence of BOOLEAN

proof end;

definition

let c₁ be binary Tree;
redefine mode Element as Element of c₁ -> FinSequence of BOOLEAN ;
coherence by Th2;

end;

theorem Th3: :: BINTREE2:3

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

proof end;

theorem Th4: :: BINTREE2:4

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

proof end;

theorem Th5: :: BINTREE2:5

for b₁ being binary Tree
for b₂ being Nat
for b₃ being Element of b₁ st b₃ in b₁ -level b₂ holds
b₃ is Tuple of b₂,BOOLEAN

proof end;

theorem Th6: :: BINTREE2:6

for b₁ being Tree st ( for b₂ being Element of b₁ holds succ b₂ = {(b₂ ^ <*0*>),(b₂ ^ <*1*>)} ) holds
Leaves b₁ = {}

proof end;

theorem Th7: :: BINTREE2:7

for b₁ being Tree st ( for b₂ being Element of b₁ holds succ b₂ = {(b₂ ^ <*0*>),(b₂ ^ <*1*>)} ) holds
b₁ is binary

proof end;

theorem Th8: :: BINTREE2:8

for b₁ being Tree holds
( b₁ = {0,1} * iff for b₂ being Element of b₁ holds succ b₂ = {(b₂ ^ <*0*>),(b₂ ^ <*1*>)} )

proof end;

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

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

provided

E7: for b₁ being Element of F₁() ex b₂, b₃ being Element of F₁() st P₁[b₁,b₂,b₃]

proof end;

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

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

provided

E7: for b₁ being Element of F₁() ex b₂ being Element of F₁() st P₁[b₁,b₂] and
E8: for b₁ being Element of F₁() ex b₂ being Element of F₁() st P₂[b₁,b₂]

proof end;

Lemma7: for b₁ being non empty set
for b₂ being FinSequence of b₁ holds Rev b₂ is FinSequence of b₁
;

definition

let c₁ be binary Tree;
let c₂ be non empty Nat;
func NumberOnLevel c₂,c₁ -> Function of a₁ -level a₂, NAT means :Def1: :: BINTREE2:def 1
for b₁ being Element of a₁ st b₁ in a₁ -level a₂ holds
for b₂ being Tuple of a₂,BOOLEAN st b₂ = Rev b₁ holds
a₃ . b₁ = (Absval b₂) + 1;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines NumberOnLevel BINTREE2:def 1 :

registration

let c₁ be binary Tree;
let c₂ be non empty Nat;
cluster NumberOnLevel a₂,a₁ -> one-to-one ;
coherence

proof end;

end;

definition

let c₁ be Tree;
attr a₁ is full means :Def2: :: BINTREE2:def 2
a₁ = {0,1} * ;

end;

:: deftheorem Def2 defines full BINTREE2:def 2 :

theorem Th9: :: BINTREE2:9

{0,1} * is Tree

proof end;

theorem Th10: :: BINTREE2:10

for b₁ being Tree st b₁ = {0,1} * holds
for b₂ being Nat holds 0* b₂ in b₁ -level b₂

proof end;

theorem Th11: :: BINTREE2:11

for b₁ being Tree st b₁ = {0,1} * holds
for b₂ being non empty Nat
for b₃ being Tuple of b₂,BOOLEAN holds b₃ in b₁ -level b₂

proof end;

registration

let c₁ be binary Tree;
let c₂ be Nat;
cluster a₁ -level a₂ -> finite ;
coherence by QC_LANG4:19;

end;

registration

cluster full -> binary set ;
coherence

proof end;

end;

registration

cluster binary full set ;
existence

proof end;

end;

theorem Th12: :: BINTREE2:12

for b₁ being full Tree
for b₂ being non empty Nat holds Seg (2 to_power b₂) c= rng (NumberOnLevel b₂,b₁)

proof end;

definition

let c₁ be full Tree;
let c₂ be non empty Nat;
func FinSeqLevel c₂,c₁ -> FinSequence of a₁ -level a₂ equals :: BINTREE2:def 3
(NumberOnLevel a₂,a₁) " ;
coherence

proof end;

end;

:: deftheorem Def3 defines FinSeqLevel BINTREE2:def 3 :

registration

let c₁ be full Tree;
let c₂ be non empty Nat;
cluster FinSeqLevel a₂,a₁ -> one-to-one ;
coherence by FUNCT_1:62;

end;

theorem Th13: :: BINTREE2:13

for b₁ being full Tree
for b₂ being non empty Nat holds (NumberOnLevel b₂,b₁) . (0* b₂) = 1

proof end;

theorem Th14: :: BINTREE2:14

for b₁ being full Tree
for b₂ being non empty Nat
for b₃ being Tuple of b₂,BOOLEAN st b₃ = 0* b₂ holds
(NumberOnLevel b₂,b₁) . ('not' b₃) = 2 to_power b₂

proof end;

theorem Th15: :: BINTREE2:15

for b₁ being full Tree
for b₂ being non empty Nat holds (FinSeqLevel b₂,b₁) . 1 = 0* b₂

proof end;

theorem Th16: :: BINTREE2:16

for b₁ being full Tree
for b₂ being non empty Nat
for b₃ being Tuple of b₂,BOOLEAN st b₃ = 0* b₂ holds
(FinSeqLevel b₂,b₁) . (2 to_power b₂) = 'not' b₃

proof end;

theorem Th17: :: BINTREE2:17

for b₁ being full Tree
for b₂ being non empty Nat
for b₃ being Nat st b₃ in Seg (2 to_power b₂) holds
(FinSeqLevel b₂,b₁) . b₃ = Rev (b₂ -BinarySequence (b₃ -' 1))

proof end;

theorem Th18: :: BINTREE2:18

for b₁ being full Tree
for b₂ being Nat holds Card (b₁ -level b₂) = 2 to_power b₂

proof end;

theorem Th19: :: BINTREE2:19

for b₁ being full Tree
for b₂ being non empty Nat holds len (FinSeqLevel b₂,b₁) = 2 to_power b₂

proof end;

theorem Th20: :: BINTREE2:20

for b₁ being full Tree
for b₂ being non empty Nat holds dom (FinSeqLevel b₂,b₁) = Seg (2 to_power b₂)

proof end;

theorem Th21: :: BINTREE2:21

for b₁ being full Tree
for b₂ being non empty Nat holds rng (FinSeqLevel b₂,b₁) = b₁ -level b₂

proof end;

theorem Th22: :: BINTREE2:22

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

proof end;

theorem Th23: :: BINTREE2:23

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

proof end;

theorem Th24: :: BINTREE2:24

for b₁ being full Tree
for b₂, b₃ being non empty Nat st b₃ <= 2 to_power (b₂ + 1) holds
for b₄ being Tuple of b₂,BOOLEAN st b₄ = (FinSeqLevel b₂,b₁) . ((b₃ + 1) div 2) holds
(FinSeqLevel (b₂ + 1),b₁) . b₃ = b₄ ^ <*((b₃ + 1) mod 2)*>

proof end;