:: 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₁ where b₁ is ext-real V20() V21() V22() V23() V27() Element of NAT : b₁ <= 9 } is set
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))