:: CQC_THE3 semantic presentation

REAL is V32() V33() V34() V38() set
NAT is V32() V33() V34() V35() V36() V37() V38() Element of K32(REAL)
K32(REAL) is non empty set
NAT is V32() V33() V34() V35() V36() V37() V38() set
K32(NAT) is non empty set
K32(NAT) is non empty set
1 is non empty ext-real positive V26() V27() V32() V33() V34() V35() V36() V37() Element of NAT
0 is ext-real V26() V27() V32() V33() V34() V35() V36() V37() Element of NAT
{} is set
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
K32((CQC-WFF A)) is non empty set
p is Element of CQC-WFF A
q is Element of K32((CQC-WFF A))
Cn q is Element of K32((CQC-WFF A))
A is QC-alphabet
CQC-WFF A is non empty Element of K32((QC-WFF A))
QC-WFF A is non empty set
K32((QC-WFF A)) is non empty set
K32((CQC-WFF A)) is non empty set
p is Element of K32((CQC-WFF A))
q is Element of K32((CQC-WFF A))
Cn q is Element of K32((CQC-WFF A))
Cn p is Element of K32((CQC-WFF A))
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
K32((CQC-WFF A)) is non empty set
p is Element of CQC-WFF A
{p} is Element of K32((CQC-WFF A))
q is Element of CQC-WFF A
h is Element of K32((CQC-WFF A))
Cn h is Element of K32((CQC-WFF A))
Cn {p} is Element of K32((CQC-WFF A))
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
K32((CQC-WFF A)) is non empty set
p is Element of CQC-WFF A
q is Element of K32((CQC-WFF A))
h is Element of K32((CQC-WFF A))
Cn q is Element of K32((CQC-WFF A))
Cn h is Element of K32((CQC-WFF A))
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
p is Element of CQC-WFF A
{p} is Element of K32((CQC-WFF A))
K32((CQC-WFF A)) is non empty set
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
p is Element of CQC-WFF A
q is Element of CQC-WFF A
h is Element of CQC-WFF A
{q} is Element of K32((CQC-WFF A))
K32((CQC-WFF A)) is non empty set
{p} is Element of K32((CQC-WFF A))
A is QC-alphabet
CQC-WFF A is non empty Element of K32((QC-WFF A))
QC-WFF A is non empty set
K32((QC-WFF A)) is non empty set
K32((CQC-WFF A)) is non empty set
A is QC-alphabet
CQC-WFF A is non empty Element of K32((QC-WFF A))
QC-WFF A is non empty set
K32((QC-WFF A)) is non empty set
K32((CQC-WFF A)) is non empty set
p is Element of K32((CQC-WFF A))
Cn p is Element of K32((CQC-WFF A))
q is Element of K32((CQC-WFF A))
h is set
x is Element of CQC-WFF A
h is Element of CQC-WFF A
A is QC-alphabet
CQC-WFF A is non empty Element of K32((QC-WFF A))
QC-WFF A is non empty set
K32((QC-WFF A)) is non empty set
K32((CQC-WFF A)) is non empty set
p is Element of K32((CQC-WFF A))
q is Element of CQC-WFF A
A is QC-alphabet
CQC-WFF A is non empty Element of K32((QC-WFF A))
QC-WFF A is non empty set
K32((QC-WFF A)) is non empty set
K32((CQC-WFF A)) is non empty set
p is Element of K32((CQC-WFF A))
q is Element of K32((CQC-WFF A))
h is Element of K32((CQC-WFF A))
x is Element of CQC-WFF A
Cn q is Element of K32((CQC-WFF A))
Cn p is Element of K32((CQC-WFF A))
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
K32((CQC-WFF A)) is non empty set
p is Element of CQC-WFF A
{p} is Element of K32((CQC-WFF A))
q is Element of K32((CQC-WFF A))
h is Element of CQC-WFF A
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
p is Element of CQC-WFF A
{p} is Element of K32((CQC-WFF A))
K32((CQC-WFF A)) is non empty set
q is Element of CQC-WFF A
{q} is Element of K32((CQC-WFF A))
A is QC-alphabet
CQC-WFF A is non empty Element of K32((QC-WFF A))
QC-WFF A is non empty set
K32((QC-WFF A)) is non empty set
K32((CQC-WFF A)) is non empty set
p is Element of K32((CQC-WFF A))
q is Element of K32((CQC-WFF A))
h is Element of CQC-WFF A
A is QC-alphabet
CQC-WFF A is non empty Element of K32((QC-WFF A))
QC-WFF A is non empty set
K32((QC-WFF A)) is non empty set
K32((CQC-WFF A)) is non empty set
TAUT A is Element of K32((CQC-WFF A))
p is Element of K32((CQC-WFF A))
Cn p is Element of K32((CQC-WFF A))
A is QC-alphabet
CQC-WFF A is non empty Element of K32((QC-WFF A))
QC-WFF A is non empty set
K32((QC-WFF A)) is non empty set
{} (CQC-WFF A) is empty proper V7() V8() V9() V32() V33() V34() V35() V36() V37() V38() Element of K32((CQC-WFF A))
K32((CQC-WFF A)) is non empty set
TAUT A is Element of K32((CQC-WFF A))
A is QC-alphabet
CQC-WFF A is non empty Element of K32((QC-WFF A))
QC-WFF A is non empty set
K32((QC-WFF A)) is non empty set
K32((CQC-WFF A)) is non empty set
A is QC-alphabet
CQC-WFF A is non empty Element of K32((QC-WFF A))
QC-WFF A is non empty set
K32((QC-WFF A)) is non empty set
K32((CQC-WFF A)) is non empty set
{} (CQC-WFF A) is empty proper V7() V8() V9() V32() V33() V34() V35() V36() V37() V38() Element of K32((CQC-WFF A))
p is Element of K32((CQC-WFF A))
q is Element of CQC-WFF A
q is Element of CQC-WFF A
A is QC-alphabet
TAUT A is Element of K32((CQC-WFF A))
CQC-WFF A is non empty Element of K32((QC-WFF A))
QC-WFF A is non empty set
K32((QC-WFF A)) is non empty set
K32((CQC-WFF A)) is non empty set
{} (CQC-WFF A) is empty proper V7() V8() V9() V32() V33() V34() V35() V36() V37() V38() Element of K32((CQC-WFF A))
A is QC-alphabet
CQC-WFF A is non empty Element of K32((QC-WFF A))
QC-WFF A is non empty set
K32((QC-WFF A)) is non empty set
K32((CQC-WFF A)) is non empty set
TAUT A is Element of K32((CQC-WFF A))
p is Element of K32((CQC-WFF A))
q is Element of CQC-WFF A
q is Element of CQC-WFF A
A is QC-alphabet
CQC-WFF A is non empty Element of K32((QC-WFF A))
QC-WFF A is non empty set
K32((QC-WFF A)) is non empty set
K32((CQC-WFF A)) is non empty set
h is Element of K32((CQC-WFF A))
x is Element of CQC-WFF A
y is Element of K32((CQC-WFF A))
y9 is Element of CQC-WFF A
h is Element of K32((CQC-WFF A))
x is Element of K32((CQC-WFF A))
y is Element of CQC-WFF A
y9 is Element of CQC-WFF A
A is QC-alphabet
CQC-WFF A is non empty Element of K32((QC-WFF A))
QC-WFF A is non empty set
K32((QC-WFF A)) is non empty set
K32((CQC-WFF A)) is non empty set
p is Element of K32((CQC-WFF A))
q is Element of K32((CQC-WFF A))
h is Element of CQC-WFF A
{h} is Element of K32((CQC-WFF A))
h is Element of CQC-WFF A
h is Element of CQC-WFF A
A is QC-alphabet
CQC-WFF A is non empty Element of K32((QC-WFF A))
QC-WFF A is non empty set
K32((QC-WFF A)) is non empty set
K32((CQC-WFF A)) is non empty set
p is Element of K32((CQC-WFF A))
q is Element of K32((CQC-WFF A))
h is Element of K32((CQC-WFF A))
A is QC-alphabet
CQC-WFF A is non empty Element of K32((QC-WFF A))
QC-WFF A is non empty set
K32((QC-WFF A)) is non empty set
K32((CQC-WFF A)) is non empty set
p is Element of K32((CQC-WFF A))
Cn p is Element of K32((CQC-WFF A))
q is Element of K32((CQC-WFF A))
Cn q is Element of K32((CQC-WFF A))
A is QC-alphabet
CQC-WFF A is non empty Element of K32((QC-WFF A))
QC-WFF A is non empty set
K32((QC-WFF A)) is non empty set
K32((CQC-WFF A)) is non empty set
p is Element of K32((CQC-WFF A))
Cn p is Element of K32((CQC-WFF A))
q is Element of K32((CQC-WFF A))
p \/ q is Element of K32((CQC-WFF A))
Cn q is Element of K32((CQC-WFF A))
(Cn p) \/ (Cn q) is Element of K32((CQC-WFF A))
A is QC-alphabet
CQC-WFF A is non empty Element of K32((QC-WFF A))
QC-WFF A is non empty set
K32((QC-WFF A)) is non empty set
K32((CQC-WFF A)) is non empty set
p is Element of K32((CQC-WFF A))
Cn p is Element of K32((CQC-WFF A))
q is Element of K32((CQC-WFF A))
Cn q is Element of K32((CQC-WFF A))
(Cn p) \/ (Cn q) is Element of K32((CQC-WFF A))
p \/ q is Element of K32((CQC-WFF A))
Cn (p \/ q) is Element of K32((CQC-WFF A))
A is QC-alphabet
CQC-WFF A is non empty Element of K32((QC-WFF A))
QC-WFF A is non empty set
K32((QC-WFF A)) is non empty set
K32((CQC-WFF A)) is non empty set
p is Element of K32((CQC-WFF A))
Cn p is Element of K32((CQC-WFF A))
q is Element of K32((CQC-WFF A))
p \/ q is Element of K32((CQC-WFF A))
Cn (p \/ q) is Element of K32((CQC-WFF A))
Cn q is Element of K32((CQC-WFF A))
(Cn p) \/ (Cn q) is Element of K32((CQC-WFF A))
Cn ((Cn p) \/ (Cn q)) is Element of K32((CQC-WFF A))
A is QC-alphabet
CQC-WFF A is non empty Element of K32((QC-WFF A))
QC-WFF A is non empty set
K32((QC-WFF A)) is non empty set
K32((CQC-WFF A)) is non empty set
p is Element of K32((CQC-WFF A))
Cn p is Element of K32((CQC-WFF A))
Cn (Cn p) is Element of K32((CQC-WFF A))
A is QC-alphabet
CQC-WFF A is non empty Element of K32((QC-WFF A))
QC-WFF A is non empty set
K32((QC-WFF A)) is non empty set
K32((CQC-WFF A)) is non empty set
p is Element of K32((CQC-WFF A))
Cn p is Element of K32((CQC-WFF A))
q is Element of K32((CQC-WFF A))
p \/ q is Element of K32((CQC-WFF A))
Cn q is Element of K32((CQC-WFF A))
(Cn p) \/ (Cn q) is Element of K32((CQC-WFF A))
Cn (p \/ q) is Element of K32((CQC-WFF A))
Cn ((Cn p) \/ (Cn q)) is Element of K32((CQC-WFF A))
A is QC-alphabet
CQC-WFF A is non empty Element of K32((QC-WFF A))
QC-WFF A is non empty set
K32((QC-WFF A)) is non empty set
K32((CQC-WFF A)) is non empty set
p is Element of K32((CQC-WFF A))
q is Element of K32((CQC-WFF A))
h is Element of K32((CQC-WFF A))
p \/ h is Element of K32((CQC-WFF A))
q \/ h is Element of K32((CQC-WFF A))
Cn p is Element of K32((CQC-WFF A))
Cn q is Element of K32((CQC-WFF A))
Cn (p \/ h) is Element of K32((CQC-WFF A))
Cn h is Element of K32((CQC-WFF A))
(Cn q) \/ (Cn h) is Element of K32((CQC-WFF A))
Cn ((Cn q) \/ (Cn h)) is Element of K32((CQC-WFF A))
Cn (q \/ h) is Element of K32((CQC-WFF A))
A is QC-alphabet
CQC-WFF A is non empty Element of K32((QC-WFF A))
QC-WFF A is non empty set
K32((QC-WFF A)) is non empty set
K32((CQC-WFF A)) is non empty set
p is Element of K32((CQC-WFF A))
q is Element of K32((CQC-WFF A))
h is Element of K32((CQC-WFF A))
p \/ h is Element of K32((CQC-WFF A))
q \/ h is Element of K32((CQC-WFF A))
x is Element of K32((CQC-WFF A))
Cn (p \/ h) is Element of K32((CQC-WFF A))
Cn (q \/ h) is Element of K32((CQC-WFF A))
A is QC-alphabet
CQC-WFF A is non empty Element of K32((QC-WFF A))
QC-WFF A is non empty set
K32((QC-WFF A)) is non empty set
K32((CQC-WFF A)) is non empty set
p is Element of K32((CQC-WFF A))
q is Element of K32((CQC-WFF A))
h is Element of K32((CQC-WFF A))
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
h is Element of CQC-WFF A
x is Element of CQC-WFF A
h is Element of CQC-WFF A
x is Element of CQC-WFF A
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
p is Element of CQC-WFF A
q is Element of CQC-WFF A
h is Element of CQC-WFF A
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
p is Element of CQC-WFF A
{p} is Element of K32((CQC-WFF A))
K32((CQC-WFF A)) is non empty set
q is Element of CQC-WFF A
{q} is Element of K32((CQC-WFF A))
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
K32((CQC-WFF A)) is non empty set
p is Element of CQC-WFF A
q is Element of CQC-WFF A
h is Element of K32((CQC-WFF A))
{p} is Element of K32((CQC-WFF A))
{q} is Element of K32((CQC-WFF A))
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
p is Element of CQC-WFF A
q is Element of CQC-WFF A
{p,q} is Element of K32((CQC-WFF A))
K32((CQC-WFF A)) is non empty set
p '&' q is Element of CQC-WFF A
{(p '&' q)} is Element of K32((CQC-WFF A))
h is Element of CQC-WFF A
x is Element of CQC-WFF A
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
p is Element of CQC-WFF A
q is Element of CQC-WFF A
p '&' q is Element of CQC-WFF A
q '&' p is Element of CQC-WFF A
{q,p} is Element of K32((CQC-WFF A))
K32((CQC-WFF A)) is non empty set
{(q '&' p)} is Element of K32((CQC-WFF A))
{(p '&' q)} is Element of K32((CQC-WFF A))
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
K32((CQC-WFF A)) is non empty set
p is Element of CQC-WFF A
q is Element of CQC-WFF A
p '&' q is Element of CQC-WFF A
h is Element of K32((CQC-WFF A))
{p,q} is Element of K32((CQC-WFF A))
x is Element of CQC-WFF A
{(p '&' q)} is Element of K32((CQC-WFF A))
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
K32((CQC-WFF A)) is non empty set
p is Element of CQC-WFF A
q is Element of CQC-WFF A
p '&' q is Element of CQC-WFF A
h is Element of K32((CQC-WFF A))
{(p '&' q)} is Element of K32((CQC-WFF A))
{p,q} is Element of K32((CQC-WFF A))
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
K32((CQC-WFF A)) is non empty set
x is QC-alphabet
QC-WFF x is non empty set
CQC-WFF x is non empty Element of K32((QC-WFF x))
K32((QC-WFF x)) is non empty set
K32((CQC-WFF x)) is non empty set
h is Element of K32((CQC-WFF A))
p is Element of CQC-WFF A
q is Element of CQC-WFF A
p '&' q is Element of CQC-WFF A
n is Element of K32((CQC-WFF x))
y is Element of CQC-WFF x
y9 is Element of CQC-WFF x
y '&' y9 is Element of CQC-WFF x
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
p is Element of CQC-WFF A
q is Element of CQC-WFF A
h is Element of CQC-WFF A
p '&' h is Element of CQC-WFF A
x is Element of CQC-WFF A
q '&' x is Element of CQC-WFF A
{h} is Element of K32((CQC-WFF A))
K32((CQC-WFF A)) is non empty set
{p,h} is Element of K32((CQC-WFF A))
{(p '&' h)} is Element of K32((CQC-WFF A))
{p} is Element of K32((CQC-WFF A))
{(q '&' x)} is Element of K32((CQC-WFF A))
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
p is Element of CQC-WFF A
q is Element of CQC-WFF A
h is Element of CQC-WFF A
p '&' h is Element of CQC-WFF A
x is Element of CQC-WFF A
q '&' x is Element of CQC-WFF A
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
K32((CQC-WFF A)) is non empty set
QC-variables A is set
bound_QC-variables A is Element of K32((QC-variables A))
K32((QC-variables A)) is non empty set
p is Element of CQC-WFF A
q is Element of K32((CQC-WFF A))
h is Element of bound_QC-variables A
All (h,p) is Element of CQC-WFF A
(All (h,p)) => p is Element of CQC-WFF A
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
QC-variables A is set
bound_QC-variables A is Element of K32((QC-variables A))
K32((QC-variables A)) is non empty set
p is Element of CQC-WFF A
q is Element of bound_QC-variables A
All (q,p) is Element of CQC-WFF A
{(All (q,p))} is Element of K32((CQC-WFF A))
K32((CQC-WFF A)) is non empty set
(All (q,p)) => p is Element of CQC-WFF A
{p} is Element of K32((CQC-WFF A))
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
QC-variables A is set
bound_QC-variables A is Element of K32((QC-variables A))
K32((QC-variables A)) is non empty set
p is Element of CQC-WFF A
q is Element of CQC-WFF A
h is Element of bound_QC-variables A
All (h,p) is Element of CQC-WFF A
x is Element of bound_QC-variables A
All (x,q) is Element of CQC-WFF A
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
p is Element of CQC-WFF A
q is Element of CQC-WFF A
QC-variables A is set
bound_QC-variables A is Element of K32((QC-variables A))
K32((QC-variables A)) is non empty set
h is ext-real V26() V27() V32() V33() V34() V35() V36() V37() Element of NAT
x is V7() Function-like FinSequence-like set
len x is ext-real V26() V27() V32() V33() V34() V35() V36() V37() Element of NAT
x . 1 is set
x . h is set
x is V7() Function-like FinSequence-like set
len x is ext-real V26() V27() V32() V33() V34() V35() V36() V37() Element of NAT
x . 1 is set
x . h is set
y is ext-real V26() V27() V32() V33() V34() V35() V36() V37() Element of NAT
x . y is set
y + 1 is ext-real V26() V27() V32() V33() V34() V35() V36() V37() Element of NAT
x . (y + 1) is set
n is Element of CQC-WFF A
y9 is Element of bound_QC-variables A
All (y9,n) is Element of CQC-WFF A
s is Element of CQC-WFF A
c₁₀ is Element of CQC-WFF A
n is Element of CQC-WFF A
s is Element of CQC-WFF A
x . 0 is set
y is Element of CQC-WFF A
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
p is Element of CQC-WFF A
q is Element of CQC-WFF A
p => q is Element of CQC-WFF A
{p} is Element of K32((CQC-WFF A))
K32((CQC-WFF A)) is non empty set
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
K32((CQC-WFF A)) is non empty set
p is Element of CQC-WFF A
{p} is Element of K32((CQC-WFF A))
q is Element of CQC-WFF A
p => q is Element of CQC-WFF A
h is Element of K32((CQC-WFF A))
h \/ {p} is Element of K32((CQC-WFF A))
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
p is Element of CQC-WFF A
q is Element of CQC-WFF A
p => q is Element of CQC-WFF A
{} (CQC-WFF A) is empty proper V7() V8() V9() V32() V33() V34() V35() V36() V37() V38() Element of K32((CQC-WFF A))
K32((CQC-WFF A)) is non empty set
{p} is Element of K32((CQC-WFF A))
({} (CQC-WFF A)) \/ {p} is Element of K32((CQC-WFF A))
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
K32((CQC-WFF A)) is non empty set
p is Element of CQC-WFF A
q is Element of CQC-WFF A
{q} is Element of K32((CQC-WFF A))
h is Element of CQC-WFF A
p => h is Element of CQC-WFF A
x is Element of K32((CQC-WFF A))
x \/ {q} is Element of K32((CQC-WFF A))
{h} is Element of K32((CQC-WFF A))
{p} is Element of K32((CQC-WFF A))
x \/ {p} is Element of K32((CQC-WFF A))
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
p is Element of CQC-WFF A
'not' p is Element of CQC-WFF A
q is Element of CQC-WFF A
'not' q is Element of CQC-WFF A
p => q is Element of CQC-WFF A
('not' q) => ('not' p) is Element of CQC-WFF A
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
K32((CQC-WFF A)) is non empty set
p is Element of CQC-WFF A
{p} is Element of K32((CQC-WFF A))
'not' p is Element of CQC-WFF A
q is Element of CQC-WFF A
'not' q is Element of CQC-WFF A
{('not' q)} is Element of K32((CQC-WFF A))
h is Element of K32((CQC-WFF A))
h \/ {p} is Element of K32((CQC-WFF A))
h \/ {('not' q)} is Element of K32((CQC-WFF A))
p => q is Element of CQC-WFF A
('not' q) => ('not' p) is Element of CQC-WFF A
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
p is Element of CQC-WFF A
'not' p is Element of CQC-WFF A
q is Element of CQC-WFF A
'not' q is Element of CQC-WFF A
('not' p) => ('not' q) is Element of CQC-WFF A
q => p is Element of CQC-WFF A
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
K32((CQC-WFF A)) is non empty set
p is Element of CQC-WFF A
'not' p is Element of CQC-WFF A
{('not' p)} is Element of K32((CQC-WFF A))
q is Element of CQC-WFF A
'not' q is Element of CQC-WFF A
{q} is Element of K32((CQC-WFF A))
h is Element of K32((CQC-WFF A))
h \/ {('not' p)} is Element of K32((CQC-WFF A))
h \/ {q} is Element of K32((CQC-WFF A))
('not' p) => ('not' q) is Element of CQC-WFF A
q => p is Element of CQC-WFF A
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
p is Element of CQC-WFF A
q is Element of CQC-WFF A
'not' q is Element of CQC-WFF A
'not' p is Element of CQC-WFF A
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
p is Element of CQC-WFF A
'not' p is Element of CQC-WFF A
q is Element of CQC-WFF A
h is Element of CQC-WFF A
'not' h is Element of CQC-WFF A
x is Element of CQC-WFF A
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
p is Element of CQC-WFF A
'not' p is Element of CQC-WFF A
q is Element of CQC-WFF A
h is Element of CQC-WFF A
'not' h is Element of CQC-WFF A
x is Element of CQC-WFF A
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
h is Element of CQC-WFF A
h <=> h is Element of CQC-WFF A
{} (CQC-WFF A) is empty proper V7() V8() V9() V32() V33() V34() V35() V36() V37() V38() Element of K32((CQC-WFF A))
K32((CQC-WFF A)) is non empty set
h => h is valid Element of CQC-WFF A
(h => h) '&' (h => h) is Element of CQC-WFF A
h is Element of CQC-WFF A
x is Element of CQC-WFF A
h <=> x is Element of CQC-WFF A
x <=> h is Element of CQC-WFF A
h => x is Element of CQC-WFF A
x => h is Element of CQC-WFF A
(h => x) '&' (x => h) is Element of CQC-WFF A
{} (CQC-WFF A) is empty proper V7() V8() V9() V32() V33() V34() V35() V36() V37() V38() Element of K32((CQC-WFF A))
K32((CQC-WFF A)) is non empty set
(x => h) '&' (h => x) is Element of CQC-WFF A
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
p is Element of CQC-WFF A
q is Element of CQC-WFF A
p => q is Element of CQC-WFF A
q => p is Element of CQC-WFF A
{} (CQC-WFF A) is empty proper V7() V8() V9() V32() V33() V34() V35() V36() V37() V38() Element of K32((CQC-WFF A))
K32((CQC-WFF A)) is non empty set
(p => q) '&' (q => p) is Element of CQC-WFF A
p <=> q is Element of CQC-WFF A
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
p is Element of CQC-WFF A
q is Element of CQC-WFF A
h is Element of CQC-WFF A
h => q is Element of CQC-WFF A
q => p is Element of CQC-WFF A
h => p is Element of CQC-WFF A
q => h is Element of CQC-WFF A
p => q is Element of CQC-WFF A
p => h is Element of CQC-WFF A
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
p is Element of CQC-WFF A
q is Element of CQC-WFF A
p <=> q is Element of CQC-WFF A
p => q is Element of CQC-WFF A
q => p is Element of CQC-WFF A
(p => q) '&' (q => p) is Element of CQC-WFF A
{} (CQC-WFF A) is empty proper V7() V8() V9() V32() V33() V34() V35() V36() V37() V38() Element of K32((CQC-WFF A))
K32((CQC-WFF A)) is non empty set
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
p is Element of CQC-WFF A
'not' p is Element of CQC-WFF A
q is Element of CQC-WFF A
'not' q is Element of CQC-WFF A
q => p is Element of CQC-WFF A
('not' p) => ('not' q) is Element of CQC-WFF A
p => q is Element of CQC-WFF A
('not' q) => ('not' p) is Element of CQC-WFF A
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
p is Element of CQC-WFF A
'not' p is Element of CQC-WFF A
q is Element of CQC-WFF A
'not' q is Element of CQC-WFF A
('not' q) => ('not' p) is Element of CQC-WFF A
p => q is Element of CQC-WFF A
('not' p) => ('not' q) is Element of CQC-WFF A
q => p is Element of CQC-WFF A
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
h is QC-alphabet
QC-WFF h is non empty set
CQC-WFF h is non empty Element of K32((QC-WFF h))
K32((QC-WFF h)) is non empty set
p is Element of CQC-WFF A
q is Element of CQC-WFF A
'not' p is Element of CQC-WFF A
'not' q is Element of CQC-WFF A
x is Element of CQC-WFF h
'not' x is Element of CQC-WFF h
y is Element of CQC-WFF h
'not' y is Element of CQC-WFF h
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
p is Element of CQC-WFF A
q is Element of CQC-WFF A
h is Element of CQC-WFF A
p '&' h is Element of CQC-WFF A
x is Element of CQC-WFF A
q '&' x is Element of CQC-WFF A
x => h is Element of CQC-WFF A
TAUT A is Element of K32((CQC-WFF A))
K32((CQC-WFF A)) is non empty set
q => p is Element of CQC-WFF A
(q '&' x) => (p '&' h) is Element of CQC-WFF A
h => x is Element of CQC-WFF A
p => q is Element of CQC-WFF A
(p '&' h) => (q '&' x) is Element of CQC-WFF A
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
p is Element of CQC-WFF A
q is Element of CQC-WFF A
h is Element of CQC-WFF A
p => h is Element of CQC-WFF A
x is Element of CQC-WFF A
q => x is Element of CQC-WFF A
'not' h is Element of CQC-WFF A
'not' x is Element of CQC-WFF A
p '&' ('not' h) is Element of CQC-WFF A
q '&' ('not' x) is Element of CQC-WFF A
'not' (p '&' ('not' h)) is Element of CQC-WFF A
'not' (q '&' ('not' x)) is Element of CQC-WFF A
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
p is Element of CQC-WFF A
q is Element of CQC-WFF A
h is Element of CQC-WFF A
p 'or' h is Element of CQC-WFF A
x is Element of CQC-WFF A
q 'or' x is Element of CQC-WFF A
x => h is Element of CQC-WFF A
TAUT A is Element of K32((CQC-WFF A))
K32((CQC-WFF A)) is non empty set
q => p is Element of CQC-WFF A
(q 'or' x) => (p 'or' h) is Element of CQC-WFF A
h => x is Element of CQC-WFF A
p => q is Element of CQC-WFF A
(p 'or' h) => (q 'or' x) is Element of CQC-WFF A
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
p is Element of CQC-WFF A
q is Element of CQC-WFF A
h is Element of CQC-WFF A
p <=> h is Element of CQC-WFF A
x is Element of CQC-WFF A
q <=> x is Element of CQC-WFF A
h => p is Element of CQC-WFF A
x => q is Element of CQC-WFF A
p => h is Element of CQC-WFF A
(p => h) '&' (h => p) is Element of CQC-WFF A
q => x is Element of CQC-WFF A
(q => x) '&' (x => q) is Element of CQC-WFF A
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
QC-variables A is set
bound_QC-variables A is Element of K32((QC-variables A))
K32((QC-variables A)) is non empty set
p is Element of CQC-WFF A
q is Element of CQC-WFF A
h is Element of bound_QC-variables A
All (h,p) is Element of CQC-WFF A
All (h,q) is Element of CQC-WFF A
q => p is Element of CQC-WFF A
All (h,(q => p)) is Element of CQC-WFF A
(All (h,q)) => (All (h,p)) is Element of CQC-WFF A
p => q is Element of CQC-WFF A
All (h,(p => q)) is Element of CQC-WFF A
(All (h,p)) => (All (h,q)) is Element of CQC-WFF A
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
QC-variables A is set
bound_QC-variables A is Element of K32((QC-variables A))
K32((QC-variables A)) is non empty set
p is Element of CQC-WFF A
q is Element of CQC-WFF A
h is Element of bound_QC-variables A
Ex (h,p) is Element of CQC-WFF A
Ex (h,q) is Element of CQC-WFF A
'not' p is Element of CQC-WFF A
'not' q is Element of CQC-WFF A
All (h,('not' p)) is Element of CQC-WFF A
All (h,('not' q)) is Element of CQC-WFF A
'not' (All (h,('not' p))) is Element of CQC-WFF A
'not' (All (h,('not' q))) is Element of CQC-WFF A
A is QC-alphabet
QC-variables A is set
free_QC-variables A is Element of K32((QC-variables A))
K32((QC-variables A)) is non empty set
bound_QC-variables A is Element of K32((QC-variables A))
p is ext-real V26() V27() V32() V33() V34() V35() V36() V37() Element of NAT
q is V7() V10( NAT ) V11( QC-variables A) Function-like V46(p) FinSequence-like FinSequence of QC-variables A
still_not-bound_in q is Element of K32((bound_QC-variables A))
K32((bound_QC-variables A)) is non empty set
h is Element of free_QC-variables A
x is Element of bound_QC-variables A
h .--> x is V7() V10( free_QC-variables A) V11( QC-variables A) Function-like Element of K32(K33((free_QC-variables A),(QC-variables A)))
K33((free_QC-variables A),(QC-variables A)) is V7() set
K32(K33((free_QC-variables A),(QC-variables A))) is non empty set
Subst (q,(h .--> x)) is V7() V10( NAT ) V11( QC-variables A) Function-like V46(p) FinSequence-like FinSequence of QC-variables A
still_not-bound_in (Subst (q,(h .--> x))) is Element of K32((bound_QC-variables A))
len q is ext-real V26() V27() V32() V33() V34() V35() V36() V37() Element of NAT
{ (q . b₁) where b₁ is ext-real V26() V27() V32() V33() V34() V35() V36() V37() Element of NAT : ( 1 <= b₁ & b₁ <= len q & q . b₁ in bound_QC-variables A ) } is set
y is set
len (Subst (q,(h .--> x))) is ext-real V26() V27() V32() V33() V34() V35() V36() V37() Element of NAT
{ ((Subst (q,(h .--> x))) . b₁) where b₁ is ext-real V26() V27() V32() V33() V34() V35() V36() V37() Element of NAT : ( 1 <= b₁ & b₁ <= len (Subst (q,(h .--> x))) & (Subst (q,(h .--> x))) . b₁ in bound_QC-variables A ) } is set
y9 is Element of still_not-bound_in q
n is ext-real V26() V27() V32() V33() V34() V35() V36() V37() Element of NAT
q . n is set
(Subst (q,(h .--> x))) . n is set
A is QC-alphabet
QC-variables A is set
free_QC-variables A is Element of K32((QC-variables A))
K32((QC-variables A)) is non empty set
bound_QC-variables A is Element of K32((QC-variables A))
p is ext-real V26() V27() V32() V33() V34() V35() V36() V37() Element of NAT
q is V7() V10( NAT ) V11( QC-variables A) Function-like V46(p) FinSequence-like FinSequence of QC-variables A
still_not-bound_in q is Element of K32((bound_QC-variables A))
K32((bound_QC-variables A)) is non empty set
h is Element of free_QC-variables A
x is Element of bound_QC-variables A
h .--> x is V7() V10( free_QC-variables A) V11( QC-variables A) Function-like Element of K32(K33((free_QC-variables A),(QC-variables A)))
K33((free_QC-variables A),(QC-variables A)) is V7() set
K32(K33((free_QC-variables A),(QC-variables A))) is non empty set
Subst (q,(h .--> x)) is V7() V10( NAT ) V11( QC-variables A) Function-like V46(p) FinSequence-like FinSequence of QC-variables A
still_not-bound_in (Subst (q,(h .--> x))) is Element of K32((bound_QC-variables A))
{x} is set
(still_not-bound_in q) \/ {x} is set
y is set
len q is ext-real V26() V27() V32() V33() V34() V35() V36() V37() Element of NAT
{ (q . b₁) where b₁ is ext-real V26() V27() V32() V33() V34() V35() V36() V37() Element of NAT : ( 1 <= b₁ & b₁ <= len q & q . b₁ in bound_QC-variables A ) } is set
len (Subst (q,(h .--> x))) is ext-real V26() V27() V32() V33() V34() V35() V36() V37() Element of NAT
{ ((Subst (q,(h .--> x))) . b₁) where b₁ is ext-real V26() V27() V32() V33() V34() V35() V36() V37() Element of NAT : ( 1 <= b₁ & b₁ <= len (Subst (q,(h .--> x))) & (Subst (q,(h .--> x))) . b₁ in bound_QC-variables A ) } is set
y9 is Element of still_not-bound_in (Subst (q,(h .--> x)))
n is ext-real V26() V27() V32() V33() V34() V35() V36() V37() Element of NAT
(Subst (q,(h .--> x))) . n is set
q . n is set
q . n is set
q . n is set
A is QC-alphabet
QC-variables A is set
bound_QC-variables A is Element of K32((QC-variables A))
K32((QC-variables A)) is non empty set
QC-WFF A is non empty set
p is Element of bound_QC-variables A
q is Element of QC-WFF A
still_not-bound_in q is Element of K32((bound_QC-variables A))
K32((bound_QC-variables A)) is non empty set
q . p is Element of QC-WFF A
still_not-bound_in (q . p) is Element of K32((bound_QC-variables A))
'not' q is Element of QC-WFF A
still_not-bound_in ('not' q) is Element of K32((bound_QC-variables A))
('not' q) . p is Element of QC-WFF A
still_not-bound_in (('not' q) . p) is Element of K32((bound_QC-variables A))
'not' (q . p) is Element of QC-WFF A
still_not-bound_in ('not' (q . p)) is Element of K32((bound_QC-variables A))
q is Element of QC-WFF A
still_not-bound_in q is Element of K32((bound_QC-variables A))
K32((bound_QC-variables A)) is non empty set
q . p is Element of QC-WFF A
still_not-bound_in (q . p) is Element of K32((bound_QC-variables A))
h is Element of QC-WFF A
still_not-bound_in h is Element of K32((bound_QC-variables A))
h . p is Element of QC-WFF A
still_not-bound_in (h . p) is Element of K32((bound_QC-variables A))
q '&' h is Element of QC-WFF A
still_not-bound_in (q '&' h) is Element of K32((bound_QC-variables A))
(q '&' h) . p is Element of QC-WFF A
still_not-bound_in ((q '&' h) . p) is Element of K32((bound_QC-variables A))
(q . p) '&' (h . p) is Element of QC-WFF A
still_not-bound_in ((q . p) '&' (h . p)) is Element of K32((bound_QC-variables A))
(still_not-bound_in (q . p)) \/ (still_not-bound_in (h . p)) is Element of K32((bound_QC-variables A))
(still_not-bound_in q) \/ (still_not-bound_in h) is Element of K32((bound_QC-variables A))
q is Element of bound_QC-variables A
h is Element of QC-WFF A
still_not-bound_in h is Element of K32((bound_QC-variables A))
K32((bound_QC-variables A)) is non empty set
h . p is Element of QC-WFF A
still_not-bound_in (h . p) is Element of K32((bound_QC-variables A))
All (q,h) is Element of QC-WFF A
still_not-bound_in (All (q,h)) is Element of K32((bound_QC-variables A))
(All (q,h)) . p is Element of QC-WFF A
still_not-bound_in ((All (q,h)) . p) is Element of K32((bound_QC-variables A))
{q} is set
(still_not-bound_in h) \ {q} is Element of K32((bound_QC-variables A))
All (q,(h . p)) is Element of QC-WFF A
still_not-bound_in (All (q,(h . p))) is Element of K32((bound_QC-variables A))
(still_not-bound_in (h . p)) \ {q} is Element of K32((bound_QC-variables A))
QC-pred_symbols A is set
q is ext-real V26() V27() V32() V33() V34() V35() V36() V37() Element of NAT
q -ary_QC-pred_symbols A is Element of K32((QC-pred_symbols A))
K32((QC-pred_symbols A)) is non empty set
h is Element of q -ary_QC-pred_symbols A
x is V7() V10( NAT ) V11( QC-variables A) Function-like V46(q) FinSequence-like FinSequence of QC-variables A
h ! x is Element of QC-WFF A
still_not-bound_in (h ! x) is Element of K32((bound_QC-variables A))
K32((bound_QC-variables A)) is non empty set
(h ! x) . p is Element of QC-WFF A
still_not-bound_in ((h ! x) . p) is Element of K32((bound_QC-variables A))
A a. 0 is Element of free_QC-variables A
free_QC-variables A is Element of K32((QC-variables A))
(A a. 0) .--> p is V7() V10( free_QC-variables A) V11( QC-variables A) Function-like Element of K32(K33((free_QC-variables A),(QC-variables A)))
K33((free_QC-variables A),(QC-variables A)) is V7() set
K32(K33((free_QC-variables A),(QC-variables A))) is non empty set
Subst (x,((A a. 0) .--> p)) is V7() V10( NAT ) V11( QC-variables A) Function-like V46(q) FinSequence-like FinSequence of QC-variables A
h ! (Subst (x,((A a. 0) .--> p))) is Element of QC-WFF A
still_not-bound_in (h ! (Subst (x,((A a. 0) .--> p)))) is Element of K32((bound_QC-variables A))
still_not-bound_in (Subst (x,((A a. 0) .--> p))) is Element of K32((bound_QC-variables A))
still_not-bound_in x is Element of K32((bound_QC-variables A))
VERUM A is Element of CQC-WFF A
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
still_not-bound_in (VERUM A) is Element of K32((bound_QC-variables A))
K32((bound_QC-variables A)) is non empty set
(VERUM A) . p is Element of QC-WFF A
still_not-bound_in ((VERUM A) . p) is Element of K32((bound_QC-variables A))
A is QC-alphabet
QC-variables A is set
bound_QC-variables A is Element of K32((QC-variables A))
K32((QC-variables A)) is non empty set
QC-WFF A is non empty set
p is Element of bound_QC-variables A
{p} is set
q is Element of QC-WFF A
q . p is Element of QC-WFF A
still_not-bound_in (q . p) is Element of K32((bound_QC-variables A))
K32((bound_QC-variables A)) is non empty set
still_not-bound_in q is Element of K32((bound_QC-variables A))
(still_not-bound_in q) \/ {p} is set
'not' q is Element of QC-WFF A
('not' q) . p is Element of QC-WFF A
still_not-bound_in (('not' q) . p) is Element of K32((bound_QC-variables A))
still_not-bound_in ('not' q) is Element of K32((bound_QC-variables A))
(still_not-bound_in ('not' q)) \/ {p} is set
'not' (q . p) is Element of QC-WFF A
still_not-bound_in ('not' (q . p)) is Element of K32((bound_QC-variables A))
q is Element of QC-WFF A
q . p is Element of QC-WFF A
still_not-bound_in (q . p) is Element of K32((bound_QC-variables A))
K32((bound_QC-variables A)) is non empty set
still_not-bound_in q is Element of K32((bound_QC-variables A))
(still_not-bound_in q) \/ {p} is set
h is Element of QC-WFF A
h . p is Element of QC-WFF A
still_not-bound_in (h . p) is Element of K32((bound_QC-variables A))
still_not-bound_in h is Element of K32((bound_QC-variables A))
(still_not-bound_in h) \/ {p} is set
q '&' h is Element of QC-WFF A
(q '&' h) . p is Element of QC-WFF A
still_not-bound_in ((q '&' h) . p) is Element of K32((bound_QC-variables A))
still_not-bound_in (q '&' h) is Element of K32((bound_QC-variables A))
(still_not-bound_in (q '&' h)) \/ {p} is set
(q . p) '&' (h . p) is Element of QC-WFF A
still_not-bound_in ((q . p) '&' (h . p)) is Element of K32((bound_QC-variables A))
(still_not-bound_in (q . p)) \/ (still_not-bound_in (h . p)) is Element of K32((bound_QC-variables A))
((still_not-bound_in q) \/ {p}) \/ ((still_not-bound_in h) \/ {p}) is set
{p} \/ (still_not-bound_in h) is set
(still_not-bound_in q) \/ ({p} \/ (still_not-bound_in h)) is set
((still_not-bound_in q) \/ ({p} \/ (still_not-bound_in h))) \/ {p} is set
(still_not-bound_in q) \/ (still_not-bound_in h) is Element of K32((bound_QC-variables A))
((still_not-bound_in q) \/ (still_not-bound_in h)) \/ {p} is set
(((still_not-bound_in q) \/ (still_not-bound_in h)) \/ {p}) \/ {p} is set
{p} \/ {p} is set
((still_not-bound_in q) \/ (still_not-bound_in h)) \/ ({p} \/ {p}) is set
q is Element of bound_QC-variables A
h is Element of QC-WFF A
h . p is Element of QC-WFF A
still_not-bound_in (h . p) is Element of K32((bound_QC-variables A))
K32((bound_QC-variables A)) is non empty set
still_not-bound_in h is Element of K32((bound_QC-variables A))
(still_not-bound_in h) \/ {p} is set
All (q,h) is Element of QC-WFF A
(All (q,h)) . p is Element of QC-WFF A
still_not-bound_in ((All (q,h)) . p) is Element of K32((bound_QC-variables A))
still_not-bound_in (All (q,h)) is Element of K32((bound_QC-variables A))
(still_not-bound_in (All (q,h))) \/ {p} is set
(still_not-bound_in h) \ {p} is Element of K32((bound_QC-variables A))
All (p,h) is Element of QC-WFF A
still_not-bound_in (All (p,h)) is Element of K32((bound_QC-variables A))
((still_not-bound_in h) \ {p}) \/ {p} is set
{q} is set
(still_not-bound_in h) \ {q} is Element of K32((bound_QC-variables A))
((still_not-bound_in h) \ {q}) \/ {p} is set
((still_not-bound_in h) \/ {p}) \ {q} is Element of K32(((still_not-bound_in h) \/ {p}))
K32(((still_not-bound_in h) \/ {p})) is non empty set
All (q,(h . p)) is Element of QC-WFF A
still_not-bound_in (All (q,(h . p))) is Element of K32((bound_QC-variables A))
(still_not-bound_in (h . p)) \ {q} is Element of K32((bound_QC-variables A))
QC-pred_symbols A is set
q is ext-real V26() V27() V32() V33() V34() V35() V36() V37() Element of NAT
q -ary_QC-pred_symbols A is Element of K32((QC-pred_symbols A))
K32((QC-pred_symbols A)) is non empty set
h is Element of q -ary_QC-pred_symbols A
x is V7() V10( NAT ) V11( QC-variables A) Function-like V46(q) FinSequence-like FinSequence of QC-variables A
h ! x is Element of QC-WFF A
(h ! x) . p is Element of QC-WFF A
still_not-bound_in ((h ! x) . p) is Element of K32((bound_QC-variables A))
K32((bound_QC-variables A)) is non empty set
still_not-bound_in (h ! x) is Element of K32((bound_QC-variables A))
(still_not-bound_in (h ! x)) \/ {p} is set
A a. 0 is Element of free_QC-variables A
free_QC-variables A is Element of K32((QC-variables A))
(A a. 0) .--> p is V7() V10( free_QC-variables A) V11( QC-variables A) Function-like Element of K32(K33((free_QC-variables A),(QC-variables A)))
K33((free_QC-variables A),(QC-variables A)) is V7() set
K32(K33((free_QC-variables A),(QC-variables A))) is non empty set
Subst (x,((A a. 0) .--> p)) is V7() V10( NAT ) V11( QC-variables A) Function-like V46(q) FinSequence-like FinSequence of QC-variables A
h ! (Subst (x,((A a. 0) .--> p))) is Element of QC-WFF A
still_not-bound_in (h ! (Subst (x,((A a. 0) .--> p)))) is Element of K32((bound_QC-variables A))
still_not-bound_in (Subst (x,((A a. 0) .--> p))) is Element of K32((bound_QC-variables A))
still_not-bound_in x is Element of K32((bound_QC-variables A))
(still_not-bound_in x) \/ {p} is set
VERUM A is Element of CQC-WFF A
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
still_not-bound_in (VERUM A) is Element of K32((bound_QC-variables A))
K32((bound_QC-variables A)) is non empty set
(VERUM A) . p is Element of QC-WFF A
still_not-bound_in ((VERUM A) . p) is Element of K32((bound_QC-variables A))
(still_not-bound_in (VERUM A)) \/ {p} is set
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
QC-variables A is set
bound_QC-variables A is Element of K32((QC-variables A))
K32((QC-variables A)) is non empty set
p is Element of CQC-WFF A
still_not-bound_in p is Element of K32((bound_QC-variables A))
K32((bound_QC-variables A)) is non empty set
q is Element of QC-WFF A
still_not-bound_in q is Element of K32((bound_QC-variables A))
h is Element of bound_QC-variables A
q . h is Element of QC-WFF A
x is Element of bound_QC-variables A
{h} is set
(still_not-bound_in q) \/ {h} is set
A is QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of K32((QC-WFF A))
K32((QC-WFF A)) is non empty set
QC-variables A is set
bound_QC-variables A is Element of K32((QC-variables A))
K32((QC-variables A)) is non empty set
p is Element of CQC-WFF A
q is Element of CQC-WFF A
h is Element of QC-WFF A
still_not-bound_in h is Element of K32((bound_QC-variables A))
K32((bound_QC-variables A)) is non empty set
x is Element of bound_QC-variables A
h . x is Element of QC-WFF A
All (x,p) is Element of CQC-WFF A
y is Element of bound_QC-variables A
h . y is Element of QC-WFF A
All (y,q) is Element of CQC-WFF A
still_not-bound_in q is Element of K32((bound_QC-variables A))
(All (y,q)) => (All (x,p)) is Element of CQC-WFF A
still_not-bound_in p is Element of K32((bound_QC-variables A))
(All (x,p)) => (All (y,q)) is Element of CQC-WFF A