:: CALCUL_2 semantic presentation

REAL is set
NAT is non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal Element of K19(REAL)
K19(REAL) is set
omega is non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal set
K19(omega) is non finite set
K19(NAT) is non finite set
K283() is set
{} is set
the Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V25() V26() V33() finite cardinal {} -element FinSequence-membered set is Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V25() V26() V33() finite cardinal {} -element FinSequence-membered set
1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
2 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
0 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
Seg 1 is non empty V12() finite 1 -element Element of K19(NAT)
Al is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
1 + Al is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
p + Al is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + Al <= b₁ & b₁ <= p + Al ) } is set
Al is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
(Al,p) is set
1 + Al is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
p + Al is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + Al <= b₁ & b₁ <= p + Al ) } is set
n is set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
Al is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
1 + p is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
q is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
(p,q) is Element of K19(NAT)
q + p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + p <= b₁ & b₁ <= q + p ) } is set
n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
Al is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
(Al,0) is Element of K19(NAT)
1 + Al is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
0 + Al is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + Al <= b₁ & b₁ <= 0 + Al ) } is set
the Element of (Al,0) is Element of (Al,0)
q is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
0 + Al is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
Al is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
Al + p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
(p,Al) is Element of K19(NAT)
1 + p is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + p <= b₁ & b₁ <= Al + p ) } is set
q is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
q + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
Al is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
q is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
(q,Al) is Element of K19(NAT)
1 + q is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
Al + q is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + q <= b₁ & b₁ <= Al + q ) } is set
(q,p) is Element of K19(NAT)
p + q is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + q <= b₁ & b₁ <= p + q ) } is set
n is set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
Al is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
(Al,p) is Element of K19(NAT)
1 + Al is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
p + Al is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + Al <= b₁ & b₁ <= p + Al ) } is set
Al + p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
(Al + p) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
{((Al + p) + 1)} is non empty V12() 1 -element set
(Al,p) \/ {((Al + p) + 1)} is set
p + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
(Al,(p + 1)) is Element of K19(NAT)
(p + 1) + Al is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + Al <= b₁ & b₁ <= (p + 1) + Al ) } is set
p + 0 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
q is set
Al + (p + 1) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
q is set
n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
(p + 1) + Al is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
Al is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
(Al,p) is Element of K19(NAT)
1 + Al is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
p + Al is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + Al <= b₁ & b₁ <= p + Al ) } is set
q is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
(Al,q) is Element of K19(NAT)
q + Al is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + Al <= b₁ & b₁ <= q + Al ) } is set
q + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
(Al,(q + 1)) is Element of K19(NAT)
(q + 1) + Al is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + Al <= b₁ & b₁ <= (q + 1) + Al ) } is set
Al + q is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
succ q is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal set
{q} is non empty V12() 1 -element set
q \/ {q} is set
n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
{(n + 1)} is non empty V12() 1 -element set
f is set
f is set
(Al,q) \/ {(n + 1)} is set
(Al,0) is Element of K19(NAT)
0 + Al is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + Al <= b₁ & b₁ <= 0 + Al ) } is set
Al is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
(Al,p) is Element of K19(NAT)
1 + Al is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
p + Al is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + Al <= b₁ & b₁ <= p + Al ) } is set
Al is Relation-like non empty QC-alphabet
CQC-WFF Al is non empty Element of K19((QC-WFF Al))
QC-WFF Al is non empty set
K19((QC-WFF Al)) is set
p is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
len p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
Al is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
(Al,p) is finite Element of K19(NAT)
1 + Al is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
p + Al is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + Al <= b₁ & b₁ <= p + Al ) } is set
Al + p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
Seg (Al + p) is finite Al + p -element Element of K19(NAT)
q is set
n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
p + Al is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
Al is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
Seg Al is finite Al -element Element of K19(NAT)
p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
(Al,p) is finite Element of K19(NAT)
1 + Al is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
p + Al is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + Al <= b₁ & b₁ <= p + Al ) } is set
q is set
n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
Al + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
Al is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
p is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Al ^ p is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom (Al ^ p) is Element of K19(NAT)
dom Al is Element of K19(NAT)
len Al is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
len p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
((len Al),(len p)) is finite Element of K19(NAT)
1 + (len Al) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
(len p) + (len Al) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + (len Al) <= b₁ & b₁ <= (len p) + (len Al) ) } is set
(dom Al) \/ ((len Al),(len p)) is Element of K19(NAT)
q is set
n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
len (Al ^ p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
(len Al) + (len p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
(len Al) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
q is set
n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
(len p) + (len Al) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
Al is Relation-like non empty QC-alphabet
CQC-WFF Al is non empty Element of K19((QC-WFF Al))
QC-WFF Al is non empty set
K19((QC-WFF Al)) is set
p is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
len p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
q is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
len q is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
((len p),(len q)) is finite Element of K19(NAT)
1 + (len p) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
(len q) + (len p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + (len p) <= b₁ & b₁ <= (len q) + (len p) ) } is set
Sgm ((len p),(len q)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
len (Sgm ((len p),(len q))) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
card ((len p),(len q)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of omega
card (len q) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of omega
(len p) + (len q) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
Seg ((len p) + (len q)) is finite (len p) + (len q) -element Element of K19(NAT)
Al is Relation-like non empty QC-alphabet
CQC-WFF Al is non empty Element of K19((QC-WFF Al))
QC-WFF Al is non empty set
K19((QC-WFF Al)) is set
p is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
len p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
q is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
len q is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
((len p),(len q)) is finite Element of K19(NAT)
1 + (len p) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
(len q) + (len p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + (len p) <= b₁ & b₁ <= (len q) + (len p) ) } is set
Sgm ((len p),(len q)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
dom (Sgm ((len p),(len q))) is Element of K19(NAT)
dom q is Element of K19(NAT)
len (Sgm ((len p),(len q))) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
Al is Relation-like non empty QC-alphabet
CQC-WFF Al is non empty Element of K19((QC-WFF Al))
QC-WFF Al is non empty set
K19((QC-WFF Al)) is set
p is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
len p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
q is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
len q is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
((len p),(len q)) is finite Element of K19(NAT)
1 + (len p) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
(len q) + (len p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + (len p) <= b₁ & b₁ <= (len q) + (len p) ) } is set
Sgm ((len p),(len q)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
rng (Sgm ((len p),(len q))) is Element of K19(NAT)
(len p) + (len q) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
Seg ((len p) + (len q)) is finite (len p) + (len q) -element Element of K19(NAT)
Al is Relation-like non empty QC-alphabet
CQC-WFF Al is non empty Element of K19((QC-WFF Al))
QC-WFF Al is non empty set
K19((QC-WFF Al)) is set
p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
q is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
len q is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
(len q) + p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
n is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
len n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
((len q),(len n)) is finite Element of K19(NAT)
1 + (len q) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
(len n) + (len q) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + (len q) <= b₁ & b₁ <= (len n) + (len q) ) } is set
Sgm ((len q),(len n)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
dom (Sgm ((len q),(len n))) is Element of K19(NAT)
(Sgm ((len q),(len n))) . p is set
dom n is Element of K19(NAT)
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
f + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
(Sgm ((len q),(len n))) . g is set
(len q) + g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
rng (Sgm ((len q),(len n))) is Element of K19(NAT)
(len q) + (f + 1) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
h is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
(Sgm ((len q),(len n))) . f is set
(len q) + f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
(len q) + (len n) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
Seg ((len q) + (len n)) is finite (len q) + (len n) -element Element of K19(NAT)
len (Sgm ((len q),(len n))) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
((len q) + f) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
F is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
(1 + (len q)) + f is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
(len n) + (len q) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
F is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
(Sgm ((len q),(len n))) . F is set
(len q) + F is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
(Sgm ((len q),(len n))) . f is set
(len q) + f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
Al is Relation-like non empty QC-alphabet
CQC-WFF Al is non empty Element of K19((QC-WFF Al))
QC-WFF Al is non empty set
K19((QC-WFF Al)) is set
p is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
len p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
q is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
len q is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
((len p),(len q)) is finite Element of K19(NAT)
1 + (len p) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
(len q) + (len p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + (len p) <= b₁ & b₁ <= (len q) + (len p) ) } is set
p ^ q is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
dom (p ^ q) is Element of K19(NAT)
n is set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
(len q) + (len p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
len (p ^ q) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
Al is Relation-like non empty QC-alphabet
CQC-WFF Al is non empty Element of K19((QC-WFF Al))
QC-WFF Al is non empty set
K19((QC-WFF Al)) is set
p is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
len p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
q is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
p ^ q is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
len q is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
((len p),(len q)) is finite Element of K19(NAT)
1 + (len p) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
(len q) + (len p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + (len p) <= b₁ & b₁ <= (len q) + (len p) ) } is set
(p ^ q) | ((len p),(len q)) is Relation-like NAT -defined CQC-WFF Al -valued Function-like FinSubsequence-like Element of K19(K20(NAT,(CQC-WFF Al)))
K20(NAT,(CQC-WFF Al)) is non finite set
K19(K20(NAT,(CQC-WFF Al))) is non finite set
dom ((p ^ q) | ((len p),(len q))) is Element of K19(NAT)
dom (p ^ q) is Element of K19(NAT)
(dom (p ^ q)) /\ ((len p),(len q)) is Element of K19(NAT)
Al is Relation-like non empty QC-alphabet
CQC-WFF Al is non empty Element of K19((QC-WFF Al))
QC-WFF Al is non empty set
K19((QC-WFF Al)) is set
p is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
len p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
q is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
p ^ q is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
len q is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
((len p),(len q)) is finite Element of K19(NAT)
1 + (len p) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
(len q) + (len p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + (len p) <= b₁ & b₁ <= (len q) + (len p) ) } is set
(p ^ q) | ((len p),(len q)) is Relation-like NAT -defined CQC-WFF Al -valued Function-like FinSubsequence-like Element of K19(K20(NAT,(CQC-WFF Al)))
K20(NAT,(CQC-WFF Al)) is non finite set
K19(K20(NAT,(CQC-WFF Al))) is non finite set
Seq ((p ^ q) | ((len p),(len q))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Sgm ((len p),(len q)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(Sgm ((len p),(len q))) * (p ^ q) is Relation-like NAT -defined CQC-WFF Al -valued Function-like Element of K19(K20(NAT,(CQC-WFF Al)))
n is Relation-like NAT -defined Function-like FinSubsequence-like set
Seq n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom n is Element of K19(NAT)
Sgm (dom n) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(Sgm (dom n)) * n is Relation-like Function-like set
(Sgm ((len p),(len q))) * n is Relation-like Function-like set
rng (Sgm ((len p),(len q))) is Element of K19(NAT)
(p ^ q) | (rng (Sgm ((len p),(len q)))) is Relation-like NAT -defined CQC-WFF Al -valued Function-like FinSubsequence-like Element of K19(K20(NAT,(CQC-WFF Al)))
(Sgm ((len p),(len q))) * ((p ^ q) | (rng (Sgm ((len p),(len q))))) is Relation-like Function-like set
(Sgm ((len p),(len q))) * (p ^ q) is Relation-like Function-like set
Al is Relation-like non empty QC-alphabet
CQC-WFF Al is non empty Element of K19((QC-WFF Al))
QC-WFF Al is non empty set
K19((QC-WFF Al)) is set
p is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
len p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
q is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
p ^ q is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
len q is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
((len p),(len q)) is finite Element of K19(NAT)
1 + (len p) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
(len q) + (len p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + (len p) <= b₁ & b₁ <= (len q) + (len p) ) } is set
(p ^ q) | ((len p),(len q)) is Relation-like NAT -defined CQC-WFF Al -valued Function-like FinSubsequence-like Element of K19(K20(NAT,(CQC-WFF Al)))
K20(NAT,(CQC-WFF Al)) is non finite set
K19(K20(NAT,(CQC-WFF Al))) is non finite set
Seq ((p ^ q) | ((len p),(len q))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom (Seq ((p ^ q) | ((len p),(len q)))) is Element of K19(NAT)
dom q is Element of K19(NAT)
Sgm ((len p),(len q)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
rng (Sgm ((len p),(len q))) is Element of K19(NAT)
dom (p ^ q) is Element of K19(NAT)
(Sgm ((len p),(len q))) * (p ^ q) is Relation-like NAT -defined CQC-WFF Al -valued Function-like Element of K19(K20(NAT,(CQC-WFF Al)))
dom ((Sgm ((len p),(len q))) * (p ^ q)) is Element of K19(NAT)
dom (Sgm ((len p),(len q))) is Element of K19(NAT)
Al is Relation-like non empty QC-alphabet
CQC-WFF Al is non empty Element of K19((QC-WFF Al))
QC-WFF Al is non empty set
K19((QC-WFF Al)) is set
p is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
q is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
q ^ p is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
len q is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
len p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
((len q),(len p)) is finite Element of K19(NAT)
1 + (len q) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
(len p) + (len q) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT : ( 1 + (len q) <= b₁ & b₁ <= (len p) + (len q) ) } is set
(q ^ p) | ((len q),(len p)) is Relation-like NAT -defined CQC-WFF Al -valued Function-like FinSubsequence-like Element of K19(K20(NAT,(CQC-WFF Al)))
K20(NAT,(CQC-WFF Al)) is non finite set
K19(K20(NAT,(CQC-WFF Al))) is non finite set
Seq ((q ^ p) | ((len q),(len p))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom (Seq ((q ^ p) | ((len q),(len p)))) is Element of K19(NAT)
n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
(Seq ((q ^ p) | ((len q),(len p)))) . n is set
p . n is set
dom p is Element of K19(NAT)
Sgm ((len q),(len p)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
dom (Sgm ((len q),(len p))) is Element of K19(NAT)
(Sgm ((len q),(len p))) * (q ^ p) is Relation-like NAT -defined CQC-WFF Al -valued Function-like Element of K19(K20(NAT,(CQC-WFF Al)))
((Sgm ((len q),(len p))) * (q ^ p)) . n is set
(Sgm ((len q),(len p))) . n is set
(q ^ p) . ((Sgm ((len q),(len p))) . n) is set
(len q) + n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
(q ^ p) . ((len q) + n) is set
dom p is Element of K19(NAT)
Al is non empty set
p is Relation-like NAT -defined Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Al
dom p is Element of K19(NAT)
K20((dom p),(dom p)) is set
K19(K20((dom p),(dom p))) is set
q is Relation-like dom p -defined dom p -valued Function-like one-to-one V14( dom p) quasi_total onto bijective Element of K19(K20((dom p),(dom p)))
q * p is Relation-like dom p -defined Al -valued Function-like Element of K19(K20((dom p),Al))
K20((dom p),Al) is set
K19(K20((dom p),Al)) is set
rng q is Element of K19((dom p))
K19((dom p)) is set
dom (q * p) is Element of K19((dom p))
dom q is Element of K19((dom p))
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
Seg f is finite f -element Element of K19(NAT)
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng n is set
rng p is Element of K19(Al)
K19(Al) is set
Al is Relation-like non empty QC-alphabet
CQC-WFF Al is non empty Element of K19((QC-WFF Al))
QC-WFF Al is non empty set
K19((QC-WFF Al)) is set
p is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
dom p is Element of K19(NAT)
K20((dom p),(dom p)) is set
K19(K20((dom p),(dom p))) is set
q is Relation-like dom p -defined dom p -valued Function-like one-to-one V14( dom p) quasi_total onto bijective Element of K19(K20((dom p),(dom p)))
((CQC-WFF Al),p,q) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
q * p is Relation-like dom p -defined CQC-WFF Al -valued Function-like Element of K19(K20((dom p),(CQC-WFF Al)))
K20((dom p),(CQC-WFF Al)) is set
K19(K20((dom p),(CQC-WFF Al))) is set
dom ((CQC-WFF Al),p,q) is Element of K19(NAT)
rng q is Element of K19((dom p))
K19((dom p)) is set
dom (q * p) is Element of K19((dom p))
dom q is Element of K19((dom p))
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K19((QC-WFF Al))
K19((QC-WFF Al)) is set
p is Element of CQC-WFF Al
<*p*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
q is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
q ^ <*p*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
n is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
n ^ q is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(n ^ q) ^ <*p*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Suc (q ^ <*p*>) is Element of CQC-WFF Al
Suc ((n ^ q) ^ <*p*>) is Element of CQC-WFF Al
Ant (q ^ <*p*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Ant ((n ^ q) ^ <*p*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Al is Relation-like non empty QC-alphabet
CQC-WFF Al is non empty Element of K19((QC-WFF Al))
QC-WFF Al is non empty set
K19((QC-WFF Al)) is set
p is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
len p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
p . 1 is set
VERUM Al is Element of CQC-WFF Al
dom p is Element of K19(NAT)
q is Element of CQC-WFF Al
q is Element of CQC-WFF Al
n is Element of CQC-WFF Al
f is Element of CQC-WFF Al
g is Element of CQC-WFF Al
Al is Relation-like non empty QC-alphabet
CQC-WFF Al is non empty Element of K19((QC-WFF Al))
QC-WFF Al is non empty set
K19((QC-WFF Al)) is set
p is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
len p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
(Al,p) is Element of CQC-WFF Al
q is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
q + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
p . (q + 1) is set
dom p is Element of K19(NAT)
f is Element of CQC-WFF Al
n is Element of CQC-WFF Al
n => f is Element of CQC-WFF Al
q is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
len q is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
q . 1 is set
dom q is Element of K19(NAT)
q . (len p) is set
n is Element of CQC-WFF Al
q is Element of CQC-WFF Al
n is Element of CQC-WFF Al
f is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
f . (len p) is set
len f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
f . 1 is set
f is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
f . (len p) is set
len f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
f . 1 is set
g is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
g . (len p) is set
len g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
g . 1 is set
g is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
g . (len p) is set
len g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
g . 1 is set
h is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
p1 is Element of CQC-WFF Al
h + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
p . (h + 1) is set
p1 is Element of CQC-WFF Al
F is Element of CQC-WFF Al
H is Element of CQC-WFF Al
p1 => p1 is Element of CQC-WFF Al
pk is Element of CQC-WFF Al
p1 is Element of CQC-WFF Al
p1 is Element of CQC-WFF Al
pk => p1 is Element of CQC-WFF Al
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K19((QC-WFF Al))
K19((QC-WFF Al)) is set
p is Element of CQC-WFF Al
<*p*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
q is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
q ^ <*p*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(q ^ <*p*>) ^ <*p*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
len (q ^ <*p*>) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
dom (q ^ <*p*>) is Element of K19(NAT)
len q is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
len <*p*> is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
(len q) + (len <*p*>) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
(len q) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
(q ^ <*p*>) . ((len q) + 1) is set
Suc ((q ^ <*p*>) ^ <*p*>) is Element of CQC-WFF Al
Ant ((q ^ <*p*>) ^ <*p*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K19((QC-WFF Al))
K19((QC-WFF Al)) is set
p is Element of CQC-WFF Al
<*p*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
q is Element of CQC-WFF Al
p '&' q is Element of CQC-WFF Al
<*(p '&' q)*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
n is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
n ^ <*(p '&' q)*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
n ^ <*p*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Suc (n ^ <*(p '&' q)*>) is Element of CQC-WFF Al
Ant (n ^ <*(p '&' q)*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(Ant (n ^ <*(p '&' q)*>)) ^ <*p*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K19((QC-WFF Al))
K19((QC-WFF Al)) is set
p is Element of CQC-WFF Al
q is Element of CQC-WFF Al
p '&' q is Element of CQC-WFF Al
<*(p '&' q)*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
<*q*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
n is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
n ^ <*(p '&' q)*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
n ^ <*q*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Suc (n ^ <*(p '&' q)*>) is Element of CQC-WFF Al
Ant (n ^ <*(p '&' q)*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(Ant (n ^ <*(p '&' q)*>)) ^ <*q*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K19((QC-WFF Al))
K19((QC-WFF Al)) is set
p is Element of CQC-WFF Al
<*p*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
q is Element of CQC-WFF Al
<*q*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
n is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
n ^ <*p*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(n ^ <*p*>) ^ <*q*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
n ^ <*q*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
len (n ^ <*p*>) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
Ant (n ^ <*p*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(Ant (n ^ <*p*>)) ^ <*q*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K19((QC-WFF Al))
K19((QC-WFF Al)) is set
p is Element of CQC-WFF Al
<*p*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
'not' p is Element of CQC-WFF Al
<*('not' p)*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
q is Element of CQC-WFF Al
<*q*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
n is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
n ^ <*p*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
n ^ <*('not' p)*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
n ^ <*q*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Ant (n ^ <*p*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Suc (n ^ <*p*>) is Element of CQC-WFF Al
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K19((QC-WFF Al))
K19((QC-WFF Al)) is set
p is Element of CQC-WFF Al
<*p*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
'not' p is Element of CQC-WFF Al
<*('not' p)*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
q is Element of CQC-WFF Al
<*q*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
n is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
n ^ <*p*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(n ^ <*p*>) ^ <*q*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
n ^ <*('not' p)*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(n ^ <*('not' p)*>) ^ <*q*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
n ^ <*q*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Ant ((n ^ <*('not' p)*>) ^ <*q*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Ant ((n ^ <*p*>) ^ <*q*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Suc (Ant ((n ^ <*p*>) ^ <*q*>)) is Element of CQC-WFF Al
'not' (Suc (Ant ((n ^ <*p*>) ^ <*q*>))) is Element of CQC-WFF Al
Suc (Ant ((n ^ <*('not' p)*>) ^ <*q*>)) is Element of CQC-WFF Al
len ((n ^ <*p*>) ^ <*q*>) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
len ((n ^ <*('not' p)*>) ^ <*q*>) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
Suc ((n ^ <*p*>) ^ <*q*>) is Element of CQC-WFF Al
Suc ((n ^ <*('not' p)*>) ^ <*q*>) is Element of CQC-WFF Al
Ant (Ant ((n ^ <*p*>) ^ <*q*>)) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Ant (Ant ((n ^ <*('not' p)*>) ^ <*q*>)) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K19((QC-WFF Al))
K19((QC-WFF Al)) is set
p is Element of CQC-WFF Al
<*p*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
q is Element of CQC-WFF Al
<*q*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
p => q is Element of CQC-WFF Al
<*(p => q)*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
n is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
n ^ <*p*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(n ^ <*p*>) ^ <*q*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
n ^ <*(p => q)*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
'not' q is Element of CQC-WFF Al
p '&' ('not' q) is Element of CQC-WFF Al
<*(p '&' ('not' q))*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
n ^ <*(p '&' ('not' q))*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(n ^ <*(p '&' ('not' q))*>) ^ <*p*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
((n ^ <*(p '&' ('not' q))*>) ^ <*p*>) ^ <*q*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Ant (((n ^ <*(p '&' ('not' q))*>) ^ <*p*>) ^ <*q*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Suc ((n ^ <*p*>) ^ <*q*>) is Element of CQC-WFF Al
Suc (((n ^ <*(p '&' ('not' q))*>) ^ <*p*>) ^ <*q*>) is Element of CQC-WFF Al
Ant ((n ^ <*p*>) ^ <*q*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
len (Ant ((n ^ <*p*>) ^ <*q*>)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
(n ^ <*(p '&' ('not' q))*>) ^ <*(p '&' ('not' q))*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Ant (Ant ((n ^ <*p*>) ^ <*q*>)) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Suc (Ant ((n ^ <*p*>) ^ <*q*>)) is Element of CQC-WFF Al
(n ^ <*(p '&' ('not' q))*>) ^ <*q*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
'not' (p '&' ('not' q)) is Element of CQC-WFF Al
<*('not' (p '&' ('not' q)))*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
n ^ <*('not' (p '&' ('not' q)))*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(n ^ <*('not' (p '&' ('not' q)))*>) ^ <*('not' (p '&' ('not' q)))*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
<*('not' q)*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(n ^ <*(p '&' ('not' q))*>) ^ <*('not' q)*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(n ^ <*(p '&' ('not' q))*>) ^ <*('not' (p '&' ('not' q)))*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Al is Relation-like non empty QC-alphabet
CQC-WFF Al is non empty Element of K19((QC-WFF Al))
QC-WFF Al is non empty set
K19((QC-WFF Al)) is set
p is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
len p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
Rev p is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(Al,(Rev p)) is Element of CQC-WFF Al
<*(Al,(Rev p))*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
q is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
q ^ p is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
q ^ <*(Al,(Rev p))*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
len (Rev p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
(Al,(Rev p)) is Element of CQC-WFF Al
f is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
f . (len (Rev p)) is set
len f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
f . 1 is set
len (q ^ p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
f . g is set
<*(f . g)*> is Relation-like NAT -defined Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like set
g + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
f . (g + 1) is set
<*(f . (g + 1))*> is Relation-like NAT -defined Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like set
h is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
(g + 1) + h is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
dom f is Element of K19(NAT)
F is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
Seg F is finite F -element Element of K19(NAT)
(q ^ p) | (Seg F) is Relation-like NAT -defined CQC-WFF Al -valued Function-like FinSubsequence-like Element of K19(K20(NAT,(CQC-WFF Al)))
K20(NAT,(CQC-WFF Al)) is non finite set
K19(K20(NAT,(CQC-WFF Al))) is non finite set
p1 is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
H is Element of CQC-WFF Al
<*H*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
p1 ^ <*H*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(len (q ^ p)) + g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
(len (q ^ p)) - g is ext-real V25() V26() V33() set
((len (q ^ p)) + g) - g is ext-real V25() V26() V33() set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
q1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
g + q1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
pk is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Seg q1 is finite q1 -element Element of K19(NAT)
(q ^ p) | (Seg q1) is Relation-like NAT -defined CQC-WFF Al -valued Function-like FinSubsequence-like Element of K19(K20(NAT,(CQC-WFF Al)))
p1 is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
pk ^ <*(f . g)*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
pk is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
pk ^ <*(f . g)*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
q1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
g + q1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
Seg q1 is finite q1 -element Element of K19(NAT)
(q ^ p) | (Seg q1) is Relation-like NAT -defined CQC-WFF Al -valued Function-like FinSubsequence-like Element of K19(K20(NAT,(CQC-WFF Al)))
p1 is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
p1 is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
q1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
g + q1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
Seg q1 is finite q1 -element Element of K19(NAT)
(q ^ p) | (Seg q1) is Relation-like NAT -defined CQC-WFF Al -valued Function-like FinSubsequence-like Element of K19(K20(NAT,(CQC-WFF Al)))
q1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
g + q1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
Seg q1 is finite q1 -element Element of K19(NAT)
(q ^ p) | (Seg q1) is Relation-like NAT -defined CQC-WFF Al -valued Function-like FinSubsequence-like Element of K19(K20(NAT,(CQC-WFF Al)))
F + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
dom (q ^ p) is Element of K19(NAT)
(q ^ p) . q1 is set
<*((q ^ p) . q1)*> is Relation-like NAT -defined Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like set
p1 ^ <*((q ^ p) . q1)*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
(p1 ^ <*((q ^ p) . q1)*>) ^ <*(f . g)*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
(Rev p) . (g + 1) is set
q1 is Element of CQC-WFF Al
g1 is Element of CQC-WFF Al
q1 => g1 is Element of CQC-WFF Al
dom (Rev p) is Element of K19(NAT)
dom p is Element of K19(NAT)
(len p) - (g + 1) is ext-real V25() V26() V33() set
((len p) - (g + 1)) + 1 is ext-real V25() V26() V33() set
p . (((len p) - (g + 1)) + 1) is set
(len p) - g is ext-real V25() V26() V33() set
p . ((len p) - g) is set
- g is ext-real non positive V25() V26() V33() set
(len p) + (- g) is ext-real V25() V26() V33() set
g + (- g) is ext-real V25() V26() V33() set
g + (len p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
i is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
len q is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
(len q) + i is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
(q ^ p) . ((len q) + i) is set
(len q) + (len p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
((len q) + (len p)) - g is ext-real V25() V26() V33() set
(q ^ p) . (((len q) + (len p)) - g) is set
(q ^ p) . ((len (q ^ p)) - g) is set
g1 is Element of CQC-WFF Al
(Rev p) . 1 is set
p . (len p) is set
p1 is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
<*(f . 1)*> is Relation-like NAT -defined Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like set
p1 ^ <*(f . 1)*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
(q ^ p) . (F + 1) is set
(q ^ p) . ((len q) + (len p)) is set
Seg (F + 1) is non empty finite F + 1 -element Element of K19(NAT)
(q ^ p) | (Seg (F + 1)) is Relation-like NAT -defined CQC-WFF Al -valued Function-like FinSubsequence-like Element of K19(K20(NAT,(CQC-WFF Al)))
<*((q ^ p) . (F + 1))*> is Relation-like NAT -defined Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like set
p1 ^ <*((q ^ p) . (F + 1))*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
Seg (len (q ^ p)) is finite len (q ^ p) -element Element of K19(NAT)
(q ^ p) | (Seg (len (q ^ p))) is Relation-like NAT -defined CQC-WFF Al -valued Function-like FinSubsequence-like Element of K19(K20(NAT,(CQC-WFF Al)))
(q ^ p) | (dom (q ^ p)) is Relation-like NAT -defined CQC-WFF Al -valued Function-like FinSubsequence-like Element of K19(K20(NAT,(CQC-WFF Al)))
p1 is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
p1 is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
p1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
(g + 1) + p1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
p1 is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Seg p1 is finite p1 -element Element of K19(NAT)
(q ^ p) | (Seg p1) is Relation-like NAT -defined CQC-WFF Al -valued Function-like FinSubsequence-like Element of K19(K20(NAT,(CQC-WFF Al)))
pk is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
p1 ^ <*(f . (g + 1))*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
q1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
(g + 1) + q1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
q1 is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Seg q1 is finite q1 -element Element of K19(NAT)
(q ^ p) | (Seg q1) is Relation-like NAT -defined CQC-WFF Al -valued Function-like FinSubsequence-like Element of K19(K20(NAT,(CQC-WFF Al)))
g1 is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
q1 ^ <*(f . (g + 1))*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
f . 0 is set
<*(f . 0)*> is Relation-like NAT -defined Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like set
<*(f . (len (Rev p)))*> is Relation-like NAT -defined Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like set
g is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
g ^ <*(f . (len (Rev p)))*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
F is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
(len (Rev p)) + F is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
Seg F is finite F -element Element of K19(NAT)
(q ^ p) | (Seg F) is Relation-like NAT -defined CQC-WFF Al -valued Function-like FinSubsequence-like Element of K19(K20(NAT,(CQC-WFF Al)))
K20(NAT,(CQC-WFF Al)) is non finite set
K19(K20(NAT,(CQC-WFF Al))) is non finite set
h is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
h is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
F is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
(len (Rev p)) + F is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
Seg F is finite F -element Element of K19(NAT)
(q ^ p) | (Seg F) is Relation-like NAT -defined CQC-WFF Al -valued Function-like FinSubsequence-like Element of K19(K20(NAT,(CQC-WFF Al)))
K20(NAT,(CQC-WFF Al)) is non finite set
K19(K20(NAT,(CQC-WFF Al))) is non finite set
F is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
(len (Rev p)) + F is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
Seg F is finite F -element Element of K19(NAT)
(q ^ p) | (Seg F) is Relation-like NAT -defined CQC-WFF Al -valued Function-like FinSubsequence-like Element of K19(K20(NAT,(CQC-WFF Al)))
K20(NAT,(CQC-WFF Al)) is non finite set
K19(K20(NAT,(CQC-WFF Al))) is non finite set
F + (len (Rev p)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
(F + (len (Rev p))) - (len (Rev p)) is ext-real V25() V26() V33() set
(len (q ^ p)) - (len p) is ext-real V25() V26() V33() set
- (len (Rev p)) is ext-real non positive V25() V26() V33() set
(F + (len (Rev p))) + (- (len (Rev p))) is ext-real V25() V26() V33() set
len q is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
(len q) + (len p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
((len q) + (len p)) - (len p) is ext-real V25() V26() V33() set
dom q is Element of K19(NAT)
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K19((QC-WFF Al))
K19((QC-WFF Al)) is set
p is Element of CQC-WFF Al
<*p*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
q is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
dom q is Element of K19(NAT)
K20((dom q),(dom q)) is set
K19(K20((dom q),(dom q))) is set
q ^ <*p*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Rev (q ^ <*p*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(Al,(Rev (q ^ <*p*>))) is Element of CQC-WFF Al
<*(Al,(Rev (q ^ <*p*>)))*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
n is Relation-like dom q -defined dom q -valued Function-like one-to-one V14( dom q) quasi_total onto bijective Element of K19(K20((dom q),(dom q)))
((CQC-WFF Al),q,n) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
n * q is Relation-like dom q -defined CQC-WFF Al -valued Function-like Element of K19(K20((dom q),(CQC-WFF Al)))
K20((dom q),(CQC-WFF Al)) is set
K19(K20((dom q),(CQC-WFF Al))) is set
((CQC-WFF Al),q,n) ^ <*(Al,(Rev (q ^ <*p*>)))*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
((CQC-WFF Al),q,n) ^ <*p*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
len (q ^ <*p*>) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
len (Rev (q ^ <*p*>)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
(Al,(Rev (q ^ <*p*>))) is Element of CQC-WFF Al
h is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
h . (len (Rev (q ^ <*p*>))) is set
len h is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
h . 1 is set
Rev h is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
len (Rev h) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
H is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
(Rev h) . H is set
H + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
(Rev h) . (H + 1) is set
0 + H is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
- H is ext-real non positive V25() V26() V33() set
(len h) + (- H) is ext-real V25() V26() V33() set
(0 + H) + (- H) is ext-real V25() V26() V33() set
(len h) - H is ext-real V25() V26() V33() set
p1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
(len (q ^ <*p*>)) - p1 is ext-real V25() V26() V33() set
(len (q ^ <*p*>)) - H is ext-real V25() V26() V33() set
(len (q ^ <*p*>)) - ((len (q ^ <*p*>)) - H) is ext-real V25() V26() V33() set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
p1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
p1 is Element of CQC-WFF Al
<*p1*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
((CQC-WFF Al),q,n) ^ <*p1*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
p1 is Element of CQC-WFF Al
<*p1*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
((CQC-WFF Al),q,n) ^ <*p1*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(len h) + H is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
((len h) + H) + (- H) is ext-real V25() V26() V33() set
(Rev (q ^ <*p*>)) . (p1 + 1) is set
h . p1 is set
h . (p1 + 1) is set
pk is Element of CQC-WFF Al
p1 is Element of CQC-WFF Al
pk => p1 is Element of CQC-WFF Al
dom (Rev h) is Element of K19(NAT)
(len h) - (H + 1) is ext-real V25() V26() V33() set
((len h) - (H + 1)) + 1 is ext-real V25() V26() V33() set
dom h is Element of K19(NAT)
q1 is Element of CQC-WFF Al
(len (q ^ <*p*>)) + p1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
- p1 is ext-real non positive V25() V26() V33() set
((len (q ^ <*p*>)) + p1) + (- p1) is ext-real V25() V26() V33() set
(len (q ^ <*p*>)) + (- p1) is ext-real V25() V26() V33() set
len q is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
len <*p*> is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
(len q) + (len <*p*>) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
p1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
(len q) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
(q ^ <*p*>) . p1 is set
(q ^ <*p*>) | (dom q) is Relation-like NAT -defined CQC-WFF Al -valued Function-like FinSubsequence-like Element of K19(K20(NAT,(CQC-WFF Al)))
K20(NAT,(CQC-WFF Al)) is non finite set
K19(K20(NAT,(CQC-WFF Al))) is non finite set
((q ^ <*p*>) | (dom q)) . p1 is set
rng n is Element of K19((dom q))
K19((dom q)) is set
dom n is Element of K19((dom q))
g1 is set
n . g1 is set
<*pk*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
((CQC-WFF Al),q,n) ^ <*pk*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
dom (Rev (q ^ <*p*>)) is Element of K19(NAT)
dom (q ^ <*p*>) is Element of K19(NAT)
(len (q ^ <*p*>)) - (p1 + 1) is ext-real V25() V26() V33() set
((len (q ^ <*p*>)) - (p1 + 1)) + 1 is ext-real V25() V26() V33() set
(q ^ <*p*>) . (((len (q ^ <*p*>)) - (p1 + 1)) + 1) is set
(q ^ <*p*>) . ((len (q ^ <*p*>)) - p1) is set
q1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
n . q1 is set
q . (n . q1) is set
(n * q) . q1 is set
Suc (((CQC-WFF Al),q,n) ^ <*pk*>) is Element of CQC-WFF Al
((CQC-WFF Al),q,n) . q1 is set
Ant (((CQC-WFF Al),q,n) ^ <*pk*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(Ant (((CQC-WFF Al),q,n) ^ <*pk*>)) . q1 is set
dom ((CQC-WFF Al),q,n) is Element of K19(NAT)
dom (Ant (((CQC-WFF Al),q,n) ^ <*pk*>)) is Element of K19(NAT)
pk => q1 is Element of CQC-WFF Al
<*q1*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
((CQC-WFF Al),q,n) ^ <*q1*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(Rev h) . 1 is set
p1 is Element of CQC-WFF Al
p1 is Element of CQC-WFF Al
(len h) - 1 is ext-real V25() V26() V33() set
((len h) - 1) + 1 is ext-real V25() V26() V33() set
h . (((len h) - 1) + 1) is set
p1 is Element of CQC-WFF Al
<*p1*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
((CQC-WFF Al),q,n) ^ <*p1*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
pk is Element of CQC-WFF Al
<*pk*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
((CQC-WFF Al),q,n) ^ <*pk*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(Rev h) . 0 is set
(Rev h) . (len (Rev h)) is set
H is Element of CQC-WFF Al
<*H*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
((CQC-WFF Al),q,n) ^ <*H*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(Rev h) . (len h) is set
(Rev (q ^ <*p*>)) . 1 is set
(q ^ <*p*>) . (len (q ^ <*p*>)) is set
len q is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
len <*p*> is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
(len q) + (len <*p*>) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
(q ^ <*p*>) . ((len q) + (len <*p*>)) is set
(len q) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
(q ^ <*p*>) . ((len q) + 1) is set
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K19((QC-WFF Al))
K19((QC-WFF Al)) is set
p is Element of CQC-WFF Al
<*p*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
q is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
dom q is Element of K19(NAT)
K20((dom q),(dom q)) is set
K19(K20((dom q),(dom q))) is set
q ^ <*p*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
n is Relation-like dom q -defined dom q -valued Function-like one-to-one V14( dom q) quasi_total onto bijective Element of K19(K20((dom q),(dom q)))
((CQC-WFF Al),q,n) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
n * q is Relation-like dom q -defined CQC-WFF Al -valued Function-like Element of K19(K20((dom q),(CQC-WFF Al)))
K20((dom q),(CQC-WFF Al)) is set
K19(K20((dom q),(CQC-WFF Al))) is set
((CQC-WFF Al),q,n) ^ <*p*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
((CQC-WFF Al),q,n) ^ q is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(((CQC-WFF Al),q,n) ^ q) ^ <*p*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
((CQC-WFF Al),q,n) ^ (q ^ <*p*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
len (q ^ <*p*>) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
Rev (q ^ <*p*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(Al,(Rev (q ^ <*p*>))) is Element of CQC-WFF Al
<*(Al,(Rev (q ^ <*p*>)))*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
((CQC-WFF Al),q,n) ^ <*(Al,(Rev (q ^ <*p*>)))*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Al is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
p is set
Al |-> p is Relation-like NAT -defined Function-like finite Al -element FinSequence-like FinSubsequence-like set
Seg Al is finite Al -element Element of K19(NAT)
K179((Seg Al),p) is Relation-like Seg Al -defined {p} -valued Function-like V14( Seg Al) quasi_total finite FinSequence-like FinSubsequence-like Element of K19(K20((Seg Al),{p}))
{p} is non empty V12() 1 -element set
K20((Seg Al),{p}) is set
K19(K20((Seg Al),{p})) is set
rng (Al |-> p) is set
<*p*> is Relation-like NAT -defined Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like set
rng <*p*> is V12() set
(Al |-> p) . Al is set
q is set
dom (Al |-> p) is Al -element Element of K19(NAT)
n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
(Al |-> p) . n is set
len (Al |-> p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
Seg (len (Al |-> p)) is finite len (Al |-> p) -element Element of K19(NAT)
q is set
len (Al |-> p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
dom (Al |-> p) is Al -element Element of K19(NAT)
Al is non empty set
p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
q is Element of Al
p |-> q is Relation-like NAT -defined Function-like finite p -element FinSequence-like FinSubsequence-like set
Seg p is finite p -element Element of K19(NAT)
K179((Seg p),q) is Relation-like Seg p -defined {q} -valued Function-like V14( Seg p) quasi_total finite FinSequence-like FinSubsequence-like Element of K19(K20((Seg p),{q}))
{q} is non empty V12() 1 -element set
K20((Seg p),{q}) is set
K19(K20((Seg p),{q})) is set
n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
dom (p |-> q) is p -element Element of K19(NAT)
len (p |-> q) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
Seg (len (p |-> q)) is finite len (p |-> q) -element Element of K19(NAT)
(p |-> q) . n is set
Al is Relation-like non empty QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K19((QC-WFF Al))
K19((QC-WFF Al)) is set
p is Element of CQC-WFF Al
<*p*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
q is Element of CQC-WFF Al
<*q*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
((CQC-WFF Al),n,p) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite n -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Seg n is finite n -element Element of K19(NAT)
K179((Seg n),p) is Relation-like Seg n -defined {p} -valued Function-like V14( Seg n) quasi_total finite FinSequence-like FinSubsequence-like Element of K19(K20((Seg n),{p}))
{p} is non empty V12() 1 -element set
K20((Seg n),{p}) is set
K19(K20((Seg n),{p})) is set
f is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
f ^ ((CQC-WFF Al),n,p) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(f ^ ((CQC-WFF Al),n,p)) ^ <*q*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
f ^ <*p*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(f ^ <*p*>) ^ <*q*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Rev ((f ^ ((CQC-WFF Al),n,p)) ^ <*q*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
len ((f ^ ((CQC-WFF Al),n,p)) ^ <*q*>) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
len (Rev ((f ^ ((CQC-WFF Al),n,p)) ^ <*q*>)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
(Al,(Rev ((f ^ ((CQC-WFF Al),n,p)) ^ <*q*>))) is Element of CQC-WFF Al
(Al,(Rev ((f ^ ((CQC-WFF Al),n,p)) ^ <*q*>))) is Element of CQC-WFF Al
F is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
F . (len (Rev ((f ^ ((CQC-WFF Al),n,p)) ^ <*q*>))) is set
len F is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
F . 1 is set
Rev F is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
len (Rev F) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
(f ^ <*p*>) ^ (f ^ ((CQC-WFF Al),n,p)) is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
((f ^ <*p*>) ^ (f ^ ((CQC-WFF Al),n,p))) ^ <*q*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(f ^ <*p*>) ^ ((f ^ ((CQC-WFF Al),n,p)) ^ <*q*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
<*(Al,(Rev ((f ^ ((CQC-WFF Al),n,p)) ^ <*q*>)))*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(f ^ <*p*>) ^ <*(Al,(Rev ((f ^ ((CQC-WFF Al),n,p)) ^ <*q*>)))*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
p1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
(Rev F) . p1 is set
p1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
(Rev F) . (p1 + 1) is set
0 + p1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
- p1 is ext-real non positive V25() V26() V33() set
(len F) + (- p1) is ext-real V25() V26() V33() set
(0 + p1) + (- p1) is ext-real V25() V26() V33() set
(len F) - p1 is ext-real V25() V26() V33() set
p1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
(len ((f ^ ((CQC-WFF Al),n,p)) ^ <*q*>)) - p1 is ext-real V25() V26() V33() set
(len ((f ^ ((CQC-WFF Al),n,p)) ^ <*q*>)) - p1 is ext-real V25() V26() V33() set
(len ((f ^ ((CQC-WFF Al),n,p)) ^ <*q*>)) - ((len ((f ^ ((CQC-WFF Al),n,p)) ^ <*q*>)) - p1) is ext-real V25() V26() V33() set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
p1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
pk is Element of CQC-WFF Al
<*pk*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(f ^ <*p*>) ^ <*pk*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
pk is Element of CQC-WFF Al
<*pk*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(f ^ <*p*>) ^ <*pk*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(len F) + p1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
((len F) + p1) + (- p1) is ext-real V25() V26() V33() set
(Rev ((f ^ ((CQC-WFF Al),n,p)) ^ <*q*>)) . (p1 + 1) is set
F . p1 is set
F . (p1 + 1) is set
p1 is Element of CQC-WFF Al
q1 is Element of CQC-WFF Al
p1 => q1 is Element of CQC-WFF Al
<*p1*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(f ^ <*p*>) ^ <*p1*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
Suc ((f ^ <*p*>) ^ <*p1*>) is Element of CQC-WFF Al
(len ((f ^ ((CQC-WFF Al),n,p)) ^ <*q*>)) + p1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
- p1 is ext-real non positive V25() V26() V33() set
((len ((f ^ ((CQC-WFF Al),n,p)) ^ <*q*>)) + p1) + (- p1) is ext-real V25() V26() V33() set
(len ((f ^ ((CQC-WFF Al),n,p)) ^ <*q*>)) + (- p1) is ext-real V25() V26() V33() set
len (f ^ ((CQC-WFF Al),n,p)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
len <*q*> is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
(len (f ^ ((CQC-WFF Al),n,p))) + (len <*q*>) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
p1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
(len (f ^ ((CQC-WFF Al),n,p))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
dom (f ^ ((CQC-WFF Al),n,p)) is Element of K19(NAT)
((f ^ ((CQC-WFF Al),n,p)) ^ <*q*>) . p1 is set
((f ^ ((CQC-WFF Al),n,p)) ^ <*q*>) | (dom (f ^ ((CQC-WFF Al),n,p))) is Relation-like NAT -defined CQC-WFF Al -valued Function-like FinSubsequence-like Element of K19(K20(NAT,(CQC-WFF Al)))
K20(NAT,(CQC-WFF Al)) is non finite set
K19(K20(NAT,(CQC-WFF Al))) is non finite set
(((f ^ ((CQC-WFF Al),n,p)) ^ <*q*>) | (dom (f ^ ((CQC-WFF Al),n,p)))) . p1 is set
(f ^ ((CQC-WFF Al),n,p)) . p1 is set
rng (f ^ ((CQC-WFF Al),n,p)) is Element of K19((CQC-WFF Al))
K19((CQC-WFF Al)) is set
rng f is Element of K19((CQC-WFF Al))
rng ((CQC-WFF Al),n,p) is Element of K19((CQC-WFF Al))
(rng f) \/ (rng ((CQC-WFF Al),n,p)) is Element of K19((CQC-WFF Al))
rng <*p*> is V12() Element of K19((CQC-WFF Al))
(rng f) \/ (rng <*p*>) is Element of K19((CQC-WFF Al))
rng (f ^ <*p*>) is Element of K19((CQC-WFF Al))
Ant ((f ^ <*p*>) ^ <*p1*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
rng (Ant ((f ^ <*p*>) ^ <*p1*>)) is Element of K19((CQC-WFF Al))
dom (Rev ((f ^ ((CQC-WFF Al),n,p)) ^ <*q*>)) is Element of K19(NAT)
dom ((f ^ ((CQC-WFF Al),n,p)) ^ <*q*>) is Element of K19(NAT)
(len ((f ^ ((CQC-WFF Al),n,p)) ^ <*q*>)) - (p1 + 1) is ext-real V25() V26() V33() set
((len ((f ^ ((CQC-WFF Al),n,p)) ^ <*q*>)) - (p1 + 1)) + 1 is ext-real V25() V26() V33() set
((f ^ ((CQC-WFF Al),n,p)) ^ <*q*>) . (((len ((f ^ ((CQC-WFF Al),n,p)) ^ <*q*>)) - (p1 + 1)) + 1) is set
((f ^ ((CQC-WFF Al),n,p)) ^ <*q*>) . ((len ((f ^ ((CQC-WFF Al),n,p)) ^ <*q*>)) - p1) is set
dom (Ant ((f ^ <*p*>) ^ <*p1*>)) is Element of K19(NAT)
q1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal set
(Ant ((f ^ <*p*>) ^ <*p1*>)) . q1 is set
dom (Rev F) is Element of K19(NAT)
(len F) - (p1 + 1) is ext-real V25() V26() V33() set
((len F) - (p1 + 1)) + 1 is ext-real V25() V26() V33() set
dom F is Element of K19(NAT)
q1 is Element of CQC-WFF Al
p1 => q1 is Element of CQC-WFF Al
<*q1*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(f ^ <*p*>) ^ <*q1*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(Rev F) . 1 is set
p1 is Element of CQC-WFF Al
p1 is Element of CQC-WFF Al
(len F) - 1 is ext-real V25() V26() V33() set
((len F) - 1) + 1 is ext-real V25() V26() V33() set
F . (((len F) - 1) + 1) is set
p1 is Element of CQC-WFF Al
<*p1*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(f ^ <*p*>) ^ <*p1*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
p1 is Element of CQC-WFF Al
<*p1*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(f ^ <*p*>) ^ <*p1*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(Rev F) . 0 is set
(Rev F) . (len (Rev F)) is set
p1 is Element of CQC-WFF Al
<*p1*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(f ^ <*p*>) ^ <*p1*> is Relation-like NAT -defined CQC-WFF Al -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of CQC-WFF Al
(Rev F) . (len F) is set
(Rev ((f ^ ((CQC-WFF Al),n,p)) ^ <*q*>)) . 1 is set
((f ^ ((CQC-WFF Al),n,p)) ^ <*q*>) . (len ((f ^ ((CQC-WFF Al),n,p)) ^ <*q*>)) is set
len (f ^ ((CQC-WFF Al),n,p)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V25() V26() V33() finite cardinal Element of NAT
len <*q*> is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
(len (f ^ ((CQC-WFF Al),n,p))) + (len <*q*>) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
((f ^ ((CQC-WFF Al),n,p)) ^ <*q*>) . ((len (f ^ ((CQC-WFF Al),n,p))) + (len <*q*>)) is set
(len (f ^ ((CQC-WFF Al),n,p))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V25() V26() V33() finite cardinal Element of NAT
((f ^ ((CQC-WFF Al),n,p)) ^ <*q*>) . ((len (f ^ ((CQC-WFF Al),n,p))) + 1) is set