:: TREES_2 semantic presentation

REAL is non empty non trivial non finite set

NAT is epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal Element of bool REAL

bool REAL is non empty non trivial non finite set

omega is epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal set

bool omega is non empty non trivial non finite set

bool NAT is non empty non trivial non finite set

{} is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty Function-yielding V32() ext-real non positive non negative V36() V37() finite finite-yielding V42() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set

the Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty Function-yielding V32() ext-real non positive non negative V36() V37() finite finite-yielding V42() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty Function-yielding V32() ext-real non positive non negative V36() V37() finite finite-yielding V42() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set

1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT

2 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT

3 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT

0 is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty Function-yielding V32() ext-real non positive non negative V36() V37() finite finite-yielding V42() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT

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

NAT * is functional non empty FinSequence-membered FinSequenceSet of NAT

<*> NAT is Relation-like non-empty empty-yielding NAT -defined NAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty proper Function-yielding V32() ext-real non positive non negative V36() V37() finite finite-yielding V42() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of NAT

[:NAT,NAT:] is Relation-like non empty non trivial non finite set

union {} is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal set

card {} is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty Function-yielding V32() ext-real non positive non negative V36() V37() finite finite-yielding V42() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set

X is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

B is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

Y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len X is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

len Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

X ^ f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

Y ^ D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

X ^ f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

Y ^ D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

X is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

B is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

Y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

X is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

X + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT

Y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

Seg X is finite X -element Element of bool NAT

Y | (Seg X) is Relation-like NAT -defined Seg X -defined NAT -defined Function-like finite FinSubsequence-like set

B is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

B ^ f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

f . 1 is set

<*(f . 1)*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set

B ^ <*(f . 1)*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set

len f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

X + (len f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

X is set

<*X*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set

Y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

Y ^ <*X*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set

ProperPrefixes (Y ^ <*X*>) is finite set

ProperPrefixes Y is finite set

{Y} is functional non empty trivial finite V42() 1 -element set

(ProperPrefixes Y) \/ {Y} is non empty finite set

B is set

f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

B is set

f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

Y ^ {} is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

F

X is set

card X is epsilon-transitive epsilon-connected ordinal cardinal set

X is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F

len X is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

X is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

X + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT

Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F

len Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

B is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

f is set

<*f*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set

B ^ <*f*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set

len B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

rng <*f*> is non empty trivial finite 1 -element set

rng Y is finite Element of bool NAT

{f} is non empty trivial finite 1 -element set

x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F

g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

X is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F

len X is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

X is non empty Tree-like set

Y is non empty Tree-like set

B is set

f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X

B is set

f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of Y

X is non empty Tree-like set

Y is non empty Tree-like set

B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

X is non empty Tree-like set

Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

X | Y is non empty Tree-like set

X with-replacement (Y,(X | Y)) is non empty Tree-like set

B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

Y ^ f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng f is finite set

rng B is finite Element of bool NAT

D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

Y ^ x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

Y ^ f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

Y ^ f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

X is non empty Tree-like set

Y is non empty Tree-like set

B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

X with-replacement (B,Y) is non empty Tree-like set

f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

X is non empty Tree-like set

Y is non empty Tree-like set

B is non empty Tree-like set

f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

X with-replacement (f,Y) is non empty Tree-like set

D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

(X with-replacement (f,Y)) with-replacement (D,B) is non empty Tree-like set

X with-replacement (D,B) is non empty Tree-like set

(X with-replacement (D,B)) with-replacement (f,Y) is non empty Tree-like set

x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

D ^ g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

f ^ g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

D ^ y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

f ^ g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

f ^ g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

D ^ g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

f ^ y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

D ^ g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

{{}} is functional non empty trivial finite V42() 1 -element Tree-like set

X is non empty Tree-like set

<*0*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X

Y ^ <*0*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT

X is non empty Tree-like set

bool X is non empty set

Y is Element of bool X

B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

{{}} is functional non empty trivial finite V42() 1 -element Tree-like set

Y is Element of bool X

{ b

B is set

len {} is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty Function-yielding V32() ext-real non positive non negative V36() V37() finite finite-yielding V42() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT

B is set

f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X

len f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X

{ (Y ^ <*b

B is set

f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

<*f*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

Y ^ <*f*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT

X is non empty Tree-like set

Y is (X)

B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal set

{ b

f is set

f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X

len x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X

len g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

X is non empty Tree-like set

Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X

(X,Y) is Element of bool X

bool X is non empty set

{ (Y ^ <*b

B is set

f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

<*f*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

Y ^ <*f*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT

B is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

len Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

(len Y) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT

D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

<*D*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

Y ^ <*D*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT

len f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

<*D*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

Y ^ <*D*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT

X is non empty Tree-like set

Y is AntiChain_of_Prefixes-like AntiChain_of_Prefixes of X

B is (X)

Y /\ B is Element of bool X

bool X is non empty set

f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

the Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X

{ the Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X} is functional non empty trivial finite V42() 1 -element set

the Element of Y /\ B is Element of Y /\ B

x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X

g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X

{g} is functional non empty trivial finite V42() 1 -element set

y is set

y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X

{D} is functional non empty trivial finite V42() 1 -element set

X is non empty Tree-like set

Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal set

{ b

{ b

bool X is non empty set

X is non empty Tree-like set

f is non empty Tree-like set

Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X

B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

<*B*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

Y ^ <*B*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT

(X,Y) is Element of bool X

bool X is non empty set

{ (Y ^ <*b

D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of f

x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

<*x*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

D ^ <*x*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT

(f,D) is Element of bool f

bool f is non empty set

{ (D ^ <*b

X is non empty Tree-like set

(X,1) is (X)

{ b

Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X

(X,Y) is Element of bool X

bool X is non empty set

{ (Y ^ <*b

B is set

f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X

len f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

f . 1 is set

<*(f . 1)*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set

rng f is finite Element of bool NAT

{(f . 1)} is non empty trivial finite 1 -element set

D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

<*D*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

Y ^ <*D*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT

B is set

f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

<*f*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

Y ^ <*f*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT

len <*f*> is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT

D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X

X is non empty Tree-like set

{ (X,b

union { (X,b

Y is set

B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X

len B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

(X,(len B)) is (X)

{ b

Y is set

B is set

f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

(X,f) is (X)

{ b

X is non empty finite Tree-like set

height X is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

{ (X,b

union { (X,b

Y is set

B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X

len B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

(X,(len B)) is finite (X)

{ b

Y is set

B is set

f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

(X,f) is finite (X)

{ b

X is non empty Tree-like set

Y is (X)

B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal set

{ b

f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

(X,f) is (X)

{ b

F

F

{ F

card { F

card F

X is Relation-like Function-like set

dom X is set

rng X is set

Y is set

B is Element of F

F

X . B is set

F

F

F

{ F

card F

card F

card { F

X is non empty Tree-like set

Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

<*Y*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

Seg Y is finite Y -element Element of bool NAT

B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X

(X,B) is Element of bool X

bool X is non empty set

{ (B ^ <*b

{ H

{ (B ^ <*(b

f is set

D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

<*D*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

B ^ <*D*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT

B ^ <*Y*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT

D + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT

(D + 1) - 1 is ext-real V36() V37() Element of REAL

f is finite set

card f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of omega

x is finite set

card x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of omega

card (Seg Y) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of omega

X is non empty Tree-like set

Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X

(X,Y) is Element of bool X

bool X is non empty set

{ (Y ^ <*b

B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

f is finite set

card f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of omega

X is non empty Tree-like () set

Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X

(X,Y) is Element of bool X

bool X is non empty set

{ (Y ^ <*b

X is non empty Tree-like set

bool X is non empty set

Y is Element of bool X

B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

{{}} is functional non empty trivial finite V42() 1 -element Tree-like set

X is non empty Tree-like set

bool X is non empty set

Y is Element of bool X

B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

X is non empty Tree-like set

X is non empty Tree-like set

X is non empty Tree-like set

bool X is non empty set

Y is set

B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

ProperPrefixes B is finite set

B is set

union B is set

f is set

D is set

f is Element of bool X

D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

g is set

y is set

D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

x is set

ProperPrefixes D is finite set

B is set

f is (X)

D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

ProperPrefixes D is finite set

D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

ProperPrefixes D is finite set

{D} is functional non empty trivial finite V42() 1 -element set

(ProperPrefixes D) \/ {D} is non empty finite set

g is Element of bool X

y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

ProperPrefixes y is finite set

y is set

y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X

X is non empty Tree-like set

Y is (X)

the Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X

f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

X is non empty Tree-like set

Y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

B is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

ProperPrefixes B is finite set

f is (X)

D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X

x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X

X is non empty Tree-like set

Y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

B is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

ProperPrefixes f is finite set

D is (X)

ProperPrefixes B is finite set

X is non empty Tree-like set

Y is (X)

X is non empty Tree-like set

Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

B is finite (X)

card B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of omega

the Element of B is Element of B

D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X

x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

len x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

f + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT

D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

len D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

len D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

Seg f is finite f -element Element of bool NAT

D | (Seg f) is Relation-like NAT -defined Seg f -defined NAT -defined NAT -valued Function-like finite FinSubsequence-like Element of bool [:NAT,NAT:]

bool [:NAT,NAT:] is non empty non trivial non finite set

x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

ProperPrefixes x is finite set

card (ProperPrefixes x) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of omega

B \ (ProperPrefixes x) is finite Element of bool X

bool X is non empty set

the Element of B \ (ProperPrefixes x) is Element of B \ (ProperPrefixes x)

y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X

{y} is functional non empty trivial finite V42() 1 -element set

(ProperPrefixes x) \/ {y} is non empty finite set

card ((ProperPrefixes x) \/ {y}) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of omega

B \ ((ProperPrefixes x) \/ {y}) is finite Element of bool X

the Element of B \ ((ProperPrefixes x) \/ {y}) is Element of B \ ((ProperPrefixes x) \/ {y})

T1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X

len y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

len T1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

X is non empty Tree-like set

Y is (X)

{ b

( b

B is set

f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X

D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

bool X is non empty set

B is Element of bool X

f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X

g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X

y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

X is non empty Tree-like set

Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

f is non empty (X) (X)

ProperPrefixes B is finite set

X is non empty Tree-like set

Y is non empty (X) (X)

the Element of Y is Element of Y

f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X

X is non empty Tree-like set

Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

len Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

len B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

f is (X)

ProperPrefixes Y is finite set

X is non empty Tree-like set

Y is (X)

bool X is non empty set

B is set

{ b

( b

D is set

x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X

D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X

g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

ProperPrefixes D is finite set

g is set

y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X

T1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

D is set

union D is set

x is set

g is set

x is Element of bool X

g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

y is set

T1 is set

g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

y is set

ProperPrefixes g is finite set

the Element of D is Element of D

D is set

x is (X)

g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

ProperPrefixes g is finite set

g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

ProperPrefixes g is finite set

{g} is functional non empty trivial finite V42() 1 -element set

(ProperPrefixes g) \/ {g} is non empty finite set

y is Element of bool X

T1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

k1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

T1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

ProperPrefixes T1 is finite set

T1 is set

k1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X

g is non empty (X) (X)

F

X is set

Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal set

B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

X is set

X /\ NAT is Element of bool REAL

Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

X /\ NAT is Element of bool REAL

Y is finite set

B is set

D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

f is set

x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

B is set

x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

f is set

g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

D is set

y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

B is set

f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

X /\ NAT is Element of bool REAL

Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

F

F

X is set

Y is set

B is set

Y is Relation-like Function-like set

dom Y is set

B is Relation-like Function-like set

dom B is set

B . 0 is set

rng B is set

f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

B . f is set

f + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT

B . (f + 1) is set

Y . (B . f) is set

f is set

D is set

B . D is set

x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

B . x is set

f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

B . f is set

f + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT

B . (f + 1) is set

Y . (B . f) is set

X is non empty Tree-like set

Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X

len Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

(X,Y) is Element of bool X

bool X is non empty set

{ (Y ^ <*b

B is set

f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

<*f*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

Y ^ <*f*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT

len (Y ^ <*f*>) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT

D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

(len (Y ^ <*f*>)) + D is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT

g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

x is non empty (X) (X)

y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

len g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

(len g) + D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

len y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

B is Relation-like Function-like set

dom B is set

rng B is set

f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

f + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT

(len Y) + (f + 1) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT

D is non empty (X) (X)

x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

len x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

len x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

(len Y) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT

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

x | (Seg ((len Y) + 1)) is Relation-like NAT -defined Seg ((len Y) + 1) -defined NAT -defined NAT -valued Function-like finite FinSubsequence-like Element of bool [:NAT,NAT:]

bool [:NAT,NAT:] is non empty non trivial non finite set

((len Y) + 1) + f is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT

g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

len g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

Y ^ y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

(len Y) + (len y) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

y . 1 is set

<*(y . 1)*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set

dom g is finite Element of bool NAT

Seg (len g) is finite len g -element Element of bool NAT

1 + (len Y) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT

Y ^ <*(y . 1)*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set

(Y ^ <*(y . 1)*>) . ((len Y) + 1) is set

rng g is finite Element of bool NAT

y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

<*y*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

Y ^ <*y*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT

B . (Y ^ <*y*>) is set

T1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

(len g) + T1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X

len Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

(len Y) + B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

B + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT

f is finite (X)

card f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of omega

D is non empty (X) (X)

B + 0 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

len x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

B is set

f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X

len f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

<*D*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

f ^ <*D*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT

len (f ^ <*D*>) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT

x is set

g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X

len g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

(len g) + y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

B is Relation-like Function-like set

dom B is set

rng B is set

B . 0 is set

B is Relation-like Function-like set

dom B is set

rng B is set

B . 0 is set

bool X is non empty set

D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal set

B . D is set

D + 0 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal set

B . (D + 0) is set

x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal set

D + x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal set

B . (D + x) is set

x + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT

D + (x + 1) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal set

B . (D + (x + 1)) is set

g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

D + (x + 1) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT

B . (D + (x + 1)) is set

y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

T1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

y + T1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

B . (y + T1) is set

(y + T1) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT

B . ((y + T1) + 1) is set

k1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

T2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

<*T2*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

k1 ^ <*T2*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT

D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

B . D is set

B . x is set

g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal set

D + y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

f is Element of bool X

D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

g is set

B . g is set

y is set

B . y is set

y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

T1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

D is (X)

x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

len x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

B . x is set

x + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT

B . (x + 1) is set

g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

len g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

<*y*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

y ^ <*y*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT

len y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

len <*y*> is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT

(len y) + (len <*y*>) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT

(len y) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT

x is set

B . x is set

g is set

B . g is set

y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

B . y is set

y + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT

B . (y + 1) is set

T1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

k1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

<*k1*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

T1 ^ <*k1*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT

y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

B . y is set

y + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT

B . (y + 1) is set

len T1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

T2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

k2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

<*k2*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

T2 ^ <*k2*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT

X is non empty Tree-like () set

Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X

(X,Y) is finite Element of bool X

bool X is non empty set

{ (Y ^ <*b

the non empty Tree-like set is non empty Tree-like set

[: the non empty Tree-like set ,NAT:] is Relation-like non empty non trivial non finite set

bool [: the non empty Tree-like set ,NAT:] is non empty non trivial non finite set

the non empty Tree-like set --> 0 is Relation-like the non empty Tree-like set -defined NAT -valued Function-like constant non empty total V25( the non empty Tree-like set , NAT ) Function-yielding V32() Element of bool [: the non empty Tree-like set ,NAT:]

Y is Relation-like the non empty Tree-like set -defined NAT -valued Function-like constant non empty total V25( the non empty Tree-like set , NAT ) Function-yielding V32() Element of bool [: the non empty Tree-like set ,NAT:]

dom Y is non empty Element of bool the non empty Tree-like set

bool the non empty Tree-like set is non empty set

X is Relation-like Function-like () set

dom X is set

X is non empty set

the non empty Tree-like set is non empty Tree-like set

the Element of X is Element of X

the non empty Tree-like set --> the Element of X is Relation-like the non empty Tree-like set -defined X -valued Function-like constant non empty total V25( the non empty Tree-like set ,X) Element of bool [: the non empty Tree-like set ,X:]

[: the non empty Tree-like set ,X:] is Relation-like non empty set

bool [: the non empty Tree-like set ,X:] is non empty set

dom ( the non empty Tree-like set --> the Element of X) is non empty Element of bool the non empty Tree-like set

bool the non empty Tree-like set is non empty set

D is Relation-like Function-like () set

X is non empty set

Y is Relation-like X -valued Function-like () set

dom Y is non empty Tree-like set

B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom Y

Y . B is set

rng Y is Element of bool X

bool X is non empty set

X is Relation-like Function-like () set

dom X is non empty Tree-like set

Y is Relation-like Function-like () set

dom Y is non empty Tree-like set

B is set

f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom X

X . f is set

Y . f is set

X . B is set

Y . B is set

F

X is set

Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F

B is set

X is Relation-like Function-like set

dom X is set

Y is Relation-like Function-like () set

dom Y is non empty Tree-like set

B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

Y . B is set

F

X is Relation-like Function-like set

dom X is set

Y is Relation-like Function-like () set

dom Y is non empty Tree-like set

B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

Y . B is set

F

X is Relation-like Function-like () set

dom X is non empty Tree-like set

Leaves (dom X) is Element of bool (dom X)

bool (dom X) is non empty set

X .: (Leaves (dom X)) is set

Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

(dom X) | Y is non empty Tree-like set

B is Relation-like Function-like () set

dom B is non empty Tree-like set

f is Relation-like Function-like () set

dom f is non empty Tree-like set

D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

B . D is set

Y ^ D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

X . (Y ^ D) is set

f . D is set

X is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

Y is Relation-like Function-like () set

dom Y is non empty Tree-like set

(Y,X) is Relation-like Function-like () set

rng (Y,X) is set

rng Y is set

B is set

dom (Y,X) is non empty Tree-like set

f is set

(Y,X) . f is set

(dom Y) | X is non empty Tree-like set

D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom (Y,X)

X ^ D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

Y . (X ^ D) is set

X is non empty set

Y is Relation-like X -valued Function-like () set

(Y) is set

dom Y is non empty Tree-like set

Leaves (dom Y) is Element of bool (dom Y)

bool (dom Y) is non empty set

Y .: (Leaves (dom Y)) is set

bool X is non empty set

rng Y is Element of bool X

X is non empty set

Y is Relation-like X -valued Function-like () set

dom Y is non empty Tree-like set

B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom Y

(Y,B) is Relation-like Function-like () set

rng (Y,B) is set

rng Y is Element of bool X

bool X is non empty set

Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

X is Relation-like Function-like () set

dom X is non empty Tree-like set

B is Relation-like Function-like () set

dom B is non empty Tree-like set

(dom X) with-replacement (Y,(dom B)) is non empty Tree-like set

f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

X . f is set

D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

Y ^ D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

B . D is set

{} NAT is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty proper Function-yielding V32() ext-real non positive non negative V36() V37() finite finite-yielding V42() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Element of bool NAT

B . ({} NAT) is set

Y ^ (<*> NAT) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

D is set

g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

Y ^ g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

x is set

B . g is set

f is Relation-like Function-like () set

dom f is non empty Tree-like set

D is Relation-like Function-like () set

dom D is non empty Tree-like set

x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

f . x is set

D . x is set

X . x is set

g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

Y ^ g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

B . g is set

y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

Y ^ y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

B . y is set

X is non empty Tree-like set

Y is set

X --> Y is Relation-like X -defined {Y} -valued Function-like constant non empty total V25(X,{Y}) Element of bool [:X,{Y}:]

{Y} is non empty trivial finite 1 -element set

[:X,{Y}:] is Relation-like non empty set

bool [:X,{Y}:] is non empty set

dom (X --> Y) is non empty Element of bool X

bool X is non empty set

X is non empty set

union X is set

the Element of X is Element of X

Y is non empty Tree-like set

B is non empty set

f is set

f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

ProperPrefixes f is finite set

D is set

x is non empty Tree-like set

f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

<*D*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

f ^ <*D*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT

x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT

<*x*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

f ^ <*x*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT

g is set

y is non empty Tree-like set

X is set

union X is set

Y is set

B is set

f is Relation-like Function-like set

Y is set

B is set

[Y,B] is set

{Y,B} is non empty finite set

{Y} is non empty trivial finite 1 -element set

{{Y,B},{Y}} is non empty finite V42() set

f is set

[Y,f] is set

{Y,f} is non empty finite set

{{Y,f},{Y}} is non empty finite V42() set

D is set

x is set

g is Relation-like Function-like set

y is Relation-like Function-like set

X is non empty set

union X is set

Y is set

B is set

f is Relation-like Function-like () set

dom f is non empty Tree-like set

B is Relation-like Function-like set

dom B is set

rng B is set

D is set

f is non empty set

x is set

B . x is set

g is Relation-like Function-like () set

dom g is non empty Tree-like set

union f is set

Y is Relation-like Function-like set

dom Y is set

D is set

x is set

[D,x] is set

{D,x} is non empty finite set