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

CY '&' c

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

p | c

v . (p | c

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

p | c

v . (p | c

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

the Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable PATH of J,Y . c

c

the Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable PATH of J,Y . (c

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

('not' CY) . (v,c

QuantNbr ('not' CY) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT

QuantNbr (('not' CY) . (v,c

c

('not' CY) . (v,c

QuantNbr (('not' CY) . (v,c

'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

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

QuantNbr c

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

QuantNbr c

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

QuantNbr c

c

QuantNbr c

f1 is Element of CQC-WFF Al

k1 is Element of CQC-WFF Al

'not' c

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

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

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

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

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

(QuantNbr c

QuantNbr ('not' c

Ex (k1,('not' c

K is Element of bound_QC-variables Al

('not' c

QuantNbr (('not' c

K is Element of bound_QC-variables Al

('not' c

QuantNbr (('not' c

'not' (Ex (k1,('not' c

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

union { (still_not-bound_in b

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

union { (still_not-bound_in b

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

union { (still_not-bound_in b

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

union { (still_not-bound_in b

(Al,p) is Element of bool (bound_QC-variables Al)

{ (still_not-bound_in b

union { (still_not-bound_in b

(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

union { (still_not-bound_in b

p is Element of bool (CQC-WFF Al)

(Al,p) is Element of bool (bound_QC-variables Al)

{ (still_not-bound_in b

union { (still_not-bound_in b

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

union { (still_not-bound_in b

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

union { (still_not-bound_in b

(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

union { (still_not-bound_in b

'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

p is set

[c

{c

{c