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

;

definition

let T be binary Tree;

:: original: Element

redefine mode Element of T -> FinSequence of BOOLEAN ;

coherence

for b_{1} being Element of T holds b_{1} is FinSequence of BOOLEAN
by Th2;

end;
:: original: Element

redefine mode Element of T -> FinSequence of BOOLEAN ;

coherence

for b

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

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 = {}

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

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

( 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_{1}() -> non empty set , F_{2}() -> Element of F_{1}(), P_{1}[ object , object , object ] } :

DecoratedBinTreeEx{ F

ex D being binary DecoratedTree of F_{1}() st

( dom D = {0,1} * & D . {} = F_{2}() & ( for x being Node of D holds P_{1}[D . x,D . (x ^ <*0*>),D . (x ^ <*1*>)] ) )

provided
( dom D = {0,1} * & D . {} = F

proof end;

scheme :: BINTREE2:sch 2

DecoratedBinTreeEx1{ F_{1}() -> non empty set , F_{2}() -> Element of F_{1}(), P_{1}[ object , object ], P_{2}[ object , object ] } :

DecoratedBinTreeEx1{ F

ex D being binary DecoratedTree of F_{1}() st

( dom D = {0,1} * & D . {} = F_{2}() & ( for x being Node of D holds

( P_{1}[D . x,D . (x ^ <*0*>)] & P_{2}[D . x,D . (x ^ <*1*>)] ) ) )

provided( dom D = {0,1} * & D . {} = F

( P

A1:
for a being Element of F_{1}() ex b being Element of F_{1}() st P_{1}[a,b]
and

A2: for a being Element of F_{1}() ex b being Element of F_{1}() st P_{2}[a,b]

A2: for a being Element of F

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;

ex b_{1} 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_{1} . t = (Absval F) + 1

for b_{1}, b_{2} 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_{1} . 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_{2} . t = (Absval F) + 1 ) holds

b_{1} = b_{2}

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

ex b

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

proof end;

uniqueness for b

for F being Element of n -tuples_on BOOLEAN st F = Rev t holds

b

for F being Element of n -tuples_on BOOLEAN st F = Rev t holds

b

b

proof end;

:: deftheorem Def1 defines NumberOnLevel BINTREE2:def 1 :

for T being binary Tree

for n being non zero Nat

for b_{3} being Function of (T -level n),NAT holds

( b_{3} = 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_{3} . t = (Absval F) + 1 );

for T being binary Tree

for n being non zero Nat

for b

( b

for F being Element of n -tuples_on BOOLEAN st F = Rev t holds

b

registration
end;

:: deftheorem Def2 defines full BINTREE2:def 2 :

for T being Tree holds

( T is full iff T = {0,1} * );

for T being Tree holds

( T is full iff T = {0,1} * );

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

for n being non zero Nat

for y being Element of n -tuples_on BOOLEAN holds y in T -level n

proof 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))

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;

(NumberOnLevel (n,T)) " is FinSequence of T -level n

end;
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)) " ;

(NumberOnLevel (n,T)) " is FinSequence of T -level n

proof 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)) " ;

for T being full Tree

for n being non zero Nat holds FinSeqLevel (n,T) = (NumberOnLevel (n,T)) " ;

registration
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

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

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

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 :: 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)*>

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;