VALUAT_1

:: VALUAT_1 semantic presentation

REAL is V4() V5() V6() V10() set
NAT is V4() V5() V6() V7() V8() V9() V10() ordinal V40() V45() V46() Element of K24(REAL)
K24(REAL) is set
NAT is V4() V5() V6() V7() V8() V9() V10() ordinal V40() V45() V46() set
K24(NAT) is V40() set
K24(NAT) is V40() set
BOOLEAN is non empty set
{} is V4() V5() V6() V7() V8() V9() V10() Function-like functional empty ordinal V45() V47( {} ) V53() set
1 is ext-real V4() V5() V6() V7() V8() V9() non empty ordinal natural V40() V45() Element of NAT
0 is ext-real non positive non negative V4() V5() V6() V7() V8() V9() V10() Function-like functional empty ordinal natural V40() V45() V47( {} ) V53() Element of NAT
FALSE is boolean Element of BOOLEAN
TRUE is boolean Element of BOOLEAN
K143() is set
K144() is set
Al is Relation-like non empty QC-alphabet
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
QC-variables Al is non empty set
K24((QC-variables Al)) is set
A is set
Funcs ((bound_QC-variables Al),A) is functional set
Al is Relation-like non empty QC-alphabet
A is non empty set
(Al,A) is set
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
QC-variables Al is non empty set
K24((QC-variables Al)) is set
Funcs ((bound_QC-variables Al),A) is functional non empty set
Al is Relation-like non empty QC-alphabet
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
QC-variables Al is non empty set
K24((QC-variables Al)) is set
A is non empty set
(Al,A) is functional non empty set
Funcs ((bound_QC-variables Al),A) is functional non empty set
K25((bound_QC-variables Al),A) is set
K24(K25((bound_QC-variables Al),A)) is set
x is set
y is Relation-like Function-like set
dom y is set
rng y is set
Al is Relation-like non empty QC-alphabet
A is non empty set
(Al,A) is functional non empty set
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
QC-variables Al is non empty set
K24((QC-variables Al)) is set
Funcs ((bound_QC-variables Al),A) is functional non empty set
K25((bound_QC-variables Al),A) is set
K24(K25((bound_QC-variables Al),A)) is set
x is Relation-like Function-like Element of (Al,A)
Al is Relation-like non empty QC-alphabet
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
K24((QC-variables Al)) is set
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((bound_QC-variables Al),A) is functional non empty set
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
y is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
x is Element of bound_QC-variables Al
{ (y . b₁) where b₁ is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A) : for b₂ being Element of bound_QC-variables Al holds
( x = b₂ or b₁ . b₂ = a₁ . b₂ ) } is set
ALL { (y . b₁) where b₁ is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A) : for b₂ being Element of bound_QC-variables Al holds
( x = b₂ or b₁ . b₂ = a₁ . b₂ ) } is boolean Element of BOOLEAN
K25((Al,A),BOOLEAN) is set
K24(K25((Al,A),BOOLEAN)) is set
p is Relation-like (Al,A) -defined BOOLEAN -valued Function-like non empty V24((Al,A)) quasi_total boolean-valued Element of K24(K25((Al,A),BOOLEAN))
dom p is set
rng p is set
q is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
J is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
q . J is boolean Element of BOOLEAN
{ (y . b₁) where b₁ is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A) : for b₂ being Element of bound_QC-variables Al holds
( x = b₂ or b₁ . b₂ = J . b₂ ) } is set
ALL { (y . b₁) where b₁ is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A) : for b₂ being Element of bound_QC-variables Al holds
( x = b₂ or b₁ . b₂ = J . b₂ ) } is boolean Element of BOOLEAN
p is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
q is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
J is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
p . J is boolean Element of BOOLEAN
q . J is boolean Element of BOOLEAN
{ (y . b₁) where b₁ is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A) : for b₂ being Element of bound_QC-variables Al holds
( x = b₂ or b₁ . b₂ = J . b₂ ) } is set
ALL { (y . b₁) where b₁ is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A) : for b₂ being Element of bound_QC-variables Al holds
( x = b₂ or b₁ . b₂ = J . b₂ ) } is boolean Element of BOOLEAN
Al is Relation-like non empty QC-alphabet
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
K24((QC-variables Al)) is set
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((bound_QC-variables Al),A) is functional non empty set
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
x is Element of bound_QC-variables Al
y is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
p is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,x,p) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,x,p) . y is boolean Element of BOOLEAN
{ (p . b₁) where b₁ is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A) : for b₂ being Element of bound_QC-variables Al holds
( x = b₂ or b₁ . b₂ = y . b₂ ) } is set
q is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
p . q is boolean Element of BOOLEAN
ALL { (p . b₁) where b₁ is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A) : for b₂ being Element of bound_QC-variables Al holds
( x = b₂ or b₁ . b₂ = y . b₂ ) } is boolean Element of BOOLEAN
q is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
p . q is boolean Element of BOOLEAN
J is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
p . J is boolean Element of BOOLEAN
Al is Relation-like non empty QC-alphabet
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
K24((QC-variables Al)) is set
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((bound_QC-variables Al),A) is functional non empty set
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
x is Element of bound_QC-variables Al
y is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
p is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,x,p) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,x,p) . y is boolean Element of BOOLEAN
{ (p . b₁) where b₁ is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A) : for b₂ being Element of bound_QC-variables Al holds
( x = b₂ or b₁ . b₂ = y . b₂ ) } is set
ALL { (p . b₁) where b₁ is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A) : for b₂ being Element of bound_QC-variables Al holds
( x = b₂ or b₁ . b₂ = y . b₂ ) } is boolean Element of BOOLEAN
q is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
p . q is boolean Element of BOOLEAN
q is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
p . q is boolean Element of BOOLEAN
q is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
p . q is boolean Element of BOOLEAN
J is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
p . J is boolean Element of BOOLEAN
Al is Relation-like non empty QC-alphabet
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
QC-variables Al is non empty set
K24((QC-variables Al)) is set
x is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((bound_QC-variables Al),A) is functional non empty set
Al is Relation-like non empty QC-alphabet
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
QC-variables Al is non empty set
K24((QC-variables Al)) is set
x is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((bound_QC-variables Al),A) is functional non empty set
y is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like V47(x) FinSequence-like FinSequence of QC-variables Al
p is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
y * p is Relation-like Function-like set
rng p is set
rng (y * p) is set
len y is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
dom p is set
rng y is set
dom (y * p) is set
dom y is V4() V5() V6() V7() V8() V9() V47(x) Element of K24(NAT)
Seg x is V4() V5() V6() V7() V8() V9() Element of K24(NAT)
q is Relation-like NAT -defined A -valued Function-like FinSequence-like FinSequence of A
len q is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
len y is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
dom p is set
rng y is set
dom y is V4() V5() V6() V7() V8() V9() V47(x) Element of K24(NAT)
dom q is V4() V5() V6() V7() V8() V9() Element of K24(NAT)
J is ext-real ordinal natural V40() V45() set
q . J is set
y . J is set
p . (y . J) is set
dom q is V4() V5() V6() V7() V8() V9() Element of K24(NAT)
dom y is V4() V5() V6() V7() V8() V9() V47(x) Element of K24(NAT)
J is set
y . J is set
J is set
q . J is set
y . J is set
p . (y . J) is set
s is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
Al is Relation-like non empty QC-alphabet
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
QC-variables Al is non empty set
K24((QC-variables Al)) is set
x is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
A is non empty set
relations_on A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((bound_QC-variables Al),A) is functional non empty set
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
y is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like V47(x) FinSequence-like FinSequence of QC-variables Al
p is Element of relations_on A
q is set
J is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
(Al,A,x,y,J) is Relation-like NAT -defined A -valued Function-like FinSequence-like FinSequence of A
K25((Al,A),BOOLEAN) is set
K24(K25((Al,A),BOOLEAN)) is set
q is Relation-like (Al,A) -defined BOOLEAN -valued Function-like non empty V24((Al,A)) quasi_total boolean-valued Element of K24(K25((Al,A),BOOLEAN))
dom q is set
rng q is set
J is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
s is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
(Al,A,x,y,s) is Relation-like NAT -defined A -valued Function-like FinSequence-like FinSequence of A
J . s is boolean Element of BOOLEAN
v is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
(Al,A,x,y,v) is Relation-like NAT -defined A -valued Function-like FinSequence-like FinSequence of A
q is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
J is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
s is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
q . s is boolean Element of BOOLEAN
J . s is boolean Element of BOOLEAN
(Al,A,x,y,s) is Relation-like NAT -defined A -valued Function-like FinSequence-like FinSequence of A
(Al,A,x,y,s) is Relation-like NAT -defined A -valued Function-like FinSequence-like FinSequence of A
(Al,A,x,y,s) is Relation-like NAT -defined A -valued Function-like FinSequence-like FinSequence of A
Al is Relation-like non empty QC-alphabet
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
QC-WFF Al is non empty set
K24((QC-WFF Al)) is set
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
QC-variables Al is non empty set
K24((QC-variables Al)) is set
Funcs ((bound_QC-variables Al),A) is functional non empty set
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
K25((CQC-WFF Al),(Funcs ((Al,A),BOOLEAN))) is set
K24(K25((CQC-WFF Al),(Funcs ((Al,A),BOOLEAN)))) is set
x is Relation-like CQC-WFF Al -defined Funcs ((Al,A),BOOLEAN) -valued Function-like non empty V24( CQC-WFF Al) quasi_total Element of K24(K25((CQC-WFF Al),(Funcs ((Al,A),BOOLEAN))))
y is Element of CQC-WFF Al
x . y is Relation-like Function-like set
x . y is Relation-like Function-like Element of Funcs ((Al,A),BOOLEAN)
Al is Relation-like non empty QC-alphabet
QC-pred_symbols Al is non empty set
A is non empty set
relations_on A is non empty set
K25((QC-pred_symbols Al),(relations_on A)) is set
K24(K25((QC-pred_symbols Al),(relations_on A))) is set
empty_rel A is Element of relations_on A
(QC-pred_symbols Al) --> (empty_rel A) is Relation-like QC-pred_symbols Al -defined relations_on A -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total Element of K24(K25((QC-pred_symbols Al),(relations_on A)))
x is Relation-like QC-pred_symbols Al -defined relations_on A -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total Element of K24(K25((QC-pred_symbols Al),(relations_on A)))
y is Element of QC-pred_symbols Al
x . y is Element of relations_on A
the_arity_of y is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
p is Element of relations_on A
the_arity_of p is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
Al is Relation-like non empty QC-alphabet
QC-pred_symbols Al is non empty set
A is non empty set
relations_on A is non empty set
x is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
x -ary_QC-pred_symbols Al is non empty Element of K24((QC-pred_symbols Al))
K24((QC-pred_symbols Al)) is set
y is Relation-like QC-pred_symbols Al -defined relations_on A -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total (Al,A)
p is Element of x -ary_QC-pred_symbols Al
y . p is set
Al is Relation-like non empty QC-alphabet
QC-pred_symbols Al is non empty set
A is non empty set
relations_on A is non empty set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
QC-variables Al is non empty set
K24((QC-variables Al)) is set
Funcs ((bound_QC-variables Al),A) is functional non empty set
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
K25((CQC-WFF Al),(Funcs ((Al,A),BOOLEAN))) is set
K24(K25((CQC-WFF Al),(Funcs ((Al,A),BOOLEAN)))) is set
y is Element of CQC-WFF Al
VERUM Al is Element of CQC-WFF Al
(Al,A) --> TRUE is Relation-like (Al,A) -defined BOOLEAN -valued Function-like non empty V24((Al,A)) quasi_total boolean-valued Element of K24(K25((Al,A),BOOLEAN))
K25((Al,A),BOOLEAN) is set
K24(K25((Al,A),BOOLEAN)) is set
x is Relation-like QC-pred_symbols Al -defined relations_on A -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total (Al,A)
In (((Al,A) --> TRUE),(Funcs ((Al,A),BOOLEAN))) is Relation-like Function-like Element of Funcs ((Al,A),BOOLEAN)
J is Relation-like CQC-WFF Al -defined Funcs ((Al,A),BOOLEAN) -valued Function-like non empty V24( CQC-WFF Al) quasi_total Element of K24(K25((CQC-WFF Al),(Funcs ((Al,A),BOOLEAN))))
(Al,A,J,(VERUM Al)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,J,y) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
s is Element of CQC-WFF Al
'not' s is Element of CQC-WFF Al
(Al,A,J,('not' s)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,J,s) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
'not' (Al,A,J,s) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like non empty V24((Al,A)) quasi_total boolean-valued Element of K24(K25((Al,A),BOOLEAN))
v is Element of CQC-WFF Al
s '&' v is Element of CQC-WFF Al
(Al,A,J,(s '&' v)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,J,v) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,J,s) '&' (Al,A,J,v) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like non empty V24((Al,A)) quasi_total boolean-valued Element of K24(K25((Al,A),BOOLEAN))
w is Element of bound_QC-variables Al
All (w,s) is Element of CQC-WFF Al
(Al,A,J,(All (w,s))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,w,(Al,A,J,s)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
l3 is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
l3 -ary_QC-pred_symbols Al is non empty Element of K24((QC-pred_symbols Al))
K24((QC-pred_symbols Al)) is set
x is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like V47(l3) FinSequence-like FinSequence of QC-variables Al
y is Element of l3 -ary_QC-pred_symbols Al
y ! x is Element of CQC-WFF Al
(Al,A,J,(y ! x)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,l3,x,y) is Element of relations_on A
(Al,A,l3,x,(Al,A,l3,x,y)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
In (('not' (Al,A,J,s)),(Funcs ((Al,A),BOOLEAN))) is Relation-like Function-like Element of Funcs ((Al,A),BOOLEAN)
In (((Al,A,J,s) '&' (Al,A,J,v)),(Funcs ((Al,A),BOOLEAN))) is Relation-like Function-like Element of Funcs ((Al,A),BOOLEAN)
In ((Al,A,w,(Al,A,J,s)),(Funcs ((Al,A),BOOLEAN))) is Relation-like Function-like Element of Funcs ((Al,A),BOOLEAN)
In (((Al,A) --> TRUE),(Funcs ((Al,A),BOOLEAN))) is Relation-like Function-like Element of Funcs ((Al,A),BOOLEAN)
J is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
s is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
v is Relation-like CQC-WFF Al -defined Funcs ((Al,A),BOOLEAN) -valued Function-like non empty V24( CQC-WFF Al) quasi_total Element of K24(K25((CQC-WFF Al),(Funcs ((Al,A),BOOLEAN))))
(Al,A,v,y) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,v,(VERUM Al)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
y is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
y -ary_QC-pred_symbols Al is non empty Element of K24((QC-pred_symbols Al))
K24((QC-pred_symbols Al)) is set
q is Element of y -ary_QC-pred_symbols Al
p is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like V47(y) FinSequence-like FinSequence of QC-variables Al
q ! p is Element of CQC-WFF Al
(Al,A,v,(q ! p)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,y,x,q) is Element of relations_on A
(Al,A,y,p,(Al,A,y,x,q)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
w is Element of CQC-WFF Al
(Al,A,v,w) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
'not' (Al,A,v,w) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like non empty V24((Al,A)) quasi_total boolean-valued Element of K24(K25((Al,A),BOOLEAN))
'not' w is Element of CQC-WFF Al
(Al,A,v,('not' w)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
In (('not' (Al,A,v,w)),(Funcs ((Al,A),BOOLEAN))) is Relation-like Function-like Element of Funcs ((Al,A),BOOLEAN)
l3 is Element of CQC-WFF Al
(Al,A,v,l3) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,v,w) '&' (Al,A,v,l3) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like non empty V24((Al,A)) quasi_total boolean-valued Element of K24(K25((Al,A),BOOLEAN))
w '&' l3 is Element of CQC-WFF Al
(Al,A,v,(w '&' l3)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
In (((Al,A,v,w) '&' (Al,A,v,l3)),(Funcs ((Al,A),BOOLEAN))) is Relation-like Function-like Element of Funcs ((Al,A),BOOLEAN)
x is Element of bound_QC-variables Al
All (x,w) is Element of CQC-WFF Al
(Al,A,v,(All (x,w))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,x,(Al,A,v,w)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
In ((Al,A,x,(Al,A,v,w)),(Funcs ((Al,A),BOOLEAN))) is Relation-like Function-like Element of Funcs ((Al,A),BOOLEAN)
w is Relation-like CQC-WFF Al -defined Funcs ((Al,A),BOOLEAN) -valued Function-like non empty V24( CQC-WFF Al) quasi_total Element of K24(K25((CQC-WFF Al),(Funcs ((Al,A),BOOLEAN))))
(Al,A,w,y) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,w,(VERUM Al)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
p is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
p -ary_QC-pred_symbols Al is non empty Element of K24((QC-pred_symbols Al))
v is Element of p -ary_QC-pred_symbols Al
q is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like V47(p) FinSequence-like FinSequence of QC-variables Al
v ! q is Element of CQC-WFF Al
(Al,A,w,(v ! q)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,p,x,v) is Element of relations_on A
(Al,A,p,q,(Al,A,p,x,v)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
l3 is Element of CQC-WFF Al
(Al,A,w,l3) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
'not' (Al,A,w,l3) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like non empty V24((Al,A)) quasi_total boolean-valued Element of K24(K25((Al,A),BOOLEAN))
'not' l3 is Element of CQC-WFF Al
(Al,A,w,('not' l3)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
In (('not' (Al,A,w,l3)),(Funcs ((Al,A),BOOLEAN))) is Relation-like Function-like Element of Funcs ((Al,A),BOOLEAN)
x is Element of CQC-WFF Al
(Al,A,w,x) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,w,l3) '&' (Al,A,w,x) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like non empty V24((Al,A)) quasi_total boolean-valued Element of K24(K25((Al,A),BOOLEAN))
l3 '&' x is Element of CQC-WFF Al
(Al,A,w,(l3 '&' x)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
In (((Al,A,w,l3) '&' (Al,A,w,x)),(Funcs ((Al,A),BOOLEAN))) is Relation-like Function-like Element of Funcs ((Al,A),BOOLEAN)
y is Element of bound_QC-variables Al
All (y,l3) is Element of CQC-WFF Al
(Al,A,w,(All (y,l3))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,y,(Al,A,w,l3)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
In ((Al,A,y,(Al,A,w,l3)),(Funcs ((Al,A),BOOLEAN))) is Relation-like Function-like Element of Funcs ((Al,A),BOOLEAN)
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
VERUM Al is Element of CQC-WFF Al
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
QC-variables Al is non empty set
K24((QC-variables Al)) is set
A is Element of CQC-WFF Al
x is non empty set
relations_on x is non empty set
(Al,x) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,x
Funcs ((bound_QC-variables Al),x) is functional non empty set
(Al,x) --> TRUE is Relation-like (Al,x) -defined BOOLEAN -valued Function-like non empty V24((Al,x)) quasi_total boolean-valued Element of K24(K25((Al,x),BOOLEAN))
K25((Al,x),BOOLEAN) is set
K24(K25((Al,x),BOOLEAN)) is set
y is Relation-like QC-pred_symbols Al -defined relations_on x -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total (Al,x)
(Al,x,y,(VERUM Al)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
Funcs ((Al,x),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,x), BOOLEAN
(Al,x,y,A) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
In (((Al,x) --> TRUE),(Funcs ((Al,x),BOOLEAN))) is Relation-like Function-like Element of Funcs ((Al,x),BOOLEAN)
K25((CQC-WFF Al),(Funcs ((Al,x),BOOLEAN))) is set
K24(K25((CQC-WFF Al),(Funcs ((Al,x),BOOLEAN)))) is set
J is Element of CQC-WFF Al
(Al,x,y,J) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
s is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
v is Relation-like CQC-WFF Al -defined Funcs ((Al,x),BOOLEAN) -valued Function-like non empty V24( CQC-WFF Al) quasi_total Element of K24(K25((CQC-WFF Al),(Funcs ((Al,x),BOOLEAN))))
(Al,x,v,J) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
(Al,x,v,(VERUM Al)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
w is Element of CQC-WFF Al
'not' w is Element of CQC-WFF Al
(Al,x,v,('not' w)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
(Al,x,v,w) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
'not' (Al,x,v,w) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like non empty V24((Al,x)) quasi_total boolean-valued Element of K24(K25((Al,x),BOOLEAN))
In (('not' (Al,x,v,w)),(Funcs ((Al,x),BOOLEAN))) is Relation-like Function-like Element of Funcs ((Al,x),BOOLEAN)
l3 is Element of CQC-WFF Al
w '&' l3 is Element of CQC-WFF Al
(Al,x,v,(w '&' l3)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
(Al,x,v,l3) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
(Al,x,v,w) '&' (Al,x,v,l3) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like non empty V24((Al,x)) quasi_total boolean-valued Element of K24(K25((Al,x),BOOLEAN))
In (((Al,x,v,w) '&' (Al,x,v,l3)),(Funcs ((Al,x),BOOLEAN))) is Relation-like Function-like Element of Funcs ((Al,x),BOOLEAN)
x is Element of bound_QC-variables Al
All (x,w) is Element of CQC-WFF Al
(Al,x,v,(All (x,w))) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
(Al,x,x,(Al,x,v,w)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
In ((Al,x,x,(Al,x,v,w)),(Funcs ((Al,x),BOOLEAN))) is Relation-like Function-like Element of Funcs ((Al,x),BOOLEAN)
y is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
y -ary_QC-pred_symbols Al is non empty Element of K24((QC-pred_symbols Al))
K24((QC-pred_symbols Al)) is set
p is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like V47(y) FinSequence-like FinSequence of QC-variables Al
q is Element of y -ary_QC-pred_symbols Al
q ! p is Element of CQC-WFF Al
(Al,x,v,(q ! p)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
(Al,x,y,y,q) is Element of relations_on x
(Al,x,y,p,(Al,x,y,y,q)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
v is Relation-like CQC-WFF Al -defined Funcs ((Al,x),BOOLEAN) -valued Function-like non empty V24( CQC-WFF Al) quasi_total Element of K24(K25((CQC-WFF Al),(Funcs ((Al,x),BOOLEAN))))
(Al,x,v,J) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
(Al,x,v,(VERUM Al)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
w is Element of CQC-WFF Al
'not' w is Element of CQC-WFF Al
(Al,x,v,('not' w)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
(Al,x,v,w) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
'not' (Al,x,v,w) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like non empty V24((Al,x)) quasi_total boolean-valued Element of K24(K25((Al,x),BOOLEAN))
l3 is Element of CQC-WFF Al
w '&' l3 is Element of CQC-WFF Al
(Al,x,v,(w '&' l3)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
(Al,x,v,l3) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
(Al,x,v,w) '&' (Al,x,v,l3) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like non empty V24((Al,x)) quasi_total boolean-valued Element of K24(K25((Al,x),BOOLEAN))
x is Element of bound_QC-variables Al
All (x,w) is Element of CQC-WFF Al
(Al,x,v,(All (x,w))) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
(Al,x,x,(Al,x,v,w)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
y is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
y -ary_QC-pred_symbols Al is non empty Element of K24((QC-pred_symbols Al))
K24((QC-pred_symbols Al)) is set
p is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like V47(y) FinSequence-like FinSequence of QC-variables Al
q is Element of y -ary_QC-pred_symbols Al
q ! p is Element of CQC-WFF Al
(Al,x,v,(q ! p)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
(Al,x,y,y,q) is Element of relations_on x
(Al,x,y,p,(Al,x,y,y,q)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
In (('not' (Al,x,v,w)),(Funcs ((Al,x),BOOLEAN))) is Relation-like Function-like Element of Funcs ((Al,x),BOOLEAN)
In (((Al,x,v,w) '&' (Al,x,v,l3)),(Funcs ((Al,x),BOOLEAN))) is Relation-like Function-like Element of Funcs ((Al,x),BOOLEAN)
In ((Al,x,x,(Al,x,v,w)),(Funcs ((Al,x),BOOLEAN))) is Relation-like Function-like Element of Funcs ((Al,x),BOOLEAN)
J is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
J -ary_QC-pred_symbols Al is non empty Element of K24((QC-pred_symbols Al))
K24((QC-pred_symbols Al)) is set
v is Element of J -ary_QC-pred_symbols Al
s is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like V47(J) FinSequence-like FinSequence of QC-variables Al
v ! s is Element of CQC-WFF Al
(Al,x,y,(v ! s)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
(Al,x,J,y,v) is Element of relations_on x
(Al,x,J,s,(Al,x,J,y,v)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
J is Element of CQC-WFF Al
(Al,x,y,J) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
'not' H₅(J) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like non empty V24((Al,x)) quasi_total boolean-valued Element of K24(K25((Al,x),BOOLEAN))
'not' J is Element of CQC-WFF Al
(Al,x,y,('not' J)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
In (('not' H₅(J)),(Funcs ((Al,x),BOOLEAN))) is Relation-like Function-like Element of Funcs ((Al,x),BOOLEAN)
J is Element of CQC-WFF Al
(Al,x,y,J) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
H₅(A) '&' H₅(J) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like non empty V24((Al,x)) quasi_total boolean-valued Element of K24(K25((Al,x),BOOLEAN))
A '&' J is Element of CQC-WFF Al
(Al,x,y,(A '&' J)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
In ((H₅(A) '&' H₅(J)),(Funcs ((Al,x),BOOLEAN))) is Relation-like Function-like Element of Funcs ((Al,x),BOOLEAN)
J is Element of bound_QC-variables Al
All (J,A) is Element of CQC-WFF Al
(Al,x,y,(All (J,A))) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
(Al,x,J,(Al,x,y,A)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
(Al,x,J,H₅(A)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
In ((Al,x,J,H₅(A)),(Funcs ((Al,x),BOOLEAN))) is Relation-like Function-like Element of Funcs ((Al,x),BOOLEAN)
Al is Relation-like non empty QC-alphabet
QC-pred_symbols Al is non empty set
A is non empty set
relations_on A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
QC-variables Al is non empty set
K24((QC-variables Al)) is set
Funcs ((bound_QC-variables Al),A) is functional non empty set
x is Relation-like QC-pred_symbols Al -defined relations_on A -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total (Al,A)
VERUM Al is Element of CQC-WFF Al
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
(Al,A,x,(VERUM Al)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
(Al,A) --> TRUE is Relation-like (Al,A) -defined BOOLEAN -valued Function-like non empty V24((Al,A)) quasi_total boolean-valued Element of K24(K25((Al,A),BOOLEAN))
K25((Al,A),BOOLEAN) is set
K24(K25((Al,A),BOOLEAN)) is set
Al is Relation-like non empty QC-alphabet
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
QC-variables Al is non empty set
K24((QC-variables Al)) is set
QC-pred_symbols 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 K24((QC-WFF Al))
K24((QC-WFF Al)) is set
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((bound_QC-variables Al),A) is functional non empty set
relations_on A is non empty set
x is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
y is Relation-like QC-pred_symbols Al -defined relations_on A -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total (Al,A)
(Al,A,y,(VERUM Al)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
(Al,A,y,(VERUM Al)) . x is boolean Element of BOOLEAN
(Al,A) --> TRUE is Relation-like (Al,A) -defined BOOLEAN -valued Function-like non empty V24((Al,A)) quasi_total boolean-valued Element of K24(K25((Al,A),BOOLEAN))
K25((Al,A),BOOLEAN) is set
K24(K25((Al,A),BOOLEAN)) is set
((Al,A) --> TRUE) . x is boolean Element of BOOLEAN
Al is Relation-like non empty QC-alphabet
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
QC-variables Al is non empty set
K24((QC-variables Al)) is set
A is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
QC-pred_symbols Al is non empty set
x is non empty set
relations_on x is non empty set
A -ary_QC-pred_symbols Al is non empty Element of K24((QC-pred_symbols Al))
K24((QC-pred_symbols Al)) is set
(Al,x) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,x
Funcs ((bound_QC-variables Al),x) is functional non empty set
p is Relation-like QC-pred_symbols Al -defined relations_on x -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total (Al,x)
q is Element of A -ary_QC-pred_symbols Al
y is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like V47(A) FinSequence-like FinSequence of QC-variables Al
q ! y is Element of CQC-WFF Al
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
(Al,x,p,(q ! y)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
Funcs ((Al,x),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,x), BOOLEAN
(Al,x,A,p,q) is Element of relations_on x
(Al,x,A,y,(Al,x,A,p,q)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
Al is Relation-like non empty QC-alphabet
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
QC-variables Al is non empty set
K24((QC-variables Al)) is set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
A -ary_QC-pred_symbols Al is non empty Element of K24((QC-pred_symbols Al))
K24((QC-pred_symbols Al)) is set
x is non empty set
(Al,x) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,x
Funcs ((bound_QC-variables Al),x) is functional non empty set
relations_on x is non empty set
y is Relation-like bound_QC-variables Al -defined x -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,x)
p is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like V47(A) FinSequence-like FinSequence of QC-variables Al
(Al,x,A,p,y) is Relation-like NAT -defined x -valued Function-like FinSequence-like FinSequence of x
q is Element of CQC-WFF Al
J is Relation-like QC-pred_symbols Al -defined relations_on x -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total (Al,x)
(Al,x,J,q) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
Funcs ((Al,x),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,x), BOOLEAN
(Al,x,J,q) . y is boolean Element of BOOLEAN
s is Element of A -ary_QC-pred_symbols Al
s ! p is Element of CQC-WFF Al
(Al,x,A,J,s) is Element of relations_on x
v is Element of relations_on x
(Al,x,A,p,(Al,x,A,J,s)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
(Al,x,A,p,(Al,x,A,J,s)) . y is boolean Element of BOOLEAN
Al is Relation-like non empty QC-alphabet
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
QC-variables Al is non empty set
K24((QC-variables Al)) is set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
A -ary_QC-pred_symbols Al is non empty Element of K24((QC-pred_symbols Al))
K24((QC-pred_symbols Al)) is set
x is non empty set
(Al,x) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,x
Funcs ((bound_QC-variables Al),x) is functional non empty set
relations_on x is non empty set
y is Relation-like bound_QC-variables Al -defined x -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,x)
p is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like V47(A) FinSequence-like FinSequence of QC-variables Al
(Al,x,A,p,y) is Relation-like NAT -defined x -valued Function-like FinSequence-like FinSequence of x
q is Element of CQC-WFF Al
J is Relation-like QC-pred_symbols Al -defined relations_on x -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total (Al,x)
(Al,x,J,q) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
Funcs ((Al,x),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,x), BOOLEAN
(Al,x,J,q) . y is boolean Element of BOOLEAN
s is Element of A -ary_QC-pred_symbols Al
s ! p is Element of CQC-WFF Al
(Al,x,A,J,s) is Element of relations_on x
v is Element of relations_on x
(Al,x,A,p,(Al,x,A,J,s)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
(Al,x,A,p,(Al,x,A,J,s)) . y is boolean Element of BOOLEAN
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
relations_on A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
QC-variables Al is non empty set
K24((QC-variables Al)) is set
Funcs ((bound_QC-variables Al),A) is functional non empty set
y is Relation-like QC-pred_symbols Al -defined relations_on A -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total (Al,A)
x is Element of CQC-WFF Al
'not' x is Element of CQC-WFF Al
(Al,A,y,('not' x)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
(Al,A,y,x) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
'not' (Al,A,y,x) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like non empty V24((Al,A)) quasi_total boolean-valued Element of K24(K25((Al,A),BOOLEAN))
K25((Al,A),BOOLEAN) is set
K24(K25((Al,A),BOOLEAN)) is set
Al is Relation-like non empty QC-alphabet
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
QC-variables Al is non empty set
K24((QC-variables Al)) is set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((bound_QC-variables Al),A) is functional non empty set
relations_on A is non empty set
x is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
y is Element of CQC-WFF Al
'not' y is Element of CQC-WFF Al
p is Relation-like QC-pred_symbols Al -defined relations_on A -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total (Al,A)
(Al,A,p,('not' y)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
(Al,A,p,('not' y)) . x is boolean Element of BOOLEAN
(Al,A,p,y) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,p,y) . x is boolean Element of BOOLEAN
'not' ((Al,A,p,y) . x) is boolean Element of BOOLEAN
'not' (Al,A,p,y) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like non empty V24((Al,A)) quasi_total boolean-valued Element of K24(K25((Al,A),BOOLEAN))
K25((Al,A),BOOLEAN) is set
K24(K25((Al,A),BOOLEAN)) is set
('not' (Al,A,p,y)) . x is boolean Element of BOOLEAN
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
relations_on A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
QC-variables Al is non empty set
K24((QC-variables Al)) is set
Funcs ((bound_QC-variables Al),A) is functional non empty set
p is Relation-like QC-pred_symbols Al -defined relations_on A -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total (Al,A)
x is Element of CQC-WFF Al
y is Element of CQC-WFF Al
x '&' y is Element of CQC-WFF Al
(Al,A,p,(x '&' y)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
(Al,A,p,x) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,p,y) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,p,x) '&' (Al,A,p,y) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like non empty V24((Al,A)) quasi_total boolean-valued Element of K24(K25((Al,A),BOOLEAN))
K25((Al,A),BOOLEAN) is set
K24(K25((Al,A),BOOLEAN)) is set
Al is Relation-like non empty QC-alphabet
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
QC-variables Al is non empty set
K24((QC-variables Al)) is set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((bound_QC-variables Al),A) is functional non empty set
relations_on A is non empty set
x is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
y is Element of CQC-WFF Al
p is Element of CQC-WFF Al
y '&' p is Element of CQC-WFF Al
q is Relation-like QC-pred_symbols Al -defined relations_on A -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total (Al,A)
(Al,A,q,(y '&' p)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
(Al,A,q,(y '&' p)) . x is boolean Element of BOOLEAN
(Al,A,q,y) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,q,y) . x is boolean Element of BOOLEAN
(Al,A,q,p) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,q,p) . x is boolean Element of BOOLEAN
((Al,A,q,y) . x) '&' ((Al,A,q,p) . x) is boolean Element of BOOLEAN
(Al,A,q,y) '&' (Al,A,q,p) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like non empty V24((Al,A)) quasi_total boolean-valued Element of K24(K25((Al,A),BOOLEAN))
K25((Al,A),BOOLEAN) is set
K24(K25((Al,A),BOOLEAN)) is set
((Al,A,q,y) '&' (Al,A,q,p)) . x is boolean Element of BOOLEAN
Al is Relation-like non empty QC-alphabet
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
K24((QC-variables Al)) is set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
relations_on A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((bound_QC-variables Al),A) is functional non empty set
p is Relation-like QC-pred_symbols Al -defined relations_on A -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total (Al,A)
x is Element of bound_QC-variables Al
y is Element of CQC-WFF Al
All (x,y) is Element of CQC-WFF Al
(Al,A,p,(All (x,y))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
(Al,A,p,y) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,x,(Al,A,p,y)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Al is Relation-like non empty QC-alphabet
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
QC-variables Al is non empty set
K24((QC-variables Al)) is set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((bound_QC-variables Al),A) is functional non empty set
relations_on A is non empty set
x is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
y is Element of CQC-WFF Al
'not' y is Element of CQC-WFF Al
y '&' ('not' y) is Element of CQC-WFF Al
p is Relation-like QC-pred_symbols Al -defined relations_on A -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total (Al,A)
(Al,A,p,(y '&' ('not' y))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
(Al,A,p,(y '&' ('not' y))) . x is boolean Element of BOOLEAN
(Al,A,p,y) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,p,y) . x is boolean Element of BOOLEAN
'not' ((Al,A,p,y) . x) is boolean Element of BOOLEAN
((Al,A,p,y) . x) '&' ('not' ((Al,A,p,y) . x)) is boolean Element of BOOLEAN
(Al,A,p,('not' y)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,p,('not' y)) . x is boolean Element of BOOLEAN
((Al,A,p,y) . x) '&' ((Al,A,p,('not' y)) . x) is boolean Element of BOOLEAN
Al is Relation-like non empty QC-alphabet
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
QC-variables Al is non empty set
K24((QC-variables Al)) is set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((bound_QC-variables Al),A) is functional non empty set
relations_on A is non empty set
x is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
y is Element of CQC-WFF Al
'not' y is Element of CQC-WFF Al
y '&' ('not' y) is Element of CQC-WFF Al
'not' (y '&' ('not' y)) is Element of CQC-WFF Al
p is Relation-like QC-pred_symbols Al -defined relations_on A -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total (Al,A)
(Al,A,p,('not' (y '&' ('not' y)))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
(Al,A,p,('not' (y '&' ('not' y)))) . x is boolean Element of BOOLEAN
(Al,A,p,(y '&' ('not' y))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,p,(y '&' ('not' y))) . x is boolean Element of BOOLEAN
'not' ((Al,A,p,(y '&' ('not' y))) . x) is boolean Element of BOOLEAN
'not' FALSE is boolean Element of BOOLEAN
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
relations_on A is non empty set
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
QC-variables Al is non empty set
K24((QC-variables Al)) is set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((bound_QC-variables Al),A) is functional non empty set
Al is Relation-like non empty QC-alphabet
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
QC-variables Al is non empty set
K24((QC-variables Al)) is set
QC-pred_symbols Al is non empty set
A is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
A -ary_QC-pred_symbols Al is non empty Element of K24((QC-pred_symbols Al))
K24((QC-pred_symbols Al)) is set
x is non empty set
(Al,x) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,x
Funcs ((bound_QC-variables Al),x) is functional non empty set
relations_on x is non empty set
y is Relation-like bound_QC-variables Al -defined x -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,x)
p is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like V47(A) FinSequence-like FinSequence of QC-variables Al
q is Relation-like QC-pred_symbols Al -defined relations_on x -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total (Al,x)
J is Element of A -ary_QC-pred_symbols Al
J ! p is Element of CQC-WFF Al
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
(Al,x,A,q,J) is Element of relations_on x
(Al,x,A,p,(Al,x,A,q,J)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
Funcs ((Al,x),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,x), BOOLEAN
(Al,x,A,p,(Al,x,A,q,J)) . y is boolean Element of BOOLEAN
(Al,x,q,(J ! p)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
(Al,x,q,(J ! p)) . y is boolean Element of BOOLEAN
Al is Relation-like non empty QC-alphabet
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
QC-variables Al is non empty set
K24((QC-variables Al)) is set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((bound_QC-variables Al),A) is functional non empty set
relations_on A is non empty set
x is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
y is Element of CQC-WFF Al
'not' y is Element of CQC-WFF Al
p is Relation-like QC-pred_symbols Al -defined relations_on A -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total (Al,A)
(Al,A,p,y) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
(Al,A,p,y) . x is boolean Element of BOOLEAN
'not' ((Al,A,p,y) . x) is boolean Element of BOOLEAN
'not' (Al,A,p,y) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like non empty V24((Al,A)) quasi_total boolean-valued Element of K24(K25((Al,A),BOOLEAN))
K25((Al,A),BOOLEAN) is set
K24(K25((Al,A),BOOLEAN)) is set
('not' (Al,A,p,y)) . x is boolean Element of BOOLEAN
(Al,A,p,('not' y)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,p,('not' y)) . x is boolean Element of BOOLEAN
Al is Relation-like non empty QC-alphabet
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
QC-variables Al is non empty set
K24((QC-variables Al)) is set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((bound_QC-variables Al),A) is functional non empty set
relations_on A is non empty set
x is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
y is Element of CQC-WFF Al
p is Element of CQC-WFF Al
y '&' p is Element of CQC-WFF Al
q is Relation-like QC-pred_symbols Al -defined relations_on A -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total (Al,A)
(Al,A,q,y) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
(Al,A,q,y) . x is boolean Element of BOOLEAN
(Al,A,q,p) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,q,p) . x is boolean Element of BOOLEAN
((Al,A,q,y) . x) '&' ((Al,A,q,p) . x) is boolean Element of BOOLEAN
(Al,A,q,y) '&' (Al,A,q,p) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like non empty V24((Al,A)) quasi_total boolean-valued Element of K24(K25((Al,A),BOOLEAN))
K25((Al,A),BOOLEAN) is set
K24(K25((Al,A),BOOLEAN)) is set
((Al,A,q,y) '&' (Al,A,q,p)) . x is boolean Element of BOOLEAN
(Al,A,q,(y '&' p)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,q,(y '&' p)) . x is boolean Element of BOOLEAN
Al is Relation-like non empty QC-alphabet
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
K24((QC-variables Al)) is set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((bound_QC-variables Al),A) is functional non empty set
relations_on A is non empty set
x is Element of bound_QC-variables Al
y is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
p is Element of CQC-WFF Al
All (x,p) is Element of CQC-WFF Al
q is Relation-like QC-pred_symbols Al -defined relations_on A -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total (Al,A)
(Al,A,q,p) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
(Al,A,x,(Al,A,q,p)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,x,(Al,A,q,p)) . y is boolean Element of BOOLEAN
(Al,A,q,(All (x,p))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,q,(All (x,p))) . y is boolean Element of BOOLEAN
Al is Relation-like non empty QC-alphabet
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
K24((QC-variables Al)) is set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((bound_QC-variables Al),A) is functional non empty set
relations_on A is non empty set
x is Element of bound_QC-variables Al
y is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
p is Element of CQC-WFF Al
All (x,p) is Element of CQC-WFF Al
q is Relation-like QC-pred_symbols Al -defined relations_on A -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total (Al,A)
(Al,A,q,p) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
(Al,A,x,(Al,A,q,p)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,x,(Al,A,q,p)) . y is boolean Element of BOOLEAN
J is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
(Al,A,q,p) . J is boolean Element of BOOLEAN
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
relations_on A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
QC-variables Al is non empty set
K24((QC-variables Al)) is set
Funcs ((bound_QC-variables Al),A) is functional non empty set
x is Element of CQC-WFF Al
'not' x is Element of CQC-WFF Al
'not' ('not' x) is Element of CQC-WFF Al
y is Relation-like QC-pred_symbols Al -defined relations_on A -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total (Al,A)
(Al,A,y,('not' ('not' x))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
(Al,A,y,x) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
p is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
(Al,A,y,('not' ('not' x))) . p is boolean Element of BOOLEAN
(Al,A,y,('not' x)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,y,('not' x)) . p is boolean Element of BOOLEAN
'not' ((Al,A,y,('not' x)) . p) is boolean Element of BOOLEAN
(Al,A,y,x) . p is boolean Element of BOOLEAN
'not' ((Al,A,y,x) . p) is boolean Element of BOOLEAN
'not' ('not' ((Al,A,y,x) . p)) is boolean Element of BOOLEAN
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
relations_on A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
QC-variables Al is non empty set
K24((QC-variables Al)) is set
Funcs ((bound_QC-variables Al),A) is functional non empty set
x is Element of CQC-WFF Al
x '&' x is Element of CQC-WFF Al
y is Relation-like QC-pred_symbols Al -defined relations_on A -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total (Al,A)
(Al,A,y,(x '&' x)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
(Al,A,y,x) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
p is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
(Al,A,y,(x '&' x)) . p is boolean Element of BOOLEAN
(Al,A,y,x) . p is boolean Element of BOOLEAN
((Al,A,y,x) . p) '&' ((Al,A,y,x) . p) is boolean Element of BOOLEAN
Al is Relation-like non empty QC-alphabet
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
QC-variables Al is non empty set
K24((QC-variables Al)) is set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((bound_QC-variables Al),A) is functional non empty set
relations_on A is non empty set
x is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
y is Element of CQC-WFF Al
p is Element of CQC-WFF Al
y => p is Element of CQC-WFF Al
q is Relation-like QC-pred_symbols Al -defined relations_on A -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total (Al,A)
(Al,A,q,y) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
(Al,A,q,y) . x is boolean Element of BOOLEAN
(Al,A,q,p) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,q,p) . x is boolean Element of BOOLEAN
(Al,A,q,(y => p)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,q,(y => p)) . x is boolean Element of BOOLEAN
'not' p is Element of CQC-WFF Al
y '&' ('not' p) is Element of CQC-WFF Al
'not' (y '&' ('not' p)) is Element of CQC-WFF Al
(Al,A,q,('not' (y '&' ('not' p)))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,q,('not' (y '&' ('not' p)))) . x is boolean Element of BOOLEAN
(Al,A,q,(y '&' ('not' p))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,q,(y '&' ('not' p))) . x is boolean Element of BOOLEAN
'not' ((Al,A,q,(y '&' ('not' p))) . x) is boolean Element of BOOLEAN
(Al,A,q,('not' p)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,q,('not' p)) . x is boolean Element of BOOLEAN
((Al,A,q,y) . x) '&' ((Al,A,q,('not' p)) . x) is boolean Element of BOOLEAN
'not' ((Al,A,q,p) . x) is boolean Element of BOOLEAN
((Al,A,q,y) . x) '&' ('not' ((Al,A,q,p) . x)) is boolean Element of BOOLEAN
Al is Relation-like non empty QC-alphabet
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
QC-variables Al is non empty set
K24((QC-variables Al)) is set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((bound_QC-variables Al),A) is functional non empty set
relations_on A is non empty set
x is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
y is Element of CQC-WFF Al
p is Element of CQC-WFF Al
y => p is Element of CQC-WFF Al
q is Relation-like QC-pred_symbols Al -defined relations_on A -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total (Al,A)
(Al,A,q,y) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
(Al,A,q,y) . x is boolean Element of BOOLEAN
(Al,A,q,p) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,q,p) . x is boolean Element of BOOLEAN
Al is Relation-like non empty QC-alphabet
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
K24((QC-variables Al)) is set
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((bound_QC-variables Al),A) is functional non empty set
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
x is Element of bound_QC-variables Al
y is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
p is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,x,p) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,x,p) . y is boolean Element of BOOLEAN
p . y is boolean Element of BOOLEAN
q is Element of bound_QC-variables Al
y . q is Element of A
Al is Relation-like non empty QC-alphabet
QC-pred_symbols Al is non empty set
A is non empty set
relations_on A is non empty set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
Al is boolean Element of BOOLEAN
A is boolean Element of BOOLEAN
'not' A is boolean Element of BOOLEAN
Al '&' ('not' A) is boolean Element of BOOLEAN
'not' (Al '&' ('not' A)) is boolean Element of BOOLEAN
x is boolean Element of BOOLEAN
A '&' x is boolean Element of BOOLEAN
'not' (A '&' x) is boolean Element of BOOLEAN
Al '&' x is boolean Element of BOOLEAN
('not' (A '&' x)) '&' (Al '&' x) is boolean Element of BOOLEAN
('not' (Al '&' ('not' A))) '&' (('not' (A '&' x)) '&' (Al '&' x)) is boolean Element of BOOLEAN
'not' (('not' (Al '&' ('not' A))) '&' (('not' (A '&' x)) '&' (Al '&' x))) is boolean Element of BOOLEAN
Al is Relation-like non empty QC-alphabet
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
K24((QC-variables Al)) is set
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((bound_QC-variables Al),A) is functional non empty set
x is Element of bound_QC-variables Al
p is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
q is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
y is Element of bound_QC-variables Al
q . y is Element of A
J is set
p . J is set
s is Element of bound_QC-variables Al
K25((bound_QC-variables Al),A) is set
K24(K25((bound_QC-variables Al),A)) is set
J is Relation-like bound_QC-variables Al -defined A -valued Function-like non empty V24( bound_QC-variables Al) quasi_total Element of K24(K25((bound_QC-variables Al),A))
dom J is set
rng J is set
s is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
s . x is Element of A
v is Element of bound_QC-variables Al
s . v is Element of A
p . v is Element of A
w is Element of bound_QC-variables Al
v is Element of bound_QC-variables Al
s . v is Element of A
p . v is Element of A
Al is Relation-like non empty QC-alphabet
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
K24((QC-variables Al)) is set
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((bound_QC-variables Al),A) is functional non empty set
x is Element of bound_QC-variables Al
p is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
q is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
y is Element of bound_QC-variables Al
q . y is Element of A
Al is Relation-like non empty QC-alphabet
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
K24((QC-variables Al)) is set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
relations_on A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((bound_QC-variables Al),A) is functional non empty set
x is Element of bound_QC-variables Al
y is Element of CQC-WFF Al
still_not-bound_in y is Element of K24((bound_QC-variables Al))
K24((bound_QC-variables Al)) is set
p is Relation-like QC-pred_symbols Al -defined relations_on A -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total (Al,A)
(Al,A,p,y) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
v is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
v -ary_QC-pred_symbols Al is non empty Element of K24((QC-pred_symbols Al))
K24((QC-pred_symbols Al)) is set
VERUM Al is Element of CQC-WFF Al
still_not-bound_in (VERUM Al) is Element of K24((bound_QC-variables Al))
(Al,A,p,(VERUM Al)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
x is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
(Al,A,p,(VERUM Al)) . x is boolean Element of BOOLEAN
y is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
(Al,A,p,(VERUM Al)) . y is boolean Element of BOOLEAN
w is Relation-like NAT -defined QC-variables Al -valued bound_QC-variables Al -valued Function-like V47(v) FinSequence-like FinSequence of QC-variables Al
rng w is set
l3 is Element of v -ary_QC-pred_symbols Al
l3 ! w is Element of CQC-WFF Al
still_not-bound_in (l3 ! w) is Element of K24((bound_QC-variables Al))
(Al,A,p,(l3 ! w)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
x is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
(Al,A,p,(l3 ! w)) . x is boolean Element of BOOLEAN
y is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
(Al,A,p,(l3 ! w)) . y is boolean Element of BOOLEAN
(Al,A,v,w,x) is Relation-like NAT -defined A -valued Function-like FinSequence-like FinSequence of A
len (Al,A,v,w,x) is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
p is ext-real ordinal natural V40() V45() set
len w is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
dom w is V4() V5() V6() V7() V8() V9() V47(v) Element of K24(NAT)
w . p is set
still_not-bound_in w is Element of K24((bound_QC-variables Al))
v is set
variables_in (w,(bound_QC-variables Al)) is Element of K24((bound_QC-variables Al))
{ (w . b₁) where b₁ is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT : ( 1 <= b₁ & b₁ <= len w & w . b₁ in bound_QC-variables Al ) } is set
q is Element of bound_QC-variables Al
y . q is Element of A
x . q is Element of A
(Al,A,v,w,x) . p is set
x . (w . p) is set
(Al,A,v,w,y) is Relation-like NAT -defined A -valued Function-like FinSequence-like FinSequence of A
(Al,A,v,w,y) . p is set
(Al,A,v,p,l3) is Element of relations_on A
(Al,A,v,w,(Al,A,v,p,l3)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,v,w,(Al,A,v,p,l3)) . x is boolean Element of BOOLEAN
len (Al,A,v,w,y) is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
(Al,A,v,w,(Al,A,v,p,l3)) . y is boolean Element of BOOLEAN
p is ext-real ordinal natural V40() V45() set
w . p is set
still_not-bound_in w is Element of K24((bound_QC-variables Al))
v is set
variables_in (w,(bound_QC-variables Al)) is Element of K24((bound_QC-variables Al))
{ (w . b₁) where b₁ is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT : ( 1 <= b₁ & b₁ <= len w & w . b₁ in bound_QC-variables Al ) } is set
q is Element of bound_QC-variables Al
y . q is Element of A
x . q is Element of A
(Al,A,v,w,x) . p is set
x . (w . p) is set
(Al,A,v,w,y) . p is set
q is Element of CQC-WFF Al
still_not-bound_in q is Element of K24((bound_QC-variables Al))
(Al,A,p,q) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
'not' q is Element of CQC-WFF Al
still_not-bound_in ('not' q) is Element of K24((bound_QC-variables Al))
(Al,A,p,('not' q)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
x is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
(Al,A,p,('not' q)) . x is boolean Element of BOOLEAN
y is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
(Al,A,p,('not' q)) . y is boolean Element of BOOLEAN
(Al,A,p,q) . x is boolean Element of BOOLEAN
'not' ((Al,A,p,q) . x) is boolean Element of BOOLEAN
(Al,A,p,q) . y is boolean Element of BOOLEAN
'not' ((Al,A,p,q) . y) is boolean Element of BOOLEAN
J is Element of CQC-WFF Al
still_not-bound_in J is Element of K24((bound_QC-variables Al))
(Al,A,p,J) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
q '&' J is Element of CQC-WFF Al
still_not-bound_in (q '&' J) is Element of K24((bound_QC-variables Al))
(Al,A,p,(q '&' J)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(still_not-bound_in q) \/ (still_not-bound_in J) is Element of K24((bound_QC-variables Al))
x is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
(Al,A,p,(q '&' J)) . x is boolean Element of BOOLEAN
y is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
(Al,A,p,(q '&' J)) . y is boolean Element of BOOLEAN
(Al,A,p,q) . x is boolean Element of BOOLEAN
(Al,A,p,q) . y is boolean Element of BOOLEAN
(Al,A,p,J) . y is boolean Element of BOOLEAN
((Al,A,p,q) . y) '&' ((Al,A,p,J) . y) is boolean Element of BOOLEAN
(Al,A,p,J) . x is boolean Element of BOOLEAN
((Al,A,p,q) . x) '&' ((Al,A,p,J) . x) is boolean Element of BOOLEAN
s is Element of bound_QC-variables Al
All (s,q) is Element of CQC-WFF Al
still_not-bound_in (All (s,q)) is Element of K24((bound_QC-variables Al))
(Al,A,p,(All (s,q))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
{s} is non empty V22() V47(1) set
(still_not-bound_in q) \ {s} is Element of K24((bound_QC-variables Al))
x is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
(Al,A,p,(All (s,q))) . x is boolean Element of BOOLEAN
y is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
(Al,A,p,(All (s,q))) . y is boolean Element of BOOLEAN
(Al,A,s,(Al,A,p,q)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,s,(Al,A,p,q)) . x is boolean Element of BOOLEAN
p is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
(Al,A,p,q) . p is boolean Element of BOOLEAN
p . s is Element of A
q is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
q . s is Element of A
v is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
ps is Element of bound_QC-variables Al
v . ps is Element of A
p . ps is Element of A
y . ps is Element of A
x . ps is Element of A
(Al,A,p,q) . v is boolean Element of BOOLEAN
ps is Element of bound_QC-variables Al
v . ps is Element of A
y . ps is Element of A
q is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
(Al,A,p,q) . q is boolean Element of BOOLEAN
v is Element of bound_QC-variables Al
p . v is Element of A
y . v is Element of A
x . v is Element of A
v is Element of bound_QC-variables Al
q . v is Element of A
y . v is Element of A
(Al,A,s,(Al,A,p,q)) . y is boolean Element of BOOLEAN
q is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
(Al,A,p,q) . q is boolean Element of BOOLEAN
v is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
(Al,A,p,q) . v is boolean Element of BOOLEAN
p is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
(Al,A,p,q) . p is boolean Element of BOOLEAN
p . s is Element of A
q is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
q . s is Element of A
v is Element of bound_QC-variables Al
q . v is Element of A
p . v is Element of A
x . v is Element of A
y . v is Element of A
(Al,A,p,q) . q is boolean Element of BOOLEAN
q is Element of bound_QC-variables Al
p . q is Element of A
x . q is Element of A
y . q is Element of A
J is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
q is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
(Al,A,p,y) . q is boolean Element of BOOLEAN
(Al,A,p,y) . J is boolean Element of BOOLEAN
Al is Relation-like non empty QC-alphabet
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
K24((QC-variables Al)) is set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((bound_QC-variables Al),A) is functional non empty set
relations_on A is non empty set
x is Element of bound_QC-variables Al
y is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
p is Element of CQC-WFF Al
still_not-bound_in p is Element of K24((bound_QC-variables Al))
K24((bound_QC-variables Al)) is set
q is Relation-like QC-pred_symbols Al -defined relations_on A -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total (Al,A)
J is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
(Al,A,q,p) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
(Al,A,q,p) . y is boolean Element of BOOLEAN
(Al,A,q,p) . J is boolean Element of BOOLEAN
J is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
Al is Relation-like non empty QC-alphabet
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
K24((QC-variables Al)) is set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((bound_QC-variables Al),A) is functional non empty set
relations_on A is non empty set
x is Element of bound_QC-variables Al
y is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
p is Element of CQC-WFF Al
All (x,p) is Element of CQC-WFF Al
q is Relation-like QC-pred_symbols Al -defined relations_on A -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total (Al,A)
(Al,A,q,p) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
J is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
(Al,A,q,p) . J is boolean Element of BOOLEAN
J is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
(Al,A,q,p) . J is boolean Element of BOOLEAN
J is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
s is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
Al is Relation-like non empty QC-alphabet
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
K24((QC-variables Al)) is set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
relations_on A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((bound_QC-variables Al),A) is functional non empty set
x is Element of bound_QC-variables Al
y is Element of bound_QC-variables Al
p is Element of CQC-WFF Al
q is Element of CQC-WFF Al
J is Relation-like QC-pred_symbols Al -defined relations_on A -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total (Al,A)
(Al,A,J,p) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
(Al,A,J,q) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
s is Element of QC-WFF Al
s . x is Element of QC-WFF Al
s . y is Element of QC-WFF Al
v is Element of QC-WFF Al
w is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
w -ary_QC-pred_symbols Al is non empty Element of K24((QC-pred_symbols Al))
K24((QC-pred_symbols Al)) is set
l3 is Element of w -ary_QC-pred_symbols Al
x is Relation-like NAT -defined QC-variables Al -valued Function-like V47(w) FinSequence-like FinSequence of QC-variables Al
l3 ! x is Element of QC-WFF Al
y is Element of bound_QC-variables Al
v . y is Element of QC-WFF Al
p is Element of bound_QC-variables Al
v . p is Element of QC-WFF Al
q is Element of CQC-WFF Al
(Al,A,J,q) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
v is Element of CQC-WFF Al
(Al,A,J,v) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Al a. 0 is Element of free_QC-variables Al
free_QC-variables Al is non empty Element of K24((QC-variables Al))
(Al a. 0) .--> y is Relation-like free_QC-variables Al -defined QC-variables Al -valued Function-like Element of K24(K25((free_QC-variables Al),(QC-variables Al)))
K25((free_QC-variables Al),(QC-variables Al)) is set
K24(K25((free_QC-variables Al),(QC-variables Al))) is set
Subst (x,((Al a. 0) .--> y)) is Relation-like NAT -defined QC-variables Al -valued Function-like V47(w) FinSequence-like FinSequence of QC-variables Al
(Al a. 0) .--> p is Relation-like free_QC-variables Al -defined QC-variables Al -valued Function-like Element of K24(K25((free_QC-variables Al),(QC-variables Al)))
Subst (x,((Al a. 0) .--> p)) is Relation-like NAT -defined QC-variables Al -valued Function-like V47(w) FinSequence-like FinSequence of QC-variables Al
v1 is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
v1 . y is Element of A
v1 . p is Element of A
(Al,A,J,q) . v1 is boolean Element of BOOLEAN
(Al,A,J,v) . v1 is boolean Element of BOOLEAN
l3 ! (Subst (x,((Al a. 0) .--> y))) is Element of QC-WFF Al
len (Subst (x,((Al a. 0) .--> y))) is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
{ ((Subst (x,((Al a. 0) .--> y))) . b₁) where b₁ is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT : ( 1 <= b₁ & b₁ <= len (Subst (x,((Al a. 0) .--> y))) & (Subst (x,((Al a. 0) .--> y))) . b₁ in free_QC-variables Al ) } is set
l3 ! (Subst (x,((Al a. 0) .--> p))) is Element of QC-WFF Al
len (Subst (x,((Al a. 0) .--> p))) is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
{ ((Subst (x,((Al a. 0) .--> p))) . b₁) where b₁ is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT : ( 1 <= b₁ & b₁ <= len (Subst (x,((Al a. 0) .--> p))) & (Subst (x,((Al a. 0) .--> p))) . b₁ in free_QC-variables Al ) } is set
fixed_QC-variables Al is non empty Element of K24((QC-variables Al))
{ ((Subst (x,((Al a. 0) .--> p))) . b₁) where b₁ is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT : ( 1 <= b₁ & b₁ <= len (Subst (x,((Al a. 0) .--> p))) & (Subst (x,((Al a. 0) .--> p))) . b₁ in fixed_QC-variables Al ) } is set
{ ((Subst (x,((Al a. 0) .--> y))) . b₁) where b₁ is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT : ( 1 <= b₁ & b₁ <= len (Subst (x,((Al a. 0) .--> y))) & (Subst (x,((Al a. 0) .--> y))) . b₁ in fixed_QC-variables Al ) } is set
lx is Relation-like NAT -defined QC-variables Al -valued bound_QC-variables Al -valued Function-like V47(w) FinSequence-like FinSequence of QC-variables Al
(Al,A,w,lx,v1) is Relation-like NAT -defined A -valued Function-like FinSequence-like FinSequence of A
len (Al,A,w,lx,v1) is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
i is ext-real ordinal natural V40() V45() set
len x is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
x . i is set
lx . i is set
ly is Relation-like NAT -defined QC-variables Al -valued bound_QC-variables Al -valued Function-like V47(w) FinSequence-like FinSequence of QC-variables Al
ly . i is set
v1 . (lx . i) is set
(Al,A,w,lx,v1) . i is set
(Al,A,w,ly,v1) is Relation-like NAT -defined A -valued Function-like FinSequence-like FinSequence of A
(Al,A,w,ly,v1) . i is set
len (Al,A,w,ly,v1) is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
(Al,A,w,J,l3) is Element of relations_on A
VERUM Al is Element of CQC-WFF Al
w is Element of bound_QC-variables Al
(VERUM Al) . w is Element of QC-WFF Al
l3 is Element of bound_QC-variables Al
(VERUM Al) . l3 is Element of QC-WFF Al
x is Element of CQC-WFF Al
(Al,A,J,x) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
y is Element of CQC-WFF Al
(Al,A,J,y) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
p is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
p . w is Element of A
p . l3 is Element of A
(Al,A,J,x) . p is boolean Element of BOOLEAN
(Al,A,J,y) . p is boolean Element of BOOLEAN
the_argument_of v is Element of QC-WFF Al
w is Element of bound_QC-variables Al
v . w is Element of QC-WFF Al
l3 is Element of bound_QC-variables Al
v . l3 is Element of QC-WFF Al
x is Element of CQC-WFF Al
(Al,A,J,x) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
y is Element of CQC-WFF Al
(Al,A,J,y) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(the_argument_of v) . l3 is Element of QC-WFF Al
'not' ((the_argument_of v) . l3) is Element of QC-WFF Al
(the_argument_of v) . w is Element of QC-WFF Al
'not' ((the_argument_of v) . w) is Element of QC-WFF Al
v is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
v . w is Element of A
v . l3 is Element of A
(Al,A,J,x) . v is boolean Element of BOOLEAN
(Al,A,J,y) . v is boolean Element of BOOLEAN
q is Element of CQC-WFF Al
(Al,A,J,q) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,J,q) . v is boolean Element of BOOLEAN
'not' ((Al,A,J,q) . v) is boolean Element of BOOLEAN
p is Element of CQC-WFF Al
(Al,A,J,p) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,J,p) . v is boolean Element of BOOLEAN
'not' ((Al,A,J,p) . v) is boolean Element of BOOLEAN
the_left_argument_of v is Element of QC-WFF Al
the_right_argument_of v is Element of QC-WFF Al
w is Element of bound_QC-variables Al
v . w is Element of QC-WFF Al
l3 is Element of bound_QC-variables Al
v . l3 is Element of QC-WFF Al
x is Element of CQC-WFF Al
(Al,A,J,x) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
y is Element of CQC-WFF Al
(Al,A,J,y) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(the_left_argument_of v) . w is Element of QC-WFF Al
(the_right_argument_of v) . w is Element of QC-WFF Al
((the_left_argument_of v) . w) '&' ((the_right_argument_of v) . w) is Element of QC-WFF Al
(the_left_argument_of v) . l3 is Element of QC-WFF Al
(the_right_argument_of v) . l3 is Element of QC-WFF Al
((the_left_argument_of v) . l3) '&' ((the_right_argument_of v) . l3) is Element of QC-WFF Al
qs is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
qs . w is Element of A
qs . l3 is Element of A
(Al,A,J,x) . qs is boolean Element of BOOLEAN
(Al,A,J,y) . qs is boolean Element of BOOLEAN
p is Element of CQC-WFF Al
(Al,A,J,p) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,J,p) . qs is boolean Element of BOOLEAN
v is Element of CQC-WFF Al
(Al,A,J,v) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,J,v) . qs is boolean Element of BOOLEAN
ps is Element of CQC-WFF Al
(Al,A,J,ps) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,J,ps) . qs is boolean Element of BOOLEAN
((Al,A,J,v) . qs) '&' ((Al,A,J,ps) . qs) is boolean Element of BOOLEAN
q is Element of CQC-WFF Al
(Al,A,J,q) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,J,q) . qs is boolean Element of BOOLEAN
((Al,A,J,p) . qs) '&' ((Al,A,J,q) . qs) is boolean Element of BOOLEAN
the_scope_of v is Element of QC-WFF Al
w is Element of bound_QC-variables Al
l3 is Element of QC-WFF Al
All (w,l3) is Element of QC-WFF Al
bound_in v is Element of bound_QC-variables Al
x is Element of bound_QC-variables Al
v . x is Element of QC-WFF Al
y is Element of bound_QC-variables Al
v . y is Element of QC-WFF Al
p is Element of CQC-WFF Al
(Al,A,J,p) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
q is Element of CQC-WFF Al
(Al,A,J,q) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
v is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
v . x is Element of A
v . y is Element of A
(Al,A,J,p) . v is boolean Element of BOOLEAN
(Al,A,J,q) . v is boolean Element of BOOLEAN
(the_scope_of v) . x is Element of QC-WFF Al
All ((bound_in v),((the_scope_of v) . x)) is Element of QC-WFF Al
ps is Element of CQC-WFF Al
All ((bound_in v),ps) is Element of CQC-WFF Al
(the_scope_of v) . y is Element of QC-WFF Al
All ((bound_in v),((the_scope_of v) . y)) is Element of QC-WFF Al
qs is Element of CQC-WFF Al
All ((bound_in v),qs) is Element of CQC-WFF Al
(Al,A,J,(All ((bound_in v),qs))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,J,qs) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,(bound_in v),(Al,A,J,qs)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,J,(All ((bound_in v),ps))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,J,ps) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,(bound_in v),(Al,A,J,ps)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
v1 is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
(Al,A,J,qs) . v1 is boolean Element of BOOLEAN
v1 . x is Element of A
v1 . y is Element of A
(Al,A,J,ps) . v1 is boolean Element of BOOLEAN
v1 is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
(Al,A,J,ps) . v1 is boolean Element of BOOLEAN
v1 . x is Element of A
v1 . y is Element of A
(Al,A,J,qs) . v1 is boolean Element of BOOLEAN
v1 is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
(Al,A,J,qs) . v1 is boolean Element of BOOLEAN
All (y,l3) is Element of QC-WFF Al
All (x,l3) is Element of QC-WFF Al
v is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
v . x is Element of A
v . y is Element of A
(Al,A,J,p) . v is boolean Element of BOOLEAN
(Al,A,J,q) . v is boolean Element of BOOLEAN
Al is Relation-like non empty QC-alphabet
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
K24((QC-variables Al)) is set
QC-WFF Al is non empty set
A is Element of bound_QC-variables Al
x is Element of bound_QC-variables Al
y is Element of QC-WFF Al
still_not-bound_in y is Element of K24((bound_QC-variables Al))
K24((bound_QC-variables Al)) is set
y . x is Element of QC-WFF Al
still_not-bound_in (y . x) is Element of K24((bound_QC-variables Al))
p is Element of QC-WFF Al
still_not-bound_in p is Element of K24((bound_QC-variables Al))
p . x is Element of QC-WFF Al
still_not-bound_in (p . x) is Element of K24((bound_QC-variables Al))
the_arguments_of p is Relation-like NAT -defined QC-variables Al -valued Function-like FinSequence-like FinSequence of QC-variables Al
Al a. 0 is Element of free_QC-variables Al
free_QC-variables Al is non empty Element of K24((QC-variables Al))
(Al a. 0) .--> x is Relation-like free_QC-variables Al -defined QC-variables Al -valued Function-like Element of K24(K25((free_QC-variables Al),(QC-variables Al)))
K25((free_QC-variables Al),(QC-variables Al)) is set
K24(K25((free_QC-variables Al),(QC-variables Al))) is set
Subst ((the_arguments_of p),((Al a. 0) .--> x)) is Relation-like NAT -defined QC-variables Al -valued Function-like FinSequence-like FinSequence of QC-variables Al
still_not-bound_in (the_arguments_of p) is Element of K24((bound_QC-variables Al))
variables_in ((the_arguments_of p),(bound_QC-variables Al)) is Element of K24((bound_QC-variables Al))
len (the_arguments_of p) is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
{ ((the_arguments_of p) . b₁) where b₁ is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT : ( 1 <= b₁ & b₁ <= len (the_arguments_of p) & (the_arguments_of p) . b₁ in bound_QC-variables Al ) } is set
len (Subst ((the_arguments_of p),((Al a. 0) .--> x))) is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
{ ((Subst ((the_arguments_of p),((Al a. 0) .--> x))) . b₁) where b₁ is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT : ( 1 <= b₁ & b₁ <= len (Subst ((the_arguments_of p),((Al a. 0) .--> x))) & (Subst ((the_arguments_of p),((Al a. 0) .--> x))) . b₁ in bound_QC-variables Al ) } is set
s is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
(Subst ((the_arguments_of p),((Al a. 0) .--> x))) . s is set
(the_arguments_of p) . s is set
the_pred_symbol_of p is Element of QC-pred_symbols Al
QC-pred_symbols Al is non empty set
(the_pred_symbol_of p) ! (Subst ((the_arguments_of p),((Al a. 0) .--> x))) is Element of QC-WFF Al
the_arguments_of (p . x) is Relation-like NAT -defined QC-variables Al -valued Function-like FinSequence-like FinSequence of QC-variables Al
s is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
s -ary_QC-pred_symbols Al is non empty Element of K24((QC-pred_symbols Al))
K24((QC-pred_symbols Al)) is set
v is Element of s -ary_QC-pred_symbols Al
w is Relation-like NAT -defined QC-variables Al -valued Function-like V47(s) FinSequence-like FinSequence of QC-variables Al
v ! w is Element of QC-WFF Al
l3 is Relation-like NAT -defined QC-variables Al -valued Function-like V47(s) FinSequence-like FinSequence of QC-variables Al
v ! l3 is Element of QC-WFF Al
still_not-bound_in (the_arguments_of (p . x)) is Element of K24((bound_QC-variables Al))
variables_in ((Subst ((the_arguments_of p),((Al a. 0) .--> x))),(bound_QC-variables Al)) is Element of K24((bound_QC-variables Al))
VERUM Al is Element of CQC-WFF Al
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
still_not-bound_in (VERUM Al) is Element of K24((bound_QC-variables Al))
(VERUM Al) . x is Element of QC-WFF Al
still_not-bound_in ((VERUM Al) . x) is Element of K24((bound_QC-variables Al))
the_argument_of p is Element of QC-WFF Al
still_not-bound_in (the_argument_of p) is Element of K24((bound_QC-variables Al))
(the_argument_of p) . x is Element of QC-WFF Al
still_not-bound_in ((the_argument_of p) . x) is Element of K24((bound_QC-variables Al))
'not' ((the_argument_of p) . x) is Element of QC-WFF Al
still_not-bound_in ('not' ((the_argument_of p) . x)) is Element of K24((bound_QC-variables Al))
the_left_argument_of p is Element of QC-WFF Al
still_not-bound_in (the_left_argument_of p) is Element of K24((bound_QC-variables Al))
(the_left_argument_of p) . x is Element of QC-WFF Al
still_not-bound_in ((the_left_argument_of p) . x) is Element of K24((bound_QC-variables Al))
the_right_argument_of p is Element of QC-WFF Al
still_not-bound_in (the_right_argument_of p) is Element of K24((bound_QC-variables Al))
(the_right_argument_of p) . x is Element of QC-WFF Al
still_not-bound_in ((the_right_argument_of p) . x) is Element of K24((bound_QC-variables Al))
(still_not-bound_in (the_left_argument_of p)) \/ (still_not-bound_in (the_right_argument_of p)) is Element of K24((bound_QC-variables Al))
(still_not-bound_in ((the_left_argument_of p) . x)) \/ (still_not-bound_in ((the_right_argument_of p) . x)) is Element of K24((bound_QC-variables Al))
((the_left_argument_of p) . x) '&' ((the_right_argument_of p) . x) is Element of QC-WFF Al
still_not-bound_in (((the_left_argument_of p) . x) '&' ((the_right_argument_of p) . x)) is Element of K24((bound_QC-variables Al))
the_scope_of p is Element of QC-WFF Al
still_not-bound_in (the_scope_of p) is Element of K24((bound_QC-variables Al))
(the_scope_of p) . x is Element of QC-WFF Al
still_not-bound_in ((the_scope_of p) . x) is Element of K24((bound_QC-variables Al))
bound_in p is Element of bound_QC-variables Al
{(bound_in p)} is non empty V22() V47(1) set
(still_not-bound_in (the_scope_of p)) \ {(bound_in p)} is Element of K24((bound_QC-variables Al))
All (A,((the_scope_of p) . x)) is Element of QC-WFF Al
still_not-bound_in (All (A,((the_scope_of p) . x))) is Element of K24((bound_QC-variables Al))
{A} is non empty V22() V47(1) set
(still_not-bound_in ((the_scope_of p) . x)) \ {A} is Element of K24((bound_QC-variables Al))
(still_not-bound_in ((the_scope_of p) . x)) \ {(bound_in p)} is Element of K24((bound_QC-variables Al))
All ((bound_in p),((the_scope_of p) . x)) is Element of QC-WFF Al
still_not-bound_in (All ((bound_in p),((the_scope_of p) . x))) is Element of K24((bound_QC-variables Al))
Al is Relation-like non empty QC-alphabet
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
QC-variables Al is non empty set
K24((QC-variables Al)) is set
QC-pred_symbols 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 K24((QC-WFF Al))
K24((QC-WFF Al)) is set
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((bound_QC-variables Al),A) is functional non empty set
relations_on A is non empty set
x is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
y is Relation-like QC-pred_symbols Al -defined relations_on A -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total (Al,A)
(Al,A) --> TRUE is Relation-like (Al,A) -defined BOOLEAN -valued Function-like non empty V24((Al,A)) quasi_total boolean-valued Element of K24(K25((Al,A),BOOLEAN))
K25((Al,A),BOOLEAN) is set
K24(K25((Al,A),BOOLEAN)) is set
((Al,A) --> TRUE) . x is boolean Element of BOOLEAN
(Al,A,y,(VERUM Al)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
(Al,A,y,(VERUM Al)) . x is boolean Element of BOOLEAN
Al is Relation-like non empty QC-alphabet
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
QC-variables Al is non empty set
K24((QC-variables Al)) is set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((bound_QC-variables Al),A) is functional non empty set
relations_on A is non empty set
x is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
y is Element of CQC-WFF Al
p is Element of CQC-WFF Al
y '&' p is Element of CQC-WFF Al
p '&' y is Element of CQC-WFF Al
(y '&' p) => (p '&' y) is Element of CQC-WFF Al
q is Relation-like QC-pred_symbols Al -defined relations_on A -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total (Al,A)
(Al,A,q,((y '&' p) => (p '&' y))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
(Al,A,q,((y '&' p) => (p '&' y))) . x is boolean Element of BOOLEAN
'not' (p '&' y) is Element of CQC-WFF Al
(y '&' p) '&' ('not' (p '&' y)) is Element of CQC-WFF Al
'not' ((y '&' p) '&' ('not' (p '&' y))) is Element of CQC-WFF Al
(Al,A,q,('not' ((y '&' p) '&' ('not' (p '&' y))))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,q,('not' ((y '&' p) '&' ('not' (p '&' y))))) . x is boolean Element of BOOLEAN
(Al,A,q,((y '&' p) '&' ('not' (p '&' y)))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,q,((y '&' p) '&' ('not' (p '&' y)))) . x is boolean Element of BOOLEAN
'not' ((Al,A,q,((y '&' p) '&' ('not' (p '&' y)))) . x) is boolean Element of BOOLEAN
(Al,A,q,(y '&' p)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,q,(y '&' p)) . x is boolean Element of BOOLEAN
(Al,A,q,('not' (p '&' y))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,q,('not' (p '&' y))) . x is boolean Element of BOOLEAN
((Al,A,q,(y '&' p)) . x) '&' ((Al,A,q,('not' (p '&' y))) . x) is boolean Element of BOOLEAN
'not' (((Al,A,q,(y '&' p)) . x) '&' ((Al,A,q,('not' (p '&' y))) . x)) is boolean Element of BOOLEAN
(Al,A,q,(p '&' y)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,q,(p '&' y)) . x is boolean Element of BOOLEAN
'not' ((Al,A,q,(p '&' y)) . x) is boolean Element of BOOLEAN
((Al,A,q,(y '&' p)) . x) '&' ('not' ((Al,A,q,(p '&' y)) . x)) is boolean Element of BOOLEAN
'not' (((Al,A,q,(y '&' p)) . x) '&' ('not' ((Al,A,q,(p '&' y)) . x))) is boolean Element of BOOLEAN
(Al,A,q,y) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,q,y) . x is boolean Element of BOOLEAN
(Al,A,q,p) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,q,p) . x is boolean Element of BOOLEAN
((Al,A,q,y) . x) '&' ((Al,A,q,p) . x) is boolean Element of BOOLEAN
Al is Relation-like non empty QC-alphabet
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
QC-variables Al is non empty set
K24((QC-variables Al)) is set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((bound_QC-variables Al),A) is functional non empty set
relations_on A is non empty set
x is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
y is Element of CQC-WFF Al
'not' y is Element of CQC-WFF Al
('not' y) => y is Element of CQC-WFF Al
(('not' y) => y) => y is Element of CQC-WFF Al
p is Relation-like QC-pred_symbols Al -defined relations_on A -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total (Al,A)
('not' y) '&' ('not' y) is Element of CQC-WFF Al
'not' (('not' y) '&' ('not' y)) is Element of CQC-WFF Al
(Al,A,p,((('not' y) => y) => y)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
(Al,A,p,((('not' y) => y) => y)) . x is boolean Element of BOOLEAN
('not' (('not' y) '&' ('not' y))) '&' ('not' y) is Element of CQC-WFF Al
'not' (('not' (('not' y) '&' ('not' y))) '&' ('not' y)) is Element of CQC-WFF Al
(Al,A,p,('not' (('not' (('not' y) '&' ('not' y))) '&' ('not' y)))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,p,('not' (('not' (('not' y) '&' ('not' y))) '&' ('not' y)))) . x is boolean Element of BOOLEAN
(Al,A,p,(('not' (('not' y) '&' ('not' y))) '&' ('not' y))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,p,(('not' (('not' y) '&' ('not' y))) '&' ('not' y))) . x is boolean Element of BOOLEAN
'not' ((Al,A,p,(('not' (('not' y) '&' ('not' y))) '&' ('not' y))) . x) is boolean Element of BOOLEAN
(Al,A,p,('not' (('not' y) '&' ('not' y)))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,p,('not' (('not' y) '&' ('not' y)))) . x is boolean Element of BOOLEAN
(Al,A,p,('not' y)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,p,('not' y)) . x is boolean Element of BOOLEAN
((Al,A,p,('not' (('not' y) '&' ('not' y)))) . x) '&' ((Al,A,p,('not' y)) . x) is boolean Element of BOOLEAN
'not' (((Al,A,p,('not' (('not' y) '&' ('not' y)))) . x) '&' ((Al,A,p,('not' y)) . x)) is boolean Element of BOOLEAN
(Al,A,p,(('not' y) '&' ('not' y))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,p,(('not' y) '&' ('not' y))) . x is boolean Element of BOOLEAN
'not' ((Al,A,p,(('not' y) '&' ('not' y))) . x) is boolean Element of BOOLEAN
'not' ((Al,A,p,('not' y)) . x) is boolean Element of BOOLEAN
(Al,A,p,y) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,p,y) . x is boolean Element of BOOLEAN
'not' ((Al,A,p,y) . x) is boolean Element of BOOLEAN
'not' ('not' ((Al,A,p,y) . x)) is boolean Element of BOOLEAN
((Al,A,p,y) . x) '&' ('not' ((Al,A,p,y) . x)) is boolean Element of BOOLEAN
'not' (((Al,A,p,y) . x) '&' ('not' ((Al,A,p,y) . x))) is boolean Element of BOOLEAN
Al is Relation-like non empty QC-alphabet
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
QC-variables Al is non empty set
K24((QC-variables Al)) is set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((bound_QC-variables Al),A) is functional non empty set
relations_on A is non empty set
x is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
y is Element of CQC-WFF Al
'not' y is Element of CQC-WFF Al
p is Element of CQC-WFF Al
('not' y) => p is Element of CQC-WFF Al
y => (('not' y) => p) is Element of CQC-WFF Al
q is Relation-like QC-pred_symbols Al -defined relations_on A -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total (Al,A)
'not' p is Element of CQC-WFF Al
('not' y) '&' ('not' p) is Element of CQC-WFF Al
'not' (('not' y) '&' ('not' p)) is Element of CQC-WFF Al
(Al,A,q,(y => (('not' y) => p))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
(Al,A,q,(y => (('not' y) => p))) . x is boolean Element of BOOLEAN
'not' ('not' (('not' y) '&' ('not' p))) is Element of CQC-WFF Al
y '&' ('not' ('not' (('not' y) '&' ('not' p)))) is Element of CQC-WFF Al
'not' (y '&' ('not' ('not' (('not' y) '&' ('not' p))))) is Element of CQC-WFF Al
(Al,A,q,('not' (y '&' ('not' ('not' (('not' y) '&' ('not' p))))))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,q,('not' (y '&' ('not' ('not' (('not' y) '&' ('not' p))))))) . x is boolean Element of BOOLEAN
(Al,A,q,(y '&' ('not' ('not' (('not' y) '&' ('not' p)))))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,q,(y '&' ('not' ('not' (('not' y) '&' ('not' p)))))) . x is boolean Element of BOOLEAN
'not' ((Al,A,q,(y '&' ('not' ('not' (('not' y) '&' ('not' p)))))) . x) is boolean Element of BOOLEAN
(Al,A,q,y) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,q,y) . x is boolean Element of BOOLEAN
(Al,A,q,('not' ('not' (('not' y) '&' ('not' p))))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,q,('not' ('not' (('not' y) '&' ('not' p))))) . x is boolean Element of BOOLEAN
((Al,A,q,y) . x) '&' ((Al,A,q,('not' ('not' (('not' y) '&' ('not' p))))) . x) is boolean Element of BOOLEAN
'not' (((Al,A,q,y) . x) '&' ((Al,A,q,('not' ('not' (('not' y) '&' ('not' p))))) . x)) is boolean Element of BOOLEAN
(Al,A,q,('not' (('not' y) '&' ('not' p)))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,q,('not' (('not' y) '&' ('not' p)))) . x is boolean Element of BOOLEAN
'not' ((Al,A,q,('not' (('not' y) '&' ('not' p)))) . x) is boolean Element of BOOLEAN
(Al,A,q,(('not' y) '&' ('not' p))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,q,(('not' y) '&' ('not' p))) . x is boolean Element of BOOLEAN
'not' ((Al,A,q,(('not' y) '&' ('not' p))) . x) is boolean Element of BOOLEAN
'not' ('not' ((Al,A,q,(('not' y) '&' ('not' p))) . x)) is boolean Element of BOOLEAN
(Al,A,q,('not' y)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,q,('not' y)) . x is boolean Element of BOOLEAN
(Al,A,q,('not' p)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,q,('not' p)) . x is boolean Element of BOOLEAN
((Al,A,q,('not' y)) . x) '&' ((Al,A,q,('not' p)) . x) is boolean Element of BOOLEAN
'not' ((Al,A,q,y) . x) is boolean Element of BOOLEAN
('not' ((Al,A,q,y) . x)) '&' ((Al,A,q,('not' p)) . x) is boolean Element of BOOLEAN
(Al,A,q,p) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,q,p) . x is boolean Element of BOOLEAN
'not' ((Al,A,q,p) . x) is boolean Element of BOOLEAN
('not' ((Al,A,q,y) . x)) '&' ('not' ((Al,A,q,p) . x)) is boolean Element of BOOLEAN
((Al,A,q,y) . x) '&' ('not' ((Al,A,q,y) . x)) is boolean Element of BOOLEAN
(((Al,A,q,y) . x) '&' ('not' ((Al,A,q,y) . x))) '&' ('not' ((Al,A,q,p) . x)) is boolean Element of BOOLEAN
'not' ((((Al,A,q,y) . x) '&' ('not' ((Al,A,q,y) . x))) '&' ('not' ((Al,A,q,p) . x))) is boolean Element of BOOLEAN
FALSE '&' ('not' ((Al,A,q,p) . x)) is boolean Element of BOOLEAN
'not' (FALSE '&' ('not' ((Al,A,q,p) . x))) is boolean Element of BOOLEAN
Al is Relation-like non empty QC-alphabet
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
QC-variables Al is non empty set
K24((QC-variables Al)) is set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((bound_QC-variables Al),A) is functional non empty set
relations_on A is non empty set
x is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
y is Element of CQC-WFF Al
p is Element of CQC-WFF Al
y => p is Element of CQC-WFF Al
q is Element of CQC-WFF Al
p '&' q is Element of CQC-WFF Al
'not' (p '&' q) is Element of CQC-WFF Al
y '&' q is Element of CQC-WFF Al
'not' (y '&' q) is Element of CQC-WFF Al
('not' (p '&' q)) => ('not' (y '&' q)) is Element of CQC-WFF Al
(y => p) => (('not' (p '&' q)) => ('not' (y '&' q))) is Element of CQC-WFF Al
J is Relation-like QC-pred_symbols Al -defined relations_on A -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total (Al,A)
'not' p is Element of CQC-WFF Al
y '&' ('not' p) is Element of CQC-WFF Al
'not' (y '&' ('not' p)) is Element of CQC-WFF Al
'not' ('not' (y '&' q)) is Element of CQC-WFF Al
('not' (p '&' q)) '&' ('not' ('not' (y '&' q))) is Element of CQC-WFF Al
'not' (('not' (p '&' q)) '&' ('not' ('not' (y '&' q)))) is Element of CQC-WFF Al
(Al,A,J,((y => p) => (('not' (p '&' q)) => ('not' (y '&' q))))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
(Al,A,J,((y => p) => (('not' (p '&' q)) => ('not' (y '&' q))))) . x is boolean Element of BOOLEAN
'not' ('not' (('not' (p '&' q)) '&' ('not' ('not' (y '&' q))))) is Element of CQC-WFF Al
('not' (y '&' ('not' p))) '&' ('not' ('not' (('not' (p '&' q)) '&' ('not' ('not' (y '&' q)))))) is Element of CQC-WFF Al
'not' (('not' (y '&' ('not' p))) '&' ('not' ('not' (('not' (p '&' q)) '&' ('not' ('not' (y '&' q))))))) is Element of CQC-WFF Al
(Al,A,J,('not' (('not' (y '&' ('not' p))) '&' ('not' ('not' (('not' (p '&' q)) '&' ('not' ('not' (y '&' q))))))))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,J,('not' (('not' (y '&' ('not' p))) '&' ('not' ('not' (('not' (p '&' q)) '&' ('not' ('not' (y '&' q))))))))) . x is boolean Element of BOOLEAN
(Al,A,J,(('not' (y '&' ('not' p))) '&' ('not' ('not' (('not' (p '&' q)) '&' ('not' ('not' (y '&' q)))))))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,J,(('not' (y '&' ('not' p))) '&' ('not' ('not' (('not' (p '&' q)) '&' ('not' ('not' (y '&' q)))))))) . x is boolean Element of BOOLEAN
'not' ((Al,A,J,(('not' (y '&' ('not' p))) '&' ('not' ('not' (('not' (p '&' q)) '&' ('not' ('not' (y '&' q)))))))) . x) is boolean Element of BOOLEAN
(Al,A,J,('not' (y '&' ('not' p)))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,J,('not' (y '&' ('not' p)))) . x is boolean Element of BOOLEAN
(Al,A,J,('not' ('not' (('not' (p '&' q)) '&' ('not' ('not' (y '&' q))))))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,J,('not' ('not' (('not' (p '&' q)) '&' ('not' ('not' (y '&' q))))))) . x is boolean Element of BOOLEAN
((Al,A,J,('not' (y '&' ('not' p)))) . x) '&' ((Al,A,J,('not' ('not' (('not' (p '&' q)) '&' ('not' ('not' (y '&' q))))))) . x) is boolean Element of BOOLEAN
'not' (((Al,A,J,('not' (y '&' ('not' p)))) . x) '&' ((Al,A,J,('not' ('not' (('not' (p '&' q)) '&' ('not' ('not' (y '&' q))))))) . x)) is boolean Element of BOOLEAN
(Al,A,J,(y '&' ('not' p))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,J,(y '&' ('not' p))) . x is boolean Element of BOOLEAN
'not' ((Al,A,J,(y '&' ('not' p))) . x) is boolean Element of BOOLEAN
(Al,A,J,y) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,J,y) . x is boolean Element of BOOLEAN
(Al,A,J,('not' p)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,J,('not' p)) . x is boolean Element of BOOLEAN
((Al,A,J,y) . x) '&' ((Al,A,J,('not' p)) . x) is boolean Element of BOOLEAN
'not' (((Al,A,J,y) . x) '&' ((Al,A,J,('not' p)) . x)) is boolean Element of BOOLEAN
(Al,A,J,p) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,J,p) . x is boolean Element of BOOLEAN
'not' ((Al,A,J,p) . x) is boolean Element of BOOLEAN
((Al,A,J,y) . x) '&' ('not' ((Al,A,J,p) . x)) is boolean Element of BOOLEAN
'not' (((Al,A,J,y) . x) '&' ('not' ((Al,A,J,p) . x))) is boolean Element of BOOLEAN
(Al,A,J,('not' (('not' (p '&' q)) '&' ('not' ('not' (y '&' q)))))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,J,('not' (('not' (p '&' q)) '&' ('not' ('not' (y '&' q)))))) . x is boolean Element of BOOLEAN
'not' ((Al,A,J,('not' (('not' (p '&' q)) '&' ('not' ('not' (y '&' q)))))) . x) is boolean Element of BOOLEAN
(Al,A,J,(('not' (p '&' q)) '&' ('not' ('not' (y '&' q))))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,J,(('not' (p '&' q)) '&' ('not' ('not' (y '&' q))))) . x is boolean Element of BOOLEAN
'not' ((Al,A,J,(('not' (p '&' q)) '&' ('not' ('not' (y '&' q))))) . x) is boolean Element of BOOLEAN
'not' ('not' ((Al,A,J,(('not' (p '&' q)) '&' ('not' ('not' (y '&' q))))) . x)) is boolean Element of BOOLEAN
(Al,A,J,('not' (p '&' q))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,J,('not' (p '&' q))) . x is boolean Element of BOOLEAN
(Al,A,J,('not' ('not' (y '&' q)))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,J,('not' ('not' (y '&' q)))) . x is boolean Element of BOOLEAN
((Al,A,J,('not' (p '&' q))) . x) '&' ((Al,A,J,('not' ('not' (y '&' q)))) . x) is boolean Element of BOOLEAN
(Al,A,J,(p '&' q)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,J,(p '&' q)) . x is boolean Element of BOOLEAN
'not' ((Al,A,J,(p '&' q)) . x) is boolean Element of BOOLEAN
('not' ((Al,A,J,(p '&' q)) . x)) '&' ((Al,A,J,('not' ('not' (y '&' q)))) . x) is boolean Element of BOOLEAN
(Al,A,J,('not' (y '&' q))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,J,('not' (y '&' q))) . x is boolean Element of BOOLEAN
'not' ((Al,A,J,('not' (y '&' q))) . x) is boolean Element of BOOLEAN
('not' ((Al,A,J,(p '&' q)) . x)) '&' ('not' ((Al,A,J,('not' (y '&' q))) . x)) is boolean Element of BOOLEAN
(Al,A,J,(y '&' q)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,J,(y '&' q)) . x is boolean Element of BOOLEAN
'not' ((Al,A,J,(y '&' q)) . x) is boolean Element of BOOLEAN
'not' ('not' ((Al,A,J,(y '&' q)) . x)) is boolean Element of BOOLEAN
('not' ((Al,A,J,(p '&' q)) . x)) '&' ('not' ('not' ((Al,A,J,(y '&' q)) . x))) is boolean Element of BOOLEAN
(Al,A,J,q) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,J,q) . x is boolean Element of BOOLEAN
((Al,A,J,p) . x) '&' ((Al,A,J,q) . x) is boolean Element of BOOLEAN
'not' (((Al,A,J,p) . x) '&' ((Al,A,J,q) . x)) is boolean Element of BOOLEAN
('not' (((Al,A,J,p) . x) '&' ((Al,A,J,q) . x))) '&' ((Al,A,J,(y '&' q)) . x) is boolean Element of BOOLEAN
((Al,A,J,y) . x) '&' ((Al,A,J,q) . x) is boolean Element of BOOLEAN
('not' (((Al,A,J,p) . x) '&' ((Al,A,J,q) . x))) '&' (((Al,A,J,y) . x) '&' ((Al,A,J,q) . x)) is boolean Element of BOOLEAN
Al is Relation-like non empty QC-alphabet
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
QC-variables Al is non empty set
K24((QC-variables Al)) is set
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((bound_QC-variables Al),A) is functional non empty set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
relations_on A is non empty set
y is Element of CQC-WFF Al
q is Relation-like QC-pred_symbols Al -defined relations_on A -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total (Al,A)
x is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
p is Element of CQC-WFF Al
y => p is Element of CQC-WFF Al
Al is Relation-like non empty QC-alphabet
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
K24((QC-variables Al)) is set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((bound_QC-variables Al),A) is functional non empty set
relations_on A is non empty set
x is Element of bound_QC-variables Al
y is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
p is Element of CQC-WFF Al
All (x,p) is Element of CQC-WFF Al
(All (x,p)) => p is Element of CQC-WFF Al
q is Relation-like QC-pred_symbols Al -defined relations_on A -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total (Al,A)
(Al,A,q,((All (x,p)) => p)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
(Al,A,q,((All (x,p)) => p)) . y is boolean Element of BOOLEAN
'not' p is Element of CQC-WFF Al
(All (x,p)) '&' ('not' p) is Element of CQC-WFF Al
'not' ((All (x,p)) '&' ('not' p)) is Element of CQC-WFF Al
(Al,A,q,('not' ((All (x,p)) '&' ('not' p)))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,q,('not' ((All (x,p)) '&' ('not' p)))) . y is boolean Element of BOOLEAN
(Al,A,q,((All (x,p)) '&' ('not' p))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,q,((All (x,p)) '&' ('not' p))) . y is boolean Element of BOOLEAN
'not' ((Al,A,q,((All (x,p)) '&' ('not' p))) . y) is boolean Element of BOOLEAN
(Al,A,q,(All (x,p))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,q,(All (x,p))) . y is boolean Element of BOOLEAN
(Al,A,q,('not' p)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,q,('not' p)) . y is boolean Element of BOOLEAN
((Al,A,q,(All (x,p))) . y) '&' ((Al,A,q,('not' p)) . y) is boolean Element of BOOLEAN
'not' (((Al,A,q,(All (x,p))) . y) '&' ((Al,A,q,('not' p)) . y)) is boolean Element of BOOLEAN
(Al,A,q,p) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,q,p) . y is boolean Element of BOOLEAN
'not' ((Al,A,q,p) . y) is boolean Element of BOOLEAN
((Al,A,q,(All (x,p))) . y) '&' ('not' ((Al,A,q,p) . y)) is boolean Element of BOOLEAN
'not' (((Al,A,q,(All (x,p))) . y) '&' ('not' ((Al,A,q,p) . y))) is boolean Element of BOOLEAN
(Al,A,x,(Al,A,q,p)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,x,(Al,A,q,p)) . y is boolean Element of BOOLEAN
Al is Relation-like non empty QC-alphabet
QC-pred_symbols 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 K24((QC-WFF Al))
K24((QC-WFF Al)) is set
A is non empty set
relations_on A is non empty set
x is Relation-like QC-pred_symbols Al -defined relations_on A -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total (Al,A)
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
QC-variables Al is non empty set
K24((QC-variables Al)) is set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((bound_QC-variables Al),A) is functional non empty set
y is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
relations_on A is non empty set
x is Element of CQC-WFF Al
y is Element of CQC-WFF Al
x '&' y is Element of CQC-WFF Al
y '&' x is Element of CQC-WFF Al
(x '&' y) => (y '&' x) is Element of CQC-WFF Al
p is Relation-like QC-pred_symbols Al -defined relations_on A -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total (Al,A)
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
QC-variables Al is non empty set
K24((QC-variables Al)) is set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((bound_QC-variables Al),A) is functional non empty set
q is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
relations_on A is non empty set
x is Element of CQC-WFF Al
'not' x is Element of CQC-WFF Al
('not' x) => x is Element of CQC-WFF Al
(('not' x) => x) => x is Element of CQC-WFF Al
y is Relation-like QC-pred_symbols Al -defined relations_on A -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total (Al,A)
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
QC-variables Al is non empty set
K24((QC-variables Al)) is set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((bound_QC-variables Al),A) is functional non empty set
p is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
relations_on A is non empty set
x is Element of CQC-WFF Al
'not' x is Element of CQC-WFF Al
y is Element of CQC-WFF Al
('not' x) => y is Element of CQC-WFF Al
x => (('not' x) => y) is Element of CQC-WFF Al
p is Relation-like QC-pred_symbols Al -defined relations_on A -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total (Al,A)
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
QC-variables Al is non empty set
K24((QC-variables Al)) is set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((bound_QC-variables Al),A) is functional non empty set
q is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
relations_on A is non empty set
x is Element of CQC-WFF Al
y is Element of CQC-WFF Al
x => y is Element of CQC-WFF Al
p is Element of CQC-WFF Al
y '&' p is Element of CQC-WFF Al
'not' (y '&' p) is Element of CQC-WFF Al
x '&' p is Element of CQC-WFF Al
'not' (x '&' p) is Element of CQC-WFF Al
('not' (y '&' p)) => ('not' (x '&' p)) is Element of CQC-WFF Al
(x => y) => (('not' (y '&' p)) => ('not' (x '&' p))) is Element of CQC-WFF Al
q is Relation-like QC-pred_symbols Al -defined relations_on A -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total (Al,A)
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
QC-variables Al is non empty set
K24((QC-variables Al)) is set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((bound_QC-variables Al),A) is functional non empty set
J is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
relations_on A is non empty set
x is Element of CQC-WFF Al
y is Element of CQC-WFF Al
x => y is Element of CQC-WFF Al
p is Relation-like QC-pred_symbols Al -defined relations_on A -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total (Al,A)
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
QC-variables Al is non empty set
K24((QC-variables Al)) is set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((bound_QC-variables Al),A) is functional non empty set
q is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
Al is Relation-like non empty QC-alphabet
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
K24((QC-variables Al)) is set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
relations_on A is non empty set
x is Element of bound_QC-variables Al
y is Element of CQC-WFF Al
All (x,y) is Element of CQC-WFF Al
(All (x,y)) => y is Element of CQC-WFF Al
p is Relation-like QC-pred_symbols Al -defined relations_on A -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total (Al,A)
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((bound_QC-variables Al),A) is functional non empty set
q is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
Al is Relation-like non empty QC-alphabet
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
K24((QC-variables Al)) is set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
relations_on A is non empty set
x is Element of bound_QC-variables Al
y is Element of CQC-WFF Al
still_not-bound_in y is Element of K24((bound_QC-variables Al))
K24((bound_QC-variables Al)) is set
p is Element of CQC-WFF Al
y => p is Element of CQC-WFF Al
All (x,p) is Element of CQC-WFF Al
y => (All (x,p)) is Element of CQC-WFF Al
q is Relation-like QC-pred_symbols Al -defined relations_on A -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total (Al,A)
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((bound_QC-variables Al),A) is functional non empty set
J is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
s is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
Al is Relation-like non empty QC-alphabet
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of K24((QC-variables Al))
K24((QC-variables Al)) is set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
relations_on A is non empty set
x is Element of bound_QC-variables Al
y is Element of bound_QC-variables Al
p is Element of CQC-WFF Al
q is Element of CQC-WFF Al
J is Relation-like QC-pred_symbols Al -defined relations_on A -valued Function-like non empty V24( QC-pred_symbols Al) quasi_total (Al,A)
s is Element of QC-WFF Al
s . x is Element of QC-WFF Al
s . y is Element of QC-WFF Al
still_not-bound_in s is Element of K24((bound_QC-variables Al))
K24((bound_QC-variables Al)) is set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((bound_QC-variables Al),A) is functional non empty set
v is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
v . y is Element of A
w is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
w . x is Element of A
w . y is Element of A
(Al,A,J,p) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
(Al,A,J,p) . w is boolean Element of BOOLEAN
(Al,A,J,q) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,J,q) . w is boolean Element of BOOLEAN
still_not-bound_in q is Element of K24((bound_QC-variables Al))
(Al,A,J,q) . v is boolean Element of BOOLEAN
v is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A)
(Al,A,J,q) . v is boolean Element of BOOLEAN