:: HILBERT2 semantic presentation

REAL is set
NAT is non empty epsilon-transitive epsilon-connected ordinal Element of bool REAL
bool REAL is non empty set
NAT is non empty epsilon-transitive epsilon-connected ordinal set
bool NAT is non empty set
bool NAT is non empty set
{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V29() ext-real non negative V33() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V50() constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding set
1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
{{},1} is non empty set
Trees is non empty constituted-Trees set
bool Trees is non empty set
FinTrees is non empty constituted-Trees constituted-FinTrees Element of bool Trees
HP-WFF is functional non empty with_VERUM with_implication with_conjunction with_propositional_variables HP-closed set
bool HP-WFF is non empty set
2 is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
3 is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V29() ext-real non negative V33() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V50() constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding Element of NAT
<*0*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*1*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*2*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
NAT * is functional non empty FinSequence-membered set
Seg 1 is non empty V33() V40(1) Element of bool NAT
<*> NAT is Relation-like non-empty empty-yielding NAT -defined NAT -valued Function-like one-to-one constant functional empty proper V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V29() ext-real non negative V33() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V50() constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding FinSequence of NAT
[:NAT,NAT:] is Relation-like non empty set
elementary_tree 0 is non empty Tree-like set
{{}} is functional non empty set
tree {} is non empty V33() Tree-like set
dom {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V29() ext-real non negative V33() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V50() constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding set
rng {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty trivial V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V29() ext-real non negative V33() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V50() constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding set
len {} is V38() set
p is set
union p is set
q is Relation-like p -defined Function-like total set
Union q is set
x is Relation-like Function-like set
dom x is set
rng q is set
union (rng q) is set
f is set
x . f is set
[f,(x . f)] is set
{f,(x . f)} is non empty set
{f} is non empty set
{{f,(x . f)},{f}} is non empty set
r is set
dom q is set
s is set
q . s is set
s is Relation-like s -defined Function-like total set
dom s is set
r is set
q . r is set
s is Relation-like r -defined Function-like total set
dom s is set
s . f is set
[f,(s . f)] is set
{f,(s . f)} is non empty set
{f} is non empty set
{{f,(s . f)},{f}} is non empty set
dom q is set
p is set
<*p*> is Relation-like NAT -defined Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like set
q is set
<*q*> is Relation-like NAT -defined Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like set
x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
<*p*> ^ x is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
<*q*> ^ f is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*q*> ^ f) . 1 is set
p is set
<*p*> is Relation-like NAT -defined Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like set
q is set
rng <*p*> is non empty set
{p} is non empty set
p is set
q is Relation-like NAT -defined p -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of p
x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
f is set
<*f*> is Relation-like NAT -defined Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like set
x ^ <*f*> is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
r is Relation-like NAT -defined p -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of p
r ^ <*f*> is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
p is set
<*p*> is Relation-like NAT -defined Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like set
q is non empty Tree-like set
x is non empty Tree-like set
tree (q,x) is non empty Tree-like set
<*q,x*> is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like Tree-yielding set
len <*q,x*> is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
tree <*q,x*> is non empty Tree-like set
f is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
r is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
f + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
<*q,x*> . (f + 1) is set
<*f*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*f*> ^ r is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
<*p*> . 1 is set
f is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
f + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
<*q,x*> . (f + 1) is set
<*f*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*f*> ^ {} is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
F₁() is non empty Tree-like set
p is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
q is set
<*q*> is Relation-like NAT -defined Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like set
p ^ <*q*> is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
x is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
f is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
r is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
<*r*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
f ^ <*r*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() FinSequence-like FinSubsequence-like FinSequence of NAT
s is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like Element of F₁()
p is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like Element of F₁()
p is set
q is Relation-like Function-like DecoratedTree-like set
x is Relation-like Function-like DecoratedTree-like set
p -tree (q,x) is Relation-like Function-like DecoratedTree-like set
(p -tree (q,x)) . {} is set
<*q,x*> is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like DTree-yielding set
p -tree <*q,x*> is Relation-like Function-like DecoratedTree-like set
p is set
q is Relation-like Function-like DecoratedTree-like set
q . {} is set
x is Relation-like Function-like DecoratedTree-like set
p -tree (q,x) is Relation-like Function-like DecoratedTree-like set
(p -tree (q,x)) . <*0*> is set
(p -tree (q,x)) . <*1*> is set
x . {} is set
<*q,x*> is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like DTree-yielding set
len <*q,x*> is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
dom q is non empty Tree-like set
0 + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
<*q,x*> . (0 + 1) is set
p -tree <*q,x*> is Relation-like Function-like DecoratedTree-like set
(p -tree <*q,x*>) . <*0*> is set
f is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like Element of dom q
<*0*> ^ f is Relation-like NAT -defined NAT -valued Function-like non empty V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(p -tree <*q,x*>) . (<*0*> ^ f) is set
dom x is non empty Tree-like set
1 + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
<*q,x*> . (1 + 1) is set
(p -tree <*q,x*>) . <*1*> is set
r is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like Element of dom x
<*1*> ^ r is Relation-like NAT -defined NAT -valued Function-like non empty V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(p -tree <*q,x*>) . (<*1*> ^ r) is set
p is set
q is Relation-like Function-like DecoratedTree-like set
x is Relation-like Function-like DecoratedTree-like set
p -tree (q,x) is Relation-like Function-like DecoratedTree-like set
(p -tree (q,x)) | <*0*> is Relation-like Function-like DecoratedTree-like set
(p -tree (q,x)) | <*1*> is Relation-like Function-like DecoratedTree-like set
<*q,x*> is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like DTree-yielding set
len <*q,x*> is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
p -tree <*q,x*> is Relation-like Function-like DecoratedTree-like set
(p -tree <*q,x*>) | <*0*> is Relation-like Function-like DecoratedTree-like set
0 + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
<*q,x*> . (0 + 1) is set
(p -tree <*q,x*>) | <*1*> is Relation-like Function-like DecoratedTree-like set
1 + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
<*q,x*> . (1 + 1) is set
p is set
q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like DTree-yielding set
p -tree q is Relation-like Function-like DecoratedTree-like set
dom (p -tree q) is non empty Tree-like set
dom q is non empty Element of bool NAT
doms q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Tree-yielding set
x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like DTree-yielding set
doms x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Tree-yielding set
tree (doms x) is non empty Tree-like set
p is set
q is Relation-like Function-like DecoratedTree-like set
p -tree q is Relation-like Function-like DecoratedTree-like set
<*q*> is Relation-like NAT -defined Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like DTree-yielding set
p -tree <*q*> is Relation-like Function-like non trivial DecoratedTree-like set
x is Relation-like Function-like DecoratedTree-like set
p -tree (q,x) is Relation-like Function-like DecoratedTree-like set
<*q,x*> is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like DTree-yielding set
p -tree <*q,x*> is Relation-like Function-like non trivial DecoratedTree-like set
p is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
3 + p is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
<*(3 + p)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
p is set
VERUM is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
q is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
(q) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
3 + q is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
<*(3 + q)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
q is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
3 + q is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
<*(3 + q)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
(q) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
p is functional Element of bool HP-WFF
q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
q => x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
<*1*> ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*1*> ^ q) ^ x is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
<*1*> ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*1*> ^ q) ^ x is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
r is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
f => r is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
<*1*> ^ f is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*1*> ^ f) ^ r is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
q '&' x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
<*2*> ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*2*> ^ q) ^ x is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
<*2*> ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*2*> ^ q) ^ x is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
r is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
f '&' r is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
<*2*> ^ f is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*2*> ^ f) ^ r is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
{ b₁ where b₁ is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF : P₁[b₁] } is set
q is set
x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
q is functional Element of bool HP-WFF
f is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
(f) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
3 + f is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
<*(3 + f)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
r is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
f => r is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
<*1*> ^ f is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*1*> ^ f) ^ r is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
s is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
s is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
f is set
f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
r is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
f '&' r is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
<*2*> ^ f is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*2*> ^ f) ^ r is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
s is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
s is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
p is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
q is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
(q) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
3 + q is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
<*(3 + q)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
q '&' x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
<*2*> ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*2*> ^ q) ^ x is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
q => x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
<*1*> ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*1*> ^ q) ^ x is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
p is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
len p is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
q '&' x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
<*2*> ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*2*> ^ q) ^ x is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
q ^ x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
<*2*> ^ (q ^ x) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
len (<*2*> ^ (q ^ x)) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
len <*2*> is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
len (q ^ x) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
(len <*2*>) + (len (q ^ x)) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
1 + (len (q ^ x)) is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
q => x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
<*1*> ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*1*> ^ q) ^ x is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
q ^ x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
<*1*> ^ (q ^ x) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
len (<*1*> ^ (q ^ x)) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
len <*1*> is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
len (q ^ x) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
(len <*1*>) + (len (q ^ x)) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
1 + (len (q ^ x)) is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
q is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
(q) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
3 + q is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
<*(3 + q)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
p is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
p . 1 is set
q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
q '&' x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
<*2*> ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*2*> ^ q) ^ x is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
q ^ x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
<*2*> ^ (q ^ x) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
q is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
(q) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
3 + q is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
<*(3 + q)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
1 + 0 is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
2 + q is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
1 + (2 + q) is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
p is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
p . 1 is set
q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
q => x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
<*1*> ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*1*> ^ q) ^ x is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
q ^ x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
<*1*> ^ (q ^ x) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
q is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
(q) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
3 + q is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
<*(3 + q)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
2 + 0 is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
1 + q is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
2 + (1 + q) is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
p is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
3 + p is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
q . 1 is set
x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
x '&' f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
<*2*> ^ x is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*2*> ^ x) ^ f is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
x ^ f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
<*2*> ^ (x ^ f) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
2 + 0 is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
1 + p is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
2 + (1 + p) is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
x => f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
<*1*> ^ x is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*1*> ^ x) ^ f is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
x ^ f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
<*1*> ^ (x ^ f) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
1 + 0 is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
2 + p is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
1 + (2 + p) is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
p is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
p . 1 is set
q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
q '&' x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
<*2*> ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*2*> ^ q) ^ x is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
q ^ x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
<*2*> ^ (q ^ x) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
q => x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
<*1*> ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*1*> ^ q) ^ x is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
q ^ x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
<*1*> ^ (q ^ x) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
q is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
(q) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
3 + q is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
<*(3 + q)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
p is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
len p is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
p '&' q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
<*2*> ^ p is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*2*> ^ p) ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
len (p '&' q) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
len q is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
len (<*2*> ^ p) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
(len (<*2*> ^ p)) + (len q) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
len <*2*> is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
(len <*2*>) + (len p) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
((len <*2*>) + (len p)) + (len q) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
1 + (len p) is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
(1 + (len p)) + (len q) is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
(len p) + (len q) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
1 + ((len p) + (len q)) is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
p is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
len p is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
p => q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
<*1*> ^ p is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*1*> ^ p) ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
len (p => q) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
len q is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
len (<*1*> ^ p) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
(len (<*1*> ^ p)) + (len q) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
len <*1*> is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
(len <*1*>) + (len p) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
((len <*1*>) + (len p)) + (len q) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
1 + (len p) is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
(1 + (len p)) + (len q) is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
(len p) + (len q) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
1 + ((len p) + (len q)) is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
p is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
q ^ x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
f is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative set
r is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
len r is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
s is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
s is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
s ^ s is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
len s is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
r . 1 is set
s . 1 is set
s is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
c₉ is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
s '&' c₉ is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
<*2*> ^ s is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*2*> ^ s) ^ c₉ is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
s ^ c₉ is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
<*2*> ^ (s ^ c₉) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*2*> ^ (s ^ c₉)) . 1 is set
Y9 is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
IMrMs is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
Y9 '&' IMrMs is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
<*2*> ^ Y9 is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*2*> ^ Y9) ^ IMrMs is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
Y9 ^ IMrMs is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(Y9 ^ IMrMs) ^ s is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
<*2*> ^ ((Y9 ^ IMrMs) ^ s) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
<*2*> ^ (Y9 ^ IMrMs) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*2*> ^ (Y9 ^ IMrMs)) ^ s is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
IMrMs ^ s is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Y9 ^ (IMrMs ^ s) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
len s is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
len Y9 is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
len s is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
(len s) + (len s) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
N is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
s ^ N is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
len c₉ is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
len Y9 is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
len s is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
N is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Y9 ^ N is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
len c₉ is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
len s is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
len Y9 is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
s is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
c₉ is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
s => c₉ is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
<*1*> ^ s is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*1*> ^ s) ^ c₉ is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
s ^ c₉ is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
<*1*> ^ (s ^ c₉) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*1*> ^ (s ^ c₉)) . 1 is set
Y9 is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
IMrMs is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
Y9 => IMrMs is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
<*1*> ^ Y9 is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*1*> ^ Y9) ^ IMrMs is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
Y9 ^ IMrMs is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(Y9 ^ IMrMs) ^ s is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
<*1*> ^ ((Y9 ^ IMrMs) ^ s) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
<*1*> ^ (Y9 ^ IMrMs) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*1*> ^ (Y9 ^ IMrMs)) ^ s is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
IMrMs ^ s is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Y9 ^ (IMrMs ^ s) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
len s is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
len Y9 is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
len s is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
(len s) + (len s) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
N is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
s ^ N is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
len c₉ is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
len Y9 is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
len s is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
N is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Y9 ^ N is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
len c₉ is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
len s is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
len Y9 is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
s is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
(s) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
3 + s is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
<*(3 + s)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
len p is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
p is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
p ^ q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
x ^ f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
len p is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
len x is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
r is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
p ^ r is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
len x is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
len p is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
r is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
x ^ r is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
len p is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
len x is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
p is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
p '&' q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
<*2*> ^ p is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*2*> ^ p) ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
x '&' f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
<*2*> ^ x is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*2*> ^ x) ^ f is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
p ^ q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
<*2*> ^ (p ^ q) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
x ^ f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
<*2*> ^ (x ^ f) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
p is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
p => q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
<*1*> ^ p is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*1*> ^ p) ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
x => f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
<*1*> ^ x is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*1*> ^ x) ^ f is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
p ^ q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
<*1*> ^ (p ^ q) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
x ^ f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
<*1*> ^ (x ^ f) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
p is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
(p) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
3 + p is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
<*(3 + p)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
q is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
(q) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
3 + q is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
<*(3 + q)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
p is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
p '&' q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
<*2*> ^ p is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*2*> ^ p) ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
x => f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
<*1*> ^ x is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*1*> ^ x) ^ f is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
p ^ q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
<*2*> ^ (p ^ q) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
x ^ f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
<*1*> ^ (x ^ f) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(p '&' q) . 1 is set
p is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
p '&' q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
<*2*> ^ p is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*2*> ^ p) ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
p ^ q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
<*2*> ^ (p ^ q) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(p '&' q) . 1 is set
p is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
(p) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
3 + p is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
<*(3 + p)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
q '&' x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
<*2*> ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*2*> ^ q) ^ x is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
2 + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
(2 + 1) + p is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
2 + 0 is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
1 + p is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
2 + (1 + p) is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
q ^ x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
<*2*> ^ (q ^ x) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(q '&' x) . 1 is set
p is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
p => q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
<*1*> ^ p is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*1*> ^ p) ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
p ^ q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
<*1*> ^ (p ^ q) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(p => q) . 1 is set
p is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
(p) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
3 + p is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
<*(3 + p)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
q => x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
<*1*> ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*1*> ^ q) ^ x is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
1 + 2 is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
(1 + 2) + p is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
1 + 0 is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
2 + p is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
1 + (2 + p) is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
q ^ x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
<*1*> ^ (q ^ x) is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(q => x) . 1 is set
p is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
p '&' q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
<*2*> ^ p is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*2*> ^ p) ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
len (p '&' q) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
len p is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
p is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
p => q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
<*1*> ^ p is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*1*> ^ p) ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
len (p => q) is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
len p is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
p is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
(p) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
3 + p is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
<*(3 + p)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
VERUM . 1 is set
F₁() is set
{ (b₁) where b₁ is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT : verum } is set
{ b₁ where b₁ is functional Element of bool HP-WFF : ( VERUM in b₁ & ( for b₂ being V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT holds (b₂) in b₁ ) & ( for b₂, b₃ being Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF holds
( ( not b₂ '&' b₃ in b₁ & not b₂ => b₃ in b₁ ) or ( b₂ in b₁ & b₃ in b₁ ) ) ) & ex b₂ being Relation-like b₁ -defined Function-like total set st
( b₂ . VERUM = F₁() & ( for b₃ being V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT holds b₂ . (b₃) = F₂(b₃) ) & ( for b₃, b₄ being Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF holds
( not b₃ '&' b₄ in b₁ or for b₅, b₆, b₇ being set holds
( not b₅ = b₂ . b₃ or not b₆ = b₂ . b₄ or not b₇ = b₂ . (b₃ '&' b₄) or P₁[b₃,b₄,b₅,b₆,b₇] ) ) ) & ( for b₃, b₄ being Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF holds
( not b₃ => b₄ in b₁ or for b₅, b₆, b₇ being set holds
( not b₅ = b₂ . b₃ or not b₆ = b₂ . b₄ or not b₇ = b₂ . (b₃ => b₄) or P₂[b₃,b₄,b₅,b₆,b₇] ) ) ) ) ) } is set
x is set
f is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
(f) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
3 + f is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
<*(3 + f)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
{VERUM} is functional non empty set
{ (b₁) where b₁ is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT : verum } \/ {VERUM} is non empty set
x is functional Element of bool HP-WFF
f is set
r is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
(r) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
3 + r is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
<*(3 + r)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
F₂(r) is set
s is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
(s) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
3 + s is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
<*(3 + s)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
F₂(s) is set
r is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
(r) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
3 + r is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
<*(3 + r)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
F₂(r) is set
f is Relation-like x -defined Function-like total set
r is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
s is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
r '&' s is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
<*2*> ^ r is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*2*> ^ r) ^ s is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
r => s is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
<*1*> ^ r is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*1*> ^ r) ^ s is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
s is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
(s) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
3 + s is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
<*(3 + s)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
s is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
(s) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
3 + s is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
<*(3 + s)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
r is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
s is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
r '&' s is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
<*2*> ^ r is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*2*> ^ r) ^ s is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
r => s is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
<*1*> ^ r is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*1*> ^ r) ^ s is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
s is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
s is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
s '&' s is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
<*2*> ^ s is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*2*> ^ s) ^ s is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
c₉ is set
f . s is set
Y9 is set
f . s is set
IMrMs is set
f . (s '&' s) is set
r is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
(r) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
3 + r is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
<*(3 + r)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
r is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
(r) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
3 + r is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
<*(3 + r)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
f . (r) is set
F₂(r) is set
r is set
union r is set
s is set
s is functional Element of bool HP-WFF
s is Relation-like s -defined Function-like total set
s . VERUM is set
s is set
s is set
c₉ is functional Element of bool HP-WFF
Y9 is Relation-like c₉ -defined Function-like total set
Y9 . VERUM is set
Y9 is Relation-like c₉ -defined Function-like total set
Y9 . VERUM is set
s is Relation-like r -defined Function-like total set
rng s is set
c₉ is set
dom s is set
Y9 is set
s . Y9 is set
IMrMs is Relation-like Y9 -defined Function-like total set
IMrMs . VERUM is set
c₉ is functional set
Y9 is Relation-like Function-like set
IMrMs is Relation-like Function-like set
dom Y9 is set
dom IMrMs is set
dom s is set
N is set
s . N is set
N is Relation-like N -defined Function-like total set
N . VERUM is set
N is set
s . N is set
p is V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real non negative Element of NAT
(p) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
3 + p is non empty V21() epsilon-transitive epsilon-connected ordinal natural V29() ext-real positive non negative Element of NAT
<*(3 + p)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
Y9 . (p) is set
IMrMs . (p) is set
F₂(p) is set
q is Relation-like N -defined Function-like total set
q . VERUM is set
q is Relation-like N -defined Function-like total set
q . VERUM is set
p is Relation-like N -defined Function-like total set
p . VERUM is set
p is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
Y9 . p is set
IMrMs . p is set
q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
Y9 . q is set
IMrMs . q is set
p '&' q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
<*2*> ^ p is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*2*> ^ p) ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
Y9 . (p '&' q) is set
IMrMs . (p '&' q) is set
p => q is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
<*1*> ^ p is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*1*> ^ p) ^ q is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
Y9 . (p => q) is set
IMrMs . (p => q) is set
z is functional Element of bool HP-WFF
x is Relation-like N -defined Function-like total set
x . VERUM is set
y is Relation-like N -defined Function-like total set
y . VERUM is set
MZ1 is Relation-like z -defined Function-like total set
MZ1 . VERUM is set
z is functional Element of bool HP-WFF
x is Relation-like N -defined Function-like total set
x . VERUM is set
y is Relation-like N -defined Function-like total set
y . VERUM is set
MZ1 is Relation-like z -defined Function-like total set
MZ1 . VERUM is set
p is set
(dom Y9) /\ (dom IMrMs) is set
Y9 . p is set
IMrMs . p is set
Y9 . VERUM is set
IMrMs . VERUM is set
q is Relation-like N -defined Function-like total set
q . VERUM is set
x is Relation-like N -defined Function-like total set
x . VERUM is set
Y9 is Relation-like Function-like set
IMrMs is Relation-like Function-like set
dom s is set
N is set
s . N is set
dom Y9 is set
N is Relation-like N -defined Function-like total set
N . VERUM is set
N is set
s . N is set
dom IMrMs is set
p is Relation-like N -defined Function-like total set
p . VERUM is set
union c₉ is set
Union s is set
IMrMs is set
s . IMrMs is set
N is Relation-like IMrMs -defined Function-like total set
N . VERUM is set
Y9 is Relation-like Function-like set
dom Y9 is set
s is functional Element of bool HP-WFF
IMrMs is Relation-like s -defined Function-like total set
N is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
IMrMs . N is set
N is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
N '&' N is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of HP-WFF
<*2*> ^ N is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(<*2*> ^ N) ^ N is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
IMrMs . N is set
IMrMs . (N '&' N) is set
p is set
dom s is set
s . p is set
q is set
x is set
y is set
z is Relation-like p -defined Function-like total set
z . VERUM is set
dom z is set
z . (N '&' N) is set
MZ1 is functional Element of bool HP-WFF
c₂₀ is Relation-like MZ1 -defined Function-like total set
c₂₀ . VERUM is set
z . N is set
MZ1 is functional Element of bool HP-WFF
c₂₀ is Relation-like MZ1 -defined Function-like total set
c₂₀ . VERUM is set
z . N is set
dom s is set
s . s is set
N is Relation-like s -defined Function-like total set
N . VERUM is set
N is set
p is functional Element of bool HP-WFF
q is Relation-like p</