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
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal set
bool NAT is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
K294() is set
{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V28() V29() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V45() set
the Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V28() V29() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V45() set is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V28() V29() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V45() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
2 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V28() V29() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V45() Element of NAT
4 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
{4} is non empty trivial finite V37() 1 -element set
9 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
5 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
6 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
7 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
8 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
Seg 1 is non empty trivial finite 1 -element Element of bool NAT
{1} is non empty trivial finite V37() 1 -element set
Seg 2 is non empty finite 2 -element Element of bool NAT
{1,2} is non empty finite V37() set
Proof_Step_Kinds is set
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT : b1 <= 9 } is set
f is non empty set
p is Relation-like NAT -defined f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of f
len p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal set
x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
Seg f is finite f -element Element of bool NAT
[:NAT,f:] is Relation-like non empty non trivial non finite set
bool [:NAT,f:] is non empty non trivial non finite set
p | (Seg f) is Relation-like NAT -defined Seg f -defined NAT -defined f -valued Function-like finite FinSubsequence-like Element of bool [:NAT,f:]
y0 is Relation-like NAT -defined Seg f -defined f -valued Function-like finite FinSubsequence-like Element of bool [:NAT,f:]
f1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
proj2 f1 is finite set
rng p is finite Element of bool f
bool f is non empty set
F is set
F is Relation-like NAT -defined f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of f
b is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
b + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
Seg b is finite b -element Element of bool NAT
p | (Seg b) is Relation-like NAT -defined Seg b -defined NAT -defined f -valued Function-like finite FinSubsequence-like Element of bool [:NAT,f:]
b is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
b + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
Seg b is finite b -element Element of bool NAT
p | (Seg b) is Relation-like NAT -defined Seg b -defined NAT -defined f -valued Function-like finite FinSubsequence-like Element of bool [:NAT,f:]
<*> f is Relation-like non-empty empty-yielding NAT -defined f -valued Function-like one-to-one constant functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V28() V29() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V45() FinSequence of f
[:NAT,f:] is Relation-like non empty non trivial non finite set
x is Relation-like NAT -defined f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of f
x is Relation-like NAT -defined f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of f
f is Relation-like NAT -defined f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of f
y0 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal set
y0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
f1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
Seg f1 is finite f1 -element Element of bool NAT
p | (Seg f1) is Relation-like NAT -defined Seg f1 -defined NAT -defined f -valued Function-like finite FinSubsequence-like Element of bool [:NAT,f:]
[:NAT,f:] is Relation-like non empty non trivial non finite set
bool [:NAT,f:] is non empty non trivial non finite set
y0 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
y0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
Seg y0 is finite y0 -element Element of bool NAT
p | (Seg y0) is Relation-like NAT -defined Seg y0 -defined NAT -defined f -valued Function-like finite FinSubsequence-like Element of bool [:NAT,f:]
[:NAT,f:] is Relation-like non empty non trivial non finite set
bool [:NAT,f:] is non empty non trivial non finite set
f1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
f1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
Seg f1 is finite f1 -element Element of bool NAT
p | (Seg f1) is Relation-like NAT -defined Seg f1 -defined NAT -defined f -valued Function-like finite FinSubsequence-like Element of bool [:NAT,f:]
f is Relation-like non empty QC-alphabet
CQC-WFF f is non empty Element of bool (QC-WFF f)
QC-WFF f is non empty set
bool (QC-WFF f) is non empty set
p is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
len p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
p . (len p) is set
VERUM f is Element of CQC-WFF f
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
dom p is finite Element of bool NAT
rng p is finite Element of bool (CQC-WFF f)
bool (CQC-WFF f) is non empty set
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
p is set
proj2 f is finite set
dom f is finite Element of bool NAT
x is set
f . x is set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
y0 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
f . y0 is set
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom f is finite Element of bool NAT
p is set
proj2 f is finite set
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
f . x is set
f is Relation-like non empty QC-alphabet
CQC-WFF f is non empty Element of bool (QC-WFF f)
QC-WFF f is non empty set
bool (QC-WFF f) is non empty set
f is Relation-like non empty QC-alphabet
CQC-WFF f is non empty Element of bool (QC-WFF f)
QC-WFF f is non empty set
bool (QC-WFF f) is non empty set
p is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
rng p is finite Element of bool (CQC-WFF f)
bool (CQC-WFF f) is non empty set
x is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
rng x is finite Element of bool (CQC-WFF f)
f is Element of bool NAT
x | f is Relation-like NAT -defined f -defined NAT -defined CQC-WFF f -valued Function-like finite FinSubsequence-like Element of bool [:NAT,(CQC-WFF f):]
[:NAT,(CQC-WFF f):] is Relation-like non empty non trivial non finite set
bool [:NAT,(CQC-WFF f):] is non empty non trivial non finite set
Seq (x | f) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng (x | f) is finite Element of bool (CQC-WFF f)
proj2 (Seq (x | f)) is finite set
dom (x | f) is finite Element of bool f
bool f is non empty set
Sgm (dom (x | f)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(x | f) * (Sgm (dom (x | f))) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite Element of bool [:NAT,(CQC-WFF f):]
rng ((x | f) * (Sgm (dom (x | f)))) is finite Element of bool (CQC-WFF f)
y0 is set
dom p is finite Element of bool NAT
f1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal set
p . f1 is set
[f1,(p . f1)] is V22() set
{f1,(p . f1)} is non empty finite set
{f1} is non empty trivial finite V37() 1 -element set
{{f1,(p . f1)},{f1}} is non empty finite V37() set
(Seq (x | f)) . f1 is set
dom (Seq (x | f)) is finite Element of bool NAT
f is Relation-like non empty QC-alphabet
CQC-WFF f is non empty Element of bool (QC-WFF f)
QC-WFF f is non empty set
bool (QC-WFF f) is non empty set
p is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
len p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
((CQC-WFF f),p) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
len ((CQC-WFF f),p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
(len ((CQC-WFF f),p)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal set
x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
Seg f is finite f -element Element of bool NAT
p | (Seg f) is Relation-like NAT -defined Seg f -defined NAT -defined CQC-WFF f -valued Function-like finite FinSubsequence-like Element of bool [:NAT,(CQC-WFF f):]
[:NAT,(CQC-WFF f):] is Relation-like non empty non trivial non finite set
bool [:NAT,(CQC-WFF f):] is non empty non trivial non finite set
dom ((CQC-WFF f),p) is finite Element of bool NAT
dom p is finite Element of bool NAT
(dom p) /\ (Seg f) is finite Element of bool NAT
Seg (len ((CQC-WFF f),p)) is finite len ((CQC-WFF f),p) -element Element of bool NAT
Seg (len p) is finite len p -element Element of bool NAT
(Seg (len p)) /\ (Seg f) is finite Element of bool NAT
f is Relation-like non empty QC-alphabet
CQC-WFF f is non empty Element of bool (QC-WFF f)
QC-WFF f is non empty set
bool (QC-WFF f) is non empty set
p is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
len p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
((CQC-WFF f),p) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
(f,p) is Element of CQC-WFF f
<*(f,p)*> is Relation-like NAT -defined CQC-WFF f -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
((CQC-WFF f),p) ^ <*(f,p)*> is Relation-like NAT -defined CQC-WFF f -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
rng p is finite Element of bool (CQC-WFF f)
bool (CQC-WFF f) is non empty set
rng ((CQC-WFF f),p) is finite Element of bool (CQC-WFF f)
{(f,p)} is non empty trivial finite 1 -element Element of bool (CQC-WFF f)
(rng ((CQC-WFF f),p)) \/ {(f,p)} is non empty finite Element of bool (CQC-WFF f)
len ((CQC-WFF f),p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
(len ((CQC-WFF f),p)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
dom p is finite Element of bool NAT
Seg (len p) is finite len p -element Element of bool NAT
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal set
dom ((CQC-WFF f),p) is finite Element of bool NAT
Seg (len ((CQC-WFF f),p)) is finite len ((CQC-WFF f),p) -element Element of bool NAT
p | (Seg (len ((CQC-WFF f),p))) is Relation-like NAT -defined Seg (len ((CQC-WFF f),p)) -defined NAT -defined CQC-WFF f -valued Function-like finite FinSubsequence-like Element of bool [:NAT,(CQC-WFF f):]
[:NAT,(CQC-WFF f):] is Relation-like non empty non trivial non finite set
bool [:NAT,(CQC-WFF f):] is non empty non trivial non finite set
p | (dom ((CQC-WFF f),p)) is Relation-like NAT -defined dom ((CQC-WFF f),p) -defined NAT -defined CQC-WFF f -valued Function-like finite FinSubsequence-like Element of bool [:NAT,(CQC-WFF f):]
p . x is set
((CQC-WFF f),p) . x is set
(((CQC-WFF f),p) ^ <*(f,p)*>) . x is set
dom <*(f,p)*> is non empty trivial finite 1 -element Element of bool NAT
<*(f,p)*> . 1 is set
len <*(f,p)*> is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
(len ((CQC-WFF f),p)) + (len <*(f,p)*>) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
len (((CQC-WFF f),p) ^ <*(f,p)*>) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
rng <*(f,p)*> is non empty trivial finite 1 -element Element of bool (CQC-WFF f)
(rng ((CQC-WFF f),p)) \/ (rng <*(f,p)*>) is non empty finite Element of bool (CQC-WFF f)
f is Relation-like non empty QC-alphabet
CQC-WFF f is non empty Element of bool (QC-WFF f)
QC-WFF f is non empty set
bool (QC-WFF f) is non empty set
p is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
len p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
((CQC-WFF f),p) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
len ((CQC-WFF f),p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
(len ((CQC-WFF f),p)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
f is Relation-like non empty QC-alphabet
QC-WFF f is non empty set
CQC-WFF f is non empty Element of bool (QC-WFF f)
bool (QC-WFF f) is non empty set
p is Element of CQC-WFF f
<*p*> is Relation-like NAT -defined CQC-WFF f -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
x is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
x ^ <*p*> is Relation-like NAT -defined CQC-WFF f -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
(f,(x ^ <*p*>)) is Element of CQC-WFF f
((CQC-WFF f),(x ^ <*p*>)) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
len (x ^ <*p*>) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
len x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
(len x) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
(x ^ <*p*>) . (len (x ^ <*p*>)) is set
f1 is set
dom x is finite Element of bool NAT
F is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal set
x . F is set
[F,(x . F)] is V22() set
{F,(x . F)} is non empty finite set
{F} is non empty trivial finite V37() 1 -element set
{{F,(x . F)},{F}} is non empty finite V37() set
dom (x ^ <*p*>) is non empty finite Element of bool NAT
(x ^ <*p*>) . F is set
(x ^ <*p*>) | (dom x) is Relation-like NAT -defined dom x -defined NAT -defined CQC-WFF f -valued Function-like finite FinSubsequence-like Element of bool [:NAT,(CQC-WFF f):]
[:NAT,(CQC-WFF f):] is Relation-like non empty non trivial non finite set
bool [:NAT,(CQC-WFF f):] is non empty non trivial non finite set
Seg (len x) is finite len x -element Element of bool NAT
(x ^ <*p*>) | (Seg (len x)) is Relation-like NAT -defined Seg (len x) -defined NAT -defined CQC-WFF f -valued Function-like finite FinSubsequence-like Element of bool [:NAT,(CQC-WFF f):]
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
p is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f ^ p is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len (f ^ p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
len p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
p ^ f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len (p ^ f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
(len f) + (len p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
(len p) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
f is Relation-like non empty QC-alphabet
CQC-WFF f is non empty Element of bool (QC-WFF f)
QC-WFF f is non empty set
bool (QC-WFF f) is non empty set
p is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
dom p is finite Element of bool NAT
x is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
p ^ x is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
(p ^ x) | (dom p) is Relation-like NAT -defined dom p -defined NAT -defined CQC-WFF f -valued Function-like finite FinSubsequence-like Element of bool [:NAT,(CQC-WFF f):]
[:NAT,(CQC-WFF f):] is Relation-like non empty non trivial non finite set
bool [:NAT,(CQC-WFF f):] is non empty non trivial non finite set
Seq ((p ^ x) | (dom p)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f is Relation-like non empty QC-alphabet
CQC-WFF f is non empty Element of bool (QC-WFF f)
QC-WFF f is non empty set
bool (QC-WFF f) is non empty set
p is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
x is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
p ^ x is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
len p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
Seg (len p) is finite len p -element Element of bool NAT
y0 is finite len p -element Element of bool NAT
(p ^ x) | y0 is Relation-like NAT -defined y0 -defined NAT -defined CQC-WFF f -valued Function-like finite FinSubsequence-like Element of bool [:NAT,(CQC-WFF f):]
[:NAT,(CQC-WFF f):] is Relation-like non empty non trivial non finite set
bool [:NAT,(CQC-WFF f):] is non empty non trivial non finite set
Seq ((p ^ x) | y0) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom p is finite Element of bool NAT
f1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f is set
<*f*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set
p is set
<*p*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set
x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
x ^ <*f*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
(x ^ <*f*>) ^ <*p*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
len ((x ^ <*f*>) ^ <*p*>) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
len (x ^ <*f*>) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
len <*p*> is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
(len (x ^ <*f*>)) + (len <*p*>) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
(len (x ^ <*f*>)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
len x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
len <*f*> is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
(len x) + (len <*f*>) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
((len x) + (len <*f*>)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
(len x) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
((len x) + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
(len x) + (1 + 1) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
f is set
<*f*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set
p is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
p ^ <*f*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
len (p ^ <*f*>) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
dom (p ^ <*f*>) is non empty finite Element of bool NAT
len p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
(len p) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
Seg p is finite p -element Element of bool NAT
p + f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
{(p + f)} is non empty trivial finite V37() 1 -element Element of bool NAT
(Seg p) \/ {(p + f)} is non empty finite Element of bool NAT
Sgm ((Seg p) \/ {(p + f)}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
len (Sgm ((Seg p) \/ {(p + f)})) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
p + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
card ((Seg p) \/ {(p + f)}) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
card (Seg p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
(card (Seg p)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
f + p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
Seg (p + f) is finite p + f -element Element of bool NAT
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
Seg p is finite p -element Element of bool NAT
p + f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
{(p + f)} is non empty trivial finite V37() 1 -element Element of bool NAT
(Seg p) \/ {(p + f)} is non empty finite Element of bool NAT
Sgm ((Seg p) \/ {(p + f)}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
dom (Sgm ((Seg p) \/ {(p + f)})) is finite Element of bool NAT
p + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
Seg (p + 1) is non empty finite p + 1 -element Element of bool NAT
len (Sgm ((Seg p) \/ {(p + f)})) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
f is Relation-like non empty QC-alphabet
CQC-WFF f is non empty Element of bool (QC-WFF f)
QC-WFF f is non empty set
bool (QC-WFF f) is non empty set
p is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
len p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
((CQC-WFF f),p) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
(f,p) is Element of CQC-WFF f
<*(f,p)*> is Relation-like NAT -defined CQC-WFF f -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
x is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
((CQC-WFF f),p) ^ x is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
(((CQC-WFF f),p) ^ x) ^ <*(f,p)*> is Relation-like NAT -defined CQC-WFF f -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
len ((CQC-WFF f),p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
len x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
Seg (len ((CQC-WFF f),p)) is finite len ((CQC-WFF f),p) -element Element of bool NAT
(len x) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
(len ((CQC-WFF f),p)) + ((len x) + 1) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
{((len ((CQC-WFF f),p)) + ((len x) + 1))} is non empty trivial finite V37() 1 -element Element of bool NAT
(Seg (len ((CQC-WFF f),p))) \/ {((len ((CQC-WFF f),p)) + ((len x) + 1))} is non empty finite Element of bool NAT
((((CQC-WFF f),p) ^ x) ^ <*(f,p)*>) | ((Seg (len ((CQC-WFF f),p))) \/ {((len ((CQC-WFF f),p)) + ((len x) + 1))}) is Relation-like NAT -defined (Seg (len ((CQC-WFF f),p))) \/ {((len ((CQC-WFF f),p)) + ((len x) + 1))} -defined NAT -defined CQC-WFF f -valued Function-like finite FinSubsequence-like Element of bool [:NAT,(CQC-WFF f):]
[:NAT,(CQC-WFF f):] is Relation-like non empty non trivial non finite set
bool [:NAT,(CQC-WFF f):] is non empty non trivial non finite set
Seq (((((CQC-WFF f),p) ^ x) ^ <*(f,p)*>) | ((Seg (len ((CQC-WFF f),p))) \/ {((len ((CQC-WFF f),p)) + ((len x) + 1))})) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
a is set
a is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
(len ((CQC-WFF f),p)) + (len x) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
((len ((CQC-WFF f),p)) + (len x)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
len ((((CQC-WFF f),p) ^ x) ^ <*(f,p)*>) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
len (((CQC-WFF f),p) ^ x) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
len <*(f,p)*> is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
(len (((CQC-WFF f),p) ^ x)) + (len <*(f,p)*>) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
((len ((CQC-WFF f),p)) + (len x)) + (len <*(f,p)*>) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
dom ((((CQC-WFF f),p) ^ x) ^ <*(f,p)*>) is non empty finite Element of bool NAT
x ^ <*(f,p)*> is Relation-like NAT -defined CQC-WFF f -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
((CQC-WFF f),p) ^ (x ^ <*(f,p)*>) is Relation-like NAT -defined CQC-WFF f -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
b is Relation-like NAT -defined Function-like FinSubsequence-like set
dom b is Element of bool NAT
(dom ((((CQC-WFF f),p) ^ x) ^ <*(f,p)*>)) /\ ((Seg (len ((CQC-WFF f),p))) \/ {((len ((CQC-WFF f),p)) + ((len x) + 1))}) is finite Element of bool NAT
Sgm (dom b) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
dom (Sgm (dom b)) is finite Element of bool NAT
(len ((CQC-WFF f),p)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
Seg ((len ((CQC-WFF f),p)) + 1) is non empty finite (len ((CQC-WFF f),p)) + 1 -element Element of bool NAT
a is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
dom p is finite Element of bool NAT
a is set
a is set
a is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
a is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
((len ((CQC-WFF f),p)) + 1) + (len x) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
a is set
a is set
k is set
[a,k] is V22() set
{a,k} is non empty finite set
{a} is non empty trivial finite 1 -element set
{{a,k},{a}} is non empty finite V37() set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
Seg ((len ((CQC-WFF f),p)) + ((len x) + 1)) is non empty finite (len ((CQC-WFF f),p)) + ((len x) + 1) -element Element of bool NAT
Sgm (Seg (len ((CQC-WFF f),p))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
Sgm {((len ((CQC-WFF f),p)) + ((len x) + 1))} is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(Sgm (Seg (len ((CQC-WFF f),p)))) ^ (Sgm {((len ((CQC-WFF f),p)) + ((len x) + 1))}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*((len ((CQC-WFF f),p)) + ((len x) + 1))*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
(Sgm (Seg (len ((CQC-WFF f),p)))) ^ <*((len ((CQC-WFF f),p)) + ((len x) + 1))*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
idseq (len ((CQC-WFF f),p)) is Relation-like NAT -defined Function-like finite len ((CQC-WFF f),p) -element FinSequence-like FinSubsequence-like set
id (Seg (len ((CQC-WFF f),p))) is Relation-like Seg (len ((CQC-WFF f),p)) -defined Seg (len ((CQC-WFF f),p)) -valued Function-like one-to-one V14( Seg (len ((CQC-WFF f),p))) finite Element of bool [:(Seg (len ((CQC-WFF f),p))),(Seg (len ((CQC-WFF f),p))):]
[:(Seg (len ((CQC-WFF f),p))),(Seg (len ((CQC-WFF f),p))):] is Relation-like finite set
bool [:(Seg (len ((CQC-WFF f),p))),(Seg (len ((CQC-WFF f),p))):] is non empty finite V37() set
(idseq (len ((CQC-WFF f),p))) ^ <*((len ((CQC-WFF f),p)) + ((len x) + 1))*> is Relation-like NAT -defined Function-like non empty finite (len ((CQC-WFF f),p)) + 1 -element FinSequence-like FinSubsequence-like set
(len ((CQC-WFF f),p)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
dom ((CQC-WFF f),p) is finite Element of bool NAT
dom (idseq (len ((CQC-WFF f),p))) is finite len ((CQC-WFF f),p) -element Element of bool NAT
(Sgm (dom b)) . p is set
(idseq (len ((CQC-WFF f),p))) . p is set
Seq b is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(Sgm (dom b)) * b is Relation-like NAT -defined Function-like finite set
(Seq b) . p is set
b . p is set
b | (Seg (len ((CQC-WFF f),p))) is Relation-like NAT -defined Seg (len ((CQC-WFF f),p)) -defined NAT -defined Function-like finite FinSubsequence-like set
(b | (Seg (len ((CQC-WFF f),p)))) . p is set
((((CQC-WFF f),p) ^ x) ^ <*(f,p)*>) | (Seg (len ((CQC-WFF f),p))) is Relation-like NAT -defined Seg (len ((CQC-WFF f),p)) -defined NAT -defined CQC-WFF f -valued Function-like finite FinSubsequence-like Element of bool [:NAT,(CQC-WFF f):]
(((((CQC-WFF f),p) ^ x) ^ <*(f,p)*>) | (Seg (len ((CQC-WFF f),p)))) . p is set
((CQC-WFF f),p) . p is set
((CQC-WFF f),p) ^ <*(f,p)*> is Relation-like NAT -defined CQC-WFF f -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
p . p is set
dom (((((CQC-WFF f),p) ^ x) ^ <*(f,p)*>) | ((Seg (len ((CQC-WFF f),p))) \/ {((len ((CQC-WFF f),p)) + ((len x) + 1))})) is finite Element of bool ((Seg (len ((CQC-WFF f),p))) \/ {((len ((CQC-WFF f),p)) + ((len x) + 1))})
bool ((Seg (len ((CQC-WFF f),p))) \/ {((len ((CQC-WFF f),p)) + ((len x) + 1))}) is non empty finite V37() set
Sgm (dom (((((CQC-WFF f),p) ^ x) ^ <*(f,p)*>) | ((Seg (len ((CQC-WFF f),p))) \/ {((len ((CQC-WFF f),p)) + ((len x) + 1))}))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
rng (Sgm (dom (((((CQC-WFF f),p) ^ x) ^ <*(f,p)*>) | ((Seg (len ((CQC-WFF f),p))) \/ {((len ((CQC-WFF f),p)) + ((len x) + 1))})))) is finite Element of bool NAT
(((((CQC-WFF f),p) ^ x) ^ <*(f,p)*>) | ((Seg (len ((CQC-WFF f),p))) \/ {((len ((CQC-WFF f),p)) + ((len x) + 1))})) * (Sgm (dom (((((CQC-WFF f),p) ^ x) ^ <*(f,p)*>) | ((Seg (len ((CQC-WFF f),p))) \/ {((len ((CQC-WFF f),p)) + ((len x) + 1))})))) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite Element of bool [:NAT,(CQC-WFF f):]
dom ((((((CQC-WFF f),p) ^ x) ^ <*(f,p)*>) | ((Seg (len ((CQC-WFF f),p))) \/ {((len ((CQC-WFF f),p)) + ((len x) + 1))})) * (Sgm (dom (((((CQC-WFF f),p) ^ x) ^ <*(f,p)*>) | ((Seg (len ((CQC-WFF f),p))) \/ {((len ((CQC-WFF f),p)) + ((len x) + 1))}))))) is finite Element of bool NAT
dom (Seq b) is finite Element of bool NAT
dom <*(f,p)*> is non empty trivial finite 1 -element Element of bool NAT
len (idseq (len ((CQC-WFF f),p))) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
b . ((len ((CQC-WFF f),p)) + ((len x) + 1)) is set
((((CQC-WFF f),p) ^ x) ^ <*(f,p)*>) . (((len ((CQC-WFF f),p)) + (len x)) + 1) is set
<*(f,p)*> . 1 is set
p . (len p) is set
p . a is set
f is Relation-like non empty QC-alphabet
CQC-WFF f is non empty Element of bool (QC-WFF f)
QC-WFF f is non empty set
bool (QC-WFF f) is non empty set
p is set
x is set
<*p,x*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like set
dom <*p,x*> is non empty finite 2 -element Element of bool NAT
f is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
f ^ <*p,x*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
len f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
(len f) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
(f ^ <*p,x*>) . ((len f) + 1) is set
(len f) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
(f ^ <*p,x*>) . ((len f) + 2) is set
len <*p,x*> is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V28() V29() finite cardinal Element of NAT
<*p,x*> . 2 is set
<*p,x*> . 1 is set
f is Relation-like non empty QC-alphabet
CQC-WFF f is non empty Element of bool (QC-WFF f)
QC-WFF f is non empty set
bool (QC-WFF f) is non empty set
bound_QC-variables f is non empty Element of bool (QC-variables f)
QC-variables f is non empty set
bool (QC-variables f) is non empty set
bool (bound_QC-variables f) is non empty set
p is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
dom p is finite Element of bool NAT
x is set
f is set
f is set
f1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
F is Element of CQC-WFF f
p . f1 is set
y0 is set
still_not-bound_in F is Element of bool (bound_QC-variables f)
x is Element of bool (bound_QC-variables f)
f is Element of bool (bound_QC-variables f)
y0 is set
f1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
F is Element of CQC-WFF f
p . f1 is set
still_not-bound_in F is Element of bool (bound_QC-variables f)
f1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
F is Element of CQC-WFF f
p . f1 is set
still_not-bound_in F is Element of bool (bound_QC-variables f)
f is Relation-like non empty QC-alphabet
CQC-WFF f is non empty Element of bool (QC-WFF f)
QC-WFF f is non empty set
bool (QC-WFF f) is non empty set
[:NAT,(CQC-WFF f):] is Relation-like REAL -defined QC-WFF f -valued non empty non trivial non finite Element of bool [:REAL,(QC-WFF f):]
[:REAL,(QC-WFF f):] is Relation-like set
bool [:REAL,(QC-WFF f):] is non empty set
bool [:NAT,(CQC-WFF f):] is non empty non trivial non finite set
p is set
x is set
f is set
p is set
x is set
f is set
f is Relation-like non empty QC-alphabet
(f) is set
[:(f),Proof_Step_Kinds:] is Relation-like set
p is Relation-like NAT -defined [:(f),Proof_Step_Kinds:] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:(f),Proof_Step_Kinds:]
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal set
p . x is set
(p . x) `2 is set
CQC-WFF f is non empty Element of bool (QC-WFF f)
QC-WFF f is non empty set
bool (QC-WFF f) is non empty set
(p . x) `1 is set
VERUM f is Element of CQC-WFF f
<*(VERUM f)*> is Relation-like NAT -defined CQC-WFF f -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
QC-variables f is non empty set
bound_QC-variables f is non empty Element of bool (QC-variables f)
bool (QC-variables f) is non empty set
f is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
((CQC-WFF f),f) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
(f,f) is Element of CQC-WFF f
y0 is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
y0 ^ <*(VERUM f)*> is Relation-like NAT -defined CQC-WFF f -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
f1 is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
((CQC-WFF f),f1) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
(f,f1) is Element of CQC-WFF f
F is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
b is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
((CQC-WFF f),b) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
a is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
((CQC-WFF f),a) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
(f,b) is Element of CQC-WFF f
(f,a) is Element of CQC-WFF f
p . F is set
(p . F) `1 is set
a is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
((CQC-WFF f),a) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
(f,a) is Element of CQC-WFF f
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
x is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
len x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
y is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
len y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
((CQC-WFF f),x) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
((CQC-WFF f),((CQC-WFF f),x)) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
((CQC-WFF f),y) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
((CQC-WFF f),((CQC-WFF f),y)) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
(f,((CQC-WFF f),x)) is Element of CQC-WFF f
'not' (f,((CQC-WFF f),x)) is Element of CQC-WFF f
(f,((CQC-WFF f),y)) is Element of CQC-WFF f
(f,x) is Element of CQC-WFF f
(f,y) is Element of CQC-WFF f
p . p is set
(p . p) `1 is set
p . k is set
(p . k) `1 is set
<*(f,x)*> is Relation-like NAT -defined CQC-WFF f -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
((CQC-WFF f),((CQC-WFF f),x)) ^ <*(f,x)*> is Relation-like NAT -defined CQC-WFF f -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
c15 is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
((CQC-WFF f),c15) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
(f,c15) is Element of CQC-WFF f
c16 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
c17 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
c18 is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
len c18 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
((CQC-WFF f),c18) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
c19 is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
((CQC-WFF f),c19) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
(f,((CQC-WFF f),c18)) is Element of CQC-WFF f
c20 is Element of CQC-WFF f
'not' c20 is Element of CQC-WFF f
(f,c18) is Element of CQC-WFF f
'not' (f,c18) is Element of CQC-WFF f
(f,c19) is Element of CQC-WFF f
p . c17 is set
(p . c17) `1 is set
p . c16 is set
(p . c16) `1 is set
((CQC-WFF f),((CQC-WFF f),c18)) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
<*c20*> is Relation-like NAT -defined CQC-WFF f -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
((CQC-WFF f),((CQC-WFF f),c18)) ^ <*c20*> is Relation-like NAT -defined CQC-WFF f -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
c21 is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
((CQC-WFF f),c21) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
(f,c21) is Element of CQC-WFF f
c22 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
c23 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
c24 is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
((CQC-WFF f),c24) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
c25 is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
((CQC-WFF f),c25) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
p . c23 is set
(p . c23) `1 is set
p . c22 is set
(p . c22) `1 is set
(f,c24) is Element of CQC-WFF f
(f,c25) is Element of CQC-WFF f
(f,c24) '&' (f,c25) is Element of CQC-WFF f
<*((f,c24) '&' (f,c25))*> is Relation-like NAT -defined CQC-WFF f -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
((CQC-WFF f),c24) ^ <*((f,c24) '&' (f,c25))*> is Relation-like NAT -defined CQC-WFF f -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
c26 is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
((CQC-WFF f),c26) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
(f,c26) is Element of CQC-WFF f
c27 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
c29 is Element of CQC-WFF f
c30 is Element of CQC-WFF f
c29 '&' c30 is Element of CQC-WFF f
c28 is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
(f,c28) is Element of CQC-WFF f
p . c27 is set
(p . c27) `1 is set
((CQC-WFF f),c28) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
<*c29*> is Relation-like NAT -defined CQC-WFF f -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
((CQC-WFF f),c28) ^ <*c29*> is Relation-like NAT -defined CQC-WFF f -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
c31 is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
((CQC-WFF f),c31) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
(f,c31) is Element of CQC-WFF f
c32 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
c34 is Element of CQC-WFF f
c35 is Element of CQC-WFF f
c34 '&' c35 is Element of CQC-WFF f
c33 is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
(f,c33) is Element of CQC-WFF f
p . c32 is set
(p . c32) `1 is set
((CQC-WFF f),c33) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
<*c35*> is Relation-like NAT -defined CQC-WFF f -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
((CQC-WFF f),c33) ^ <*c35*> is Relation-like NAT -defined CQC-WFF f -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
c36 is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
((CQC-WFF f),c36) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
(f,c36) is Element of CQC-WFF f
c37 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
c38 is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
(f,c38) is Element of CQC-WFF f
c40 is Element of bound_QC-variables f
c39 is Element of CQC-WFF f
All (c40,c39) is Element of CQC-WFF f
p . c37 is set
(p . c37) `1 is set
((CQC-WFF f),c38) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
c41 is Element of bound_QC-variables f
c39 . (c40,c41) is Element of CQC-WFF f
<*(c39 . (c40,c41))*> is Relation-like NAT -defined CQC-WFF f -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
((CQC-WFF f),c38) ^ <*(c39 . (c40,c41))*> is Relation-like NAT -defined CQC-WFF f -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
c42 is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
((CQC-WFF f),c42) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
(f,c42) is Element of CQC-WFF f
c43 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
c44 is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
(f,c44) is Element of CQC-WFF f
c45 is Element of CQC-WFF f
c46 is Element of bound_QC-variables f
c47 is Element of bound_QC-variables f
c45 . (c46,c47) is Element of CQC-WFF f
((CQC-WFF f),c44) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
(f,((CQC-WFF f),c44)) is Element of bool (bound_QC-variables f)
bool (bound_QC-variables f) is non empty set
All (c46,c45) is Element of CQC-WFF f
still_not-bound_in (All (c46,c45)) is Element of bool (bound_QC-variables f)
p . c43 is set
(p . c43) `1 is set
<*(All (c46,c45))*> is Relation-like NAT -defined CQC-WFF f -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
((CQC-WFF f),c44) ^ <*(All (c46,c45))*> is Relation-like NAT -defined CQC-WFF f -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
c48 is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
c48 ^ <*(VERUM f)*> is Relation-like NAT -defined CQC-WFF f -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
c49 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
c50 is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
((CQC-WFF f),c50) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
c51 is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
((CQC-WFF f),c51) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
(f,c50) is Element of CQC-WFF f
(f,c51) is Element of CQC-WFF f
p . c49 is set
(p . c49) `1 is set
c52 is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
c52 ^ <*(VERUM f)*> is Relation-like NAT -defined CQC-WFF f -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
c53 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
c54 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
c55 is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
len c55 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
c56 is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
len c56 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
((CQC-WFF f),c55) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
((CQC-WFF f),((CQC-WFF f),c55)) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
((CQC-WFF f),c56) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
((CQC-WFF f),((CQC-WFF f),c56)) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
(f,((CQC-WFF f),c55)) is Element of CQC-WFF f
'not' (f,((CQC-WFF f),c55)) is Element of CQC-WFF f
(f,((CQC-WFF f),c56)) is Element of CQC-WFF f
(f,c55) is Element of CQC-WFF f
(f,c56) is Element of CQC-WFF f
p . c54 is set
(p . c54) `1 is set
p . c53 is set
(p . c53) `1 is set
<*(f,c55)*> is Relation-like NAT -defined CQC-WFF f -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
((CQC-WFF f),((CQC-WFF f),c55)) ^ <*(f,c55)*> is Relation-like NAT -defined CQC-WFF f -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
c57 is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
c57 ^ <*(VERUM f)*> is Relation-like NAT -defined CQC-WFF f -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
c58 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
c59 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
c60 is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
len c60 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
((CQC-WFF f),c60) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
c61 is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
((CQC-WFF f),c61) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
(f,((CQC-WFF f),c60)) is Element of CQC-WFF f
c62 is Element of CQC-WFF f
'not' c62 is Element of CQC-WFF f
(f,c60) is Element of CQC-WFF f
'not' (f,c60) is Element of CQC-WFF f
(f,c61) is Element of CQC-WFF f
p . c59 is set
(p . c59) `1 is set
p . c58 is set
(p . c58) `1 is set
((CQC-WFF f),((CQC-WFF f),c60)) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
<*c62*> is Relation-like NAT -defined CQC-WFF f -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
((CQC-WFF f),((CQC-WFF f),c60)) ^ <*c62*> is Relation-like NAT -defined CQC-WFF f -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
c63 is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
c63 ^ <*(VERUM f)*> is Relation-like NAT -defined CQC-WFF f -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
c64 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
c65 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
c66 is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
((CQC-WFF f),c66) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
c67 is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
((CQC-WFF f),c67) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
p . c65 is set
(p . c65) `1 is set
p . c64 is set
(p . c64) `1 is set
(f,c66) is Element of CQC-WFF f
(f,c67) is Element of CQC-WFF f
(f,c66) '&' (f,c67) is Element of CQC-WFF f
<*((f,c66) '&' (f,c67))*> is Relation-like NAT -defined CQC-WFF f -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
((CQC-WFF f),c66) ^ <*((f,c66) '&' (f,c67))*> is Relation-like NAT -defined CQC-WFF f -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
c68 is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
c68 ^ <*(VERUM f)*> is Relation-like NAT -defined CQC-WFF f -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
c69 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
c71 is Element of CQC-WFF f
c72 is Element of CQC-WFF f
c71 '&' c72 is Element of CQC-WFF f
c70 is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
(f,c70) is Element of CQC-WFF f
p . c69 is set
(p . c69) `1 is set
((CQC-WFF f),c70) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
<*c71*> is Relation-like NAT -defined CQC-WFF f -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
((CQC-WFF f),c70) ^ <*c71*> is Relation-like NAT -defined CQC-WFF f -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
c73 is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
c73 ^ <*(VERUM f)*> is Relation-like NAT -defined CQC-WFF f -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
c74 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
c76 is Element of CQC-WFF f
c77 is Element of CQC-WFF f
c76 '&' c77 is Element of CQC-WFF f
c75 is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
(f,c75) is Element of CQC-WFF f
p . c74 is set
(p . c74) `1 is set
((CQC-WFF f),c75) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
<*c77*> is Relation-like NAT -defined CQC-WFF f -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
((CQC-WFF f),c75) ^ <*c77*> is Relation-like NAT -defined CQC-WFF f -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
c78 is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
c78 ^ <*(VERUM f)*> is Relation-like NAT -defined CQC-WFF f -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
c79 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V28() V29() finite cardinal Element of NAT
c80 is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
(f,c80) is Element of CQC-WFF f
c82 is Element of bound_QC-variables f
c81 is Element of CQC-WFF f
All (c82,c81) is Element of CQC-WFF f
p . c79 is set
(p . c79) `1 is set
((CQC-WFF f),c80) is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
c83 is Element of bound_QC-variables f
c81 . (c82,c83) is Element of CQC-WFF f
<*(c81 . (c82,c83))*> is Relation-like NAT -defined CQC-WFF f -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
((CQC-WFF f),c80) ^ <*(c81 . (c82,c83))*> is Relation-like NAT -defined CQC-WFF f -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF f
c84 is Relation-like NAT -defined CQC-WFF f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF</