REAL is V45() V46() V47() V51() V63() V64() V66() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V52() V61() V63() cardinal limit_cardinal Element of bool REAL
bool REAL is non empty set
COMPLEX is V45() V51() set
RAT is V45() V46() V47() V48() V51() set
INT is V45() V46() V47() V48() V49() V51() set
omega is non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V52() V61() V63() cardinal limit_cardinal set
bool omega is non empty V52() set
bool NAT is non empty V52() set
[:COMPLEX,COMPLEX:] is Relation-like set
bool [:COMPLEX,COMPLEX:] is non empty set
[:COMPLEX,REAL:] is Relation-like set
bool [:COMPLEX,REAL:] is non empty set
K370() is set
{} is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V45() V46() V47() V48() V49() V50() V51() V52() V63() V64() V65() V66() cardinal {} -element Function-yielding V82() set
the empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V45() V46() V47() V48() V49() V50() V51() V52() V63() V64() V65() V66() cardinal {} -element Function-yielding V82() set is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V45() V46() V47() V48() V49() V50() V51() V52() V63() V64() V65() V66() cardinal {} -element Function-yielding V82() set
1 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal Element of NAT
TRUE is Element of K370()
0 is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V51() V52() V63() V64() V65() V66() cardinal {} -element Function-yielding V82() Element of NAT
[0,0] is V1() set
{0,0} is non empty functional V45() V46() V47() V48() V49() V50() V61() V63() set
{0} is non empty trivial functional V45() V46() V47() V48() V49() V50() V61() V63() 1 -element set
{{0,0},{0}} is non empty set
<*[0,0]*> is Relation-like Function-like set
[:NAT,NAT:] is non empty Relation-like V52() set
[:NAT,[:NAT,NAT:]:] is non empty Relation-like V52() set
bool [:NAT,[:NAT,NAT:]:] is non empty V52() set
[0,0] is V1() Element of [:NAT,NAT:]
<*[0,0]*> is Relation-like NAT -defined [:NAT,NAT:] -valued Function-like FinSequence-like FinSequence of [:NAT,NAT:]
[1,0] is V1() Element of [:NAT,NAT:]
{1,0} is non empty V45() V46() V47() V48() V49() V50() V61() V63() set
{1} is non empty trivial V45() V46() V47() V48() V49() V50() V61() V63() 1 -element set
{{1,0},{1}} is non empty set
<*[1,0]*> is Relation-like NAT -defined [:NAT,NAT:] -valued Function-like FinSequence-like FinSequence of [:NAT,NAT:]
2 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal Element of NAT
[2,0] is V1() Element of [:NAT,NAT:]
{2,0} is non empty V45() V46() V47() V48() V49() V50() V61() V63() set
{2} is non empty trivial V45() V46() V47() V48() V49() V50() V61() V63() 1 -element set
{{2,0},{2}} is non empty set
<*[2,0]*> is Relation-like NAT -defined [:NAT,NAT:] -valued Function-like FinSequence-like FinSequence of [:NAT,NAT:]
3 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal Element of NAT
[3,0] is V1() Element of [:NAT,NAT:]
{3,0} is non empty V45() V46() V47() V48() V49() V50() V61() V63() set
{3} is non empty trivial V45() V46() V47() V48() V49() V50() V61() V63() 1 -element set
{{3,0},{3}} is non empty set
<*[3,0]*> is Relation-like NAT -defined [:NAT,NAT:] -valued Function-like FinSequence-like FinSequence of [:NAT,NAT:]
xSQ is Relation-like Function-like set
proj1 xSQ is set
J is Relation-like Function-like set
proj1 J is set
S is Relation-like Function-like set
proj1 S is set
Al is Relation-like Function-like set
A is Relation-like Function-like set
Al +* A is Relation-like Function-like set
(Al +* A) +* J is Relation-like Function-like set
Al +* xSQ is Relation-like Function-like set
A +* S is Relation-like Function-like set
(Al +* xSQ) +* (A +* S) is Relation-like Function-like set
((Al +* xSQ) +* (A +* S)) +* J is Relation-like Function-like set
proj1 (Al +* xSQ) is set
proj1 Al is set
(proj1 Al) \/ (proj1 xSQ) is set
proj1 (A +* S) is set
proj1 A is set
(proj1 A) \/ (proj1 S) is set
proj1 ((Al +* xSQ) +* (A +* S)) is set
((proj1 Al) \/ (proj1 xSQ)) \/ ((proj1 A) \/ (proj1 S)) is set
proj1 (((Al +* xSQ) +* (A +* S)) +* J) is set
(((proj1 Al) \/ (proj1 xSQ)) \/ ((proj1 A) \/ (proj1 S))) \/ (proj1 J) is set
((proj1 A) \/ (proj1 S)) \/ (proj1 J) is set
((proj1 Al) \/ (proj1 xSQ)) \/ (((proj1 A) \/ (proj1 S)) \/ (proj1 J)) is set
(proj1 S) \/ (proj1 J) is set
(proj1 A) \/ ((proj1 S) \/ (proj1 J)) is set
((proj1 Al) \/ (proj1 xSQ)) \/ ((proj1 A) \/ ((proj1 S) \/ (proj1 J))) is set
(proj1 A) \/ (proj1 J) is set
((proj1 Al) \/ (proj1 xSQ)) \/ ((proj1 A) \/ (proj1 J)) is set
((proj1 Al) \/ (proj1 xSQ)) \/ (proj1 J) is set
(((proj1 Al) \/ (proj1 xSQ)) \/ (proj1 J)) \/ (proj1 A) is set
(proj1 xSQ) \/ (proj1 J) is set
(proj1 Al) \/ ((proj1 xSQ) \/ (proj1 J)) is set
((proj1 Al) \/ ((proj1 xSQ) \/ (proj1 J))) \/ (proj1 A) is set
(proj1 Al) \/ (proj1 J) is set
((proj1 Al) \/ (proj1 J)) \/ (proj1 A) is set
proj1 ((Al +* A) +* J) is set
xSQ is set
((Al +* A) +* J) . xSQ is set
(((Al +* xSQ) +* (A +* S)) +* J) . xSQ is set
((Al +* xSQ) +* (A +* S)) . xSQ is set
(Al +* A) . xSQ is set
(A +* S) . xSQ is set
A . xSQ is set
(Al +* xSQ) . xSQ is set
Al . xSQ is set
J . xSQ is set
proj1 (Al +* A) is set
(proj1 Al) \/ (proj1 A) is set
((proj1 Al) \/ (proj1 A)) \/ (proj1 J) is set
Al is non empty Relation-like QC-alphabet
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
A is Element of bound_QC-variables Al
{A} is non empty trivial 1 -element Element of bool (bound_QC-variables Al)
bool (bound_QC-variables Al) is non empty set
J is Relation-like Function-like set
proj1 J is set
(proj1 J) \ {A} is Element of bool (proj1 J)
bool (proj1 J) is non empty set
J | ((proj1 J) \ {A}) is Relation-like Function-like set
J . A is set
A .--> (J . A) is trivial Relation-like bound_QC-variables Al -defined {A} -defined Function-like one-to-one constant set
{A} is non empty trivial 1 -element set
{A} --> (J . A) is non empty Relation-like {A} -defined {(J . A)} -valued Function-like constant total quasi_total Element of bool [:{A},{(J . A)}:]
{(J . A)} is non empty trivial 1 -element set
[:{A},{(J . A)}:] is non empty Relation-like set
bool [:{A},{(J . A)}:] is non empty set
(J | ((proj1 J) \ {A})) +* (A .--> (J . A)) is Relation-like Function-like set
((proj1 J) \ {A}) \/ {A} is non empty set
(proj1 J) \/ {A} is non empty set
Al is non empty Relation-like QC-alphabet
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
QC-variables Al is non empty set
bool (QC-variables Al) is non empty set
A is non empty set
Valuations_in (Al,A) is non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
[:(bound_QC-variables Al),A:] is non empty Relation-like set
bool [:(bound_QC-variables Al),A:] is non empty set
Al is non empty Relation-like QC-alphabet
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
QC-variables Al is non empty set
bool (QC-variables Al) is non empty set
A is non empty set
Valuations_in (Al,A) is non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
[:(bound_QC-variables Al),A:] is non empty Relation-like set
bool [:(bound_QC-variables Al),A:] is non empty set
J is Relation-like bound_QC-variables Al -defined A -valued Function-like quasi_total Element of Valuations_in (Al,A)
xSQ is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),A:]
J +* xSQ is Relation-like bound_QC-variables Al -defined A -valued Function-like set
Funcs ((bound_QC-variables Al),A) is non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
J +* xSQ is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),A:]
dom (J +* xSQ) is Element of bool (bound_QC-variables Al)
bool (bound_QC-variables Al) is non empty set
dom xSQ is Element of bool (bound_QC-variables Al)
(bound_QC-variables Al) \/ (dom xSQ) is non empty set
S is Relation-like Function-like set
proj1 S is set
proj2 S is set
rng (J +* xSQ) is Element of bool A
bool A is non empty set
rng J is Element of bool A
rng xSQ is Element of bool A
(rng J) \/ (rng xSQ) is Element of bool A
Al is non empty Relation-like QC-alphabet
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
A is Element of CQC-Sub-WFF Al
A `1 is set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
{ b1 where b1 is Element of QC-Sub-WFF Al : b1 `1 is Element of CQC-WFF Al } is set
J is Element of QC-Sub-WFF Al
J `1 is Element of QC-WFF Al
Al is non empty Relation-like QC-alphabet
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
QC-variables Al is non empty set
bool (QC-variables Al) is non empty set
J is non empty set
Valuations_in (Al,J) is non empty FUNCTION_DOMAIN of bound_QC-variables Al,J
A is Element of CQC-Sub-WFF Al
A `2 is Relation-like Function-like Element of vSUB Al
vSUB Al is non empty functional set
@ (A `2) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -valued Function-like Element of bool [:(bound_QC-variables Al),(bound_QC-variables Al):]
[:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty Relation-like set
bool [:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty set
xSQ is Relation-like bound_QC-variables Al -defined J -valued Function-like quasi_total Element of Valuations_in (Al,J)
(@ (A `2)) * xSQ is Relation-like bound_QC-variables Al -defined J -valued Function-like Element of bool [:(bound_QC-variables Al),J:]
[:(bound_QC-variables Al),J:] is non empty Relation-like set
bool [:(bound_QC-variables Al),J:] is non empty set
Al is non empty Relation-like QC-alphabet
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
VERUM Al is Element of CQC-WFF Al
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
A is Element of CQC-Sub-WFF Al
CQC_Sub A is Element of CQC-WFF Al
[:(QC-Sub-WFF Al),(QC-WFF Al):] is non empty Relation-like set
bool [:(QC-Sub-WFF Al),(QC-WFF Al):] is non empty set
J is Relation-like QC-Sub-WFF Al -defined QC-WFF Al -valued Function-like quasi_total Element of bool [:(QC-Sub-WFF Al),(QC-WFF Al):]
J . A is Element of QC-WFF Al
Al is non empty Relation-like QC-alphabet
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
QC-variables Al is non empty set
bool (QC-variables Al) is non empty set
J is non empty set
Valuations_in (Al,J) is non empty FUNCTION_DOMAIN of bound_QC-variables Al,J
QC-pred_symbols Al is non empty set
K367(J) is set
Al is non empty Relation-like QC-alphabet
QC-pred_symbols Al is non empty set
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
QC-variables Al is non empty set
bool (QC-variables Al) is non empty set
A is non empty set
K367(A) is set
Valuations_in (Al,A) is non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
J is Relation-like QC-pred_symbols Al -defined K367(A) -valued Function-like quasi_total interpretation of Al,A
xSQ is Element of CQC-Sub-WFF Al
CQC_Sub xSQ is Element of CQC-WFF Al
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
S is Relation-like bound_QC-variables Al -defined A -valued Function-like quasi_total Element of Valuations_in (Al,A)
(Al,xSQ,A,S) is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),A:]
[:(bound_QC-variables Al),A:] is non empty Relation-like set
bool [:(bound_QC-variables Al),A:] is non empty set
xSQ `2 is Relation-like Function-like Element of vSUB Al
vSUB Al is non empty functional set
@ (xSQ `2) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -valued Function-like Element of bool [:(bound_QC-variables Al),(bound_QC-variables Al):]
[:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty Relation-like set
bool [:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty set
(@ (xSQ `2)) * S is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),A:]
(Al,A,S,(Al,xSQ,A,S)) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -defined A -valued Function-like quasi_total Element of Valuations_in (Al,A)
VERUM Al is Element of CQC-WFF Al
(Al,xSQ) is Element of CQC-WFF Al
xSQ is Relation-like Function-like Element of vSUB Al
[(VERUM Al),xSQ] is V1() Element of [:(CQC-WFF Al),(vSUB Al):]
[:(CQC-WFF Al),(vSUB Al):] is non empty Relation-like set
{(VERUM Al),xSQ} is non empty set
{(VERUM Al)} is non empty trivial 1 -element set
{{(VERUM Al),xSQ},{(VERUM Al)}} is non empty set
Al is non empty Relation-like QC-alphabet
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
QC-variables Al is non empty set
bool (QC-variables Al) is non empty set
A is ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
J is ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
xSQ is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like A -element FinSequence-like FinSequence of QC-variables Al
dom xSQ is V45() V46() V47() V48() V49() V50() V63() A -element Element of bool NAT
xSQ . J is set
rng xSQ is Element of bool (QC-variables Al)
Al is non empty Relation-like QC-alphabet
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
A is Element of CQC-Sub-WFF Al
CQC_Sub A is Element of CQC-WFF Al
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
(Al,A) is Element of CQC-WFF Al
the_pred_symbol_of (Al,A) is Element of QC-pred_symbols Al
QC-pred_symbols Al is non empty set
Sub_the_arguments_of A is Relation-like NAT -defined QC-variables Al -valued Function-like FinSequence-like FinSequence of QC-variables Al
QC-variables Al is non empty set
A `2 is Relation-like Function-like Element of vSUB Al
vSUB Al is non empty functional set
CQC_Subst ((Sub_the_arguments_of A),(A `2)) is Relation-like NAT -defined QC-variables Al -valued Function-like FinSequence-like FinSequence of QC-variables Al
(the_pred_symbol_of (Al,A)) ! (CQC_Subst ((Sub_the_arguments_of A),(A `2))) is Element of QC-WFF Al
[:(QC-Sub-WFF Al),(QC-WFF Al):] is non empty Relation-like set
bool [:(QC-Sub-WFF Al),(QC-WFF Al):] is non empty set
VERUM Al is Element of CQC-WFF Al
J is Relation-like QC-Sub-WFF Al -defined QC-WFF Al -valued Function-like quasi_total Element of bool [:(QC-Sub-WFF Al),(QC-WFF Al):]
J . A is Element of QC-WFF Al
Al is non empty Relation-like QC-alphabet
QC-pred_symbols Al is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
QC-variables Al is non empty set
bool (QC-variables Al) is non empty set
vSUB Al is non empty functional set
A is ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
A -ary_QC-pred_symbols Al is non empty Element of bool (QC-pred_symbols Al)
bool (QC-pred_symbols Al) is non empty set
J is Element of A -ary_QC-pred_symbols Al
xSQ is Element of A -ary_QC-pred_symbols Al
S is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like A -element FinSequence-like FinSequence of QC-variables Al
xSQ is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like A -element FinSequence-like FinSequence of QC-variables Al
v is Relation-like Function-like Element of vSUB Al
Sub_P (J,S,v) is Sub_atomic Element of QC-Sub-WFF Al
QC-Sub-WFF Al is non empty Al -Sub-closed set
Sub_the_arguments_of (Sub_P (J,S,v)) is Relation-like NAT -defined QC-variables Al -valued Function-like FinSequence-like FinSequence of QC-variables Al
S1 is Relation-like Function-like Element of vSUB Al
Sub_P (xSQ,xSQ,S1) is Sub_atomic Element of QC-Sub-WFF Al
Sub_the_arguments_of (Sub_P (xSQ,xSQ,S1)) is Relation-like NAT -defined QC-variables Al -valued Function-like FinSequence-like FinSequence of QC-variables Al
z is ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
z -ary_QC-pred_symbols Al is non empty Element of bool (QC-pred_symbols Al)
p is Relation-like NAT -defined QC-variables Al -valued Function-like z -element FinSequence-like FinSequence of QC-variables Al
q is Element of z -ary_QC-pred_symbols Al
a is Relation-like Function-like Element of vSUB Al
Sub_P (q,p,a) is Sub_atomic Element of QC-Sub-WFF Al
J ! S is Element of CQC-WFF Al
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
<*J*> is Relation-like NAT -defined A -ary_QC-pred_symbols Al -valued Function-like FinSequence-like FinSequence of A -ary_QC-pred_symbols Al
<*J*> ^ S is Relation-like Function-like FinSequence-like set
q ! p is Element of QC-WFF Al
<*q*> is Relation-like NAT -defined z -ary_QC-pred_symbols Al -valued Function-like FinSequence-like FinSequence of z -ary_QC-pred_symbols Al
<*q*> ^ p is Relation-like Function-like FinSequence-like set
[(J ! S),v] is V1() Element of [:(CQC-WFF Al),(vSUB Al):]
[:(CQC-WFF Al),(vSUB Al):] is non empty Relation-like set
{(J ! S),v} is non empty set
{(J ! S)} is non empty trivial 1 -element set
{{(J ! S),v},{(J ! S)}} is non empty set
[(q ! p),a] is V1() Element of [:(QC-WFF Al),(vSUB Al):]
[:(QC-WFF Al),(vSUB Al):] is non empty Relation-like set
{(q ! p),a} is non empty set
{(q ! p)} is non empty trivial 1 -element set
{{(q ! p),a},{(q ! p)}} is non empty set
(<*q*> ^ p) . 1 is set
(<*J*> ^ S) . 1 is set
x is ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
x -ary_QC-pred_symbols Al is non empty Element of bool (QC-pred_symbols Al)
x is Relation-like NAT -defined QC-variables Al -valued Function-like x -element FinSequence-like FinSequence of QC-variables Al
b is Element of x -ary_QC-pred_symbols Al
e2 is Relation-like Function-like Element of vSUB Al
Sub_P (b,x,e2) is Sub_atomic Element of QC-Sub-WFF Al
xSQ ! xSQ is Element of CQC-WFF Al
<*xSQ*> is Relation-like NAT -defined A -ary_QC-pred_symbols Al -valued Function-like FinSequence-like FinSequence of A -ary_QC-pred_symbols Al
<*xSQ*> ^ xSQ is Relation-like Function-like FinSequence-like set
b ! x is Element of QC-WFF Al
<*b*> is Relation-like NAT -defined x -ary_QC-pred_symbols Al -valued Function-like FinSequence-like FinSequence of x -ary_QC-pred_symbols Al
<*b*> ^ x is Relation-like Function-like FinSequence-like set
[(xSQ ! xSQ),S1] is V1() Element of [:(CQC-WFF Al),(vSUB Al):]
{(xSQ ! xSQ),S1} is non empty set
{(xSQ ! xSQ)} is non empty trivial 1 -element set
{{(xSQ ! xSQ),S1},{(xSQ ! xSQ)}} is non empty set
[(b ! x),e2] is V1() Element of [:(QC-WFF Al),(vSUB Al):]
{(b ! x),e2} is non empty set
{(b ! x)} is non empty trivial 1 -element set
{{(b ! x),e2},{(b ! x)}} is non empty set
(<*b*> ^ x) . 1 is set
(<*xSQ*> ^ xSQ) . 1 is set
A is non empty Relation-like QC-alphabet
QC-pred_symbols A is non empty set
Al is ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
Al -ary_QC-pred_symbols A is non empty Element of bool (QC-pred_symbols A)
bool (QC-pred_symbols 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
bool (QC-variables A) is non empty set
vSUB A is non empty functional set
J is Element of Al -ary_QC-pred_symbols A
xSQ is Relation-like NAT -defined bound_QC-variables A -valued QC-variables A -valued Function-like Al -element FinSequence-like FinSequence of QC-variables A
S is Relation-like Function-like Element of vSUB A
Sub_P (J,xSQ,S) is Sub_atomic Element of QC-Sub-WFF A
QC-Sub-WFF A is non empty A -Sub-closed set
CQC-Sub-WFF A is non empty Element of bool (QC-Sub-WFF A)
bool (QC-Sub-WFF A) is non empty set
QC-WFF A is non empty set
CQC-WFF A is non empty Element of bool (QC-WFF A)
bool (QC-WFF A) is non empty set
{ b1 where b1 is Element of QC-Sub-WFF A : b1 `1 is Element of CQC-WFF A } is set
v is Element of QC-Sub-WFF A
v `1 is Element of QC-WFF A
J ! xSQ is Element of CQC-WFF A
[(J ! xSQ),S] is V1() Element of [:(CQC-WFF A),(vSUB A):]
[:(CQC-WFF A),(vSUB A):] is non empty Relation-like set
{(J ! xSQ),S} is non empty set
{(J ! xSQ)} is non empty trivial 1 -element set
{{(J ! xSQ),S},{(J ! xSQ)}} is non empty set
(Sub_P (J,xSQ,S)) `1 is Element of QC-WFF A
Al is non empty Relation-like QC-alphabet
QC-pred_symbols Al is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
QC-variables Al is non empty set
bool (QC-variables Al) is non empty set
vSUB Al is non empty functional set
A is ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
A -ary_QC-pred_symbols Al is non empty Element of bool (QC-pred_symbols Al)
bool (QC-pred_symbols Al) is non empty set
J is Element of A -ary_QC-pred_symbols Al
xSQ is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like A -element FinSequence-like FinSequence of QC-variables Al
S is Relation-like Function-like Element of vSUB Al
(A,Al,J,xSQ,S) is Sub_atomic Element of CQC-Sub-WFF Al
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
CQC_Sub (A,Al,J,xSQ,S) is Element of CQC-WFF Al
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
CQC_Subst (xSQ,S) is Relation-like NAT -defined QC-variables Al -valued Function-like FinSequence-like FinSequence of QC-variables Al
J ! (CQC_Subst (xSQ,S)) is Element of QC-WFF Al
J ! xSQ is Element of CQC-WFF Al
[(J ! xSQ),S] is V1() Element of [:(CQC-WFF Al),(vSUB Al):]
[:(CQC-WFF Al),(vSUB Al):] is non empty Relation-like set
{(J ! xSQ),S} is non empty set
{(J ! xSQ)} is non empty trivial 1 -element set
{{(J ! xSQ),S},{(J ! xSQ)}} is non empty set
(A,Al,J,xSQ,S) `2 is Relation-like Function-like Element of vSUB Al
(Al,(A,Al,J,xSQ,S)) is Element of CQC-WFF Al
Sub_the_arguments_of (A,Al,J,xSQ,S) is Relation-like NAT -defined QC-variables Al -valued Function-like FinSequence-like FinSequence of QC-variables Al
the_pred_symbol_of (Al,(A,Al,J,xSQ,S)) is Element of QC-pred_symbols Al
Al is non empty Relation-like QC-alphabet
QC-pred_symbols Al is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
QC-variables Al is non empty set
bool (QC-variables Al) is non empty set
vSUB Al is non empty functional set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
A is ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
A -ary_QC-pred_symbols Al is non empty Element of bool (QC-pred_symbols Al)
bool (QC-pred_symbols Al) is non empty set
J is Element of A -ary_QC-pred_symbols Al
xSQ is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like A -element FinSequence-like FinSequence of QC-variables Al
S is Relation-like Function-like Element of vSUB Al
CQC_Subst (xSQ,S) is Relation-like NAT -defined QC-variables Al -valued Function-like FinSequence-like FinSequence of QC-variables Al
J ! (CQC_Subst (xSQ,S)) is Element of QC-WFF Al
(A,Al,J,xSQ,S) is Sub_atomic Element of CQC-Sub-WFF Al
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
CQC_Sub (A,Al,J,xSQ,S) is Element of CQC-WFF Al
Al is non empty Relation-like QC-alphabet
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
QC-variables Al is non empty set
bool (QC-variables Al) is non empty set
vSUB Al is non empty functional set
A is ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
J is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like A -element FinSequence-like FinSequence of QC-variables Al
xSQ is Relation-like Function-like Element of vSUB Al
CQC_Subst (J,xSQ) is Relation-like NAT -defined QC-variables Al -valued Function-like FinSequence-like FinSequence of QC-variables Al
S is Relation-like NAT -defined bound_QC-variables Al -valued Function-like FinSequence-like FinSequence of bound_QC-variables Al
CQC_Subst (S,xSQ) is Relation-like NAT -defined bound_QC-variables Al -valued Function-like FinSequence-like FinSequence of bound_QC-variables Al
xSQ is Relation-like NAT -defined bound_QC-variables Al -valued Function-like FinSequence-like FinSequence of bound_QC-variables Al
@ S is Relation-like NAT -defined QC-variables Al -valued Function-like FinSequence-like FinSequence of QC-variables Al
CQC_Subst ((@ S),xSQ) is Relation-like NAT -defined QC-variables Al -valued Function-like FinSequence-like FinSequence of QC-variables Al
len S is ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
len (@ S) is ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
len xSQ is ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
Al is non empty Relation-like QC-alphabet
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
QC-variables Al is non empty set
bool (QC-variables Al) is non empty set
A is ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
vSUB Al is non empty functional set
J is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like A -element FinSequence-like FinSequence of QC-variables Al
xSQ is Relation-like Function-like Element of vSUB Al
CQC_Subst (J,xSQ) is Relation-like NAT -defined QC-variables Al -valued Function-like FinSequence-like FinSequence of QC-variables Al
Al is non empty Relation-like QC-alphabet
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
A is Element of bound_QC-variables Al
J is non empty set
Valuations_in (Al,J) is non empty FUNCTION_DOMAIN of bound_QC-variables Al,J
xSQ is Relation-like bound_QC-variables Al -defined J -valued Function-like quasi_total Element of Valuations_in (Al,J)
xSQ . A is Element of J
S is Element of CQC-Sub-WFF Al
S `2 is Relation-like Function-like Element of vSUB Al
vSUB Al is non empty functional set
proj1 (S `2) is set
(Al,S,J,xSQ) is Relation-like bound_QC-variables Al -defined J -valued Function-like Element of bool [:(bound_QC-variables Al),J:]
[:(bound_QC-variables Al),J:] is non empty Relation-like set
bool [:(bound_QC-variables Al),J:] is non empty set
@ (S `2) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -valued Function-like Element of bool [:(bound_QC-variables Al),(bound_QC-variables Al):]
[:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty Relation-like set
bool [:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty set
(@ (S `2)) * xSQ is Relation-like bound_QC-variables Al -defined J -valued Function-like Element of bool [:(bound_QC-variables Al),J:]
(Al,J,xSQ,(Al,S,J,xSQ)) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -defined J -valued Function-like quasi_total Element of Valuations_in (Al,J)
(Al,J,xSQ,(Al,S,J,xSQ)) . A is Element of J
dom (@ (S `2)) is Element of bool (bound_QC-variables Al)
bool (bound_QC-variables Al) is non empty set
dom ((@ (S `2)) * xSQ) is Element of bool (bound_QC-variables Al)
dom (Al,S,J,xSQ) is Element of bool (bound_QC-variables Al)
Al is non empty Relation-like QC-alphabet
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
A is Element of bound_QC-variables Al
J is non empty set
Valuations_in (Al,J) is non empty FUNCTION_DOMAIN of bound_QC-variables Al,J
xSQ is Relation-like bound_QC-variables Al -defined J -valued Function-like quasi_total Element of Valuations_in (Al,J)
S is Element of CQC-Sub-WFF Al
S `2 is Relation-like Function-like Element of vSUB Al
vSUB Al is non empty functional set
proj1 (S `2) is set
(Al,S,J,xSQ) is Relation-like bound_QC-variables Al -defined J -valued Function-like Element of bool [:(bound_QC-variables Al),J:]
[:(bound_QC-variables Al),J:] is non empty Relation-like set
bool [:(bound_QC-variables Al),J:] is non empty set
@ (S `2) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -valued Function-like Element of bool [:(bound_QC-variables Al),(bound_QC-variables Al):]
[:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty Relation-like set
bool [:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty set
(@ (S `2)) * xSQ is Relation-like bound_QC-variables Al -defined J -valued Function-like Element of bool [:(bound_QC-variables Al),J:]
(Al,J,xSQ,(Al,S,J,xSQ)) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -defined J -valued Function-like quasi_total Element of Valuations_in (Al,J)
(Al,J,xSQ,(Al,S,J,xSQ)) . A is Element of J
(Al,S,J,xSQ) . A is set
dom (@ (S `2)) is Element of bool (bound_QC-variables Al)
bool (bound_QC-variables Al) is non empty set
rng (@ (S `2)) is Element of bool (bound_QC-variables Al)
dom xSQ is Element of bool (bound_QC-variables Al)
dom (Al,S,J,xSQ) is Element of bool (bound_QC-variables Al)
Al is non empty Relation-like QC-alphabet
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
QC-variables Al is non empty set
bool (QC-variables Al) is non empty set
QC-pred_symbols Al is non empty set
vSUB Al is non empty functional set
A is ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
A -ary_QC-pred_symbols Al is non empty Element of bool (QC-pred_symbols Al)
bool (QC-pred_symbols Al) is non empty set
J is non empty set
Valuations_in (Al,J) is non empty FUNCTION_DOMAIN of bound_QC-variables Al,J
xSQ is Relation-like bound_QC-variables Al -defined J -valued Function-like quasi_total Element of Valuations_in (Al,J)
S is Element of A -ary_QC-pred_symbols Al
xSQ is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like A -element FinSequence-like FinSequence of QC-variables Al
v is Relation-like Function-like Element of vSUB Al
(A,Al,S,xSQ,v) is Sub_atomic Element of CQC-Sub-WFF Al
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
(Al,(A,Al,S,xSQ,v),J,xSQ) is Relation-like bound_QC-variables Al -defined J -valued Function-like Element of bool [:(bound_QC-variables Al),J:]
[:(bound_QC-variables Al),J:] is non empty Relation-like set
bool [:(bound_QC-variables Al),J:] is non empty set
(A,Al,S,xSQ,v) `2 is Relation-like Function-like Element of vSUB Al
@ ((A,Al,S,xSQ,v) `2) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -valued Function-like Element of bool [:(bound_QC-variables Al),(bound_QC-variables Al):]
[:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty Relation-like set
bool [:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty set
(@ ((A,Al,S,xSQ,v) `2)) * xSQ is Relation-like bound_QC-variables Al -defined J -valued Function-like Element of bool [:(bound_QC-variables Al),J:]
(Al,J,xSQ,(Al,(A,Al,S,xSQ,v),J,xSQ)) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -defined J -valued Function-like quasi_total Element of Valuations_in (Al,J)
(Al,J,xSQ,(Al,(A,Al,S,xSQ,v),J,xSQ)) *' xSQ is Relation-like NAT -defined J -valued Function-like FinSequence-like FinSequence of J
CQC_Subst (xSQ,v) is Relation-like NAT -defined QC-variables Al -valued bound_QC-variables Al -valued Function-like A -element FinSequence-like FinSequence of QC-variables Al
xSQ *' (CQC_Subst (xSQ,v)) is Relation-like NAT -defined J -valued Function-like FinSequence-like FinSequence of J
len xSQ is ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
S ! xSQ is Element of CQC-WFF Al
[(S ! xSQ),v] is V1() Element of [:(CQC-WFF Al),(vSUB Al):]
[:(CQC-WFF Al),(vSUB Al):] is non empty Relation-like set
{(S ! xSQ),v} is non empty set
{(S ! xSQ)} is non empty trivial 1 -element set
{{(S ! xSQ),v},{(S ! xSQ)}} is non empty set
len ((Al,J,xSQ,(Al,(A,Al,S,xSQ,v),J,xSQ)) *' xSQ) is ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
dom ((Al,J,xSQ,(Al,(A,Al,S,xSQ,v),J,xSQ)) *' xSQ) is V45() V46() V47() V48() V49() V50() V63() Element of bool NAT
Seg A is V45() V46() V47() V48() V49() V50() V63() Element of bool NAT
q is ext-real epsilon-transitive epsilon-connected ordinal natural V52() cardinal set
((Al,J,xSQ,(Al,(A,Al,S,xSQ,v),J,xSQ)) *' xSQ) . q is set
(xSQ *' (CQC_Subst (xSQ,v))) . q is set
p is ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
Seg (len xSQ) is V45() V46() V47() V48() V49() V50() V63() Element of bool NAT
dom xSQ is V45() V46() V47() V48() V49() V50() V63() A -element Element of bool NAT
xSQ . p is set
proj1 v is set
(Al,J,xSQ,(Al,(A,Al,S,xSQ,v),J,xSQ)) . (xSQ . p) is set
a is Element of bound_QC-variables Al
(Al,(A,Al,S,xSQ,v),J,xSQ) . a is set
dom (@ ((A,Al,S,xSQ,v) `2)) is Element of bool (bound_QC-variables Al)
bool (bound_QC-variables Al) is non empty set
(@ ((A,Al,S,xSQ,v) `2)) . (xSQ . p) is set
xSQ . ((@ ((A,Al,S,xSQ,v) `2)) . (xSQ . p)) is set
((A,Al,S,xSQ,v) `2) . (xSQ . p) is set
xSQ . (((A,Al,S,xSQ,v) `2) . (xSQ . p)) is set
((Al,J,xSQ,(Al,(A,Al,S,xSQ,v),J,xSQ)) *' xSQ) . p is set
(CQC_Subst (xSQ,v)) . p is set
xSQ . ((CQC_Subst (xSQ,v)) . p) is set
xSQ . (xSQ . p) is set
xSQ . a is Element of J
(xSQ *' (CQC_Subst (xSQ,v))) . p is set
len (xSQ *' (CQC_Subst (xSQ,v))) is ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
Al is non empty Relation-like QC-alphabet
QC-pred_symbols Al is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
QC-variables Al is non empty set
bool (QC-variables Al) is non empty set
vSUB Al is non empty functional set
A is ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
A -ary_QC-pred_symbols Al is non empty Element of bool (QC-pred_symbols Al)
bool (QC-pred_symbols Al) is non empty set
J is Element of A -ary_QC-pred_symbols Al
xSQ is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like A -element FinSequence-like FinSequence of QC-variables Al
J ! xSQ is Element of CQC-WFF Al
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
S is Relation-like Function-like Element of vSUB Al
(A,Al,J,xSQ,S) is Sub_atomic Element of CQC-Sub-WFF Al
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
(Al,(A,Al,J,xSQ,S)) is Element of CQC-WFF Al
[(J ! xSQ),S] is V1() Element of [:(CQC-WFF Al),(vSUB Al):]
[:(CQC-WFF Al),(vSUB Al):] is non empty Relation-like set
{(J ! xSQ),S} is non empty set
{(J ! xSQ)} is non empty trivial 1 -element set
{{(J ! xSQ),S},{(J ! xSQ)}} is non empty set
Al is non empty Relation-like QC-alphabet
QC-pred_symbols Al is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
QC-variables Al is non empty set
bool (QC-variables Al) is non empty set
vSUB Al is non empty functional set
A is ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
A -ary_QC-pred_symbols Al is non empty Element of bool (QC-pred_symbols Al)
bool (QC-pred_symbols Al) is non empty set
J is non empty set
K367(J) is set
Valuations_in (Al,J) is non empty FUNCTION_DOMAIN of bound_QC-variables Al,J
xSQ is Relation-like QC-pred_symbols Al -defined K367(J) -valued Function-like quasi_total interpretation of Al,J
S is Element of A -ary_QC-pred_symbols Al
xSQ is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like A -element FinSequence-like FinSequence of QC-variables Al
v is Relation-like Function-like Element of vSUB Al
(A,Al,S,xSQ,v) is Sub_atomic Element of CQC-Sub-WFF Al
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
CQC_Sub (A,Al,S,xSQ,v) is Element of CQC-WFF Al
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
CQC_Subst (xSQ,v) is Relation-like NAT -defined QC-variables Al -valued bound_QC-variables Al -valued Function-like A -element FinSequence-like FinSequence of QC-variables Al
S ! (CQC_Subst (xSQ,v)) is Element of CQC-WFF Al
a is Relation-like bound_QC-variables Al -defined J -valued Function-like quasi_total Element of Valuations_in (Al,J)
(Al,(A,Al,S,xSQ,v),J,a) is Relation-like bound_QC-variables Al -defined J -valued Function-like Element of bool [:(bound_QC-variables Al),J:]
[:(bound_QC-variables Al),J:] is non empty Relation-like set
bool [:(bound_QC-variables Al),J:] is non empty set
(A,Al,S,xSQ,v) `2 is Relation-like Function-like Element of vSUB Al
@ ((A,Al,S,xSQ,v) `2) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -valued Function-like Element of bool [:(bound_QC-variables Al),(bound_QC-variables Al):]
[:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty Relation-like set
bool [:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty set
(@ ((A,Al,S,xSQ,v) `2)) * a is Relation-like bound_QC-variables Al -defined J -valued Function-like Element of bool [:(bound_QC-variables Al),J:]
(Al,J,a,(Al,(A,Al,S,xSQ,v),J,a)) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -defined J -valued Function-like quasi_total Element of Valuations_in (Al,J)
q is Element of CQC-WFF Al
Valid (q,xSQ) is Relation-like Valuations_in (Al,J) -defined K370() -valued Function-like quasi_total Element of Funcs ((Valuations_in (Al,J)),K370())
Funcs ((Valuations_in (Al,J)),K370()) is non empty FUNCTION_DOMAIN of Valuations_in (Al,J),K370()
(Valid (q,xSQ)) . a is Element of K370()
p is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like A -element FinSequence-like FinSequence of QC-variables Al
a *' p is Relation-like NAT -defined J -valued Function-like FinSequence-like FinSequence of J
xSQ . S is Element of K367(J)
(Al,J,a,(Al,(A,Al,S,xSQ,v),J,a)) *' xSQ is Relation-like NAT -defined J -valued Function-like FinSequence-like FinSequence of J
S ! xSQ is Element of CQC-WFF Al
Valid ((S ! xSQ),xSQ) is Relation-like Valuations_in (Al,J) -defined K370() -valued Function-like quasi_total Element of Funcs ((Valuations_in (Al,J)),K370())
(Valid ((S ! xSQ),xSQ)) . (Al,J,a,(Al,(A,Al,S,xSQ,v),J,a)) is Element of K370()
(Al,(A,Al,S,xSQ,v)) is Element of CQC-WFF Al
Al is non empty Relation-like QC-alphabet
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
A is Element of CQC-Sub-WFF Al
Sub_not A is Sub_negative Element of QC-Sub-WFF Al
(Sub_not A) `1 is Element of QC-WFF Al
QC-WFF Al is non empty set
(Al,A) is Element of CQC-WFF Al
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
'not' (Al,A) is Element of CQC-WFF Al
(Sub_not A) `2 is Relation-like Function-like Element of vSUB Al
vSUB Al is non empty functional set
A `2 is Relation-like Function-like Element of vSUB Al
[('not' (Al,A)),(A `2)] is V1() Element of [:(CQC-WFF Al),(vSUB Al):]
[:(CQC-WFF Al),(vSUB Al):] is non empty Relation-like set
{('not' (Al,A)),(A `2)} is non empty set
{('not' (Al,A))} is non empty trivial 1 -element set
{{('not' (Al,A)),(A `2)},{('not' (Al,A))}} is non empty set
Al is non empty Relation-like QC-alphabet
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
A is Element of CQC-Sub-WFF Al
Sub_not A is Sub_negative Element of QC-Sub-WFF Al
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
{ b1 where b1 is Element of QC-Sub-WFF Al : b1 `1 is Element of CQC-WFF Al } is set
xSQ is Element of QC-Sub-WFF Al
xSQ `1 is Element of QC-WFF Al
(Al,A) is Element of CQC-WFF Al
'not' (Al,A) is Element of CQC-WFF Al
(Sub_not A) `1 is Element of QC-WFF Al
Al is non empty Relation-like QC-alphabet
QC-pred_symbols Al is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
QC-variables Al is non empty set
bool (QC-variables Al) is non empty set
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
A is non empty set
K367(A) is set
Valuations_in (Al,A) is non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
J is Relation-like QC-pred_symbols Al -defined K367(A) -valued Function-like quasi_total interpretation of Al,A
xSQ is Relation-like bound_QC-variables Al -defined A -valued Function-like quasi_total Element of Valuations_in (Al,A)
S is Element of CQC-Sub-WFF Al
(Al,S,A,xSQ) is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),A:]
[:(bound_QC-variables Al),A:] is non empty Relation-like set
bool [:(bound_QC-variables Al),A:] is non empty set
S `2 is Relation-like Function-like Element of vSUB Al
vSUB Al is non empty functional set
@ (S `2) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -valued Function-like Element of bool [:(bound_QC-variables Al),(bound_QC-variables Al):]
[:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty Relation-like set
bool [:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty set
(@ (S `2)) * xSQ is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),A:]
(Al,A,xSQ,(Al,S,A,xSQ)) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -defined A -valued Function-like quasi_total Element of Valuations_in (Al,A)
(Al,S) is Sub_negative Element of CQC-Sub-WFF Al
(Al,S) is Element of CQC-WFF Al
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
'not' (Al,S) is Element of CQC-WFF Al
(Al,(Al,S)) is Element of CQC-WFF Al
Al is non empty Relation-like QC-alphabet
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
QC-variables Al is non empty set
bool (QC-variables Al) is non empty set
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
A is non empty set
Valuations_in (Al,A) is non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
J is Relation-like bound_QC-variables Al -defined A -valued Function-like quasi_total Element of Valuations_in (Al,A)
xSQ is Element of CQC-Sub-WFF Al
(Al,xSQ,A,J) is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),A:]
[:(bound_QC-variables Al),A:] is non empty Relation-like set
bool [:(bound_QC-variables Al),A:] is non empty set
xSQ `2 is Relation-like Function-like Element of vSUB Al
vSUB Al is non empty functional set
@ (xSQ `2) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -valued Function-like Element of bool [:(bound_QC-variables Al),(bound_QC-variables Al):]
[:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty Relation-like set
bool [:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty set
(@ (xSQ `2)) * J is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),A:]
(Al,xSQ) is Sub_negative Element of CQC-Sub-WFF Al
(Al,(Al,xSQ),A,J) is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),A:]
(Al,xSQ) `2 is Relation-like Function-like Element of vSUB Al
@ ((Al,xSQ) `2) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -valued Function-like Element of bool [:(bound_QC-variables Al),(bound_QC-variables Al):]
(@ ((Al,xSQ) `2)) * J is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),A:]
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
(Al,xSQ) is Element of CQC-WFF Al
'not' (Al,xSQ) is Element of CQC-WFF Al
[('not' (Al,xSQ)),(xSQ `2)] is V1() Element of [:(CQC-WFF Al),(vSUB Al):]
[:(CQC-WFF Al),(vSUB Al):] is non empty Relation-like set
{('not' (Al,xSQ)),(xSQ `2)} is non empty set
{('not' (Al,xSQ))} is non empty trivial 1 -element set
{{('not' (Al,xSQ)),(xSQ `2)},{('not' (Al,xSQ))}} is non empty set
Al is non empty Relation-like QC-alphabet
QC-pred_symbols Al is non empty set
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
QC-variables Al is non empty set
bool (QC-variables Al) is non empty set
A is non empty set
K367(A) is set
Valuations_in (Al,A) is non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
J is Relation-like QC-pred_symbols Al -defined K367(A) -valued Function-like quasi_total interpretation of Al,A
xSQ is Element of CQC-Sub-WFF Al
CQC_Sub xSQ is Element of CQC-WFF Al
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
(Al,xSQ) is Sub_negative Element of CQC-Sub-WFF Al
CQC_Sub (Al,xSQ) is Element of CQC-WFF Al
S is Relation-like bound_QC-variables Al -defined A -valued Function-like quasi_total Element of Valuations_in (Al,A)
(Al,(Al,xSQ),A,S) is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),A:]
[:(bound_QC-variables Al),A:] is non empty Relation-like set
bool [:(bound_QC-variables Al),A:] is non empty set
(Al,xSQ) `2 is Relation-like Function-like Element of vSUB Al
vSUB Al is non empty functional set
@ ((Al,xSQ) `2) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -valued Function-like Element of bool [:(bound_QC-variables Al),(bound_QC-variables Al):]
[:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty Relation-like set
bool [:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty set
(@ ((Al,xSQ) `2)) * S is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),A:]
(Al,A,S,(Al,(Al,xSQ),A,S)) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -defined A -valued Function-like quasi_total Element of Valuations_in (Al,A)
'not' (CQC_Sub xSQ) is Element of CQC-WFF Al
(Al,xSQ,A,S) is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),A:]
xSQ `2 is Relation-like Function-like Element of vSUB Al
@ (xSQ `2) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -valued Function-like Element of bool [:(bound_QC-variables Al),(bound_QC-variables Al):]
(@ (xSQ `2)) * S is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),A:]
(Al,A,S,(Al,xSQ,A,S)) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -defined A -valued Function-like quasi_total Element of Valuations_in (Al,A)
Al is non empty Relation-like QC-alphabet
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
A is Element of CQC-Sub-WFF Al
A `2 is Relation-like Function-like Element of vSUB Al
vSUB Al is non empty functional set
J is Element of CQC-Sub-WFF Al
J `2 is Relation-like Function-like Element of vSUB Al
Sub_& (A,J) is Element of QC-Sub-WFF Al
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
{ b1 where b1 is Element of QC-Sub-WFF Al : b1 `1 is Element of CQC-WFF Al } is set
S is Element of QC-Sub-WFF Al
S `1 is Element of QC-WFF Al
(Al,A) is Element of CQC-WFF Al
(Al,J) is Element of CQC-WFF Al
(Al,A) '&' (Al,J) is Element of CQC-WFF Al
[((Al,A) '&' (Al,J)),(A `2)] is V1() Element of [:(CQC-WFF Al),(vSUB Al):]
[:(CQC-WFF Al),(vSUB Al):] is non empty Relation-like set
{((Al,A) '&' (Al,J)),(A `2)} is non empty set
{((Al,A) '&' (Al,J))} is non empty trivial 1 -element set
{{((Al,A) '&' (Al,J)),(A `2)},{((Al,A) '&' (Al,J))}} is non empty set
(Sub_& (A,J)) `1 is Element of QC-WFF Al
Al is non empty Relation-like QC-alphabet
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
A is Element of CQC-Sub-WFF Al
A `2 is Relation-like Function-like Element of vSUB Al
vSUB Al is non empty functional set
(Al,A) is Element of CQC-WFF Al
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
J is Element of CQC-Sub-WFF Al
J `2 is Relation-like Function-like Element of vSUB Al
(Al,A,J) is Element of CQC-Sub-WFF Al
(Al,(Al,A,J)) is Element of CQC-WFF Al
(Al,J) is Element of CQC-WFF Al
(Al,A) '&' (Al,J) is Element of CQC-WFF Al
(Al,A,J) `2 is Relation-like Function-like Element of vSUB Al
Sub_& (A,J) is Element of QC-Sub-WFF Al
[((Al,A) '&' (Al,J)),(A `2)] is V1() Element of [:(CQC-WFF Al),(vSUB Al):]
[:(CQC-WFF Al),(vSUB Al):] is non empty Relation-like set
{((Al,A) '&' (Al,J)),(A `2)} is non empty set
{((Al,A) '&' (Al,J))} is non empty trivial 1 -element set
{{((Al,A) '&' (Al,J)),(A `2)},{((Al,A) '&' (Al,J))}} is non empty set
Al is non empty Relation-like QC-alphabet
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
A is Element of CQC-Sub-WFF Al
A `2 is Relation-like Function-like Element of vSUB Al
vSUB Al is non empty functional set
J is Element of CQC-Sub-WFF Al
J `2 is Relation-like Function-like Element of vSUB Al
(Al,A,J) is Element of CQC-Sub-WFF Al
(Al,A,J) `2 is Relation-like Function-like Element of vSUB Al
Sub_& (A,J) is Element of QC-Sub-WFF Al
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
(Al,A) is Element of CQC-WFF Al
(Al,J) is Element of CQC-WFF Al
(Al,A) '&' (Al,J) is Element of CQC-WFF Al
[((Al,A) '&' (Al,J)),(A `2)] is V1() Element of [:(CQC-WFF Al),(vSUB Al):]
[:(CQC-WFF Al),(vSUB Al):] is non empty Relation-like set
{((Al,A) '&' (Al,J)),(A `2)} is non empty set
{((Al,A) '&' (Al,J))} is non empty trivial 1 -element set
{{((Al,A) '&' (Al,J)),(A `2)},{((Al,A) '&' (Al,J))}} is non empty set
Al is non empty Relation-like QC-alphabet
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
QC-variables Al is non empty set
bool (QC-variables Al) is non empty set
A is non empty set
Valuations_in (Al,A) is non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
xSQ is Element of CQC-Sub-WFF Al
xSQ `2 is Relation-like Function-like Element of vSUB Al
vSUB Al is non empty functional set
S is Element of CQC-Sub-WFF Al
S `2 is Relation-like Function-like Element of vSUB Al
J is Relation-like bound_QC-variables Al -defined A -valued Function-like quasi_total Element of Valuations_in (Al,A)
(Al,xSQ,A,J) is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),A:]
[:(bound_QC-variables Al),A:] is non empty Relation-like set
bool [:(bound_QC-variables Al),A:] is non empty set
@ (xSQ `2) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -valued Function-like Element of bool [:(bound_QC-variables Al),(bound_QC-variables Al):]
[:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty Relation-like set
bool [:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty set
(@ (xSQ `2)) * J is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),A:]
(Al,xSQ,S) is Element of CQC-Sub-WFF Al
(Al,(Al,xSQ,S),A,J) is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),A:]
(Al,xSQ,S) `2 is Relation-like Function-like Element of vSUB Al
@ ((Al,xSQ,S) `2) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -valued Function-like Element of bool [:(bound_QC-variables Al),(bound_QC-variables Al):]
(@ ((Al,xSQ,S) `2)) * J is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),A:]
(Al,S,A,J) is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),A:]
@ (S `2) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -valued Function-like Element of bool [:(bound_QC-variables Al),(bound_QC-variables Al):]
(@ (S `2)) * J is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),A:]
Al is non empty Relation-like QC-alphabet
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
A is Element of CQC-Sub-WFF Al
A `2 is Relation-like Function-like Element of vSUB Al
vSUB Al is non empty functional set
CQC_Sub A is Element of CQC-WFF Al
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
J is Element of CQC-Sub-WFF Al
J `2 is Relation-like Function-like Element of vSUB Al
(Al,A,J) is Element of CQC-Sub-WFF Al
CQC_Sub (Al,A,J) is Element of CQC-WFF Al
CQC_Sub J is Element of CQC-WFF Al
(CQC_Sub A) '&' (CQC_Sub J) is Element of CQC-WFF Al
Sub_& (A,J) is Element of QC-Sub-WFF Al
Al is non empty Relation-like QC-alphabet
QC-pred_symbols Al is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
QC-variables Al is non empty set
bool (QC-variables Al) is non empty set
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
A is non empty set
K367(A) is set
Valuations_in (Al,A) is non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
J is Relation-like QC-pred_symbols Al -defined K367(A) -valued Function-like quasi_total interpretation of Al,A
xSQ is Relation-like bound_QC-variables Al -defined A -valued Function-like quasi_total Element of Valuations_in (Al,A)
S is Element of CQC-Sub-WFF Al
S `2 is Relation-like Function-like Element of vSUB Al
vSUB Al is non empty functional set
(Al,S,A,xSQ) is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),A:]
[:(bound_QC-variables Al),A:] is non empty Relation-like set
bool [:(bound_QC-variables Al),A:] is non empty set
@ (S `2) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -valued Function-like Element of bool [:(bound_QC-variables Al),(bound_QC-variables Al):]
[:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty Relation-like set
bool [:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty set
(@ (S `2)) * xSQ is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),A:]
(Al,A,xSQ,(Al,S,A,xSQ)) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -defined A -valued Function-like quasi_total Element of Valuations_in (Al,A)
xSQ is Element of CQC-Sub-WFF Al
xSQ `2 is Relation-like Function-like Element of vSUB Al
(Al,xSQ,A,xSQ) is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),A:]
@ (xSQ `2) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -valued Function-like Element of bool [:(bound_QC-variables Al),(bound_QC-variables Al):]
(@ (xSQ `2)) * xSQ is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),A:]
(Al,A,xSQ,(Al,xSQ,A,xSQ)) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -defined A -valued Function-like quasi_total Element of Valuations_in (Al,A)
(Al,S,xSQ) is Element of CQC-Sub-WFF Al
(Al,(Al,S,xSQ),A,xSQ) is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),A:]
(Al,S,xSQ) `2 is Relation-like Function-like Element of vSUB Al
@ ((Al,S,xSQ) `2) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -valued Function-like Element of bool [:(bound_QC-variables Al),(bound_QC-variables Al):]
(@ ((Al,S,xSQ) `2)) * xSQ is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),A:]
(Al,A,xSQ,(Al,(Al,S,xSQ),A,xSQ)) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -defined A -valued Function-like quasi_total Element of Valuations_in (Al,A)
(Al,S) is Element of CQC-WFF Al
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
(Al,xSQ) is Element of CQC-WFF Al
(Al,S) '&' (Al,xSQ) is Element of CQC-WFF Al
(Al,(Al,S,xSQ)) is Element of CQC-WFF Al
Al is non empty Relation-like QC-alphabet
QC-pred_symbols Al is non empty set
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
QC-variables Al is non empty set
bool (QC-variables Al) is non empty set
A is non empty set
K367(A) is set
Valuations_in (Al,A) is non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
J is Relation-like QC-pred_symbols Al -defined K367(A) -valued Function-like quasi_total interpretation of Al,A
xSQ is Element of CQC-Sub-WFF Al
xSQ `2 is Relation-like Function-like Element of vSUB Al
vSUB Al is non empty functional set
CQC_Sub xSQ is Element of CQC-WFF Al
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
S is Element of CQC-Sub-WFF Al
S `2 is Relation-like Function-like Element of vSUB Al
CQC_Sub S is Element of CQC-WFF Al
(Al,xSQ,S) is Element of CQC-Sub-WFF Al
CQC_Sub (Al,xSQ,S) is Element of CQC-WFF Al
xSQ is Relation-like bound_QC-variables Al -defined A -valued Function-like quasi_total Element of Valuations_in (Al,A)
(Al,(Al,xSQ,S),A,xSQ) is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),A:]
[:(bound_QC-variables Al),A:] is non empty Relation-like set
bool [:(bound_QC-variables Al),A:] is non empty set
(Al,xSQ,S) `2 is Relation-like Function-like Element of vSUB Al
@ ((Al,xSQ,S) `2) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -valued Function-like Element of bool [:(bound_QC-variables Al),(bound_QC-variables Al):]
[:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty Relation-like set
bool [:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty set
(@ ((Al,xSQ,S) `2)) * xSQ is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),A:]
(Al,A,xSQ,(Al,(Al,xSQ,S),A,xSQ)) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -defined A -valued Function-like quasi_total Element of Valuations_in (Al,A)
(Al,xSQ,A,xSQ) is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),A:]
@ (xSQ `2) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -valued Function-like Element of bool [:(bound_QC-variables Al),(bound_QC-variables Al):]
(@ (xSQ `2)) * xSQ is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),A:]
(Al,A,xSQ,(Al,xSQ,A,xSQ)) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -defined A -valued Function-like quasi_total Element of Valuations_in (Al,A)
(Al,S,A,xSQ) is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),A:]
@ (S `2) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -valued Function-like Element of bool [:(bound_QC-variables Al),(bound_QC-variables Al):]
(@ (S `2)) * xSQ is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),A:]
(Al,A,xSQ,(Al,S,A,xSQ)) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -defined A -valued Function-like quasi_total Element of Valuations_in (Al,A)
(CQC_Sub xSQ) '&' (CQC_Sub S) is Element of CQC-WFF Al
Al is non empty Relation-like QC-alphabet
QC-Sub-WFF Al is non empty Al -Sub-closed set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
QC-variables Al is non empty set
bool (QC-variables Al) is non empty set
[:(QC-Sub-WFF Al),(bound_QC-variables Al):] is non empty Relation-like set
A is Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):]
A `2 is Element of bound_QC-variables Al
A `1 is Element of QC-Sub-WFF Al
(A `1) `1 is Element of QC-WFF Al
QC-WFF Al is non empty set
All ((A `2),((A `1) `1)) is Element of QC-WFF Al
J is Relation-like Function-like second_Q_comp of A
Sub_All (A,J) is Element of QC-Sub-WFF Al
(Sub_All (A,J)) `1 is Element of QC-WFF Al
(Sub_All (A,J)) `2 is Relation-like Function-like Element of vSUB Al
vSUB Al is non empty functional set
[(All ((A `2),((A `1) `1))),J] is V1() Element of [:(QC-WFF Al),(vSUB Al):]
[:(QC-WFF Al),(vSUB Al):] is non empty Relation-like set
{(All ((A `2),((A `1) `1))),J} is non empty set
{(All ((A `2),((A `1) `1)))} is non empty trivial 1 -element set
{{(All ((A `2),((A `1) `1))),J},{(All ((A `2),((A `1) `1)))}} is non empty set
Al is non empty Relation-like QC-alphabet
QC-Sub-WFF Al is non empty Al -Sub-closed set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
QC-variables Al is non empty set
bool (QC-variables Al) is non empty set
[:(QC-Sub-WFF Al),(bound_QC-variables Al):] is non empty Relation-like set
Al is non empty Relation-like QC-alphabet
QC-Sub-WFF Al is non empty Al -Sub-closed set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
QC-variables Al is non empty set
bool (QC-variables Al) is non empty set
[:(QC-Sub-WFF Al),(bound_QC-variables Al):] is non empty Relation-like set
vSUB Al is non empty functional set
the Relation-like Function-like Element of vSUB Al is Relation-like Function-like Element of vSUB Al
the Element of bound_QC-variables Al is Element of bound_QC-variables Al
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
[:(CQC-WFF Al),(vSUB Al):] is non empty Relation-like set
VERUM Al is Element of CQC-WFF Al
[(VERUM Al), the Relation-like Function-like Element of vSUB Al] is V1() Element of [:(CQC-WFF Al),(vSUB Al):]
{(VERUM Al), the Relation-like Function-like Element of vSUB Al} is non empty set
{(VERUM Al)} is non empty trivial 1 -element set
{{(VERUM Al), the Relation-like Function-like Element of vSUB Al},{(VERUM Al)}} is non empty set
[[(VERUM Al), the Relation-like Function-like Element of vSUB Al], the Element of bound_QC-variables Al] is V1() Element of [:[:(CQC-WFF Al),(vSUB Al):],(bound_QC-variables Al):]
[:[:(CQC-WFF Al),(vSUB Al):],(bound_QC-variables Al):] is non empty Relation-like set
{[(VERUM Al), the Relation-like Function-like Element of vSUB Al], the Element of bound_QC-variables Al} is non empty set
{[(VERUM Al), the Relation-like Function-like Element of vSUB Al]} is non empty trivial Relation-like Function-like constant 1 -element set
{{[(VERUM Al), the Relation-like Function-like Element of vSUB Al], the Element of bound_QC-variables Al},{[(VERUM Al), the Relation-like Function-like Element of vSUB Al]}} is non empty set
[<*[0,0]*>, the Relation-like Function-like Element of vSUB Al] is V1() Element of [:(bool [:NAT,[:NAT,NAT:]:]),(vSUB Al):]
[:(bool [:NAT,[:NAT,NAT:]:]),(vSUB Al):] is non empty Relation-like V52() set
{<*[0,0]*>, the Relation-like Function-like