REAL is V24() V25() V26() V30() set
NAT is non empty V24() V25() V26() V27() V28() V29() V30() V31() V32() V33() Element of bool REAL
bool REAL is non empty set
NAT is non empty V24() V25() V26() V27() V28() V29() V30() V31() V32() V33() set
bool NAT is non empty set
bool NAT is non empty set
{} is set
1 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
F1() is V1() non empty QC-alphabet
QC-WFF F1() is non empty set
F2() is non empty set
[:(QC-WFF F1()),F2():] is non empty set
bool [:(QC-WFF F1()),F2():] is non empty set
VERUM F1() is Element of QC-WFF F1()
K98() is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
[K98(),K98()] is set
{K98(),K98()} is V24() V25() V26() V27() V28() V29() set
{K98()} is V24() V25() V26() V27() V28() V29() set
{{K98(),K98()},{K98()}} is set
<*[K98(),K98()]*> is V1() Function-like set
F3() is V1() V4( QC-WFF F1()) V5(F2()) Function-like V18( QC-WFF F1(),F2()) Element of bool [:(QC-WFF F1()),F2():]
F5() is Element of F2()
F4() is V1() V4( QC-WFF F1()) V5(F2()) Function-like V18( QC-WFF F1(),F2()) Element of bool [:(QC-WFF F1()),F2():]
QC-pred_symbols F1() is non empty set
QC-symbols F1() is non empty set
K49(F1()) is set
7 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
{ [b1,b2] where b1 is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT , b2 is Element of QC-symbols F1() : 7 <= b1 } is set
QC-variables F1() is non empty set
6 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
{6} is V24() V25() V26() V27() V28() V29() set
[:{6},NAT:] is set
4 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
5 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
{4,5} is V24() V25() V26() V27() V28() V29() set
[:{4,5},(QC-symbols F1()):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols F1()):] is set
A is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
A -ary_QC-pred_symbols F1() is non empty Element of bool (QC-pred_symbols F1())
bool (QC-pred_symbols F1()) is non empty set
{ b1 where b1 is Element of QC-pred_symbols F1() : the_arity_of b1 = A } is set
x is Element of A -ary_QC-pred_symbols F1()
p is V1() V4( NAT ) V5( QC-variables F1()) Function-like V45(A) FinSequence-like FinSequence of QC-variables F1()
x ! p is Element of QC-WFF F1()
F3() . (x ! p) is Element of F2()
F4() . (x ! p) is Element of F2()
F6((x ! p)) is Element of F2()
bound_QC-variables F1() is non empty Element of bool (QC-variables F1())
bool (QC-variables F1()) is non empty set
{4} is V24() V25() V26() V27() V28() V29() set
[:{4},(QC-symbols F1()):] is set
A is Element of bound_QC-variables F1()
x is Element of QC-WFF F1()
F3() . x is Element of F2()
F4() . x is Element of F2()
All (A,x) is Element of QC-WFF F1()
3 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
[3,K98()] is set
{3,K98()} is V24() V25() V26() V27() V28() V29() set
{3} is V24() V25() V26() V27() V28() V29() set
{{3,K98()},{3}} is set
<*[3,K98()]*> is V1() Function-like set
<*A*> is V1() V4( NAT ) V5( bound_QC-variables F1()) Function-like FinSequence-like FinSequence of bound_QC-variables F1()
K113(<*[3,K98()]*>,<*A*>) is V1() Function-like FinSequence-like set
@ x is V1() V4( NAT ) V5([:NAT,(QC-symbols F1()):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols F1()):]
[:NAT,(QC-symbols F1()):] is non empty set
K113(K113(<*[3,K98()]*>,<*A*>),(@ x)) is V1() Function-like FinSequence-like set
F3() . (All (A,x)) is Element of F2()
F4() . (All (A,x)) is Element of F2()
the_scope_of (All (A,x)) is Element of QC-WFF F1()
F4() . (the_scope_of (All (A,x))) is Element of F2()
F9((All (A,x)),(F4() . (the_scope_of (All (A,x))))) is Element of F2()
A is Element of QC-WFF F1()
F3() . A is Element of F2()
F4() . A is Element of F2()
x is Element of QC-WFF F1()
F3() . x is Element of F2()
F4() . x is Element of F2()
A '&' x is Element of QC-WFF F1()
2 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
[2,K98()] is set
{2,K98()} is V24() V25() V26() V27() V28() V29() set
{2} is V24() V25() V26() V27() V28() V29() set
{{2,K98()},{2}} is set
<*[2,K98()]*> is V1() Function-like set
@ A is V1() V4( NAT ) V5([:NAT,(QC-symbols F1()):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols F1()):]
[:NAT,(QC-symbols F1()):] is non empty set
K113(<*[2,K98()]*>,(@ A)) is V1() Function-like FinSequence-like set
@ x is V1() V4( NAT ) V5([:NAT,(QC-symbols F1()):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols F1()):]
K113(K113(<*[2,K98()]*>,(@ A)),(@ x)) is V1() Function-like FinSequence-like set
F3() . (A '&' x) is Element of F2()
F4() . (A '&' x) is Element of F2()
the_left_argument_of (A '&' x) is Element of QC-WFF F1()
the_right_argument_of (A '&' x) is Element of QC-WFF F1()
F8((F4() . A),(F4() . x)) is Element of F2()
A is Element of QC-WFF F1()
F3() . A is Element of F2()
F4() . A is Element of F2()
'not' A is Element of QC-WFF F1()
[1,K98()] is set
{1,K98()} is V24() V25() V26() V27() V28() V29() set
{1} is V24() V25() V26() V27() V28() V29() set
{{1,K98()},{1}} is set
<*[1,K98()]*> is V1() Function-like set
@ A is V1() V4( NAT ) V5([:NAT,(QC-symbols F1()):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols F1()):]
[:NAT,(QC-symbols F1()):] is non empty set
K113(<*[1,K98()]*>,(@ A)) is V1() Function-like FinSequence-like set
F3() . ('not' A) is Element of F2()
F4() . ('not' A) is Element of F2()
the_argument_of ('not' A) is Element of QC-WFF F1()
F7((F4() . A)) is Element of F2()
F3() . (VERUM F1()) is Element of F2()
F4() . (VERUM F1()) is Element of F2()
F2() is non empty set
F1() is V1() non empty QC-alphabet
QC-WFF F1() is non empty set
[:(QC-WFF F1()),F2():] is non empty set
bool [:(QC-WFF F1()),F2():] is non empty set
F4() is Element of QC-WFF F1()
VERUM F1() is Element of QC-WFF F1()
K98() is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
[K98(),K98()] is set
{K98(),K98()} is V24() V25() V26() V27() V28() V29() set
{K98()} is V24() V25() V26() V27() V28() V29() set
{{K98(),K98()},{K98()}} is set
<*[K98(),K98()]*> is V1() Function-like set
F3() is Element of F2()
A is V1() V4( QC-WFF F1()) V5(F2()) Function-like V18( QC-WFF F1(),F2()) Element of bool [:(QC-WFF F1()),F2():]
A . (VERUM F1()) is Element of F2()
A . F4() is Element of F2()
x is Element of QC-WFF F1()
A . x is Element of F2()
p is Element of QC-WFF F1()
A . p is Element of F2()
F5(p) is Element of F2()
V is Element of QC-WFF F1()
x is Element of F2()
the_argument_of V is Element of QC-WFF F1()
A . (the_argument_of V) is Element of F2()
A . V is Element of F2()
F6(x) is Element of F2()
a1 is Element of QC-WFF F1()
a2 is Element of F2()
the_left_argument_of a1 is Element of QC-WFF F1()
A . (the_left_argument_of a1) is Element of F2()
c8 is Element of F2()
the_right_argument_of a1 is Element of QC-WFF F1()
A . (the_right_argument_of a1) is Element of F2()
A . a1 is Element of F2()
F7(a2,c8) is Element of F2()
c9 is Element of QC-WFF F1()
c10 is Element of F2()
the_scope_of c9 is Element of QC-WFF F1()
A . (the_scope_of c9) is Element of F2()
A . c9 is Element of F2()
F8(c9,c10) is Element of F2()
A is Element of F2()
x is Element of F2()
p is V1() V4( QC-WFF F1()) V5(F2()) Function-like V18( QC-WFF F1(),F2()) Element of bool [:(QC-WFF F1()),F2():]
p . F4() is Element of F2()
V is V1() V4( QC-WFF F1()) V5(F2()) Function-like V18( QC-WFF F1(),F2()) Element of bool [:(QC-WFF F1()),F2():]
V . F4() is Element of F2()
F1() is V1() non empty QC-alphabet
QC-WFF F1() is non empty set
F2() is non empty set
[:(QC-WFF F1()),F2():] is non empty set
bool [:(QC-WFF F1()),F2():] is non empty set
VERUM F1() is Element of QC-WFF F1()
K98() is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
[K98(),K98()] is set
{K98(),K98()} is V24() V25() V26() V27() V28() V29() set
{K98()} is V24() V25() V26() V27() V28() V29() set
{{K98(),K98()},{K98()}} is set
<*[K98(),K98()]*> is V1() Function-like set
F4() is Element of F2()
F3((VERUM F1())) is Element of F2()
A is V1() V4( QC-WFF F1()) V5(F2()) Function-like V18( QC-WFF F1(),F2()) Element of bool [:(QC-WFF F1()),F2():]
A . (VERUM F1()) is Element of F2()
F2() is non empty set
F1() is V1() non empty QC-alphabet
QC-WFF F1() is non empty set
[:(QC-WFF F1()),F2():] is non empty set
bool [:(QC-WFF F1()),F2():] is non empty set
VERUM F1() is Element of QC-WFF F1()
K98() is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
[K98(),K98()] is set
{K98(),K98()} is V24() V25() V26() V27() V28() V29() set
{K98()} is V24() V25() V26() V27() V28() V29() set
{{K98(),K98()},{K98()}} is set
<*[K98(),K98()]*> is V1() Function-like set
F3() is Element of F2()
F5() is Element of QC-WFF F1()
F4(F5()) is Element of F2()
F6(F5()) is Element of F2()
A is V1() V4( QC-WFF F1()) V5(F2()) Function-like V18( QC-WFF F1(),F2()) Element of bool [:(QC-WFF F1()),F2():]
A . F5() is Element of F2()
F2() is non empty set
F1() is V1() non empty QC-alphabet
QC-WFF F1() is non empty set
[:(QC-WFF F1()),F2():] is non empty set
bool [:(QC-WFF F1()),F2():] is non empty set
VERUM F1() is Element of QC-WFF F1()
K98() is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
[K98(),K98()] is set
{K98(),K98()} is V24() V25() V26() V27() V28() V29() set
{K98()} is V24() V25() V26() V27() V28() V29() set
{{K98(),K98()},{K98()}} is set
<*[K98(),K98()]*> is V1() Function-like set
F3() is Element of F2()
F4() is Element of QC-WFF F1()
F9(F4()) is Element of F2()
the_argument_of F4() is Element of QC-WFF F1()
F9((the_argument_of F4())) is Element of F2()
F6(F9((the_argument_of F4()))) is Element of F2()
A is V1() V4( QC-WFF F1()) V5(F2()) Function-like V18( QC-WFF F1(),F2()) Element of bool [:(QC-WFF F1()),F2():]
A . F4() is Element of F2()
A . (the_argument_of F4()) is Element of F2()
F2() is non empty set
F1() is V1() non empty QC-alphabet
QC-WFF F1() is non empty set
[:(QC-WFF F1()),F2():] is non empty set
bool [:(QC-WFF F1()),F2():] is non empty set
VERUM F1() is Element of QC-WFF F1()
K98() is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
[K98(),K98()] is set
{K98(),K98()} is V24() V25() V26() V27() V28() V29() set
{K98()} is V24() V25() V26() V27() V28() V29() set
{{K98(),K98()},{K98()}} is set
<*[K98(),K98()]*> is V1() Function-like set
F3() is Element of F2()
F9() is Element of QC-WFF F1()
the_left_argument_of F9() is Element of QC-WFF F1()
F8((the_left_argument_of F9())) is Element of F2()
the_right_argument_of F9() is Element of QC-WFF F1()
F8((the_right_argument_of F9())) is Element of F2()
F8(F9()) is Element of F2()
A is V1() V4( QC-WFF F1()) V5(F2()) Function-like V18( QC-WFF F1(),F2()) Element of bool [:(QC-WFF F1()),F2():]
A . F9() is Element of F2()
x is Element of F2()
p is Element of F2()
F6(x,p) is Element of F2()
A . (the_left_argument_of F9()) is Element of F2()
A . (the_right_argument_of F9()) is Element of F2()
F2() is non empty set
F1() is V1() non empty QC-alphabet
QC-WFF F1() is non empty set
[:(QC-WFF F1()),F2():] is non empty set
bool [:(QC-WFF F1()),F2():] is non empty set
VERUM F1() is Element of QC-WFF F1()
K98() is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
[K98(),K98()] is set
{K98(),K98()} is V24() V25() V26() V27() V28() V29() set
{K98()} is V24() V25() V26() V27() V28() V29() set
{{K98(),K98()},{K98()}} is set
<*[K98(),K98()]*> is V1() Function-like set
F3() is Element of F2()
F4() is Element of QC-WFF F1()
F9(F4()) is Element of F2()
the_scope_of F4() is Element of QC-WFF F1()
F9((the_scope_of F4())) is Element of F2()
F8(F4(),F9((the_scope_of F4()))) is Element of F2()
A is V1() V4( QC-WFF F1()) V5(F2()) Function-like V18( QC-WFF F1(),F2()) Element of bool [:(QC-WFF F1()),F2():]
A . F4() is Element of F2()
A . (the_scope_of F4()) is Element of F2()
A is V1() non empty QC-alphabet
QC-pred_symbols A is non empty set
QC-symbols A is non empty set
K49(A) is set
7 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
{ [b1,b2] where b1 is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT , b2 is Element of QC-symbols A : 7 <= b1 } is set
x is Element of QC-pred_symbols A
the_arity_of x is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
(the_arity_of x) -ary_QC-pred_symbols A is non empty Element of bool (QC-pred_symbols A)
bool (QC-pred_symbols A) is non empty set
{ b1 where b1 is Element of QC-pred_symbols A : the_arity_of b1 = the_arity_of x } is set
A is V1() non empty QC-alphabet
QC-variables A is non empty set
6 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
{6} is V24() V25() V26() V27() V28() V29() set
[:{6},NAT:] is set
4 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
5 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
{4,5} is V24() V25() V26() V27() V28() V29() set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
x is V1() V4( NAT ) V5( QC-variables A) Function-like FinSequence-like FinSequence of QC-variables A
len x is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
p is non empty Element of bool (QC-variables A)
{ (x . b1) where b1 is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT : ( 1 <= b1 & b1 <= len x & x . b1 in p ) } is set
bool p is non empty set
x is set
a1 is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
x . a1 is set
A is V1() non empty QC-alphabet
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
x is V1() V4( NAT ) V5( QC-variables A) Function-like FinSequence-like FinSequence of QC-variables A
still_not-bound_in x is Element of bool (bound_QC-variables A)
bound_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is non empty set
{4} is V24() V25() V26() V27() V28() V29() set
[:{4},(QC-symbols A):] is set
bool (bound_QC-variables A) is non empty set
len x is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
{ (x . b1) where b1 is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT : ( 1 <= b1 & b1 <= len x & x . b1 in bound_QC-variables A ) } is set
(A,x,(bound_QC-variables A)) is Element of bool (bound_QC-variables A)
A is V1() non empty QC-alphabet
QC-WFF A is non empty set
bound_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
{4} is V24() V25() V26() V27() V28() V29() set
[:{4},(QC-symbols A):] is set
bool (bound_QC-variables A) is non empty set
[:(QC-WFF A),(bool (bound_QC-variables A)):] is non empty set
bool [:(QC-WFF A),(bool (bound_QC-variables A)):] is non empty set
VERUM A is Element of QC-WFF A
K98() is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
[K98(),K98()] is set
{K98(),K98()} is V24() V25() V26() V27() V28() V29() set
{K98()} is V24() V25() V26() V27() V28() V29() set
{{K98(),K98()},{K98()}} is set
<*[K98(),K98()]*> is V1() Function-like set
{} (bound_QC-variables A) is empty proper V24() V25() V26() V27() V28() V29() V30() V31() V32() V33() V35() V36() V37() Element of bool (bound_QC-variables A)
x is Element of QC-WFF A
still_not-bound_in x is Element of bool (bound_QC-variables A)
p is Element of bool (bound_QC-variables A)
V is V1() V4( QC-WFF A) V5( bool (bound_QC-variables A)) Function-like V18( QC-WFF A, bool (bound_QC-variables A)) Element of bool [:(QC-WFF A),(bool (bound_QC-variables A)):]
V . x is Element of bool (bound_QC-variables A)
V . (VERUM A) is Element of bool (bound_QC-variables A)
x is Element of QC-WFF A
V . x is Element of bool (bound_QC-variables A)
the_arguments_of x is V1() V4( NAT ) V5( QC-variables A) Function-like FinSequence-like FinSequence of QC-variables A
still_not-bound_in (the_arguments_of x) is Element of bool (bound_QC-variables A)
len (the_arguments_of x) is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
{ ((the_arguments_of x) . b1) where b1 is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT : ( 1 <= b1 & b1 <= len (the_arguments_of x) & (the_arguments_of x) . b1 in bound_QC-variables A ) } is set
the_argument_of x is Element of QC-WFF A
V . (the_argument_of x) is Element of bool (bound_QC-variables A)
the_left_argument_of x is Element of QC-WFF A
V . (the_left_argument_of x) is Element of bool (bound_QC-variables A)
the_right_argument_of x is Element of QC-WFF A
V . (the_right_argument_of x) is Element of bool (bound_QC-variables A)
the_scope_of x is Element of QC-WFF A
V . (the_scope_of x) is Element of bool (bound_QC-variables A)
bound_in x is Element of bound_QC-variables A
{(bound_in x)} is set
a1 is Element of bool (bound_QC-variables A)
a2 is Element of bool (bound_QC-variables A)
a1 \/ a2 is Element of bool (bound_QC-variables A)
a1 \ {(bound_in x)} is Element of bool (bound_QC-variables A)
V is V1() V4( QC-WFF A) V5( bool (bound_QC-variables A)) Function-like V18( QC-WFF A, bool (bound_QC-variables A)) Element of bool [:(QC-WFF A),(bool (bound_QC-variables A)):]
V . x is Element of bool (bound_QC-variables A)
V . (VERUM A) is Element of bool (bound_QC-variables A)
x is Element of QC-WFF A
V . x is Element of bool (bound_QC-variables A)
the_arguments_of x is V1() V4( NAT ) V5( QC-variables A) Function-like FinSequence-like FinSequence of QC-variables A
len (the_arguments_of x) is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
{ ((the_arguments_of x) . b1) where b1 is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT : ( 1 <= b1 & b1 <= len (the_arguments_of x) & (the_arguments_of x) . b1 in bound_QC-variables A ) } is set
still_not-bound_in (the_arguments_of x) is Element of bool (bound_QC-variables A)
the_argument_of x is Element of QC-WFF A
V . (the_argument_of x) is Element of bool (bound_QC-variables A)
the_left_argument_of x is Element of QC-WFF A
V . (the_left_argument_of x) is Element of bool (bound_QC-variables A)
the_right_argument_of x is Element of QC-WFF A
V . (the_right_argument_of x) is Element of bool (bound_QC-variables A)
(V . (the_left_argument_of x)) \/ (V . (the_right_argument_of x)) is Element of bool (bound_QC-variables A)
the_scope_of x is Element of QC-WFF A
V . (the_scope_of x) is Element of bool (bound_QC-variables A)
bound_in x is Element of bound_QC-variables A
{(bound_in x)} is set
(V . (the_scope_of x)) \ {(bound_in x)} is Element of bool (bound_QC-variables A)
A is V1() non empty QC-alphabet
VERUM A is Element of QC-WFF A
QC-WFF A is non empty set
still_not-bound_in (VERUM A) is Element of bool (bound_QC-variables A)
bound_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
[:{4},(QC-symbols A):] is set
bool (bound_QC-variables A) is non empty set
[:(QC-WFF A),(bool (bound_QC-variables A)):] is non empty set
bool [:(QC-WFF A),(bool (bound_QC-variables A)):] is non empty set
{} (bound_QC-variables A) is empty proper V24() V25() V26() V27() V28() V29() V30() V31() V32() V33() V35() V36() V37() Element of bool (bound_QC-variables A)
p is Element of bool (bound_QC-variables A)
x is Element of QC-WFF A
still_not-bound_in x is Element of bool (bound_QC-variables A)
x is Element of bool (bound_QC-variables A)
a1 is V1() V4( QC-WFF A) V5( bool (bound_QC-variables A)) Function-like V18( QC-WFF A, bool (bound_QC-variables A)) Element of bool [:(QC-WFF A),(bool (bound_QC-variables A)):]
V is Element of QC-WFF A
a1 . V is Element of bool (bound_QC-variables A)
still_not-bound_in V is Element of bool (bound_QC-variables A)
A is V1() non empty QC-alphabet
QC-WFF A is non empty set
bound_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
[:{4},(QC-symbols A):] is set
bool (bound_QC-variables A) is non empty set
[:(QC-WFF A),(bool (bound_QC-variables A)):] is non empty set
bool [:(QC-WFF A),(bool (bound_QC-variables A)):] is non empty set
VERUM A is Element of QC-WFF A
{} (bound_QC-variables A) is empty proper V24() V25() V26() V27() V28() V29() V30() V31() V32() V33() V35() V36() V37() Element of bool (bound_QC-variables A)
p is Element of bool (bound_QC-variables A)
x is Element of QC-WFF A
still_not-bound_in x is Element of bool (bound_QC-variables A)
x is Element of bool (bound_QC-variables A)
a1 is V1() V4( QC-WFF A) V5( bool (bound_QC-variables A)) Function-like V18( QC-WFF A, bool (bound_QC-variables A)) Element of bool [:(QC-WFF A),(bool (bound_QC-variables A)):]
V is Element of QC-WFF A
a1 . V is Element of bool (bound_QC-variables A)
still_not-bound_in V is Element of bool (bound_QC-variables A)
x is Element of QC-WFF A
still_not-bound_in x is Element of bool (bound_QC-variables A)
the_arguments_of x is V1() V4( NAT ) V5( QC-variables A) Function-like FinSequence-like FinSequence of QC-variables A
still_not-bound_in (the_arguments_of x) is Element of bool (bound_QC-variables A)
len (the_arguments_of x) is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
{ ((the_arguments_of x) . b1) where b1 is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT : ( 1 <= b1 & b1 <= len (the_arguments_of x) & (the_arguments_of x) . b1 in bound_QC-variables A ) } is set
A is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
x is V1() non empty QC-alphabet
QC-pred_symbols x is non empty set
QC-symbols x is non empty set
K49(x) is set
7 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
{ [b1,b2] where b1 is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT , b2 is Element of QC-symbols x : 7 <= b1 } is set
A -ary_QC-pred_symbols x is non empty Element of bool (QC-pred_symbols x)
bool (QC-pred_symbols x) is non empty set
{ b1 where b1 is Element of QC-pred_symbols x : the_arity_of b1 = A } is set
QC-variables x is non empty set
[:{4,5},(QC-symbols x):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols x):] is set
p is Element of A -ary_QC-pred_symbols x
V is V1() V4( NAT ) V5( QC-variables x) Function-like V45(A) FinSequence-like FinSequence of QC-variables x
p ! V is Element of QC-WFF x
QC-WFF x is non empty set
still_not-bound_in (p ! V) is Element of bool (bound_QC-variables x)
bound_QC-variables x is non empty Element of bool (QC-variables x)
bool (QC-variables x) is non empty set
[:{4},(QC-symbols x):] is set
bool (bound_QC-variables x) is non empty set
still_not-bound_in V is Element of bool (bound_QC-variables x)
len V is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
{ (V . b1) where b1 is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT : ( 1 <= b1 & b1 <= len V & V . b1 in bound_QC-variables x ) } is set
the_arguments_of (p ! V) is V1() V4( NAT ) V5( QC-variables x) Function-like FinSequence-like FinSequence of QC-variables x
A is V1() non empty QC-alphabet
QC-WFF A is non empty set
bound_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
[:{4},(QC-symbols A):] is set
bool (bound_QC-variables A) is non empty set
[:(QC-WFF A),(bool (bound_QC-variables A)):] is non empty set
bool [:(QC-WFF A),(bool (bound_QC-variables A)):] is non empty set
VERUM A is Element of QC-WFF A
{} (bound_QC-variables A) is empty proper V24() V25() V26() V27() V28() V29() V30() V31() V32() V33() V35() V36() V37() Element of bool (bound_QC-variables A)
p is Element of bool (bound_QC-variables A)
x is Element of QC-WFF A
still_not-bound_in x is Element of bool (bound_QC-variables A)
x is Element of bool (bound_QC-variables A)
a1 is V1() V4( QC-WFF A) V5( bool (bound_QC-variables A)) Function-like V18( QC-WFF A, bool (bound_QC-variables A)) Element of bool [:(QC-WFF A),(bool (bound_QC-variables A)):]
V is Element of QC-WFF A
a1 . V is Element of bool (bound_QC-variables A)
still_not-bound_in V is Element of bool (bound_QC-variables A)
x is Element of QC-WFF A
still_not-bound_in x is Element of bool (bound_QC-variables A)
the_argument_of x is Element of QC-WFF A
still_not-bound_in (the_argument_of x) is Element of bool (bound_QC-variables A)
A is V1() non empty QC-alphabet
QC-WFF A is non empty set
x is Element of QC-WFF A
'not' x is Element of QC-WFF A
[1,K98()] is set
{1,K98()} is V24() V25() V26() V27() V28() V29() set
{1} is V24() V25() V26() V27() V28() V29() set
{{1,K98()},{1}} is set
<*[1,K98()]*> is V1() Function-like set
@ x is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
QC-symbols A is non empty set
K49(A) is set
[:NAT,(QC-symbols A):] is non empty set
K113(<*[1,K98()]*>,(@ x)) is V1() Function-like FinSequence-like set
still_not-bound_in ('not' x) is Element of bool (bound_QC-variables A)
bound_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
[:{4},(QC-symbols A):] is set
bool (bound_QC-variables A) is non empty set
still_not-bound_in x is Element of bool (bound_QC-variables A)
the_argument_of ('not' x) is Element of QC-WFF A
A is V1() non empty QC-alphabet
FALSUM A is Element of QC-WFF A
QC-WFF A is non empty set
still_not-bound_in (FALSUM A) is Element of bool (bound_QC-variables A)
bound_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
[:{4},(QC-symbols A):] is set
bool (bound_QC-variables A) is non empty set
VERUM A is Element of QC-WFF A
'not' (VERUM A) is Element of QC-WFF A
[1,K98()] is set
{1,K98()} is V24() V25() V26() V27() V28() V29() set
{1} is V24() V25() V26() V27() V28() V29() set
{{1,K98()},{1}} is set
<*[1,K98()]*> is V1() Function-like set
@ (VERUM A) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
[:NAT,(QC-symbols A):] is non empty set
K113(<*[1,K98()]*>,(@ (VERUM A))) is V1() Function-like FinSequence-like set
still_not-bound_in ('not' (VERUM A)) is Element of bool (bound_QC-variables A)
still_not-bound_in (VERUM A) is Element of bool (bound_QC-variables A)
A is V1() non empty QC-alphabet
QC-WFF A is non empty set
bound_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
[:{4},(QC-symbols A):] is set
bool (bound_QC-variables A) is non empty set
[:(QC-WFF A),(bool (bound_QC-variables A)):] is non empty set
bool [:(QC-WFF A),(bool (bound_QC-variables A)):] is non empty set
VERUM A is Element of QC-WFF A
{} (bound_QC-variables A) is empty proper V24() V25() V26() V27() V28() V29() V30() V31() V32() V33() V35() V36() V37() Element of bool (bound_QC-variables A)
p is Element of bool (bound_QC-variables A)
x is Element of QC-WFF A
still_not-bound_in x is Element of bool (bound_QC-variables A)
x is Element of bool (bound_QC-variables A)
a1 is V1() V4( QC-WFF A) V5( bool (bound_QC-variables A)) Function-like V18( QC-WFF A, bool (bound_QC-variables A)) Element of bool [:(QC-WFF A),(bool (bound_QC-variables A)):]
V is Element of QC-WFF A
a1 . V is Element of bool (bound_QC-variables A)
still_not-bound_in V is Element of bool (bound_QC-variables A)
x is Element of QC-WFF A
still_not-bound_in x is Element of bool (bound_QC-variables A)
the_left_argument_of x is Element of QC-WFF A
still_not-bound_in (the_left_argument_of x) is Element of bool (bound_QC-variables A)
the_right_argument_of x is Element of QC-WFF A
still_not-bound_in (the_right_argument_of x) is Element of bool (bound_QC-variables A)
(still_not-bound_in (the_left_argument_of x)) \/ (still_not-bound_in (the_right_argument_of x)) is Element of bool (bound_QC-variables A)
A is V1() non empty QC-alphabet
QC-WFF A is non empty set
bound_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
[:{4},(QC-symbols A):] is set
x is Element of QC-WFF A
p is Element of QC-WFF A
x '&' p is Element of QC-WFF A
2 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
[2,K98()] is set
{2,K98()} is V24() V25() V26() V27() V28() V29() set
{2} is V24() V25() V26() V27() V28() V29() set
{{2,K98()},{2}} is set
<*[2,K98()]*> is V1() Function-like set
@ x is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
[:NAT,(QC-symbols A):] is non empty set
K113(<*[2,K98()]*>,(@ x)) is V1() Function-like FinSequence-like set
@ p is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(K113(<*[2,K98()]*>,(@ x)),(@ p)) is V1() Function-like FinSequence-like set
still_not-bound_in (x '&' p) is Element of bool (bound_QC-variables A)
bool (bound_QC-variables A) is non empty set
still_not-bound_in x is Element of bool (bound_QC-variables A)
still_not-bound_in p is Element of bool (bound_QC-variables A)
(still_not-bound_in x) \/ (still_not-bound_in p) is Element of bool (bound_QC-variables A)
the_left_argument_of (x '&' p) is Element of QC-WFF A
the_right_argument_of (x '&' p) is Element of QC-WFF A
A is V1() non empty QC-alphabet
QC-WFF A is non empty set
bound_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
[:{4},(QC-symbols A):] is set
bool (bound_QC-variables A) is non empty set
[:(QC-WFF A),(bool (bound_QC-variables A)):] is non empty set
bool [:(QC-WFF A),(bool (bound_QC-variables A)):] is non empty set
VERUM A is Element of QC-WFF A
{} (bound_QC-variables A) is empty proper V24() V25() V26() V27() V28() V29() V30() V31() V32() V33() V35() V36() V37() Element of bool (bound_QC-variables A)
p is Element of bool (bound_QC-variables A)
x is Element of QC-WFF A
still_not-bound_in x is Element of bool (bound_QC-variables A)
x is Element of bool (bound_QC-variables A)
a1 is V1() V4( QC-WFF A) V5( bool (bound_QC-variables A)) Function-like V18( QC-WFF A, bool (bound_QC-variables A)) Element of bool [:(QC-WFF A),(bool (bound_QC-variables A)):]
V is Element of QC-WFF A
a1 . V is Element of bool (bound_QC-variables A)
still_not-bound_in V is Element of bool (bound_QC-variables A)
x is Element of QC-WFF A
still_not-bound_in x is Element of bool (bound_QC-variables A)
the_scope_of x is Element of QC-WFF A
still_not-bound_in (the_scope_of x) is Element of bool (bound_QC-variables A)
bound_in x is Element of bound_QC-variables A
{(bound_in x)} is set
(still_not-bound_in (the_scope_of x)) \ {(bound_in x)} is Element of bool (bound_QC-variables A)
H1( the_scope_of x) \ {(bound_in x)} is Element of bool (bound_QC-variables A)
A is V1() non empty QC-alphabet
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bound_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is non empty set
[:{4},(QC-symbols A):] is set
QC-WFF A is non empty set
x is Element of bound_QC-variables A
{x} is set
p is Element of QC-WFF A
All (x,p) is Element of QC-WFF A
3 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
[3,K98()] is set
{3,K98()} is V24() V25() V26() V27() V28() V29() set
{3} is V24() V25() V26() V27() V28() V29() set
{{3,K98()},{3}} is set
<*[3,K98()]*> is V1() Function-like set
<*x*> is V1() V4( NAT ) V5( bound_QC-variables A) Function-like FinSequence-like FinSequence of bound_QC-variables A
K113(<*[3,K98()]*>,<*x*>) is V1() Function-like FinSequence-like set
@ p is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
[:NAT,(QC-symbols A):] is non empty set
K113(K113(<*[3,K98()]*>,<*x*>),(@ p)) is V1() Function-like FinSequence-like set
still_not-bound_in (All (x,p)) is Element of bool (bound_QC-variables A)
bool (bound_QC-variables A) is non empty set
still_not-bound_in p is Element of bool (bound_QC-variables A)
(still_not-bound_in p) \ {x} is Element of bool (bound_QC-variables A)
the_scope_of (All (x,p)) is Element of QC-WFF A
bound_in (All (x,p)) is Element of bound_QC-variables A
A is V1() non empty QC-alphabet
QC-WFF A is non empty set
bound_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
[:{4},(QC-symbols A):] is set
x is Element of QC-WFF A
still_not-bound_in x is Element of bool (bound_QC-variables A)
bool (bound_QC-variables A) is non empty set
the_left_disjunct_of x is Element of QC-WFF A
still_not-bound_in (the_left_disjunct_of x) is Element of bool (bound_QC-variables A)
the_right_disjunct_of x is Element of QC-WFF A
still_not-bound_in (the_right_disjunct_of x) is Element of bool (bound_QC-variables A)
(still_not-bound_in (the_left_disjunct_of x)) \/ (still_not-bound_in (the_right_disjunct_of x)) is Element of bool (bound_QC-variables A)
(the_left_disjunct_of x) 'or' (the_right_disjunct_of x) is Element of QC-WFF A
'not' (the_left_disjunct_of x) is Element of QC-WFF A
[1,K98()] is set
{1,K98()} is V24() V25() V26() V27() V28() V29() set
{1} is V24() V25() V26() V27() V28() V29() set
{{1,K98()},{1}} is set
<*[1,K98()]*> is V1() Function-like set
@ (the_left_disjunct_of x) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
[:NAT,(QC-symbols A):] is non empty set
K113(<*[1,K98()]*>,(@ (the_left_disjunct_of x))) is V1() Function-like FinSequence-like set
'not' (the_right_disjunct_of x) is Element of QC-WFF A
@ (the_right_disjunct_of x) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(<*[1,K98()]*>,(@ (the_right_disjunct_of x))) is V1() Function-like FinSequence-like set
('not' (the_left_disjunct_of x)) '&' ('not' (the_right_disjunct_of x)) is Element of QC-WFF A
2 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
[2,K98()] is set
{2,K98()} is V24() V25() V26() V27() V28() V29() set
{2} is V24() V25() V26() V27() V28() V29() set
{{2,K98()},{2}} is set
<*[2,K98()]*> is V1() Function-like set
@ ('not' (the_left_disjunct_of x)) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(<*[2,K98()]*>,(@ ('not' (the_left_disjunct_of x)))) is V1() Function-like FinSequence-like set
@ ('not' (the_right_disjunct_of x)) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(K113(<*[2,K98()]*>,(@ ('not' (the_left_disjunct_of x)))),(@ ('not' (the_right_disjunct_of x)))) is V1() Function-like FinSequence-like set
'not' (('not' (the_left_disjunct_of x)) '&' ('not' (the_right_disjunct_of x))) is Element of QC-WFF A
@ (('not' (the_left_disjunct_of x)) '&' ('not' (the_right_disjunct_of x))) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(<*[1,K98()]*>,(@ (('not' (the_left_disjunct_of x)) '&' ('not' (the_right_disjunct_of x))))) is V1() Function-like FinSequence-like set
still_not-bound_in (('not' (the_left_disjunct_of x)) '&' ('not' (the_right_disjunct_of x))) is Element of bool (bound_QC-variables A)
still_not-bound_in ('not' (the_left_disjunct_of x)) is Element of bool (bound_QC-variables A)
still_not-bound_in ('not' (the_right_disjunct_of x)) is Element of bool (bound_QC-variables A)
(still_not-bound_in ('not' (the_left_disjunct_of x))) \/ (still_not-bound_in ('not' (the_right_disjunct_of x))) is Element of bool (bound_QC-variables A)
(still_not-bound_in (the_left_disjunct_of x)) \/ (still_not-bound_in ('not' (the_right_disjunct_of x))) is Element of bool (bound_QC-variables A)
A is V1() non empty QC-alphabet
QC-WFF A is non empty set
bound_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
[:{4},(QC-symbols A):] is set
x is Element of QC-WFF A
p is Element of QC-WFF A
x 'or' p is Element of QC-WFF A
still_not-bound_in (x 'or' p) is Element of bool (bound_QC-variables A)
bool (bound_QC-variables A) is non empty set
still_not-bound_in x is Element of bool (bound_QC-variables A)
still_not-bound_in p is Element of bool (bound_QC-variables A)
(still_not-bound_in x) \/ (still_not-bound_in p) is Element of bool (bound_QC-variables A)
the_right_disjunct_of (x 'or' p) is Element of QC-WFF A
the_left_disjunct_of (x 'or' p) is Element of QC-WFF A
A is V1() non empty QC-alphabet
QC-WFF A is non empty set
bound_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
[:{4},(QC-symbols A):] is set
x is Element of QC-WFF A
still_not-bound_in x is Element of bool (bound_QC-variables A)
bool (bound_QC-variables A) is non empty set
the_antecedent_of x is Element of QC-WFF A
still_not-bound_in (the_antecedent_of x) is Element of bool (bound_QC-variables A)
the_right_disjunct_of x is Element of QC-WFF A
still_not-bound_in (the_right_disjunct_of x) is Element of bool (bound_QC-variables A)
(still_not-bound_in (the_antecedent_of x)) \/ (still_not-bound_in (the_right_disjunct_of x)) is Element of bool (bound_QC-variables A)
(the_antecedent_of x) => (the_right_disjunct_of x) is Element of QC-WFF A
'not' (the_right_disjunct_of x) is Element of QC-WFF A
[1,K98()] is set
{1,K98()} is V24() V25() V26() V27() V28() V29() set
{1} is V24() V25() V26() V27() V28() V29() set
{{1,K98()},{1}} is set
<*[1,K98()]*> is V1() Function-like set
@ (the_right_disjunct_of x) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
[:NAT,(QC-symbols A):] is non empty set
K113(<*[1,K98()]*>,(@ (the_right_disjunct_of x))) is V1() Function-like FinSequence-like set
(the_antecedent_of x) '&' ('not' (the_right_disjunct_of x)) is Element of QC-WFF A
2 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
[2,K98()] is set
{2,K98()} is V24() V25() V26() V27() V28() V29() set
{2} is V24() V25() V26() V27() V28() V29() set
{{2,K98()},{2}} is set
<*[2,K98()]*> is V1() Function-like set
@ (the_antecedent_of x) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(<*[2,K98()]*>,(@ (the_antecedent_of x))) is V1() Function-like FinSequence-like set
@ ('not' (the_right_disjunct_of x)) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(K113(<*[2,K98()]*>,(@ (the_antecedent_of x))),(@ ('not' (the_right_disjunct_of x)))) is V1() Function-like FinSequence-like set
'not' ((the_antecedent_of x) '&' ('not' (the_right_disjunct_of x))) is Element of QC-WFF A
@ ((the_antecedent_of x) '&' ('not' (the_right_disjunct_of x))) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(<*[1,K98()]*>,(@ ((the_antecedent_of x) '&' ('not' (the_right_disjunct_of x))))) is V1() Function-like FinSequence-like set
still_not-bound_in ((the_antecedent_of x) '&' ('not' (the_right_disjunct_of x))) is Element of bool (bound_QC-variables A)
still_not-bound_in ('not' (the_right_disjunct_of x)) is Element of bool (bound_QC-variables A)
(still_not-bound_in (the_antecedent_of x)) \/ (still_not-bound_in ('not' (the_right_disjunct_of x))) is Element of bool (bound_QC-variables A)
A is V1() non empty QC-alphabet
QC-WFF A is non empty set
bound_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
[:{4},(QC-symbols A):] is set
x is Element of QC-WFF A
p is Element of QC-WFF A
x => p is Element of QC-WFF A
still_not-bound_in (x => p) is Element of bool (bound_QC-variables A)
bool (bound_QC-variables A) is non empty set
still_not-bound_in x is Element of bool (bound_QC-variables A)
still_not-bound_in p is Element of bool (bound_QC-variables A)
(still_not-bound_in x) \/ (still_not-bound_in p) is Element of bool (bound_QC-variables A)
the_right_disjunct_of (x => p) is Element of QC-WFF A
the_antecedent_of (x => p) is Element of QC-WFF A
A is V1() non empty QC-alphabet
QC-WFF A is non empty set
bound_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
[:{4},(QC-symbols A):] is set
x is Element of QC-WFF A
still_not-bound_in x is Element of bool (bound_QC-variables A)
bool (bound_QC-variables A) is non empty set
the_left_side_of x is Element of QC-WFF A
still_not-bound_in (the_left_side_of x) is Element of bool (bound_QC-variables A)
the_right_side_of x is Element of QC-WFF A
still_not-bound_in (the_right_side_of x) is Element of bool (bound_QC-variables A)
(still_not-bound_in (the_left_side_of x)) \/ (still_not-bound_in (the_right_side_of x)) is Element of bool (bound_QC-variables A)
(the_left_side_of x) <=> (the_right_side_of x) is Element of QC-WFF A
(the_left_side_of x) => (the_right_side_of x) is Element of QC-WFF A
(the_right_side_of x) => (the_left_side_of x) is Element of QC-WFF A
((the_left_side_of x) => (the_right_side_of x)) '&' ((the_right_side_of x) => (the_left_side_of x)) is Element of QC-WFF A
2 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
[2,K98()] is set
{2,K98()} is V24() V25() V26() V27() V28() V29() set
{2} is V24() V25() V26() V27() V28() V29() set
{{2,K98()},{2}} is set
<*[2,K98()]*> is V1() Function-like set
@ ((the_left_side_of x) => (the_right_side_of x)) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
[:NAT,(QC-symbols A):] is non empty set
K113(<*[2,K98()]*>,(@ ((the_left_side_of x) => (the_right_side_of x)))) is V1() Function-like FinSequence-like set
@ ((the_right_side_of x) => (the_left_side_of x)) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(K113(<*[2,K98()]*>,(@ ((the_left_side_of x) => (the_right_side_of x)))),(@ ((the_right_side_of x) => (the_left_side_of x)))) is V1() Function-like FinSequence-like set
still_not-bound_in ((the_left_side_of x) => (the_right_side_of x)) is Element of bool (bound_QC-variables A)
still_not-bound_in ((the_right_side_of x) => (the_left_side_of x)) is Element of bool (bound_QC-variables A)
(still_not-bound_in ((the_left_side_of x) => (the_right_side_of x))) \/ (still_not-bound_in ((the_right_side_of x) => (the_left_side_of x))) is Element of bool (bound_QC-variables A)
((still_not-bound_in (the_left_side_of x)) \/ (still_not-bound_in (the_right_side_of x))) \/ (still_not-bound_in ((the_right_side_of x) => (the_left_side_of x))) is Element of bool (bound_QC-variables A)
((still_not-bound_in (the_left_side_of x)) \/ (still_not-bound_in (the_right_side_of x))) \/ ((still_not-bound_in (the_left_side_of x)) \/ (still_not-bound_in (the_right_side_of x))) is Element of bool (bound_QC-variables A)
A is V1() non empty QC-alphabet
QC-WFF A is non empty set
bound_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
[:{4},(QC-symbols A):] is set
x is Element of QC-WFF A
p is Element of QC-WFF A
x <=> p is Element of QC-WFF A
still_not-bound_in (x <=> p) is Element of bool (bound_QC-variables A)
bool (bound_QC-variables A) is non empty set
still_not-bound_in x is Element of bool (bound_QC-variables A)
still_not-bound_in p is Element of bool (bound_QC-variables A)
(still_not-bound_in x) \/ (still_not-bound_in p) is Element of bool (bound_QC-variables A)
the_right_side_of (x <=> p) is Element of QC-WFF A
the_left_side_of (x <=> p) is Element of QC-WFF A
A is V1() non empty QC-alphabet
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bound_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is non empty set
[:{4},(QC-symbols A):] is set
QC-WFF A is non empty set
x is Element of bound_QC-variables A
{x} is set
p is Element of QC-WFF A
Ex (x,p) is Element of QC-WFF A
still_not-bound_in (Ex (x,p)) is Element of bool (bound_QC-variables A)
bool (bound_QC-variables A) is non empty set
still_not-bound_in p is Element of bool (bound_QC-variables A)
(still_not-bound_in p) \ {x} is Element of bool (bound_QC-variables A)
'not' p is Element of QC-WFF A
[1,K98()] is set
{1,K98()} is V24() V25() V26() V27() V28() V29() set
{1} is V24() V25() V26() V27() V28() V29() set
{{1,K98()},{1}} is set
<*[1,K98()]*> is V1() Function-like set
@ p is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
[:NAT,(QC-symbols A):] is non empty set
K113(<*[1,K98()]*>,(@ p)) is V1() Function-like FinSequence-like set
All (x,('not' p)) is Element of QC-WFF A
3 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
[3,K98()] is set
{3,K98()} is V24() V25() V26() V27() V28() V29() set
{3} is V24() V25() V26() V27() V28() V29() set
{{3,K98()},{3}} is set
<*[3,K98()]*> is V1() Function-like set
<*x*> is V1() V4( NAT ) V5( bound_QC-variables A) Function-like FinSequence-like FinSequence of bound_QC-variables A
K113(<*[3,K98()]*>,<*x*>) is V1() Function-like FinSequence-like set
@ ('not' p) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(K113(<*[3,K98()]*>,<*x*>),(@ ('not' p))) is V1() Function-like FinSequence-like set
'not' (All (x,('not' p))) is Element of QC-WFF A
@ (All (x,('not' p))) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(<*[1,K98()]*>,(@ (All (x,('not' p))))) is V1() Function-like FinSequence-like set
still_not-bound_in (All (x,('not' p))) is Element of bool (bound_QC-variables A)
still_not-bound_in ('not' p) is Element of bool (bound_QC-variables A)
(still_not-bound_in ('not' p)) \ {x} is Element of bool (bound_QC-variables A)
A is V1() non empty QC-alphabet
VERUM A is Element of QC-WFF A
QC-WFF A is non empty set
FALSUM A is Element of QC-WFF A
still_not-bound_in (VERUM A) is Element of bool (bound_QC-variables A)
bound_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
[:{4},(QC-symbols A):] is set
bool (bound_QC-variables A) is non empty set
still_not-bound_in (FALSUM A) is Element of bool (bound_QC-variables A)
A is V1() non empty QC-alphabet
QC-WFF A is non empty set
x is Element of QC-WFF A
'not' x is Element of QC-WFF A
[1,K98()] is set
{1,K98()} is V24() V25() V26() V27() V28() V29() set
{1} is V24() V25() V26() V27() V28() V29() set
{{1,K98()},{1}} is set
<*[1,K98()]*> is V1() Function-like set
@ x is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
QC-symbols A is non empty set
K49(A) is set
[:NAT,(QC-symbols A):] is non empty set
K113(<*[1,K98()]*>,(@ x)) is V1() Function-like FinSequence-like set
still_not-bound_in x is Element of bool (bound_QC-variables A)
bound_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
[:{4},(QC-symbols A):] is set
bool (bound_QC-variables A) is non empty set
still_not-bound_in ('not' x) is Element of bool (bound_QC-variables A)
still_not-bound_in ('not' x) is Element of bool (bound_QC-variables A)
bound_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
[:{4},(QC-symbols A):] is set
bool (bound_QC-variables A) is non empty set
still_not-bound_in x is Element of bool (bound_QC-variables A)
A is V1() non empty QC-alphabet
QC-WFF A is non empty set
x is Element of QC-WFF A
p is Element of QC-WFF A
x '&' p is Element of QC-WFF A
2 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
[2,K98()] is set
{2,K98()} is V24() V25() V26() V27() V28() V29() set
{2} is V24() V25() V26() V27() V28() V29() set
{{2,K98()},{2}} is set
<*[2,K98()]*> is V1() Function-like set
@ x is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
QC-symbols A is non empty set
K49(A) is set
[:NAT,(QC-symbols A):] is non empty set
K113(<*[2,K98()]*>,(@ x)) is V1() Function-like FinSequence-like set
@ p is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(K113(<*[2,K98()]*>,(@ x)),(@ p)) is V1() Function-like FinSequence-like set
still_not-bound_in x is Element of bool (bound_QC-variables A)
bound_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
[:{4},(QC-symbols A):] is set
bool (bound_QC-variables A) is non empty set
still_not-bound_in p is Element of bool (bound_QC-variables A)
(still_not-bound_in x) \/ (still_not-bound_in p) is Element of bool (bound_QC-variables A)
still_not-bound_in (x '&' p) is Element of bool (bound_QC-variables A)
still_not-bound_in (x '&' p) is Element of bool (bound_QC-variables A)
bound_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
[:{4},(QC-symbols A):] is set
bool (bound_QC-variables A) is non empty set
still_not-bound_in x is Element of bool (bound_QC-variables A)
still_not-bound_in p is Element of bool (bound_QC-variables A)
(still_not-bound_in x) \/ (still_not-bound_in p) is Element of bool (bound_QC-variables A)
A is V1() non empty QC-alphabet
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bound_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is non empty set
[:{4},(QC-symbols A):] is set
QC-WFF A is non empty set
x is Element of bound_QC-variables A
{x} is set
p is Element of QC-WFF A
All (x,p) is Element of QC-WFF A
3 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
[3,K98()] is set
{3,K98()} is V24() V25() V26() V27() V28() V29() set
{3} is V24() V25() V26() V27() V28() V29() set
{{3,K98()},{3}} is set
<*[3,K98()]*> is V1() Function-like set
<*x*> is V1() V4( NAT ) V5( bound_QC-variables A) Function-like FinSequence-like FinSequence of bound_QC-variables A
K113(<*[3,K98()]*>,<*x*>) is V1() Function-like FinSequence-like set
@ p is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
[:NAT,(QC-symbols A):] is non empty set
K113(K113(<*[3,K98()]*>,<*x*>),(@ p)) is V1() Function-like FinSequence-like set
still_not-bound_in p is Element of bool (bound_QC-variables A)
bool (bound_QC-variables A) is non empty set
still_not-bound_in (All (x,p)) is Element of bool (bound_QC-variables A)
(still_not-bound_in p) \ {x} is Element of bool (bound_QC-variables A)
(still_not-bound_in p) \ {x} is Element of bool (bound_QC-variables A)
still_not-bound_in (All (x,p)) is Element of bool (bound_QC-variables A)
A is V1() non empty QC-alphabet
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bound_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is non empty set
[:{4},(QC-symbols A):] is set
QC-WFF A is non empty set
x is Element of bound_QC-variables A
p is Element of QC-WFF A
All (x,p) is Element of QC-WFF A
3 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
[3,K98()] is set
{3,K98()} is V24() V25() V26() V27() V28() V29() set
{3} is V24() V25() V26() V27() V28() V29() set
{{3,K98()},{3}} is set
<*[3,K98()]*> is V1() Function-like set
<*x*> is V1() V4( NAT ) V5( bound_QC-variables A) Function-like FinSequence-like FinSequence of bound_QC-variables A
K113(<*[3,K98()]*>,<*x*>) is V1() Function-like FinSequence-like set
@ p is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
[:NAT,(QC-symbols A):] is non empty set
K113(K113(<*[3,K98()]*>,<*x*>),(@ p)) is V1() Function-like FinSequence-like set
still_not-bound_in p is Element of bool (bound_QC-variables A)
bool (bound_QC-variables A) is non empty set
{x} is set
A is V1() non empty QC-alphabet
QC-WFF A is non empty set
x is Element of QC-WFF A
p is Element of QC-WFF A
x 'or' p is Element of QC-WFF A
'not' x is Element of QC-WFF A
[1,K98()] is set
{1,K98()} is V24() V25() V26() V27() V28() V29() set
{1} is V24() V25() V26() V27() V28() V29() set
{{1,K98()},{1}} is set
<*[1,K98()]*> is V1() Function-like set
@ x is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
QC-symbols A is non empty set
K49(A) is set
[:NAT,(QC-symbols A):] is non empty set
K113(<*[1,K98()]*>,(@ x)) is V1() Function-like FinSequence-like set
'not' p is Element of QC-WFF A
@ p is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(<*[1,K98()]*>,(@ p)) is V1() Function-like FinSequence-like set
('not' x) '&' ('not' p) is Element of QC-WFF A
2 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
[2,K98()] is set
{2,K98()} is V24() V25() V26() V27() V28() V29() set
{2} is V24() V25() V26() V27() V28() V29() set
{{2,K98()},{2}} is set
<*[2,K98()]*> is V1() Function-like set
@ ('not' x) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(<*[2,K98()]*>,(@ ('not' x))) is V1() Function-like FinSequence-like set
@ ('not' p) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(K113(<*[2,K98()]*>,(@ ('not' x))),(@ ('not' p))) is V1() Function-like FinSequence-like set
'not' (('not' x) '&' ('not' p)) is Element of QC-WFF A
@ (('not' x) '&' ('not' p)) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(<*[1,K98()]*>,(@ (('not' x) '&' ('not' p)))) is V1() Function-like FinSequence-like set
A is V1() non empty QC-alphabet
QC-WFF A is non empty set
x is Element of QC-WFF A
p is Element of QC-WFF A
x => p is Element of QC-WFF A
'not' p is Element of QC-WFF A
[1,K98()] is set
{1,K98()} is V24() V25() V26() V27() V28() V29() set
{1} is V24() V25() V26() V27() V28() V29() set
{{1,K98()},{1}} is set
<*[1,K98()]*> is V1() Function-like set
@ p is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
QC-symbols A is non empty set
K49(A) is set
[:NAT,(QC-symbols A):] is non empty set
K113(<*[1,K98()]*>,(@ p)) is V1() Function-like FinSequence-like set
x '&' ('not' p) is Element of QC-WFF A
2 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
[2,K98()] is set
{2,K98()} is V24() V25() V26() V27() V28() V29() set
{2} is V24() V25() V26() V27() V28() V29() set
{{2,K98()},{2}} is set
<*[2,K98()]*> is V1() Function-like set
@ x is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(<*[2,K98()]*>,(@ x)) is V1() Function-like FinSequence-like set
@ ('not' p) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(K113(<*[2,K98()]*>,(@ x)),(@ ('not' p))) is V1() Function-like FinSequence-like set
'not' (x '&' ('not' p)) is Element of QC-WFF A
@ (x '&' ('not' p)) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(<*[1,K98()]*>,(@ (x '&' ('not' p)))) is V1() Function-like FinSequence-like set
A is V1() non empty QC-alphabet
QC-WFF A is non empty set
x is Element of QC-WFF A
p is Element of QC-WFF A
x <=> p is Element of QC-WFF A
x => p is Element of QC-WFF A
p => x is Element of QC-WFF A
(x => p) '&' (p => x) is Element of QC-WFF A
2 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
[2,K98()] is set
{2,K98()} is V24() V25() V26() V27() V28() V29() set
{2} is V24() V25() V26() V27() V28() V29() set
{{2,K98()},{2}} is set
<*[2,K98()]*> is V1() Function-like set
@ (x => p) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
QC-symbols A is non empty set
K49(A) is set
[:NAT,(QC-symbols A):] is non empty set
K113(<*[2,K98()]*>,(@ (x => p))) is V1() Function-like FinSequence-like set
@ (p => x) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(K113(<*[2,K98()]*>,(@ (x => p))),(@ (p => x))) is V1() Function-like FinSequence-like set
A is V1() non empty QC-alphabet
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bound_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is non empty set
[:{4},(QC-symbols A):] is set
QC-WFF A is non empty set
x is Element of bound_QC-variables A
{x} is set
p is Element of QC-WFF A
Ex (x,p) is Element of QC-WFF A
still_not-bound_in p is Element of bool (bound_QC-variables A)
bool (bound_QC-variables A) is non empty set
still_not-bound_in (Ex (x,p)) is Element of bool (bound_QC-variables A)
(still_not-bound_in p) \ {x} is Element of bool (bound_QC-variables A)
(still_not-bound_in p) \ {x} is Element of bool (bound_QC-variables A)
still_not-bound_in (Ex (x,p)) is Element of bool (bound_QC-variables A)
A is V1() non empty QC-alphabet
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bound_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is non empty set
[:{4},(QC-symbols A):] is set
QC-WFF A is non empty set
x is Element of bound_QC-variables A
p is Element of QC-WFF A
Ex (x,p) is Element of QC-WFF A
still_not-bound_in p is Element of bool (bound_QC-variables A)
bool (bound_QC-variables A) is non empty set
{x} is set
A is V1() non empty QC-alphabet
QC-symbols A is non empty set
K49(A) is set
x is Element of QC-symbols A
[4,x] is set
{4,x} is set
{{4,x},{4}} is set
QC-variables A is non empty set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bound_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is non empty set
[:{4},(QC-symbols A):] is set
A is V1() non empty QC-alphabet
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bound_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is non empty set
[:{4},(QC-symbols A):] is set
x is Element of bound_QC-variables A
p is set
V is set
[p,V] is set
{p,V} is set
{p} is set
{{p,V},{p}} is set
x is Element of QC-symbols A
(A,x) is Element of bound_QC-variables A
[4,x] is set
{4,x} is set
{{4,x},{4}} is set
x is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
[6,x] is set
{6,x} is V24() V25() V26() V27() V28() V29() set
{{6,x},{6}} is set
A is V1() non empty QC-alphabet
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
free_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is non empty set
A is V1() non empty QC-alphabet
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
free_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is non empty set
x is Element of free_QC-variables A
p is set
V is set
[p,V] is set
{p,V} is set
{p} is set
{{p,V},{p}} is set
x is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
(A,x) is Element of free_QC-variables A
[6,x] is set
{6,x} is V24() V25() V26() V27() V28() V29() set
{{6,x},{6}} is set
A is V1() non empty QC-alphabet
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
fixed_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is non empty set
{5} is V24() V25() V26() V27() V28() V29() set
[:{5},(QC-symbols A):] is set
free_QC-variables A is non empty Element of bool (QC-variables A)
x is Element of fixed_QC-variables A
p is Element of free_QC-variables A
V is set
x is set
[V,x] is set
{V,x} is set
{V} is set
{{V,x},{V}} is set
a1 is set
a2 is set
[a1,a2] is set
{a1,a2} is set
{a1} is set
{{a1,a2},{a1}} is set
A is V1() non empty QC-alphabet
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
fixed_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is non empty set
{5} is V24() V25() V26() V27() V28() V29() set
[:{5},(QC-symbols A):] is set
bound_QC-variables A is non empty Element of bool (QC-variables A)
[:{4},(QC-symbols A):] is set
x is Element of fixed_QC-variables A
p is Element of bound_QC-variables A
V is set
x is set
[V,x] is set
{V,x} is set
{V} is set
{{V,x},{V}} is set
a1 is set
a2 is set
[a1,a2] is set
{a1,a2} is set
{a1} is set
{{a1,a2},{a1}} is set
A is V1() non empty QC-alphabet
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
free_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is non empty set
bound_QC-variables A is non empty Element of bool (QC-variables A)
[:{4},(QC-symbols A):] is set
x is Element of free_QC-variables A
p is Element of bound_QC-variables A
V is set
x is set
[V,x] is set
{V,x} is set
{V} is set
{{V,x},{V}} is set
a1 is set
a2 is set
[a1,a2] is set
{a1,a2} is set
{a1} is set
{{a1,a2},{a1}} is set
A is V1() non empty QC-alphabet
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
QC-WFF A is non empty set
x is non empty Element of bool (QC-variables A)
bool x is non empty set
[:(QC-WFF A),(bool x):] is non empty set
bool [:(QC-WFF A),(bool x):] is non empty set
p is Element of QC-WFF A
VERUM A is Element of QC-WFF A
{} x is empty proper V24() V25() V26() V27() V28() V29() V30() V31() V32() V33() V35() V36() V37() Element of bool x
A is V1() non empty QC-alphabet
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
QC-WFF A is non empty set
x is non empty Element of bool (QC-variables A)
bool x is non empty set
[:(QC-WFF A),(bool x):] is non empty set
bool [:(QC-WFF A),(bool x):] is non empty set
VERUM A is Element of QC-WFF A
{} x is empty proper V24() V25() V26() V27() V28() V29() V30() V31() V32() V33() V35() V36() V37() Element of bool x
V is Element of bool x
p is Element of QC-WFF A
(A,x,p) is Element of bool x
a1 is Element of bool x
a2 is V1() V4( QC-WFF A) V5( bool x) Function-like V18( QC-WFF A, bool x) Element of bool [:(QC-WFF A),(bool x):]
x is Element of QC-WFF A
a2 . x is Element of bool x
(A,x,x) is Element of bool x
(A,x,(VERUM A)) is Element of bool x
p is Element of QC-WFF A
(A,x,p) is Element of bool x
the_arguments_of p is V1() V4( NAT ) V5( QC-variables A) Function-like FinSequence-like FinSequence of QC-variables A
(A,(the_arguments_of p),x) is Element of bool x
len (the_arguments_of p) is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
{ ((the_arguments_of p) . b1) where b1 is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT : ( 1 <= b1 & b1 <= len (the_arguments_of p) & (the_arguments_of p) . b1 in x ) } is set
p is Element of QC-WFF A
(A,x,p) is Element of bool x
the_argument_of p is Element of QC-WFF A
(A,x,(the_argument_of p)) is Element of bool x
p is Element of QC-WFF A
(A,x,p) is Element of bool x
the_left_argument_of p is Element of QC-WFF A
(A,x,(the_left_argument_of p)) is Element of bool x
the_right_argument_of p is Element of QC-WFF A
(A,x,(the_right_argument_of p)) is Element of bool x
(A,x,(the_left_argument_of p)) \/ (A,x,(the_right_argument_of p)) is Element of bool x
p is Element of QC-WFF A
(A,x,p) is Element of bool x
the_scope_of p is Element of QC-WFF A
(A,x,(the_scope_of p)) is Element of bool x
A is V1() non empty QC-alphabet
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
x is non empty Element of bool (QC-variables A)
VERUM A is Element of QC-WFF A
QC-WFF A is non empty set
(A,x,(VERUM A)) is Element of bool x
bool x is non empty set
A is V1() non empty QC-alphabet
QC-WFF A is non empty set
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
x is Element of QC-WFF A
the_arguments_of x is V1() V4( NAT ) V5( QC-variables A) Function-like FinSequence-like FinSequence of QC-variables A
len (the_arguments_of x) is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
p is non empty Element of bool (QC-variables A)
(A,p,x) is Element of bool p
bool p is non empty set
(A,(the_arguments_of x),p) is Element of bool p
{ ((the_arguments_of x) . b1) where b1 is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT : ( 1 <= b1 & b1 <= len (the_arguments_of x) & (the_arguments_of x) . b1 in p ) } is set
A is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
x is V1() non empty QC-alphabet
QC-variables x is non empty set
QC-symbols x is non empty set
K49(x) is set
[:{4,5},(QC-symbols x):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols x):] is set
bool (QC-variables x) is non empty set
QC-pred_symbols x is non empty set
7 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
{ [b1,b2] where b1 is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT , b2 is Element of QC-symbols x : 7 <= b1 } is set
A -ary_QC-pred_symbols x is non empty Element of bool (QC-pred_symbols x)
bool (QC-pred_symbols x) is non empty set
{ b1 where b1 is Element of QC-pred_symbols x : the_arity_of b1 = A } is set
p is non empty Element of bool (QC-variables x)
V is Element of A -ary_QC-pred_symbols x
x is V1() V4( NAT ) V5( QC-variables x) Function-like V45(A) FinSequence-like FinSequence of QC-variables x
V ! x is Element of QC-WFF x
QC-WFF x is non empty set
(x,p,(V ! x)) is Element of bool p
bool p is non empty set
(x,x,p) is Element of bool p
len x is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
{ (x . b1) where b1 is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT : ( 1 <= b1 & b1 <= len x & x . b1 in p ) } is set
the_arguments_of (V ! x) is V1() V4( NAT ) V5( QC-variables x) Function-like FinSequence-like FinSequence of QC-variables x
A is V1() non empty QC-alphabet
QC-WFF A is non empty set
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
x is Element of QC-WFF A
p is non empty Element of bool (QC-variables A)
(A,p,x) is Element of bool p
bool p is non empty set
the_argument_of x is Element of QC-WFF A
(A,p,(the_argument_of x)) is Element of bool p
A is V1() non empty QC-alphabet
QC-WFF A is non empty set
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
x is Element of QC-WFF A
'not' x is Element of QC-WFF A
[1,K98()] is set
{1,K98()} is V24() V25() V26() V27() V28() V29() set
{1} is V24() V25() V26() V27() V28() V29() set
{{1,K98()},{1}} is set
<*[1,K98()]*> is V1() Function-like set
@ x is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
[:NAT,(QC-symbols A):] is non empty set
K113(<*[1,K98()]*>,(@ x)) is V1() Function-like FinSequence-like set
p is non empty Element of bool (QC-variables A)
(A,p,('not' x)) is Element of bool p
bool p is non empty set
(A,p,x) is Element of bool p
the_argument_of ('not' x) is Element of QC-WFF A
A is V1() non empty QC-alphabet
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
FALSUM A is Element of QC-WFF A
QC-WFF A is non empty set
x is non empty Element of bool (QC-variables A)
(A,x,(FALSUM A)) is Element of bool x
bool x is non empty set
VERUM A is Element of QC-WFF A
'not' (VERUM A) is Element of QC-WFF A
[1,K98()] is set
{1,K98()} is V24() V25() V26() V27() V28() V29() set
{1} is V24() V25() V26() V27() V28() V29() set
{{1,K98()},{1}} is set
<*[1,K98()]*> is V1() Function-like set
@ (VERUM A) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
[:NAT,(QC-symbols A):] is non empty set
K113(<*[1,K98()]*>,(@ (VERUM A))) is V1() Function-like FinSequence-like set
(A,x,(VERUM A)) is Element of bool x
A is V1() non empty QC-alphabet
QC-WFF A is non empty set
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
x is Element of QC-WFF A
p is non empty Element of bool (QC-variables A)
(A,p,x) is Element of bool p
bool p is non empty set
the_left_argument_of x is Element of QC-WFF A
(A,p,(the_left_argument_of x)) is Element of bool p
the_right_argument_of x is Element of QC-WFF A
(A,p,(the_right_argument_of x)) is Element of bool p
(A,p,(the_left_argument_of x)) \/ (A,p,(the_right_argument_of x)) is Element of bool p
A is V1() non empty QC-alphabet
QC-WFF A is non empty set
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
x is Element of QC-WFF A
p is Element of QC-WFF A
x '&' p is Element of QC-WFF A
2 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
[2,K98()] is set
{2,K98()} is V24() V25() V26() V27() V28() V29() set
{2} is V24() V25() V26() V27() V28() V29() set
{{2,K98()},{2}} is set
<*[2,K98()]*> is V1() Function-like set
@ x is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
[:NAT,(QC-symbols A):] is non empty set
K113(<*[2,K98()]*>,(@ x)) is V1() Function-like FinSequence-like set
@ p is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(K113(<*[2,K98()]*>,(@ x)),(@ p)) is V1() Function-like FinSequence-like set
V is non empty Element of bool (QC-variables A)
(A,V,(x '&' p)) is Element of bool V
bool V is non empty set
(A,V,x) is Element of bool V
(A,V,p) is Element of bool V
(A,V,x) \/ (A,V,p) is Element of bool V
the_left_argument_of (x '&' p) is Element of QC-WFF A
the_right_argument_of (x '&' p) is Element of QC-WFF A
A is V1() non empty QC-alphabet
QC-WFF A is non empty set
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
x is Element of QC-WFF A
p is non empty Element of bool (QC-variables A)
(A,p,x) is Element of bool p
bool p is non empty set
the_scope_of x is Element of QC-WFF A
(A,p,(the_scope_of x)) is Element of bool p
A is V1() non empty QC-alphabet
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bound_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is non empty set
[:{4},(QC-symbols A):] is set
QC-WFF A is non empty set
x is Element of bound_QC-variables A
p is Element of QC-WFF A
All (x,p) is Element of QC-WFF A
3 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
[3,K98()] is set
{3,K98()} is V24() V25() V26() V27() V28() V29() set
{3} is V24() V25() V26() V27() V28() V29() set
{{3,K98()},{3}} is set
<*[3,K98()]*> is V1() Function-like set
<*x*> is V1() V4( NAT ) V5( bound_QC-variables A) Function-like FinSequence-like FinSequence of bound_QC-variables A
K113(<*[3,K98()]*>,<*x*>) is V1() Function-like FinSequence-like set
@ p is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
[:NAT,(QC-symbols A):] is non empty set
K113(K113(<*[3,K98()]*>,<*x*>),(@ p)) is V1() Function-like FinSequence-like set
V is non empty Element of bool (QC-variables A)
(A,V,(All (x,p))) is Element of bool V
bool V is non empty set
(A,V,p) is Element of bool V
the_scope_of (All (x,p)) is Element of QC-WFF A
A is V1() non empty QC-alphabet
QC-WFF A is non empty set
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
x is Element of QC-WFF A
the_left_disjunct_of x is Element of QC-WFF A
the_right_disjunct_of x is Element of QC-WFF A
p is non empty Element of bool (QC-variables A)
(A,p,x) is Element of bool p
bool p is non empty set
(A,p,(the_left_disjunct_of x)) is Element of bool p
(A,p,(the_right_disjunct_of x)) is Element of bool p
(A,p,(the_left_disjunct_of x)) \/ (A,p,(the_right_disjunct_of x)) is Element of bool p
(the_left_disjunct_of x) 'or' (the_right_disjunct_of x) is Element of QC-WFF A
'not' (the_left_disjunct_of x) is Element of QC-WFF A
[1,K98()] is set
{1,K98()} is V24() V25() V26() V27() V28() V29() set
{1} is V24() V25() V26() V27() V28() V29() set
{{1,K98()},{1}} is set
<*[1,K98()]*> is V1() Function-like set
@ (the_left_disjunct_of x) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
[:NAT,(QC-symbols A):] is non empty set
K113(<*[1,K98()]*>,(@ (the_left_disjunct_of x))) is V1() Function-like FinSequence-like set
'not' (the_right_disjunct_of x) is Element of QC-WFF A
@ (the_right_disjunct_of x) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(<*[1,K98()]*>,(@ (the_right_disjunct_of x))) is V1() Function-like FinSequence-like set
('not' (the_left_disjunct_of x)) '&' ('not' (the_right_disjunct_of x)) is Element of QC-WFF A
2 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
[2,K98()] is set
{2,K98()} is V24() V25() V26() V27() V28() V29() set
{2} is V24() V25() V26() V27() V28() V29() set
{{2,K98()},{2}} is set
<*[2,K98()]*> is V1() Function-like set
@ ('not' (the_left_disjunct_of x)) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(<*[2,K98()]*>,(@ ('not' (the_left_disjunct_of x)))) is V1() Function-like FinSequence-like set
@ ('not' (the_right_disjunct_of x)) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(K113(<*[2,K98()]*>,(@ ('not' (the_left_disjunct_of x)))),(@ ('not' (the_right_disjunct_of x)))) is V1() Function-like FinSequence-like set
'not' (('not' (the_left_disjunct_of x)) '&' ('not' (the_right_disjunct_of x))) is Element of QC-WFF A
@ (('not' (the_left_disjunct_of x)) '&' ('not' (the_right_disjunct_of x))) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(<*[1,K98()]*>,(@ (('not' (the_left_disjunct_of x)) '&' ('not' (the_right_disjunct_of x))))) is V1() Function-like FinSequence-like set
(A,p,(('not' (the_left_disjunct_of x)) '&' ('not' (the_right_disjunct_of x)))) is Element of bool p
(A,p,('not' (the_left_disjunct_of x))) is Element of bool p
(A,p,('not' (the_right_disjunct_of x))) is Element of bool p
(A,p,('not' (the_left_disjunct_of x))) \/ (A,p,('not' (the_right_disjunct_of x))) is Element of bool p
(A,p,(the_left_disjunct_of x)) \/ (A,p,('not' (the_right_disjunct_of x))) is Element of bool p
A is V1() non empty QC-alphabet
QC-WFF A is non empty set
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
x is Element of QC-WFF A
p is Element of QC-WFF A
x 'or' p is Element of QC-WFF A
V is non empty Element of bool (QC-variables A)
(A,V,(x 'or' p)) is Element of bool V
bool V is non empty set
(A,V,x) is Element of bool V
(A,V,p) is Element of bool V
(A,V,x) \/ (A,V,p) is Element of bool V
the_right_disjunct_of (x 'or' p) is Element of QC-WFF A
the_left_disjunct_of (x 'or' p) is Element of QC-WFF A
A is V1() non empty QC-alphabet
QC-WFF A is non empty set
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
x is Element of QC-WFF A
the_antecedent_of x is Element of QC-WFF A
the_right_disjunct_of x is Element of QC-WFF A
p is non empty Element of bool (QC-variables A)
(A,p,x) is Element of bool p
bool p is non empty set
(A,p,(the_antecedent_of x)) is Element of bool p
(A,p,(the_right_disjunct_of x)) is Element of bool p
(A,p,(the_antecedent_of x)) \/ (A,p,(the_right_disjunct_of x)) is Element of bool p
(the_antecedent_of x) => (the_right_disjunct_of x) is Element of QC-WFF A
'not' (the_right_disjunct_of x) is Element of QC-WFF A
[1,K98()] is set
{1,K98()} is V24() V25() V26() V27() V28() V29() set
{1} is V24() V25() V26() V27() V28() V29() set
{{1,K98()},{1}} is set
<*[1,K98()]*> is V1() Function-like set
@ (the_right_disjunct_of x) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
[:NAT,(QC-symbols A):] is non empty set
K113(<*[1,K98()]*>,(@ (the_right_disjunct_of x))) is V1() Function-like FinSequence-like set
(the_antecedent_of x) '&' ('not' (the_right_disjunct_of x)) is Element of QC-WFF A
2 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
[2,K98()] is set
{2,K98()} is V24() V25() V26() V27() V28() V29() set
{2} is V24() V25() V26() V27() V28() V29() set
{{2,K98()},{2}} is set
<*[2,K98()]*> is V1() Function-like set
@ (the_antecedent_of x) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(<*[2,K98()]*>,(@ (the_antecedent_of x))) is V1() Function-like FinSequence-like set
@ ('not' (the_right_disjunct_of x)) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(K113(<*[2,K98()]*>,(@ (the_antecedent_of x))),(@ ('not' (the_right_disjunct_of x)))) is V1() Function-like FinSequence-like set
'not' ((the_antecedent_of x) '&' ('not' (the_right_disjunct_of x))) is Element of QC-WFF A
@ ((the_antecedent_of x) '&' ('not' (the_right_disjunct_of x))) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(<*[1,K98()]*>,(@ ((the_antecedent_of x) '&' ('not' (the_right_disjunct_of x))))) is V1() Function-like FinSequence-like set
(A,p,((the_antecedent_of x) '&' ('not' (the_right_disjunct_of x)))) is Element of bool p
(A,p,('not' (the_right_disjunct_of x))) is Element of bool p
(A,p,(the_antecedent_of x)) \/ (A,p,('not' (the_right_disjunct_of x))) is Element of bool p
A is V1() non empty QC-alphabet
QC-WFF A is non empty set
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
x is Element of QC-WFF A
p is Element of QC-WFF A
x => p is Element of QC-WFF A
V is non empty Element of bool (QC-variables A)
(A,V,(x => p)) is Element of bool V
bool V is non empty set
(A,V,x) is Element of bool V
(A,V,p) is Element of bool V
(A,V,x) \/ (A,V,p) is Element of bool V
the_right_disjunct_of (x => p) is Element of QC-WFF A
the_antecedent_of (x => p) is Element of QC-WFF A
A is V1() non empty QC-alphabet
QC-WFF A is non empty set
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
x is Element of QC-WFF A
the_left_side_of x is Element of QC-WFF A
the_right_side_of x is Element of QC-WFF A
p is non empty Element of bool (QC-variables A)
(A,p,x) is Element of bool p
bool p is non empty set
(A,p,(the_left_side_of x)) is Element of bool p
(A,p,(the_right_side_of x)) is Element of bool p
(A,p,(the_left_side_of x)) \/ (A,p,(the_right_side_of x)) is Element of bool p
(the_left_side_of x) <=> (the_right_side_of x) is Element of QC-WFF A
(the_left_side_of x) => (the_right_side_of x) is Element of QC-WFF A
(the_right_side_of x) => (the_left_side_of x) is Element of QC-WFF A
((the_left_side_of x) => (the_right_side_of x)) '&' ((the_right_side_of x) => (the_left_side_of x)) is Element of QC-WFF A
2 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
[2,K98()] is set
{2,K98()} is V24() V25() V26() V27() V28() V29() set
{2} is V24() V25() V26() V27() V28() V29() set
{{2,K98()},{2}} is set
<*[2,K98()]*> is V1() Function-like set
@ ((the_left_side_of x) => (the_right_side_of x)) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
[:NAT,(QC-symbols A):] is non empty set
K113(<*[2,K98()]*>,(@ ((the_left_side_of x) => (the_right_side_of x)))) is V1() Function-like FinSequence-like set
@ ((the_right_side_of x) => (the_left_side_of x)) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(K113(<*[2,K98()]*>,(@ ((the_left_side_of x) => (the_right_side_of x)))),(@ ((the_right_side_of x) => (the_left_side_of x)))) is V1() Function-like FinSequence-like set
(A,p,((the_left_side_of x) => (the_right_side_of x))) is Element of bool p
(A,p,((the_right_side_of x) => (the_left_side_of x))) is Element of bool p
(A,p,((the_left_side_of x) => (the_right_side_of x))) \/ (A,p,((the_right_side_of x) => (the_left_side_of x))) is Element of bool p
((A,p,(the_left_side_of x)) \/ (A,p,(the_right_side_of x))) \/ (A,p,((the_right_side_of x) => (the_left_side_of x))) is Element of bool p
((A,p,(the_left_side_of x)) \/ (A,p,(the_right_side_of x))) \/ ((A,p,(the_left_side_of x)) \/ (A,p,(the_right_side_of x))) is Element of bool p
A is V1() non empty QC-alphabet
QC-WFF A is non empty set
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
x is Element of QC-WFF A
p is Element of QC-WFF A
x <=> p is Element of QC-WFF A
V is non empty Element of bool (QC-variables A)
(A,V,(x <=> p)) is Element of bool V
bool V is non empty set
(A,V,x) is Element of bool V
(A,V,p) is Element of bool V
(A,V,x) \/ (A,V,p) is Element of bool V
the_right_side_of (x <=> p) is Element of QC-WFF A
the_left_side_of (x <=> p) is Element of QC-WFF A
A is V1() non empty QC-alphabet
QC-WFF A is non empty set
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
x is Element of QC-WFF A
the_argument_of x is Element of QC-WFF A
the_scope_of (the_argument_of x) is Element of QC-WFF A
the_argument_of (the_scope_of (the_argument_of x)) is Element of QC-WFF A
p is non empty Element of bool (QC-variables A)
(A,p,x) is Element of bool p
bool p is non empty set
(A,p,(the_argument_of (the_scope_of (the_argument_of x)))) is Element of bool p
bound_in (the_argument_of x) is Element of bound_QC-variables A
bound_QC-variables A is non empty Element of bool (QC-variables A)
[:{4},(QC-symbols A):] is set
Ex ((bound_in (the_argument_of x)),(the_argument_of (the_scope_of (the_argument_of x)))) is Element of QC-WFF A
'not' (the_argument_of (the_scope_of (the_argument_of x))) is Element of QC-WFF A
[1,K98()] is set
{1,K98()} is V24() V25() V26() V27() V28() V29() set
{1} is V24() V25() V26() V27() V28() V29() set
{{1,K98()},{1}} is set
<*[1,K98()]*> is V1() Function-like set
@ (the_argument_of (the_scope_of (the_argument_of x))) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
[:NAT,(QC-symbols A):] is non empty set
K113(<*[1,K98()]*>,(@ (the_argument_of (the_scope_of (the_argument_of x))))) is V1() Function-like FinSequence-like set
All ((bound_in (the_argument_of x)),('not' (the_argument_of (the_scope_of (the_argument_of x))))) is Element of QC-WFF A
3 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
[3,K98()] is set
{3,K98()} is V24() V25() V26() V27() V28() V29() set
{3} is V24() V25() V26() V27() V28() V29() set
{{3,K98()},{3}} is set
<*[3,K98()]*> is V1() Function-like set
<*(bound_in (the_argument_of x))*> is V1() V4( NAT ) V5( bound_QC-variables A) Function-like FinSequence-like FinSequence of bound_QC-variables A
K113(<*[3,K98()]*>,<*(bound_in (the_argument_of x))*>) is V1() Function-like FinSequence-like set
@ ('not' (the_argument_of (the_scope_of (the_argument_of x)))) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(K113(<*[3,K98()]*>,<*(bound_in (the_argument_of x))*>),(@ ('not' (the_argument_of (the_scope_of (the_argument_of x)))))) is V1() Function-like FinSequence-like set
'not' (All ((bound_in (the_argument_of x)),('not' (the_argument_of (the_scope_of (the_argument_of x)))))) is Element of QC-WFF A
@ (All ((bound_in (the_argument_of x)),('not' (the_argument_of (the_scope_of (the_argument_of x)))))) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(<*[1,K98()]*>,(@ (All ((bound_in (the_argument_of x)),('not' (the_argument_of (the_scope_of (the_argument_of x)))))))) is V1() Function-like FinSequence-like set
(A,p,(All ((bound_in (the_argument_of x)),('not' (the_argument_of (the_scope_of (the_argument_of x))))))) is Element of bool p
(A,p,('not' (the_argument_of (the_scope_of (the_argument_of x))))) is Element of bool p
A is V1() non empty QC-alphabet
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bound_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is non empty set
[:{4},(QC-symbols A):] is set
QC-WFF A is non empty set
x is Element of bound_QC-variables A
p is Element of QC-WFF A
Ex (x,p) is Element of QC-WFF A
V is non empty Element of bool (QC-variables A)
(A,V,(Ex (x,p))) is Element of bool V
bool V is non empty set
(A,V,p) is Element of bool V
'not' p is Element of QC-WFF A
[1,K98()] is set
{1,K98()} is V24() V25() V26() V27() V28() V29() set
{1} is V24() V25() V26() V27() V28() V29() set
{{1,K98()},{1}} is set
<*[1,K98()]*> is V1() Function-like set
@ p is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
[:NAT,(QC-symbols A):] is non empty set
K113(<*[1,K98()]*>,(@ p)) is V1() Function-like FinSequence-like set
All (x,('not' p)) is Element of QC-WFF A
3 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
[3,K98()] is set
{3,K98()} is V24() V25() V26() V27() V28() V29() set
{3} is V24() V25() V26() V27() V28() V29() set
{{3,K98()},{3}} is set
<*[3,K98()]*> is V1() Function-like set
<*x*> is V1() V4( NAT ) V5( bound_QC-variables A) Function-like FinSequence-like FinSequence of bound_QC-variables A
K113(<*[3,K98()]*>,<*x*>) is V1() Function-like FinSequence-like set
@ ('not' p) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(K113(<*[3,K98()]*>,<*x*>),(@ ('not' p))) is V1() Function-like FinSequence-like set
'not' (All (x,('not' p))) is Element of QC-WFF A
@ (All (x,('not' p))) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(<*[1,K98()]*>,(@ (All (x,('not' p))))) is V1() Function-like FinSequence-like set
(A,V,(All (x,('not' p)))) is Element of bool V
(A,V,('not' p)) is Element of bool V
A is V1() non empty QC-alphabet
QC-WFF A is non empty set
free_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
x is Element of QC-WFF A
(A,(free_QC-variables A),x) is Element of bool (free_QC-variables A)
bool (free_QC-variables A) is non empty set
A is V1() non empty QC-alphabet
VERUM A is Element of QC-WFF A
QC-WFF A is non empty set
(A,(VERUM A)) is Element of bool (free_QC-variables A)
free_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
bool (free_QC-variables A) is non empty set
(A,(free_QC-variables A),(VERUM A)) is Element of bool (free_QC-variables A)
x is V1() non empty QC-alphabet
QC-pred_symbols x is non empty set
QC-symbols x is non empty set
K49(x) is set
7 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
{ [b1,b2] where b1 is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT , b2 is Element of QC-symbols x : 7 <= b1 } is set
A is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
A -ary_QC-pred_symbols x is non empty Element of bool (QC-pred_symbols x)
bool (QC-pred_symbols x) is non empty set
{ b1 where b1 is Element of QC-pred_symbols x : the_arity_of b1 = A } is set
QC-variables x is non empty set
[:{4,5},(QC-symbols x):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols x):] is set
p is Element of A -ary_QC-pred_symbols x
V is V1() V4( NAT ) V5( QC-variables x) Function-like V45(A) FinSequence-like FinSequence of QC-variables x
p ! V is Element of QC-WFF x
QC-WFF x is non empty set
(x,(p ! V)) is Element of bool (free_QC-variables x)
free_QC-variables x is non empty Element of bool (QC-variables x)
bool (QC-variables x) is non empty set
bool (free_QC-variables x) is non empty set
(x,(free_QC-variables x),(p ! V)) is Element of bool (free_QC-variables x)
len V is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
{ (V . b1) where b1 is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT : ( 1 <= b1 & b1 <= len V & V . b1 in free_QC-variables x ) } is set
A is V1() non empty QC-alphabet
QC-WFF A is non empty set
x is Element of QC-WFF A
'not' x is Element of QC-WFF A
[1,K98()] is set
{1,K98()} is V24() V25() V26() V27() V28() V29() set
{1} is V24() V25() V26() V27() V28() V29() set
{{1,K98()},{1}} is set
<*[1,K98()]*> is V1() Function-like set
@ x is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
QC-symbols A is non empty set
K49(A) is set
[:NAT,(QC-symbols A):] is non empty set
K113(<*[1,K98()]*>,(@ x)) is V1() Function-like FinSequence-like set
(A,('not' x)) is Element of bool (free_QC-variables A)
free_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
bool (free_QC-variables A) is non empty set
(A,(free_QC-variables A),('not' x)) is Element of bool (free_QC-variables A)
(A,x) is Element of bool (free_QC-variables A)
(A,(free_QC-variables A),x) is Element of bool (free_QC-variables A)
A is V1() non empty QC-alphabet
FALSUM A is Element of QC-WFF A
QC-WFF A is non empty set
(A,(FALSUM A)) is Element of bool (free_QC-variables A)
free_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
bool (free_QC-variables A) is non empty set
(A,(free_QC-variables A),(FALSUM A)) is Element of bool (free_QC-variables A)
A is V1() non empty QC-alphabet
QC-WFF A is non empty set
x is Element of QC-WFF A
p is Element of QC-WFF A
x '&' p is Element of QC-WFF A
2 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
[2,K98()] is set
{2,K98()} is V24() V25() V26() V27() V28() V29() set
{2} is V24() V25() V26() V27() V28() V29() set
{{2,K98()},{2}} is set
<*[2,K98()]*> is V1() Function-like set
@ x is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
QC-symbols A is non empty set
K49(A) is set
[:NAT,(QC-symbols A):] is non empty set
K113(<*[2,K98()]*>,(@ x)) is V1() Function-like FinSequence-like set
@ p is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(K113(<*[2,K98()]*>,(@ x)),(@ p)) is V1() Function-like FinSequence-like set
(A,(x '&' p)) is Element of bool (free_QC-variables A)
free_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
bool (free_QC-variables A) is non empty set
(A,(free_QC-variables A),(x '&' p)) is Element of bool (free_QC-variables A)
(A,x) is Element of bool (free_QC-variables A)
(A,(free_QC-variables A),x) is Element of bool (free_QC-variables A)
(A,p) is Element of bool (free_QC-variables A)
(A,(free_QC-variables A),p) is Element of bool (free_QC-variables A)
(A,x) \/ (A,p) is Element of bool (free_QC-variables A)
A is V1() non empty QC-alphabet
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bound_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is non empty set
[:{4},(QC-symbols A):] is set
QC-WFF A is non empty set
x is Element of bound_QC-variables A
p is Element of QC-WFF A
All (x,p) is Element of QC-WFF A
3 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
[3,K98()] is set
{3,K98()} is V24() V25() V26() V27() V28() V29() set
{3} is V24() V25() V26() V27() V28() V29() set
{{3,K98()},{3}} is set
<*[3,K98()]*> is V1() Function-like set
<*x*> is V1() V4( NAT ) V5( bound_QC-variables A) Function-like FinSequence-like FinSequence of bound_QC-variables A
K113(<*[3,K98()]*>,<*x*>) is V1() Function-like FinSequence-like set
@ p is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
[:NAT,(QC-symbols A):] is non empty set
K113(K113(<*[3,K98()]*>,<*x*>),(@ p)) is V1() Function-like FinSequence-like set
(A,(All (x,p))) is Element of bool (free_QC-variables A)
free_QC-variables A is non empty Element of bool (QC-variables A)
bool (free_QC-variables A) is non empty set
(A,(free_QC-variables A),(All (x,p))) is Element of bool (free_QC-variables A)
(A,p) is Element of bool (free_QC-variables A)
(A,(free_QC-variables A),p) is Element of bool (free_QC-variables A)
A is V1() non empty QC-alphabet
QC-WFF A is non empty set
free_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
x is Element of QC-WFF A
(A,x) is Element of bool (free_QC-variables A)
bool (free_QC-variables A) is non empty set
(A,(free_QC-variables A),x) is Element of bool (free_QC-variables A)
p is Element of QC-WFF A
x 'or' p is Element of QC-WFF A
(A,(x 'or' p)) is Element of bool (free_QC-variables A)
(A,(free_QC-variables A),(x 'or' p)) is Element of bool (free_QC-variables A)
(A,p) is Element of bool (free_QC-variables A)
(A,(free_QC-variables A),p) is Element of bool (free_QC-variables A)
(A,x) \/ (A,p) is Element of bool (free_QC-variables A)
'not' x is Element of QC-WFF A
[1,K98()] is set
{1,K98()} is V24() V25() V26() V27() V28() V29() set
{1} is V24() V25() V26() V27() V28() V29() set
{{1,K98()},{1}} is set
<*[1,K98()]*> is V1() Function-like set
@ x is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
[:NAT,(QC-symbols A):] is non empty set
K113(<*[1,K98()]*>,(@ x)) is V1() Function-like FinSequence-like set
'not' p is Element of QC-WFF A
@ p is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(<*[1,K98()]*>,(@ p)) is V1() Function-like FinSequence-like set
('not' x) '&' ('not' p) is Element of QC-WFF A
2 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
[2,K98()] is set
{2,K98()} is V24() V25() V26() V27() V28() V29() set
{2} is V24() V25() V26() V27() V28() V29() set
{{2,K98()},{2}} is set
<*[2,K98()]*> is V1() Function-like set
@ ('not' x) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(<*[2,K98()]*>,(@ ('not' x))) is V1() Function-like FinSequence-like set
@ ('not' p) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(K113(<*[2,K98()]*>,(@ ('not' x))),(@ ('not' p))) is V1() Function-like FinSequence-like set
'not' (('not' x) '&' ('not' p)) is Element of QC-WFF A
@ (('not' x) '&' ('not' p)) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(<*[1,K98()]*>,(@ (('not' x) '&' ('not' p)))) is V1() Function-like FinSequence-like set
(A,(('not' x) '&' ('not' p))) is Element of bool (free_QC-variables A)
(A,(free_QC-variables A),(('not' x) '&' ('not' p))) is Element of bool (free_QC-variables A)
(A,('not' x)) is Element of bool (free_QC-variables A)
(A,(free_QC-variables A),('not' x)) is Element of bool (free_QC-variables A)
(A,('not' p)) is Element of bool (free_QC-variables A)
(A,(free_QC-variables A),('not' p)) is Element of bool (free_QC-variables A)
(A,('not' x)) \/ (A,('not' p)) is Element of bool (free_QC-variables A)
(A,x) \/ (A,('not' p)) is Element of bool (free_QC-variables A)
A is V1() non empty QC-alphabet
QC-WFF A is non empty set
free_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
x is Element of QC-WFF A
(A,x) is Element of bool (free_QC-variables A)
bool (free_QC-variables A) is non empty set
(A,(free_QC-variables A),x) is Element of bool (free_QC-variables A)
p is Element of QC-WFF A
x => p is Element of QC-WFF A
(A,(x => p)) is Element of bool (free_QC-variables A)
(A,(free_QC-variables A),(x => p)) is Element of bool (free_QC-variables A)
(A,p) is Element of bool (free_QC-variables A)
(A,(free_QC-variables A),p) is Element of bool (free_QC-variables A)
(A,x) \/ (A,p) is Element of bool (free_QC-variables A)
'not' p is Element of QC-WFF A
[1,K98()] is set
{1,K98()} is V24() V25() V26() V27() V28() V29() set
{1} is V24() V25() V26() V27() V28() V29() set
{{1,K98()},{1}} is set
<*[1,K98()]*> is V1() Function-like set
@ p is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
[:NAT,(QC-symbols A):] is non empty set
K113(<*[1,K98()]*>,(@ p)) is V1() Function-like FinSequence-like set
x '&' ('not' p) is Element of QC-WFF A
2 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
[2,K98()] is set
{2,K98()} is V24() V25() V26() V27() V28() V29() set
{2} is V24() V25() V26() V27() V28() V29() set
{{2,K98()},{2}} is set
<*[2,K98()]*> is V1() Function-like set
@ x is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(<*[2,K98()]*>,(@ x)) is V1() Function-like FinSequence-like set
@ ('not' p) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(K113(<*[2,K98()]*>,(@ x)),(@ ('not' p))) is V1() Function-like FinSequence-like set
'not' (x '&' ('not' p)) is Element of QC-WFF A
@ (x '&' ('not' p)) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(<*[1,K98()]*>,(@ (x '&' ('not' p)))) is V1() Function-like FinSequence-like set
(A,(x '&' ('not' p))) is Element of bool (free_QC-variables A)
(A,(free_QC-variables A),(x '&' ('not' p))) is Element of bool (free_QC-variables A)
(A,('not' p)) is Element of bool (free_QC-variables A)
(A,(free_QC-variables A),('not' p)) is Element of bool (free_QC-variables A)
(A,x) \/ (A,('not' p)) is Element of bool (free_QC-variables A)
A is V1() non empty QC-alphabet
QC-WFF A is non empty set
free_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
x is Element of QC-WFF A
(A,x) is Element of bool (free_QC-variables A)
bool (free_QC-variables A) is non empty set
(A,(free_QC-variables A),x) is Element of bool (free_QC-variables A)
p is Element of QC-WFF A
x <=> p is Element of QC-WFF A
(A,(x <=> p)) is Element of bool (free_QC-variables A)
(A,(free_QC-variables A),(x <=> p)) is Element of bool (free_QC-variables A)
(A,p) is Element of bool (free_QC-variables A)
(A,(free_QC-variables A),p) is Element of bool (free_QC-variables A)
(A,x) \/ (A,p) is Element of bool (free_QC-variables A)
x => p is Element of QC-WFF A
p => x is Element of QC-WFF A
(x => p) '&' (p => x) is Element of QC-WFF A
2 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
[2,K98()] is set
{2,K98()} is V24() V25() V26() V27() V28() V29() set
{2} is V24() V25() V26() V27() V28() V29() set
{{2,K98()},{2}} is set
<*[2,K98()]*> is V1() Function-like set
@ (x => p) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
[:NAT,(QC-symbols A):] is non empty set
K113(<*[2,K98()]*>,(@ (x => p))) is V1() Function-like FinSequence-like set
@ (p => x) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(K113(<*[2,K98()]*>,(@ (x => p))),(@ (p => x))) is V1() Function-like FinSequence-like set
(A,(x => p)) is Element of bool (free_QC-variables A)
(A,(free_QC-variables A),(x => p)) is Element of bool (free_QC-variables A)
(A,(p => x)) is Element of bool (free_QC-variables A)
(A,(free_QC-variables A),(p => x)) is Element of bool (free_QC-variables A)
(A,(x => p)) \/ (A,(p => x)) is Element of bool (free_QC-variables A)
((A,x) \/ (A,p)) \/ (A,(p => x)) is Element of bool (free_QC-variables A)
((A,x) \/ (A,p)) \/ ((A,x) \/ (A,p)) is Element of bool (free_QC-variables A)
A is V1() non empty QC-alphabet
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bound_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is non empty set
[:{4},(QC-symbols A):] is set
QC-WFF A is non empty set
x is Element of bound_QC-variables A
p is Element of QC-WFF A
Ex (x,p) is Element of QC-WFF A
(A,(Ex (x,p))) is Element of bool (free_QC-variables A)
free_QC-variables A is non empty Element of bool (QC-variables A)
bool (free_QC-variables A) is non empty set
(A,(free_QC-variables A),(Ex (x,p))) is Element of bool (free_QC-variables A)
(A,p) is Element of bool (free_QC-variables A)
(A,(free_QC-variables A),p) is Element of bool (free_QC-variables A)
'not' p is Element of QC-WFF A
[1,K98()] is set
{1,K98()} is V24() V25() V26() V27() V28() V29() set
{1} is V24() V25() V26() V27() V28() V29() set
{{1,K98()},{1}} is set
<*[1,K98()]*> is V1() Function-like set
@ p is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
[:NAT,(QC-symbols A):] is non empty set
K113(<*[1,K98()]*>,(@ p)) is V1() Function-like FinSequence-like set
All (x,('not' p)) is Element of QC-WFF A
3 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
[3,K98()] is set
{3,K98()} is V24() V25() V26() V27() V28() V29() set
{3} is V24() V25() V26() V27() V28() V29() set
{{3,K98()},{3}} is set
<*[3,K98()]*> is V1() Function-like set
<*x*> is V1() V4( NAT ) V5( bound_QC-variables A) Function-like FinSequence-like FinSequence of bound_QC-variables A
K113(<*[3,K98()]*>,<*x*>) is V1() Function-like FinSequence-like set
@ ('not' p) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(K113(<*[3,K98()]*>,<*x*>),(@ ('not' p))) is V1() Function-like FinSequence-like set
'not' (All (x,('not' p))) is Element of QC-WFF A
@ (All (x,('not' p))) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(<*[1,K98()]*>,(@ (All (x,('not' p))))) is V1() Function-like FinSequence-like set
(A,(All (x,('not' p)))) is Element of bool (free_QC-variables A)
(A,(free_QC-variables A),(All (x,('not' p)))) is Element of bool (free_QC-variables A)
(A,('not' p)) is Element of bool (free_QC-variables A)
(A,(free_QC-variables A),('not' p)) is Element of bool (free_QC-variables A)
A is V1() non empty QC-alphabet
QC-WFF A is non empty set
fixed_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
{5} is V24() V25() V26() V27() V28() V29() set
[:{5},(QC-symbols A):] is set
x is Element of QC-WFF A
(A,(fixed_QC-variables A),x) is Element of bool (fixed_QC-variables A)
bool (fixed_QC-variables A) is non empty set
A is V1() non empty QC-alphabet
VERUM A is Element of QC-WFF A
QC-WFF A is non empty set
(A,(VERUM A)) is Element of bool (fixed_QC-variables A)
fixed_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
[:{5},(QC-symbols A):] is set
bool (fixed_QC-variables A) is non empty set
(A,(fixed_QC-variables A),(VERUM A)) is Element of bool (fixed_QC-variables A)
x is V1() non empty QC-alphabet
QC-pred_symbols x is non empty set
QC-symbols x is non empty set
K49(x) is set
7 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
{ [b1,b2] where b1 is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT , b2 is Element of QC-symbols x : 7 <= b1 } is set
A is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
A -ary_QC-pred_symbols x is non empty Element of bool (QC-pred_symbols x)
bool (QC-pred_symbols x) is non empty set
{ b1 where b1 is Element of QC-pred_symbols x : the_arity_of b1 = A } is set
QC-variables x is non empty set
[:{4,5},(QC-symbols x):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols x):] is set
p is Element of A -ary_QC-pred_symbols x
V is V1() V4( NAT ) V5( QC-variables x) Function-like V45(A) FinSequence-like FinSequence of QC-variables x
p ! V is Element of QC-WFF x
QC-WFF x is non empty set
(x,(p ! V)) is Element of bool (fixed_QC-variables x)
fixed_QC-variables x is non empty Element of bool (QC-variables x)
bool (QC-variables x) is non empty set
[:{5},(QC-symbols x):] is set
bool (fixed_QC-variables x) is non empty set
(x,(fixed_QC-variables x),(p ! V)) is Element of bool (fixed_QC-variables x)
len V is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
{ (V . b1) where b1 is ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT : ( 1 <= b1 & b1 <= len V & V . b1 in fixed_QC-variables x ) } is set
A is V1() non empty QC-alphabet
QC-WFF A is non empty set
x is Element of QC-WFF A
'not' x is Element of QC-WFF A
[1,K98()] is set
{1,K98()} is V24() V25() V26() V27() V28() V29() set
{1} is V24() V25() V26() V27() V28() V29() set
{{1,K98()},{1}} is set
<*[1,K98()]*> is V1() Function-like set
@ x is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
QC-symbols A is non empty set
K49(A) is set
[:NAT,(QC-symbols A):] is non empty set
K113(<*[1,K98()]*>,(@ x)) is V1() Function-like FinSequence-like set
(A,('not' x)) is Element of bool (fixed_QC-variables A)
fixed_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
[:{5},(QC-symbols A):] is set
bool (fixed_QC-variables A) is non empty set
(A,(fixed_QC-variables A),('not' x)) is Element of bool (fixed_QC-variables A)
(A,x) is Element of bool (fixed_QC-variables A)
(A,(fixed_QC-variables A),x) is Element of bool (fixed_QC-variables A)
A is V1() non empty QC-alphabet
FALSUM A is Element of QC-WFF A
QC-WFF A is non empty set
(A,(FALSUM A)) is Element of bool (fixed_QC-variables A)
fixed_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
[:{5},(QC-symbols A):] is set
bool (fixed_QC-variables A) is non empty set
(A,(fixed_QC-variables A),(FALSUM A)) is Element of bool (fixed_QC-variables A)
VERUM A is Element of QC-WFF A
'not' (VERUM A) is Element of QC-WFF A
[1,K98()] is set
{1,K98()} is V24() V25() V26() V27() V28() V29() set
{1} is V24() V25() V26() V27() V28() V29() set
{{1,K98()},{1}} is set
<*[1,K98()]*> is V1() Function-like set
@ (VERUM A) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
[:NAT,(QC-symbols A):] is non empty set
K113(<*[1,K98()]*>,(@ (VERUM A))) is V1() Function-like FinSequence-like set
(A,('not' (VERUM A))) is Element of bool (fixed_QC-variables A)
(A,(fixed_QC-variables A),('not' (VERUM A))) is Element of bool (fixed_QC-variables A)
(A,(VERUM A)) is Element of bool (fixed_QC-variables A)
(A,(fixed_QC-variables A),(VERUM A)) is Element of bool (fixed_QC-variables A)
A is V1() non empty QC-alphabet
QC-WFF A is non empty set
x is Element of QC-WFF A
p is Element of QC-WFF A
x '&' p is Element of QC-WFF A
2 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
[2,K98()] is set
{2,K98()} is V24() V25() V26() V27() V28() V29() set
{2} is V24() V25() V26() V27() V28() V29() set
{{2,K98()},{2}} is set
<*[2,K98()]*> is V1() Function-like set
@ x is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
QC-symbols A is non empty set
K49(A) is set
[:NAT,(QC-symbols A):] is non empty set
K113(<*[2,K98()]*>,(@ x)) is V1() Function-like FinSequence-like set
@ p is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(K113(<*[2,K98()]*>,(@ x)),(@ p)) is V1() Function-like FinSequence-like set
(A,(x '&' p)) is Element of bool (fixed_QC-variables A)
fixed_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
[:{5},(QC-symbols A):] is set
bool (fixed_QC-variables A) is non empty set
(A,(fixed_QC-variables A),(x '&' p)) is Element of bool (fixed_QC-variables A)
(A,x) is Element of bool (fixed_QC-variables A)
(A,(fixed_QC-variables A),x) is Element of bool (fixed_QC-variables A)
(A,p) is Element of bool (fixed_QC-variables A)
(A,(fixed_QC-variables A),p) is Element of bool (fixed_QC-variables A)
(A,x) \/ (A,p) is Element of bool (fixed_QC-variables A)
A is V1() non empty QC-alphabet
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bound_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is non empty set
[:{4},(QC-symbols A):] is set
QC-WFF A is non empty set
x is Element of bound_QC-variables A
p is Element of QC-WFF A
All (x,p) is Element of QC-WFF A
3 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
[3,K98()] is set
{3,K98()} is V24() V25() V26() V27() V28() V29() set
{3} is V24() V25() V26() V27() V28() V29() set
{{3,K98()},{3}} is set
<*[3,K98()]*> is V1() Function-like set
<*x*> is V1() V4( NAT ) V5( bound_QC-variables A) Function-like FinSequence-like FinSequence of bound_QC-variables A
K113(<*[3,K98()]*>,<*x*>) is V1() Function-like FinSequence-like set
@ p is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
[:NAT,(QC-symbols A):] is non empty set
K113(K113(<*[3,K98()]*>,<*x*>),(@ p)) is V1() Function-like FinSequence-like set
(A,(All (x,p))) is Element of bool (fixed_QC-variables A)
fixed_QC-variables A is non empty Element of bool (QC-variables A)
[:{5},(QC-symbols A):] is set
bool (fixed_QC-variables A) is non empty set
(A,(fixed_QC-variables A),(All (x,p))) is Element of bool (fixed_QC-variables A)
(A,p) is Element of bool (fixed_QC-variables A)
(A,(fixed_QC-variables A),p) is Element of bool (fixed_QC-variables A)
A is V1() non empty QC-alphabet
QC-WFF A is non empty set
fixed_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
[:{5},(QC-symbols A):] is set
x is Element of QC-WFF A
(A,x) is Element of bool (fixed_QC-variables A)
bool (fixed_QC-variables A) is non empty set
(A,(fixed_QC-variables A),x) is Element of bool (fixed_QC-variables A)
p is Element of QC-WFF A
x 'or' p is Element of QC-WFF A
(A,(x 'or' p)) is Element of bool (fixed_QC-variables A)
(A,(fixed_QC-variables A),(x 'or' p)) is Element of bool (fixed_QC-variables A)
(A,p) is Element of bool (fixed_QC-variables A)
(A,(fixed_QC-variables A),p) is Element of bool (fixed_QC-variables A)
(A,x) \/ (A,p) is Element of bool (fixed_QC-variables A)
'not' x is Element of QC-WFF A
[1,K98()] is set
{1,K98()} is V24() V25() V26() V27() V28() V29() set
{1} is V24() V25() V26() V27() V28() V29() set
{{1,K98()},{1}} is set
<*[1,K98()]*> is V1() Function-like set
@ x is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
[:NAT,(QC-symbols A):] is non empty set
K113(<*[1,K98()]*>,(@ x)) is V1() Function-like FinSequence-like set
'not' p is Element of QC-WFF A
@ p is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(<*[1,K98()]*>,(@ p)) is V1() Function-like FinSequence-like set
('not' x) '&' ('not' p) is Element of QC-WFF A
2 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
[2,K98()] is set
{2,K98()} is V24() V25() V26() V27() V28() V29() set
{2} is V24() V25() V26() V27() V28() V29() set
{{2,K98()},{2}} is set
<*[2,K98()]*> is V1() Function-like set
@ ('not' x) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(<*[2,K98()]*>,(@ ('not' x))) is V1() Function-like FinSequence-like set
@ ('not' p) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(K113(<*[2,K98()]*>,(@ ('not' x))),(@ ('not' p))) is V1() Function-like FinSequence-like set
'not' (('not' x) '&' ('not' p)) is Element of QC-WFF A
@ (('not' x) '&' ('not' p)) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(<*[1,K98()]*>,(@ (('not' x) '&' ('not' p)))) is V1() Function-like FinSequence-like set
(A,(('not' x) '&' ('not' p))) is Element of bool (fixed_QC-variables A)
(A,(fixed_QC-variables A),(('not' x) '&' ('not' p))) is Element of bool (fixed_QC-variables A)
(A,('not' x)) is Element of bool (fixed_QC-variables A)
(A,(fixed_QC-variables A),('not' x)) is Element of bool (fixed_QC-variables A)
(A,('not' p)) is Element of bool (fixed_QC-variables A)
(A,(fixed_QC-variables A),('not' p)) is Element of bool (fixed_QC-variables A)
(A,('not' x)) \/ (A,('not' p)) is Element of bool (fixed_QC-variables A)
(A,x) \/ (A,('not' p)) is Element of bool (fixed_QC-variables A)
A is V1() non empty QC-alphabet
QC-WFF A is non empty set
fixed_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
[:{5},(QC-symbols A):] is set
x is Element of QC-WFF A
(A,x) is Element of bool (fixed_QC-variables A)
bool (fixed_QC-variables A) is non empty set
(A,(fixed_QC-variables A),x) is Element of bool (fixed_QC-variables A)
p is Element of QC-WFF A
x => p is Element of QC-WFF A
(A,(x => p)) is Element of bool (fixed_QC-variables A)
(A,(fixed_QC-variables A),(x => p)) is Element of bool (fixed_QC-variables A)
(A,p) is Element of bool (fixed_QC-variables A)
(A,(fixed_QC-variables A),p) is Element of bool (fixed_QC-variables A)
(A,x) \/ (A,p) is Element of bool (fixed_QC-variables A)
'not' p is Element of QC-WFF A
[1,K98()] is set
{1,K98()} is V24() V25() V26() V27() V28() V29() set
{1} is V24() V25() V26() V27() V28() V29() set
{{1,K98()},{1}} is set
<*[1,K98()]*> is V1() Function-like set
@ p is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
[:NAT,(QC-symbols A):] is non empty set
K113(<*[1,K98()]*>,(@ p)) is V1() Function-like FinSequence-like set
x '&' ('not' p) is Element of QC-WFF A
2 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
[2,K98()] is set
{2,K98()} is V24() V25() V26() V27() V28() V29() set
{2} is V24() V25() V26() V27() V28() V29() set
{{2,K98()},{2}} is set
<*[2,K98()]*> is V1() Function-like set
@ x is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(<*[2,K98()]*>,(@ x)) is V1() Function-like FinSequence-like set
@ ('not' p) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(K113(<*[2,K98()]*>,(@ x)),(@ ('not' p))) is V1() Function-like FinSequence-like set
'not' (x '&' ('not' p)) is Element of QC-WFF A
@ (x '&' ('not' p)) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(<*[1,K98()]*>,(@ (x '&' ('not' p)))) is V1() Function-like FinSequence-like set
(A,(x '&' ('not' p))) is Element of bool (fixed_QC-variables A)
(A,(fixed_QC-variables A),(x '&' ('not' p))) is Element of bool (fixed_QC-variables A)
(A,('not' p)) is Element of bool (fixed_QC-variables A)
(A,(fixed_QC-variables A),('not' p)) is Element of bool (fixed_QC-variables A)
(A,x) \/ (A,('not' p)) is Element of bool (fixed_QC-variables A)
A is V1() non empty QC-alphabet
QC-WFF A is non empty set
fixed_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bool (QC-variables A) is non empty set
[:{5},(QC-symbols A):] is set
x is Element of QC-WFF A
(A,x) is Element of bool (fixed_QC-variables A)
bool (fixed_QC-variables A) is non empty set
(A,(fixed_QC-variables A),x) is Element of bool (fixed_QC-variables A)
p is Element of QC-WFF A
x <=> p is Element of QC-WFF A
(A,(x <=> p)) is Element of bool (fixed_QC-variables A)
(A,(fixed_QC-variables A),(x <=> p)) is Element of bool (fixed_QC-variables A)
(A,p) is Element of bool (fixed_QC-variables A)
(A,(fixed_QC-variables A),p) is Element of bool (fixed_QC-variables A)
(A,x) \/ (A,p) is Element of bool (fixed_QC-variables A)
x => p is Element of QC-WFF A
p => x is Element of QC-WFF A
(x => p) '&' (p => x) is Element of QC-WFF A
2 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
[2,K98()] is set
{2,K98()} is V24() V25() V26() V27() V28() V29() set
{2} is V24() V25() V26() V27() V28() V29() set
{{2,K98()},{2}} is set
<*[2,K98()]*> is V1() Function-like set
@ (x => p) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
[:NAT,(QC-symbols A):] is non empty set
K113(<*[2,K98()]*>,(@ (x => p))) is V1() Function-like FinSequence-like set
@ (p => x) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(K113(<*[2,K98()]*>,(@ (x => p))),(@ (p => x))) is V1() Function-like FinSequence-like set
(A,(x => p)) is Element of bool (fixed_QC-variables A)
(A,(fixed_QC-variables A),(x => p)) is Element of bool (fixed_QC-variables A)
(A,(p => x)) is Element of bool (fixed_QC-variables A)
(A,(fixed_QC-variables A),(p => x)) is Element of bool (fixed_QC-variables A)
(A,(x => p)) \/ (A,(p => x)) is Element of bool (fixed_QC-variables A)
((A,x) \/ (A,p)) \/ (A,(p => x)) is Element of bool (fixed_QC-variables A)
(A,p) \/ (A,x) is Element of bool (fixed_QC-variables A)
((A,x) \/ (A,p)) \/ ((A,p) \/ (A,x)) is Element of bool (fixed_QC-variables A)
A is V1() non empty QC-alphabet
QC-variables A is non empty set
QC-symbols A is non empty set
K49(A) is set
[:{4,5},(QC-symbols A):] is set
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set
bound_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is non empty set
[:{4},(QC-symbols A):] is set
QC-WFF A is non empty set
x is Element of bound_QC-variables A
p is Element of QC-WFF A
Ex (x,p) is Element of QC-WFF A
(A,(Ex (x,p))) is Element of bool (fixed_QC-variables A)
fixed_QC-variables A is non empty Element of bool (QC-variables A)
[:{5},(QC-symbols A):] is set
bool (fixed_QC-variables A) is non empty set
(A,(fixed_QC-variables A),(Ex (x,p))) is Element of bool (fixed_QC-variables A)
(A,p) is Element of bool (fixed_QC-variables A)
(A,(fixed_QC-variables A),p) is Element of bool (fixed_QC-variables A)
'not' p is Element of QC-WFF A
[1,K98()] is set
{1,K98()} is V24() V25() V26() V27() V28() V29() set
{1} is V24() V25() V26() V27() V28() V29() set
{{1,K98()},{1}} is set
<*[1,K98()]*> is V1() Function-like set
@ p is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
[:NAT,(QC-symbols A):] is non empty set
K113(<*[1,K98()]*>,(@ p)) is V1() Function-like FinSequence-like set
All (x,('not' p)) is Element of QC-WFF A
3 is non empty ext-real V24() V25() V26() V27() V28() V29() V31() V32() V33() V37() Element of NAT
[3,K98()] is set
{3,K98()} is V24() V25() V26() V27() V28() V29() set
{3} is V24() V25() V26() V27() V28() V29() set
{{3,K98()},{3}} is set
<*[3,K98()]*> is V1() Function-like set
<*x*> is V1() V4( NAT ) V5( bound_QC-variables A) Function-like FinSequence-like FinSequence of bound_QC-variables A
K113(<*[3,K98()]*>,<*x*>) is V1() Function-like FinSequence-like set
@ ('not' p) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(K113(<*[3,K98()]*>,<*x*>),(@ ('not' p))) is V1() Function-like FinSequence-like set
'not' (All (x,('not' p))) is Element of QC-WFF A
@ (All (x,('not' p))) is V1() V4( NAT ) V5([:NAT,(QC-symbols A):]) Function-like FinSequence-like FinSequence of [:NAT,(QC-symbols A):]
K113(<*[1,K98()]*>,(@ (All (x,('not' p))))) is V1() Function-like FinSequence-like set
(A,(All (x,('not' p)))) is Element of bool (fixed_QC-variables A)
(A,(fixed_QC-variables A),(All (x,('not' p)))) is Element of bool (fixed_QC-variables A)
(A,('not' p)) is Element of bool (fixed_QC-variables A)
(A,(fixed_QC-variables A),('not' p)) is Element of bool (fixed_QC-variables A)