:: 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)) => (Ex (G,F))) => (Ex (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
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
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,F) is Element of CQC-WFF A
X '&' (All (G,F)) is Element of CQC-WFF A
(All (G,(X '&' F))) => (X '&' (All (G,F))) is Element of CQC-WFF A
(All (G,(X '&' F))) => (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
(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
(X '&' F) => X is Element of CQC-WFF A
(All (G,(X '&' 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 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,X)) '&' F is Element of CQC-WFF A
(All (G,(X '&' F))) => ((All (G,X)) '&' F) is Element of CQC-WFF A
F '&' (All (G,X)) is Element of CQC-WFF A
(F '&' (All (G,X))) => ((All (G,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,(F '&' X)) is Element of CQC-WFF A
(All (G,(X '&' F))) => (All (G,(F '&' X))) 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,(F '&' X))) => (F '&' (All (G,X))) is Element of CQC-WFF A
(All (G,(X '&' F))) => (F '&' (All (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
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
X '&' F is Element of CQC-WFF A
G is Element of bound_QC-variables A
All (G,F) is Element of CQC-WFF A
X '&' (All (G,F)) is Element of CQC-WFF A
All (G,(X '&' F)) is Element of CQC-WFF A
(X '&' (All (G,F))) => (All (G,(X '&' F))) is Element of CQC-WFF A
(All (G,F)) => F is Element of CQC-WFF A
(X '&' (All (G,F))) => (X '&' F) is Element of CQC-WFF A
still_not-bound_in (All (G,F)) is Element of bool (bound_QC-variables A)
still_not-bound_in (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
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
X '&' F is Element of CQC-WFF A
G is Element of bound_QC-variables A
All (G,F) is Element of CQC-WFF A
X '&' (All (G,F)) is Element of CQC-WFF A
All (G,(X '&' F)) is Element of CQC-WFF A
(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
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
X 'or' F is Element of CQC-WFF A
G is Element of bound_QC-variables A
All (G,F) is Element of CQC-WFF A
X 'or' (All (G,F)) is Element of CQC-WFF A
All (G,(X 'or' F)) is Element of CQC-WFF A
(X 'or' (All (G,F))) => (All (G,(X 'or' F))) is Element of CQC-WFF A
(All (G,(X 'or' F))) => (X 'or' (All (G,F))) is Element of CQC-WFF A
still_not-bound_in (All (G,(X 'or' F))) is Element of bool (bound_QC-variables A)
(All (G,(X 'or' F))) => (X 'or' F) is Element of CQC-WFF A
'not' X 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
(All (G,(X 'or' F))) => (('not' X) => F) is Element of CQC-WFF A
(All (G,(X 'or' F))) '&' ('not' X) is Element of CQC-WFF A
((All (G,(X 'or' F))) '&' ('not' X)) => F is Element of CQC-WFF A
still_not-bound_in ('not' X) is Element of bool (bound_QC-variables A)
still_not-bound_in ((All (G,(X 'or' F))) '&' ('not' X)) is Element of bool (bound_QC-variables A)
((All (G,(X 'or' F))) '&' ('not' X)) => (All (G,F)) is Element of CQC-WFF A
('not' X) => (All (G,F)) is Element of CQC-WFF A
(All (G,(X 'or' F))) => (('not' X) => (All (G,F))) is Element of CQC-WFF A
X => X is valid Element of CQC-WFF A
All (G,X) is Element of CQC-WFF A
X => (All (G,X)) is Element of CQC-WFF A
(All (G,X)) 'or' (All (G,F)) is Element of CQC-WFF A
(X 'or' (All (G,F))) => ((All (G,X)) 'or' (All (G,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
(('not' X) => (All (G,F))) => (X 'or' (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
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
X 'or' F is Element of CQC-WFF A
G is Element of bound_QC-variables A
All (G,F) is Element of CQC-WFF A
X 'or' (All (G,F)) is Element of CQC-WFF A
All (G,(X 'or' F)) is Element of CQC-WFF A
(X 'or' (All (G,F))) <=> (All (G,(X 'or' F))) is Element of CQC-WFF A
(X 'or' (All (G,F))) => (All (G,(X 'or' F))) is Element of CQC-WFF A
(All (G,(X 'or' F))) => (X 'or' (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
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
X 'or' F is Element of CQC-WFF A
G is Element of bound_QC-variables A
All (G,F) is Element of CQC-WFF A
X 'or' (All (G,F)) is Element of CQC-WFF A
All (G,(X 'or' F)) is Element of CQC-WFF A
(X 'or' (All (G,F))) <=> (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
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
X '&' F is Element of CQC-WFF A
G is Element of bound_QC-variables A
Ex (G,F) is Element of CQC-WFF A
X '&' (Ex (G,F)) is Element of CQC-WFF A
Ex (G,(X '&' F)) is Element of CQC-WFF A
(X '&' (Ex (G,F))) => (Ex (G,(X '&' F))) is Element of CQC-WFF A
(Ex (G,(X '&' F))) => (X '&' (Ex (G,F))) is Element of CQC-WFF A
(X '&' F) => (Ex (G,(X '&' F))) is Element of CQC-WFF A
X => (Ex (G,(X '&' F))) is Element of CQC-WFF A
F => (X => (Ex (G,(X '&' F)))) is Element of CQC-WFF A
still_not-bound_in (Ex (G,(X '&' F))) is Element of bool (bound_QC-variables A)
still_not-bound_in (X => (Ex (G,(X '&' F)))) is Element of bool (bound_QC-variables A)
(Ex (G,F)) => (X => (Ex (G,(X '&' F)))) is Element of CQC-WFF A
F => (Ex (G,F)) is Element of CQC-WFF A
(X '&' F) => (X '&' (Ex (G,F))) is Element of CQC-WFF A
still_not-bound_in (Ex (G,F)) is Element of bool (bound_QC-variables A)
still_not-bound_in (X '&' (Ex (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
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
X '&' F is Element of CQC-WFF A
G is Element of bound_QC-variables A
Ex (G,F) is Element of CQC-WFF A
X '&' (Ex (G,F)) is Element of CQC-WFF A
Ex (G,(X '&' F)) is Element of CQC-WFF A
(X '&' (Ex (G,F))) <=> (Ex (G,(X '&' F))) is Element of CQC-WFF A
(X '&' (Ex (G,F))) => (Ex (G,(X '&' F))) is Element of CQC-WFF A
(Ex (G,(X '&' F))) => (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
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
X '&' F is Element of CQC-WFF A
G is Element of bound_QC-variables A
Ex (G,F) is Element of CQC-WFF A
X '&' (Ex (G,F)) is Element of CQC-WFF A
Ex (G,(X '&' F)) is Element of CQC-WFF A
(X '&' (Ex (G,F))) <=> (Ex (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
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
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,F) is Element of CQC-WFF A
X => (All (G,F)) is Element of CQC-WFF A
(All (G,(X => F))) => (X => (All (G,F))) is Element of CQC-WFF A
All (G,X) is Element of CQC-WFF A
X => (All (G,X)) 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,F)) is Element of CQC-WFF A
(All (G,X)) => ((All (G,(X => F))) => (All (G,F))) is Element of CQC-WFF A
X => ((All (G,(X => F))) => (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
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
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,F) is Element of CQC-WFF A
X => (All (G,F)) is Element of CQC-WFF A
(All (G,(X => F))) => (X => (All (G,F))) is Element of CQC-WFF A
(X => (All (G,F))) => (All (G,(X => F))) is Element of CQC-WFF A
still_not-bound_in (All (G,F)) is Element of bool (bound_QC-variables A)
still_not-bound_in (X => (All (G,F))) is Element of bool (bound_QC-variables A)
(X => (All (G,F))) => (X => F) is Element of CQC-WFF A
All (G,((X => (All (G,F))) => (X => F))) is Element of CQC-WFF A
(All (G,((X => (All (G,F))) => (X => F)))) => ((X => (All (G,F))) => (All (G,(X => F)))) is Element of CQC-WFF A
(All (G,F)) => F is Element of CQC-WFF A
((All (G,F)) => F) => ((X => (All (G,F))) => (X => F)) is valid Element of CQC-WFF A
All (G,(((All (G,F)) => F) => ((X => (All (G,F))) => (X => F)))) is Element of CQC-WFF A
All (G,((All (G,F)) => F)) is Element of CQC-WFF A
(All (G,((All (G,F)) => F))) => (All (G,((X => (All (G,F))) => (X => F)))) is Element of CQC-WFF A
(All (G,(((All (G,F)) => F) => ((X => (All (G,F))) => (X => F))))) => ((All (G,((All (G,F)) => F))) => (All (G,((X => (All (G,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 CQC-WFF A
X => F is Element of CQC-WFF A
G is Element of bound_QC-variables A
All (G,F) is Element of CQC-WFF A
X => (All (G,F)) is Element of CQC-WFF A
All (G,(X => F)) is Element of CQC-WFF A
(X => (All (G,F))) <=> (All (G,(X => F))) is Element of CQC-WFF A
(X => (All (G,F))) => (All (G,(X => F))) is Element of CQC-WFF A
(All (G,(X => F))) => (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
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
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,F) is Element of CQC-WFF A
X => (All (G,F)) is Element of CQC-WFF A
(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
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
F => X is Element of CQC-WFF A
G is Element of bound_QC-variables A
Ex (G,(F => X)) is Element of CQC-WFF A
All (G,F) is Element of CQC-WFF A
(All (G,F)) => X is Element of CQC-WFF A
(Ex (G,(F => X))) => ((All (G,F)) => X) is Element of CQC-WFF A
still_not-bound_in (All (G,F)) is Element of bool (bound_QC-variables A)
still_not-bound_in ((All (G,F)) => X) is Element of bool (bound_QC-variables A)
Ex (G,((All (G,F)) => X)) is Element of CQC-WFF A
(Ex (G,((All (G,F)) => X))) => ((All (G,F)) => X) is Element of CQC-WFF A
(All (G,F)) => F is Element of CQC-WFF A
(F => X) => ((All (G,F)) => X) is Element of CQC-WFF A
All (G,((F => X) => ((All (G,F)) => X))) is Element of CQC-WFF A
(Ex (G,(F => X))) => (Ex (G,((All (G,F)) => X))) is Element of CQC-WFF A
(All (G,((F => X) => ((All (G,F)) => X)))) => ((Ex (G,(F => X))) => (Ex (G,((All (G,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 CQC-WFF A
X => 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,X)) => F is Element of CQC-WFF A
Ex (G,(X => F)) is Element of CQC-WFF A
((All (G,X)) => F) => (Ex (G,(X => 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,X)) '&' ('not' F) is Element of CQC-WFF A
(All (G,(X '&' ('not' F)))) => ((All (G,X)) '&' ('not' F)) is Element of CQC-WFF A
'not' ((All (G,X)) '&' ('not' F)) is Element of CQC-WFF A
'not' (All (G,(X '&' ('not' F)))) is Element of CQC-WFF A
('not' ((All (G,X)) '&' ('not' F))) => ('not' (All (G,(X '&' ('not' F))))) is Element of CQC-WFF A
((All (G,X)) => F) => ('not' (All (G,(X '&' ('not' F))))) is Element of CQC-WFF A
'not' (X '&' ('not' F)) is Element of CQC-WFF A
'not' ('not' (X '&' ('not' F))) is Element of CQC-WFF A
('not' ('not' (X '&' ('not' F)))) => (X '&' ('not' F)) is valid Element of CQC-WFF A
All (G,(('not' ('not' (X '&' ('not' F)))) => (X '&' ('not' F)))) is Element of CQC-WFF A
All (G,('not' ('not' (X '&' ('not' F))))) is Element of CQC-WFF A
(All (G,('not' ('not' (X '&' ('not' F)))))) => (All (G,(X '&' ('not' F)))) is Element of CQC-WFF A
(All (G,(('not' ('not' (X '&' ('not' F)))) => (X '&' ('not' F))))) => ((All (G,('not' ('not' (X '&' ('not' F)))))) => (All (G,(X '&' ('not' F))))) is Element of CQC-WFF A
'not' (All (G,('not' ('not' (X '&' ('not' F)))))) is Element of CQC-WFF A
('not' (All (G,(X '&' ('not' F))))) => ('not' (All (G,('not' ('not' (X '&' ('not' F))))))) is Element of CQC-WFF A
((All (G,X)) => F) => ('not' (All (G,('not' ('not' (X '&' ('not' F))))))) is Element of CQC-WFF A
Ex (G,('not' (X '&' ('not' F)))) is Element of CQC-WFF A
((All (G,X)) => F) => (Ex (G,('not' (X '&' ('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 CQC-WFF A
F => X is Element of CQC-WFF A
G is Element of bound_QC-variables A
All (G,F) is Element of CQC-WFF A
(All (G,F)) => X is Element of CQC-WFF A
Ex (G,(F => X)) is Element of CQC-WFF A
(Ex (G,(F => X))) => ((All (G,F)) => X) is Element of CQC-WFF A
((All (G,F)) => X) => (Ex (G,(F => X))) is Element of CQC-WFF A
((All (G,F)) => X) <=> (Ex (G,(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 CQC-WFF A
F => X is Element of CQC-WFF A
G is Element of bound_QC-variables A
Ex (G,F) is Element of CQC-WFF A
(Ex (G,F)) => X is Element of CQC-WFF A
All (G,(F => X)) is Element of CQC-WFF A
((Ex (G,F)) => X) => (All (G,(F => X))) is Element of CQC-WFF A
(All (G,(F => X))) => ((Ex (G,F)) => X) is Element of CQC-WFF A
F => (Ex (G,F)) is Element of CQC-WFF A
((Ex (G,F)) => X) => (F => X) is Element of CQC-WFF A
still_not-bound_in (Ex (G,F)) is Element of bool (bound_QC-variables A)
still_not-bound_in ((Ex (G,F)) => X) is Element of bool (bound_QC-variables A)
Ex (G,X) is Element of CQC-WFF A
(Ex (G,F)) => (Ex (G,X)) is Element of CQC-WFF A
(All (G,(F => X))) => ((Ex (G,F)) => (Ex (G,X))) is Element of CQC-WFF A
(All (G,(F => X))) '&' (Ex (G,F)) is Element of CQC-WFF A
((All (G,(F => X))) '&' (Ex (G,F))) => (Ex (G,X)) is Element of CQC-WFF A
(Ex (G,X)) => X is Element of CQC-WFF A
((All (G,(F => X))) '&' (Ex (G,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 CQC-WFF A
F => X is Element of CQC-WFF A
G is Element of bound_QC-variables A
Ex (G,F) is Element of CQC-WFF A
(Ex (G,F)) => X is Element of CQC-WFF A
All (G,(F => X)) is Element of CQC-WFF A
((Ex (G,F)) => X) <=> (All (G,(F => X))) is Element of CQC-WFF A
((Ex (G,F)) => X) => (All (G,(F => X))) is Element of CQC-WFF A
(All (G,(F => X))) => ((Ex (G,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 CQC-WFF A
F => X is Element of CQC-WFF A
G is Element of bound_QC-variables A
Ex (G,F) is Element of CQC-WFF A
(Ex (G,F)) => X is Element of CQC-WFF A
All (G,(F => X)) is Element of CQC-WFF A
((Ex (G,F)) => X) <=> (All (G,(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 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,F) is Element of CQC-WFF A
X => (Ex (G,F)) is Element of CQC-WFF A
(Ex (G,(X => F))) => (X => (Ex (G,F))) is Element of CQC-WFF A
still_not-bound_in (Ex (G,F)) is Element of bool (bound_QC-variables A)
still_not-bound_in (X => (Ex (G,F))) is Element of bool (bound_QC-variables A)
Ex (G,(X => (Ex (G,F)))) is Element of CQC-WFF A
(Ex (G,(X => (Ex (G,F))))) => (X => (Ex (G,F))) is Element of CQC-WFF A
F => (Ex (G,F)) is Element of CQC-WFF A
(X => F) => (X => (Ex (G,F))) is Element of CQC-WFF A
All (G,((X => F) => (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
(All (G,((X => F) => (X => (Ex (G,F)))))) => ((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
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,F) is Element of CQC-WFF A
X => (Ex (G,F)) is Element of CQC-WFF A
Ex (G,(X => F)) is Element of CQC-WFF A
(X => (Ex (G,F))) => (Ex (G,(X => F))) is Element of CQC-WFF A
'not' F is Element of CQC-WFF A
X '&' ('not' F) is Element of CQC-WFF A
'not' (X '&' ('not' F)) is Element of CQC-WFF A
'not' ('not' (X '&' ('not' F))) is Element of CQC-WFF A
('not' ('not' (X '&' ('not' F)))) => (X '&' ('not' F)) is valid Element of CQC-WFF A
All (G,(('not' ('not' (X '&' ('not' F)))) => (X '&' ('not' F)))) is Element of CQC-WFF A
All (G,('not' ('not' (X '&' ('not' F))))) is Element of CQC-WFF A
All (G,(X '&' ('not' F))) is Element of CQC-WFF A
(All (G,('not' ('not' (X '&' ('not' F)))))) => (All (G,(X '&' ('not' F)))) is Element of CQC-WFF A
(All (G,(('not' ('not' (X '&' ('not' F)))) => (X '&' ('not' F))))) => ((All (G,('not' ('not' (X '&' ('not' F)))))) => (All (G,(X '&' ('not' F))))) is Element of CQC-WFF A
'not' (All (G,(X '&' ('not' F)))) is Element of CQC-WFF A
'not' (All (G,('not' ('not' (X '&' ('not' F)))))) is Element of CQC-WFF A
('not' (All (G,(X '&' ('not' F))))) => ('not' (All (G,('not' ('not' (X '&' ('not' F))))))) is Element of CQC-WFF A
All (G,('not' F)) is Element of CQC-WFF A
'not' (Ex (G,F)) is Element of CQC-WFF A
(All (G,('not' F))) <=> ('not' (Ex (G,F))) is Element of CQC-WFF A
(All (G,('not' F))) => ('not' (Ex (G,F))) is Element of CQC-WFF A
X '&' (All (G,('not' F))) is Element of CQC-WFF A
X '&' ('not' (Ex (G,F))) is Element of CQC-WFF A
(X '&' (All (G,('not' F)))) => (X '&' ('not' (Ex (G,F)))) is Element of CQC-WFF A
'not' (X '&' ('not' (Ex (G,F)))) is Element of CQC-WFF A
'not' (X '&' (All (G,('not' F)))) is Element of CQC-WFF A
('not' (X '&' ('not' (Ex (G,F))))) => ('not' (X '&' (All (G,('not' F))))) is Element of CQC-WFF A
(All (G,(X '&' ('not' F)))) => (X '&' (All (G,('not' F)))) is Element of CQC-WFF A
('not' (X '&' (All (G,('not' F))))) => ('not' (All (G,(X '&' ('not' F))))) is Element of CQC-WFF A
('not' (X '&' ('not' (Ex (G,F))))) => ('not' (All (G,(X '&' ('not' F))))) is Element of CQC-WFF A
(X => (Ex (G,F))) => ('not' (All (G,(X '&' ('not' F))))) is Element of CQC-WFF A
(X => (Ex (G,F))) => ('not' (All (G,('not' ('not' (X '&' ('not' F))))))) is Element of CQC-WFF A
'not' (X => F) is Element of CQC-WFF A
All (G,('not' (X => F))) is Element of CQC-WFF A
'not' (All (G,('not' (X => F)))) is Element of CQC-WFF A
(X => (Ex (G,F))) => ('not' (All (G,('not' (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 CQC-WFF A
X => F is Element of CQC-WFF A
G is Element of bound_QC-variables A
Ex (G,F) is Element of CQC-WFF A
X => (Ex (G,F)) is Element of CQC-WFF A
Ex (G,(X => F)) is Element of CQC-WFF A
(X => (Ex (G,F))) <=> (Ex (G,(X => F))) is Element of CQC-WFF A
(Ex (G,(X => F))) => (X => (Ex (G,F))) is Element of CQC-WFF A
(X => (Ex (G,F))) => (Ex (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
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
X => F is Element of CQC-WFF A
G is Element of bound_QC-variables A
Ex (G,F) is Element of CQC-WFF A
X => (Ex (G,F)) is Element of CQC-WFF A
Ex (G,(X => F)) is Element of CQC-WFF A
(X => (Ex (G,F))) <=> (Ex (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
X is Element of CQC-WFF A
{X} is non empty Element of bool (CQC-WFF A)
bool (CQC-WFF A) is set
Cn {X} 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
{X} is non empty Element of bool (CQC-WFF A)
bool (CQC-WFF A) is set
F is Element of CQC-WFF A
{F} is non empty Element of bool (CQC-WFF A)
{X} \/ {F} is non empty Element of bool (CQC-WFF A)
Cn ({X} \/ {F}) is Element of bool (CQC-WFF A)
X '&' F is Element of CQC-WFF A
{(X '&' F)} is non empty Element of bool (CQC-WFF A)
Cn {(X '&' F)} is Element of bool (CQC-WFF A)
G is Element of CQC-WFF A
f is Element of bool (CQC-WFF A)
TAUT A is Element of bool (CQC-WFF A)
{} (CQC-WFF A) is Element of bool (CQC-WFF A)
Cn ({} (CQC-WFF A)) is Element of bool (CQC-WFF A)
(X '&' F) => F is Element of CQC-WFF A
(X '&' F) => X is Element of CQC-WFF A
f is Element of bool (CQC-WFF A)
F => (X '&' F) is Element of CQC-WFF A
X => (F => (X '&' F)) is Element of CQC-WFF A
TAUT A is Element of bool (CQC-WFF A)
{} (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 non empty Element of bool (CQC-WFF A)
bool (CQC-WFF A) is set
X '&' F is Element of CQC-WFF A
{(X '&' F)} is non empty Element of bool (CQC-WFF A)
G is Element of CQC-WFF A
Cn {X,F} is Element of bool (CQC-WFF A)
{X} is non empty Element of bool (CQC-WFF A)
{F} is non empty Element of bool (CQC-WFF A)
{X} \/ {F} is non empty Element of bool (CQC-WFF A)
Cn ({X} \/ {F}) is Element of bool (CQC-WFF A)
Cn {(X '&' F)} is Element of bool (CQC-WFF A)
Cn {(X '&' F)} is Element of bool (CQC-WFF A)
{X} is non empty Element of bool (CQC-WFF A)
{F} is non empty Element of bool (CQC-WFF A)
{X} \/ {F} is non empty Element of bool (CQC-WFF A)
Cn ({X} \/ {F}) is Element of bool (CQC-WFF A)
Cn {X,F} is Element of bool (CQC-WFF A)
A is QC-alphabet
CQC-WFF A is non empty Element of bool (QC-WFF A)
QC-WFF A is non empty set
bool (QC-WFF A) is set
bool (CQC-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 bool (CQC-WFF A)
F is Element of CQC-WFF A
G is Element of bound_QC-variables A
All (G,F) is Element of CQC-WFF A
(All (G,F)) => (All (G,F)) is valid Element of CQC-WFF A
((All (G,F)) => (All (G,F))) => F is Element of CQC-WFF A
F => (((All (G,F)) => (All (G,F))) => F) is valid Element of CQC-WFF A
still_not-bound_in (All (G,F)) is Element of bool (bound_QC-variables A)
bool (bound_QC-variables A) is set
still_not-bound_in ((All (G,F)) => (All (G,F))) is Element of bool (bound_QC-variables A)
((All (G,F)) => (All (G,F))) => (All (G,F)) is Element of CQC-WFF A
A is QC-alphabet
CQC-WFF A is non empty Element of bool (QC-WFF A)
QC-WFF A is non empty set
bool (QC-WFF A) is set
bool (CQC-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
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
X is Element of bool (CQC-WFF A)
G is Element of CQC-WFF A
F => G is Element of CQC-WFF A
All (f,(F => G)) is Element of CQC-WFF A
All (f,G) is Element of CQC-WFF A
F => (All (f,G)) is Element of CQC-WFF A
(All (f,(F => G))) => (F => (All (f,G))) is Element of CQC-WFF A
A is QC-alphabet
CQC-WFF A is non empty Element of bool (QC-WFF A)
QC-WFF A is non empty set
bool (QC-WFF A) is set
bool (CQC-WFF A) is set
X is Element of bool (CQC-WFF A)
F is Element of CQC-WFF A
{F} is non empty Element of bool (CQC-WFF A)
X \/ {F} is non empty Element of bool (CQC-WFF A)
G is Element of CQC-WFF A
F => G is Element of CQC-WFF A
Cn (X \/ {F}) is Element of bool (CQC-WFF A)
[:(CQC-WFF A),Proof_Step_Kinds:] is set
f is V7() V10( NAT ) V11([:(CQC-WFF A),Proof_Step_Kinds:]) Function-like FinSequence-like FinSequence of [:(CQC-WFF A),Proof_Step_Kinds:]
Effect f is Element of CQC-WFF A
len f is ext-real V20() V21() V22() V23() V27() Element of NAT
f . (len f) is set
(f . (len f)) `1 is set
n is ext-real V20() V21() V22() V23() V27() set
f . n is set
(f . n) `1 is set
H is Element of CQC-WFF A
F => H is Element of CQC-WFF A
(f . n) `2 is set
Cn X is Element of bool (CQC-WFF A)
H => (F => H) is valid Element of CQC-WFF A
(f . n) `2 is set
VERUM A is Element of CQC-WFF A
(f . n) `2 is set
i is Element of CQC-WFF A
'not' i is Element of CQC-WFF A
('not' i) => i is Element of CQC-WFF A
(('not' i) => i) => i is Element of CQC-WFF A
(f . n) `2 is set
i is Element of CQC-WFF A
'not' i is Element of CQC-WFF A
x is Element of CQC-WFF A
('not' i) => x is Element of CQC-WFF A
i => (('not' i) => x) is Element of CQC-WFF A
(f . n) `2 is set
i is Element of CQC-WFF A
x is Element of CQC-WFF A
i => x is Element of CQC-WFF A
y is Element of CQC-WFF A
x '&' y is Element of CQC-WFF A
'not' (x '&' y) is Element of CQC-WFF A
i '&' y is Element of CQC-WFF A
'not' (i '&' y) is Element of CQC-WFF A
('not' (x '&' y)) => ('not' (i '&' y)) is Element of CQC-WFF A
(i => x) => (('not' (x '&' y)) => ('not' (i '&' y))) is Element of CQC-WFF A
(f . n) `2 is set
i is Element of CQC-WFF A
x is Element of CQC-WFF A
i '&' x is Element of CQC-WFF A
x '&' i is Element of CQC-WFF A
(i '&' x) => (x '&' i) is Element of CQC-WFF A
(f . n) `2 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 bound_QC-variables A
i is Element of CQC-WFF A
All (x,i) is Element of CQC-WFF A
(All (x,i)) => i is Element of CQC-WFF A
(f . n) `2 is set
i is ext-real V20() V21() V22() V23() V27() Element of NAT
x is ext-real V20() V21() V22() V23() V27() Element of NAT
y is Element of CQC-WFF A
f . x is set
(f . x) `1 is set
s is Element of CQC-WFF A
f . i is set
(f . i) `1 is set
y => s is Element of CQC-WFF A
F => (y => s) is Element of CQC-WFF A
F => y is Element of CQC-WFF A
F => s is Element of CQC-WFF A
(F => y) => (F => s) is Element of CQC-WFF A
(F => (y => s)) => ((F => y) => (F => s)) is valid Element of CQC-WFF A
(f . n) `2 is set
QC-variables A is set
bound_QC-variables A is Element of bool (QC-variables A)
bool (QC-variables A) is set
i is ext-real V20() V21() V22() V23() V27() Element of NAT
f . i is set
(f . i) `1 is set
x is Element of CQC-WFF A
y is Element of CQC-WFF A
x => y is Element of CQC-WFF A
s is Element of bound_QC-variables A
still_not-bound_in x is Element of bool (bound_QC-variables A)
bool (bound_QC-variables A) is set
All (s,y) is Element of CQC-WFF A
x => (All (s,y)) is Element of CQC-WFF A
All (s,(x => y)) is Element of CQC-WFF A
(All (s,(x => y))) => (x => (All (s,y))) is Element of CQC-WFF A
still_not-bound_in F is Element of bool (bound_QC-variables A)
F => (x => y) is Element of CQC-WFF A
All (s,(F => (x => y))) is Element of CQC-WFF A
F => (All (s,(x => y))) is Element of CQC-WFF A
(All (s,(F => (x => y)))) => (F => (All (s,(x => y)))) is Element of CQC-WFF A
(f . n) `2 is set
QC-variables A is set
bound_QC-variables A is Element of bool (QC-variables A)
bool (QC-variables A) is set
i is ext-real V20() V21() V22() V23() V27() Element of NAT
s is Element of QC-WFF A
x is Element of bound_QC-variables A
s . x is Element of QC-WFF A
y is Element of bound_QC-variables A
s . y is Element of QC-WFF A
still_not-bound_in s is Element of bool (bound_QC-variables A)
bool (bound_QC-variables A) is set
f . i is set
(f . i) `1 is set
s1 is Element of CQC-WFF A
All (x,s1) is Element of CQC-WFF A
s2 is Element of CQC-WFF A
(All (x,s1)) => s2 is Element of CQC-WFF A
still_not-bound_in F is Element of bool (bound_QC-variables A)
F => s1 is Element of CQC-WFF A
All (x,(F => s1)) is Element of CQC-WFF A
F => (All (x,s1)) is Element of CQC-WFF A
(All (x,(F => s1))) => (F => (All (x,s1))) is Element of CQC-WFF A
(f . n) `2 is set