:: 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

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

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

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

len (Subst (q,(h .--> x))) is ext-real V26() V27() V32() V33() V34() V35() V36() V37() Element of NAT

{ ((Subst (q,(h .--> x))) . b

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