:: MODAL_1 semantic presentation

REAL is set

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

bool REAL is non empty set

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

bool NAT 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 Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V28() V29() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding set

the Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V28() V29() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding set is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V28() V29() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding set

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

{{},1} is non empty finite V37() set

Trees is non empty constituted-Trees set

bool Trees is non empty set

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

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

0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V28() V29() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding Element of NAT

ProperPrefixes {} is finite set

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

NAT * is functional non empty FinSequence-membered M8( NAT )

<*> NAT is Relation-like non-empty empty-yielding NAT -defined NAT -valued Function-like one-to-one constant functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V28() V29() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding FinSequence of NAT

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

elementary_tree 0 is non empty finite Tree-like set

elementary_tree 1 is non empty finite 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

{{},<*0*>} is functional non empty finite V37() set

elementary_tree 2 is non empty finite Tree-like set

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

{{},<*0*>,<*1*>} is non empty finite set

card {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V28() V29() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding set

[:NAT,NAT:] is Relation-like REAL -defined REAL -valued non empty non trivial non finite Element of bool [:REAL,REAL:]

[:REAL,REAL:] is Relation-like set

bool [:REAL,REAL:] is non empty set

F is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() 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

F is non empty Tree-like set

F is non empty set

F is Relation-like F -valued Function-like DecoratedTree-like set

proj1 F is non empty Tree-like set

((proj1 F)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 F

F . ((proj1 F)) is Element of F

F is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() 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

F is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() 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

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

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

(<*F*> ^ A) . 1 is set

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

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

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

(<*F*> ^ A) ^ G is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set

((<*F*> ^ A) ^ G) . 1 is set

A ^ G is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

<*F*> ^ (A ^ G) is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set

(<*F*> ^ (A ^ G)) . 1 is set

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

F is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() 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

F is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() 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

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

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

(<*F*> ^ A) . 1 is set

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

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

F is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

F is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() 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

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

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

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

F is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() 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

F is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() 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

F is non empty Tree-like set

A is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

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

G is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

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

{} ^ <*G*> is Relation-like NAT -defined Function-like non empty finite {} + 1 -element FinSequence-like FinSubsequence-like set

{} + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT

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

F ^ <*A*> is Relation-like NAT -defined NAT -valued Function-like non empty 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

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

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

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

F ^ A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

PFuncs ((NAT *),[:NAT,NAT:]) is set

F is Relation-like [:NAT,NAT:] -valued Function-like DecoratedTree-like set

rng F is Relation-like NAT -defined NAT -valued Element of bool [:NAT,NAT:]

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

proj1 F is non empty Tree-like set

F is non empty Tree-like set

F is non empty Tree-like set

A is non empty Tree-like set

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

F with-replacement (G,F) is non empty Tree-like set

F with-replacement (G,A) is non empty Tree-like set

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

G ^ A 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

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

G ^ A 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

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

F is non empty set

F is Relation-like F -valued Function-like DecoratedTree-like set

proj1 F is non empty Tree-like set

A is Relation-like F -valued Function-like DecoratedTree-like set

G is Relation-like F -valued Function-like DecoratedTree-like set

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

F with-replacement (A,A) is Relation-like Function-like DecoratedTree-like set

F with-replacement (A,G) is Relation-like Function-like DecoratedTree-like set

proj1 (F with-replacement (A,A)) is non empty Tree-like set

proj1 A is non empty Tree-like set

(proj1 F) with-replacement (A,(proj1 A)) is non empty Tree-like set

proj1 G is non empty Tree-like set

(proj1 F) with-replacement (A,(proj1 G)) is non empty Tree-like set

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

A . k2 is set

G . k2 is set

A ^ k2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

(F with-replacement (A,A)) . (A ^ k2) is set

(F with-replacement (A,G)) . (A ^ k2) is set

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

A ^ A1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

G . A1 is set

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

A ^ G is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

A . G is set

proj1 (F with-replacement (A,G)) is non empty Tree-like set

F is non empty Tree-like set

F is non empty Tree-like set

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

F with-replacement (A,F) is non empty Tree-like set

A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F with-replacement (A,F)

succ A is Element of bool (F with-replacement (A,F))

bool (F with-replacement (A,F)) is non empty set

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

succ B is Element of bool F

bool F is non empty set

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

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

k2 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal set

dom k1 is finite Element of bool NAT

len B is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

(len B) + k2 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

dom A is finite Element of bool NAT

A . ((len B) + k2) is set

rng A is finite Element of bool NAT

k1 . k2 is set

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

A1 is set

{ (A ^ <*b

G is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

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

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

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

{ (B ^ <*b

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

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

A ^ a is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

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

A ^ a is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

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

k2 ^ a is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

B ^ (k2 ^ a) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

len a is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT

len k2 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

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

(len k2) + (len a) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

len <*G*> is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

{ (B ^ <*b

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

{ (B ^ <*b

G is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

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

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

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

ProperPrefixes <*G*> is finite set

{ (A ^ <*b

F is non empty Tree-like set

F is non empty Tree-like set

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

F with-replacement (A,F) is non empty Tree-like set

A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F with-replacement (A,F)

succ A is Element of bool (F with-replacement (A,F))

bool (F with-replacement (A,F)) is non empty set

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

succ B is Element of bool F

bool F is non empty set

k1 is set

{ (A ^ <*b

k2 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() 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

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

A1 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

A ^ G is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

{ (B ^ <*b

{ (B ^ <*b

k2 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() 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

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

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

{ (A ^ <*b

F is non empty Tree-like set

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

F is non empty Tree-like set

F with-replacement (A,F) is non empty Tree-like set

G is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F with-replacement (A,F)

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

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

succ G is Element of bool (F with-replacement (A,F))

bool (F with-replacement (A,F)) is non empty set

succ A is Element of bool F

bool F is non empty set

F is non empty Tree-like set

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

F | F is non empty Tree-like set

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

succ G is Element of bool F

bool F is non empty set

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

F ^ A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

succ A is Element of bool (F | F)

bool (F | F) is non empty set

B is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() 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

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

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

F ^ (A ^ <*B*>) is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT

B is set

{ (G ^ <*b

k1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() 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

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

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

k2 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() 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

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

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

B is Relation-like Function-like set

proj1 B is set

k1 is set

proj2 B is set

k2 is set

B . k2 is set

{ (G ^ <*b

A1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

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

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

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

{ (A ^ <*b

{ (A ^ <*b

k2 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() 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

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

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

{ (G ^ <*b

B . (G ^ <*k2*>) is set

k1 is set

k2 is set

B . k1 is set

B . k2 is set

A1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

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

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

G is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

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

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

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

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

F is non empty finite Tree-like set

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

branchdeg (F) is set

card F is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

succ (F) is finite Element of bool F

bool F is non empty finite V37() set

card (succ (F)) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

F is set

{(F)} is functional non empty trivial finite V37() 1 -element Element of bool F

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

A is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

<*A*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element 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

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

{} ^ <*A*> is Relation-like NAT -defined Function-like non empty finite {} + 1 -element FinSequence-like FinSubsequence-like set

{} + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT

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

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

{<*0*>} is functional non empty trivial finite V37() 1 -element Element of bool (bool [:NAT,NAT:])

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

F is non empty finite Tree-like set

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

branchdeg (F) is set

succ (F) is finite Element of bool F

bool F is non empty finite V37() set

card (succ (F)) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

F is set

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

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

{ ((F) ^ <*b

G is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

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

(F) ^ <*G*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT

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

{<*0*>,<*1*>} is functional non empty finite V37() Element of bool (bool [:NAT,NAT:])

F is non empty finite Tree-like set

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

branchdeg (F) is set

succ (F) is finite Element of bool F

bool F is non empty finite V37() set

card (succ (F)) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

F is set

A is set

{F,A} is non empty finite set

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

{ ((F) ^ <*b

A is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

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

(F) ^ <*A*> 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 NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F

k1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() 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

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

(F) ^ <*1*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT

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

(F) ^ <*1*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT

F is non empty Tree-like set

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

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

F | F is non empty Tree-like set

{ (F ^ b

G is set

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

F ^ A 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 ^ B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

G is Relation-like Function-like set

proj1 G is set

G is Relation-like Function-like set

proj1 G is set

A is set

proj2 G is set

B is set

G . B is set

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

k2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of NAT *

F ^ k2 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 Element of NAT *

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

G . B is set

A is set

B is set

G . A is set

G . B is set

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

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

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

F ^ k2 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 NAT *

F ^ G is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

F is non empty finite Tree-like set

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

card F is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

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

F | F is non empty finite Tree-like set

card (F | F) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

{ (F ^ b

G is finite set

{(F)} is functional non empty trivial finite V37() 1 -element Element of bool F

bool F is non empty finite V37() set

G \/ {(F)} is non empty finite set

B is set

A is finite set

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

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

card A is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

card G is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

(card G) + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

(card (F | F)) + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

F is non empty finite Tree-like set

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

succ (F) is finite Element of bool F

bool F is non empty finite V37() set

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

{F} is functional non empty trivial finite V37() 1 -element Element of bool F

F | F is non empty finite Tree-like set

(elementary_tree 1) with-replacement (<*0*>,(F | F)) is non empty Tree-like set

card (succ (F)) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

branchdeg (F) is set

G is set

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

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

k1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() 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

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

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

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

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

A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of (elementary_tree 1) with-replacement (<*0*>,(F | F))

A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of (elementary_tree 1) with-replacement (<*0*>,(F | F))

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

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

A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of (elementary_tree 1) with-replacement (<*0*>,(F | F))

F is Relation-like Function-like set

proj1 F is set

proj2 F is set

[:(proj1 F),(proj2 F):] is Relation-like set

F is non empty set

A is Relation-like F -valued Function-like finite DecoratedTree-like set

proj1 A is non empty finite Tree-like set

((proj1 A)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 A

succ ((proj1 A)) is finite Element of bool (proj1 A)

bool (proj1 A) is non empty finite V37() set

(F,A) is Element of F

A . ((proj1 A)) is Element of F

(elementary_tree 1) --> (F,A) is Relation-like elementary_tree 1 -defined F -valued Function-like V30( elementary_tree 1,F) finite DecoratedTree-like Element of bool [:(elementary_tree 1),F:]

[:(elementary_tree 1),F:] is Relation-like non empty set

bool [:(elementary_tree 1),F:] is non empty set

G is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 A

{G} is functional non empty trivial finite V37() 1 -element Element of bool (proj1 A)

A | G is Relation-like F -valued Function-like DecoratedTree-like set

((elementary_tree 1) --> (F,A)) with-replacement (<*0*>,(A | G)) is Relation-like Function-like DecoratedTree-like set

dom ((elementary_tree 1) --> (F,A)) is non empty finite Tree-like Element of bool (elementary_tree 1)

bool (elementary_tree 1) is non empty finite V37() set

proj1 (A | G) is non empty Tree-like set

(proj1 A) | G is non empty finite Tree-like set

card (succ ((proj1 A))) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

branchdeg ((proj1 A)) is set

proj1 (((elementary_tree 1) --> (F,A)) with-replacement (<*0*>,(A | G))) is non empty Tree-like set

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

(((elementary_tree 1) --> (F,A)) with-replacement (<*0*>,(A | G))) . B is set

A . B is set

(dom ((elementary_tree 1) --> (F,A))) with-replacement (<*0*>,(proj1 (A | G))) is non empty Tree-like set

((elementary_tree 1) --> (F,A)) . B is set

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

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

(A | G) . k1 is set

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

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

(A | G) . k1 is set

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

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

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

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

(A | G) . k2 is set

(elementary_tree 1) with-replacement (<*0*>,((proj1 A) | G)) is non empty Tree-like set

F is non empty Tree-like set

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

succ (F) is Element of bool F

bool F is non empty set

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

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

{A,G} is functional non empty finite V37() Element of bool F

F | A is non empty Tree-like set

(elementary_tree 2) with-replacement (<*0*>,(F | A)) is non empty Tree-like set

F | G is non empty Tree-like set

((elementary_tree 2) with-replacement (<*0*>,(F | A))) with-replacement (<*1*>,(F | G)) is non empty Tree-like set

B 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 V28() V29() 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

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

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

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

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

<*1*> ^ A1 is Relation-like NAT -defined NAT -valued Function-like non empty 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

<*0*> ^ k1 is Relation-like NAT -defined NAT -valued Function-like non empty 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

<*1*> ^ k1 is Relation-like NAT -defined NAT -valued Function-like non empty 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

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

F is non empty set

A is Relation-like F -valued Function-like DecoratedTree-like set

proj1 A is non empty Tree-like set

((proj1 A)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 A

succ ((proj1 A)) is Element of bool (proj1 A)

bool (proj1 A) is non empty set

(F,A) is Element of F

A . ((proj1 A)) is Element of F

(elementary_tree 2) --> (F,A) is Relation-like elementary_tree 2 -defined F -valued Function-like V30( elementary_tree 2,F) finite DecoratedTree-like Element of bool [:(elementary_tree 2),F:]

[:(elementary_tree 2),F:] is Relation-like non empty set

bool [:(elementary_tree 2),F:] is non empty set

G is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 A

A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 A

{G,A} is functional non empty finite V37() Element of bool (proj1 A)

A | G is Relation-like F -valued Function-like DecoratedTree-like set

((elementary_tree 2) --> (F,A)) with-replacement (<*0*>,(A | G)) is Relation-like Function-like DecoratedTree-like set

A | A is Relation-like F -valued Function-like DecoratedTree-like set

(((elementary_tree 2) --> (F,A)) with-replacement (<*0*>,(A | G))) with-replacement (<*1*>,(A | A)) is Relation-like Function-like DecoratedTree-like set

proj1 (A | A) is non empty Tree-like set

(proj1 A) | A is non empty Tree-like set

proj1 (A | G) is non empty Tree-like set

(proj1 A) | G is non empty Tree-like set

dom ((elementary_tree 2) --> (F,A)) is non empty finite Tree-like Element of bool (elementary_tree 2)

bool (elementary_tree 2) is non empty finite V37() set

proj1 (((elementary_tree 2) --> (F,A)) with-replacement (<*0*>,(A | G))) is non empty Tree-like set

(dom ((elementary_tree 2) --> (F,A))) with-replacement (<*0*>,(proj1 (A | G))) is non empty Tree-like set

proj1 ((((elementary_tree 2) --> (F,A)) with-replacement (<*0*>,(A | G))) with-replacement (<*1*>,(A | A))) is non empty Tree-like set

(proj1 (((elementary_tree 2) --> (F,A)) with-replacement (<*0*>,(A | G)))) with-replacement (<*1*>,(proj1 (A | A))) is non empty Tree-like set

(elementary_tree 2) with-replacement (<*0*>,((proj1 A) | G)) is non empty Tree-like set

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

((((elementary_tree 2) --> (F,A)) with-replacement (<*0*>,(A | G))) with-replacement (<*1*>,(A | A))) . A1 is set

A . A1 is set

(((elementary_tree 2) --> (F,A)) with-replacement (<*0*>,(A | G))) . A1 is set

((elementary_tree 2) --> (F,A)) . A1 is set

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

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

(A | A) . G is set

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

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

(A | G) . G is set

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

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

(A | A) . G is set

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

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

(A | G) . k is set

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

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

(A | A) . G is set

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

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

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

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

(A | A) . k is set

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

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

(A | G) . a is set

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

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

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

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

(A | A) . k is set

{3} is non empty trivial finite V37() 1 -element Element of bool NAT

[:{3},NAT:] is Relation-like NAT -defined REAL -valued non empty non trivial non finite Element of bool [:NAT,REAL:]

[:NAT,REAL:] is Relation-like set

bool [:NAT,REAL:] is non empty set

() is set

{0,1,2} is non empty finite Element of bool NAT

[:{0,1,2},NAT:] is Relation-like NAT -defined REAL -valued non empty non trivial non finite Element of bool [:NAT,REAL:]

() is set

F is set

F is set

A is set

[F,A] is V22() set

{F,A} is non empty finite set

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

{{F,A},{F}} is non empty finite V37() set

F is non empty finite Tree-like set

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

branchdeg F is set

succ F is finite Element of bool F

bool F is non empty finite V37() set

card (succ F) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

[0,0] is V22() Element of [:NAT,NAT:]

{0,0} is functional non empty finite V37() set

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

{{0,0},{0}} is non empty finite V37() set

[1,0] is V22() Element of [:NAT,NAT:]

{1,0} is non empty finite V37() set

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

{{1,0},{1}} is non empty finite V37() set

[1,1] is V22() Element of [:NAT,NAT:]

{1,1} is non empty finite V37() set

{{1,1},{1}} is non empty finite V37() set

[2,0] is V22() Element of [:NAT,NAT:]

{2,0} is non empty finite V37() set

{2} is non empty trivial finite V37() 1 -element set

{{2,0},{2}} is non empty finite V37() set

A is set

G is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like set

proj1 G is non empty finite Tree-like set

A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 G

((proj1 G),A) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

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

((proj1 G),B) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

G . B is Element of [:NAT,NAT:]

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

((proj1 G),k1) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

G . k1 is Element of [:NAT,NAT:]

k2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 G

((proj1 G),k2) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

G . k2 is Element of [:NAT,NAT:]

A is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like set

proj1 A is non empty finite Tree-like set

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

((proj1 A),B) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

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

((proj1 A),k1) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

A . k1 is Element of [:NAT,NAT:]

k2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 A

((proj1 A),k2) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

A . k2 is Element of [:NAT,NAT:]

A1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 A

((proj1 A),A1) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

A . A1 is Element of [:NAT,NAT:]

G is Relation-like Function-like DecoratedTree-like set

proj1 G is non empty Tree-like set

proj2 G is set

A is set

B is set

G . B is set

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

G . k1 is set

A is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like set

B is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like set

proj1 B is non empty finite Tree-like set

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

((proj1 B),k1) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

B . k1 is Element of [:NAT,NAT:]

succ k1 is finite Element of bool (proj1 B)

bool (proj1 B) is non empty finite V37() set

the Element of succ k1 is Element of succ k1

{ (k1 ^ <*b

A1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

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

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

B is non empty set

k1 is set

k1 is functional non empty constituted-DTrees DTree-set of [:NAT,NAT:]

A1 is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like set

proj1 A1 is non empty finite Tree-like set

k2 is Relation-like [:NAT,NAT:] -valued Function-like DecoratedTree-like set

G is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 A1

((proj1 A1),G) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

k is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 A1

((proj1 A1),k) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

A1 . k is Element of [:NAT,NAT:]

a is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 A1

((proj1 A1),a) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

A1 . a is Element of [:NAT,NAT:]

v is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 A1

((proj1 A1),v) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

A1 . v is Element of [:NAT,NAT:]

s is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like set

proj1 s is non empty finite Tree-like set

F is functional non empty constituted-DTrees DTree-set of [:NAT,NAT:]

F is functional non empty constituted-DTrees DTree-set of [:NAT,NAT:]

A is set

G is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like set

proj1 G is non empty finite Tree-like set

A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 G

((proj1 G),A) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

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

((proj1 G),B) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

G . B is Element of [:NAT,NAT:]

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

((proj1 G),k1) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

G . k1 is Element of [:NAT,NAT:]

k2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 G

((proj1 G),k2) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

G . k2 is Element of [:NAT,NAT:]

A is set

G is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like set

proj1 G is non empty finite Tree-like set

A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 G

((proj1 G),A) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

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

((proj1 G),B) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

G . B is Element of [:NAT,NAT:]

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

((proj1 G),k1) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

G . k1 is Element of [:NAT,NAT:]

k2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 G

((proj1 G),k2) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

G . k2 is Element of [:NAT,NAT:]

() is functional non empty constituted-DTrees DTree-set of [:NAT,NAT:]

F is Relation-like [:NAT,NAT:] -valued Function-like DecoratedTree-like Element of ()

F is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()

proj1 F is non empty finite Tree-like set

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

F | F is Relation-like [:NAT,NAT:] -valued Function-like DecoratedTree-like set

proj1 (F | F) is non empty Tree-like set

(proj1 F) | F is non empty finite Tree-like set

G is non empty finite Tree-like set

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

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

k2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of (proj1 F) | F

succ k2 is finite Element of bool ((proj1 F) | F)

bool ((proj1 F) | F) is non empty finite V37() set

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

succ A1 is finite Element of bool (proj1 F)

bool (proj1 F) is non empty finite V37() set

succ B is finite Element of bool G

bool G is non empty finite V37() set

card (succ B) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

card (succ A1) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

(G,B) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

((proj1 F),A1) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

A is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like set

A . B is set

F . A1 is Element of [:NAT,NAT:]

F . A1 is Element of [:NAT,NAT:]

G is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

[3,G] is V22() Element of [:NAT,NAT:]

{3,G} is non empty finite V37() set

{3} is non empty trivial finite V37() 1 -element set

{{3,G},{3}} is non empty finite V37() set

G is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

[3,G] is V22() Element of [:NAT,NAT:]

{3,G} is non empty finite V37() set

{3} is non empty trivial finite V37() 1 -element set

{{3,G},{3}} is non empty finite V37() set

k is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

[3,k] is V22() Element of [:NAT,NAT:]

{3,k} is non empty finite V37() set

{{3,k},{3}} is non empty finite V37() set

k is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

[3,k] is V22() Element of [:NAT,NAT:]

{3,k} is non empty finite V37() set

{{3,k},{3}} is non empty finite V37() set

F . A1 is Element of [:NAT,NAT:]

F . A1 is Element of [:NAT,NAT:]

F . A1 is Element of [:NAT,NAT:]

F . A1 is Element of [:NAT,NAT:]

F . A1 is Element of [:NAT,NAT:]

F is Element of ()

F `1 is set

F is non empty set

A is Element of F

G is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

[A,G] is V22() Element of [:F,NAT:]

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

{A,G} is non empty finite set

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

{{A,G},{A}} is non empty finite V37() set

F is non empty set

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

F is Relation-like F -valued Function-like DecoratedTree-like set

proj1 F is non empty Tree-like set

A is Relation-like F -valued Function-like DecoratedTree-like set

F with-replacement (G,A) is Relation-like Function-like DecoratedTree-like set

proj2 (F with-replacement (G,A)) is set

B is set

proj1 (F with-replacement (G,A)) is non empty Tree-like set

k1 is set

(F with-replacement (G,A)) . k1 is set

proj1 A is non empty Tree-like set

(proj1 F) with-replacement (G,(proj1 A)) is non empty Tree-like set

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

(F with-replacement (G,A)) . k2 is set

F . k2 is set

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

G ^ A1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

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

F . A1 is Element of F

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

(F with-replacement (G,A)) . k2 is set

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

G ^ A1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

A . A1 is set

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

G ^ A1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

A . A1 is set

G is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 A

A . G is Element of F

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

(F with-replacement (G,A)) . k2 is set

F . k2 is set

(elementary_tree 1) --> [1,0] is Relation-like elementary_tree 1 -defined [:NAT,NAT:] -valued Function-like V30( elementary_tree 1,[:NAT,NAT:]) finite DecoratedTree-like Element of bool [:(elementary_tree 1),[:NAT,NAT:]:]

[:(elementary_tree 1),[:NAT,NAT:]:] is Relation-like non empty non trivial non finite set

bool [:(elementary_tree 1),[:NAT,NAT:]:] is non empty non trivial non finite set

F is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like Element of ()

((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,F) is Relation-like Function-like DecoratedTree-like set

dom ((elementary_tree 1) --> [1,0]) is non empty finite Tree-like Element of bool (elementary_tree 1)

bool (elementary_tree 1) is non empty finite V37() set

([:NAT,NAT:],((elementary_tree 1) --> [1,0]),F,<*0*>) is Relation-like [:NAT,NAT:] -valued Function-like DecoratedTree-like set

proj1 (((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,F)) is non empty Tree-like set

proj1 F is non empty finite Tree-like set

(dom ((elementary_tree 1) --> [1,0])) with-replacement (<*0*>,(proj1 F)) is non empty Tree-like set

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

(elementary_tree 1) with-replacement (F,(proj1 F)) is non empty finite Tree-like set

G is Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like set

proj1 G is non empty finite Tree-like set

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

((proj1 G),B) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

G . B is Element of [:NAT,NAT:]

((elementary_tree 1) --> [1,0]) . B is set

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

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

k2 is set

k1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom ((elementary_tree 1) --> [1,0])

succ k1 is finite Element of bool (dom ((elementary_tree 1) --> [1,0]))

bool (dom ((elementary_tree 1) --> [1,0])) is non empty finite V37() set

{ (k1 ^ <*b

A1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() finite cardinal Element of NAT

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

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

k1 ^ <*0*> is Relation-like NAT -defined NAT -valued Function-like non empty finite