:: BINTREE2 semantic presentation

REAL is set

bool REAL is non empty set

bool NAT is non empty set
bool NAT is non empty set
RAT is set
INT is set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set
is non empty set
is non empty set
bool is non empty set
BOOLEAN is non empty set

{0,1} is non empty finite set

{{},1} is non empty finite set
K457() is set
bool K457() is non empty set
[:1,1:] is non empty set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty set
bool [:[:1,1:],1:] is non empty set
[:[:1,1:],REAL:] is set
bool [:[:1,1:],REAL:] is non empty set

[:2,2:] is non empty set
[:[:2,2:],REAL:] is set
bool [:[:2,2:],REAL:] is non empty set
TOP-REAL 2 is V201() L15()
the U1 of () is set

Seg 1 is non empty finite 1 -element Element of bool NAT

is non empty finite V38() set
T is set

T is non empty set
n is Element of T

T is set

T is non empty Tree-like finite-order V95() binary set

proj2 (i ^ <*F*>) is finite set
{ (i ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT : i ^ <*b1*> in T } is set

succ dp is finite Element of bool T
bool T is non empty set
Leaves T is Element of bool T
bool is non empty set

{(),(i ^ <*1*>)} is non empty finite V38() Element of bool ()
bool () is non empty set
{0,1} is non empty finite Element of bool NAT
{F} is non empty finite Element of bool NAT
Tn10 is set

() \/ () is finite set

T is non empty Tree-like finite-order V95() binary set
n is Element of T
{0,1} is non empty finite Element of bool NAT
{0,1} * is non empty functional FinSequence-membered FinSequenceSet of {0,1}
T is non empty Tree-like set

Leaves T is Element of bool T
bool T is non empty set
{ (n ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT : n ^ <*b1*> in T } is set
bool is non empty set

{(),(n ^ <*1*>)} is non empty finite V38() Element of bool ()
bool () is non empty set
i is set

Seg ((len n) + 1) is non empty finite (len n) + 1 -element Element of bool NAT

Seg (len dp) is finite len dp -element Element of bool NAT
dom dp is finite Element of bool NAT
dp /. ((len n) + 1) is Element of {0,1}
(n ^ <*F*>) . ((len n) + 1) is set
i is set

F is set
{1} is non empty finite Element of bool NAT

F is set
is non empty finite V38() Element of bool NAT
succ n is Element of bool T
is non empty finite V38() Element of bool NAT
T is set
T is non empty Tree-like set
Leaves T is Element of bool T
bool T is non empty set
n is set

T is non empty Tree-like finite-order V95() binary set

T -level n is Level of T

{ } is set

{ } is set

bool is non empty set

T is non empty Tree-like set
Leaves T is Element of bool T
bool T is non empty set
n is set

succ i is Element of bool T

{(),(i ^ <*1*>)} is non empty finite V38() Element of bool ()
bool () is non empty set
T is non empty Tree-like set
Leaves T is Element of bool T
bool T is non empty set

succ n is Element of bool T

{(),(n ^ <*1*>)} is non empty finite V38() Element of bool ()
bool () is non empty set
T is non empty Tree-like set

succ n is Element of bool T
bool T is non empty set

{(),(n ^ <*1*>)} is non empty finite V38() Element of bool ()
bool () is non empty set
Leaves T is Element of bool T
n is set
n is set

F is Element of {0,1}

succ dp is Element of bool T
bool T is non empty set

{(dp ^ ),(dp ^ <*1*>)} is non empty finite V38() Element of bool ()
bool () is non empty set

[:NAT,{0,1}:] is non empty set
F1() is non empty set
F2() is Element of F1()
[:F1(),F1():] is non empty set
T is set
n is Element of F1()
i is Element of F1()
[n,i] is V13() Element of [:F1(),F1():]
{n,i} is non empty finite set
{n} is non empty finite set
{{n,i},{n}} is non empty finite V38() set
F is V13() Element of [:F1(),F1():]

proj1 T is set
proj2 T is set
[:F1(),NAT:] is non empty set
n is set
n `2 is set
n `1 is set
T . (n `1) is set
(T . (n `1)) `1 is set
(T . (n `1)) `2 is set
IFEQ ((n `2),0,((T . (n `1)) `1),((T . (n `1)) `2)) is set
[:[:F1(),NAT:],F1():] is non empty set
bool [:[:F1(),NAT:],F1():] is non empty set
n is Relation-like [:F1(),NAT:] -defined F1() -valued Function-like V29([:F1(),NAT:],F1()) Element of bool [:[:F1(),NAT:],F1():]

i . {} is set
proj1 i is non empty Tree-like set

Leaves () is Element of bool ()
bool () is non empty set
{ (F ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT : not 2 <= b1 } is set

{(),(F ^ <*1*>)} is non empty finite V38() Element of bool ()
bool () is non empty set
dp is set

dp is set
succ F is Element of bool ()

proj1 F is non empty Tree-like set
F . {} is set

{ (dp ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT : not 2 <= b1 } is set

{(dp ^ ),(dp ^ <*1*>)} is non empty finite V38() Element of bool ()
Tn10 is set

Tn10 is set
succ dp is Element of bool ()
bool () is non empty set

F . dp is Element of F1()

F . (dp ^ ) is set

F . (dp ^ <*1*>) is set
Tn10 is set
n . (Tn10,0) is set
[Tn10,0] is V13() set
{Tn10,0} is non empty finite set
{Tn10} is non empty finite set
{{Tn10,0},{Tn10}} is non empty finite V38() set
n . [Tn10,0] is set
n . (Tn10,1) is set
[Tn10,1] is V13() set
{Tn10,1} is non empty finite set
{{Tn10,1},{Tn10}} is non empty finite V38() set
n . [Tn10,1] is set
T . Tn10 is set
Tn11 is Element of F1()
f1 is Element of F1()
[Tn11,f1] is V13() Element of [:F1(),F1():]
{Tn11,f1} is non empty finite set
{Tn11} is non empty finite set
{{Tn11,f1},{Tn11}} is non empty finite V38() set
[Tn10,1] `2 is set
[Tn10,1] `1 is set
T . ([Tn10,1] `1) is set
(T . ([Tn10,1] `1)) `1 is set
(T . ([Tn10,1] `1)) `2 is set
IFEQ (([Tn10,1] `2),0,((T . ([Tn10,1] `1)) `1),((T . ([Tn10,1] `1)) `2)) is set
(T . Tn10) `2 is set
[Tn10,0] `2 is set
[Tn10,0] `1 is set
T . ([Tn10,0] `1) is set
(T . ([Tn10,0] `1)) `1 is set
(T . ([Tn10,0] `1)) `2 is set
IFEQ (([Tn10,0] `2),0,((T . ([Tn10,0] `1)) `1),((T . ([Tn10,0] `1)) `2)) is set
(T . Tn10) `1 is set
n . ((F . dp),0) is Element of F1()
[(F . dp),0] is V13() set
{(F . dp),0} is non empty finite set
{(F . dp)} is non empty finite set
{{(F . dp),0},{(F . dp)}} is non empty finite V38() set
n . [(F . dp),0] is set
n . ((F . dp),1) is Element of F1()
[(F . dp),1] is V13() set
{(F . dp),1} is non empty finite set
{{(F . dp),1},{(F . dp)}} is non empty finite V38() set
n . [(F . dp),1] is set
F1() is non empty set
F2() is Element of F1()
[:F1(),NAT:] is non empty set
T is set
T `2 is set
T `1 is set
n is Element of F1()
i is Element of F1()
F is Element of F1()
IFEQ ((T `2),0,i,F) is Element of F1()
dp is Element of F1()

proj1 T is set
proj2 T is set
[:[:F1(),NAT:],F1():] is non empty set
bool [:[:F1(),NAT:],F1():] is non empty set
n is Relation-like [:F1(),NAT:] -defined F1() -valued Function-like V29([:F1(),NAT:],F1()) Element of bool [:[:F1(),NAT:],F1():]

i . {} is set
proj1 i is non empty Tree-like set

Leaves () is Element of bool ()
bool () is non empty set
{ (F ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT : not 2 <= b1 } is set

{(),(F ^ <*1*>)} is non empty finite V38() Element of bool ()
bool () is non empty set
dp is set

dp is set
succ F is Element of bool ()

proj1 F is non empty Tree-like set
F . {} is set

{ (dp ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT : not 2 <= b1 } is set

{(dp ^ ),(dp ^ <*1*>)} is non empty finite V38() Element of bool ()
Tn10 is set

Tn10 is set
succ dp is Element of bool ()
bool () is non empty set

F . dp is Element of F1()

F . (dp ^ ) is set

F . (dp ^ <*1*>) is set
[(F . dp),0] is V13() Element of [:F1(),NAT:]
{(F . dp),0} is non empty finite set
{(F . dp)} is non empty finite set
{{(F . dp),0},{(F . dp)}} is non empty finite V38() set

[(F . dp),0] `1 is Element of F1()
n . [(F . dp),0] is Element of F1()
n . ((F . dp),0) is Element of F1()
[(F . dp),0] is V13() set
n . [(F . dp),0] is set
[(F . dp),1] is V13() Element of [:F1(),NAT:]
{(F . dp),1} is non empty finite set
{{(F . dp),1},{(F . dp)}} is non empty finite V38() set

[(F . dp),1] `1 is Element of F1()
n . [(F . dp),1] is Element of F1()
n . ((F . dp),1) is Element of F1()
[(F . dp),1] is V13() set
n . [(F . dp),1] is set
T is non empty set

T is non empty Tree-like finite-order V95() binary set

T -level n is Level of T
[:(T -level n),NAT:] is set
bool [:(T -level n),NAT:] is non empty set

{ } is set
i is set
{ } is set

proj1 i is set
proj2 i is set

F . dp is set

dp is set
{ } is set

i . dp is set

F . dp is set
T is non empty Tree-like finite-order V95() binary set

(T,n) is Relation-like T -level n -defined NAT -valued Function-like V29(T -level n, NAT ) Element of bool [:(T -level n),NAT:]
T -level n is Level of T
[:(T -level n),NAT:] is set
bool [:(T -level n),NAT:] is non empty set
i is set
proj1 (T,n) is set
F is set
(T,n) . i is set
(T,n) . F is set
{ } is set

{ } is set

i is set

Seg dp is finite dp -element Element of bool NAT

dp . 1 is set

T is non empty Tree-like set

{ } is set

is non empty finite V38() set
[:(Seg n),:] is finite set
bool [:(Seg n),:] is non empty finite V38() set
T -level n is Level of T

{ } is set
T is non empty Tree-like set

{ } is set
T -level n is Level of T

{ } is set
T is non empty Tree-like finite-order V95() binary set

T -level n is Level of T
T is non empty Tree-like set
T is non empty Tree-like set
T is non empty Tree-like finite-order V95() binary () set

Seg (2 to_power n) is finite 2 to_power n -element Element of bool NAT
(T,n) is Relation-like T -level n -defined NAT -valued Function-like V29(T -level n, NAT ) Element of bool [:(T -level n),NAT:]
T -level n is Level of T
[:(T -level n),NAT:] is set
bool [:(T -level n),NAT:] is non empty set
proj2 (T,n) is set
i is set
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= 2 to_power n ) } is set

1 - 1 is V24() V25() V26() ext-real set
F - 1 is V24() V25() V26() ext-real set

len (Rev (n -BinarySequence (F -' 1))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT

len (Rev (Rev (n -BinarySequence (F -' 1)))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT

{ } is set
{ } is set
proj1 (T,n) is set

(T,n) . (Rev (n -BinarySequence (F -' 1))) is set

(Absval (n -BinarySequence (F -' 1))) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative Element of NAT

(F - 1) + 1 is V24() V25() V26() ext-real set
T is non empty Tree-like finite-order V95() binary () set

(T,n) is Relation-like T -level n -defined NAT -valued Function-like V29(T -level n, NAT ) Element of bool [:(T -level n),NAT:]
T -level n is Level of T
[:(T -level n),NAT:] is set
bool [:(T -level n),NAT:] is non empty set

Seg (2 to_power n) is finite 2 to_power n -element Element of bool NAT

T -level i is finite Level of T
[:(T -level i),NAT:] is set
bool [:(T -level i),NAT:] is non empty set
proj1 (T,i) is finite set
F is set
((T,n) ") . F is set
(T,i) . (((T,n) ") . F) is set
proj2 (T,n) is set
dp is set
(T,i) . dp is set
{ } is set

{ } is set

proj2 (T,n) is set

proj1 ((T,i) ") is set
proj2 ((T,i) ") is set
[:(Seg (2 to_power n)),(T -level n):] is set
bool [:(Seg (2 to_power n)),(T -level n):] is non empty set
T is non empty Tree-like finite-order V95() binary () set

T -level n is finite Level of T

[:(T -level n),NAT:] is set
bool [:(T -level n),NAT:] is non empty set

T is non empty Tree-like finite-order V95() binary () set

T -level n is finite Level of T
[:(T -level n),NAT:] is set
bool [:(T -level n),NAT:] is non empty set

{ } is set

Seg n is non empty finite n -element Element of bool NAT

is non empty finite V38() set
[:(Seg n),:] is non empty finite set
bool [:(Seg n),:] is non empty finite V38() set
(T,n) . (0* n) is set

{ } is set

T is non empty Tree-like finite-order V95() binary () set

{ } is set

{ } is set

Seg n is non empty finite n -element Element of bool NAT

is non empty finite V38() set
[:(Seg n),:] is non empty finite set
bool [:(Seg n),:] is non empty finite V38() set

T -level n is finite Level of T
[:(T -level n),NAT:] is set
bool [:(T -level n),NAT:] is non empty set

(T,n) . () is set

(2 to_power n) - 1 is V24() V25() V26() ext-real set
((2 to_power n) - 1) + 1 is V24() V25() V26() ext-real set
T is non empty Tree-like finite-order V95() binary () set

T -level n is finite Level of T

[:(T -level n),NAT:] is set
bool [:(T -level n),NAT:] is non empty set

(T,n) . 1 is set

{ } is set

Seg n is non empty finite n -element Element of bool NAT

is non empty finite V38() set
[:(Seg n),:] is non empty finite set
bool [:(Seg n),:] is non empty finite V38() set
proj1 (T,n) is finite set
(T,n) . (0* n) is set
T is non empty Tree-like finite-order V95() binary () set

{ } is set

{ } is set

Seg n is non empty finite n -element Element of bool NAT

is non empty finite V38() set
[:(Seg n),:] is non empty finite set
bool [:(Seg n),:] is non empty finite V38() set

T -level n is finite Level of T

[:(T -level n),NAT:] is set
bool [:(T -level n),NAT:] is non empty set

(T,n) . (2 to_power n) is set

proj1 (T,n) is finite set
(T,n) . () is set
T is non empty Tree-like finite-order V95() binary () set

Seg (2 to_power n) is finite 2 to_power n -element Element of bool NAT

T -level n is finite Level of T

[:(T -level n),NAT:] is set
bool [:(T -level n),NAT:] is non empty set

(T,n) . i is set

{ } is set

i - 1 is V24() V25() V26() ext-real set

(i - 1) + 1 is V24() V25() V26() ext-real set

{ } is set

(T,n) . dp is set
proj1 (T,n) is finite set
T is non empty Tree-like finite-order V95() binary () set

T -level n is finite Level of T

T -level (n + 1) is finite Level of T
card (T -level (n + 1)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT

{ b1 where b1 is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like (T) : ( len b1 = n + 1 & b1 . (n + 1) = 0 ) } is set
{ b1 where b1 is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like (T) : ( len b1 = n + 1 & b1 . (n + 1) = 1 ) } is set

{ } is set

Seg (n + 1) is non empty finite n + 1 -element Element of bool NAT
(Seg (n + 1)) --> 0 is Relation-like Seg (n + 1) -defined -valued Function-like V29( Seg (n + 1),) finite FinSequence-like FinSubsequence-like Element of bool [:(Seg (n + 1)),:]
is non empty finite V38() set
[:(Seg (n + 1)),:] is non empty finite set
bool [:(Seg (n + 1)),:] is non empty finite V38() set
(0* (n + 1)) . (n + 1) is set

dp is set

Tn10 . (n + 1) is set
{ } is set

dp is set
{1} is non empty finite Element of bool NAT
dp is set

Tn10 . (n + 1) is set
{ } is set

{ } is set

[:(Seg n),:] is finite set
bool [:(Seg n),:] is non empty finite V38() set

((0* n) ^ <*1*>) . (n + 1) is set

Tn10 is non empty finite set
Tn11 is non empty finite set
Tn10 \/ Tn11 is non empty finite set
dp is non empty finite set
f1 is Element of dp
{ } is set

(f0 ^ <*1*>) . (n + 1) is set
x2 is Element of Tn11
[:dp,Tn11:] is non empty finite set
bool [:dp,Tn11:] is non empty finite V38() set
f1 is Relation-like dp -defined Tn11 -valued Function-like V29(dp,Tn11) finite Element of bool [:dp,Tn11:]
f0 is set

x . (n + 1) is set

x19 is boolean Element of BOOLEAN

x29 is set

{ } is set
x is set
x is Element of dp
f1 . x is Element of Tn11
f1 . x is set

proj2 f1 is finite set
f0 is Element of dp

x19 is set
is non empty finite V38() Element of bool NAT

() . (n + 1) is set
x19 is Element of Tn10
[:dp,Tn10:] is non empty finite set
bool [:dp,Tn10:] is non empty finite V38() set
f0 is Relation-like dp -defined Tn10 -valued Function-like V29(dp,Tn10) finite Element of bool [:dp,Tn10:]
x is set
proj1 f1 is finite set
x2 is set
f1 . x is set
f1 . x2 is set
x19 is Element of dp
f1 . x19 is Element of Tn11
x29 is Element of dp
f1 . x29 is Element of Tn11

f1 .: dp is finite set
x is set
{ } is set