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
{ b1 where b1 is Element of QC-WFF A : b1 is_immediate_constituent_of F } is set
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 ^ <*b1*>) where b1 is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT : G1 ^ <*b1*> in proj1 G2 } is set
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 ^ <*b1*>) where b1 is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT : H ^ <*b1*> in proj1 t1 } is set
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 ^ <*b1*>) where b1 is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT : t2 ^ <*b1*> in proj1 H } is set
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 ^ <*b1*>) where b1 is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT : G1 ^ <*b1*> in proj1 (A,G2) } is set
{ (G1 ^ <*b1*>) where b1 is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT : G1 ^ <*b1*> in proj1 (A,G2) } is set
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
{ b1 where b1 is Element of QC-WFF A : b1 is_immediate_constituent_of (A,G2) . G1 } is set
(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
{ b1 where b1 is Element of QC-WFF A : b1 is_immediate_constituent_of (A,G2) . G1 } is set
(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 ^ <*b1*>) where b1 is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT : G1 ^ <*b1*> in proj1 (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 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 ^ <*b1*>) where b1 is ext-real non negative V27() epsilon-transitive epsilon-connected ordinal natural V35() finite cardinal Element of NAT : G1 ^ <*b1*> in proj1 (A,F) } is set
(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
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 (A,F) : (A,F) . b1 = G2 } is set
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)
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 (A,F) : (A,F) . b1 = G2 } is set
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
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 (A,G2) : (A,G2) . b1 = F } is set
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
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 (A,s) : (A,s) . b1 = t2 } is set
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)
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 (A,t2) : (A,t2) . b1 = H9 } is set
c24 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 (A,t2)
(A,t2) . c24 is Element of QC-WFF A
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
c24 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 (A,t2)
(A,t2) . c24 is Element of QC-WFF A
the_left_argument_of H9 is Element of QC-WFF A
the_right_argument_of H9 is Element of QC-WFF A
c24 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 (A,t2)
(A,t2) . c24 is Element of QC-WFF A
the_scope_of H9 is Element of QC-WFF A
c24 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 (A,t2)
(A,t2) . c24 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
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
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 (A,H) : (A,H) . b1 = t2 } is set
v is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 (A,H)
(A,H) . v is Element of QC-WFF A
(A,F) . t1 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,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)
{ (b1 ^ b2) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 (A,F), b2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 (A,G2) : ( b1 in (A,F,G2) & b2 in (A,G2,G1) ) } is set
(A,F,G1) is finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,F)
t1 is set
H 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)
H ^ H is Relation-like NAT -defined NAT -valued Function-like 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 Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set
(A,F) . G2 is Element of QC-WFF A
(A,((A,F) . G2)) is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set
proj1 ((A,F) | G2) is non empty finite Tree-like finite-order finite-branching set
proj1 (A,((A,F) . G2)) 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 FinSequence of NAT
H is Element of QC-WFF A
(A,F,H) is finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,F)
G2 ^ H is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
s is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(proj1 (A,F)) | G2 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,F)
(A,F) . t2 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,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
(A,F,t2) is finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,F)
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 Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 (A,H)
(A,H) . 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,F,t2) is finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,F)
(A,F,H) is finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,F)
G2 ^ s is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
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
H is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 ((A,F) | G2)
(proj1 (A,F)) | G2 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,H)
G2 ^ s is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
((A,F) | G2) . H is Element of QC-WFF A
t2 is Element of QC-WFF A
(A,F,H) is finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,F)
G2 ^ H is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(A,F) . (G2 ^ H) is set
t2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 (A,F)
(A,F,t2) is finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,F)
(A,H,t2) is finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,H)
(A,((A,F) . G2)) . H is set
H is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 ((A,F) | G2)
((A,F) | G2) . H is Element of QC-WFF A
(A,((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,F,G2) is finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,F)
(A,G2) is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-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,F)
(A,F) | G1 is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set
(A,F) . G1 is Element of QC-WFF A
(A,G2) . {} 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,F,G2) is finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,F)
(A,G2) is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 (A,F) : (A,F) | b1 = (A,G2) } is set
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 Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set
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 Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching 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
G1 is Element of QC-WFF A
t1 is finite Chain of proj1 (A,F)
{ ((A,F) . b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 (A,F) : b1 in 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
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 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 (A,F)
proj2 (A,F) is finite set
G1 is set
(A,F) . G1 is set
A is QC-alphabet
QC-WFF A is non empty set
F is Element of QC-WFF A
G2 is (A,F)
G1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (A,F,G2)
t1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (A,F,G2)
(A,F) is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set
(A,F) . G1 is Element of QC-WFF A
(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 (A,F)
(A,F,G2) is finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,F)
(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
A is QC-alphabet
QC-WFF A is non empty set
F is Element of QC-WFF A
G2 is (A,F)
(A,F,G2) is non empty finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,F)
(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
(A,F,G2) is finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,F)
G1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (A,F,G2)
(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
G2 is (A,F)
(A,F,G2) is non empty finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,F)
(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
(A,F,G2) is finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,F)
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (A,F,G2) : b1 = b1 } is set
G1 is set
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 (A,F) : (A,F) . b1 = G2 } 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
H is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (A,F,G2)
G1 is set
t1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (A,F,G2)
A is QC-alphabet
QC-WFF A is non empty set
F is Element of QC-WFF A
G2 is (A,F)
(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 (A,F)
(A,G2,G1) is finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,G2)
t1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (A,F,G2)
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
(A,F) is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set
(A,F) . t1 is Element of QC-WFF A
(A,F,G2) is finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,F)
proj1 (A,F) is non empty finite Tree-like finite-order finite-branching set
(A,F,G1) is finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,F)
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
G2 is (A,F)
G1 is (A,F)
(A,G1,G2) is finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,G1)
(A,G1) is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set
proj1 (A,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 (A,F,G1)
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 Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(A,F) is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set
(A,F) . t1 is Element of QC-WFF A
(A,F,G1) is finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,F)
proj1 (A,F) is non empty finite Tree-like finite-order finite-branching set
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (A,F,G2) : b1 = b1 } is set
(A,F,G2) is non empty finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,F)
(A,F,G2) is finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,F)
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 (A,F)
(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 (A,F)
(A,G2,G1) is finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,G2)
{ (b1 ^ b2) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (A,F,G2), b2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 (A,G2) : b2 in (A,G2,G1) } is set
{ (b1 ^ b2) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 (A,F), b2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 (A,G2) : ( b1 in (A,F,G2) & b2 in (A,G2,G1) ) } is set
t1 is set
H is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (A,F,G2)
H is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 (A,G2)
H ^ H is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(A,F) . H 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)
H is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 (A,G2)
H ^ H is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(A,F) . H is Element of QC-WFF A
s is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (A,F,G2)
s ^ H is Relation-like NAT -defined NAT -valued Function-like 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
G2 is (A,F)
(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 (A,F)
(A,G2,G1) is finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,G2)
{ (b1 ^ b2) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (A,F,G2), b2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 (A,G2) : b2 in (A,G2,G1) } is set
(A,F,G1) is non empty finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,F)
(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
(A,F,G1) is finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,F)
(A,F,G2) is finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,F)
{ (b1 ^ b2) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 (A,F), b2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 (A,G2) : ( b1 in (A,F,G2) & b2 in (A,G2,G1) ) } is set
A is QC-alphabet
QC-WFF A is non empty set
F is Element of QC-WFF A
G2 is (A,F)
G1 is (A,F)
t1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (A,F,G2)
H is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (A,F,G1)
(A,F) is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set
(A,F) . t1 is Element of QC-WFF A
(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
G2 is (A,F)
G1 is (A,F)
H is Element of QC-WFF A
H is (A,G1)
the Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (A,G1,H) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (A,G1,H)
(A,G1) is Relation-like QC-WFF A -valued Function-like finite DecoratedTree-like finite-order finite-branching set
(A,G1) . the Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (A,G1,H) is Element of QC-WFF A
(A,G1,G2) is finite AntiChain_of_Prefixes-like AntiChain_of_Prefixes of proj1 (A,G1)
proj1 (A,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 (A,F,G1)
t1 ^ the Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (A,G1,H) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
t2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (A,F,G2)
t2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (A,F,G2)
t1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (A,F,G1)