:: GOEDELCP semantic presentation

REAL is set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable Element of bool REAL
bool REAL is non empty set
COMPLEX is set
omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable set
bool omega is non empty set
bool NAT is non empty set
K357() is set
1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
3 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
{} is set
the empty Relation-like non-empty empty-yielding functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() V35() finite finite-yielding V42() FinSequence-like FinSequence-membered countable set is empty Relation-like non-empty empty-yielding functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() V35() finite finite-yielding V42() FinSequence-like FinSequence-membered countable set
0 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
[0,0] is V7() set
{0,0} is finite countable set
{0} is finite countable set
{{0,0},{0}} is finite V42() countable set
<*[0,0]*> is non empty Relation-like NAT -defined Function-like finite V45(1) FinSequence-like FinSubsequence-like countable set
[1,0] is V7() set
{1,0} is finite countable set
{1} is finite countable set
{{1,0},{1}} is finite V42() countable set
<*[1,0]*> is non empty Relation-like NAT -defined Function-like finite V45(1) FinSequence-like FinSubsequence-like countable set
[2,0] is V7() set
{2,0} is finite countable set
{2} is finite countable set
{{2,0},{2}} is finite V42() countable set
<*[2,0]*> is non empty Relation-like NAT -defined Function-like finite V45(1) FinSequence-like FinSubsequence-like countable set
[3,0] is V7() set
{3,0} is finite countable set
{3} is finite countable set
{{3,0},{3}} is finite V42() countable set
<*[3,0]*> is non empty Relation-like NAT -defined Function-like finite V45(1) FinSequence-like FinSubsequence-like countable set
Seg 1 is non empty finite V45(1) countable Element of bool NAT
[:NAT,NAT:] is non empty Relation-like REAL -defined REAL -valued Element of bool [:REAL,REAL:]
[:REAL,REAL:] is Relation-like set
bool [:REAL,REAL:] is non empty set
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
p is Consistent Element of bool (CQC-WFF Al)
X is Element of CQC-WFF Al
'not' X is Element of CQC-WFF Al
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
X is Element of CQC-WFF Al
'not' X is Element of CQC-WFF Al
<*X*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
p is Element of CQC-WFF Al
('not' X) 'or' p is Element of CQC-WFF Al
<*(('not' X) 'or' p)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
<*p*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Y is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Y ^ <*(('not' X) 'or' p)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Y ^ <*X*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Y ^ <*p*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
<*('not' X)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Y ^ <*('not' X)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(Y ^ <*('not' X)*>) ^ <*X*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Ant ((Y ^ <*('not' X)*>) ^ <*X*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Ant (Y ^ <*X*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Suc (Y ^ <*X*>) is Element of CQC-WFF Al
Suc ((Y ^ <*('not' X)*>) ^ <*X*>) is Element of CQC-WFF Al
(Y ^ <*('not' X)*>) ^ <*('not' X)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Ant ((Y ^ <*('not' X)*>) ^ <*('not' X)*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Suc ((Y ^ <*('not' X)*>) ^ <*('not' X)*>) is Element of CQC-WFF Al
len Y is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
(len Y) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
(Ant ((Y ^ <*('not' X)*>) ^ <*('not' X)*>)) . ((len Y) + 1) is set
len <*('not' X)*> is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
(len Y) + (len <*('not' X)*>) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
len (Ant ((Y ^ <*('not' X)*>) ^ <*('not' X)*>)) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
dom (Ant ((Y ^ <*('not' X)*>) ^ <*('not' X)*>)) is finite countable Element of bool NAT
0 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
len ((Y ^ <*('not' X)*>) ^ <*('not' X)*>) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
'not' (Suc ((Y ^ <*('not' X)*>) ^ <*X*>)) is Element of CQC-WFF Al
<*('not' (Suc ((Y ^ <*('not' X)*>) ^ <*X*>)))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(Ant ((Y ^ <*('not' X)*>) ^ <*X*>)) ^ <*('not' (Suc ((Y ^ <*('not' X)*>) ^ <*X*>)))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(Ant ((Y ^ <*('not' X)*>) ^ <*X*>)) ^ <*p*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(Y ^ <*p*>) ^ <*p*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Ant ((Y ^ <*p*>) ^ <*p*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Suc ((Y ^ <*p*>) ^ <*p*>) is Element of CQC-WFF Al
(Ant ((Y ^ <*p*>) ^ <*p*>)) . ((len Y) + 1) is set
len <*p*> is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
(len Y) + (len <*p*>) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
len (Ant ((Y ^ <*p*>) ^ <*p*>)) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
dom (Ant ((Y ^ <*p*>) ^ <*p*>)) is finite countable Element of bool NAT
(Y ^ <*(('not' X) 'or' p)*>) ^ <*p*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
'not' ('not' X) is Element of CQC-WFF Al
'not' p is Element of CQC-WFF Al
('not' ('not' X)) '&' ('not' p) is Element of CQC-WFF Al
'not' (('not' ('not' X)) '&' ('not' p)) is Element of CQC-WFF Al
<*('not' (('not' ('not' X)) '&' ('not' p)))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Y ^ <*('not' (('not' ('not' X)) '&' ('not' p)))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(Y ^ <*('not' (('not' ('not' X)) '&' ('not' p)))*>) ^ <*p*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
<*('not' p)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Y ^ <*('not' p)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
<*(('not' ('not' X)) '&' ('not' p))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(Y ^ <*('not' p)*>) ^ <*(('not' ('not' X)) '&' ('not' p))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Suc ((Y ^ <*('not' p)*>) ^ <*(('not' ('not' X)) '&' ('not' p))*>) is Element of CQC-WFF Al
Ant ((Y ^ <*('not' p)*>) ^ <*(('not' ('not' X)) '&' ('not' p))*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
<*('not' ('not' X))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(Ant ((Y ^ <*('not' p)*>) ^ <*(('not' ('not' X)) '&' ('not' p))*>)) ^ <*('not' ('not' X))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(Ant ((Y ^ <*('not' p)*>) ^ <*(('not' ('not' X)) '&' ('not' p))*>)) ^ <*('not' p)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Ant ((Ant ((Y ^ <*('not' p)*>) ^ <*(('not' ('not' X)) '&' ('not' p))*>)) ^ <*('not' ('not' X))*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Suc ((Ant ((Y ^ <*('not' p)*>) ^ <*(('not' ('not' X)) '&' ('not' p))*>)) ^ <*('not' ('not' X))*>) is Element of CQC-WFF Al
Ant ((Ant ((Y ^ <*('not' p)*>) ^ <*(('not' ('not' X)) '&' ('not' p))*>)) ^ <*('not' p)*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Suc ((Ant ((Y ^ <*('not' p)*>) ^ <*(('not' ('not' X)) '&' ('not' p))*>)) ^ <*('not' p)*>) is Element of CQC-WFF Al
(Ant ((Y ^ <*('not' p)*>) ^ <*(('not' ('not' X)) '&' ('not' p))*>)) ^ <*(('not' ('not' X)) '&' ('not' p))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
len (Y ^ <*(('not' X) 'or' p)*>) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
Ant (Y ^ <*(('not' X) 'or' p)*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(Ant (Y ^ <*(('not' X) 'or' p)*>)) ^ <*p*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
X is Element of bool (CQC-WFF Al)
p is Element of CQC-WFF Al
Y is Element of bound_QC-variables Al
Ex (Y,p) is Element of CQC-WFF Al
<*(Ex (Y,p))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
J is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
rng J is finite countable Element of bool (CQC-WFF Al)
J ^ <*(Ex (Y,p))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
'not' (Ex (Y,p)) is Element of CQC-WFF Al
v is Element of bound_QC-variables Al
p . (Y,v) is Element of CQC-WFF Al
('not' (Ex (Y,p))) 'or' (p . (Y,v)) is Element of CQC-WFF Al
<*(('not' (Ex (Y,p))) 'or' (p . (Y,v)))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
CY is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
rng CY is finite countable Element of bool (CQC-WFF Al)
CY ^ <*(('not' (Ex (Y,p))) 'or' (p . (Y,v)))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
J ^ CY is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(J ^ CY) ^ <*(Ex (Y,p))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(J ^ CY) ^ <*(('not' (Ex (Y,p))) 'or' (p . (Y,v)))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
<*(p . (Y,v))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(J ^ CY) ^ <*(p . (Y,v))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
rng (J ^ CY) is finite countable Element of bool (CQC-WFF Al)
(rng J) \/ (rng CY) is finite countable Element of bool (CQC-WFF Al)
J is Element of bound_QC-variables Al
p . (Y,J) is Element of CQC-WFF Al
<*(p . (Y,J))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
v is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
rng v is finite countable Element of bool (CQC-WFF Al)
v ^ <*(p . (Y,J))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
<*(Ex (Y,p))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
v ^ <*(Ex (Y,p))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
QC-pred_symbols Al is set
HCar Al is non empty set
K354((HCar Al)) is set
p is Consistent Element of bool (CQC-WFF Al)
X is Element of CQC-WFF Al
Y is Relation-like QC-pred_symbols Al -defined K354((HCar Al)) -valued Function-like V32( QC-pred_symbols Al,K354((HCar Al))) Henkin_interpretation of p
valH Al is Relation-like bound_QC-variables Al -defined HCar Al -valued Function-like V32( bound_QC-variables Al, HCar Al) Element of Valuations_in (Al,(HCar Al))
bound_QC-variables Al is Element of bool (QC-variables Al)
QC-variables Al is set
bool (QC-variables Al) is non empty set
Valuations_in (Al,(HCar Al)) is non empty M5( bound_QC-variables Al, HCar Al)
'not' X is Element of CQC-WFF Al
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
X is Element of CQC-WFF Al
<*X*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
p is Element of CQC-WFF Al
<*p*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
X '&' p is Element of CQC-WFF Al
<*(X '&' p)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Y is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Y ^ <*X*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Y ^ <*p*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Y ^ <*(X '&' p)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Ant (Y ^ <*X*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Suc (Y ^ <*X*>) is Element of CQC-WFF Al
Suc (Y ^ <*p*>) is Element of CQC-WFF Al
Ant (Y ^ <*p*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
X is Element of bool (CQC-WFF Al)
p is Element of CQC-WFF Al
Y is Element of CQC-WFF Al
p '&' Y is Element of CQC-WFF Al
<*p*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
J is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
rng J is finite countable Element of bool (CQC-WFF Al)
J ^ <*p*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
<*Y*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
v is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
rng v is finite countable Element of bool (CQC-WFF Al)
v ^ <*Y*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
J ^ v is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(J ^ v) ^ <*p*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(J ^ v) ^ <*Y*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
<*(p '&' Y)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(J ^ v) ^ <*(p '&' Y)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
rng (J ^ v) is finite countable Element of bool (CQC-WFF Al)
(rng J) \/ (rng v) is finite countable Element of bool (CQC-WFF Al)
<*(p '&' Y)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
J is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
rng J is finite countable Element of bool (CQC-WFF Al)
J ^ <*(p '&' Y)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
<*p*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
J ^ <*p*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
<*Y*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
J ^ <*Y*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
QC-pred_symbols Al is set
HCar Al is non empty set
K354((HCar Al)) is set
Y is Consistent Element of bool (CQC-WFF Al)
X is Element of CQC-WFF Al
J is Relation-like QC-pred_symbols Al -defined K354((HCar Al)) -valued Function-like V32( QC-pred_symbols Al,K354((HCar Al))) Henkin_interpretation of Y
valH Al is Relation-like bound_QC-variables Al -defined HCar Al -valued Function-like V32( bound_QC-variables Al, HCar Al) Element of Valuations_in (Al,(HCar Al))
bound_QC-variables Al is Element of bool (QC-variables Al)
QC-variables Al is set
bool (QC-variables Al) is non empty set
Valuations_in (Al,(HCar Al)) is non empty M5( bound_QC-variables Al, HCar Al)
p is Element of CQC-WFF Al
X '&' p is Element of CQC-WFF Al
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
QC-pred_symbols Al is set
HCar Al is non empty set
K354((HCar Al)) is set
valH Al is Relation-like bound_QC-variables Al -defined HCar Al -valued Function-like V32( bound_QC-variables Al, HCar Al) Element of Valuations_in (Al,(HCar Al))
bound_QC-variables Al is Element of bool (QC-variables Al)
QC-variables Al is set
bool (QC-variables Al) is non empty set
Valuations_in (Al,(HCar Al)) is non empty M5( bound_QC-variables Al, HCar Al)
X is Consistent Element of bool (CQC-WFF Al)
p is Relation-like QC-pred_symbols Al -defined K354((HCar Al)) -valued Function-like V32( QC-pred_symbols Al,K354((HCar Al))) Henkin_interpretation of X
VERUM Al is Element of CQC-WFF Al
Y is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
Y -ary_QC-pred_symbols Al is Element of bool (QC-pred_symbols Al)
bool (QC-pred_symbols Al) is non empty set
v is Element of Y -ary_QC-pred_symbols Al
J is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like finite V45(Y) FinSequence-like FinSubsequence-like countable FinSequence of QC-variables Al
v ! J is Element of CQC-WFF Al
CY is Element of CQC-WFF Al
'not' CY is Element of CQC-WFF Al
CY is Element of CQC-WFF Al
c₉ is Element of CQC-WFF Al
CY '&' c₉ is Element of CQC-WFF Al
Y is Element of CQC-WFF Al
QuantNbr Y is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
Y is Element of CQC-WFF Al
QuantNbr Y is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
QC-pred_symbols Al is set
X is Element of CQC-WFF Al
p is Element of bound_QC-variables Al
Ex (p,X) is Element of CQC-WFF Al
Y is non empty set
K354(Y) is set
Valuations_in (Al,Y) is non empty M5( bound_QC-variables Al,Y)
J is Relation-like QC-pred_symbols Al -defined K354(Y) -valued Function-like V32( QC-pred_symbols Al,K354(Y)) interpretation of Al,Y
v is Relation-like bound_QC-variables Al -defined Y -valued Function-like V32( bound_QC-variables Al,Y) Element of Valuations_in (Al,Y)
'not' X is Element of CQC-WFF Al
All (p,('not' X)) is Element of CQC-WFF Al
'not' (All (p,('not' X))) is Element of CQC-WFF Al
CY is Element of Y
p | CY is Relation-like bound_QC-variables Al -defined Y -valued Function-like finite countable Element of bool [:(bound_QC-variables Al),Y:]
[:(bound_QC-variables Al),Y:] is Relation-like set
bool [:(bound_QC-variables Al),Y:] is non empty set
v . (p | CY) is Relation-like bound_QC-variables Al -defined Y -valued Function-like V32( bound_QC-variables Al,Y) Element of Valuations_in (Al,Y)
CY is Element of Y
p | CY is Relation-like bound_QC-variables Al -defined Y -valued Function-like finite countable Element of bool [:(bound_QC-variables Al),Y:]
[:(bound_QC-variables Al),Y:] is Relation-like set
bool [:(bound_QC-variables Al),Y:] is non empty set
v . (p | CY) is Relation-like bound_QC-variables Al -defined Y -valued Function-like V32( bound_QC-variables Al,Y) Element of Valuations_in (Al,Y)
CY is Element of Y
p | CY is Relation-like bound_QC-variables Al -defined Y -valued Function-like finite countable Element of bool [:(bound_QC-variables Al),Y:]
[:(bound_QC-variables Al),Y:] is Relation-like set
bool [:(bound_QC-variables Al),Y:] is non empty set
v . (p | CY) is Relation-like bound_QC-variables Al -defined Y -valued Function-like V32( bound_QC-variables Al,Y) Element of Valuations_in (Al,Y)
CY is Element of Y
p | CY is Relation-like bound_QC-variables Al -defined Y -valued Function-like finite countable Element of bool [:(bound_QC-variables Al),Y:]
v . (p | CY) is Relation-like bound_QC-variables Al -defined Y -valued Function-like V32( bound_QC-variables Al,Y) Element of Valuations_in (Al,Y)
c₉ is Element of Y
p | c₉ is Relation-like bound_QC-variables Al -defined Y -valued Function-like finite countable Element of bool [:(bound_QC-variables Al),Y:]
v . (p | c₉) is Relation-like bound_QC-variables Al -defined Y -valued Function-like V32( bound_QC-variables Al,Y) Element of Valuations_in (Al,Y)
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
bool (CQC-WFF Al) is non empty set
QC-pred_symbols Al is set
HCar Al is non empty set
K354((HCar Al)) is set
valH Al is Relation-like bound_QC-variables Al -defined HCar Al -valued Function-like V32( bound_QC-variables Al, HCar Al) Element of Valuations_in (Al,(HCar Al))
Valuations_in (Al,(HCar Al)) is non empty M5( bound_QC-variables Al, HCar Al)
X is Element of CQC-WFF Al
p is Element of bound_QC-variables Al
Ex (p,X) is Element of CQC-WFF Al
Y is Consistent Element of bool (CQC-WFF Al)
J is Relation-like QC-pred_symbols Al -defined K354((HCar Al)) -valued Function-like V32( QC-pred_symbols Al,K354((HCar Al))) Henkin_interpretation of Y
v is Element of HCar Al
p | v is Relation-like bound_QC-variables Al -defined HCar Al -valued Function-like finite countable Element of bool [:(bound_QC-variables Al),(HCar Al):]
[:(bound_QC-variables Al),(HCar Al):] is Relation-like set
bool [:(bound_QC-variables Al),(HCar Al):] is non empty set
(valH Al) . (p | v) is Relation-like bound_QC-variables Al -defined HCar Al -valued Function-like V32( bound_QC-variables Al, HCar Al) Element of Valuations_in (Al,(HCar Al))
id (bound_QC-variables Al) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -valued Element of K131((bound_QC-variables Al),(bound_QC-variables Al))
K131((bound_QC-variables Al),(bound_QC-variables Al)) is set
rng (valH Al) is Element of bool (HCar Al)
bool (HCar Al) is non empty set
dom (valH Al) is Element of bool (bound_QC-variables Al)
bool (bound_QC-variables Al) is non empty set
CY is set
(valH Al) . CY is set
CY is Element of bound_QC-variables Al
X . (p,CY) is Element of CQC-WFF Al
v is Element of bound_QC-variables Al
X . (p,v) is Element of CQC-WFF Al
(valH Al) . v is set
CY is Element of HCar Al
p | CY is Relation-like bound_QC-variables Al -defined HCar Al -valued Function-like finite countable Element of bool [:(bound_QC-variables Al),(HCar Al):]
[:(bound_QC-variables Al),(HCar Al):] is Relation-like set
bool [:(bound_QC-variables Al),(HCar Al):] is non empty set
(valH Al) . (p | CY) is Relation-like bound_QC-variables Al -defined HCar Al -valued Function-like V32( bound_QC-variables Al, HCar Al) Element of Valuations_in (Al,(HCar Al))
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
QC-pred_symbols Al is set
X is Element of CQC-WFF Al
'not' X is Element of CQC-WFF Al
p is Element of bound_QC-variables Al
Ex (p,('not' X)) is Element of CQC-WFF Al
'not' (Ex (p,('not' X))) is Element of CQC-WFF Al
All (p,X) is Element of CQC-WFF Al
Y is non empty set
K354(Y) is set
Valuations_in (Al,Y) is non empty M5( bound_QC-variables Al,Y)
J is Relation-like QC-pred_symbols Al -defined K354(Y) -valued Function-like V32( QC-pred_symbols Al,K354(Y)) interpretation of Al,Y
v is Relation-like bound_QC-variables Al -defined Y -valued Function-like V32( bound_QC-variables Al,Y) Element of Valuations_in (Al,Y)
CY is Element of Y
p | CY is Relation-like bound_QC-variables Al -defined Y -valued Function-like finite countable Element of bool [:(bound_QC-variables Al),Y:]
[:(bound_QC-variables Al),Y:] is Relation-like set
bool [:(bound_QC-variables Al),Y:] is non empty set
v . (p | CY) is Relation-like bound_QC-variables Al -defined Y -valued Function-like V32( bound_QC-variables Al,Y) Element of Valuations_in (Al,Y)
CY is Element of Y
p | CY is Relation-like bound_QC-variables Al -defined Y -valued Function-like finite countable Element of bool [:(bound_QC-variables Al),Y:]
[:(bound_QC-variables Al),Y:] is Relation-like set
bool [:(bound_QC-variables Al),Y:] is non empty set
v . (p | CY) is Relation-like bound_QC-variables Al -defined Y -valued Function-like V32( bound_QC-variables Al,Y) Element of Valuations_in (Al,Y)
CY is Element of Y
p | CY is Relation-like bound_QC-variables Al -defined Y -valued Function-like finite countable Element of bool [:(bound_QC-variables Al),Y:]
[:(bound_QC-variables Al),Y:] is Relation-like set
bool [:(bound_QC-variables Al),Y:] is non empty set
v . (p | CY) is Relation-like bound_QC-variables Al -defined Y -valued Function-like V32( bound_QC-variables Al,Y) Element of Valuations_in (Al,Y)
CY is Element of Y
p | CY is Relation-like bound_QC-variables Al -defined Y -valued Function-like finite countable Element of bool [:(bound_QC-variables Al),Y:]
[:(bound_QC-variables Al),Y:] is Relation-like set
bool [:(bound_QC-variables Al),Y:] is non empty set
v . (p | CY) is Relation-like bound_QC-variables Al -defined Y -valued Function-like V32( bound_QC-variables Al,Y) Element of Valuations_in (Al,Y)
CY is Element of Y
p | CY is Relation-like bound_QC-variables Al -defined Y -valued Function-like finite countable Element of bool [:(bound_QC-variables Al),Y:]
v . (p | CY) is Relation-like bound_QC-variables Al -defined Y -valued Function-like V32( bound_QC-variables Al,Y) Element of Valuations_in (Al,Y)
c₉ is Element of Y
p | c₉ is Relation-like bound_QC-variables Al -defined Y -valued Function-like finite countable Element of bool [:(bound_QC-variables Al),Y:]
v . (p | c₉) is Relation-like bound_QC-variables Al -defined Y -valued Function-like V32( bound_QC-variables Al,Y) Element of Valuations_in (Al,Y)
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
X is Element of bool (CQC-WFF Al)
p is Element of CQC-WFF Al
'not' p is Element of CQC-WFF Al
Y is Element of bound_QC-variables Al
Ex (Y,('not' p)) is Element of CQC-WFF Al
'not' (Ex (Y,('not' p))) is Element of CQC-WFF Al
All (Y,p) is Element of CQC-WFF Al
<*('not' (Ex (Y,('not' p))))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
J is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
rng J is finite countable Element of bool (CQC-WFF Al)
J ^ <*('not' (Ex (Y,('not' p))))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
<*(All (Y,p))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
J ^ <*(All (Y,p))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
<*(All (Y,p))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
J is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
rng J is finite countable Element of bool (CQC-WFF Al)
J ^ <*(All (Y,p))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
<*('not' (Ex (Y,('not' p))))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
J ^ <*('not' (Ex (Y,('not' p))))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
X is Element of CQC-WFF Al
QuantNbr X is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
(QuantNbr X) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
p is Element of bound_QC-variables Al
Ex (p,X) is Element of CQC-WFF Al
QuantNbr (Ex (p,X)) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
'not' X is Element of CQC-WFF Al
All (p,('not' X)) is Element of CQC-WFF Al
'not' (All (p,('not' X))) is Element of CQC-WFF Al
QuantNbr ('not' (All (p,('not' X)))) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
QuantNbr (All (p,('not' X))) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
QuantNbr ('not' X) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
(QuantNbr ('not' X)) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
X is Element of CQC-WFF Al
QuantNbr X is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
p is Element of bound_QC-variables Al
Y is Element of bound_QC-variables Al
X . (p,Y) is Element of CQC-WFF Al
QuantNbr (X . (p,Y)) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
Sbst (p,Y) is finite countable Element of vSUB Al
vSUB Al is set
[X,(Sbst (p,Y))] is V7() Element of CQC-Sub-WFF Al
QC-Sub-WFF Al is non empty set
CQC-Sub-WFF Al is Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
{X,(Sbst (p,Y))} is finite countable set
{X} is finite countable set
{{X,(Sbst (p,Y))},{X}} is finite V42() countable set
CQC_Sub [X,(Sbst (p,Y))] is Element of CQC-WFF Al
QuantNbr (CQC_Sub [X,(Sbst (p,Y))]) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
QC-pred_symbols Al is set
HCar Al is non empty set
K354((HCar Al)) is set
valH Al is Relation-like bound_QC-variables Al -defined HCar Al -valued Function-like V32( bound_QC-variables Al, HCar Al) Element of Valuations_in (Al,(HCar Al))
bound_QC-variables Al is Element of bool (QC-variables Al)
QC-variables Al is set
bool (QC-variables Al) is non empty set
Valuations_in (Al,(HCar Al)) is non empty M5( bound_QC-variables Al, HCar Al)
X is Consistent Element of bool (CQC-WFF Al)
p is Relation-like QC-pred_symbols Al -defined K354((HCar Al)) -valued Function-like V32( QC-pred_symbols Al,K354((HCar Al))) Henkin_interpretation of X
Y is Element of CQC-WFF Al
QuantNbr Y is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
J is Element of CQC-WFF Al
v is Element of bound_QC-variables Al
CY is Element of CQC-WFF Al
All (v,CY) is Element of CQC-WFF Al
v is Element of bound_QC-variables Al
CY is Element of CQC-WFF Al
All (v,CY) is Element of CQC-WFF Al
QuantNbr J is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
QuantNbr CY is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
(QuantNbr CY) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
the Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable PATH of J,Y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable PATH of J,Y
len the Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable PATH of J,Y is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
the Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable PATH of J,Y . 0 is set
c₉ is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
the Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable PATH of J,Y . c₉ is set
c₉ + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
the Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable PATH of J,Y . (c₉ + 1) is set
y is Element of CQC-WFF Al
QuantNbr y is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
'not' CY is Element of CQC-WFF Al
Ex (v,('not' CY)) is Element of CQC-WFF Al
c₁₂ is Element of bound_QC-variables Al
('not' CY) . (v,c₁₂) is Element of CQC-WFF Al
QuantNbr ('not' CY) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
QuantNbr (('not' CY) . (v,c₁₂)) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
c₁₂ is Element of bound_QC-variables Al
('not' CY) . (v,c₁₂) is Element of CQC-WFF Al
QuantNbr (('not' CY) . (v,c₁₂)) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
'not' (Ex (v,('not' CY))) is Element of CQC-WFF Al
0 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
y is Element of QC-WFF Al
c₁₂ is Element of QC-WFF Al
f1 is Element of CQC-WFF Al
QuantNbr f1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
f1 is Element of CQC-WFF Al
QuantNbr f1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
k1 is Element of CQC-WFF Al
k1 is Element of CQC-WFF Al
'not' f1 is Element of CQC-WFF Al
QuantNbr k1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
K is Element of QC-WFF Al
K is Element of QC-WFF Al
f1 '&' K is Element of QC-WFF Al
r1 is Element of CQC-WFF Al
QuantNbr r1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
(QuantNbr f1) + (QuantNbr r1) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
1 - 1 is ext-real V30() V35() set
(QuantNbr r1) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
((QuantNbr r1) + 1) - 1 is ext-real V30() V35() set
K is Element of QC-WFF Al
K '&' f1 is Element of QC-WFF Al
r1 is Element of CQC-WFF Al
QuantNbr r1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
(QuantNbr f1) + (QuantNbr r1) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
K is Element of bound_QC-variables Al
All (K,f1) is Element of CQC-WFF Al
(QuantNbr f1) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
K is Element of CQC-WFF Al
QuantNbr K is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
r1 is Element of CQC-WFF Al
QuantNbr r1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
L is Element of CQC-WFF Al
QuantNbr L is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
c₁₂ is Element of CQC-WFF Al
QuantNbr c₁₂ is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
f1 is Element of CQC-WFF Al
QuantNbr f1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
k1 is Element of CQC-WFF Al
QuantNbr k1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
the Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable PATH of J,Y . (len the Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable PATH of J,Y) is set
c₉ is Element of CQC-WFF Al
QuantNbr c₉ is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
QC-pred_symbols Al is set
HCar Al is non empty set
K354((HCar Al)) is set
valH Al is Relation-like bound_QC-variables Al -defined HCar Al -valued Function-like V32( bound_QC-variables Al, HCar Al) Element of Valuations_in (Al,(HCar Al))
bound_QC-variables Al is Element of bool (QC-variables Al)
QC-variables Al is set
bool (QC-variables Al) is non empty set
Valuations_in (Al,(HCar Al)) is non empty M5( bound_QC-variables Al, HCar Al)
X is Consistent Element of bool (CQC-WFF Al)
p is Relation-like QC-pred_symbols Al -defined K354((HCar Al)) -valued Function-like V32( QC-pred_symbols Al,K354((HCar Al))) Henkin_interpretation of X
Y is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
Y + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
J is Element of CQC-WFF Al
QuantNbr J is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
v is Element of CQC-WFF Al
QuantNbr v is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
the Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable PATH of v,J is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable PATH of v,J
len the Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable PATH of v,J is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
the Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable PATH of v,J . 0 is set
CY is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
the Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable PATH of v,J . CY is set
CY + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
the Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable PATH of v,J . (CY + 1) is set
p is Element of CQC-WFF Al
0 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
p is Element of QC-WFF Al
y is Element of QC-WFF Al
c₁₂ is Element of CQC-WFF Al
QuantNbr c₁₂ is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
c₁₂ is Element of CQC-WFF Al
QuantNbr c₁₂ is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
f1 is Element of CQC-WFF Al
k1 is Element of CQC-WFF Al
'not' c₁₂ is Element of CQC-WFF Al
QuantNbr k1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
k1 is Element of QC-WFF Al
k1 is Element of QC-WFF Al
c₁₂ '&' k1 is Element of QC-WFF Al
K is Element of CQC-WFF Al
QuantNbr K is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
(QuantNbr c₁₂) + (QuantNbr K) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
1 + (QuantNbr K) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
(QuantNbr K) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
- 1 is ext-real non positive V30() V35() set
((QuantNbr K) + 1) + (- 1) is ext-real V30() V35() set
(Y + 1) + (- 1) is ext-real V30() V35() set
k1 is Element of QC-WFF Al
k1 '&' c₁₂ is Element of QC-WFF Al
K is Element of CQC-WFF Al
QuantNbr K is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
(QuantNbr c₁₂) + (QuantNbr K) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
1 + (QuantNbr K) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
(QuantNbr K) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
((QuantNbr K) + 1) + (- 1) is ext-real V30() V35() set
k1 is Element of bound_QC-variables Al
All (k1,c₁₂) is Element of CQC-WFF Al
(QuantNbr c₁₂) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
QuantNbr ('not' c₁₂) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
Ex (k1,('not' c₁₂)) is Element of CQC-WFF Al
K is Element of bound_QC-variables Al
('not' c₁₂) . (k1,K) is Element of CQC-WFF Al
QuantNbr (('not' c₁₂) . (k1,K)) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
K is Element of bound_QC-variables Al
('not' c₁₂) . (k1,K) is Element of CQC-WFF Al
QuantNbr (('not' c₁₂) . (k1,K)) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
'not' (Ex (k1,('not' c₁₂))) is Element of CQC-WFF Al
k1 is Element of CQC-WFF Al
QuantNbr k1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
K is Element of CQC-WFF Al
QuantNbr K is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
r1 is Element of CQC-WFF Al
QuantNbr r1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
L is Element of CQC-WFF Al
QuantNbr L is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
y is Element of CQC-WFF Al
QuantNbr y is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
f1 is Element of CQC-WFF Al
QuantNbr f1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
the Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable PATH of v,J . (len the Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable PATH of v,J) is set
CY is Element of CQC-WFF Al
QuantNbr CY is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
QC-pred_symbols Al is set
HCar Al is non empty set
K354((HCar Al)) is set
valH Al is Relation-like bound_QC-variables Al -defined HCar Al -valued Function-like V32( bound_QC-variables Al, HCar Al) Element of Valuations_in (Al,(HCar Al))
bound_QC-variables Al is Element of bool (QC-variables Al)
QC-variables Al is set
bool (QC-variables Al) is non empty set
Valuations_in (Al,(HCar Al)) is non empty M5( bound_QC-variables Al, HCar Al)
X is Consistent Element of bool (CQC-WFF Al)
p is Relation-like QC-pred_symbols Al -defined K354((HCar Al)) -valued Function-like V32( QC-pred_symbols Al,K354((HCar Al))) Henkin_interpretation of X
Y is Element of CQC-WFF Al
QuantNbr Y is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
Y is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
J is Element of CQC-WFF Al
QuantNbr J is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
Y + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
Al is QC-alphabet
QC-WFF Al is non empty set
QC-symbols Al is non empty set
[:NAT,(QC-symbols Al):] is non empty Relation-like set
[:NAT,(QC-symbols Al):] * is non empty functional FinSequence-membered set
bool ([:NAT,(QC-symbols Al):] *) is non empty set
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
X is set
p is set
p is Element of bool (CQC-WFF Al)
Y is set
J is set
v is Element of bound_QC-variables Al
CY is Element of CQC-WFF Al
Ex (v,CY) is Element of CQC-WFF Al
X is Element of bool (CQC-WFF Al)
p is Element of bool (CQC-WFF Al)
Y is set
J is Element of bound_QC-variables Al
v is Element of CQC-WFF Al
Ex (J,v) is Element of CQC-WFF Al
J is Element of bound_QC-variables Al
v is Element of CQC-WFF Al
Ex (J,v) is Element of CQC-WFF Al
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
Al is QC-alphabet
(Al) is Element of bool (CQC-WFF Al)
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
the Element of bound_QC-variables Al is Element of bound_QC-variables Al
the Element of CQC-WFF Al is Element of CQC-WFF Al
Ex ( the Element of bound_QC-variables Al, the Element of CQC-WFF Al) is Element of CQC-WFF Al
Al is non empty set
[:NAT,Al:] is non empty Relation-like set
bool [:NAT,Al:] is non empty set
X is Relation-like NAT -defined Al -valued Function-like V32( NAT ,Al) Element of bool [:NAT,Al:]
rng X is Element of bool Al
bool Al is non empty set
dom X is countable Element of bool NAT
Al is QC-alphabet
QC-WFF Al is non empty set
X is Element of QC-WFF Al
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
p is Element of bound_QC-variables Al
J is Element of QC-WFF Al
Ex (p,J) is Element of QC-WFF Al
Y is Element of bound_QC-variables Al
v is Element of QC-WFF Al
Ex (Y,v) is Element of QC-WFF Al
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
X is Element of CQC-WFF Al
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
p is Element of bound_QC-variables Al
Y is Element of QC-WFF Al
Ex (p,Y) is Element of QC-WFF Al
'not' Y is Element of QC-WFF Al
All (p,('not' Y)) is Element of QC-WFF Al
'not' (All (p,('not' Y))) is Element of QC-WFF Al
J is Element of bound_QC-variables Al
p is Element of CQC-WFF Al
Ex (J,p) is Element of CQC-WFF Al
v is Element of bound_QC-variables Al
Y is Element of CQC-WFF Al
Ex (v,Y) is Element of CQC-WFF Al
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
[:NAT,(CQC-WFF Al):] is non empty Relation-like set
bool [:NAT,(CQC-WFF Al):] is non empty set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
X is Relation-like NAT -defined CQC-WFF Al -valued Function-like V32( NAT , CQC-WFF Al) Element of bool [:NAT,(CQC-WFF Al):]
p is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
X . p is Element of CQC-WFF Al
Y is Element of CQC-WFF Al
(Al,Y) is Element of bound_QC-variables Al
J is Element of CQC-WFF Al
(Al,J) is Element of bound_QC-variables Al
Y is Element of bound_QC-variables Al
J is Element of bound_QC-variables Al
v is Element of CQC-WFF Al
(Al,v) is Element of bound_QC-variables Al
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
[:NAT,(CQC-WFF Al):] is non empty Relation-like set
bool [:NAT,(CQC-WFF Al):] is non empty set
X is Relation-like NAT -defined CQC-WFF Al -valued Function-like V32( NAT , CQC-WFF Al) Element of bool [:NAT,(CQC-WFF Al):]
p is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
X . p is Element of CQC-WFF Al
Y is Element of CQC-WFF Al
(Al,Y) is Element of CQC-WFF Al
J is Element of CQC-WFF Al
(Al,J) is Element of CQC-WFF Al
Y is Element of CQC-WFF Al
J is Element of CQC-WFF Al
v is Element of CQC-WFF Al
(Al,v) is Element of CQC-WFF Al
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
X is Element of bool (CQC-WFF Al)
{ (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in X } is set
union { (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in X } is set
bound_QC-variables Al is Element of bool (QC-variables Al)
QC-variables Al is set
bool (QC-variables Al) is non empty set
bool (bound_QC-variables Al) is non empty set
Y is set
J is set
v is Element of CQC-WFF Al
still_not-bound_in v is Element of bool (bound_QC-variables Al)
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
X is Element of bool (CQC-WFF Al)
p is Element of CQC-WFF Al
Y is set
<*p*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
rng <*p*> is non empty finite countable Element of bool (CQC-WFF Al)
{p} is finite countable Element of bool (CQC-WFF Al)
<*> (CQC-WFF Al) is empty proper Relation-like non-empty empty-yielding NAT -defined CQC-WFF Al -valued Function-like functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() V35() finite finite-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable FinSequence of CQC-WFF Al
[:NAT,(CQC-WFF Al):] is non empty Relation-like set
(<*> (CQC-WFF Al)) ^ <*p*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
((<*> (CQC-WFF Al)) ^ <*p*>) ^ <*p*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
<*p*> ^ <*p*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1 + 1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
1 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
X is Element of CQC-WFF Al
p is Element of bound_QC-variables Al
Ex (p,X) is Element of CQC-WFF Al
(Al,(Ex (p,X))) is Element of bound_QC-variables Al
(Al,(Ex (p,X))) is Element of CQC-WFF Al
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
VERUM Al is Element of CQC-WFF Al
X is Element of bool (CQC-WFF Al)
<*> (CQC-WFF Al) is empty proper Relation-like non-empty empty-yielding NAT -defined CQC-WFF Al -valued Function-like functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() V35() finite finite-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable FinSequence of CQC-WFF Al
[:NAT,(CQC-WFF Al):] is non empty Relation-like set
rng (<*> (CQC-WFF Al)) is empty proper Relation-like non-empty empty-yielding functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() V35() finite finite-yielding V42() FinSequence-like FinSequence-membered countable Element of bool (CQC-WFF Al)
<*(VERUM Al)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(<*> (CQC-WFF Al)) ^ <*(VERUM Al)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
VERUM Al is Element of CQC-WFF Al
'not' (VERUM Al) is Element of CQC-WFF Al
X is Element of bool (CQC-WFF Al)
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
X is Element of CQC-WFF Al
<*X*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
p is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
len p is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
p ^ <*X*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Ant p is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Y is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(Ant p) ^ Y is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Suc p is Element of CQC-WFF Al
<*(Suc p)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
((Ant p) ^ Y) ^ <*(Suc p)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(((Ant p) ^ Y) ^ <*(Suc p)*>) ^ <*X*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Ant (p ^ <*X*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Ant ((((Ant p) ^ Y) ^ <*(Suc p)*>) ^ <*X*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Suc (p ^ <*X*>) is Element of CQC-WFF Al
Suc ((((Ant p) ^ Y) ^ <*(Suc p)*>) ^ <*X*>) is Element of CQC-WFF Al
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
X is Element of CQC-WFF Al
{X} is finite countable Element of bool (CQC-WFF Al)
bool (CQC-WFF Al) is non empty set
(Al,{X}) is Element of bool (bound_QC-variables Al)
bound_QC-variables Al is Element of bool (QC-variables Al)
QC-variables Al is set
bool (QC-variables Al) is non empty set
bool (bound_QC-variables Al) is non empty set
{ (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in {X} } is set
union { (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in {X} } is set
still_not-bound_in X is Element of bool (bound_QC-variables Al)
p is set
Y is set
J is Element of CQC-WFF Al
still_not-bound_in J is Element of bool (bound_QC-variables Al)
p is set
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
bound_QC-variables Al is Element of bool (QC-variables Al)
QC-variables Al is set
bool (QC-variables Al) is non empty set
X is Element of bool (CQC-WFF Al)
(Al,X) is Element of bool (bound_QC-variables Al)
bool (bound_QC-variables Al) is non empty set
{ (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in X } is set
union { (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in X } is set
p is Element of bool (CQC-WFF Al)
X \/ p is Element of bool (CQC-WFF Al)
(Al,(X \/ p)) is Element of bool (bound_QC-variables Al)
{ (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in X \/ p } is set
union { (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in X \/ p } is set
(Al,p) is Element of bool (bound_QC-variables Al)
{ (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in p } is set
union { (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in p } is set
(Al,X) \/ (Al,p) is Element of bool (bound_QC-variables Al)
J is set
v is set
CY is Element of CQC-WFF Al
still_not-bound_in CY is Element of bool (bound_QC-variables Al)
Y is set
J is set
v is Element of CQC-WFF Al
still_not-bound_in v is Element of bool (bound_QC-variables Al)
J is set
v is Element of CQC-WFF Al
still_not-bound_in v is Element of bool (bound_QC-variables Al)
Al is QC-alphabet
bound_QC-variables Al is Element of bool (QC-variables Al)
QC-variables Al is set
bool (QC-variables Al) is non empty set
bool (bound_QC-variables Al) is non empty set
X is Element of bool (bound_QC-variables Al)
p is set
Y is set
p is set
Y is Element of bound_QC-variables Al
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
X is Element of bool (CQC-WFF Al)
(Al,X) is Element of bool (bound_QC-variables Al)
bound_QC-variables Al is Element of bool (QC-variables Al)
QC-variables Al is set
bool (QC-variables Al) is non empty set
bool (bound_QC-variables Al) is non empty set
{ (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in X } is set
union { (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in X } is set
p is Element of bool (CQC-WFF Al)
(Al,p) is Element of bool (bound_QC-variables Al)
{ (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in p } is set
union { (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in p } is set
J is set
v is set
CY is Element of CQC-WFF Al
still_not-bound_in CY is Element of bool (bound_QC-variables Al)
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
X is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
rng X is finite countable Element of bool (CQC-WFF Al)
bool (CQC-WFF Al) is non empty set
(Al,(rng X)) is Element of bool (bound_QC-variables Al)
bound_QC-variables Al is Element of bool (QC-variables Al)
QC-variables Al is set
bool (QC-variables Al) is non empty set
bool (bound_QC-variables Al) is non empty set
{ (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in rng X } is set
union { (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in rng X } is set
still_not-bound_in X is Element of bool (bound_QC-variables Al)
Y is set
J is set
v is Element of CQC-WFF Al
still_not-bound_in v is Element of bool (bound_QC-variables Al)
dom X is finite countable Element of bool NAT
CY is set
X . CY is set
Y is set
J is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
v is Element of CQC-WFF Al
X . J is set
still_not-bound_in v is Element of bool (bound_QC-variables Al)
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
X is Consistent Element of bool (CQC-WFF Al)
(Al,X) is Element of bool (bound_QC-variables Al)
bound_QC-variables Al is Element of bool (QC-variables Al)
QC-variables Al is set
bool (QC-variables Al) is non empty set
bool (bound_QC-variables Al) is non empty set
{ (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in X } is set
union { (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in X } is set
(Al) is Element of bool (CQC-WFF Al)
p is Relation-like Function-like set
dom p is set
rng p is set
[:NAT,(CQC-WFF Al):] is non empty Relation-like set
bool [:NAT,(CQC-WFF Al):] is non empty set
Y is Relation-like NAT -defined CQC-WFF Al -valued Function-like V32( NAT , CQC-WFF Al) Element of bool [:NAT,(CQC-WFF Al):]
QC-symbols Al is non empty set
[:(CQC-WFF Al),(bool (bound_QC-variables Al)):] is non empty Relation-like set
J is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
J + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
Y . (J + 1) is Element of CQC-WFF Al
{(Y . (J + 1))} is finite countable Element of bool (CQC-WFF Al)
(Al,{(Y . (J + 1))}) is Element of bool (bound_QC-variables Al)
{ (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in {(Y . (J + 1))} } is set
union { (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in {(Y . (J + 1))} } is set
'not' (Y . (J + 1)) is Element of CQC-WFF Al
(Al,Y,(J + 1)) is Element of CQC-WFF Al
(Al,Y,(J + 1)) is Element of bound_QC-variables Al
v is Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):]
v `2 is set
c₉ is set
p is set
[c₉,p] is V7() set
{c₉,p} is finite countable set
{c₉} is finite countable set