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

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

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

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

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

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

(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

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

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

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

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

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

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

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

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

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

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

(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

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

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

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

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

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

(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

(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

(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

(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