:: QC_LANG4 semantic presentation

REAL is set

NAT is non empty non root epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal Element of K19(REAL)

K19(REAL) is non empty set

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

K19(NAT) is non empty non root non finite set

K19(NAT) is non empty non root non finite set

{} is set

the Relation-like non-empty empty-yielding functional empty ext-real non negative V27() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSequence-membered set is Relation-like non-empty empty-yielding functional empty ext-real non negative V27() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSequence-membered set

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

{{},1} is finite set

K218() is set

K19(K218()) is non empty set

K219() is Element of K19(K218())

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

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

0 is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

Seg 1 is non empty root finite 1 -element Element of K19(NAT)

{1} is non empty root finite V40() 1 -element set

Seg 2 is non empty finite 2 -element Element of K19(NAT)

{1,2} is finite V40() set

<*> NAT is Relation-like non-empty empty-yielding NAT -defined NAT -valued Function-like functional empty proper ext-real non negative V27() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of NAT

K20(NAT,NAT) is Relation-like non empty non root non finite set

A is QC-alphabet

QC-WFF A is non empty set

F is Element of QC-WFF A

@ F is Relation-like NAT -defined K20(NAT,(QC-symbols A)) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of K20(NAT,(QC-symbols A))

QC-symbols A is non empty set

K20(NAT,(QC-symbols A)) is Relation-like non empty non root non finite set

len (@ F) is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

G2 is Element of QC-WFF A

@ G2 is Relation-like NAT -defined K20(NAT,(QC-symbols A)) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of K20(NAT,(QC-symbols A))

len (@ G2) is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

A is QC-alphabet

QC-WFF A is non empty set

F is Element of QC-WFF A

@ F is Relation-like NAT -defined K20(NAT,(QC-symbols A)) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of K20(NAT,(QC-symbols A))

QC-symbols A is non empty set

K20(NAT,(QC-symbols A)) is Relation-like non empty non root non finite set

len (@ F) is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

G2 is Element of QC-WFF A

@ G2 is Relation-like NAT -defined K20(NAT,(QC-symbols A)) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of K20(NAT,(QC-symbols A))

len (@ G2) is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

A is QC-alphabet

QC-WFF A is non empty set

F is Element of QC-WFF A

VERUM A is Element of QC-WFF A

<*> (QC-WFF A) is Relation-like non-empty empty-yielding NAT -defined QC-WFF A -valued Function-like functional empty proper ext-real non negative V27() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of QC-WFF A

K20(NAT,(QC-WFF A)) is Relation-like non empty non root non finite set

the_argument_of F is Element of QC-WFF A

<*(the_argument_of F)*> is Relation-like NAT -defined QC-WFF A -valued Function-like non empty root finite 1 -element FinSequence-like FinSubsequence-like FinSequence of QC-WFF A

the_left_argument_of F is Element of QC-WFF A

the_right_argument_of F is Element of QC-WFF A

<*(the_left_argument_of F),(the_right_argument_of F)*> is Relation-like NAT -defined QC-WFF A -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of QC-WFF A

the_scope_of F is Element of QC-WFF A

<*(the_scope_of F)*> is Relation-like NAT -defined QC-WFF A -valued Function-like non empty root finite 1 -element FinSequence-like FinSubsequence-like FinSequence of QC-WFF A

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

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

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

A is QC-alphabet

QC-WFF A is non empty set

F is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

G2 is Element of QC-WFF A

(A,G2) is Relation-like NAT -defined QC-WFF A -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of QC-WFF A

dom (A,G2) is finite Element of K19(NAT)

(A,G2) . F is set

G1 is Element of QC-WFF A

<*> (QC-WFF A) is Relation-like non-empty empty-yielding NAT -defined QC-WFF A -valued Function-like functional empty proper ext-real non negative V27() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of QC-WFF A

K20(NAT,(QC-WFF A)) is Relation-like non empty non root non finite set

VERUM A is Element of QC-WFF A

the_argument_of G2 is Element of QC-WFF A

<*(the_argument_of G2)*> is Relation-like NAT -defined QC-WFF A -valued Function-like non empty root finite 1 -element FinSequence-like FinSubsequence-like FinSequence of QC-WFF A

the_scope_of G2 is Element of QC-WFF A

<*(the_scope_of G2)*> is Relation-like NAT -defined QC-WFF A -valued Function-like non empty root finite 1 -element FinSequence-like FinSubsequence-like FinSequence of QC-WFF A

the_left_argument_of G2 is Element of QC-WFF A

the_right_argument_of G2 is Element of QC-WFF A

<*(the_left_argument_of G2),(the_right_argument_of G2)*> is Relation-like NAT -defined QC-WFF A -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of QC-WFF A

<*(the_left_argument_of G2),(the_right_argument_of G2)*> . 2 is set

<*(the_left_argument_of G2),(the_right_argument_of G2)*> . 1 is set

len <*(the_left_argument_of G2),(the_right_argument_of G2)*> is non empty ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

the_scope_of G2 is Element of QC-WFF A

<*(the_scope_of G2)*> is Relation-like NAT -defined QC-WFF A -valued Function-like non empty root finite 1 -element FinSequence-like FinSubsequence-like FinSequence of QC-WFF A

A is QC-alphabet

QC-WFF A is non empty set

F is Element of QC-WFF A

(A,F) is Relation-like NAT -defined QC-WFF A -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of QC-WFF A

proj2 (A,F) is finite set

{ b

G2 is set

dom (A,F) is finite Element of K19(NAT)

G1 is Element of QC-WFF A

t1 is set

(A,F) . t1 is set

G2 is set

G1 is Element of QC-WFF A

dom (A,F) is finite Element of K19(NAT)

VERUM A is Element of QC-WFF A

the_argument_of F is Element of QC-WFF A

<*(the_argument_of F)*> is Relation-like NAT -defined QC-WFF A -valued Function-like non empty root finite 1 -element FinSequence-like FinSubsequence-like FinSequence of QC-WFF A

t1 is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

dom <*(the_argument_of F)*> is non empty root finite 1 -element Element of K19(NAT)

<*(the_argument_of F)*> . t1 is set

the_left_argument_of F is Element of QC-WFF A

the_right_argument_of F is Element of QC-WFF A

<*(the_left_argument_of F),(the_right_argument_of F)*> is Relation-like NAT -defined QC-WFF A -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of QC-WFF A

<*(the_left_argument_of F),(the_right_argument_of F)*> . 2 is set

len <*(the_left_argument_of F),(the_right_argument_of F)*> is non empty ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

dom <*(the_left_argument_of F),(the_right_argument_of F)*> is non empty finite 2 -element Element of K19(NAT)

<*(the_left_argument_of F),(the_right_argument_of F)*> . 1 is set

t1 is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

(A,F) . t1 is set

the_scope_of F is Element of QC-WFF A

<*(the_scope_of F)*> is Relation-like NAT -defined QC-WFF A -valued Function-like non empty root finite 1 -element FinSequence-like FinSubsequence-like FinSequence of QC-WFF A

t1 is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

dom <*(the_scope_of F)*> is non empty root finite 1 -element Element of K19(NAT)

<*(the_scope_of F)*> . t1 is set

t1 is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

(A,F) . t1 is set

A is QC-alphabet

QC-WFF A is non empty set

F is Element of QC-WFF A

G2 is Relation-like QC-WFF A -valued Function-like DecoratedTree-like finite-branching set

G2 . {} is set

proj1 G2 is non empty Tree-like finite-branching set

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

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

succ G1 is finite Element of K19((proj1 G2))

K19((proj1 G2)) is non empty set

{ (G1 ^ <*b

G2 . t1 is Element of QC-WFF A

G2 . G1 is Element of QC-WFF A

@ (G2 . G1) is Relation-like NAT -defined K20(NAT,(QC-symbols A)) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of K20(NAT,(QC-symbols A))

QC-symbols A is non empty set

K20(NAT,(QC-symbols A)) is Relation-like non empty non root non finite set

len (@ (G2 . G1)) is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

H is Element of QC-WFF A

@ H is Relation-like NAT -defined K20(NAT,(QC-symbols A)) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of K20(NAT,(QC-symbols A))

len (@ H) is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

H is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

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

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

succ (G2,G1) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

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

(succ (G2,G1)) . (H + 1) is set

(A,(G2 . G1)) is Relation-like NAT -defined QC-WFF A -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of QC-WFF A

(A,(G2 . G1)) . (H + 1) is set

dom (A,(G2 . G1)) is finite Element of K19(NAT)

dom (succ (G2,G1)) is finite Element of K19(NAT)

G1 succ is Relation-like NAT -defined proj1 G2 -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like FinSequence of proj1 G2

dom (G1 succ) is finite Element of K19(NAT)

G1 is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set

G1 . {} is set

proj1 G1 is non empty finite Tree-like finite-order finite-branching set

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

succ (G1,t1) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

G1 . t1 is Element of QC-WFF A

(A,(G1 . t1)) is Relation-like NAT -defined QC-WFF A -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of QC-WFF A

G2 is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set

G2 . {} is set

proj1 G2 is non empty finite Tree-like finite-order finite-branching set

G1 is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set

G1 . {} is set

proj1 G1 is non empty finite Tree-like finite-order finite-branching set

t1 is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set

t1 . {} is set

proj1 t1 is non empty finite Tree-like finite-order finite-branching set

H is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set

H . {} is set

proj1 H is non empty finite Tree-like finite-order finite-branching set

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

t1 . H is set

H . H is set

s is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

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

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

t1 . (H ^ <*s*>) is set

H . (H ^ <*s*>) is set

succ (t1,H) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

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

H . t2 is Element of QC-WFF A

(A,(H . t2)) is Relation-like NAT -defined QC-WFF A -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of QC-WFF A

succ (H,t2) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

succ H is finite Element of K19((proj1 t1))

K19((proj1 t1)) is non empty finite V40() set

{ (H ^ <*b

card (succ H) is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

H succ is Relation-like NAT -defined proj1 t1 -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like FinSequence of proj1 t1

len (H succ) is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

len (succ (t1,H)) is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

t2 succ is Relation-like NAT -defined proj1 H -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like FinSequence of proj1 H

len (t2 succ) is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

succ t2 is finite Element of K19((proj1 H))

K19((proj1 H)) is non empty finite V40() set

{ (t2 ^ <*b

card (succ t2) is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

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

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

(succ (H,t2)) . (s + 1) is set

H is set

H is set

t1 . H is set

H . H is set

A is QC-alphabet

QC-WFF A is non empty set

F is Element of QC-WFF A

(A,F) is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set

proj2 (A,F) is finite set

(A,F) . {} is set

proj1 (A,F) is non empty finite Tree-like finite-order finite-branching set

A is QC-alphabet

QC-WFF A is non empty set

F is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

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

G2 is Element of QC-WFF A

(A,G2) is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set

proj1 (A,G2) is non empty finite Tree-like finite-order finite-branching set

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

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

(A,G2) . (G1 ^ <*F*>) is set

(A,G2) . G1 is Element of QC-WFF A

succ G1 is finite Element of K19((proj1 (A,G2)))

K19((proj1 (A,G2))) is non empty finite V40() set

{ (G1 ^ <*b

{ (G1 ^ <*b

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

(A,((A,G2) . G1)) is Relation-like NAT -defined QC-WFF A -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of QC-WFF A

proj2 (A,((A,G2) . G1)) is finite set

{ b

(A,G2) . t1 is Element of QC-WFF A

H is Element of QC-WFF A

succ ((A,G2),G1) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

proj2 (succ ((A,G2),G1)) is finite set

A is QC-alphabet

QC-WFF A is non empty set

F is Element of QC-WFF A

G2 is Element of QC-WFF A

(A,G2) is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set

proj1 (A,G2) is non empty finite Tree-like finite-order finite-branching set

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

(A,G2) . G1 is Element of QC-WFF A

{ b

(A,((A,G2) . G1)) is Relation-like NAT -defined QC-WFF A -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of QC-WFF A

proj2 (A,((A,G2) . G1)) is finite set

succ ((A,G2),G1) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

succ G1 is finite Element of K19((proj1 (A,G2)))

K19((proj1 (A,G2))) is non empty finite V40() set

{ (G1 ^ <*b

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

(A,G2) . H is Element of QC-WFF A

H is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

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

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

t1 is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

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

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

(A,G2) . (G1 ^ <*t1*>) is set

t1 is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

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

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

(A,G2) . (G1 ^ <*t1*>) is set

H is Element of QC-WFF A

A is QC-alphabet

QC-WFF A is non empty set

F is Element of QC-WFF A

G2 is Element of QC-WFF A

(A,G2) is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set

proj2 (A,G2) is finite set

G1 is Element of QC-WFF A

proj1 (A,G2) is non empty finite Tree-like finite-order finite-branching set

t1 is set

(A,G2) . t1 is set

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

H is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

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

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

(A,G2) . (H ^ <*H*>) is set

A is QC-alphabet

QC-WFF A is non empty set

F is Element of QC-WFF A

G2 is Element of QC-WFF A

(A,G2) is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set

proj2 (A,G2) is finite set

G1 is Element of QC-WFF A

t1 is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

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

len H is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

H . 1 is set

H . t1 is set

dom H is finite Element of K19(NAT)

Seg t1 is finite t1 -element Element of K19(NAT)

H is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal set

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

H . (H + 1) is set

s is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal set

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

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

Seg (len H) is finite len H -element Element of K19(NAT)

t2 is Element of QC-WFF A

H . H is set

t2 is Element of QC-WFF A

t2 is Element of QC-WFF A

s is Element of QC-WFF A

Seg t1 is finite t1 -element Element of K19(NAT)

H is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal set

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

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

H . (0 + 1) is set

H is Element of QC-WFF A

A is QC-alphabet

QC-WFF A is non empty set

F is Element of QC-WFF A

G2 is Element of QC-WFF A

(A,G2) is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set

proj2 (A,G2) is finite set

proj1 (A,G2) is non empty finite Tree-like finite-order finite-branching set

t1 is set

(A,G2) . t1 is set

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

(A,G2) . H is set

s is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

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

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

(A,G2) . (H ^ <*s*>) is set

t2 is Element of QC-WFF A

(A,G2) . H is Element of QC-WFF A

t2 is Element of QC-WFF A

t2 is Element of QC-WFF A

s is Element of QC-WFF A

(A,G2) . {} is set

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

(A,G2) . H is Element of QC-WFF A

H is Element of QC-WFF A

A is QC-alphabet

QC-WFF A is non empty set

F is Element of QC-WFF A

(A,F) is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set

proj2 (A,F) is finite set

Subformulae F is set

G2 is set

G1 is Element of QC-WFF A

G2 is set

G1 is Element of QC-WFF A

A is QC-alphabet

QC-WFF A is non empty set

F is Element of QC-WFF A

(A,F) is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set

proj1 (A,F) is non empty finite Tree-like finite-order finite-branching set

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

(A,F) . G2 is Element of QC-WFF A

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

succ G1 is finite Element of K19((proj1 (A,F)))

K19((proj1 (A,F))) is non empty finite V40() set

{ (G1 ^ <*b

(A,F) . G1 is Element of QC-WFF A

t1 is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

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

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

A is QC-alphabet

QC-WFF A is non empty set

F is Element of QC-WFF A

(A,F) is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set

proj1 (A,F) is non empty finite Tree-like finite-order finite-branching set

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

(A,F) . G2 is Element of QC-WFF A

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

(A,F) . G1 is Element of QC-WFF A

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

G2 ^ t1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

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

len H is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

H is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

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

Seg (H + 1) is non empty finite H + 1 -element Element of K19(NAT)

s is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal set

t2 is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal set

s + t2 is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal set

t2 is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

Seg t2 is finite t2 -element Element of K19(NAT)

H | (Seg t2) is Relation-like Seg t2 -defined NAT -defined NAT -valued finite FinSubsequence-like set

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

G2 ^ s is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

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

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

(A,F) . s9 is Element of QC-WFF A

v is Element of QC-WFF A

s + t2 is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal set

(A,F) . (G2 ^ s) is set

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

dom s is finite Element of K19(NAT)

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

dom s is finite Element of K19(NAT)

len s is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

t2 is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

s . t2 is set

t2 is Element of QC-WFF A

s is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal set

s9 is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal set

s + s9 is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal set

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

Seg s9 is finite s9 -element Element of K19(NAT)

H | (Seg s9) is Relation-like Seg s9 -defined NAT -defined NAT -valued finite FinSubsequence-like set

G2 ^ v is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

(A,F) . (G2 ^ v) is set

t2 is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

s . t2 is set

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

s . (t2 + 1) is set

t2 is Element of QC-WFF A

s is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal set

t2 + s is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

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

Seg s is finite s -element Element of K19(NAT)

H | (Seg s) is Relation-like Seg s -defined NAT -defined NAT -valued finite FinSubsequence-like set

G2 ^ s9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

(A,F) . (G2 ^ s9) is set

v is Element of QC-WFF A

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

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

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

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

H | (Seg x) is Relation-like Seg x -defined NAT -defined NAT -valued finite FinSubsequence-like set

G2 ^ t99 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

(A,F) . (G2 ^ t99) is set

s1 is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

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

u is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

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

v is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

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

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

Seg u is finite u -element Element of K19(NAT)

H | (Seg u) is Relation-like Seg u -defined NAT -defined NAT -valued finite FinSubsequence-like set

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

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

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

Seg s1 is finite s1 -element Element of K19(NAT)

H | (Seg s1) is Relation-like Seg s1 -defined NAT -defined NAT -valued finite FinSubsequence-like set

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

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

s . 1 is set

t2 is Element of QC-WFF A

t2 is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal set

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

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

Seg t2 is finite t2 -element Element of K19(NAT)

H | (Seg t2) is Relation-like Seg t2 -defined NAT -defined NAT -valued finite FinSubsequence-like set

G2 ^ s is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

(A,F) . (G2 ^ s) is set

s . (H + 1) is set

s9 is Element of QC-WFF A

v is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal set

(H + 1) + v is non empty ext-real positive non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

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

Seg v is finite v -element Element of K19(NAT)

H | (Seg v) is Relation-like Seg v -defined NAT -defined NAT -valued finite FinSubsequence-like set

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

(A,F) . (G2 ^ x) is set

dom H is finite Element of K19(NAT)

A is QC-alphabet

QC-WFF A is non empty set

F is Element of QC-WFF A

(A,F) is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set

proj1 (A,F) is non empty finite Tree-like finite-order finite-branching set

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

(A,F) . G2 is Element of QC-WFF A

@ ((A,F) . G2) is Relation-like NAT -defined K20(NAT,(QC-symbols A)) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of K20(NAT,(QC-symbols A))

QC-symbols A is non empty set

K20(NAT,(QC-symbols A)) is Relation-like non empty non root non finite set

len (@ ((A,F) . G2)) is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

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

(A,F) . G1 is Element of QC-WFF A

@ ((A,F) . G1) is Relation-like NAT -defined K20(NAT,(QC-symbols A)) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of K20(NAT,(QC-symbols A))

len (@ ((A,F) . G1)) is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

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

G2 ^ H is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

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

len s is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

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

len t2 is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

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

Seg (len s) is finite len s -element Element of K19(NAT)

t2 is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal set

Seg t2 is finite t2 -element Element of K19(NAT)

s | (Seg t2) is Relation-like Seg t2 -defined NAT -defined NAT -valued finite FinSubsequence-like set

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

G2 ^ t2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

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

(A,F) . s is Element of QC-WFF A

s9 is set

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

dom t2 is finite Element of K19(NAT)

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

dom t2 is finite Element of K19(NAT)

t2 is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

Seg t2 is finite t2 -element Element of K19(NAT)

s | (Seg t2) is Relation-like Seg t2 -defined NAT -defined NAT -valued finite FinSubsequence-like set

t2 . t2 is set

v is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal set

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

Seg v is finite v -element Element of K19(NAT)

s | (Seg v) is Relation-like Seg v -defined NAT -defined NAT -valued finite FinSubsequence-like set

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

G2 ^ s9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

(A,F) . s is Element of QC-WFF A

s | (Seg 1) is Relation-like Seg 1 -defined NAT -defined NAT -valued finite FinSubsequence-like set

t2 . 1 is set

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

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

G2 ^ s is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

(A,F) . t2 is Element of QC-WFF A

v is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

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

@ ((A,F) . t2) is Relation-like NAT -defined K20(NAT,(QC-symbols A)) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of K20(NAT,(QC-symbols A))

len (@ ((A,F) . t2)) is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

A is QC-alphabet

QC-WFF A is non empty set

F is Element of QC-WFF A

(A,F) is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set

proj1 (A,F) is non empty finite Tree-like finite-order finite-branching set

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

(A,F) . G2 is Element of QC-WFF A

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

(A,F) . G1 is Element of QC-WFF A

@ ((A,F) . G2) is Relation-like NAT -defined K20(NAT,(QC-symbols A)) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of K20(NAT,(QC-symbols A))

QC-symbols A is non empty set

K20(NAT,(QC-symbols A)) is Relation-like non empty non root non finite set

len (@ ((A,F) . G2)) is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

@ ((A,F) . G1) is Relation-like NAT -defined K20(NAT,(QC-symbols A)) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of K20(NAT,(QC-symbols A))

len (@ ((A,F) . G1)) is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

A is QC-alphabet

QC-WFF A is non empty set

F is Element of QC-WFF A

(A,F) is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set

proj1 (A,F) is non empty finite Tree-like finite-order finite-branching set

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

(A,F) . G2 is Element of QC-WFF A

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

(A,F) . G1 is Element of QC-WFF A

A is QC-alphabet

QC-WFF A is non empty set

F is Element of QC-WFF A

(A,F) is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set

proj1 (A,F) is non empty finite Tree-like finite-order finite-branching set

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

(A,F) . G2 is Element of QC-WFF A

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

(A,F) . G1 is Element of QC-WFF A

A is QC-alphabet

QC-WFF A is non empty set

F is Element of QC-WFF A

(A,F) is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set

proj1 (A,F) is non empty finite Tree-like finite-order finite-branching set

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

(A,F) . G2 is Element of QC-WFF A

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

(A,F) . G1 is Element of QC-WFF A

A is QC-alphabet

QC-WFF A is non empty set

F is Element of QC-WFF A

(A,F) is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set

proj1 (A,F) is non empty finite Tree-like finite-order finite-branching set

G2 is Element of QC-WFF A

{ b

G1 is set

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

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

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

(A,F) . H is Element of QC-WFF A

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

(A,F) . s is Element of QC-WFF A

t1 is set

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

(A,F) . H is Element of QC-WFF A

t1 is AntiChain_of_Prefixes-like set

H is set

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

(A,F) . H is Element of QC-WFF A

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

(A,F) . t1 is Element of QC-WFF A

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

(A,F) . H is Element of QC-WFF A

G1 is finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,F)

t1 is finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,F)

H is set

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

(A,F) . H is Element of QC-WFF A

H is set

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

(A,F) . H is Element of QC-WFF A

A is QC-alphabet

QC-WFF A is non empty set

F is Element of QC-WFF A

(A,F) is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set

proj1 (A,F) is non empty finite Tree-like finite-order finite-branching set

G2 is Element of QC-WFF A

(A,F,G2) is finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,F)

{ b

G1 is set

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

(A,F) . t1 is Element of QC-WFF A

G1 is set

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

(A,F) . t1 is Element of QC-WFF A

A is QC-alphabet

QC-WFF A is non empty set

F is Element of QC-WFF A

G2 is Element of QC-WFF A

(A,G2,F) is finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,G2)

(A,G2) is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set

proj1 (A,G2) is non empty finite Tree-like finite-order finite-branching set

proj2 (A,G2) is finite set

G1 is set

(A,G2) . G1 is set

G1 is set

{ b

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

(A,G2) . t1 is Element of QC-WFF A

A is QC-alphabet

QC-WFF A is non empty set

F is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

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

G2 is Element of QC-WFF A

(A,G2) is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set

proj1 (A,G2) is non empty finite Tree-like finite-order finite-branching set

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

(A,G2) . G1 is Element of QC-WFF A

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

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

(A,G2) . t1 is Element of QC-WFF A

the_argument_of ((A,G2) . t1) is Element of QC-WFF A

<*(the_argument_of ((A,G2) . t1))*> is Relation-like NAT -defined QC-WFF A -valued Function-like non empty root finite 1 -element FinSequence-like FinSubsequence-like FinSequence of QC-WFF A

dom <*(the_argument_of ((A,G2) . t1))*> is non empty root finite 1 -element Element of K19(NAT)

succ ((A,G2),t1) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

(A,((A,G2) . t1)) is Relation-like NAT -defined QC-WFF A -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of QC-WFF A

t1 succ is Relation-like NAT -defined proj1 (A,G2) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like FinSequence of proj1 (A,G2)

dom (t1 succ) is finite Element of K19(NAT)

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

s succ is Relation-like NAT -defined proj1 (A,G2) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like FinSequence of proj1 (A,G2)

(s succ) * (A,G2) is Relation-like NAT -defined QC-WFF A -valued finite set

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

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

A is QC-alphabet

QC-WFF A is non empty set

F is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

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

G2 is Element of QC-WFF A

(A,G2) is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set

proj1 (A,G2) is non empty finite Tree-like finite-order finite-branching set

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

(A,G2) . G1 is Element of QC-WFF A

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

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

(A,G2) . t1 is Element of QC-WFF A

the_left_argument_of ((A,G2) . t1) is Element of QC-WFF A

the_right_argument_of ((A,G2) . t1) is Element of QC-WFF A

(A,((A,G2) . t1)) is Relation-like NAT -defined QC-WFF A -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of QC-WFF A

<*(the_left_argument_of ((A,G2) . t1)),(the_right_argument_of ((A,G2) . t1))*> is Relation-like NAT -defined QC-WFF A -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of QC-WFF A

len <*(the_left_argument_of ((A,G2) . t1)),(the_right_argument_of ((A,G2) . t1))*> is non empty ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

dom <*(the_left_argument_of ((A,G2) . t1)),(the_right_argument_of ((A,G2) . t1))*> is non empty finite 2 -element Element of K19(NAT)

succ ((A,G2),t1) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

t1 succ is Relation-like NAT -defined proj1 (A,G2) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like FinSequence of proj1 (A,G2)

dom (t1 succ) is finite Element of K19(NAT)

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

s succ is Relation-like NAT -defined proj1 (A,G2) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like FinSequence of proj1 (A,G2)

(s succ) * (A,G2) is Relation-like NAT -defined QC-WFF A -valued finite set

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

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

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

(succ ((A,G2),t1)) . (F + 1) is set

(succ ((A,G2),t1)) . (F + 1) is set

A is QC-alphabet

QC-WFF A is non empty set

F is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

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

G2 is Element of QC-WFF A

(A,G2) is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set

proj1 (A,G2) is non empty finite Tree-like finite-order finite-branching set

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

(A,G2) . G1 is Element of QC-WFF A

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

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

(A,G2) . t1 is Element of QC-WFF A

the_scope_of ((A,G2) . t1) is Element of QC-WFF A

<*(the_scope_of ((A,G2) . t1))*> is Relation-like NAT -defined QC-WFF A -valued Function-like non empty root finite 1 -element FinSequence-like FinSubsequence-like FinSequence of QC-WFF A

dom <*(the_scope_of ((A,G2) . t1))*> is non empty root finite 1 -element Element of K19(NAT)

succ ((A,G2),t1) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

(A,((A,G2) . t1)) is Relation-like NAT -defined QC-WFF A -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of QC-WFF A

VERUM A is Element of QC-WFF A

t1 succ is Relation-like NAT -defined proj1 (A,G2) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like FinSequence of proj1 (A,G2)

dom (t1 succ) is finite Element of K19(NAT)

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

s succ is Relation-like NAT -defined proj1 (A,G2) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like FinSequence of proj1 (A,G2)

(s succ) * (A,G2) is Relation-like NAT -defined QC-WFF A -valued finite set

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

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

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

A is QC-alphabet

QC-WFF A is non empty set

F is Element of QC-WFF A

(A,F) is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set

proj1 (A,F) is non empty finite Tree-like finite-order finite-branching set

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

(A,F) . G2 is Element of QC-WFF A

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

(A,F) . (G2 ^ <*0*>) is set

the_argument_of ((A,F) . G2) is Element of QC-WFF A

t1 is Element of QC-WFF A

H is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

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

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

(A,F) . (G2 ^ <*H*>) is set

A is set

F is set

<*A,F*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like set

dom <*A,F*> is non empty finite 2 -element Element of K19(NAT)

len <*A,F*> is non empty ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

Seg (len <*A,F*>) is non empty finite len <*A,F*> -element Element of K19(NAT)

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

A is QC-alphabet

QC-WFF A is non empty set

F is Element of QC-WFF A

(A,F) is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set

proj1 (A,F) is non empty finite Tree-like finite-order finite-branching set

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

(A,F) . G2 is Element of QC-WFF A

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

(A,F) . (G2 ^ <*0*>) is set

the_left_argument_of ((A,F) . G2) is Element of QC-WFF A

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

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

the_right_argument_of ((A,F) . G2) is Element of QC-WFF A

G2 succ is Relation-like NAT -defined proj1 (A,F) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like FinSequence of proj1 (A,F)

(G2 succ) * (A,F) is Relation-like NAT -defined QC-WFF A -valued finite set

succ ((A,F),G2) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

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

t1 succ is Relation-like NAT -defined proj1 (A,F) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like FinSequence of proj1 (A,F)

(t1 succ) * (A,F) is Relation-like NAT -defined QC-WFF A -valued finite set

dom (G2 succ) is finite Element of K19(NAT)

dom (succ ((A,F),G2)) is finite Element of K19(NAT)

(A,((A,F) . G2)) is Relation-like NAT -defined QC-WFF A -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of QC-WFF A

dom (A,((A,F) . G2)) is finite Element of K19(NAT)

<*(the_left_argument_of ((A,F) . G2)),(the_right_argument_of ((A,F) . G2))*> is Relation-like NAT -defined QC-WFF A -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of QC-WFF A

dom <*(the_left_argument_of ((A,F) . G2)),(the_right_argument_of ((A,F) . G2))*> is non empty finite 2 -element Element of K19(NAT)

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

(succ ((A,F),G2)) . (0 + 1) is set

(A,((A,F) . G2)) . 1 is set

<*(the_left_argument_of ((A,F) . G2)),(the_right_argument_of ((A,F) . G2))*> . 1 is set

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

(succ ((A,F),G2)) . (1 + 1) is set

(A,((A,F) . G2)) . 2 is set

<*(the_left_argument_of ((A,F) . G2)),(the_right_argument_of ((A,F) . G2))*> . 2 is set

A is QC-alphabet

QC-WFF A is non empty set

F is Element of QC-WFF A

(A,F) is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set

proj1 (A,F) is non empty finite Tree-like finite-order finite-branching set

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

(A,F) . G2 is Element of QC-WFF A

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

(A,F) . (G2 ^ <*0*>) is set

the_scope_of ((A,F) . G2) is Element of QC-WFF A

t1 is Element of QC-WFF A

H is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

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

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

(A,F) . (G2 ^ <*H*>) is set

A is QC-alphabet

QC-WFF A is non empty set

F is Element of QC-WFF A

(A,F) is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set

proj1 (A,F) is non empty finite Tree-like finite-order finite-branching set

G2 is Element of QC-WFF A

(A,G2) is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set

proj1 (A,G2) is non empty finite Tree-like finite-order finite-branching set

(A,F,G2) is finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,F)

G1 is Element of QC-WFF A

(A,G2,G1) is finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,G2)

(A,F,G1) is finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,F)

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

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

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

H is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

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

s is Element of QC-WFF A

(A,s) is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set

proj1 (A,s) is non empty finite Tree-like finite-order finite-branching set

t2 is Element of QC-WFF A

(A,t2) is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set

proj1 (A,t2) is non empty finite Tree-like finite-order finite-branching set

t2 is Element of QC-WFF A

(A,s,t2) is finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,s)

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

(A,s) . s is Element of QC-WFF A

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

(A,t2) . s9 is Element of QC-WFF A

len s9 is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

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

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

x is set

<*x*> is Relation-like NAT -defined Function-like non empty root finite 1 -element FinSequence-like FinSubsequence-like set

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

len v is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

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

proj2 t99 is finite set

dom t99 is finite Element of K19(NAT)

t99 . 1 is set

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

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

(A,t2) . v is Element of QC-WFF A

m is Element of QC-WFF A

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

(A,s,m) is finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,s)

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

(A,s) . t9 is Element of QC-WFF A

s1 is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

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

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

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

(A,s) . (t9 ^ <*s1*>) is set

VERUM A is Element of QC-WFF A

the_argument_of m is Element of QC-WFF A

the_left_argument_of m is Element of QC-WFF A

the_right_argument_of m is Element of QC-WFF A

the_scope_of m is Element of QC-WFF A

H is Element of QC-WFF A

(A,H) is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set

proj1 (A,H) is non empty finite Tree-like finite-order finite-branching set

s is Element of QC-WFF A

(A,s) is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set

proj1 (A,s) is non empty finite Tree-like finite-order finite-branching set

t2 is Element of QC-WFF A

(A,H,t2) is finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,H)

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

(A,H) . t2 is Element of QC-WFF A

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

(A,s) . s is Element of QC-WFF A

len s is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

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

(A,F) . t1 is Element of QC-WFF A

(A,G2) . H is Element of QC-WFF A

len H is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

A is QC-alphabet

QC-WFF A is non empty set

F is Element of QC-WFF A

(A,F) is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set

proj1 (A,F) is non empty finite Tree-like finite-order finite-branching set

G2 is Element of QC-WFF A

(A,F,G2) is finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,F)

G1 is Element of QC-WFF A

(A,F,G1) is finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,F)

(A,G2,G1) is finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,G2)

(A,G2) is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set

proj1 (A,G2) is non empty finite Tree-like finite-order finite-branching set

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

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

t1 ^ H is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

H is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

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

s is Element of QC-WFF A

(A,s) is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set

proj1 (A,s) is non empty finite Tree-like finite-order finite-branching set

t2 is Element of QC-WFF A

t2 is Element of QC-WFF A

(A,s,t2) is finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,s)

(A,t2,t2) is finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,t2)

(A,t2) is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set

proj1 (A,t2) is non empty finite Tree-like finite-order finite-branching set

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

(A,s) . s is Element of QC-WFF A

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

s ^ s9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len s9 is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

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

x is set

<*x*> is Relation-like NAT -defined Function-like non empty root finite 1 -element FinSequence-like FinSubsequence-like set

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

len v is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

{ b

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

(A,s) . t99 is Element of QC-WFF A

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

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

proj2 u is finite set

dom u is finite Element of K19(NAT)

u . 1 is set

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

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

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

m is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

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

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

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

(A,s) . t9 is Element of QC-WFF A

H9 is Element of QC-WFF A

(A,s,H9) is finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,s)

(A,t2,H9) is finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,t2)

{ b

c

(A,t2) . c

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

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

(A,t2) . (v ^ <*m*>) is set

VERUM A is Element of QC-WFF A

the_argument_of H9 is Element of QC-WFF A

c

(A,t2) . c

the_left_argument_of H9 is Element of QC-WFF A

the_right_argument_of H9 is Element of QC-WFF A

c

(A,t2) . c

the_scope_of H9 is Element of QC-WFF A

c

(A,t2) . c

H is Element of QC-WFF A

(A,H) is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set

proj1 (A,H) is non empty finite Tree-like finite-order finite-branching set

s is Element of QC-WFF A

t2 is Element of QC-WFF A

(A,H,t2) is finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,H)

(A,s,t2) is finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,s)

(A,s) is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set

proj1 (A,s) is non empty finite Tree-like finite-order finite-branching set

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

(A,H) . t2 is Element of QC-WFF A

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

t2 ^ s is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len s is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT

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

(A,s) . s9 is Element of QC-WFF A

{ b