:: QC_LANG2 semantic presentation

REAL is set
NAT is non empty V8() V9() V10() Element of K20(REAL)
K20(REAL) is set
NAT is non empty V8() V9() V10() set
K20(NAT) is set
K20(NAT) is set
1 is ext-real positive V4() non empty V8() V9() V10() V14() V15() Element of NAT
2 is ext-real positive V4() non empty V8() V9() V10() V14() V15() Element of NAT
3 is ext-real positive V4() non empty V8() V9() V10() V14() V15() Element of NAT
0 is ext-real V4() V8() V9() V10() V14() V15() Element of NAT
the ext-real V4() empty V8() V9() V10() V12() V13() V14() V15() functional FinSequence-membered set is ext-real V4() empty V8() V9() V10() V12() V13() V14() V15() functional FinSequence-membered set
A is QC-alphabet
QC-WFF A is non empty set
H is Element of QC-WFF A
'not' H is Element of QC-WFF A
[1,0] is V27() set
{1,0} is set
{1} is set
{{1,0},{1}} is set
<*[1,0]*> is non empty Relation-like NAT -defined Function-like V33() V40(1) FinSequence-like FinSubsequence-like set
@ H is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
QC-symbols A is non empty set
rng A is set
K21(NAT,(QC-symbols A)) is set
<*[1,0]*> ^ (@ H) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
the_argument_of ('not' H) is Element of QC-WFF A
A is QC-alphabet
QC-WFF A is non empty set
H is Element of QC-WFF A
G is Element of QC-WFF A
H '&' G is Element of QC-WFF A
[2,0] is V27() set
{2,0} is set
{2} is set
{{2,0},{2}} is set
<*[2,0]*> is non empty Relation-like NAT -defined Function-like V33() V40(1) FinSequence-like FinSubsequence-like set
@ H is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
QC-symbols A is non empty set
rng A is set
K21(NAT,(QC-symbols A)) is set
<*[2,0]*> ^ (@ H) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
@ G is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
(<*[2,0]*> ^ (@ H)) ^ (@ G) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
F is Element of QC-WFF A
F is Element of QC-WFF A
F '&' F is Element of QC-WFF A
@ F is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[2,0]*> ^ (@ F) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
@ F is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
(<*[2,0]*> ^ (@ F)) ^ (@ F) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(@ H) ^ (@ G) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[2,0]*> ^ ((@ H) ^ (@ G)) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(@ F) ^ (@ F) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[2,0]*> ^ ((@ F) ^ (@ F)) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
len (@ F) is ext-real V4() V8() V9() V10() V14() V15() Element of NAT
len (@ H) is ext-real V4() V8() V9() V10() V14() V15() Element of NAT
F is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(@ H) ^ F is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
k is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(@ F) ^ k is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
F is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(@ H) ^ F is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
F is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(@ F) ^ F is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
k is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(@ H) ^ k is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
A is QC-alphabet
QC-WFF A is non empty set
H is Element of QC-WFF A
the_left_argument_of H is Element of QC-WFF A
the_right_argument_of H is Element of QC-WFF A
(the_left_argument_of H) '&' (the_right_argument_of H) is Element of QC-WFF A
[2,0] is V27() set
{2,0} is set
{2} is set
{{2,0},{2}} is set
<*[2,0]*> is non empty Relation-like NAT -defined Function-like V33() V40(1) FinSequence-like FinSubsequence-like set
@ (the_left_argument_of H) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
QC-symbols A is non empty set
rng A is set
K21(NAT,(QC-symbols A)) is set
<*[2,0]*> ^ (@ (the_left_argument_of H)) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
@ (the_right_argument_of H) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
(<*[2,0]*> ^ (@ (the_left_argument_of H))) ^ (@ (the_right_argument_of H)) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
G is Element of QC-WFF A
F is Element of QC-WFF A
G '&' F is Element of QC-WFF A
@ G is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[2,0]*> ^ (@ G) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
@ F is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
(<*[2,0]*> ^ (@ G)) ^ (@ F) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
A is QC-alphabet
QC-WFF A is non empty set
H is Element of QC-WFF A
G is Element of QC-WFF A
H '&' G is Element of QC-WFF A
[2,0] is V27() set
{2,0} is set
{2} is set
{{2,0},{2}} is set
<*[2,0]*> is non empty Relation-like NAT -defined Function-like V33() V40(1) FinSequence-like FinSubsequence-like set
@ H is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
QC-symbols A is non empty set
rng A is set
K21(NAT,(QC-symbols A)) is set
<*[2,0]*> ^ (@ H) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
@ G is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
(<*[2,0]*> ^ (@ H)) ^ (@ G) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
the_left_argument_of (H '&' G) is Element of QC-WFF A
the_right_argument_of (H '&' G) is Element of QC-WFF A
A is QC-alphabet
QC-variables A is set
6 is ext-real positive V4() non empty V8() V9() V10() V14() V15() Element of NAT
{6} is set
K21({6},NAT) is set
4 is ext-real positive V4() non empty V8() V9() V10() V14() V15() Element of NAT
5 is ext-real positive V4() non empty V8() V9() V10() V14() V15() Element of NAT
{4,5} is set
QC-symbols A is non empty set
rng A is set
K21({4,5},(QC-symbols A)) is set
K21({6},NAT) \/ K21({4,5},(QC-symbols A)) is set
bound_QC-variables A is Element of K20((QC-variables A))
K20((QC-variables A)) is set
{4} is set
K21({4},(QC-symbols A)) is set
QC-WFF A is non empty set
H is Element of bound_QC-variables A
G is Element of bound_QC-variables A
F is Element of QC-WFF A
All (H,F) is Element of QC-WFF A
[3,0] is V27() set
{3,0} is set
{3} is set
{{3,0},{3}} is set
<*[3,0]*> is non empty Relation-like NAT -defined Function-like V33() V40(1) FinSequence-like FinSubsequence-like set
<*H*> is non empty Relation-like NAT -defined bound_QC-variables A -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of bound_QC-variables A
<*[3,0]*> ^ <*H*> is non empty Relation-like NAT -defined Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like set
1 + 1 is ext-real V4() V8() V9() V10() V14() V15() Element of NAT
@ F is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
K21(NAT,(QC-symbols A)) is set
(<*[3,0]*> ^ <*H*>) ^ (@ F) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
F is Element of QC-WFF A
All (G,F) is Element of QC-WFF A
<*G*> is non empty Relation-like NAT -defined bound_QC-variables A -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of bound_QC-variables A
<*[3,0]*> ^ <*G*> is non empty Relation-like NAT -defined Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like set
@ F is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
(<*[3,0]*> ^ <*G*>) ^ (@ F) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
<*H*> is non empty Relation-like NAT -defined Function-like V33() V40(1) FinSequence-like FinSubsequence-like set
<*[3,0]*> ^ <*H*> is non empty Relation-like NAT -defined Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like set
(<*[3,0]*> ^ <*H*>) ^ (@ F) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
<*H*> ^ (@ F) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
<*[3,0]*> ^ (<*H*> ^ (@ F)) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
<*G*> is non empty Relation-like NAT -defined Function-like V33() V40(1) FinSequence-like FinSubsequence-like set
<*[3,0]*> ^ <*G*> is non empty Relation-like NAT -defined Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like set
(<*[3,0]*> ^ <*G*>) ^ (@ F) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
<*G*> ^ (@ F) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
<*[3,0]*> ^ (<*G*> ^ (@ F)) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(<*H*> ^ (@ F)) . 1 is set
(<*G*> ^ (@ F)) . 1 is set
A is QC-alphabet
QC-WFF A is non empty set
H is Element of QC-WFF A
bound_in H is Element of bound_QC-variables A
QC-variables A is set
6 is ext-real positive V4() non empty V8() V9() V10() V14() V15() Element of NAT
{6} is set
K21({6},NAT) is set
4 is ext-real positive V4() non empty V8() V9() V10() V14() V15() Element of NAT
5 is ext-real positive V4() non empty V8() V9() V10() V14() V15() Element of NAT
{4,5} is set
QC-symbols A is non empty set
rng A is set
K21({4,5},(QC-symbols A)) is set
K21({6},NAT) \/ K21({4,5},(QC-symbols A)) is set
bound_QC-variables A is Element of K20((QC-variables A))
K20((QC-variables A)) is set
{4} is set
K21({4},(QC-symbols A)) is set
the_scope_of H is Element of QC-WFF A
All ((bound_in H),(the_scope_of H)) is Element of QC-WFF A
[3,0] is V27() set
{3,0} is set
{3} is set
{{3,0},{3}} is set
<*[3,0]*> is non empty Relation-like NAT -defined Function-like V33() V40(1) FinSequence-like FinSubsequence-like set
<*(bound_in H)*> is non empty Relation-like NAT -defined bound_QC-variables A -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of bound_QC-variables A
<*[3,0]*> ^ <*(bound_in H)*> is non empty Relation-like NAT -defined Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like set
1 + 1 is ext-real V4() V8() V9() V10() V14() V15() Element of NAT
@ (the_scope_of H) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
K21(NAT,(QC-symbols A)) is set
(<*[3,0]*> ^ <*(bound_in H)*>) ^ (@ (the_scope_of H)) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
G is Element of bound_QC-variables A
F is Element of QC-WFF A
All (G,F) is Element of QC-WFF A
<*G*> is non empty Relation-like NAT -defined bound_QC-variables A -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of bound_QC-variables A
<*[3,0]*> ^ <*G*> is non empty Relation-like NAT -defined Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like set
@ F is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
(<*[3,0]*> ^ <*G*>) ^ (@ F) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
A is QC-alphabet
QC-variables A is set
6 is ext-real positive V4() non empty V8() V9() V10() V14() V15() Element of NAT
{6} is set
K21({6},NAT) is set
4 is ext-real positive V4() non empty V8() V9() V10() V14() V15() Element of NAT
5 is ext-real positive V4() non empty V8() V9() V10() V14() V15() Element of NAT
{4,5} is set
QC-symbols A is non empty set
rng A is set
K21({4,5},(QC-symbols A)) is set
K21({6},NAT) \/ K21({4,5},(QC-symbols A)) is set
bound_QC-variables A is Element of K20((QC-variables A))
K20((QC-variables A)) is set
{4} is set
K21({4},(QC-symbols A)) is set
QC-WFF A is non empty set
H is Element of bound_QC-variables A
G is Element of QC-WFF A
All (H,G) is Element of QC-WFF A
[3,0] is V27() set
{3,0} is set
{3} is set
{{3,0},{3}} is set
<*[3,0]*> is non empty Relation-like NAT -defined Function-like V33() V40(1) FinSequence-like FinSubsequence-like set
<*H*> is non empty Relation-like NAT -defined bound_QC-variables A -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of bound_QC-variables A
<*[3,0]*> ^ <*H*> is non empty Relation-like NAT -defined Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like set
1 + 1 is ext-real V4() V8() V9() V10() V14() V15() Element of NAT
@ G is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
K21(NAT,(QC-symbols A)) is set
(<*[3,0]*> ^ <*H*>) ^ (@ G) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
bound_in (All (H,G)) is Element of bound_QC-variables A
the_scope_of (All (H,G)) is Element of QC-WFF A
All ((bound_in (All (H,G))),(the_scope_of (All (H,G)))) is Element of QC-WFF A
<*(bound_in (All (H,G)))*> is non empty Relation-like NAT -defined bound_QC-variables A -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of bound_QC-variables A
<*[3,0]*> ^ <*(bound_in (All (H,G)))*> is non empty Relation-like NAT -defined Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like set
@ (the_scope_of (All (H,G))) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
(<*[3,0]*> ^ <*(bound_in (All (H,G)))*>) ^ (@ (the_scope_of (All (H,G)))) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
A is QC-alphabet
VERUM A is Element of QC-WFF A
QC-WFF A is non empty set
[0,0] is V27() set
{0,0} is set
{0} is set
{{0,0},{0}} is set
<*[0,0]*> is non empty Relation-like NAT -defined Function-like V33() V40(1) FinSequence-like FinSubsequence-like set
'not' (VERUM A) is Element of QC-WFF A
[1,0] is V27() set
{1,0} is set
{1} is set
{{1,0},{1}} is set
<*[1,0]*> is non empty Relation-like NAT -defined Function-like V33() V40(1) FinSequence-like FinSubsequence-like set
@ (VERUM A) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
QC-symbols A is non empty set
rng A is set
K21(NAT,(QC-symbols A)) is set
<*[1,0]*> ^ (@ (VERUM A)) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
H is Element of QC-WFF A
G is Element of QC-WFF A
'not' G is Element of QC-WFF A
@ G is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[1,0]*> ^ (@ G) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
H '&' ('not' G) is Element of QC-WFF A
[2,0] is V27() set
{2,0} is set
{2} is set
{{2,0},{2}} is set
<*[2,0]*> is non empty Relation-like NAT -defined Function-like V33() V40(1) FinSequence-like FinSubsequence-like set
@ H is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[2,0]*> ^ (@ H) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
@ ('not' G) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
(<*[2,0]*> ^ (@ H)) ^ (@ ('not' G)) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
'not' (H '&' ('not' G)) is Element of QC-WFF A
@ (H '&' ('not' G)) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[1,0]*> ^ (@ (H '&' ('not' G))) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
'not' H is Element of QC-WFF A
<*[1,0]*> ^ (@ H) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
('not' H) '&' ('not' G) is Element of QC-WFF A
@ ('not' H) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[2,0]*> ^ (@ ('not' H)) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(<*[2,0]*> ^ (@ ('not' H))) ^ (@ ('not' G)) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
'not' (('not' H) '&' ('not' G)) is Element of QC-WFF A
@ (('not' H) '&' ('not' G)) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[1,0]*> ^ (@ (('not' H) '&' ('not' G))) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
A is QC-alphabet
QC-WFF A is non empty set
H is Element of QC-WFF A
G is Element of QC-WFF A
(A,H,G) is Element of QC-WFF A
'not' G is Element of QC-WFF A
@ G is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
QC-symbols A is non empty set
rng A is set
K21(NAT,(QC-symbols A)) is set
<*[1,0]*> ^ (@ G) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
H '&' ('not' G) is Element of QC-WFF A
@ H is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[2,0]*> ^ (@ H) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
@ ('not' G) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
(<*[2,0]*> ^ (@ H)) ^ (@ ('not' G)) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
'not' (H '&' ('not' G)) is Element of QC-WFF A
@ (H '&' ('not' G)) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[1,0]*> ^ (@ (H '&' ('not' G))) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(A,G,H) is Element of QC-WFF A
'not' H is Element of QC-WFF A
<*[1,0]*> ^ (@ H) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
G '&' ('not' H) is Element of QC-WFF A
<*[2,0]*> ^ (@ G) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
@ ('not' H) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
(<*[2,0]*> ^ (@ G)) ^ (@ ('not' H)) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
'not' (G '&' ('not' H)) is Element of QC-WFF A
@ (G '&' ('not' H)) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[1,0]*> ^ (@ (G '&' ('not' H))) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(A,H,G) '&' (A,G,H) is Element of QC-WFF A
@ (A,H,G) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[2,0]*> ^ (@ (A,H,G)) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
@ (A,G,H) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
(<*[2,0]*> ^ (@ (A,H,G))) ^ (@ (A,G,H)) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
A is QC-alphabet
QC-variables A is set
6 is ext-real positive V4() non empty V8() V9() V10() V14() V15() Element of NAT
{6} is set
K21({6},NAT) is set
4 is ext-real positive V4() non empty V8() V9() V10() V14() V15() Element of NAT
5 is ext-real positive V4() non empty V8() V9() V10() V14() V15() Element of NAT
{4,5} is set
QC-symbols A is non empty set
rng A is set
K21({4,5},(QC-symbols A)) is set
K21({6},NAT) \/ K21({4,5},(QC-symbols A)) is set
bound_QC-variables A is Element of K20((QC-variables A))
K20((QC-variables A)) is set
{4} is set
K21({4},(QC-symbols A)) is set
QC-WFF A is non empty set
H is Element of bound_QC-variables A
G is Element of QC-WFF A
'not' G is Element of QC-WFF A
@ G is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
K21(NAT,(QC-symbols A)) is set
<*[1,0]*> ^ (@ G) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
All (H,('not' G)) is Element of QC-WFF A
[3,0] is V27() set
{3,0} is set
{3} is set
{{3,0},{3}} is set
<*[3,0]*> is non empty Relation-like NAT -defined Function-like V33() V40(1) FinSequence-like FinSubsequence-like set
<*H*> is non empty Relation-like NAT -defined bound_QC-variables A -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of bound_QC-variables A
<*[3,0]*> ^ <*H*> is non empty Relation-like NAT -defined Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like set
1 + 1 is ext-real V4() V8() V9() V10() V14() V15() Element of NAT
@ ('not' G) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
(<*[3,0]*> ^ <*H*>) ^ (@ ('not' G)) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
'not' (All (H,('not' G))) is Element of QC-WFF A
@ (All (H,('not' G))) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[1,0]*> ^ (@ (All (H,('not' G)))) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
A is QC-alphabet
(A) is Element of QC-WFF A
QC-WFF A is non empty set
VERUM A is Element of QC-WFF A
'not' (VERUM A) is Element of QC-WFF A
@ (VERUM A) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
QC-symbols A is non empty set
rng A is set
K21(NAT,(QC-symbols A)) is set
<*[1,0]*> ^ (@ (VERUM A)) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
H is QC-alphabet
(H) is Element of QC-WFF H
QC-WFF H is non empty set
VERUM H is Element of QC-WFF H
'not' (VERUM H) is Element of QC-WFF H
@ (VERUM H) is Relation-like NAT -defined K21(NAT,(QC-symbols H)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols H))
QC-symbols H is non empty set
rng H is set
K21(NAT,(QC-symbols H)) is set
<*[1,0]*> ^ (@ (VERUM H)) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
the_argument_of (H) is Element of QC-WFF H
A is QC-alphabet
QC-WFF A is non empty set
H is Element of QC-WFF A
G is Element of QC-WFF A
(A,H,G) is Element of QC-WFF A
'not' H is Element of QC-WFF A
@ H is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
QC-symbols A is non empty set
rng A is set
K21(NAT,(QC-symbols A)) is set
<*[1,0]*> ^ (@ H) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
'not' G is Element of QC-WFF A
@ G is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[1,0]*> ^ (@ G) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
('not' H) '&' ('not' G) is Element of QC-WFF A
@ ('not' H) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[2,0]*> ^ (@ ('not' H)) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
@ ('not' G) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
(<*[2,0]*> ^ (@ ('not' H))) ^ (@ ('not' G)) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
'not' (('not' H) '&' ('not' G)) is Element of QC-WFF A
@ (('not' H) '&' ('not' G)) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[1,0]*> ^ (@ (('not' H) '&' ('not' G))) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(A,('not' H),G) is Element of QC-WFF A
A is QC-alphabet
QC-WFF A is non empty set
H is Element of QC-WFF A
G is Element of QC-WFF A
(A,H,G) is Element of QC-WFF A
'not' H is Element of QC-WFF A
@ H is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
QC-symbols A is non empty set
rng A is set
K21(NAT,(QC-symbols A)) is set
<*[1,0]*> ^ (@ H) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
'not' G is Element of QC-WFF A
@ G is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[1,0]*> ^ (@ G) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
('not' H) '&' ('not' G) is Element of QC-WFF A
@ ('not' H) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[2,0]*> ^ (@ ('not' H)) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
@ ('not' G) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
(<*[2,0]*> ^ (@ ('not' H))) ^ (@ ('not' G)) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
'not' (('not' H) '&' ('not' G)) is Element of QC-WFF A
@ (('not' H) '&' ('not' G)) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[1,0]*> ^ (@ (('not' H) '&' ('not' G))) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
F is Element of QC-WFF A
F is Element of QC-WFF A
(A,F,F) is Element of QC-WFF A
'not' F is Element of QC-WFF A
@ F is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[1,0]*> ^ (@ F) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
'not' F is Element of QC-WFF A
@ F is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[1,0]*> ^ (@ F) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
('not' F) '&' ('not' F) is Element of QC-WFF A
@ ('not' F) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[2,0]*> ^ (@ ('not' F)) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
@ ('not' F) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
(<*[2,0]*> ^ (@ ('not' F))) ^ (@ ('not' F)) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
'not' (('not' F) '&' ('not' F)) is Element of QC-WFF A
@ (('not' F) '&' ('not' F)) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[1,0]*> ^ (@ (('not' F) '&' ('not' F))) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
A is QC-alphabet
QC-WFF A is non empty set
H is Element of QC-WFF A
G is Element of QC-WFF A
(A,H,G) is Element of QC-WFF A
'not' G is Element of QC-WFF A
@ G is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
QC-symbols A is non empty set
rng A is set
K21(NAT,(QC-symbols A)) is set
<*[1,0]*> ^ (@ G) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
H '&' ('not' G) is Element of QC-WFF A
@ H is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[2,0]*> ^ (@ H) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
@ ('not' G) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
(<*[2,0]*> ^ (@ H)) ^ (@ ('not' G)) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
'not' (H '&' ('not' G)) is Element of QC-WFF A
@ (H '&' ('not' G)) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[1,0]*> ^ (@ (H '&' ('not' G))) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
F is Element of QC-WFF A
F is Element of QC-WFF A
(A,F,F) is Element of QC-WFF A
'not' F is Element of QC-WFF A
@ F is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[1,0]*> ^ (@ F) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
F '&' ('not' F) is Element of QC-WFF A
@ F is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[2,0]*> ^ (@ F) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
@ ('not' F) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
(<*[2,0]*> ^ (@ F)) ^ (@ ('not' F)) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
'not' (F '&' ('not' F)) is Element of QC-WFF A
@ (F '&' ('not' F)) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[1,0]*> ^ (@ (F '&' ('not' F))) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
A is QC-alphabet
QC-WFF A is non empty set
H is Element of QC-WFF A
G is Element of QC-WFF A
(A,H,G) is Element of QC-WFF A
(A,H,G) is Element of QC-WFF A
'not' G is Element of QC-WFF A
@ G is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
QC-symbols A is non empty set
rng A is set
K21(NAT,(QC-symbols A)) is set
<*[1,0]*> ^ (@ G) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
H '&' ('not' G) is Element of QC-WFF A
@ H is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[2,0]*> ^ (@ H) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
@ ('not' G) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
(<*[2,0]*> ^ (@ H)) ^ (@ ('not' G)) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
'not' (H '&' ('not' G)) is Element of QC-WFF A
@ (H '&' ('not' G)) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[1,0]*> ^ (@ (H '&' ('not' G))) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(A,G,H) is Element of QC-WFF A
'not' H is Element of QC-WFF A
<*[1,0]*> ^ (@ H) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
G '&' ('not' H) is Element of QC-WFF A
<*[2,0]*> ^ (@ G) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
@ ('not' H) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
(<*[2,0]*> ^ (@ G)) ^ (@ ('not' H)) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
'not' (G '&' ('not' H)) is Element of QC-WFF A
@ (G '&' ('not' H)) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[1,0]*> ^ (@ (G '&' ('not' H))) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(A,H,G) '&' (A,G,H) is Element of QC-WFF A
@ (A,H,G) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[2,0]*> ^ (@ (A,H,G)) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
@ (A,G,H) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
(<*[2,0]*> ^ (@ (A,H,G))) ^ (@ (A,G,H)) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
F is Element of QC-WFF A
F is Element of QC-WFF A
(A,F,F) is Element of QC-WFF A
(A,F,F) is Element of QC-WFF A
'not' F is Element of QC-WFF A
@ F is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[1,0]*> ^ (@ F) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
F '&' ('not' F) is Element of QC-WFF A
@ F is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[2,0]*> ^ (@ F) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
@ ('not' F) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
(<*[2,0]*> ^ (@ F)) ^ (@ ('not' F)) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
'not' (F '&' ('not' F)) is Element of QC-WFF A
@ (F '&' ('not' F)) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[1,0]*> ^ (@ (F '&' ('not' F))) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(A,F,F) is Element of QC-WFF A
'not' F is Element of QC-WFF A
<*[1,0]*> ^ (@ F) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
F '&' ('not' F) is Element of QC-WFF A
<*[2,0]*> ^ (@ F) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
@ ('not' F) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
(<*[2,0]*> ^ (@ F)) ^ (@ ('not' F)) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
'not' (F '&' ('not' F)) is Element of QC-WFF A
@ (F '&' ('not' F)) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[1,0]*> ^ (@ (F '&' ('not' F))) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(A,F,F) '&' (A,F,F) is Element of QC-WFF A
@ (A,F,F) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[2,0]*> ^ (@ (A,F,F)) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
@ (A,F,F) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
(<*[2,0]*> ^ (@ (A,F,F))) ^ (@ (A,F,F)) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
A is QC-alphabet
QC-variables A is set
QC-symbols A is non empty set
rng A is set
K21({4,5},(QC-symbols A)) is set
K21({6},NAT) \/ K21({4,5},(QC-symbols A)) is set
bound_QC-variables A is Element of K20((QC-variables A))
K20((QC-variables A)) is set
K21({4},(QC-symbols A)) is set
QC-WFF A is non empty set
H is Element of bound_QC-variables A
G is Element of bound_QC-variables A
F is Element of QC-WFF A
(A,H,F) is Element of QC-WFF A
'not' F is Element of QC-WFF A
@ F is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
K21(NAT,(QC-symbols A)) is set
<*[1,0]*> ^ (@ F) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
All (H,('not' F)) is Element of QC-WFF A
<*H*> is non empty Relation-like NAT -defined bound_QC-variables A -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of bound_QC-variables A
<*[3,0]*> ^ <*H*> is non empty Relation-like NAT -defined Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like set
@ ('not' F) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
(<*[3,0]*> ^ <*H*>) ^ (@ ('not' F)) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
'not' (All (H,('not' F))) is Element of QC-WFF A
@ (All (H,('not' F))) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[1,0]*> ^ (@ (All (H,('not' F)))) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
F is Element of QC-WFF A
(A,G,F) is Element of QC-WFF A
'not' F is Element of QC-WFF A
@ F is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[1,0]*> ^ (@ F) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
All (G,('not' F)) is Element of QC-WFF A
<*G*> is non empty Relation-like NAT -defined bound_QC-variables A -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of bound_QC-variables A
<*[3,0]*> ^ <*G*> is non empty Relation-like NAT -defined Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like set
@ ('not' F) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
(<*[3,0]*> ^ <*G*>) ^ (@ ('not' F)) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
'not' (All (G,('not' F))) is Element of QC-WFF A
@ (All (G,('not' F))) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[1,0]*> ^ (@ (All (G,('not' F)))) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
A is QC-alphabet
QC-variables A is set
QC-symbols A is non empty set
rng A is set
K21({4,5},(QC-symbols A)) is set
K21({6},NAT) \/ K21({4,5},(QC-symbols A)) is set
bound_QC-variables A is Element of K20((QC-variables A))
K20((QC-variables A)) is set
K21({4},(QC-symbols A)) is set
QC-WFF A is non empty set
H is Element of bound_QC-variables A
G is Element of bound_QC-variables A
F is Element of QC-WFF A
All (G,F) is Element of QC-WFF A
<*G*> is non empty Relation-like NAT -defined bound_QC-variables A -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of bound_QC-variables A
<*[3,0]*> ^ <*G*> is non empty Relation-like NAT -defined Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like set
@ F is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
K21(NAT,(QC-symbols A)) is set
(<*[3,0]*> ^ <*G*>) ^ (@ F) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
All (H,(All (G,F))) is Element of QC-WFF A
<*H*> is non empty Relation-like NAT -defined bound_QC-variables A -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of bound_QC-variables A
<*[3,0]*> ^ <*H*> is non empty Relation-like NAT -defined Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like set
@ (All (G,F)) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
(<*[3,0]*> ^ <*H*>) ^ (@ (All (G,F))) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(A,G,F) is Element of QC-WFF A
'not' F is Element of QC-WFF A
<*[1,0]*> ^ (@ F) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
All (G,('not' F)) is Element of QC-WFF A
@ ('not' F) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
(<*[3,0]*> ^ <*G*>) ^ (@ ('not' F)) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
'not' (All (G,('not' F))) is Element of QC-WFF A
@ (All (G,('not' F))) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[1,0]*> ^ (@ (All (G,('not' F)))) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(A,H,(A,G,F)) is Element of QC-WFF A
'not' (A,G,F) is Element of QC-WFF A
@ (A,G,F) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[1,0]*> ^ (@ (A,G,F)) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
All (H,('not' (A,G,F))) is Element of QC-WFF A
@ ('not' (A,G,F)) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
(<*[3,0]*> ^ <*H*>) ^ (@ ('not' (A,G,F))) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
'not' (All (H,('not' (A,G,F)))) is Element of QC-WFF A
@ (All (H,('not' (A,G,F)))) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[1,0]*> ^ (@ (All (H,('not' (A,G,F))))) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
A is QC-alphabet
QC-variables A is set
QC-symbols A is non empty set
rng A is set
K21({4,5},(QC-symbols A)) is set
K21({6},NAT) \/ K21({4,5},(QC-symbols A)) is set
bound_QC-variables A is Element of K20((QC-variables A))
K20((QC-variables A)) is set
K21({4},(QC-symbols A)) is set
QC-WFF A is non empty set
F is QC-alphabet
QC-variables F is set
QC-symbols F is non empty set
rng F is set
K21({4,5},(QC-symbols F)) is set
K21({6},NAT) \/ K21({4,5},(QC-symbols F)) is set
bound_QC-variables F is Element of K20((QC-variables F))
K20((QC-variables F)) is set
K21({4},(QC-symbols F)) is set
QC-WFF F is non empty set
H is Element of bound_QC-variables A
G is Element of bound_QC-variables A
F is Element of QC-WFF A
(A,H,G,F) is Element of QC-WFF A
All (G,F) is Element of QC-WFF A
<*G*> is non empty Relation-like NAT -defined bound_QC-variables A -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of bound_QC-variables A
<*[3,0]*> ^ <*G*> is non empty Relation-like NAT -defined Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like set
@ F is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
K21(NAT,(QC-symbols A)) is set
(<*[3,0]*> ^ <*G*>) ^ (@ F) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
All (H,(All (G,F))) is Element of QC-WFF A
<*H*> is non empty Relation-like NAT -defined bound_QC-variables A -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of bound_QC-variables A
<*[3,0]*> ^ <*H*> is non empty Relation-like NAT -defined Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like set
@ (All (G,F)) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
(<*[3,0]*> ^ <*H*>) ^ (@ (All (G,F))) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
F is Element of bound_QC-variables F
k is Element of bound_QC-variables F
k is Element of QC-WFF F
(F,F,k,k) is Element of QC-WFF F
(F,k,k) is Element of QC-WFF F
'not' k is Element of QC-WFF F
@ k is Relation-like NAT -defined K21(NAT,(QC-symbols F)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols F))
K21(NAT,(QC-symbols F)) is set
<*[1,0]*> ^ (@ k) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
All (k,('not' k)) is Element of QC-WFF F
<*k*> is non empty Relation-like NAT -defined bound_QC-variables F -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of bound_QC-variables F
<*[3,0]*> ^ <*k*> is non empty Relation-like NAT -defined Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like set
@ ('not' k) is Relation-like NAT -defined K21(NAT,(QC-symbols F)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols F))
(<*[3,0]*> ^ <*k*>) ^ (@ ('not' k)) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
'not' (All (k,('not' k))) is Element of QC-WFF F
@ (All (k,('not' k))) is Relation-like NAT -defined K21(NAT,(QC-symbols F)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols F))
<*[1,0]*> ^ (@ (All (k,('not' k)))) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(F,F,(F,k,k)) is Element of QC-WFF F
'not' (F,k,k) is Element of QC-WFF F
@ (F,k,k) is Relation-like NAT -defined K21(NAT,(QC-symbols F)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols F))
<*[1,0]*> ^ (@ (F,k,k)) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
All (F,('not' (F,k,k))) is Element of QC-WFF F
<*F*> is non empty Relation-like NAT -defined bound_QC-variables F -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of bound_QC-variables F
<*[3,0]*> ^ <*F*> is non empty Relation-like NAT -defined Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like set
@ ('not' (F,k,k)) is Relation-like NAT -defined K21(NAT,(QC-symbols F)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols F))
(<*[3,0]*> ^ <*F*>) ^ (@ ('not' (F,k,k))) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
'not' (All (F,('not' (F,k,k)))) is Element of QC-WFF F
@ (All (F,('not' (F,k,k)))) is Relation-like NAT -defined K21(NAT,(QC-symbols F)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols F))
<*[1,0]*> ^ (@ (All (F,('not' (F,k,k))))) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
A is QC-alphabet
QC-WFF A is non empty set
QC-variables A is set
QC-symbols A is non empty set
rng A is set
K21({4,5},(QC-symbols A)) is set
K21({6},NAT) \/ K21({4,5},(QC-symbols A)) is set
bound_QC-variables A is Element of K20((QC-variables A))
K20((QC-variables A)) is set
K21({4},(QC-symbols A)) is set
H is Element of QC-WFF A
G is Element of QC-WFF A
F is Element of bound_QC-variables A
F is Element of bound_QC-variables A
(A,F,F,H) is Element of QC-WFF A
All (F,H) is Element of QC-WFF A
<*F*> is non empty Relation-like NAT -defined bound_QC-variables A -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of bound_QC-variables A
<*[3,0]*> ^ <*F*> is non empty Relation-like NAT -defined Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like set
@ H is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
K21(NAT,(QC-symbols A)) is set
(<*[3,0]*> ^ <*F*>) ^ (@ H) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
All (F,(All (F,H))) is Element of QC-WFF A
<*F*> is non empty Relation-like NAT -defined bound_QC-variables A -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of bound_QC-variables A
<*[3,0]*> ^ <*F*> is non empty Relation-like NAT -defined Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like set
@ (All (F,H)) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
(<*[3,0]*> ^ <*F*>) ^ (@ (All (F,H))) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
F is Element of bound_QC-variables A
k is Element of bound_QC-variables A
(A,F,k,G) is Element of QC-WFF A
All (k,G) is Element of QC-WFF A
<*k*> is non empty Relation-like NAT -defined bound_QC-variables A -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of bound_QC-variables A
<*[3,0]*> ^ <*k*> is non empty Relation-like NAT -defined Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like set
@ G is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
(<*[3,0]*> ^ <*k*>) ^ (@ G) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
All (F,(All (k,G))) is Element of QC-WFF A
<*F*> is non empty Relation-like NAT -defined bound_QC-variables A -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of bound_QC-variables A
<*[3,0]*> ^ <*F*> is non empty Relation-like NAT -defined Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like set
@ (All (k,G)) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
(<*[3,0]*> ^ <*F*>) ^ (@ (All (k,G))) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
A is QC-alphabet
QC-variables A is set
QC-symbols A is non empty set
rng A is set
K21({4,5},(QC-symbols A)) is set
K21({6},NAT) \/ K21({4,5},(QC-symbols A)) is set
bound_QC-variables A is Element of K20((QC-variables A))
K20((QC-variables A)) is set
K21({4},(QC-symbols A)) is set
QC-WFF A is non empty set
H is Element of bound_QC-variables A
G is Element of bound_QC-variables A
F is Element of QC-WFF A
(A,H,G,F) is Element of QC-WFF A
All (G,F) is Element of QC-WFF A
<*G*> is non empty Relation-like NAT -defined bound_QC-variables A -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of bound_QC-variables A
<*[3,0]*> ^ <*G*> is non empty Relation-like NAT -defined Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like set
@ F is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
K21(NAT,(QC-symbols A)) is set
(<*[3,0]*> ^ <*G*>) ^ (@ F) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
All (H,(All (G,F))) is Element of QC-WFF A
<*H*> is non empty Relation-like NAT -defined bound_QC-variables A -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of bound_QC-variables A
<*[3,0]*> ^ <*H*> is non empty Relation-like NAT -defined Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like set
@ (All (G,F)) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
(<*[3,0]*> ^ <*H*>) ^ (@ (All (G,F))) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
F is Element of bound_QC-variables A
F is Element of QC-WFF A
All (F,F) is Element of QC-WFF A
<*F*> is non empty Relation-like NAT -defined bound_QC-variables A -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of bound_QC-variables A
<*[3,0]*> ^ <*F*> is non empty Relation-like NAT -defined Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like set
@ F is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
(<*[3,0]*> ^ <*F*>) ^ (@ F) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
A is QC-alphabet
QC-WFF A is non empty set
QC-variables A is set
QC-symbols A is non empty set
rng A is set
K21({4,5},(QC-symbols A)) is set
K21({6},NAT) \/ K21({4,5},(QC-symbols A)) is set
bound_QC-variables A is Element of K20((QC-variables A))
K20((QC-variables A)) is set
K21({4},(QC-symbols A)) is set
H is Element of QC-WFF A
G is Element of QC-WFF A
F is Element of bound_QC-variables A
F is Element of bound_QC-variables A
(A,F,F,H) is Element of QC-WFF A
(A,F,H) is Element of QC-WFF A
'not' H is Element of QC-WFF A
@ H is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
K21(NAT,(QC-symbols A)) is set
<*[1,0]*> ^ (@ H) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
All (F,('not' H)) is Element of QC-WFF A
<*F*> is non empty Relation-like NAT -defined bound_QC-variables A -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of bound_QC-variables A
<*[3,0]*> ^ <*F*> is non empty Relation-like NAT -defined Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like set
@ ('not' H) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
(<*[3,0]*> ^ <*F*>) ^ (@ ('not' H)) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
'not' (All (F,('not' H))) is Element of QC-WFF A
@ (All (F,('not' H))) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[1,0]*> ^ (@ (All (F,('not' H)))) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(A,F,(A,F,H)) is Element of QC-WFF A
'not' (A,F,H) is Element of QC-WFF A
@ (A,F,H) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[1,0]*> ^ (@ (A,F,H)) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
All (F,('not' (A,F,H))) is Element of QC-WFF A
<*F*> is non empty Relation-like NAT -defined bound_QC-variables A -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of bound_QC-variables A
<*[3,0]*> ^ <*F*> is non empty Relation-like NAT -defined Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like set
@ ('not' (A,F,H)) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
(<*[3,0]*> ^ <*F*>) ^ (@ ('not' (A,F,H))) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
'not' (All (F,('not' (A,F,H)))) is Element of QC-WFF A
@ (All (F,('not' (A,F,H)))) is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of K21(NAT,(QC-symbols A))
<*[1,0]*> ^ (@ (All (F,('not' (A,F,H))))) is non empty Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
F is Element of bound_QC-variables A
k is Element of bound_QC-variables A
(A,F,k,G) is Element of QC-WFF A
(A,k,G) is Element of QC-WFF A
'not' G is Element of QC-WFF A
@ G is Relation-like NAT -defined K21(NAT,(QC-symbols A)) -valued