:: HENMODEL semantic presentation

REAL is set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal Element of bool REAL
bool REAL is non empty set
omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal set
bool omega is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
BOOLEAN is set
{} is set
the empty Function-like functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V32() V37() integer finite V43() cardinal {} -element FinSequence-membered set is empty Function-like functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V32() V37() integer finite V43() cardinal {} -element FinSequence-membered set
1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V32() V37() integer finite cardinal Element of NAT
2 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V32() V37() integer finite cardinal Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V32() V37() integer finite cardinal Element of NAT
0 is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
Seg 1 is non empty trivial finite 1 -element Element of bool NAT
TRUE is Element of BOOLEAN
Proof_Step_Kinds is set
4 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V32() V37() integer finite cardinal Element of NAT
5 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V32() V37() integer finite cardinal Element of NAT
6 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V32() V37() integer finite cardinal Element of NAT
7 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V32() V37() integer finite cardinal Element of NAT
8 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V32() V37() integer finite cardinal Element of NAT
9 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V32() V37() integer finite cardinal Element of NAT
Al is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
union Al is epsilon-transitive epsilon-connected ordinal set
k is non empty finite Element of bool NAT
[:Al,k:] is finite set
bool [:Al,k:] is non empty finite V43() set
P is Relation-like Al -defined k -valued Function-like quasi_total finite Element of bool [:Al,k:]
rng P is finite Element of bool k
bool k is non empty finite V43() set
dom P is finite Element of bool Al
bool Al is non empty finite V43() set
P . (union Al) is set
union (rng P) is set
ll is set
CX is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
succ CX is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of omega
CX is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
succ CX is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of omega
P . CX is set
ll is set
CX is set
JH is set
P . JH is set
rel is epsilon-transitive epsilon-connected ordinal set
fin9 is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
succ fin9 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of omega
fin9 is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
succ fin9 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of omega
rel is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
P . rel is set
P . fin9 is set
a is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
i is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT : not fin9 <= b₁ } is set
a is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
Al is non empty finite Element of bool NAT
union Al is set
RelIncl Al is Relation-like finite set
k is epsilon-transitive epsilon-connected ordinal set
RelIncl k is Relation-like set
P is Relation-like Function-like set
dom P is set
field (RelIncl Al) is finite set
ll is set
rng P is set
field (RelIncl k) is set
P . ll is set
CX is Relation-like Function-like set
dom CX is set
JH is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
CX . JH is set
rel is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
CX . rel is set
rng CX is set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT : not JH <= b₁ } is set
[rel,JH] is V26() Element of [:NAT,NAT:]
[:NAT,NAT:] is non empty non trivial non finite set
{rel,JH} is finite V43() set
{rel} is non empty trivial finite V43() 1 -element set
{{rel,JH},{rel}} is finite V43() set
[(CX . rel),(CX . JH)] is V26() set
{(CX . rel),(CX . JH)} is finite set
{(CX . rel)} is non empty trivial finite 1 -element set
{{(CX . rel),(CX . JH)},{(CX . rel)}} is finite V43() set
rel is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
fin9 is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
JH is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
RelIncl JH is Relation-like finite set
field (RelIncl JH) is finite set
rel is epsilon-transitive epsilon-connected ordinal set
succ rel is non empty epsilon-transitive epsilon-connected ordinal set
rel is epsilon-transitive epsilon-connected ordinal set
succ rel is non empty epsilon-transitive epsilon-connected ordinal set
rel is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
succ rel is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of omega
rel is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
succ rel is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of omega
rel is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
succ rel is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of omega
rng CX is set
[:JH,Al:] is finite set
bool [:JH,Al:] is non empty finite V43() set
rel is Relation-like JH -defined Al -valued Function-like quasi_total finite Element of bool [:JH,Al:]
dom rel is finite Element of bool JH
bool JH is non empty finite V43() set
a is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
fin9 is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
rel . fin9 is set
rel . a is set
rng rel is finite Element of bool Al
bool Al is non empty finite V43() set
union JH is epsilon-transitive epsilon-connected ordinal set
rel . (union JH) is set
union (rng rel) is set
fin9 is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
succ fin9 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of omega
fin9 is set
a is set
rel . a is set
i is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT : not rel <= b₁ } is set
C is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
Al is non empty set
[:NAT,Al:] is non empty non trivial non finite set
bool [:NAT,Al:] is non empty non trivial non finite set
k is Relation-like NAT -defined Al -valued Function-like quasi_total Element of bool [:NAT,Al:]
dom k is Element of bool NAT
rng k is Element of bool Al
bool Al is non empty set
union (rng k) is set
P is finite set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT : a₁ in k . b₁ } is set
min* { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT : a₁ in k . b₁ } is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
ll is Relation-like Function-like set
dom ll is set
rng ll is set
JH is set
CX is finite set
rel is set
ll . rel is set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT : rel in k . b₁ } is set
min* { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT : rel in k . b₁ } is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
rel is set
JH is non empty finite Element of bool NAT
union JH is set
rel is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
rel is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
k . rel is Element of Al
fin9 is set
a is set
i is set
k . i is set
C is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT : fin9 in k . b₁ } is set
F is set
F is non empty set
F is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
k . F is Element of Al
ll . fin9 is set
F is non empty Element of bool NAT
min* F is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
F is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT : not rel <= b₁ } is set
k . F is Element of Al
F is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
F is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
k . F is Element of Al
F is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
k . F is Element of Al
ll is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
k . ll is Element of Al
CX is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
k . CX is Element of Al
JH is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
k . JH is Element of Al
Al is non empty Relation-like 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 non empty Relation-like 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 non empty Relation-like 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 non empty Relation-like 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 non empty Relation-like 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 non empty Relation-like 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
k is Element of bool (CQC-WFF Al)
P is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
rng P is finite Element of bool (CQC-WFF Al)
ll is Element of CQC-WFF Al
<*ll*> is non empty trivial Relation-like NAT -defined CQC-WFF Al -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
P ^ <*ll*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
'not' ll is Element of CQC-WFF Al
<*('not' ll)*> is non empty trivial Relation-like NAT -defined CQC-WFF Al -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
P ^ <*('not' ll)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Al is non empty Relation-like 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
k is Element of CQC-WFF Al
<*k*> is non empty trivial Relation-like NAT -defined CQC-WFF Al -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
P is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
P ^ <*k*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
ll is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
P ^ ll is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(P ^ ll) ^ <*k*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Ant (P ^ <*k*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Ant ((P ^ ll) ^ <*k*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Suc ((P ^ ll) ^ <*k*>) is Element of CQC-WFF Al
Suc (P ^ <*k*>) is Element of CQC-WFF Al
Al is non empty Relation-like 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
k is Element of bool (CQC-WFF Al)
P is Element of CQC-WFF Al
'not' P is Element of CQC-WFF Al
<*('not' P)*> is non empty trivial Relation-like NAT -defined CQC-WFF Al -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
ll is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
rng ll is finite Element of bool (CQC-WFF Al)
ll ^ <*('not' P)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
CX is Element of CQC-WFF Al
<*P*> is non empty trivial Relation-like NAT -defined CQC-WFF Al -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
JH is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
rng JH is finite Element of bool (CQC-WFF Al)
JH ^ <*P*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
JH ^ ll is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
rel is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
rng rel is finite Element of bool (CQC-WFF Al)
<*CX*> is non empty trivial Relation-like NAT -defined CQC-WFF Al -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
rel ^ <*CX*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(rng JH) \/ (rng ll) is finite Element of bool (CQC-WFF Al)
(JH ^ ll) ^ <*('not' P)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(JH ^ ll) ^ <*P*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
VERUM Al is Element of CQC-WFF Al
'not' (VERUM Al) is Element of CQC-WFF Al
Al is non empty Relation-like 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
k is Element of bool (CQC-WFF Al)
P is Element of CQC-WFF Al
'not' P is Element of CQC-WFF Al
<*P*> is non empty trivial Relation-like NAT -defined CQC-WFF Al -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
ll is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
rng ll is finite Element of bool (CQC-WFF Al)
ll ^ <*P*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
<*('not' P)*> is non empty trivial Relation-like NAT -defined CQC-WFF Al -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
CX is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
rng CX is finite Element of bool (CQC-WFF Al)
CX ^ <*('not' P)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
ll ^ CX is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
rng (ll ^ CX) is finite Element of bool (CQC-WFF Al)
JH is Element of bool (CQC-WFF Al)
(rng ll) \/ (rng CX) is finite Element of bool (CQC-WFF Al)
(ll ^ CX) ^ <*('not' P)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(ll ^ CX) ^ <*P*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Al is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Al ^ k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len (Al ^ k) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
Seg (len (Al ^ k)) is finite len (Al ^ k) -element Element of bool NAT
len Al is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
Seg (len Al) is finite len Al -element Element of bool NAT
len k is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
seq ((len Al),(len k)) is Element of bool NAT
(Seg (len Al)) \/ (seq ((len Al),(len k))) is Element of bool NAT
dom (Al ^ k) is finite Element of bool NAT
dom Al is finite Element of bool NAT
(dom Al) \/ (seq ((len Al),(len k))) is Element of bool NAT
Al is non empty Relation-like 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
k is Element of bool (CQC-WFF Al)
P is Element of CQC-WFF Al
{P} is non empty trivial finite 1 -element Element of bool (CQC-WFF Al)
k \/ {P} is Element of bool (CQC-WFF Al)
<*P*> is non empty trivial Relation-like NAT -defined CQC-WFF Al -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
ll is Element of CQC-WFF Al
<*ll*> is non empty trivial Relation-like NAT -defined CQC-WFF Al -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
CX is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
rng CX is finite Element of bool (CQC-WFF Al)
CX ^ <*ll*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
CX - {P} is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
CX " {P} is finite Element of bool NAT
dom CX is finite Element of bool NAT
rel is finite set
card rel is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of omega
IdFinS (P,(card rel)) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite card rel -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Seg (card rel) is finite card rel -element Element of bool NAT
K253((Seg (card rel)),P) is Relation-like Seg (card rel) -defined {P} -valued Function-like quasi_total finite FinSequence-like FinSubsequence-like Element of bool [:(Seg (card rel)),{P}:]
{P} is non empty trivial finite 1 -element set
[:(Seg (card rel)),{P}:] is finite set
bool [:(Seg (card rel)),{P}:] is non empty finite V43() set
(CX - {P}) ^ (IdFinS (P,(card rel))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len (IdFinS (P,(card rel))) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
rel is finite set
len CX is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
Seg (len CX) is finite len CX -element Element of bool NAT
i is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
len (CX - {P}) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
i - (len (CX - {P})) is ext-real V32() V37() integer set
seq ((len (CX - {P})),(card rel)) is Element of bool NAT
1 + (len (CX - {P})) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
C is ext-real V32() V37() integer set
(card rel) + (len (CX - {P})) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
F is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
Sgm rel is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
dom (Sgm rel) is finite Element of bool NAT
i is set
C is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set
CX . C is set
rel \ rel is finite Element of bool rel
bool rel is non empty finite V43() set
Seg (len (CX - {P})) is finite len (CX - {P}) -element Element of bool NAT
Sgm (rel \ rel) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
F is finite set
card F is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of omega
card rel is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of omega
(card rel) - (card rel) is ext-real V32() V37() integer set
card (Seg (len CX)) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of omega
(card (Seg (len CX))) - (card rel) is ext-real V32() V37() integer set
(len CX) - (card rel) is ext-real V32() V37() integer set
len ((CX - {P}) ^ (IdFinS (P,(card rel)))) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
Seg (len ((CX - {P}) ^ (IdFinS (P,(card rel))))) is finite len ((CX - {P}) ^ (IdFinS (P,(card rel)))) -element Element of bool NAT
F is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set
(Sgm (rel \ rel)) . F is set
F - (len (CX - {P})) is ext-real V32() V37() integer set
(Sgm rel) . (F - (len (CX - {P}))) is set
F is set
F is set
F is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom F is finite Element of bool NAT
F is set
Sgm F is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
dom (Sgm F) is finite Element of bool NAT
Seg (card F) is finite card F -element Element of bool NAT
rng F is finite set
F is set
F is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set
F . F is set
(Sgm F) . F is set
rng (Sgm F) is finite Element of bool NAT
rng (Sgm rel) is finite Element of bool NAT
F - (len (CX - {P})) is ext-real V32() V37() integer set
(Sgm rel) . (F - (len (CX - {P}))) is set
(Seg (len (CX - {P}))) \/ (seq ((len (CX - {P})),(card rel))) is Element of bool NAT
F is set
F is set
F is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set
(Sgm F) . F is set
len (Sgm F) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
F . F is set
F is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set
(Sgm rel) . F is set
j is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
j + (len (CX - {P})) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
len (Sgm rel) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
(len (CX - {P})) + (len (IdFinS (P,(card rel)))) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
dom ((CX - {P}) ^ (IdFinS (P,(card rel)))) is finite Element of bool NAT
(j + (len (CX - {P}))) - (len (CX - {P})) is ext-real V32() V37() integer set
(Sgm rel) . ((j + (len (CX - {P}))) - (len (CX - {P}))) is set
F . (j + (len (CX - {P}))) is set
(len (CX - {P})) + (len (IdFinS (P,(card rel)))) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
((len CX) - (card rel)) + (len (IdFinS (P,(card rel)))) is ext-real V32() V37() integer set
((len CX) - (card rel)) + (card rel) is ext-real V32() V37() integer set
[:rel,rel:] is finite set
bool [:rel,rel:] is non empty finite V43() set
F is Relation-like rel -defined rel -valued finite Element of bool [:rel,rel:]
rng F is finite Element of bool rel
F is Relation-like rel -defined rel -valued Function-like quasi_total finite Element of bool [:rel,rel:]
j is set
dom F is finite set
F . j is set
h is set
F . h is set
dom F is finite Element of bool rel
(Seg (len (CX - {P}))) \/ (seq ((len (CX - {P})),(card rel))) is Element of bool NAT
(Sgm F) . j is set
rng (Sgm F) is finite Element of bool NAT
k is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
k - (len (CX - {P})) is ext-real V32() V37() integer set
(Sgm rel) . (k - (len (CX - {P}))) is set
rng (Sgm rel) is finite Element of bool NAT
(Sgm F) . h is set
k is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
k - (len (CX - {P})) is ext-real V32() V37() integer set
g is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
g - (len (CX - {P})) is ext-real V32() V37() integer set
(Sgm rel) . (g - (len (CX - {P}))) is set
(Sgm rel) . (k - (len (CX - {P}))) is set
(g - (len (CX - {P}))) + (len (CX - {P})) is ext-real V32() V37() integer set
(k - (len (CX - {P}))) + (len (CX - {P})) is ext-real V32() V37() integer set
[:(dom CX),(dom CX):] is finite set
bool [:(dom CX),(dom CX):] is non empty finite V43() set
j is Relation-like dom CX -defined dom CX -valued Function-like quasi_total bijective finite Element of bool [:(dom CX),(dom CX):]
dom j is finite Element of bool (dom CX)
bool (dom CX) is non empty finite V43() set
h is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set
j . h is set
Per (CX,j) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
dom (Per (CX,j)) is finite Element of bool NAT
dom ((CX - {P}) ^ (IdFinS (P,(card rel)))) is finite Element of bool NAT
k is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set
j * CX is Relation-like dom CX -defined CQC-WFF Al -valued Function-like finite Element of bool [:(dom CX),(CQC-WFF Al):]
[:(dom CX),(CQC-WFF Al):] is set
bool [:(dom CX),(CQC-WFF Al):] is non empty set
dom (j * CX) is finite Element of bool (dom CX)
dom (IdFinS (P,(card rel))) is finite card rel -element Element of bool NAT
g is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set
(len (CX - {P})) + g is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
j . k is set
k - (len (CX - {P})) is ext-real V32() V37() integer set
(Sgm rel) . (k - (len (CX - {P}))) is set
rng (Sgm rel) is finite Element of bool NAT
CX . (j . k) is set
(j * CX) . k is set
(Per (CX,j)) . k is set
(IdFinS (P,(card rel))) . g is set
((CX - {P}) ^ (IdFinS (P,(card rel)))) . k is set
dom (CX - {P}) is finite Element of bool NAT
(Sgm F) . k is set
CX . ((Sgm F) . k) is set
(Sgm F) * CX is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite Element of bool [:NAT,(CQC-WFF Al):]
[:NAT,(CQC-WFF Al):] is non empty non trivial non finite set
bool [:NAT,(CQC-WFF Al):] is non empty non trivial non finite set
((Sgm F) * CX) . k is set
(CX - {P}) . k is set
(j * CX) . h is set
k is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
k . h is set
(CX - {P}) . h is set
rng (CX - {P}) is finite set
(rng CX) \ {P} is finite Element of bool (CQC-WFF Al)
dom k is finite Element of bool NAT
g is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set
(len (CX - {P})) + g is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
k ^ <*ll*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
g is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
g ^ <*P*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(g ^ <*P*>) ^ <*ll*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
g is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
rng g is finite Element of bool (CQC-WFF Al)
(k \/ {P}) \ {P} is Element of bool (CQC-WFF Al)
k \ {P} is Element of bool (CQC-WFF Al)
JH is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
JH ^ <*P*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(JH ^ <*P*>) ^ <*ll*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
rel is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
rng rel is finite Element of bool (CQC-WFF Al)
rel ^ <*P*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(rel ^ <*P*>) ^ <*ll*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
fin9 is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
rng fin9 is finite Element of bool (CQC-WFF Al)
fin9 ^ <*P*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(fin9 ^ <*P*>) ^ <*ll*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Al is non empty Relation-like 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
k is Element of bool (CQC-WFF Al)
P is Element of CQC-WFF Al
'not' P is Element of CQC-WFF Al
{('not' P)} is non empty trivial finite 1 -element Element of bool (CQC-WFF Al)
k \/ {('not' P)} is Element of bool (CQC-WFF Al)
<*P*> is non empty trivial Relation-like NAT -defined CQC-WFF Al -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
ll is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
rng ll is finite Element of bool (CQC-WFF Al)
ll ^ <*P*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
<*('not' P)*> is non empty trivial Relation-like NAT -defined CQC-WFF Al -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
ll ^ <*('not' P)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(ll ^ <*('not' P)*>) ^ <*('not' P)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Ant ((ll ^ <*('not' P)*>) ^ <*('not' P)*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
dom <*('not' P)*> is non empty trivial finite 1 -element Element of bool NAT
len ll is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
(len ll) + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
dom (Ant ((ll ^ <*('not' P)*>) ^ <*('not' P)*>)) is finite Element of bool NAT
Suc ((ll ^ <*('not' P)*>) ^ <*('not' P)*>) is Element of CQC-WFF Al
(Ant ((ll ^ <*('not' P)*>) ^ <*('not' P)*>)) . ((len ll) + 1) is set
0 + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
len (ll ^ <*('not' P)*>) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
Ant (ll ^ <*('not' P)*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Suc (ll ^ <*('not' P)*>) is Element of CQC-WFF Al
rng (ll ^ <*('not' P)*>) is finite Element of bool (CQC-WFF Al)
(rng ll) \/ {('not' P)} is finite Element of bool (CQC-WFF Al)
(ll ^ <*('not' P)*>) ^ <*P*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
<*P*> is non empty trivial Relation-like NAT -defined CQC-WFF Al -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
ll is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
rng ll is finite Element of bool (CQC-WFF Al)
ll ^ <*P*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
ll - {('not' P)} is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
ll " {('not' P)} is finite Element of bool NAT
dom ll is finite Element of bool NAT
JH is finite set
card JH is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of omega
IdFinS (('not' P),(card JH)) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite card JH -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Seg (card JH) is finite card JH -element Element of bool NAT
K253((Seg (card JH)),('not' P)) is Relation-like Seg (card JH) -defined {('not' P)} -valued Function-like quasi_total finite FinSequence-like FinSubsequence-like Element of bool [:(Seg (card JH)),{('not' P)}:]
{('not' P)} is non empty trivial finite 1 -element set
[:(Seg (card JH)),{('not' P)}:] is finite set
bool [:(Seg (card JH)),{('not' P)}:] is non empty finite V43() set
(ll - {('not' P)}) ^ (IdFinS (('not' P),(card JH))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len (IdFinS (('not' P),(card JH))) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
rel is finite set
len ll is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
Seg (len ll) is finite len ll -element Element of bool NAT
a is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
len (ll - {('not' P)}) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
a - (len (ll - {('not' P)})) is ext-real V32() V37() integer set
seq ((len (ll - {('not' P)})),(card JH)) is Element of bool NAT
1 + (len (ll - {('not' P)})) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
i is ext-real V32() V37() integer set
(card JH) + (len (ll - {('not' P)})) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
C is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
Sgm JH is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
dom (Sgm JH) is finite Element of bool NAT
a is set
i is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set
ll . i is set
rel \ JH is finite Element of bool rel
bool rel is non empty finite V43() set
Seg (len (ll - {('not' P)})) is finite len (ll - {('not' P)}) -element Element of bool NAT
Sgm (rel \ JH) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
C is finite set
card C is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of omega
card rel is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of omega
(card rel) - (card JH) is ext-real V32() V37() integer set
card (Seg (len ll)) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of omega
(card (Seg (len ll))) - (card JH) is ext-real V32() V37() integer set
(len ll) - (card JH) is ext-real V32() V37() integer set
len ((ll - {('not' P)}) ^ (IdFinS (('not' P),(card JH)))) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
Seg (len ((ll - {('not' P)}) ^ (IdFinS (('not' P),(card JH))))) is finite len ((ll - {('not' P)}) ^ (IdFinS (('not' P),(card JH)))) -element Element of bool NAT
F is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set
(Sgm (rel \ JH)) . F is set
F - (len (ll - {('not' P)})) is ext-real V32() V37() integer set
(Sgm JH) . (F - (len (ll - {('not' P)}))) is set
F is set
F is set
F is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom F is finite Element of bool NAT
F is set
Sgm C is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
dom (Sgm C) is finite Element of bool NAT
Seg (card C) is finite card C -element Element of bool NAT
rng F is finite set
F is set
F is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set
F . F is set
(Sgm C) . F is set
rng (Sgm C) is finite Element of bool NAT
rng (Sgm JH) is finite Element of bool NAT
F - (len (ll - {('not' P)})) is ext-real V32() V37() integer set
(Sgm JH) . (F - (len (ll - {('not' P)}))) is set
(Seg (len (ll - {('not' P)}))) \/ (seq ((len (ll - {('not' P)})),(card JH))) is Element of bool NAT
F is set
F is set
F is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set
(Sgm C) . F is set
len (Sgm C) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
F . F is set
F is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set
(Sgm JH) . F is set
F is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
F + (len (ll - {('not' P)})) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
len (Sgm JH) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
(len (ll - {('not' P)})) + (len (IdFinS (('not' P),(card JH)))) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
dom ((ll - {('not' P)}) ^ (IdFinS (('not' P),(card JH)))) is finite Element of bool NAT
(F + (len (ll - {('not' P)}))) - (len (ll - {('not' P)})) is ext-real V32() V37() integer set
(Sgm JH) . ((F + (len (ll - {('not' P)}))) - (len (ll - {('not' P)}))) is set
F . (F + (len (ll - {('not' P)}))) is set
(len (ll - {('not' P)})) + (len (IdFinS (('not' P),(card JH)))) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
((len ll) - (card JH)) + (len (IdFinS (('not' P),(card JH)))) is ext-real V32() V37() integer set
((len ll) - (card JH)) + (card JH) is ext-real V32() V37() integer set
[:rel,rel:] is finite set
bool [:rel,rel:] is non empty finite V43() set
F is Relation-like rel -defined rel -valued finite Element of bool [:rel,rel:]
rng F is finite Element of bool rel
F is Relation-like rel -defined rel -valued Function-like quasi_total finite Element of bool [:rel,rel:]
F is set
dom F is finite set
F . F is set
j is set
F . j is set
dom F is finite Element of bool rel
(Seg (len (ll - {('not' P)}))) \/ (seq ((len (ll - {('not' P)})),(card JH))) is Element of bool NAT
(Sgm C) . F is set
rng (Sgm C) is finite Element of bool NAT
h is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
h - (len (ll - {('not' P)})) is ext-real V32() V37() integer set
(Sgm JH) . (h - (len (ll - {('not' P)}))) is set
rng (Sgm JH) is finite Element of bool NAT
(Sgm C) . j is set
h is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
h - (len (ll - {('not' P)})) is ext-real V32() V37() integer set
k is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
k - (len (ll - {('not' P)})) is ext-real V32() V37() integer set
(Sgm JH) . (k - (len (ll - {('not' P)}))) is set
(Sgm JH) . (h - (len (ll - {('not' P)}))) is set
[:(dom ll),(dom ll):] is finite set
bool [:(dom ll),(dom ll):] is non empty finite V43() set
F is Relation-like dom ll -defined dom ll -valued Function-like quasi_total bijective finite Element of bool [:(dom ll),(dom ll):]
dom F is finite Element of bool (dom ll)
bool (dom ll) is non empty finite V43() set
j is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set
F . j is set
Per (ll,F) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
dom (Per (ll,F)) is finite Element of bool NAT
dom ((ll - {('not' P)}) ^ (IdFinS (('not' P),(card JH)))) is finite Element of bool NAT
h is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set
F * ll is Relation-like dom ll -defined CQC-WFF Al -valued Function-like finite Element of bool [:(dom ll),(CQC-WFF Al):]
[:(dom ll),(CQC-WFF Al):] is set
bool [:(dom ll),(CQC-WFF Al):] is non empty set
dom (F * ll) is finite Element of bool (dom ll)
dom (IdFinS (('not' P),(card JH))) is finite card JH -element Element of bool NAT
k is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set
(len (ll - {('not' P)})) + k is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
F . h is set
h - (len (ll - {('not' P)})) is ext-real V32() V37() integer set
(Sgm JH) . (h - (len (ll - {('not' P)}))) is set
rng (Sgm JH) is finite Element of bool NAT
ll . (F . h) is set
(F * ll) . h is set
(Per (ll,F)) . h is set
(IdFinS (('not' P),(card JH))) . k is set
((ll - {('not' P)}) ^ (IdFinS (('not' P),(card JH)))) . h is set
dom (ll - {('not' P)}) is finite Element of bool NAT
(Sgm C) . h is set
ll . ((Sgm C) . h) is set
(Sgm C) * ll is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite Element of bool [:NAT,(CQC-WFF Al):]
[:NAT,(CQC-WFF Al):] is non empty non trivial non finite set
bool [:NAT,(CQC-WFF Al):] is non empty non trivial non finite set
((Sgm C) * ll) . h is set
(ll - {('not' P)}) . h is set
(F * ll) . j is set
h is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
h . j is set
(ll - {('not' P)}) . j is set
rng (ll - {('not' P)}) is finite set
(rng ll) \ {('not' P)} is finite Element of bool (CQC-WFF Al)
dom h is finite Element of bool NAT
k is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set
(len (ll - {('not' P)})) + k is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
h ^ <*P*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
g is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
<*('not' P)*> is non empty trivial Relation-like NAT -defined CQC-WFF Al -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
g ^ <*('not' P)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(g ^ <*('not' P)*>) ^ <*P*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
rng g is finite Element of bool (CQC-WFF Al)
(k \/ {('not' P)}) \ {('not' P)} is Element of bool (CQC-WFF Al)
k \ {('not' P)} is Element of bool (CQC-WFF Al)
g ^ <*P*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(g ^ <*P*>) ^ <*P*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Al is non empty Relation-like 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
k is Element of bool (CQC-WFF Al)
P is Element of CQC-WFF Al
'not' P is Element of CQC-WFF Al
{P} is non empty trivial finite 1 -element Element of bool (CQC-WFF Al)
k \/ {P} is Element of bool (CQC-WFF Al)
<*('not' P)*> is non empty trivial Relation-like NAT -defined CQC-WFF Al -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
ll is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
rng ll is finite Element of bool (CQC-WFF Al)
ll ^ <*('not' P)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
<*P*> is non empty trivial Relation-like NAT -defined CQC-WFF Al -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
ll ^ <*P*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(ll ^ <*P*>) ^ <*P*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Ant ((ll ^ <*P*>) ^ <*P*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
dom <*P*> is non empty trivial finite 1 -element Element of bool NAT
len ll is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
(len ll) + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
dom (Ant ((ll ^ <*P*>) ^ <*P*>)) is finite Element of bool NAT
Suc ((ll ^ <*P*>) ^ <*P*>) is Element of CQC-WFF Al
(Ant ((ll ^ <*P*>) ^ <*P*>)) . ((len ll) + 1) is set
0 + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
len (ll ^ <*P*>) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
Ant (ll ^ <*P*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Suc (ll ^ <*P*>) is Element of CQC-WFF Al
rng (ll ^ <*P*>) is finite Element of bool (CQC-WFF Al)
(rng ll) \/ {P} is finite Element of bool (CQC-WFF Al)
(ll ^ <*P*>) ^ <*('not' P)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
<*('not' P)*> is non empty trivial Relation-like NAT -defined CQC-WFF Al -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
ll is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
rng ll is finite Element of bool (CQC-WFF Al)
ll ^ <*('not' P)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
ll - {P} is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
ll " {P} is finite Element of bool NAT
dom ll is finite Element of bool NAT
JH is finite set
card JH is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of omega
IdFinS (P,(card JH)) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite card JH -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Seg (card JH) is finite card JH -element Element of bool NAT
K253((Seg (card JH)),P) is Relation-like Seg (card JH) -defined {P} -valued Function-like quasi_total finite FinSequence-like FinSubsequence-like Element of bool [:(Seg (card JH)),{P}:]
{P} is non empty trivial finite 1 -element set
[:(Seg (card JH)),{P}:] is finite set
bool [:(Seg (card JH)),{P}:] is non empty finite V43() set
(ll - {P}) ^ (IdFinS (P,(card JH))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len (IdFinS (P,(card JH))) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
rel is finite set
len ll is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
Seg (len ll) is finite len ll -element Element of bool NAT
a is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
len (ll - {P}) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
a - (len (ll - {P})) is ext-real V32() V37() integer set
seq ((len (ll - {P})),(card JH)) is Element of bool NAT
1 + (len (ll - {P})) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
i is ext-real V32() V37() integer set
(card JH) + (len (ll - {P})) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
C is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
Sgm JH is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
dom (Sgm JH) is finite Element of bool NAT
a is set
i is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set
ll . i is set
rel \ JH is finite Element of bool rel
bool rel is non empty finite V43() set
Seg (len (ll - {P})) is finite len (ll - {P}) -element Element of bool NAT
Sgm (rel \ JH) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
C is finite set
card C is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of omega
card rel is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of omega
(card rel) - (card JH) is ext-real V32() V37() integer set
card (Seg (len ll)) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of omega
(card (Seg (len ll))) - (card JH) is ext-real V32() V37() integer set
(len ll) - (card JH) is ext-real V32() V37() integer set
len ((ll - {P}) ^ (IdFinS (P,(card JH)))) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
Seg (len ((ll - {P}) ^ (IdFinS (P,(card JH))))) is finite len ((ll - {P}) ^ (IdFinS (P,(card JH)))) -element Element of bool NAT
F is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set
(Sgm (rel \ JH)) . F is set
F - (len (ll - {P})) is ext-real V32() V37() integer set
(Sgm JH) . (F - (len (ll - {P}))) is set
F is set
F is set
F is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom F is finite Element of bool NAT
F is set
Sgm C is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
dom (Sgm C) is finite Element of bool NAT
Seg (card C) is finite card C -element Element of bool NAT
rng F is finite set
F is set
F is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set
F . F is set
(Sgm C) . F is set
rng (Sgm C) is finite Element of bool NAT
rng (Sgm JH) is finite Element of bool NAT
F - (len (ll - {P})) is ext-real V32() V37() integer set
(Sgm JH) . (F - (len (ll - {P}))) is set
(Seg (len (ll - {P}))) \/ (seq ((len (ll - {P})),(card JH))) is Element of bool NAT
F is set
F is set
F is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set
(Sgm C) . F is set
len (Sgm C) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
F . F is set
F is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set
(Sgm JH) . F is set
F is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
F + (len (ll - {P})) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
len (Sgm JH) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
(len (ll - {P})) + (len (IdFinS (P,(card JH)))) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
dom ((ll - {P}) ^ (IdFinS (P,(card JH)))) is finite Element of bool NAT
(F + (len (ll - {P}))) - (len (ll - {P})) is ext-real V32() V37() integer set
(Sgm JH) . ((F + (len (ll - {P}))) - (len (ll - {P}))) is set
F . (F + (len (ll - {P}))) is set
(len (ll - {P})) + (len (IdFinS (P,(card JH)))) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
((len ll) - (card JH)) + (len (IdFinS (P,(card JH)))) is ext-real V32() V37() integer set
((len ll) - (card JH)) + (card JH) is ext-real V32() V37() integer set
[:rel,rel:] is finite set
bool [:rel,rel:] is non empty finite V43() set
F is Relation-like rel -defined rel -valued finite Element of bool [:rel,rel:]
rng F is finite Element of bool rel
F is Relation-like rel -defined rel -valued Function-like quasi_total finite Element of bool [:rel,rel:]
F is set
dom F is finite set
F . F is set
j is set
F . j is set
dom F is finite Element of bool rel
(Seg (len (ll - {P}))) \/ (seq ((len (ll - {P})),(card JH))) is Element of bool NAT
(Sgm C) . F is set
rng (Sgm C) is finite Element of bool NAT
h is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
h - (len (ll - {P})) is ext-real V32() V37() integer set
(Sgm JH) . (h - (len (ll - {P}))) is set
rng (Sgm JH) is finite Element of bool NAT
(Sgm C) . j is set
h is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
h - (len (ll - {P})) is ext-real V32() V37() integer set
k is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
k - (len (ll - {P})) is ext-real V32() V37() integer set
(Sgm JH) . (k - (len (ll - {P}))) is set
(Sgm JH) . (h - (len (ll - {P}))) is set
(k - (len (ll - {P}))) + (len (ll - {P})) is ext-real V32() V37() integer set
(h - (len (ll - {P}))) + (len (ll - {P})) is ext-real V32() V37() integer set
[:(dom ll),(dom ll):] is finite set
bool [:(dom ll),(dom ll):] is non empty finite V43() set
F is Relation-like dom ll -defined dom ll -valued Function-like quasi_total bijective finite Element of bool [:(dom ll),(dom ll):]
dom F is finite Element of bool (dom ll)
bool (dom ll) is non empty finite V43() set
j is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set
F . j is set
Per (ll,F) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
dom (Per (ll,F)) is finite Element of bool NAT
dom ((ll - {P}) ^ (IdFinS (P,(card JH)))) is finite Element of bool NAT
h is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set
F * ll is Relation-like dom ll -defined CQC-WFF Al -valued Function-like finite Element of bool [:(dom ll),(CQC-WFF Al):]
[:(dom ll),(CQC-WFF Al):] is set
bool [:(dom ll),(CQC-WFF Al):] is non empty set
dom (F * ll) is finite Element of bool (dom ll)
dom (IdFinS (P,(card JH))) is finite card JH -element Element of bool NAT
k is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set
(len (ll - {P})) + k is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
F . h is set
h - (len (ll - {P})) is ext-real V32() V37() integer set
(Sgm JH) . (h - (len (ll - {P}))) is set
rng (Sgm JH) is finite Element of bool NAT
ll . (F . h) is set
(F * ll) . h is set
(Per (ll,F)) . h is set
(IdFinS (P,(card JH))) . k is set
((ll - {P}) ^ (IdFinS (P,(card JH)))) . h is set
dom (ll - {P}) is finite Element of bool NAT
(Sgm C) . h is set
ll . ((Sgm C) . h) is set
(Sgm C) * ll is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite Element of bool [:NAT,(CQC-WFF Al):]
[:NAT,(CQC-WFF Al):] is non empty non trivial non finite set
bool [:NAT,(CQC-WFF Al):] is non empty non trivial non finite set
((Sgm C) * ll) . h is set
(ll - {P}) . h is set
(F * ll) . j is set
h is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
h . j is set
(ll - {P}) . j is set
rng (ll - {P}) is finite set
(rng ll) \ {P} is finite Element of bool (CQC-WFF Al)
dom h is finite Element of bool NAT
k is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set
(len (ll - {P})) + k is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
h ^ <*('not' P)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
g is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
<*P*> is non empty trivial Relation-like NAT -defined CQC-WFF Al -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
g ^ <*P*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(g ^ <*P*>) ^ <*('not' P)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
rng g is finite Element of bool (CQC-WFF Al)
(k \/ {P}) \ {P} is Element of bool (CQC-WFF Al)
k \ {P} is Element of bool (CQC-WFF Al)
g ^ <*('not' P)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(g ^ <*('not' P)*>) ^ <*('not' P)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Al is non empty Relation-like 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 Element of bool (bool (CQC-WFF Al))
bool (CQC-WFF Al) is non empty set
bool (bool (CQC-WFF Al)) is non empty set
[:NAT,(bool (CQC-WFF Al)):] is non empty non trivial non finite set
bool [:NAT,(bool (CQC-WFF Al)):] is non empty non trivial non finite set
k is Relation-like NAT -defined bool (CQC-WFF Al) -valued Function-like quasi_total Element of bool [:NAT,(bool (CQC-WFF Al)):]
dom k is Element of bool NAT
rng k is Element of bool (bool (CQC-WFF Al))
bool (bool (CQC-WFF Al)) is non empty set
union (rng k) is Element of bool (CQC-WFF Al)
P is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
k . P is Element of bool (CQC-WFF Al)
P + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
P is Element of bool (CQC-WFF Al)
CX is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
ll is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
k . ll is Element of bool (CQC-WFF Al)
k . CX is Element of bool (CQC-WFF Al)
ll is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
k . ll is Element of bool (CQC-WFF Al)
JH is Element of CQC-WFF Al
'not' JH is Element of CQC-WFF Al
<*JH*> is non empty trivial Relation-like NAT -defined CQC-WFF Al -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
rel is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
rng rel is finite Element of bool (CQC-WFF Al)
rel ^ <*JH*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
<*('not' JH)*> is non empty trivial Relation-like NAT -defined CQC-WFF Al -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
rel is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
rng rel is finite Element of bool (CQC-WFF Al)
rel ^ <*('not' JH)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
rel ^ rel is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
rng (rel ^ rel) is finite Element of bool (CQC-WFF Al)
(rng rel) \/ (rng rel) is finite Element of bool (CQC-WFF Al)
CX is Element of bool (CQC-WFF Al)
(rel ^ rel) ^ <*('not' JH)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(rel ^ rel) ^ <*JH*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Al is non empty Relation-like 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 non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
QC-variables Al is non empty set
bool (QC-variables Al) is non empty set
k is Element of bool (CQC-WFF Al)
P is non empty set
relations_on P is set
Valuations_in (Al,P) is non empty FUNCTION_DOMAIN of bound_QC-variables Al,P
VERUM Al is Element of CQC-WFF Al
'not' (VERUM Al) is Element of CQC-WFF Al
<*('not' (VERUM Al))*> is non empty trivial Relation-like NAT -defined CQC-WFF Al -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
CX is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
rng CX is finite Element of bool (CQC-WFF Al)
CX ^ <*('not' (VERUM Al))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
JH is Relation-like QC-pred_symbols Al -defined relations_on P -valued Function-like quasi_total interpretation of Al,P
rel is Relation-like bound_QC-variables Al -defined P -valued Function-like quasi_total Element of Valuations_in (Al,P)
ll is Element of CQC-WFF Al
<*ll*> is non empty trivial Relation-like NAT -defined CQC-WFF Al -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
CX ^ <*ll*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Suc (CX ^ <*ll*>) is Element of CQC-WFF Al
Ant (CX ^ <*ll*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
rng (Ant (CX ^ <*ll*>)) is finite Element of bool (CQC-WFF Al)
Al is non empty Relation-like 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
VERUM Al is Element of CQC-WFF Al
{(VERUM Al)} is non empty trivial finite 1 -element Element of bool (CQC-WFF Al)
bool (CQC-WFF Al) is non empty set
the non empty set is non empty set
QC-pred_symbols Al is non empty set
relations_on the non empty set is set
the Relation-like QC-pred_symbols Al -defined relations_on the non empty set -valued Function-like quasi_total interpretation of Al, the non empty set is Relation-like QC-pred_symbols Al -defined relations_on the non empty set -valued Function-like quasi_total interpretation of Al, the non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
QC-variables Al is non empty set
bool (QC-variables Al) is non empty set
Valuations_in (Al, the non empty set ) is non empty FUNCTION_DOMAIN of bound_QC-variables Al, the non empty set
the Relation-like bound_QC-variables Al -defined the non empty set -valued Function-like quasi_total Element of Valuations_in (Al, the non empty set ) is Relation-like bound_QC-variables Al -defined the non empty set -valued Function-like quasi_total Element of Valuations_in (Al, the non empty set )
CX is Element of CQC-WFF Al
Al is non empty Relation-like 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
{(VERUM Al)} is non empty trivial finite 1 -element Element of bool (CQC-WFF Al)
Al is non empty Relation-like QC-alphabet
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
QC-variables Al is non empty set
bool (QC-variables Al) is non empty set
Al is non empty Relation-like QC-alphabet
QC-pred_symbols Al is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
QC-variables Al is non empty set
bool (QC-variables Al) is non empty set
k is Element of QC-pred_symbols Al
the_arity_of k is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
P is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like finite the_arity_of k -element FinSequence-like FinSubsequence-like FinSequence of QC-variables Al
k ! P is Element of QC-WFF Al
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
(the_arity_of k) -ary_QC-pred_symbols Al is non empty Element of bool (QC-pred_symbols Al)
bool (QC-pred_symbols Al) is non empty set
CX is Element of (the_arity_of k) -ary_QC-pred_symbols Al
CX ! P is Element of CQC-WFF Al
Al is non empty Relation-like 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 non empty set
(Al) is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
QC-variables Al is non empty set
bool (QC-variables Al) is non empty set
relations_on (Al) is set
k is (Al) Element of bool (CQC-WFF Al)
ll is set
CX is Element of QC-pred_symbols Al
the_arity_of CX is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
{ b₁ where b₁ is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like finite the_arity_of CX -element FinSequence-like FinSubsequence-like FinSequence of QC-variables Al : (Al,k,(Al,CX,b₁)) } is set
JH is set
ll is Relation-like Function-like set
dom ll is set
CX is Element of QC-pred_symbols Al
ll . CX is set
the_arity_of CX is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
JH is Element of relations_on (Al)
rel is set
rel is Element of QC-pred_symbols Al
the_arity_of rel is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
{ b₁ where b₁ is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like finite the_arity_of rel -element FinSequence-like FinSubsequence-like FinSequence of QC-variables Al : (Al,k,(Al,rel,b₁)) } is set
rel is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like finite the_arity_of CX -element FinSequence-like FinSubsequence-like FinSequence of QC-variables Al
(Al,CX,rel) is Element of CQC-WFF Al
fin9 is Element of QC-pred_symbols Al
the_arity_of fin9 is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
{ b₁ where b₁ is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like finite the_arity_of fin9 -element FinSequence-like FinSubsequence-like FinSequence of QC-variables Al : (Al,k,(Al,fin9,b₁)) } is set
empty_rel (Al) is Element of relations_on (Al)
CX is Element of QC-pred_symbols Al
ll . CX is set
the_arity_of CX is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
JH is Element of relations_on (Al)
the_arity_of JH is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
rel is Element of QC-pred_symbols Al
the_arity_of rel is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
{ b₁ where b₁ is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like finite the_arity_of rel -element FinSequence-like FinSubsequence-like FinSequence of QC-variables Al : (Al,k,(Al,rel,b₁)) } is set
rel is set
fin9 is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like finite the_arity_of rel -element FinSequence-like FinSubsequence-like FinSequence of QC-variables Al
(Al,rel,fin9) is Element of CQC-WFF Al
rng fin9 is finite Element of bool (QC-variables Al)
a is Relation-like NAT -defined (Al) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of (Al)
len a is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
rng ll is set
CX is set
JH is set
ll . JH is set
rel is Element of QC-pred_symbols Al
the_arity_of rel is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
{ b₁ where b₁ is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like finite the_arity_of rel -element FinSequence-like FinSubsequence-like FinSequence of QC-variables Al : (Al,k,(Al,rel,b₁)) } is set
(Al) * is non empty functional FinSequence-membered set
rel is set
fin9 is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like finite the_arity_of rel -element FinSequence-like FinSubsequence-like FinSequence of QC-variables Al
(Al,rel,fin9) is Element of CQC-WFF Al
rng fin9 is finite Element of bool (QC-variables Al)
rel is Relation-like NAT -defined (Al) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of (Al)
fin9 is Relation-like NAT -defined (Al) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of (Al)
len rel is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
len fin9 is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
a is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like finite the_arity_of rel -element FinSequence-like FinSubsequence-like FinSequence of QC-variables Al
(Al,rel,a) is Element of CQC-WFF Al
a is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like finite the_arity_of rel -element FinSequence-like FinSubsequence-like FinSequence of QC-variables Al
(Al,rel,a) is Element of CQC-WFF Al
[:(QC-pred_symbols Al),(relations_on (Al)):] is set
bool [:(QC-pred_symbols Al),(relations_on (Al)):] is non empty set
CX is Relation-like QC-pred_symbols Al -defined relations_on (Al) -valued Function-like quasi_total Element of bool [:(QC-pred_symbols Al),(relations_on (Al)):]
JH is Relation-like QC-pred_symbols Al -defined relations_on (Al) -valued Function-like quasi_total interpretation of Al,(Al)
rel is Element of QC-pred_symbols Al
the_arity_of rel is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
JH . rel is Element of relations_on (Al)
rel is Element of relations_on (Al)
fin9 is set
a is set
i is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like finite the_arity_of rel -element FinSequence-like FinSubsequence-like FinSequence of QC-variables Al
(Al,rel,i) is Element of CQC-WFF Al
Al is non empty Relation-like QC-alphabet
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
QC-variables Al is non empty set
bool (QC-variables Al) is non empty set
id (bound_QC-variables Al) is non empty Relation-like Function-like one-to-one Element of Funcs ((bound_QC-variables Al),(bound_QC-variables Al))
Funcs ((bound_QC-variables Al),(bound_QC-variables Al)) is set
(Al) is non empty set
Valuations_in (Al,(Al)) is non empty FUNCTION_DOMAIN of bound_QC-variables Al,(Al)
Al is non empty Relation-like QC-alphabet
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
QC-variables Al is non empty set
bool (QC-variables Al) is non empty set
(Al) is non empty set
(Al) is Relation-like bound_QC-variables Al -defined (Al) -valued Function-like quasi_total Element of Valuations_in (Al,(Al))
Valuations_in (Al,(Al)) is non empty FUNCTION_DOMAIN of bound_QC-variables Al,(Al)
id (bound_QC-variables Al) is non empty Relation-like Function-like one-to-one Element of Funcs ((bound_QC-variables Al),(bound_QC-variables Al))
Funcs ((bound_QC-variables Al),(bound_QC-variables Al)) is set
k is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
P is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like finite k -element FinSequence-like FinSubsequence-like FinSequence of QC-variables Al
(Al) *' P is Relation-like NAT -defined (Al) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of (Al)
dom ((Al) *' P) is finite Element of bool NAT
dom P is finite k -element Element of bool NAT
ll is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
P . ll is set
(Al) . (P . ll) is set
rng P is finite Element of bool (QC-variables Al)
ll is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
P . ll is set
(Al) . (P . ll) is set
len ((Al) *' P) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
len P is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
dom P is finite k -element Element of bool NAT
Seg k is finite k -element Element of bool NAT
ll is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set
((Al) *' P) . ll is set
P . ll is set
CX is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
((Al) *' P) . CX is set
P . CX is set
(Al) . (P . CX) is set
len ((Al) *' P) is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
Al is non empty Relation-like 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
VERUM Al is Element of CQC-WFF Al
<*(VERUM Al)*> is non empty trivial Relation-like NAT -defined CQC-WFF Al -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
k is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
k ^ <*(VERUM Al)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
[:NAT,(CQC-WFF Al):] is non empty non trivial non finite set
bool [:NAT,(CQC-WFF Al):] is non empty non trivial non finite set
[:(bool [:NAT,(CQC-WFF Al):]),NAT:] is non empty non trivial non finite set
[(k ^ <*(VERUM Al)*>),1] is V26() Element of [:(bool [:NAT,(CQC-WFF Al):]),NAT:]
{(k ^ <*(VERUM Al)*>),1} is finite V43() set
{(k ^ <*(VERUM Al)*>)} is non empty trivial functional finite V43() 1 -element set
{{(k ^ <*(VERUM Al)*>),1},{(k ^ <*(VERUM Al)*>)}} is finite V43() set
<*[(k ^ <*(VERUM Al)*>),1]*> is non empty trivial Relation-like NAT -defined [:(bool [:NAT,(CQC-WFF Al):]),NAT:] -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of [:(bool [:NAT,(CQC-WFF Al):]),NAT:]
rng <*[(k ^ <*(VERUM Al)*>),1]*> is trivial Relation-like bool [:NAT,(CQC-WFF Al):] -defined NAT -valued finite Element of bool [:(bool [:NAT,(CQC-WFF Al):]),NAT:]
bool [:(bool [:NAT,(CQC-WFF Al):]),NAT:] is non empty non trivial non finite set
{[(k ^ <*(VERUM Al)*>),1]} is non empty trivial Relation-like bool [:NAT,(CQC-WFF Al):] -defined NAT -valued Function-like constant finite 1 -element Element of bool [:(bool [:NAT,(CQC-WFF Al):]),NAT:]
ll is set
set_of_CQC-WFF-seq Al is set
[:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] is set
CX is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal set
ll is Relation-like NAT -defined [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:]
len ll is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
ll . CX is set
(ll . CX) `1 is set
(ll . CX) `2 is set
ll . 1 is set
ll . (len ll) is set
(ll . (len ll)) `1 is set
Al is non empty Relation-like 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 non empty set
(Al) is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
QC-variables Al is non empty set
bool (QC-variables Al) is non empty set
relations_on (Al) is set
VERUM Al is Element of CQC-WFF Al
(Al) is Relation-like bound_QC-variables Al -defined (Al) -valued Function-like quasi_total Element of Valuations_in (Al,(Al))
Valuations_in (Al,(Al)) is non empty FUNCTION_DOMAIN of bound_QC-variables Al,(Al)
id (bound_QC-variables Al) is non empty Relation-like Function-like one-to-one Element of Funcs ((bound_QC-variables Al),(bound_QC-variables Al))
Funcs ((bound_QC-variables Al),(bound_QC-variables Al)) is set
k is (Al) Element of bool (CQC-WFF Al)
P is Relation-like QC-pred_symbols Al -defined relations_on (Al) -valued Function-like quasi_total (Al,k)
<*> (CQC-WFF Al) is empty proper Relation-like NAT -defined CQC-WFF Al -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V32() V37() integer finite finite-yielding V43() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of CQC-WFF Al
[:NAT,(CQC-WFF Al):] is non empty non trivial non finite set
rng (<*> (CQC-WFF Al)) is empty trivial proper Function-like functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V32() V37() integer finite V43() cardinal {} -element FinSequence-membered Element of bool (CQC-WFF Al)
<*(VERUM Al)*> is non empty trivial Relation-like NAT -defined CQC-WFF Al -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like 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 FinSequence of CQC-WFF Al
Al is non empty Relation-like QC-alphabet
QC-pred_symbols Al is non empty set
bound_QC-variables Al is non empty Element of bool (QC-variables Al)
QC-variables Al is non empty set
bool (QC-variables Al) is non empty set
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 non empty set
relations_on (Al) is set
(Al) is Relation-like bound_QC-variables Al -defined (Al) -valued Function-like quasi_total Element of Valuations_in (Al,(Al))
Valuations_in (Al,(Al)) is non empty FUNCTION_DOMAIN of bound_QC-variables Al,(Al)
id (bound_QC-variables Al) is non empty Relation-like Function-like one-to-one Element of Funcs ((bound_QC-variables Al),(bound_QC-variables Al))
Funcs ((bound_QC-variables Al),(bound_QC-variables Al)) is set
k is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
k -ary_QC-pred_symbols Al is non empty Element of bool (QC-pred_symbols Al)
bool (QC-pred_symbols Al) is non empty set
P is Element of k -ary_QC-pred_symbols Al
ll is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like finite k -element FinSequence-like FinSubsequence-like FinSequence of QC-variables Al
P ! ll is Element of CQC-WFF Al
CX is (Al) Element of bool (CQC-WFF Al)
JH is Relation-like QC-pred_symbols Al -defined relations_on (Al) -valued Function-like quasi_total (Al,CX)
JH . P is Element of relations_on (Al)
Valid ((P ! ll),JH) is Relation-like Valuations_in (Al,(Al)) -defined BOOLEAN -valued Function-like quasi_total Element of Funcs ((Valuations_in (Al,(Al))),BOOLEAN)
Funcs ((Valuations_in (Al,(Al))),BOOLEAN) is non empty FUNCTION_DOMAIN of Valuations_in (Al,(Al)), BOOLEAN
(Valid ((P ! ll),JH)) . (Al) is Element of BOOLEAN
(Al) *' ll is Relation-like NAT -defined (Al) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of (Al)
rel is Element of relations_on (Al)
the_arity_of P is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
fin9 is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like finite the_arity_of P -element FinSequence-like FinSubsequence-like FinSequence of QC-variables Al
(Al,P,fin9) is Element of CQC-WFF Al
the_arity_of P is epsilon-transitive epsilon-connected ordinal natural ext-real V32() V37() integer finite cardinal Element of NAT
(the_arity_of P) -ary_QC-pred_symbols Al is non empty Element of bool (QC-pred_symbols Al)
JH . P is Element of relations_on (Al)
(Al) *' ll is Relation-like NAT -defined (Al) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of (Al)
Valid ((P ! ll),JH) is Relation-like Valuations_in (Al,(Al)) -defined BOOLEAN -valued Function-like quasi_total Element of Funcs ((Valuations_in (Al,(Al))),BOOLEAN)
Funcs ((Valuations_in (Al,(Al))),BOOLEAN) is non empty FUNCTION_DOMAIN of Valuations_in (Al,(Al)), BOOLEAN
(Valid ((P ! ll),JH)) . (Al) is Element of BOOLEAN