:: 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-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
dom x2 is finite Element of bool NAT
x2 . (n + 1) is set
x is set
x2 is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like (T)
len x2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
x2 . (n + 1) is set
x19 is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
x29 is boolean Element of BOOLEAN
<*x29*> is Relation-like NAT -defined BOOLEAN -valued non empty Function-like finite 1 -element FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
x19 ^ <*x29*> is Relation-like NAT -defined BOOLEAN -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
x is set
len x19 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
(len x19) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative Element of NAT
x is set
x9 is Element of dp
f0 . x9 is Element of Tn10
f0 . x is set
c₁₇ is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
c₁₇ ^ <*0*> is Relation-like NAT -defined non empty Function-like finite FinSequence-like FinSubsequence-like set
proj2 f0 is finite set
x is set
proj1 f0 is finite set
x2 is set
f0 . x is set
f0 . x2 is set
x19 is Element of dp
f0 . x19 is Element of Tn10
x29 is Element of dp
f0 . x29 is Element of Tn10
x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
x ^ <*0*> 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 ^ <*0*> is Relation-like NAT -defined non empty Function-like finite FinSequence-like FinSubsequence-like set
f0 .: dp is finite set
card dp is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
card Tn10 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
Tn10 /\ Tn11 is finite set
x is set
x2 is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like (T)
len x2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
x2 . (n + 1) is set
x19 is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like (T)
len x19 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
x19 . (n + 1) is set
2 to_power 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
(2 to_power n) * (2 to_power 1) is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
2 * (2 to_power n) is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
(card dp) + (card dp) is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
card Tn11 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
(card Tn10) + (card Tn11) is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
card (Tn10 \/ Tn11) is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
T -level 0 is finite Level of T
card (T -level 0) is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
card {{}} is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
2 to_power 0 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real 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
(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
len (T,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
proj2 (T,n) is finite set
proj1 (T,n) is finite set
dom (T,n) is finite Element of bool NAT
Seg (len (T,n)) is finite len (T,n) -element Element of bool NAT
card (Seg (len (T,n))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
card (dom (T,n)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
card (T -level n) is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real 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
(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
dom (T,n) is finite Element of bool 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
len (T,n) is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
Seg (len (T,n)) is finite len (T,n) -element Element of bool 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
(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
proj2 (T,n) is finite set
dom (T,n) is finite Element of bool NAT
[:(dom (T,n)),(T -level n):] is finite set
bool [:(dom (T,n)),(T -level n):] is non empty finite V38() set
F is Relation-like dom (T,n) -defined T -level n -valued Function-like V29( dom (T,n),T -level n) finite Element of bool [:(dom (T,n)),(T -level n):]
proj1 F is finite set
dp is finite set
card dp 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
Seg (2 to_power n) is finite 2 to_power n -element Element of bool NAT
card (Seg (2 to_power n)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
i is finite set
card i is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
T is non empty Tree-like finite-order V95() binary () set
(T,1) is Relation-like NAT -defined T -level 1 -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like FinSequence of T -level 1
T -level 1 is finite Level of T
(T,1) is Relation-like T -level 1 -defined NAT -valued Function-like one-to-one V29(T -level 1, NAT ) finite Element of bool [:(T -level 1),NAT:]
[:(T -level 1),NAT:] is set
bool [:(T -level 1),NAT:] is non empty set
(T,1) " is Relation-like Function-like set
(T,1) . 1 is set
0* 1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL 1
REAL 1 is functional FinSequence-membered FinSequenceSet of REAL
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₁ = 1 } is set
1 |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like finite 1 -element FinSequence-like FinSubsequence-like Element of 1 -tuples_on REAL
(Seg 1) --> 0 is Relation-like Seg 1 -defined {0} -valued Function-like V29( Seg 1,{0}) finite FinSequence-like FinSubsequence-like Element of bool [:(Seg 1),{0}:]
{0} is non empty finite V38() set
[:(Seg 1),{0}:] is non empty finite set
bool [:(Seg 1),{0}:] is non empty finite V38() set
T is non empty Tree-like finite-order V95() binary () set
(T,1) is Relation-like NAT -defined T -level 1 -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like FinSequence of T -level 1
T -level 1 is finite Level of T
(T,1) is Relation-like T -level 1 -defined NAT -valued Function-like one-to-one V29(T -level 1, NAT ) finite Element of bool [:(T -level 1),NAT:]
[:(T -level 1),NAT:] is set
bool [:(T -level 1),NAT:] is non empty set
(T,1) " is Relation-like Function-like set
(T,1) . 2 is set
0* 1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL 1
REAL 1 is functional FinSequence-membered FinSequenceSet of REAL
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₁ = 1 } is set
1 |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like finite 1 -element FinSequence-like FinSubsequence-like Element of 1 -tuples_on REAL
(Seg 1) --> 0 is Relation-like Seg 1 -defined {0} -valued Function-like V29( Seg 1,{0}) finite FinSequence-like FinSubsequence-like Element of bool [:(Seg 1),{0}:]
{0} is non empty finite V38() set
[:(Seg 1),{0}:] is non empty finite set
bool [:(Seg 1),{0}:] is non empty finite V38() set
1 -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₁ = 1 } is set
2 to_power 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
(T,1) . (2 to_power 1) is set
n is Relation-like NAT -defined BOOLEAN -valued Function-like finite 1 -element FinSequence-like FinSubsequence-like Element of 1 -tuples_on BOOLEAN
'not' n is Relation-like NAT -defined BOOLEAN -valued Function-like finite 1 -element FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
T is non empty Tree-like finite-order V95() binary () set
i is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive 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
2 to_power (n + 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
(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 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative Element of NAT
(i + 1) div 2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
(T,n) . ((i + 1) div 2) is set
(T,(n + 1)) is Relation-like NAT -defined T -level (n + 1) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like FinSequence of T -level (n + 1)
T -level (n + 1) is finite Level of T
(T,(n + 1)) is Relation-like T -level (n + 1) -defined NAT -valued Function-like one-to-one V29(T -level (n + 1), NAT ) finite Element of bool [:(T -level (n + 1)),NAT:]
[:(T -level (n + 1)),NAT:] is set
bool [:(T -level (n + 1)),NAT:] is non empty set
(T,(n + 1)) " is Relation-like Function-like set
(T,(n + 1)) . i is set
(i + 1) mod 2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
<*((i + 1) mod 2)*> is Relation-like NAT -defined NAT -valued non empty Function-like finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
i -' 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
(i -' 1) mod 2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
1 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative Element of NAT
(1 + 1) * 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
(i -' 1) + ((1 + 1) * 1) is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
((i -' 1) + ((1 + 1) * 1)) mod 2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real 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) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative Element of NAT
(((i -' 1) + 1) + 1) mod 2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
i -' 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
(i -' 1) mod 2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
1 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative Element of NAT
(1 + 1) * 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
(i -' 1) + ((1 + 1) * 1) is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
((i -' 1) + ((1 + 1) * 1)) mod 2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real 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) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative Element of NAT
(((i -' 1) + 1) + 1) mod 2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
i -' 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
(i -' 1) mod 2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
i -' 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
(i -' 1) mod 2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
F is Relation-like NAT -defined BOOLEAN -valued Function-like finite n -element FinSequence-like FinSubsequence-like Element of n -tuples_on BOOLEAN
F ^ <*((i + 1) mod 2)*> is Relation-like NAT -defined non empty Function-like finite n + 1 -element FinSequence-like FinSubsequence-like set
n + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative Element of NAT
1 + 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 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
2 to_power 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
(2 to_power n) * (2 to_power 1) is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
2 * (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 -' 1) div 2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
((i -' 1) div 2) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative Element of NAT
(((i -' 1) div 2) + 1) - 1 is V24() V25() V26() ext-real set
(i -' 1) + (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 + 1)) div 2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
(((i -' 1) + (1 + 1)) div 2) - 1 is V24() V25() V26() ext-real set
(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) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative Element of NAT
(((i -' 1) + 1) + 1) div 2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
((((i -' 1) + 1) + 1) div 2) - 1 is V24() V25() V26() ext-real set
((i + 1) div 2) - 1 is V24() V25() V26() ext-real set
((i + 1) div 2) -' 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() V26() ext-real non negative Element of NAT
Seg (2 to_power (n + 1)) is finite 2 to_power (n + 1) -element Element of bool NAT
(n + 1) -BinarySequence (i -' 1) is Relation-like NAT -defined BOOLEAN -valued Function-like finite n + 1 -element FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
Rev ((n + 1) -BinarySequence (i -' 1)) is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
<*((i -' 1) mod 2)*> is Relation-like NAT -defined NAT -valued non empty Function-like finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
n -BinarySequence ((i -' 1) div 2) is Relation-like NAT -defined BOOLEAN -valued Function-like finite n -element FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
<*((i -' 1) mod 2)*> ^ (n -BinarySequence ((i -' 1) div 2)) is Relation-like NAT -defined non empty Function-like finite 1 + n -element FinSequence-like FinSubsequence-like set
1 + n is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() V26() ext-real positive non negative Element of NAT
Rev (<*((i -' 1) mod 2)*> ^ (n -BinarySequence ((i -' 1) div 2))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
n -BinarySequence (((i + 1) div 2) -' 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) div 2) -' 1)) is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of BOOLEAN
(Rev (n -BinarySequence (((i + 1) div 2) -' 1))) ^ <*((i + 1) mod 2)*> is Relation-like NAT -defined non empty Function-like finite FinSequence-like FinSubsequence-like set