:: TREES_2 semantic presentation

REAL is non empty non trivial non finite set

bool REAL is non empty non trivial non finite set

bool omega is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set

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

is Relation-like non empty non trivial non finite set

f . 1 is set

X is set

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

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

B is set

F1() is non empty Tree-like set
X is set

f is set

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

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

X is non empty Tree-like set
Y is non empty Tree-like set
B is set

B is set

X is non empty Tree-like set
Y is non empty Tree-like set

X is non empty Tree-like set

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

rng f is finite set

X is non empty Tree-like set
Y is non empty Tree-like set

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

X is non empty Tree-like set
Y is non empty Tree-like set
B is non empty Tree-like set

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

(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 non empty Tree-like set

X is non empty Tree-like set
bool X is non empty set
Y is Element of bool X

Y is Element of bool X
{ } is set
B is set

B is set

{ (Y ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : Y ^ <*b1*> in X } is set
B is set

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

{ } is set
f is set

X is non empty Tree-like set

(X,Y) is Element of bool X
bool X is non empty set
{ (Y ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : Y ^ <*b1*> in X } is set
B is set

X is non empty Tree-like set

B is (X)
Y /\ B is Element of bool X
bool X is non empty set

{} is functional non empty trivial finite V42() 1 -element set
the Element of Y /\ B is Element of Y /\ B

y is set

X is non empty Tree-like set

{ } is set
{ } is set
bool X is non empty set
X is non empty Tree-like set
f is non empty Tree-like set

(X,Y) is Element of bool X
bool X is non empty set
{ (Y ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : Y ^ <*b1*> in X } is set

(f,D) is Element of bool f
bool f is non empty set
{ (D ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : D ^ <*b1*> in f } is set
X is non empty Tree-like set
(X,1) is (X)
{ } is set

(X,Y) is Element of bool X
bool X is non empty set
{ (Y ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : Y ^ <*b1*> in X } is set
B is set

f . 1 is set

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

B is set

X is non empty Tree-like set
{ (X,b1) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : verum } is set
union { (X,b1) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : verum } is set
Y is set

(X,(len B)) is (X)
{ } is set
Y is set
B is set

(X,f) is (X)
{ } is set
X is non empty finite Tree-like set

{ (X,b1) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : b1 <= height X } is set
union { (X,b1) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : b1 <= height X } is set
Y is set

(X,(len B)) is finite (X)
{ } is set
Y is set
B is set

(X,f) is finite (X)
{ } is set
X is non empty Tree-like set
Y is (X)

{ } is set

(X,f) is (X)
{ } is set
F1() is non empty set
F2() is set
{ F3(b1) where b1 is Element of F1() : b1 in F2() } is set
card { F3(b1) where b1 is Element of F1() : b1 in F2() } is epsilon-transitive epsilon-connected ordinal cardinal set

dom X is set
rng X is set
Y is set
B is Element of F1()
F3(B) is set
X . B is set
F3() is finite set
F1() is non empty set
F2() is finite set
{ F4(b1) where b1 is Element of F1() : b1 in F2() } is set

card { F4(b1) where b1 is Element of F1() : b1 in F2() } is epsilon-transitive epsilon-connected ordinal cardinal set
X is non empty Tree-like set

(X,B) is Element of bool X
bool X is non empty set
{ (B ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : B ^ <*b1*> in X } is set
{ H1(b1) where b1 is ext-real V36() V37() Element of REAL : b1 in Seg Y } is set
{ (B ^ <*(b1 - 1)*>) where b1 is ext-real V36() V37() Element of REAL : b1 in Seg Y } is set
f is set

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

x is finite set

X is non empty Tree-like set

(X,Y) is Element of bool X
bool X is non empty set
{ (Y ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : Y ^ <*b1*> in X } is set

f is finite set

X is non empty Tree-like () set

(X,Y) is Element of bool X
bool X is non empty set
{ (Y ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : Y ^ <*b1*> in X } is set
X is non empty Tree-like set
bool X is non empty set
Y is Element of bool X

X is non empty Tree-like set
bool X is non empty set
Y is Element of bool X

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 set
union B is set
f is set
D is set
f is Element of bool X

g is set
y is set

x is set

B is set
f is (X)

() \/ {D} is non empty finite set
g is Element of bool X

y is set

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

X is non empty Tree-like set

f is (X)

X is non empty Tree-like set

D is (X)

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

B is finite (X)

the Element of B is Element of B

bool is non empty non trivial non finite set

B \ () is finite Element of bool X
bool X is non empty set
the Element of B \ () is Element of B \ ()

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

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

X is non empty Tree-like set
Y is (X)
{ } is set
B is set

bool X is non empty set
B is Element of bool X

X is non empty Tree-like set

f is non empty (X) (X)

X is non empty Tree-like set
Y is non empty (X) (X)
the Element of Y is Element of Y

X is non empty Tree-like set

f is (X)

X is non empty Tree-like set
Y is (X)
bool X is non empty set
B is set
{ } is set
D is set

g is set

D is set
union D is set
x is set
g is set
x is Element of bool X

y is set
T1 is set

y is set

the Element of D is Element of D
D is set
x is (X)

() \/ {g} is non empty finite set
y is Element of bool X

T1 is set

g is non empty (X) (X)
F1() is set
X is set

X is set
X /\ NAT is Element of bool REAL

X /\ NAT is Element of bool REAL
Y is finite set
B is set

f is set

B is set

f is set

D is set

B is set

X /\ NAT is Element of bool REAL

F2() is set
F1() is set
X is set
Y is set
B is set

dom Y is set

dom B is set
B . 0 is set
rng B is set

B . f is set

B . (f + 1) is set
Y . (B . f) is set
f is set
D is set
B . D is set

B . x is set

B . f is set

B . (f + 1) is set
Y . (B . f) is set
X is non empty Tree-like set

(X,Y) is Element of bool X
bool X is non empty set
{ (Y ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : Y ^ <*b1*> in X } is set
B is set

x is non empty (X) (X)

dom B is set
rng B is set

D is non empty (X) (X)

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

bool is non empty non trivial non finite set

y . 1 is set

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

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

f is finite (X)

D is non empty (X) (X)

B is set

x is set

dom B is set
rng B is set
B . 0 is set

dom B is set
rng B is set
B . 0 is set
bool X is non empty set

B . D is set

B . (D + 0) is set

B . (D + x) is set

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

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

B . (y + T1) is set

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

B . D is set
B . x is set

f is Element of bool X

g is set
B . g is set
y is set
B . y is set

D is (X)

B . x is set

B . (x + 1) is set

x is set
B . x is set
g is set
B . g is set

B . y is set

B . (y + 1) is set

B . y is set

B . (y + 1) is set

X is non empty Tree-like () set

(X,Y) is finite Element of bool X
bool X is non empty set
{ (Y ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : Y ^ <*b1*> in X } is set
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

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

X is non empty set

dom Y is non empty Tree-like set

Y . B is set
rng Y is Element of bool X
bool X is non empty set

dom X is non empty Tree-like set

dom Y is non empty Tree-like set
B is set

X . f is set
Y . f is set
X . B is set
Y . B is set
F1() is non empty Tree-like set
X is set

B is set

dom X is set

dom Y is non empty Tree-like set

Y . B is set
F1() is non empty Tree-like set

dom X is set

dom Y is non empty Tree-like set

Y . B is set
F2(B) is 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

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

dom B is non empty Tree-like set

dom f is non empty Tree-like set

B . D is set

X . (Y ^ D) is set
f . D is 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

Y . (X ^ D) is set
X is non empty 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

dom Y is non empty Tree-like set

(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

dom X is non empty Tree-like set

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

X . f is set

B . D is set

B . () is set

D is set

x is set
B . g is set

dom f is non empty Tree-like set

dom D is non empty Tree-like set

f . x is set
D . x is set
X . x is set

B . g is set

B . y is set
X is non empty Tree-like set
Y is set

{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

D is set
x is non empty Tree-like set

g is set
y is non empty Tree-like set
X is set
union X is set
Y is set
B is 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

X is non empty set
union X is set
Y is set
B is set

dom f is non empty Tree-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

dom g is non empty Tree-like set
union f is set

dom Y is set
D is set
x is set
[D,x] is set
{D,x} is non empty finite set