:: BINTREE2 semantic presentation

REAL is set
NAT is epsilon-transitive epsilon-connected ordinal non empty Element of bool REAL
bool REAL is non empty set
COMPLEX is set
NAT is epsilon-transitive epsilon-connected ordinal non empty set
bool NAT is non empty set
bool NAT is non empty set
RAT is set
INT is set
[:NAT,REAL:] is set
bool [:NAT,REAL:] is non empty set
[:COMPLEX,COMPLEX:] is set
bool [:COMPLEX,COMPLEX:] is non empty set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set
[:REAL,REAL:] is set
bool [:REAL,REAL:] is non empty set
[:[:REAL,REAL:],REAL:] is set
bool [:[:REAL,REAL:],REAL:] is non empty set
[:RAT,RAT:] is set
bool [:RAT,RAT:] is non empty set
[:[:RAT,RAT:],RAT:] is set
bool [:[:RAT,RAT:],RAT:] is non empty set
[:INT,INT:] is set
bool [:INT,INT:] is non empty set
[:[:INT,INT:],INT:] is set
bool [:[:INT,INT:],INT:] is non empty set
[:NAT,NAT:] is non empty set
[:[:NAT,NAT:],NAT:] is non empty set
bool [:[:NAT,NAT:],NAT:] is non empty set
BOOLEAN is non empty set
0 is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty functional V24() V25() V26() finite V38() FinSequence-membered ext-real non positive non negative V75() Element of NAT
the epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty functional V24() V25() V26() finite V38() FinSequence-membered ext-real non positive non negative V75() set is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty functional V24() V25() V26() finite V38() FinSequence-membered ext-real non positive non negative V75() set
1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative Element of NAT
{0,1} is non empty finite set
{} is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty functional V24() V25() V26() finite V38() FinSequence-membered ext-real non positive non negative V75() 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 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative Element of NAT
[: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 (TOP-REAL 2) is set
3 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative Element of NAT
Seg 1 is non empty finite 1 -element Element of bool NAT
BOOLEAN * is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
FALSE is boolean Element of BOOLEAN
<*FALSE*> is Relation-like NAT -defined BOOLEAN -valued non empty Function-like finite 1 -element FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
'not' <*FALSE*> is Relation-like NAT -defined BOOLEAN -valued Function-like finite 1 -element FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
TRUE is boolean Element of BOOLEAN
<*TRUE*> is Relation-like NAT -defined BOOLEAN -valued non empty Function-like finite 1 -element FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
NAT * is non empty functional FinSequence-membered FinSequenceSet of NAT
<*> NAT is Relation-like NAT -defined NAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty proper Function-like functional V24() V25() V26() finite finite-yielding V38() FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V75() FinSequence of NAT
<*0*> is Relation-like NAT -defined non empty Function-like finite 1 -element FinSequence-like FinSubsequence-like set
<*1*> is Relation-like NAT -defined non empty Function-like finite 1 -element FinSequence-like FinSubsequence-like set
{{}} is non empty finite V38() set
T is set
n is Relation-like NAT -defined T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of T
i is Relation-like NAT -defined T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of T
n ^ i is Relation-like NAT -defined T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of T
T is non empty set
n is Element of T
<*n*> is Relation-like NAT -defined T -valued non empty Function-like finite 1 -element FinSequence-like FinSubsequence-like FinSequence of T
T is set
T * is non empty functional FinSequence-membered FinSequenceSet of T
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
i is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
Seg i is finite i -element Element of bool NAT
n | (Seg i) is Relation-like finite FinSubsequence-like set
T is non empty Tree-like finite-order V95() binary set
n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of T
i is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
proj2 i is finite set
F is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
<*F*> is Relation-like NAT -defined NAT -valued non empty Function-like finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
i ^ <*F*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
proj2 (i ^ <*F*>) is finite set
{ (i ^ <*b₁*>) where b₁ is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT : i ^ <*b₁*> in T } is set
dp is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of T
succ dp is finite Element of bool T
bool T is non empty set
Leaves T is Element of bool T
bool [:NAT,NAT:] is non empty set
<*0*> is Relation-like NAT -defined NAT -valued non empty Function-like finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
i ^ <*0*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*1*> is Relation-like NAT -defined NAT -valued non empty Function-like finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
i ^ <*1*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
{(i ^ <*0*>),(i ^ <*1*>)} is non empty finite V38() Element of bool (bool [:NAT,NAT:])
bool (bool [:NAT,NAT:]) 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
proj2 <*F*> is finite set
(proj2 i) \/ (proj2 <*F*>) is finite set
proj2 (<*> NAT) is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty functional V24() V25() V26() finite V38() FinSequence-membered ext-real non positive non negative V75() set
proj2 n 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
n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of T
Leaves T is Element of bool T
bool T is non empty set
{ (n ^ <*b₁*>) where b₁ is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT : n ^ <*b₁*> in T } is set
bool [:NAT,NAT:] is non empty set
<*0*> is Relation-like NAT -defined NAT -valued non empty Function-like finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
n ^ <*0*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*1*> is Relation-like NAT -defined NAT -valued non empty Function-like finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
n ^ <*1*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
{(n ^ <*0*>),(n ^ <*1*>)} is non empty finite V38() Element of bool (bool [:NAT,NAT:])
bool (bool [:NAT,NAT:]) is non empty set
i is set
F is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
<*F*> is Relation-like NAT -defined NAT -valued non empty Function-like finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
n ^ <*F*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
len n is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
(len n) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative Element of NAT
Seg ((len n) + 1) is non empty finite (len n) + 1 -element Element of bool NAT
dp is Relation-like NAT -defined {0,1} -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of {0,1}
len dp is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of 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
proj2 <*1*> is finite set
F is set
{1} is non empty finite Element of bool NAT
proj2 <*0*> is finite set
F is set
{0} is non empty finite V38() Element of bool NAT
succ n is Element of bool T
{0} 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
i is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of T
F is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> is Relation-like NAT -defined NAT -valued non empty Function-like finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
F ^ <*0*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
T is non empty Tree-like finite-order V95() binary set
n is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
T -level n is Level of T
n -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
{ b₁ where b₁ is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like Element of BOOLEAN * : len b₁ = n } is set
i is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like (T)
{ b₁ where b₁ is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like (T) : len b₁ = n } is set
F is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like (T)
len F is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
bool [:NAT,NAT:] is non empty set
<*0*> is Relation-like NAT -defined NAT -valued non empty Function-like finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
<*1*> is Relation-like NAT -defined NAT -valued non empty Function-like finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
T is non empty Tree-like set
Leaves T is Element of bool T
bool T is non empty set
n is set
i is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of T
succ i is Element of bool T
i ^ <*0*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
i ^ <*1*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
{(i ^ <*0*>),(i ^ <*1*>)} is non empty finite V38() Element of bool (bool [:NAT,NAT:])
bool (bool [:NAT,NAT:]) 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 Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of T
succ n is Element of bool T
n ^ <*0*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
n ^ <*1*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
{(n ^ <*0*>),(n ^ <*1*>)} is non empty finite V38() Element of bool (bool [:NAT,NAT:])
bool (bool [:NAT,NAT:]) is non empty set
T is non empty Tree-like set
n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of T
succ n is Element of bool T
bool T is non empty set
n ^ <*0*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
n ^ <*1*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
{(n ^ <*0*>),(n ^ <*1*>)} is non empty finite V38() Element of bool (bool [:NAT,NAT:])
bool (bool [:NAT,NAT:]) is non empty set
Leaves T is Element of bool T
n is set
n is set
i is Relation-like NAT -defined {0,1} -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of {0,1}
F is Element of {0,1}
<*F*> is Relation-like NAT -defined {0,1} -valued non empty Function-like finite 1 -element FinSequence-like FinSubsequence-like FinSequence of {0,1}
i ^ <*F*> is Relation-like NAT -defined {0,1} -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of {0,1}
dp is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of T
succ dp is Element of bool T
bool T is non empty set
dp ^ <*0*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
dp ^ <*1*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
{(dp ^ <*0*>),(dp ^ <*1*>)} is non empty finite V38() Element of bool (bool [:NAT,NAT:])
bool (bool [:NAT,NAT:]) is non empty set
<*> {0,1} is Relation-like NAT -defined {0,1} -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty proper Function-like functional V24() V25() V26() finite finite-yielding V38() FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V75() FinSequence of {0,1}
[:NAT,{0,1}:] is non empty set
F₁() is non empty set
F₂() is Element of F₁()
[:F₁(),F₁():] is non empty set
T is set
n is Element of F₁()
i is Element of F₁()
[n,i] is V13() Element of [:F₁(),F₁():]
{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 [:F₁(),F₁():]
T is Relation-like Function-like set
proj1 T is set
proj2 T is set
[:F₁(),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
[:[:F₁(),NAT:],F₁():] is non empty set
bool [:[:F₁(),NAT:],F₁():] is non empty set
n is Relation-like [:F₁(),NAT:] -defined F₁() -valued Function-like V29([:F₁(),NAT:],F₁()) Element of bool [:[:F₁(),NAT:],F₁():]
i is Relation-like F₁() -valued Function-like DecoratedTree-like set
i . {} is set
proj1 i is non empty Tree-like set
F is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 i
Leaves (proj1 i) is Element of bool (proj1 i)
bool (proj1 i) is non empty set
{ (F ^ <*b₁*>) where b₁ is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT : not 2 <= b₁ } is set
F ^ <*0*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
F ^ <*1*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
{(F ^ <*0*>),(F ^ <*1*>)} is non empty finite V38() Element of bool (bool [:NAT,NAT:])
bool (bool [:NAT,NAT:]) is non empty set
dp is set
Tn10 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
<*Tn10*> is Relation-like NAT -defined NAT -valued non empty Function-like finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
F ^ <*Tn10*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
dp is set
succ F is Element of bool (proj1 i)
F is Relation-like F₁() -valued Function-like DecoratedTree-like binary set
proj1 F is non empty Tree-like set
F . {} is set
dp is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 F
{ (dp ^ <*b₁*>) where b₁ is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT : not 2 <= b₁ } is set
dp ^ <*0*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
dp ^ <*1*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
{(dp ^ <*0*>),(dp ^ <*1*>)} is non empty finite V38() Element of bool (bool [:NAT,NAT:])
Tn10 is set
Tn11 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
<*Tn11*> is Relation-like NAT -defined NAT -valued non empty Function-like finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
dp ^ <*Tn11*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
Tn10 is set
succ dp is Element of bool (proj1 F)
bool (proj1 F) is non empty set
dp is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 F
F . dp is Element of F₁()
dp ^ <*0*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
F . (dp ^ <*0*>) is set
dp ^ <*1*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
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 F₁()
f1 is Element of F₁()
[Tn11,f1] is V13() Element of [:F₁(),F₁():]
{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 F₁()
[(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 F₁()
[(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
F₁() is non empty set
F₂() is Element of F₁()
[:F₁(),NAT:] is non empty set
T is set
T `2 is set
T `1 is set
n is Element of F₁()
i is Element of F₁()
F is Element of F₁()
IFEQ ((T `2),0,i,F) is Element of F<sub>1</sub>()
dp is Element of F<sub>1</sub>()
T is Relation-like Function-like set
proj1 T is set
proj2 T is set
[:[:F<sub>1</sub>(),NAT:],F<sub>1</sub>():] is non empty set
bool [:[:F<sub>1</sub>(),NAT:],F<sub>1</sub>():] is non empty set
n is Relation-like [:F<sub>1</sub>(),NAT:] -defined F<sub>1</sub>() -valued Function-like V29([:F<sub>1</sub>(),NAT:],F<sub>1</sub>()) Element of bool [:[:F<sub>1</sub>(),NAT:],F<sub>1</sub>():]
i is Relation-like F<sub>1</sub>() -valued Function-like DecoratedTree-like set
i . {} is set
proj1 i is non empty Tree-like set
F is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 i
Leaves (proj1 i) is Element of bool (proj1 i)
bool (proj1 i) is non empty set
{ (F ^ <*b<sub>1</sub>*>) where b<sub>1</sub> is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT : not 2 <= b<sub>1</sub> } is set
F ^ <*0*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
F ^ <*1*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
{(F ^ <*0*>),(F ^ <*1*>)} is non empty finite V38() Element of bool (bool [:NAT,NAT:])
bool (bool [:NAT,NAT:]) is non empty set
dp is set
Tn10 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
<*Tn10*> is Relation-like NAT -defined NAT -valued non empty Function-like finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
F ^ <*Tn10*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
dp is set
succ F is Element of bool (proj1 i)
F is Relation-like F<sub>1</sub>() -valued Function-like DecoratedTree-like binary set
proj1 F is non empty Tree-like set
F . {} is set
dp is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 F
{ (dp ^ <*b<sub>1</sub>*>) where b<sub>1</sub> is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT : not 2 <= b<sub>1</sub> } is set
dp ^ <*0*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
dp ^ <*1*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
{(dp ^ <*0*>),(dp ^ <*1*>)} is non empty finite V38() Element of bool (bool [:NAT,NAT:])
Tn10 is set
Tn11 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
<*Tn11*> is Relation-like NAT -defined NAT -valued non empty Function-like finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
dp ^ <*Tn11*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
Tn10 is set
succ dp is Element of bool (proj1 F)
bool (proj1 F) is non empty set
dp is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 F
F . dp is Element of F<sub>1</sub>()
dp ^ <*0*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
F . (dp ^ <*0*>) is set
dp ^ <*1*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
F . (dp ^ <*1*>) is set
[(F . dp),0] is V13() Element of [:F<sub>1</sub>(),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] `2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
[(F . dp),0] `1 is Element of F<sub>1</sub>()
n . [(F . dp),0] is Element of F<sub>1</sub>()
n . ((F . dp),0) is Element of F<sub>1</sub>()
[(F . dp),0] is V13() set
n . [(F . dp),0] is set
[(F . dp),1] is V13() Element of [:F<sub>1</sub>(),NAT:]
{(F . dp),1} is non empty finite set
{{(F . dp),1},{(F . dp)}} is non empty finite V38() set
[(F . dp),1] `2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
[(F . dp),1] `1 is Element of F₁()
n . [(F . dp),1] is Element of F₁()
n . ((F . dp),1) is Element of F₁()
[(F . dp),1] is V13() set
n . [(F . dp),1] is set
T is non empty set
n is Relation-like NAT -defined T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of T
Rev n is Relation-like NAT -defined T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of T
T is non empty Tree-like finite-order V95() binary set
n is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative set
T -level n is Level of T
[:(T -level n),NAT:] is set
bool [:(T -level n),NAT:] is non empty set
n -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
{ b₁ where b₁ is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like Element of BOOLEAN * : len b₁ = n } is set
i is set
{ b₁ where b₁ is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like (T) : len b₁ = n } is set
F is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like (T)
len F is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
Rev F is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
len (Rev F) is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
dp is Relation-like NAT -defined BOOLEAN -valued Function-like finite n -element FinSequence-like FinSubsequence-like Element of n -tuples_on BOOLEAN
Absval dp is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
(Absval dp) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative Element of NAT
Tn10 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative Element of NAT
Tn11 is Relation-like NAT -defined BOOLEAN -valued Function-like finite n -element FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
Absval Tn11 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
(Absval Tn11) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative Element of NAT
i is Relation-like Function-like set
proj1 i is set
proj2 i is set
F is Relation-like T -level n -defined NAT -valued Function-like V29(T -level n, NAT ) Element of bool [:(T -level n),NAT:]
dp is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like (T)
Rev dp is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
F . dp is set
Tn10 is Relation-like NAT -defined BOOLEAN -valued Function-like finite n -element FinSequence-like FinSubsequence-like Element of n -tuples_on BOOLEAN
Absval Tn10 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
(Absval Tn10) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative Element of NAT
Tn11 is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like (T)
Rev Tn11 is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
i is Relation-like T -level n -defined NAT -valued Function-like V29(T -level n, NAT ) Element of bool [:(T -level n),NAT:]
F is Relation-like T -level n -defined NAT -valued Function-like V29(T -level n, NAT ) Element of bool [:(T -level n),NAT:]
dp is set
{ b₁ where b₁ is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like (T) : len b₁ = n } is set
Tn10 is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like (T)
len Tn10 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
Rev Tn10 is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
len (Rev Tn10) is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
i . dp is set
Tn11 is Relation-like NAT -defined BOOLEAN -valued Function-like finite n -element FinSequence-like FinSubsequence-like Element of n -tuples_on BOOLEAN
Absval Tn11 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
(Absval Tn11) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative Element of NAT
F . dp is set
T is non empty Tree-like finite-order V95() binary set
n is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative Element of 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
i is set
proj1 (T,n) is set
F is set
(T,n) . i is set
(T,n) . F is set
{ b₁ where b₁ is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like (T) : len b₁ = n } is set
dp is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like (T)
len dp is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
Tn10 is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like (T)
len Tn10 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
Rev Tn10 is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
len (Rev Tn10) is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
n -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
{ b₁ where b₁ is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like Element of BOOLEAN * : len b₁ = n } is set
Rev dp is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
len (Rev dp) is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
f1 is Relation-like NAT -defined BOOLEAN -valued Function-like finite n -element FinSequence-like FinSubsequence-like Element of n -tuples_on BOOLEAN
Absval f1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
(Absval f1) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative Element of NAT
Tn11 is Relation-like NAT -defined BOOLEAN -valued Function-like finite n -element FinSequence-like FinSubsequence-like Element of n -tuples_on BOOLEAN
Absval Tn11 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
(Absval Tn11) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative Element of NAT
n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
ProperPrefixes n is set
i is set
F is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dp is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
Seg dp is finite dp -element Element of bool NAT
n | (Seg dp) is Relation-like NAT -defined NAT -valued Function-like finite FinSubsequence-like Element of bool [:NAT,NAT:]
n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
i is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
<*i*> is Relation-like NAT -defined NAT -valued non empty Function-like finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
n ^ <*i*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
F is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
dom <*i*> is finite Element of bool NAT
dp is Relation-like NAT -defined {0,1} -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of {0,1}
dp . 1 is set
0 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative Element of NAT
<*F*> is Relation-like NAT -defined NAT -valued non empty Function-like finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
n ^ <*F*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
T is non empty Tree-like set
n is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative set
0* n is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL n
REAL n is functional FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = n } is set
n |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
Seg n is finite n -element Element of bool NAT
(Seg n) --> 0 is Relation-like Seg n -defined {0} -valued Function-like V29( Seg n,{0}) finite FinSequence-like FinSubsequence-like Element of bool [:(Seg n),{0}:]
{0} is non empty finite V38() set
[:(Seg n),{0}:] is finite set
bool [:(Seg n),{0}:] is non empty finite V38() set
T -level n is Level of T
len (0* n) is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of T : len b₁ = n } is set
T is non empty Tree-like set
n is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative Element of NAT
n -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
{ b₁ where b₁ is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like Element of BOOLEAN * : len b₁ = n } is set
T -level n is Level of T
i is Relation-like NAT -defined BOOLEAN -valued Function-like finite n -element FinSequence-like FinSubsequence-like Element of n -tuples_on BOOLEAN
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of T : len b₁ = n } is set
T is non empty Tree-like finite-order V95() binary set
n is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
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
n is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative set
2 to_power n is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
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
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ <= 2 to_power n ) } is set
F is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
1 - 1 is V24() V25() V26() ext-real set
F - 1 is V24() V25() V26() ext-real set
F -' 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
n -BinarySequence (F -' 1) is Relation-like NAT -defined BOOLEAN -valued Function-like finite n -element FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
Rev (n -BinarySequence (F -' 1)) is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
len (Rev (n -BinarySequence (F -' 1))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
len (n -BinarySequence (F -' 1)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
Rev (Rev (n -BinarySequence (F -' 1))) is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
len (Rev (Rev (n -BinarySequence (F -' 1)))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
n -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
{ b₁ where b₁ is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like Element of BOOLEAN * : len b₁ = n } is set
{ b₁ where b₁ is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like (T) : len b₁ = n } is set
proj1 (T,n) is set
(2 to_power n) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative Element of NAT
(T,n) . (Rev (n -BinarySequence (F -' 1))) is set
Tn10 is Relation-like NAT -defined BOOLEAN -valued Function-like finite n -element FinSequence-like FinSubsequence-like Element of n -tuples_on BOOLEAN
Absval Tn10 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
(Absval Tn10) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative Element of NAT
Absval (n -BinarySequence (F -' 1)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
(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 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
n is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative 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
(T,n) " is Relation-like Function-like set
2 to_power n is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
Seg (2 to_power n) is finite 2 to_power n -element Element of bool NAT
i is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative Element of NAT
(T,i) is Relation-like T -level i -defined NAT -valued Function-like one-to-one V29(T -level i, NAT ) finite Element of bool [:(T -level i),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
{ b₁ where b₁ is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like (T) : len b₁ = n } is set
Tn10 is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like (T)
len Tn10 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
Rev Tn10 is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
len (Rev Tn10) is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
n -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
{ b₁ where b₁ is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like Element of BOOLEAN * : len b₁ = n } is set
Tn11 is Relation-like NAT -defined BOOLEAN -valued Function-like finite n -element FinSequence-like FinSubsequence-like Element of n -tuples_on BOOLEAN
Absval Tn11 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
(Absval Tn11) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative Element of NAT
proj2 (T,n) is set
(T,i) " is Relation-like Function-like 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
n is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative Element of NAT
(T,n) is Relation-like NAT -defined T -level n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of T -level n
T -level n is finite Level of T
(T,n) is Relation-like T -level n -defined NAT -valued Function-like one-to-one V29(T -level n, NAT ) finite Element of bool [:(T -level n),NAT:]
[:(T -level n),NAT:] is set
bool [:(T -level n),NAT:] is non empty set
(T,n) " is Relation-like Function-like set
T is non empty Tree-like finite-order V95() binary () set
n is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative Element of NAT
(T,n) is Relation-like T -level n -defined NAT -valued Function-like one-to-one V29(T -level n, NAT ) finite Element of bool [:(T -level n),NAT:]
T -level n is finite Level of T
[:(T -level n),NAT:] is set
bool [:(T -level n),NAT:] is non empty set
0* n is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL n
REAL n is functional FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = n } is set
n |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
Seg n is non empty finite n -element Element of bool NAT
(Seg n) --> 0 is Relation-like Seg n -defined {0} -valued Function-like V29( Seg n,{0}) finite FinSequence-like FinSubsequence-like Element of bool [:(Seg n),{0}:]
{0} is non empty finite V38() set
[:(Seg n),{0}:] is non empty finite set
bool [:(Seg n),{0}:] is non empty finite V38() set
(T,n) . (0* n) is set
Rev (0* n) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of REAL
len (Rev (0* n)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
len (0* n) is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
n -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
{ b₁ where b₁ is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like Element of BOOLEAN * : len b₁ = n } is set
i is Relation-like NAT -defined BOOLEAN -valued Function-like finite n -element FinSequence-like FinSubsequence-like Element of n -tuples_on BOOLEAN
Absval i is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
(Absval i) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative Element of NAT
0 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative Element of NAT
T is non empty Tree-like finite-order V95() binary () set
n is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative Element of NAT
n -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
{ b₁ where b₁ is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like Element of BOOLEAN * : len b₁ = n } is set
0* n is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL n
REAL n is functional FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = n } is set
n |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
Seg n is non empty finite n -element Element of bool NAT
(Seg n) --> 0 is Relation-like Seg n -defined {0} -valued Function-like V29( Seg n,{0}) finite FinSequence-like FinSubsequence-like Element of bool [:(Seg n),{0}:]
{0} is non empty finite V38() set
[:(Seg n),{0}:] is non empty finite set
bool [:(Seg n),{0}:] is non empty finite V38() set
(T,n) is Relation-like T -level n -defined NAT -valued Function-like one-to-one V29(T -level n, NAT ) finite Element of bool [:(T -level n),NAT:]
T -level n is finite Level of T
[:(T -level n),NAT:] is set
bool [:(T -level n),NAT:] is non empty set
2 to_power n is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
i is Relation-like NAT -defined BOOLEAN -valued Function-like finite n -element FinSequence-like FinSubsequence-like Element of n -tuples_on BOOLEAN
'not' i is Relation-like NAT -defined BOOLEAN -valued Function-like finite n -element FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(T,n) . ('not' i) is set
Rev ('not' i) is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
len (Rev ('not' i)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
len ('not' i) is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
dp is Relation-like NAT -defined BOOLEAN -valued Function-like finite n -element FinSequence-like FinSubsequence-like Element of n -tuples_on BOOLEAN
F is Relation-like NAT -defined BOOLEAN -valued Function-like finite n -element FinSequence-like FinSubsequence-like Element of n -tuples_on BOOLEAN
Absval F is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
(Absval F) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative Element of NAT
(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
n is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative Element of NAT
(T,n) is Relation-like NAT -defined T -level n -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like FinSequence of T -level n
T -level n is finite Level of T
(T,n) is Relation-like T -level n -defined NAT -valued Function-like one-to-one V29(T -level n, NAT ) finite Element of bool [:(T -level n),NAT:]
[:(T -level n),NAT:] is set
bool [:(T -level n),NAT:] is non empty set
(T,n) " is Relation-like Function-like set
(T,n) . 1 is set
0* n is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL n
REAL n is functional FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = n } is set
n |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
Seg n is non empty finite n -element Element of bool NAT
(Seg n) --> 0 is Relation-like Seg n -defined {0} -valued Function-like V29( Seg n,{0}) finite FinSequence-like FinSubsequence-like Element of bool [:(Seg n),{0}:]
{0} is non empty finite V38() set
[:(Seg n),{0}:] is non empty finite set
bool [:(Seg n),{0}:] 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
n is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative Element of NAT
n -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
{ b₁ where b₁ is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like Element of BOOLEAN * : len b₁ = n } is set
0* n is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL n
REAL n is functional FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = n } is set
n |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
Seg n is non empty finite n -element Element of bool NAT
(Seg n) --> 0 is Relation-like Seg n -defined {0} -valued Function-like V29( Seg n,{0}) finite FinSequence-like FinSubsequence-like Element of bool [:(Seg n),{0}:]
{0} is non empty finite V38() set
[:(Seg n),{0}:] is non empty finite set
bool [:(Seg n),{0}:] is non empty finite V38() set
(T,n) is Relation-like NAT -defined T -level n -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like FinSequence of T -level n
T -level n is finite Level of T
(T,n) is Relation-like T -level n -defined NAT -valued Function-like one-to-one V29(T -level n, NAT ) finite Element of bool [:(T -level n),NAT:]
[:(T -level n),NAT:] is set
bool [:(T -level n),NAT:] is non empty set
(T,n) " is Relation-like Function-like set
2 to_power n is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
(T,n) . (2 to_power n) is set
i is Relation-like NAT -defined BOOLEAN -valued Function-like finite n -element FinSequence-like FinSubsequence-like Element of n -tuples_on BOOLEAN
'not' i is Relation-like NAT -defined BOOLEAN -valued Function-like finite n -element FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
F is Relation-like NAT -defined BOOLEAN -valued Function-like finite n -element FinSequence-like FinSubsequence-like Element of n -tuples_on BOOLEAN
proj1 (T,n) is finite set
(T,n) . ('not' i) is set
T is non empty Tree-like finite-order V95() binary () set
n is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative Element of NAT
2 to_power n is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
Seg (2 to_power n) is finite 2 to_power n -element Element of bool NAT
(T,n) is Relation-like NAT -defined T -level n -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like FinSequence of T -level n
T -level n is finite Level of T
(T,n) is Relation-like T -level n -defined NAT -valued Function-like one-to-one V29(T -level n, NAT ) finite Element of bool [:(T -level n),NAT:]
[:(T -level n),NAT:] is set
bool [:(T -level n),NAT:] is non empty set
(T,n) " is Relation-like Function-like set
i is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
(T,n) . i is set
i -' 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
n -BinarySequence (i -' 1) is Relation-like NAT -defined BOOLEAN -valued Function-like finite n -element FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
Rev (n -BinarySequence (i -' 1)) is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
n -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
{ b₁ where b₁ is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like Element of BOOLEAN * : len b₁ = n } is set
(2 to_power n) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative Element of NAT
i - 1 is V24() V25() V26() ext-real set
F is Relation-like NAT -defined BOOLEAN -valued Function-like finite n -element FinSequence-like FinSubsequence-like Element of n -tuples_on BOOLEAN
Absval F is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
(Absval F) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative Element of NAT
(i -' 1) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative Element of NAT
(i - 1) + 1 is V24() V25() V26() ext-real set
Rev F is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
len (Rev F) is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
len F is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
dp is Relation-like NAT -defined BOOLEAN -valued Function-like finite n -element FinSequence-like FinSubsequence-like Element of n -tuples_on BOOLEAN
{ b₁ where b₁ is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like (T) : len b₁ = n } is set
Rev dp is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(T,n) . dp is set
proj1 (T,n) is finite set
T is non empty Tree-like finite-order V95() binary () set
n is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
T -level n is finite Level of T
card (T -level n) is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
2 to_power n is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
n + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative Element of NAT
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
2 to_power (n + 1) is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
{ b₁ where b₁ is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like (T) : ( len b₁ = n + 1 & b₁ . (n + 1) = 0 ) } is set
{ b₁ where b₁ is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like (T) : ( len b₁ = n + 1 & b₁ . (n + 1) = 1 ) } is set
0* (n + 1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL (n + 1)
REAL (n + 1) is functional FinSequence-membered FinSequenceSet of REAL
(n + 1) -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = n + 1 } is set
(n + 1) |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like finite n + 1 -element FinSequence-like FinSubsequence-like Element of (n + 1) -tuples_on REAL
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 {0} -valued Function-like V29( Seg (n + 1),{0}) finite FinSequence-like FinSubsequence-like Element of bool [:(Seg (n + 1)),{0}:]
{0} is non empty finite V38() set
[:(Seg (n + 1)),{0}:] is non empty finite set
bool [:(Seg (n + 1)),{0}:] is non empty finite V38() set
(0* (n + 1)) . (n + 1) is set
len (0* (n + 1)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
dp is set
Tn10 is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like (T)
len Tn10 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
Tn10 . (n + 1) is set
{ b₁ where b₁ is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like (T) : len b₁ = n + 1 } is set
proj2 <*1*> is finite set
dp is set
{1} is non empty finite Element of bool NAT
dp is set
Tn10 is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like (T)
len Tn10 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
Tn10 . (n + 1) is set
{ b₁ where b₁ is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like (T) : len b₁ = n + 1 } is set
0* n is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL n
REAL n is functional FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = n } is set
n |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like Element of n -tuples_on REAL
Seg n is finite n -element Element of bool NAT
(Seg n) --> 0 is Relation-like Seg n -defined {0} -valued Function-like V29( Seg n,{0}) finite FinSequence-like FinSubsequence-like Element of bool [:(Seg n),{0}:]
[:(Seg n),{0}:] is finite set
bool [:(Seg n),{0}:] is non empty finite V38() set
(0* n) ^ <*1*> is Relation-like NAT -defined non empty Function-like finite FinSequence-like FinSubsequence-like set
len (0* n) is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
((0* n) ^ <*1*>) . (n + 1) is set
len ((0* n) ^ <*1*>) is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
(len (0* n)) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative Element of NAT
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
{ b₁ where b₁ is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like (T) : len b₁ = n } is set
f0 is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like (T)
len f0 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
f0 ^ <*1*> is Relation-like NAT -defined non empty Function-like finite FinSequence-like FinSubsequence-like set
len (f0 ^ <*1*>) is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
(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 is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like (T)
len x is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
x . (n + 1) is set
x2 is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
x19 is boolean Element of BOOLEAN
<*x19*> is Relation-like NAT -defined BOOLEAN -valued non empty Function-like finite 1 -element FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
x2 ^ <*x19*> is Relation-like NAT -defined BOOLEAN -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
x29 is set
len x2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
(len x2) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative Element of NAT
{ b₁ where b₁ is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like (T) : len b₁ = n } is set
x is set
x is Element of dp
f1 . x is Element of Tn11
f1 . x is set
x9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
x9 ^ <*1*> is Relation-like NAT -defined non empty Function-like finite FinSequence-like FinSubsequence-like set
proj2 f1 is finite set
f0 is Element of dp
x is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like (T)
len x is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
x ^ <*0*> is Relation-like NAT -defined non empty Function-like finite FinSequence-like FinSubsequence-like set
proj2 <*0*> is finite set
x19 is set
{0} is non empty finite V38() Element of bool NAT
len (x ^ <*0*>) is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
(x ^ <*0*>) . (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
x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
x ^ <*1*> is Relation-like NAT -defined non empty Function-like finite FinSequence-like FinSubsequence-like set
x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
x ^ <*1*> is Relation-like NAT -defined non empty Function-like finite FinSequence-like FinSubsequence-like set
f1 .: dp is finite set
x is set
{ b₁ where b₁ is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like (T) : len b₁ = n + 1 } is set
x2 is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like (T)
len x2 is epsilon-transit