:: CQC_THE2 semantic presentation

REAL is set

NAT is non empty V21() V22() V23() Element of bool REAL

bool REAL is set

NAT is non empty V21() V22() V23() set

bool NAT is set

bool NAT is set

Proof_Step_Kinds is set

9 is non empty ext-real V20() V21() V22() V23() V27() Element of NAT

{ b

1 is non empty ext-real V20() V21() V22() V23() V27() Element of NAT

0 is empty ext-real V20() V21() V22() V23() V25() V26() V27() Element of NAT

2 is non empty ext-real V20() V21() V22() V23() V27() Element of NAT

3 is non empty ext-real V20() V21() V22() V23() V27() Element of NAT

4 is non empty ext-real V20() V21() V22() V23() V27() Element of NAT

5 is non empty ext-real V20() V21() V22() V23() V27() Element of NAT

6 is non empty ext-real V20() V21() V22() V23() V27() Element of NAT

7 is non empty ext-real V20() V21() V22() V23() V27() Element of NAT

8 is non empty ext-real V20() V21() V22() V23() V27() Element of NAT

{} is empty ext-real V20() V21() V22() V23() V25() V26() V27() set

A is QC-alphabet

QC-WFF A is non empty set

CQC-WFF A is non empty Element of bool (QC-WFF A)

bool (QC-WFF A) is set

X is Element of CQC-WFF A

F is Element of CQC-WFF A

X '&' F is Element of CQC-WFF A

G is Element of CQC-WFF A

F => G is Element of CQC-WFF A

X => (F => G) is Element of CQC-WFF A

(X '&' F) => G is Element of CQC-WFF A

(X => (F => G)) => ((X '&' F) => G) is Element of CQC-WFF A

TAUT A is Element of bool (CQC-WFF A)

bool (CQC-WFF A) is set

{} (CQC-WFF A) is Element of bool (CQC-WFF A)

Cn ({} (CQC-WFF A)) is Element of bool (CQC-WFF A)

A is QC-alphabet

QC-WFF A is non empty set

CQC-WFF A is non empty Element of bool (QC-WFF A)

bool (QC-WFF A) is set

X is Element of CQC-WFF A

F is Element of CQC-WFF A

F '&' X is Element of CQC-WFF A

G is Element of CQC-WFF A

F => G is Element of CQC-WFF A

X => (F => G) is Element of CQC-WFF A

(F '&' X) => G is Element of CQC-WFF A

TAUT A is Element of bool (CQC-WFF A)

bool (CQC-WFF A) is set

{} (CQC-WFF A) is Element of bool (CQC-WFF A)

Cn ({} (CQC-WFF A)) is Element of bool (CQC-WFF A)

X '&' F is Element of CQC-WFF A

(X '&' F) => G is Element of CQC-WFF A

(F '&' X) => (X '&' F) 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 bool (QC-WFF A)

bool (QC-WFF A) is set

X is Element of CQC-WFF A

F is Element of CQC-WFF A

X '&' F is Element of CQC-WFF A

G is Element of CQC-WFF A

(X '&' F) => G is Element of CQC-WFF A

F => G is Element of CQC-WFF A

X => (F => G) is Element of CQC-WFF A

((X '&' F) => G) => (X => (F => G)) is Element of CQC-WFF A

TAUT A is Element of bool (CQC-WFF A)

bool (CQC-WFF A) is set

{} (CQC-WFF A) is Element of bool (CQC-WFF A)

Cn ({} (CQC-WFF A)) is Element of bool (CQC-WFF A)

A is QC-alphabet

QC-WFF A is non empty set

CQC-WFF A is non empty Element of bool (QC-WFF A)

bool (QC-WFF A) is set

X is Element of CQC-WFF A

F is Element of CQC-WFF A

X '&' F is Element of CQC-WFF A

G is Element of CQC-WFF A

(X '&' F) => G is Element of CQC-WFF A

X => G is Element of CQC-WFF A

F => (X => G) is Element of CQC-WFF A

F '&' X is Element of CQC-WFF A

(F '&' X) => (X '&' F) is Element of CQC-WFF A

TAUT A is Element of bool (CQC-WFF A)

bool (CQC-WFF A) is set

{} (CQC-WFF A) is Element of bool (CQC-WFF A)

Cn ({} (CQC-WFF A)) is Element of bool (CQC-WFF A)

(F '&' X) => G 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 bool (QC-WFF A)

bool (QC-WFF A) is set

X is Element of CQC-WFF A

F is Element of CQC-WFF A

X '&' F is Element of CQC-WFF A

(X '&' F) => X is Element of CQC-WFF A

(X '&' F) => F is Element of CQC-WFF A

TAUT A is Element of bool (CQC-WFF A)

bool (CQC-WFF A) is set

{} (CQC-WFF A) is Element of bool (CQC-WFF A)

Cn ({} (CQC-WFF A)) is Element of bool (CQC-WFF A)

A is QC-alphabet

QC-WFF A is non empty set

CQC-WFF A is non empty Element of bool (QC-WFF A)

bool (QC-WFF A) is set

X is Element of CQC-WFF A

F is Element of CQC-WFF A

X '&' F is Element of CQC-WFF A

(X '&' F) => X is Element of CQC-WFF A

(X '&' F) => F 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 bool (QC-WFF A)

bool (QC-WFF A) is set

X is Element of CQC-WFF A

F is Element of CQC-WFF A

X => F is Element of CQC-WFF A

G is Element of CQC-WFF A

X => G is Element of CQC-WFF A

F '&' G is Element of CQC-WFF A

X => (F '&' G) is Element of CQC-WFF A

TAUT A is Element of bool (CQC-WFF A)

bool (CQC-WFF A) is set

{} (CQC-WFF A) is Element of bool (CQC-WFF A)

Cn ({} (CQC-WFF A)) is Element of bool (CQC-WFF A)

A is QC-alphabet

QC-WFF A is non empty set

CQC-WFF A is non empty Element of bool (QC-WFF A)

bool (QC-WFF A) is set

X is Element of CQC-WFF A

F is Element of CQC-WFF A

X => F is Element of CQC-WFF A

G is Element of CQC-WFF A

X 'or' G is Element of CQC-WFF A

f is Element of CQC-WFF A

G => f is Element of CQC-WFF A

F 'or' f is Element of CQC-WFF A

(X 'or' G) => (F 'or' f) is Element of CQC-WFF A

TAUT A is Element of bool (CQC-WFF A)

bool (CQC-WFF A) is set

{} (CQC-WFF A) is Element of bool (CQC-WFF A)

Cn ({} (CQC-WFF A)) is Element of bool (CQC-WFF A)

A is QC-alphabet

QC-WFF A is non empty set

CQC-WFF A is non empty Element of bool (QC-WFF A)

bool (QC-WFF A) is set

X is Element of CQC-WFF A

F is Element of CQC-WFF A

X => F is Element of CQC-WFF A

G is Element of CQC-WFF A

X '&' G is Element of CQC-WFF A

f is Element of CQC-WFF A

G => f is Element of CQC-WFF A

F '&' f is Element of CQC-WFF A

(X '&' G) => (F '&' f) is Element of CQC-WFF A

TAUT A is Element of bool (CQC-WFF A)

bool (CQC-WFF A) is set

{} (CQC-WFF A) is Element of bool (CQC-WFF A)

Cn ({} (CQC-WFF A)) is Element of bool (CQC-WFF A)

A is QC-alphabet

QC-WFF A is non empty set

CQC-WFF A is non empty Element of bool (QC-WFF A)

bool (QC-WFF A) is set

X is Element of CQC-WFF A

F is Element of CQC-WFF A

X 'or' F is Element of CQC-WFF A

X => (X 'or' F) is Element of CQC-WFF A

F 'or' X is Element of CQC-WFF A

X => (F 'or' X) is Element of CQC-WFF A

TAUT A is Element of bool (CQC-WFF A)

bool (CQC-WFF A) is set

{} (CQC-WFF A) is Element of bool (CQC-WFF A)

Cn ({} (CQC-WFF A)) is Element of bool (CQC-WFF A)

A is QC-alphabet

QC-WFF A is non empty set

CQC-WFF A is non empty Element of bool (QC-WFF A)

bool (QC-WFF A) is set

X is Element of CQC-WFF A

F is Element of CQC-WFF A

X => F is Element of CQC-WFF A

G is Element of CQC-WFF A

G => F is Element of CQC-WFF A

X 'or' G is Element of CQC-WFF A

(X 'or' G) => F is Element of CQC-WFF A

TAUT A is Element of bool (CQC-WFF A)

bool (CQC-WFF A) is set

{} (CQC-WFF A) is Element of bool (CQC-WFF A)

Cn ({} (CQC-WFF A)) is Element of bool (CQC-WFF A)

A is QC-alphabet

QC-WFF A is non empty set

CQC-WFF A is non empty Element of bool (QC-WFF A)

bool (QC-WFF A) is set

X is Element of CQC-WFF A

F is Element of CQC-WFF A

X '&' F is Element of CQC-WFF A

TAUT A is Element of bool (CQC-WFF A)

bool (CQC-WFF A) is set

{} (CQC-WFF A) is Element of bool (CQC-WFF A)

Cn ({} (CQC-WFF A)) is Element of bool (CQC-WFF A)

A is QC-alphabet

QC-WFF A is non empty set

CQC-WFF A is non empty Element of bool (QC-WFF A)

bool (QC-WFF A) is set

X is Element of CQC-WFF A

F is Element of CQC-WFF A

X => F is Element of CQC-WFF A

G is Element of CQC-WFF A

G '&' X is Element of CQC-WFF A

G '&' F is Element of CQC-WFF A

(G '&' X) => (G '&' F) is Element of CQC-WFF A

TAUT A is Element of bool (CQC-WFF A)

bool (CQC-WFF A) is set

{} (CQC-WFF A) is Element of bool (CQC-WFF A)

Cn ({} (CQC-WFF A)) is Element of bool (CQC-WFF A)

A is QC-alphabet

QC-WFF A is non empty set

CQC-WFF A is non empty Element of bool (QC-WFF A)

bool (QC-WFF A) is set

X is Element of CQC-WFF A

F is Element of CQC-WFF A

X => F is Element of CQC-WFF A

G is Element of CQC-WFF A

X 'or' G is Element of CQC-WFF A

F 'or' G is Element of CQC-WFF A

(X 'or' G) => (F 'or' G) is Element of CQC-WFF A

TAUT A is Element of bool (CQC-WFF A)

bool (CQC-WFF A) is set

{} (CQC-WFF A) is Element of bool (CQC-WFF A)

Cn ({} (CQC-WFF A)) is Element of bool (CQC-WFF A)

A is QC-alphabet

QC-WFF A is non empty set

CQC-WFF A is non empty Element of bool (QC-WFF A)

bool (QC-WFF A) is set

X is Element of CQC-WFF A

'not' X is Element of CQC-WFF A

F is Element of CQC-WFF A

X 'or' F is Element of CQC-WFF A

('not' X) => F is Element of CQC-WFF A

(X 'or' F) => (('not' X) => F) is Element of CQC-WFF A

TAUT A is Element of bool (CQC-WFF A)

bool (CQC-WFF A) is set

{} (CQC-WFF A) is Element of bool (CQC-WFF A)

Cn ({} (CQC-WFF A)) is Element of bool (CQC-WFF A)

A is QC-alphabet

QC-WFF A is non empty set

CQC-WFF A is non empty Element of bool (QC-WFF A)

bool (QC-WFF A) is set

X is Element of CQC-WFF A

'not' X is Element of CQC-WFF A

F is Element of CQC-WFF A

('not' X) => F is Element of CQC-WFF A

X 'or' F is Element of CQC-WFF A

(('not' X) => F) => (X 'or' F) is Element of CQC-WFF A

'not' ('not' X) is Element of CQC-WFF A

('not' ('not' X)) => X is valid Element of CQC-WFF A

TAUT A is Element of bool (CQC-WFF A)

bool (CQC-WFF A) is set

{} (CQC-WFF A) is Element of bool (CQC-WFF A)

Cn ({} (CQC-WFF A)) is Element of bool (CQC-WFF A)

('not' ('not' X)) 'or' F is Element of CQC-WFF A

(('not' X) => F) => (('not' ('not' X)) 'or' F) is Element of CQC-WFF A

(('not' ('not' X)) 'or' F) => (X 'or' F) 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 bool (QC-WFF A)

bool (QC-WFF A) is set

X is Element of CQC-WFF A

X <=> X is Element of CQC-WFF A

X => X is valid Element of CQC-WFF A

(X => X) '&' (X => 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 bool (QC-WFF A)

bool (QC-WFF A) is set

X is Element of CQC-WFF A

F is Element of CQC-WFF A

X => F is Element of CQC-WFF A

F => X is Element of CQC-WFF A

X <=> F is Element of CQC-WFF A

(X => F) '&' (F => X) is Element of CQC-WFF A

(X => F) '&' (F => 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 bool (QC-WFF A)

bool (QC-WFF A) is set

X is Element of CQC-WFF A

F is Element of CQC-WFF A

X <=> F is Element of CQC-WFF A

TAUT A is Element of bool (CQC-WFF A)

bool (CQC-WFF A) is set

{} (CQC-WFF A) is Element of bool (CQC-WFF A)

Cn ({} (CQC-WFF A)) is Element of bool (CQC-WFF A)

X => F is Element of CQC-WFF A

(X <=> F) => (X => F) is Element of CQC-WFF A

F => X is Element of CQC-WFF A

(X <=> F) => (F => 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 bool (QC-WFF A)

bool (QC-WFF A) is set

X is Element of CQC-WFF A

F is Element of CQC-WFF A

G is Element of CQC-WFF A

F => G is Element of CQC-WFF A

X => (F => G) is Element of CQC-WFF A

f is Element of CQC-WFF A

G => f is Element of CQC-WFF A

F => f is Element of CQC-WFF A

X => (F => f) is Element of CQC-WFF A

X '&' F is Element of CQC-WFF A

(X '&' F) => G is Element of CQC-WFF A

(X '&' F) => f is Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is non empty set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of QC-WFF A

still_not-bound_in X is Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is set

F is Element of bound_QC-variables A

G is Element of bound_QC-variables A

All (G,X) is Element of QC-WFF A

still_not-bound_in (All (G,X)) is Element of bool (bound_QC-variables A)

{G} is non empty set

(still_not-bound_in X) \ {G} is Element of bool (bound_QC-variables A)

A is QC-alphabet

QC-WFF A is non empty set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of QC-WFF A

still_not-bound_in X is Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is set

F is Element of bound_QC-variables A

G is Element of bound_QC-variables A

Ex (G,X) is Element of QC-WFF A

still_not-bound_in (Ex (G,X)) is Element of bool (bound_QC-variables A)

{G} is non empty set

(still_not-bound_in X) \ {G} is Element of bool (bound_QC-variables A)

A is QC-alphabet

QC-WFF A is non empty set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of QC-WFF A

still_not-bound_in X is Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is set

F is Element of QC-WFF A

X => F is Element of QC-WFF A

still_not-bound_in (X => F) is Element of bool (bound_QC-variables A)

still_not-bound_in F is Element of bool (bound_QC-variables A)

G is Element of bound_QC-variables A

(still_not-bound_in X) \/ (still_not-bound_in F) is Element of bool (bound_QC-variables A)

A is QC-alphabet

QC-WFF A is non empty set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of QC-WFF A

still_not-bound_in X is Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is set

F is Element of QC-WFF A

X '&' F is Element of QC-WFF A

still_not-bound_in (X '&' F) is Element of bool (bound_QC-variables A)

still_not-bound_in F is Element of bool (bound_QC-variables A)

G is Element of bound_QC-variables A

(still_not-bound_in X) \/ (still_not-bound_in F) is Element of bool (bound_QC-variables A)

A is QC-alphabet

QC-WFF A is non empty set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of QC-WFF A

still_not-bound_in X is Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is set

F is Element of QC-WFF A

X 'or' F is Element of QC-WFF A

still_not-bound_in (X 'or' F) is Element of bool (bound_QC-variables A)

still_not-bound_in F is Element of bool (bound_QC-variables A)

G is Element of bound_QC-variables A

(still_not-bound_in X) \/ (still_not-bound_in F) is Element of bool (bound_QC-variables A)

A is QC-alphabet

QC-WFF A is non empty set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of QC-WFF A

F is Element of bound_QC-variables A

G is Element of bound_QC-variables A

All (F,G,X) is Element of QC-WFF A

still_not-bound_in (All (F,G,X)) is Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is set

All (G,X) is Element of QC-WFF A

still_not-bound_in (All (G,X)) is Element of bool (bound_QC-variables A)

All (F,(All (G,X))) is Element of QC-WFF A

still_not-bound_in (All (F,(All (G,X)))) is Element of bool (bound_QC-variables A)

A is QC-alphabet

QC-WFF A is non empty set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of QC-WFF A

F is Element of bound_QC-variables A

G is Element of bound_QC-variables A

Ex (F,G,X) is Element of QC-WFF A

still_not-bound_in (Ex (F,G,X)) is Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is set

Ex (G,X) is Element of QC-WFF A

still_not-bound_in (Ex (G,X)) is Element of bool (bound_QC-variables A)

Ex (F,(Ex (G,X))) is Element of QC-WFF A

still_not-bound_in (Ex (F,(Ex (G,X)))) is Element of bool (bound_QC-variables A)

A is QC-alphabet

QC-WFF A is non empty set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of QC-WFF A

F is Element of QC-WFF A

X => F is Element of QC-WFF A

G is Element of bound_QC-variables A

(X => F) . G is Element of QC-WFF A

X . G is Element of QC-WFF A

F . G is Element of QC-WFF A

(X . G) => (F . G) is Element of QC-WFF A

'not' F is Element of QC-WFF A

X '&' ('not' F) is Element of QC-WFF A

'not' (X '&' ('not' F)) is Element of QC-WFF A

(X '&' ('not' F)) . G is Element of QC-WFF A

'not' ((X '&' ('not' F)) . G) is Element of QC-WFF A

('not' F) . G is Element of QC-WFF A

(X . G) '&' (('not' F) . G) is Element of QC-WFF A

'not' ((X . G) '&' (('not' F) . G)) is Element of QC-WFF A

'not' (F . G) is Element of QC-WFF A

(X . G) '&' ('not' (F . G)) is Element of QC-WFF A

'not' ((X . G) '&' ('not' (F . G))) is Element of QC-WFF A

A is QC-alphabet

QC-WFF A is non empty set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of QC-WFF A

F is Element of QC-WFF A

X 'or' F is Element of QC-WFF A

G is Element of bound_QC-variables A

(X 'or' F) . G is Element of QC-WFF A

X . G is Element of QC-WFF A

F . G is Element of QC-WFF A

(X . G) 'or' (F . G) is Element of QC-WFF A

'not' X is Element of QC-WFF A

'not' F is Element of QC-WFF A

('not' X) '&' ('not' F) is Element of QC-WFF A

'not' (('not' X) '&' ('not' F)) is Element of QC-WFF A

('not' (('not' X) '&' ('not' F))) . G is Element of QC-WFF A

(('not' X) '&' ('not' F)) . G is Element of QC-WFF A

'not' ((('not' X) '&' ('not' F)) . G) is Element of QC-WFF A

('not' X) . G is Element of QC-WFF A

('not' F) . G is Element of QC-WFF A

(('not' X) . G) '&' (('not' F) . G) is Element of QC-WFF A

'not' ((('not' X) . G) '&' (('not' F) . G)) is Element of QC-WFF A

'not' (X . G) is Element of QC-WFF A

('not' (X . G)) '&' (('not' F) . G) is Element of QC-WFF A

'not' (('not' (X . G)) '&' (('not' F) . G)) is Element of QC-WFF A

'not' (F . G) is Element of QC-WFF A

('not' (X . G)) '&' ('not' (F . G)) is Element of QC-WFF A

'not' (('not' (X . G)) '&' ('not' (F . G))) is Element of QC-WFF A

A is QC-alphabet

QC-WFF A is non empty set

CQC-WFF A is non empty Element of bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

F is Element of bound_QC-variables A

Ex (F,X) is Element of CQC-WFF A

G is Element of bound_QC-variables A

(Ex (F,X)) . G is Element of QC-WFF A

X . G is Element of QC-WFF A

Ex (F,(X . G)) is Element of QC-WFF A

'not' X is Element of CQC-WFF A

All (F,('not' X)) is Element of CQC-WFF A

'not' (All (F,('not' X))) is Element of CQC-WFF A

('not' (All (F,('not' X)))) . G is Element of QC-WFF A

(All (F,('not' X))) . G is Element of QC-WFF A

'not' ((All (F,('not' X))) . G) is Element of QC-WFF A

('not' X) . G is Element of QC-WFF A

All (F,(('not' X) . G)) is Element of QC-WFF A

'not' (All (F,(('not' X) . G))) is Element of QC-WFF A

'not' (X . G) is Element of QC-WFF A

All (F,('not' (X . G))) is Element of QC-WFF A

'not' (All (F,('not' (X . G)))) is Element of QC-WFF A

A is QC-alphabet

QC-WFF A is non empty set

CQC-WFF A is non empty Element of bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

F is Element of bound_QC-variables A

Ex (F,X) is Element of CQC-WFF A

X => (Ex (F,X)) is Element of CQC-WFF A

'not' X is Element of CQC-WFF A

All (F,('not' X)) is Element of CQC-WFF A

(All (F,('not' X))) => ('not' X) is Element of CQC-WFF A

'not' ('not' X) is Element of CQC-WFF A

'not' (All (F,('not' X))) is Element of CQC-WFF A

('not' ('not' X)) => ('not' (All (F,('not' X)))) is Element of CQC-WFF A

('not' ('not' X)) => (Ex (F,X)) is Element of CQC-WFF A

(('not' ('not' X)) => (Ex (F,X))) => (X => (Ex (F,X))) is valid Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is non empty set

CQC-WFF A is non empty Element of bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

F is Element of bound_QC-variables A

Ex (F,X) is Element of CQC-WFF A

X => (Ex (F,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 bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

F is Element of bound_QC-variables A

All (F,X) is Element of CQC-WFF A

Ex (F,X) is Element of CQC-WFF A

(All (F,X)) => (Ex (F,X)) is Element of CQC-WFF A

(All (F,X)) => X is Element of CQC-WFF A

X => (Ex (F,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 bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

F is Element of bound_QC-variables A

All (F,X) is Element of CQC-WFF A

G is Element of bound_QC-variables A

Ex (G,X) is Element of CQC-WFF A

(All (F,X)) => (Ex (G,X)) is Element of CQC-WFF A

(All (F,X)) => X is Element of CQC-WFF A

X => (Ex (G,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 bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

F is Element of CQC-WFF A

X => F is Element of CQC-WFF A

still_not-bound_in F is Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is set

G is Element of bound_QC-variables A

Ex (G,X) is Element of CQC-WFF A

(Ex (G,X)) => F is Element of CQC-WFF A

'not' F is Element of CQC-WFF A

'not' X is Element of CQC-WFF A

('not' F) => ('not' X) is Element of CQC-WFF A

still_not-bound_in ('not' F) is Element of bool (bound_QC-variables A)

All (G,('not' X)) is Element of CQC-WFF A

('not' F) => (All (G,('not' X))) is Element of CQC-WFF A

'not' (All (G,('not' X))) is Element of CQC-WFF A

'not' ('not' F) is Element of CQC-WFF A

('not' (All (G,('not' X)))) => ('not' ('not' F)) is Element of CQC-WFF A

(Ex (G,X)) => ('not' ('not' F)) 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 bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

still_not-bound_in X is Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is set

F is Element of bound_QC-variables A

Ex (F,X) is Element of CQC-WFF A

(Ex (F,X)) => X is Element of CQC-WFF A

X => X is valid Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is non empty set

CQC-WFF A is non empty Element of bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

still_not-bound_in X is Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is set

F is Element of bound_QC-variables A

Ex (F,X) is Element of CQC-WFF A

(Ex (F,X)) => 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 bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

F is Element of CQC-WFF A

G is Element of QC-WFF A

still_not-bound_in G is Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is set

f is Element of bound_QC-variables A

G . f is Element of QC-WFF A

n is Element of bound_QC-variables A

G . n is Element of QC-WFF A

Ex (n,F) is Element of CQC-WFF A

X => (Ex (n,F)) is Element of CQC-WFF A

G => (Ex (n,F)) is Element of QC-WFF A

(G => (Ex (n,F))) . f is Element of QC-WFF A

(Ex (n,F)) . f is Element of QC-WFF A

(G . f) => ((Ex (n,F)) . f) is Element of QC-WFF A

still_not-bound_in (Ex (n,F)) is Element of bool (bound_QC-variables A)

still_not-bound_in (G => (Ex (n,F))) is Element of bool (bound_QC-variables A)

F => (Ex (n,F)) is Element of CQC-WFF A

(G => (Ex (n,F))) . n is Element of QC-WFF A

(Ex (n,F)) . n is Element of QC-WFF A

(G . n) => ((Ex (n,F)) . n) is Element of QC-WFF A

A is QC-alphabet

QC-WFF A is non empty set

CQC-WFF A is non empty Element of bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

F is Element of bound_QC-variables A

All (F,X) is Element of CQC-WFF A

(All (F,X)) => (All (F,X)) is valid Element of CQC-WFF A

((All (F,X)) => (All (F,X))) => X is Element of CQC-WFF A

X => (((All (F,X)) => (All (F,X))) => X) is valid Element of CQC-WFF A

still_not-bound_in (All (F,X)) is Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is set

still_not-bound_in ((All (F,X)) => (All (F,X))) is Element of bool (bound_QC-variables A)

((All (F,X)) => (All (F,X))) => (All (F,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 bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

still_not-bound_in X is Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is set

F is Element of bound_QC-variables A

All (F,X) is Element of CQC-WFF A

X => (All (F,X)) is Element of CQC-WFF A

X => X is valid Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is non empty set

CQC-WFF A is non empty Element of bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

F is Element of CQC-WFF A

G is Element of QC-WFF A

still_not-bound_in G is Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is set

f is Element of bound_QC-variables A

G . f is Element of QC-WFF A

All (f,X) is Element of CQC-WFF A

(All (f,X)) => F is Element of CQC-WFF A

n is Element of bound_QC-variables A

G . n is Element of QC-WFF A

(All (f,X)) => G is Element of QC-WFF A

((All (f,X)) => G) . n is Element of QC-WFF A

(All (f,X)) . n is Element of QC-WFF A

((All (f,X)) . n) => F is Element of QC-WFF A

still_not-bound_in (All (f,X)) is Element of bool (bound_QC-variables A)

(All (f,X)) => X is Element of CQC-WFF A

still_not-bound_in ((All (f,X)) => G) is Element of bool (bound_QC-variables A)

((All (f,X)) => G) . f is Element of QC-WFF A

(All (f,X)) . f is Element of QC-WFF A

((All (f,X)) . f) => X is Element of QC-WFF A

A is QC-alphabet

QC-WFF A is non empty set

CQC-WFF A is non empty Element of bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

still_not-bound_in X is Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is set

F is Element of bound_QC-variables A

All (F,X) is Element of CQC-WFF A

G is Element of bound_QC-variables A

All (G,X) is Element of CQC-WFF A

(All (G,X)) => (All (F,X)) is Element of CQC-WFF A

(All (G,X)) => X is Element of CQC-WFF A

still_not-bound_in (All (G,X)) is Element of bool (bound_QC-variables A)

A is QC-alphabet

QC-WFF A is non empty set

CQC-WFF A is non empty Element of bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

still_not-bound_in X is Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is set

F is Element of CQC-WFF A

G is Element of QC-WFF A

still_not-bound_in G is Element of bool (bound_QC-variables A)

f is Element of bound_QC-variables A

G . f is Element of QC-WFF A

All (f,X) is Element of CQC-WFF A

n is Element of bound_QC-variables A

G . n is Element of QC-WFF A

All (n,F) is Element of CQC-WFF A

(All (f,X)) => (All (n,F)) is Element of CQC-WFF A

still_not-bound_in (All (f,X)) is Element of bool (bound_QC-variables A)

(All (f,X)) => F 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 bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

still_not-bound_in X is Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is set

F is Element of bound_QC-variables A

Ex (F,X) is Element of CQC-WFF A

G is Element of bound_QC-variables A

Ex (G,X) is Element of CQC-WFF A

(Ex (F,X)) => (Ex (G,X)) is Element of CQC-WFF A

still_not-bound_in (Ex (G,X)) is Element of bool (bound_QC-variables A)

X => (Ex (G,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 bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

F is Element of CQC-WFF A

still_not-bound_in F is Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is set

G is Element of QC-WFF A

still_not-bound_in G is Element of bool (bound_QC-variables A)

f is Element of bound_QC-variables A

G . f is Element of QC-WFF A

Ex (f,X) is Element of CQC-WFF A

n is Element of bound_QC-variables A

G . n is Element of QC-WFF A

Ex (n,F) is Element of CQC-WFF A

(Ex (f,X)) => (Ex (n,F)) is Element of CQC-WFF A

still_not-bound_in (Ex (n,F)) is Element of bool (bound_QC-variables A)

X => (Ex (n,F)) 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 bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

F is Element of CQC-WFF A

X => F is Element of CQC-WFF A

G is Element of bound_QC-variables A

All (G,(X => F)) is Element of CQC-WFF A

All (G,X) is Element of CQC-WFF A

All (G,F) is Element of CQC-WFF A

(All (G,X)) => (All (G,F)) is Element of CQC-WFF A

(All (G,(X => F))) => ((All (G,X)) => (All (G,F))) is Element of CQC-WFF A

(All (G,(X => F))) => (X => F) is Element of CQC-WFF A

(All (G,(X => F))) => F is Element of CQC-WFF A

X => ((All (G,(X => F))) => F) is Element of CQC-WFF A

(All (G,X)) => X is Element of CQC-WFF A

(All (G,X)) => ((All (G,(X => F))) => F) is Element of CQC-WFF A

(All (G,(X => F))) '&' (All (G,X)) is Element of CQC-WFF A

((All (G,(X => F))) '&' (All (G,X))) => F is Element of CQC-WFF A

still_not-bound_in (All (G,(X => F))) is Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is set

still_not-bound_in (All (G,X)) is Element of bool (bound_QC-variables A)

still_not-bound_in ((All (G,(X => F))) '&' (All (G,X))) is Element of bool (bound_QC-variables A)

((All (G,(X => F))) '&' (All (G,X))) => (All (G,F)) 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 bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

F is Element of CQC-WFF A

X => F is Element of CQC-WFF A

G is Element of bound_QC-variables A

All (G,(X => F)) is Element of CQC-WFF A

All (G,X) is Element of CQC-WFF A

All (G,F) is Element of CQC-WFF A

(All (G,X)) => (All (G,F)) is Element of CQC-WFF A

(All (G,(X => F))) => ((All (G,X)) => (All (G,F))) 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 bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

F is Element of CQC-WFF A

X <=> F is Element of CQC-WFF A

G is Element of bound_QC-variables A

All (G,(X <=> F)) is Element of CQC-WFF A

All (G,X) is Element of CQC-WFF A

All (G,F) is Element of CQC-WFF A

(All (G,X)) <=> (All (G,F)) is Element of CQC-WFF A

(All (G,(X <=> F))) => ((All (G,X)) <=> (All (G,F))) is Element of CQC-WFF A

X => F is Element of CQC-WFF A

F => X is Element of CQC-WFF A

(X => F) '&' (F => X) is Element of CQC-WFF A

All (G,((X => F) '&' (F => X))) is Element of CQC-WFF A

(All (G,((X => F) '&' (F => X)))) => ((X => F) '&' (F => X)) is Element of CQC-WFF A

(X <=> F) => (X <=> F) is valid Element of CQC-WFF A

(X <=> F) => ((X => F) '&' (F => X)) is Element of CQC-WFF A

All (G,((X <=> F) => ((X => F) '&' (F => X)))) is Element of CQC-WFF A

(All (G,(X <=> F))) => (All (G,((X => F) '&' (F => X)))) is Element of CQC-WFF A

All (G,(X => F)) is Element of CQC-WFF A

(All (G,X)) => (All (G,F)) is Element of CQC-WFF A

(All (G,(X => F))) => ((All (G,X)) => (All (G,F))) is Element of CQC-WFF A

All (G,(F => X)) is Element of CQC-WFF A

(All (G,F)) => (All (G,X)) is Element of CQC-WFF A

(All (G,(F => X))) => ((All (G,F)) => (All (G,X))) is Element of CQC-WFF A

(All (G,(X => F))) '&' (All (G,(F => X))) is Element of CQC-WFF A

((All (G,X)) => (All (G,F))) '&' ((All (G,F)) => (All (G,X))) is Element of CQC-WFF A

((All (G,(X => F))) '&' (All (G,(F => X)))) => (((All (G,X)) => (All (G,F))) '&' ((All (G,F)) => (All (G,X)))) is Element of CQC-WFF A

((All (G,(X => F))) '&' (All (G,(F => X)))) => ((All (G,X)) <=> (All (G,F))) is Element of CQC-WFF A

still_not-bound_in (All (G,((X => F) '&' (F => X)))) is Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is set

((X => F) '&' (F => X)) => (F => X) is Element of CQC-WFF A

(All (G,((X => F) '&' (F => X)))) => (F => X) is Element of CQC-WFF A

(All (G,((X => F) '&' (F => X)))) => (All (G,(F => X))) is Element of CQC-WFF A

((X => F) '&' (F => X)) => (X => F) is Element of CQC-WFF A

(All (G,((X => F) '&' (F => X)))) => (X => F) is Element of CQC-WFF A

(All (G,((X => F) '&' (F => X)))) => (All (G,(X => F))) is Element of CQC-WFF A

(All (G,((X => F) '&' (F => X)))) => ((All (G,(X => F))) '&' (All (G,(F => X)))) is Element of CQC-WFF A

(All (G,((X => F) '&' (F => X)))) => ((All (G,X)) <=> (All (G,F))) 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 bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

F is Element of CQC-WFF A

X <=> F is Element of CQC-WFF A

G is Element of bound_QC-variables A

All (G,(X <=> F)) is Element of CQC-WFF A

All (G,X) is Element of CQC-WFF A

All (G,F) is Element of CQC-WFF A

(All (G,X)) <=> (All (G,F)) is Element of CQC-WFF A

(All (G,(X <=> F))) => ((All (G,X)) <=> (All (G,F))) 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 bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

F is Element of CQC-WFF A

X => F is Element of CQC-WFF A

G is Element of bound_QC-variables A

All (G,(X => F)) is Element of CQC-WFF A

Ex (G,X) is Element of CQC-WFF A

Ex (G,F) is Element of CQC-WFF A

(Ex (G,X)) => (Ex (G,F)) is Element of CQC-WFF A

(All (G,(X => F))) => ((Ex (G,X)) => (Ex (G,F))) is Element of CQC-WFF A

(All (G,(X => F))) => (X => F) is Element of CQC-WFF A

X '&' (All (G,(X => F))) is Element of CQC-WFF A

(X '&' (All (G,(X => F)))) => F is Element of CQC-WFF A

F => (Ex (G,F)) is Element of CQC-WFF A

(X '&' (All (G,(X => F)))) => (Ex (G,F)) is Element of CQC-WFF A

(All (G,(X => F))) => (Ex (G,F)) is Element of CQC-WFF A

X => ((All (G,(X => F))) => (Ex (G,F))) is Element of CQC-WFF A

still_not-bound_in (All (G,(X => F))) is Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is set

still_not-bound_in (Ex (G,F)) is Element of bool (bound_QC-variables A)

still_not-bound_in ((All (G,(X => F))) => (Ex (G,F))) is Element of bool (bound_QC-variables A)

(Ex (G,X)) => ((All (G,(X => F))) => (Ex (G,F))) 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 bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

F is Element of CQC-WFF A

X => F is Element of CQC-WFF A

G is Element of bound_QC-variables A

All (G,(X => F)) is Element of CQC-WFF A

Ex (G,X) is Element of CQC-WFF A

Ex (G,F) is Element of CQC-WFF A

(Ex (G,X)) => (Ex (G,F)) is Element of CQC-WFF A

(All (G,(X => F))) => ((Ex (G,X)) => (Ex (G,F))) 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 bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

F is Element of CQC-WFF A

X '&' F is Element of CQC-WFF A

G is Element of bound_QC-variables A

All (G,(X '&' F)) is Element of CQC-WFF A

All (G,X) is Element of CQC-WFF A

All (G,F) is Element of CQC-WFF A

(All (G,X)) '&' (All (G,F)) is Element of CQC-WFF A

(All (G,(X '&' F))) => ((All (G,X)) '&' (All (G,F))) is Element of CQC-WFF A

((All (G,X)) '&' (All (G,F))) => (All (G,(X '&' F))) is Element of CQC-WFF A

(All (G,X)) => X is Element of CQC-WFF A

(All (G,F)) => F is Element of CQC-WFF A

((All (G,X)) '&' (All (G,F))) => (X '&' F) is Element of CQC-WFF A

(X '&' F) => F is Element of CQC-WFF A

All (G,((X '&' F) => F)) is Element of CQC-WFF A

(All (G,(X '&' F))) => (All (G,F)) is Element of CQC-WFF A

(All (G,((X '&' F) => F))) => ((All (G,(X '&' F))) => (All (G,F))) is Element of CQC-WFF A

(X '&' F) => X is Element of CQC-WFF A

All (G,((X '&' F) => X)) is Element of CQC-WFF A

(All (G,(X '&' F))) => (All (G,X)) is Element of CQC-WFF A

(All (G,((X '&' F) => X))) => ((All (G,(X '&' F))) => (All (G,X))) is Element of CQC-WFF A

still_not-bound_in (All (G,X)) is Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is set

still_not-bound_in (All (G,F)) is Element of bool (bound_QC-variables A)

still_not-bound_in ((All (G,X)) '&' (All (G,F))) is Element of bool (bound_QC-variables A)

A is QC-alphabet

QC-WFF A is non empty set

CQC-WFF A is non empty Element of bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

F is Element of CQC-WFF A

X '&' F is Element of CQC-WFF A

G is Element of bound_QC-variables A

All (G,(X '&' F)) is Element of CQC-WFF A

All (G,X) is Element of CQC-WFF A

All (G,F) is Element of CQC-WFF A

(All (G,X)) '&' (All (G,F)) is Element of CQC-WFF A

(All (G,(X '&' F))) <=> ((All (G,X)) '&' (All (G,F))) is Element of CQC-WFF A

(All (G,(X '&' F))) => ((All (G,X)) '&' (All (G,F))) is Element of CQC-WFF A

((All (G,X)) '&' (All (G,F))) => (All (G,(X '&' F))) 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 bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

F is Element of CQC-WFF A

X '&' F is Element of CQC-WFF A

G is Element of bound_QC-variables A

All (G,(X '&' F)) is Element of CQC-WFF A

All (G,X) is Element of CQC-WFF A

All (G,F) is Element of CQC-WFF A

(All (G,X)) '&' (All (G,F)) is Element of CQC-WFF A

(All (G,(X '&' F))) <=> ((All (G,X)) '&' (All (G,F))) 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 bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

F is Element of CQC-WFF A

X 'or' F is Element of CQC-WFF A

G is Element of bound_QC-variables A

All (G,X) is Element of CQC-WFF A

All (G,F) is Element of CQC-WFF A

(All (G,X)) 'or' (All (G,F)) is Element of CQC-WFF A

All (G,(X 'or' F)) is Element of CQC-WFF A

((All (G,X)) 'or' (All (G,F))) => (All (G,(X 'or' F))) is Element of CQC-WFF A

F => (X 'or' F) is Element of CQC-WFF A

All (G,(F => (X 'or' F))) is Element of CQC-WFF A

(All (G,F)) => (All (G,(X 'or' F))) is Element of CQC-WFF A

(All (G,(F => (X 'or' F)))) => ((All (G,F)) => (All (G,(X 'or' F)))) is Element of CQC-WFF A

X => (X 'or' F) is Element of CQC-WFF A

All (G,(X => (X 'or' F))) is Element of CQC-WFF A

(All (G,X)) => (All (G,(X 'or' F))) is Element of CQC-WFF A

(All (G,(X => (X 'or' F)))) => ((All (G,X)) => (All (G,(X 'or' F)))) 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 bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

F is Element of CQC-WFF A

X 'or' F is Element of CQC-WFF A

G is Element of bound_QC-variables A

Ex (G,(X 'or' F)) is Element of CQC-WFF A

Ex (G,X) is Element of CQC-WFF A

Ex (G,F) is Element of CQC-WFF A

(Ex (G,X)) 'or' (Ex (G,F)) is Element of CQC-WFF A

(Ex (G,(X 'or' F))) => ((Ex (G,X)) 'or' (Ex (G,F))) is Element of CQC-WFF A

((Ex (G,X)) 'or' (Ex (G,F))) => (Ex (G,(X 'or' F))) is Element of CQC-WFF A

still_not-bound_in (Ex (G,X)) is Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is set

still_not-bound_in (Ex (G,F)) is Element of bool (bound_QC-variables A)

still_not-bound_in ((Ex (G,X)) 'or' (Ex (G,F))) is Element of bool (bound_QC-variables A)

X => (Ex (G,X)) is Element of CQC-WFF A

F => (Ex (G,F)) is Element of CQC-WFF A

(X 'or' F) => ((Ex (G,X)) 'or' (Ex (G,F))) is Element of CQC-WFF A

F => (X 'or' F) is Element of CQC-WFF A

All (G,(F => (X 'or' F))) is Element of CQC-WFF A

(Ex (G,F)) => (Ex (G,(X 'or' F))) is Element of CQC-WFF A

(All (G,(F => (X 'or' F)))) => ((Ex (G,F)) => (Ex (G,(X 'or' F)))) is Element of CQC-WFF A

X => (X 'or' F) is Element of CQC-WFF A

All (G,(X => (X 'or' F))) is Element of CQC-WFF A

(Ex (G,X)) => (Ex (G,(X 'or' F))) is Element of CQC-WFF A

(All (G,(X => (X 'or' F)))) => ((Ex (G,X)) => (Ex (G,(X 'or' F)))) 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 bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

F is Element of CQC-WFF A

X 'or' F is Element of CQC-WFF A

G is Element of bound_QC-variables A

Ex (G,(X 'or' F)) is Element of CQC-WFF A

Ex (G,X) is Element of CQC-WFF A

Ex (G,F) is Element of CQC-WFF A

(Ex (G,X)) 'or' (Ex (G,F)) is Element of CQC-WFF A

(Ex (G,(X 'or' F))) <=> ((Ex (G,X)) 'or' (Ex (G,F))) is Element of CQC-WFF A

(Ex (G,(X 'or' F))) => ((Ex (G,X)) 'or' (Ex (G,F))) is Element of CQC-WFF A

((Ex (G,X)) 'or' (Ex (G,F))) => (Ex (G,(X 'or' F))) 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 bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

F is Element of CQC-WFF A

X 'or' F is Element of CQC-WFF A

G is Element of bound_QC-variables A

Ex (G,(X 'or' F)) is Element of CQC-WFF A

Ex (G,X) is Element of CQC-WFF A

Ex (G,F) is Element of CQC-WFF A

(Ex (G,X)) 'or' (Ex (G,F)) is Element of CQC-WFF A

(Ex (G,(X 'or' F))) <=> ((Ex (G,X)) 'or' (Ex (G,F))) 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 bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

F is Element of CQC-WFF A

X '&' F is Element of CQC-WFF A

G is Element of bound_QC-variables A

Ex (G,(X '&' F)) is Element of CQC-WFF A

Ex (G,X) is Element of CQC-WFF A

Ex (G,F) is Element of CQC-WFF A

(Ex (G,X)) '&' (Ex (G,F)) is Element of CQC-WFF A

(Ex (G,(X '&' F))) => ((Ex (G,X)) '&' (Ex (G,F))) is Element of CQC-WFF A

(X '&' F) => F is Element of CQC-WFF A

All (G,((X '&' F) => F)) is Element of CQC-WFF A

(Ex (G,(X '&' F))) => (Ex (G,F)) is Element of CQC-WFF A

(X '&' F) => X is Element of CQC-WFF A

All (G,((X '&' F) => X)) is Element of CQC-WFF A

(Ex (G,(X '&' F))) => (Ex (G,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 bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

F is Element of CQC-WFF A

X '&' F is Element of CQC-WFF A

G is Element of bound_QC-variables A

Ex (G,(X '&' F)) is Element of CQC-WFF A

Ex (G,X) is Element of CQC-WFF A

Ex (G,F) is Element of CQC-WFF A

(Ex (G,X)) '&' (Ex (G,F)) is Element of CQC-WFF A

(Ex (G,(X '&' F))) => ((Ex (G,X)) '&' (Ex (G,F))) 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 bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

'not' X is Element of CQC-WFF A

'not' ('not' X) is Element of CQC-WFF A

F is Element of bound_QC-variables A

All (F,('not' ('not' X))) is Element of CQC-WFF A

All (F,X) is Element of CQC-WFF A

(All (F,('not' ('not' X)))) => (All (F,X)) is Element of CQC-WFF A

(All (F,X)) => (All (F,('not' ('not' X)))) is Element of CQC-WFF A

('not' ('not' X)) => X is valid Element of CQC-WFF A

All (F,(('not' ('not' X)) => X)) is Element of CQC-WFF A

X => ('not' ('not' X)) is valid Element of CQC-WFF A

All (F,(X => ('not' ('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 bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

'not' X is Element of CQC-WFF A

'not' ('not' X) is Element of CQC-WFF A

F is Element of bound_QC-variables A

All (F,('not' ('not' X))) is Element of CQC-WFF A

All (F,X) is Element of CQC-WFF A

(All (F,('not' ('not' X)))) <=> (All (F,X)) is Element of CQC-WFF A

(All (F,('not' ('not' X)))) => (All (F,X)) is Element of CQC-WFF A

(All (F,X)) => (All (F,('not' ('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 bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

'not' X is Element of CQC-WFF A

'not' ('not' X) is Element of CQC-WFF A

F is Element of bound_QC-variables A

Ex (F,('not' ('not' X))) is Element of CQC-WFF A

Ex (F,X) is Element of CQC-WFF A

(Ex (F,('not' ('not' X)))) => (Ex (F,X)) is Element of CQC-WFF A

(Ex (F,X)) => (Ex (F,('not' ('not' X)))) is Element of CQC-WFF A

('not' ('not' X)) => X is valid Element of CQC-WFF A

All (F,(('not' ('not' X)) => X)) is Element of CQC-WFF A

X => ('not' ('not' X)) is valid Element of CQC-WFF A

All (F,(X => ('not' ('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 bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

'not' X is Element of CQC-WFF A

'not' ('not' X) is Element of CQC-WFF A

F is Element of bound_QC-variables A

Ex (F,('not' ('not' X))) is Element of CQC-WFF A

Ex (F,X) is Element of CQC-WFF A

(Ex (F,('not' ('not' X)))) <=> (Ex (F,X)) is Element of CQC-WFF A

(Ex (F,('not' ('not' X)))) => (Ex (F,X)) is Element of CQC-WFF A

(Ex (F,X)) => (Ex (F,('not' ('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 bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

'not' X is Element of CQC-WFF A

F is Element of bound_QC-variables A

Ex (F,('not' X)) is Element of CQC-WFF A

'not' (Ex (F,('not' X))) is Element of CQC-WFF A

All (F,X) is Element of CQC-WFF A

('not' (Ex (F,('not' X)))) => (All (F,X)) is Element of CQC-WFF A

(All (F,X)) => ('not' (Ex (F,('not' X)))) is Element of CQC-WFF A

'not' ('not' X) is Element of CQC-WFF A

All (F,('not' ('not' X))) is Element of CQC-WFF A

(All (F,('not' ('not' X)))) => (All (F,X)) is Element of CQC-WFF A

'not' (All (F,('not' ('not' X)))) is Element of CQC-WFF A

'not' ('not' (All (F,('not' ('not' X))))) is Element of CQC-WFF A

('not' (Ex (F,('not' X)))) => (All (F,('not' ('not' X)))) is Element of CQC-WFF A

(All (F,X)) => (All (F,('not' ('not' X)))) is Element of CQC-WFF A

(All (F,('not' ('not' X)))) => ('not' ('not' (All (F,('not' ('not' X)))))) is valid Element of CQC-WFF A

A is QC-alphabet

QC-WFF A is non empty set

CQC-WFF A is non empty Element of bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

'not' X is Element of CQC-WFF A

F is Element of bound_QC-variables A

Ex (F,('not' X)) is Element of CQC-WFF A

'not' (Ex (F,('not' X))) is Element of CQC-WFF A

All (F,X) is Element of CQC-WFF A

('not' (Ex (F,('not' X)))) <=> (All (F,X)) is Element of CQC-WFF A

('not' (Ex (F,('not' X)))) => (All (F,X)) is Element of CQC-WFF A

(All (F,X)) => ('not' (Ex (F,('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 bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

'not' X is Element of CQC-WFF A

F is Element of bound_QC-variables A

All (F,X) is Element of CQC-WFF A

'not' (All (F,X)) is Element of CQC-WFF A

Ex (F,('not' X)) is Element of CQC-WFF A

('not' (All (F,X))) => (Ex (F,('not' X))) is Element of CQC-WFF A

(Ex (F,('not' X))) => ('not' (All (F,X))) is Element of CQC-WFF A

'not' ('not' X) is Element of CQC-WFF A

All (F,('not' ('not' X))) is Element of CQC-WFF A

'not' (All (F,('not' ('not' X)))) is Element of CQC-WFF A

(All (F,('not' ('not' X)))) => (All (F,X)) is Element of CQC-WFF A

(All (F,X)) => (All (F,('not' ('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 bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

'not' X is Element of CQC-WFF A

F is Element of bound_QC-variables A

All (F,X) is Element of CQC-WFF A

'not' (All (F,X)) is Element of CQC-WFF A

Ex (F,('not' X)) is Element of CQC-WFF A

('not' (All (F,X))) <=> (Ex (F,('not' X))) is Element of CQC-WFF A

('not' (All (F,X))) => (Ex (F,('not' X))) is Element of CQC-WFF A

(Ex (F,('not' X))) => ('not' (All (F,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 bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

'not' X is Element of CQC-WFF A

F is Element of bound_QC-variables A

Ex (F,X) is Element of CQC-WFF A

'not' (Ex (F,X)) is Element of CQC-WFF A

All (F,('not' X)) is Element of CQC-WFF A

('not' (Ex (F,X))) => (All (F,('not' X))) is Element of CQC-WFF A

(All (F,('not' X))) => ('not' (Ex (F,X))) is Element of CQC-WFF A

'not' (All (F,('not' X))) is Element of CQC-WFF A

'not' ('not' (All (F,('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 bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

'not' X is Element of CQC-WFF A

F is Element of bound_QC-variables A

All (F,('not' X)) is Element of CQC-WFF A

Ex (F,X) is Element of CQC-WFF A

'not' (Ex (F,X)) is Element of CQC-WFF A

(All (F,('not' X))) <=> ('not' (Ex (F,X))) is Element of CQC-WFF A

'not' (All (F,('not' X))) is Element of CQC-WFF A

'not' ('not' (All (F,('not' X)))) is Element of CQC-WFF A

('not' ('not' (All (F,('not' X))))) => (All (F,('not' X))) is valid Element of CQC-WFF A

('not' (Ex (F,X))) => (All (F,('not' X))) is Element of CQC-WFF A

(All (F,('not' X))) => ('not' ('not' (All (F,('not' X))))) is valid Element of CQC-WFF A

(All (F,('not' X))) => ('not' (Ex (F,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 bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

F is Element of bound_QC-variables A

All (F,X) is Element of CQC-WFF A

G is Element of bound_QC-variables A

All (G,X) is Element of CQC-WFF A

All (F,(All (G,X))) is Element of CQC-WFF A

All (G,(All (F,X))) is Element of CQC-WFF A

(All (F,(All (G,X)))) => (All (G,(All (F,X)))) is Element of CQC-WFF A

All (F,G,X) is Element of QC-WFF A

All (G,F,X) is Element of QC-WFF A

(All (F,G,X)) => (All (G,F,X)) is Element of QC-WFF A

still_not-bound_in (All (G,X)) is Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is set

still_not-bound_in (All (F,(All (G,X)))) is Element of bool (bound_QC-variables A)

(All (G,X)) => X is Element of CQC-WFF A

All (F,((All (G,X)) => X)) is Element of CQC-WFF A

(All (F,(All (G,X)))) => (All (F,X)) is Element of CQC-WFF A

(All (F,((All (G,X)) => X))) => ((All (F,(All (G,X)))) => (All (F,X))) is Element of CQC-WFF A

(All (F,G,X)) => (All (G,(All (F,X)))) is Element of QC-WFF A

A is QC-alphabet

QC-WFF A is non empty set

CQC-WFF A is non empty Element of bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

F is Element of CQC-WFF A

G is Element of QC-WFF A

still_not-bound_in G is Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is set

f is Element of bound_QC-variables A

G . f is Element of QC-WFF A

All (f,X) is Element of CQC-WFF A

n is Element of bound_QC-variables A

G . n is Element of QC-WFF A

All (n,F) is Element of CQC-WFF A

All (f,(All (n,F))) is Element of CQC-WFF A

(All (f,(All (n,F)))) => (All (f,X)) is Element of CQC-WFF A

(All (n,F)) => X is Element of CQC-WFF A

All (f,((All (n,F)) => 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 bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

F is Element of bound_QC-variables A

Ex (F,X) is Element of CQC-WFF A

G is Element of bound_QC-variables A

Ex (G,X) is Element of CQC-WFF A

Ex (F,(Ex (G,X))) is Element of CQC-WFF A

Ex (G,(Ex (F,X))) is Element of CQC-WFF A

(Ex (F,(Ex (G,X)))) => (Ex (G,(Ex (F,X)))) is Element of CQC-WFF A

Ex (F,G,X) is Element of QC-WFF A

Ex (G,F,X) is Element of QC-WFF A

(Ex (F,G,X)) => (Ex (G,F,X)) is Element of QC-WFF A

still_not-bound_in (Ex (F,X)) is Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is set

still_not-bound_in (Ex (G,(Ex (F,X)))) is Element of bool (bound_QC-variables A)

X => (Ex (F,X)) is Element of CQC-WFF A

All (G,(X => (Ex (F,X)))) is Element of CQC-WFF A

(Ex (G,X)) => (Ex (G,(Ex (F,X)))) is Element of CQC-WFF A

(All (G,(X => (Ex (F,X))))) => ((Ex (G,X)) => (Ex (G,(Ex (F,X))))) is Element of CQC-WFF A

(Ex (F,G,X)) => (Ex (G,(Ex (F,X)))) is Element of QC-WFF A

A is QC-alphabet

QC-WFF A is non empty set

CQC-WFF A is non empty Element of bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

F is Element of CQC-WFF A

G is Element of QC-WFF A

still_not-bound_in G is Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is set

f is Element of bound_QC-variables A

G . f is Element of QC-WFF A

Ex (f,X) is Element of CQC-WFF A

n is Element of bound_QC-variables A

G . n is Element of QC-WFF A

Ex (f,n,F) is Element of QC-WFF A

(Ex (f,X)) => (Ex (f,n,F)) is Element of QC-WFF A

Ex (n,F) is Element of CQC-WFF A

X => (Ex (n,F)) is Element of CQC-WFF A

All (f,(X => (Ex (n,F)))) is Element of CQC-WFF A

Ex (f,(Ex (n,F))) is Element of CQC-WFF A

(Ex (f,X)) => (Ex (f,(Ex (n,F)))) 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 bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

F is Element of bound_QC-variables A

Ex (F,X) is Element of CQC-WFF A

G is Element of bound_QC-variables A

All (G,X) is Element of CQC-WFF A

Ex (F,(All (G,X))) is Element of CQC-WFF A

All (G,(Ex (F,X))) is Element of CQC-WFF A

(Ex (F,(All (G,X)))) => (All (G,(Ex (F,X)))) is Element of CQC-WFF A

still_not-bound_in (Ex (F,X)) is Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is set

still_not-bound_in (All (G,(Ex (F,X)))) is Element of bool (bound_QC-variables A)

X => (Ex (F,X)) is Element of CQC-WFF A

All (G,(X => (Ex (F,X)))) is Element of CQC-WFF A

(All (G,X)) => (All (G,(Ex (F,X)))) is Element of CQC-WFF A

(All (G,(X => (Ex (F,X))))) => ((All (G,X)) => (All (G,(Ex (F,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 bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

F is Element of bound_QC-variables A

X is Element of CQC-WFF A

X <=> X is Element of CQC-WFF A

Ex (F,(X <=> 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 bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

F is Element of CQC-WFF A

X => F is Element of CQC-WFF A

G is Element of bound_QC-variables A

Ex (G,(X => F)) is Element of CQC-WFF A

All (G,X) is Element of CQC-WFF A

Ex (G,F) is Element of CQC-WFF A

(All (G,X)) => (Ex (G,F)) is Element of CQC-WFF A

(Ex (G,(X => F))) => ((All (G,X)) => (Ex (G,F))) is Element of CQC-WFF A

((All (G,X)) => (Ex (G,F))) => (Ex (G,(X => F))) is Element of CQC-WFF A

(All (G,X)) => X is Element of CQC-WFF A

(All (G,X)) => F is Element of CQC-WFF A

(X => F) => ((All (G,X)) => F) is Element of CQC-WFF A

still_not-bound_in (All (G,X)) is Element of bool (bound_QC-variables A)

bool (bound_QC-variables A) is set

still_not-bound_in (Ex (G,F)) is Element of bool (bound_QC-variables A)

still_not-bound_in ((All (G,X)) => (Ex (G,F))) is Element of bool (bound_QC-variables A)

F => (Ex (G,F)) is Element of CQC-WFF A

(X => F) => ((All (G,X)) => (Ex (G,F))) is Element of CQC-WFF A

'not' F is Element of CQC-WFF A

X '&' ('not' F) is Element of CQC-WFF A

All (G,(X '&' ('not' F))) is Element of CQC-WFF A

All (G,('not' F)) is Element of CQC-WFF A

(All (G,X)) '&' (All (G,('not' F))) is Element of CQC-WFF A

(All (G,(X '&' ('not' F)))) => ((All (G,X)) '&' (All (G,('not' F)))) is Element of CQC-WFF A

'not' ((All (G,X)) '&' (All (G,('not' F)))) is Element of CQC-WFF A

'not' (All (G,(X '&' ('not' F)))) is Element of CQC-WFF A

('not' ((All (G,X)) '&' (All (G,('not' F))))) => ('not' (All (G,(X '&' ('not' F))))) is Element of CQC-WFF A

'not' (X '&' ('not' F)) is Element of CQC-WFF A

Ex (G,('not' (X '&' ('not' F)))) is Element of CQC-WFF A

('not' (All (G,(X '&' ('not' F))))) => (Ex (G,('not' (X '&' ('not' F))))) is Element of CQC-WFF A

('not' ((All (G,X)) '&' (All (G,('not' F))))) => (Ex (G,('not' (X '&' ('not' F))))) is Element of CQC-WFF A

('not' ((All (G,X)) '&' (All (G,('not' F))))) => (Ex (G,(X => F))) is Element of CQC-WFF A

'not' (All (G,('not' F))) is Element of CQC-WFF A

'not' ('not' (All (G,('not' F)))) is Element of CQC-WFF A

(All (G,('not' F))) => ('not' ('not' (All (G,('not' F))))) is valid Element of CQC-WFF A

(All (G,X)) '&' ('not' ('not' (All (G,('not' F))))) is Element of CQC-WFF A

((All (G,X)) '&' (All (G,('not' F)))) => ((All (G,X)) '&' ('not' ('not' (All (G,('not' F)))))) is Element of CQC-WFF A

(All (G,X)) => ('not' (All (G,('not' F)))) is Element of CQC-WFF A

'not' ((All (G,X)) '&' ('not' ('not' (All (G,('not' F)))))) is Element of CQC-WFF A

((All (G,X)) => (Ex (G,F))) => ('not' ((All (G,X)) '&' (All (G,('not' F))))) 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 bool (QC-WFF A)

bool (QC-WFF A) is set

QC-variables A is set

bound_QC-variables A is Element of bool (QC-variables A)

bool (QC-variables A) is set

X is Element of CQC-WFF A

F is Element of CQC-WFF A

X => F is Element of CQC-WFF A

G is Element of bound_QC-variables A

Ex (G,(X => F)) is Element of CQC-WFF A

All (G,X) is Element of CQC-WFF A

Ex (G,F) is Element of CQC-WFF A

(All (G,X)) => (Ex (G,F)) is Element of CQC-WFF A

(Ex (G,(X => F))) <=> ((All (G,X)) => (Ex (G,F))) is Element of CQC-WFF A

(Ex (G,(X => F))) => ((All (G,X)) => (Ex (G,F))) is Element of CQC-WFF A

((All (G,X))