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

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

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

i is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like (T)

{ b

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

F

[:F

T is set

n is Element of F

i is Element of F

[n,i] is V13() Element of [: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

T is Relation-like Function-like set

proj1 T is set

proj2 T is set

[:F

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

bool [:[:F

n is Relation-like [:F

i is Relation-like F

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

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

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

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

{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

F

[:F

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

dp is Element of F

T is Relation-like Function-like set

proj1 T is set

proj2 T is set

[:[:F

bool [:[:F

n is Relation-like [:F

i is Relation-like F

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

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

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

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

[(F . dp),0] is V13() Element of [:F

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

n . [(F . dp),0] is Element of F

n . ((F . dp),0) is Element of F

[(F . dp),0] is V13() set

n . [(F . dp),0] is set

[(F . dp),1] is V13() Element of [:F

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

i is set

{ b

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

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

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

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

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

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

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

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

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

{ b

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

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

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

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

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

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

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

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

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

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

(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

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

{ b

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

(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

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

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

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

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

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

x2 is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like (T)

len x2 is epsilon-transit