:: TREES_1 semantic presentation

REAL is set

K40(REAL) is set

K40(omega) is V18() non finite set
K40(NAT) is V18() non finite set

Seg 1 is non empty V18() finite 1 -element Element of K40(NAT)

dom D is finite Element of K40(NAT)

Seg a is finite a -element Element of K40(NAT)

Seg k is finite k -element Element of K40(NAT)

Seg a is finite a -element Element of K40(NAT)

Seg a is finite a -element Element of K40(NAT)

dom D is finite Element of K40(NAT)

Seg (len D) is finite len D -element Element of K40(NAT)

D is set

f is set

<*D*> . 1 is set
D is finite set
f is finite set

f \ D is finite Element of K40(f)
K40(f) is finite V37() set

(card f) - (card D) is ext-real V16() V20() set
D is finite set
f is finite set

D is set

f is set

<*D*> . 1 is set
D is finite set
f is finite set

D is set

((len f) + ()) + (len k) is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

((len f) + 1) + (len k) is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
D is set

((len a) + ()) + (len k) is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

((len a) + 1) + (len k) is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
D is set

rng D is finite set
(rng D) * is non empty functional FinSequence-membered FinSequenceSet of rng D
a is set
k is set

rng x is finite set

Seg y is finite y -element Element of K40(NAT)

f is set
a is set
k is set
x is set

k is set
x is set

D is set

(f) is set

(f) is set

(f) is set

(D) is set
({}) is set
the Element of ({}) is Element of ({})

is non empty V18() functional finite V37() 1 -element set
f is set

(<*f*>) is set
a is set

a is set

(f) is set
(a) is set
k is set

(f) is set

Seg x is finite x -element Element of K40(NAT)

Seg y is finite y -element Element of K40(NAT)

f is set

(f) is set

{()} is non empty V18() functional finite V37() 1 -element set
f is non empty V18() functional finite V37() 1 -element set
f is set
a is non empty () set
f is non empty () set
a is Element of f
f is non empty () set

(x) is set
(a) is set

a is non empty () set

Seg (len f) is finite len f -element Element of K40(NAT)

dom f is finite Element of K40(NAT)
x . z is set
f . z is set
y . z is set
(x) is set

f is non empty () set

f is non empty () set
a is non empty () set
f \/ a is non empty set

(x) is set

f /\ a is set

(x) is set

f is non empty () set
a is non empty () set
f \/ a is non empty () set
f is non empty () set
a is non empty () set
f /\ a is non empty () set
f is non empty finite () set
a is non empty finite () set
f \/ a is non empty finite () set
a is non empty finite () set
f is non empty () set
a /\ f is non empty finite () set

{ <*b1*> where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : not f <= b1 } is set
{ <*b1*> where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : not f <= b1 } \/ is non empty set
k is set

(k) is set

<*x*> . 1 is set

(f) is non empty () set
{ <*b1*> where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : not f <= b1 } is set
{ <*b1*> where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : not f <= b1 } \/ is non empty set

Seg (f + 1) is non empty finite f + 1 -element Element of K40(NAT)
k is set
x is set
y is set

<*z*> . 1 is set

k is set

y is set
z is set
x is set
y is set
x is set

y is set

x is set

x is set

dom k is set
rng k is set
x is set
k . x is set
y is set
k . y is set

x is set
y is set
k . y is set

<*z*> . 1 is set
<*x*> . 1 is set

x is set

k . {} is set

k . <*x*> is set

(a) is non empty finite () set
{ <*b1*> where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : not a <= b1 } is set
{ <*b1*> where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : not a <= b1 } \/ is non empty set
(0) is non empty finite () set
{ <*b1*> where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : not 0 <= b1 } is set
{ <*b1*> where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : not 0 <= b1 } \/ is non empty set
the Element of { <*b1*> where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : not 0 <= b1 } is Element of { <*b1*> where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : not 0 <= b1 }

(f) is non empty finite () set
{ <*b1*> where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : not f <= b1 } is set
{ <*b1*> where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : not f <= b1 } \/ is non empty set

f is non empty () set
K40(f) is set
a is set
k is set
k is Element of K40(f)

a is Element of K40(f)
k is Element of K40(f)
x is set

k is set

x is non empty set
y is set

(y) is set
z is set

Seg m is finite m -element Element of K40(NAT)

Seg m is finite m -element Element of K40(NAT)

y is non empty () set

k is non empty () set
x is non empty () set
y is set

f is non empty () set
(f,()) is non empty () set
a is set

a is set

f is non empty finite () set

(f,a) is non empty () set

rng k is set
dom k is set
x is set
k . x is set

z is set

dom x is set
rng x is set
y is set
z is set
x . z is set
k . z is set

y is set

x is set
k . x is set
x . x is set

f is non empty () set
(f) is Element of K40(f)
K40(f) is set
the Element of (f) is Element of (f)

f is non empty () set

f is non empty () set
k is non empty () set

{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (f) : not a c< b1 } is set
{ (a ^ b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (k) : b1 = b1 } is set
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (f) : not a c< b1 } \/ { (a ^ b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (k) : b1 = b1 } is set
z is set

y is non empty set
z is set

(z) is set

x is set

x is set

dom r is finite Element of K40(NAT)

Seg (len r) is finite len r -element Element of K40(NAT)

dom m is finite Element of K40(NAT)

Seg (len m) is finite len m -element Element of K40(NAT)

dom m is finite Element of K40(NAT)

Seg (len m) is finite len m -element Element of K40(NAT)

z is non empty () set

x is non empty () set
y is non empty () set
z is set

z is set

a is non empty () set
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (a) : not f c< b1 } is set
k is non empty () set
(a,f,k) is non empty () set
{ (f ^ b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (k) : b1 = b1 } is set
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (a) : not f c< b1 } \/ { (f ^ b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (k) : b1 = b1 } is set
x is set

x is set

a is non empty () set
k is non empty () set
(a,f,k) is non empty () set
((a,f,k),f) is non empty () set
x is set

x is set

f is non empty finite () set

k is non empty finite () set
(f,a,k) is non empty () set
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (f) : not a c< b1 } is set
x is set

{ (a ^ b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (k) : b1 = b1 } is set
x is set

dom x is set
rng x is set
y is set
x . y is set
z is set
x . z is set

y is set
z is set
x . z is set

y is set

x . z is set

{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (f) : not a c< b1 } \/ { (a ^ b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (k) : b1 = b1 } is set

(f) is set
dom f is finite Element of K40(NAT)
a is set

x is set

dom a is set
rng a is set
k is set
a . k is set
x is set
a . x is set

k is set
x is set
a . x is set

Seg (len f) is finite len f -element Element of K40(NAT)
k is set

Seg (len f) is finite len f -element Element of K40(NAT)

Seg z is finite z -element Element of K40(NAT)

a . x is set

(f) is set
dom f is finite Element of K40(NAT)

(f) is finite set

dom f is finite Element of K40(NAT)
Seg (len f) is finite len f -element Element of K40(NAT)

f is set

{f} is non empty V18() functional finite V37() 1 -element set
a is set

{f,a} is non empty functional finite V37() set
k is set

f is non empty () set

{} is non empty V18() functional finite V37() 1 -element set
k is () set
x is set
f is non empty () set
a is set

a is () set
k is () set
x is set
f is non empty () set

{a} is non empty V18() functional finite V37() 1 -element set
k is () set
x is set
f is non empty () set

{a,k} is non empty functional finite V37() set
x is () set
y is set
f is non empty finite () set
a is () (f)
f is non empty finite () set

Seg a is finite a -element Element of K40(NAT)

(k) is finite set
dom k is finite Element of K40(NAT)

card (dom k) is