:: INTPRO_1 semantic presentation

REAL is set
NAT is non empty V4() V5() V6() Element of K6(REAL)
K6(REAL) is non empty set
NAT is non empty V4() V5() V6() set
K6(NAT) is non empty set
K6(NAT) is non empty set
1 is non empty V4() V5() V6() V10() Element of NAT
2 is non empty V4() V5() V6() V10() Element of NAT
3 is non empty V4() V5() V6() V10() Element of NAT
{} is set
0 is V4() V5() V6() V10() Element of NAT

5 is non empty V4() V5() V6() V10() Element of NAT
6 is non empty V4() V5() V6() V10() Element of NAT

T is set
T is set
K6(()) is non empty set

T is set
a is set
a is non empty set
q is set

T is set

q is V4() V5() V6() V10() Element of NAT
2 * q is V4() V5() V6() V10() Element of NAT
5 + (2 * q) is V4() V5() V6() V10() Element of NAT
<*(5 + (2 * q))*> is non empty V15() V18( NAT ) V19( NAT ) Function-like V32() V39(1) FinSequence-like FinSubsequence-like FinSequence of NAT

S is set

(<*3*> ^ q) ^ r is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
T is set

(<*2*> ^ q) ^ r is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
T is set

(<*1*> ^ q) ^ r is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
T is set

q is set
r is set
T is set
a is set
() is set
T is V15() Function-like Element of ()

(<*1*> ^ T) ^ a is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set

(<*2*> ^ T) ^ a is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set

(<*3*> ^ T) ^ a is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set

K6(()) is non empty set
T is functional Element of K6(())
a is set
q is set
q is functional Element of K6(())

T is functional Element of K6(())

a is functional Element of K6(())
q is functional Element of K6(())
r is set

S is functional Element of K6(())

S is functional Element of K6(())
{} () is empty proper V4() V5() V6() V8() V9() V10() Function-like functional FinSequence-membered Element of K6(())
(({} ())) is functional Element of K6(())
() is functional Element of K6(())

(T,()) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ T) ^ () is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((),()) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ ()) ^ () is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set

T is functional Element of K6(())
(T) is functional Element of K6(())

(q,a) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ q) ^ a is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(a,(q,a)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ a) ^ (q,a) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
r is functional Element of K6(())
T is functional Element of K6(())
(T) is functional Element of K6(())

(a,q) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ a) ^ q is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set

(q,r) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ q) ^ r is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(a,(q,r)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ a) ^ (q,r) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(a,r) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ a) ^ r is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((a,q),(a,r)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (a,q) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (a,q)) ^ (a,r) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((a,(q,r)),((a,q),(a,r))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (a,(q,r)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (a,(q,r))) ^ ((a,q),(a,r)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
T is functional Element of K6(())
T is functional Element of K6(())
(T) is functional Element of K6(())

(a,q) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*2*> ^ a) ^ q is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((a,q),a) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (a,q) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (a,q)) ^ a is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
r is functional Element of K6(())
T is functional Element of K6(())
(T) is functional Element of K6(())

(a,q) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*2*> ^ a) ^ q is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((a,q),q) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (a,q) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (a,q)) ^ q is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
r is functional Element of K6(())
T is functional Element of K6(())
(T) is functional Element of K6(())

(a,q) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*2*> ^ a) ^ q is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(q,(a,q)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ q) ^ (a,q) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(a,(q,(a,q))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ a) ^ (q,(a,q)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
r is functional Element of K6(())
T is functional Element of K6(())
(T) is functional Element of K6(())

(a,q) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*3*> ^ a) ^ q is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(a,(a,q)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ a) ^ (a,q) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
r is functional Element of K6(())
T is functional Element of K6(())
(T) is functional Element of K6(())

(q,a) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*3*> ^ q) ^ a is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(a,(q,a)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ a) ^ (q,a) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
r is functional Element of K6(())
T is functional Element of K6(())
(T) is functional Element of K6(())

(a,q) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ a) ^ q is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set

(r,q) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ r) ^ q is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(a,r) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*3*> ^ a) ^ r is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((a,r),q) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (a,r) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (a,r)) ^ q is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((r,q),((a,r),q)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (r,q) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (r,q)) ^ ((a,r),q) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((a,q),((r,q),((a,r),q))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (a,q) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (a,q)) ^ ((r,q),((a,r),q)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
T is functional Element of K6(())
T is functional Element of K6(())
(T) is functional Element of K6(())

((),a) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ ()) ^ a is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
q is functional Element of K6(())
T is functional Element of K6(())
(T) is functional Element of K6(())

(a,q) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ a) ^ q is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
r is functional Element of K6(())
T is functional Element of K6(())
a is functional Element of K6(())
(a) is functional Element of K6(())
q is set
T is functional Element of K6(())
(T) is functional Element of K6(())
a is set

r is functional Element of K6(())
T is functional Element of K6(())
(T) is functional Element of K6(())
a is functional Element of K6(())
(a) is functional Element of K6(())
q is set

T is functional Element of K6(())
T is functional Element of K6(())
(T) is functional Element of K6(())
((T)) is functional Element of K6(())
a is set

r is functional Element of K6(())
T is functional Element of K6(())
(T) is functional Element of K6(())
((T)) is functional Element of K6(())
T is functional Element of K6(())
(T) is functional Element of K6(())

((),a) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ ()) ^ a is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set

(q,a) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ q) ^ a is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(a,(q,a)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ a) ^ (q,a) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(a,q) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ a) ^ q is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(a,q) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*2*> ^ a) ^ q is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((a,q),a) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (a,q) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (a,q)) ^ a is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((a,q),q) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ (a,q)) ^ q is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(q,(a,q)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ q) ^ (a,q) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(a,(q,(a,q))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ a) ^ (q,(a,q)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(a,q) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*3*> ^ a) ^ q is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(a,(a,q)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ a) ^ (a,q) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(q,(a,q)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ q) ^ (a,q) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set

(q,r) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ q) ^ r is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(a,(q,r)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ a) ^ (q,r) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(a,r) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ a) ^ r is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((a,q),(a,r)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (a,q) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (a,q)) ^ (a,r) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((a,(q,r)),((a,q),(a,r))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (a,(q,r)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (a,(q,r))) ^ ((a,q),(a,r)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((a,q),r) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (a,q) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (a,q)) ^ r is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((q,r),((a,q),r)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (q,r) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (q,r)) ^ ((a,q),r) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((a,r),((q,r),((a,q),r))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (a,r) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (a,r)) ^ ((q,r),((a,q),r)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
T is functional Element of K6(())
(T) is functional Element of K6(())
T is functional Element of K6(())
(T) is functional () Element of K6(())
a is set
T is functional Element of K6(())
(T) is functional () Element of K6(())

(T,T) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ T) ^ T is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(T,(T,T)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ T) ^ (T,T) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((T,T),T) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (T,T) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (T,T)) ^ T is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(T,((T,T),T)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ T) ^ ((T,T),T) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((T,(T,T)),(T,T)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (T,(T,T)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (T,(T,T))) ^ (T,T) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((T,((T,T),T)),((T,(T,T)),(T,T))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (T,((T,T),T)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (T,((T,T),T))) ^ ((T,(T,T)),(T,T)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set

(a,T) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ a) ^ T is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(T,(a,T)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ T) ^ (a,T) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set

(T,a) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ T) ^ a is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(T,T) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ T) ^ T is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((T,a),(T,T)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (T,a) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (T,a)) ^ (T,T) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set

(T,a) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ T) ^ a is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(a,a) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ a) ^ a is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((T,a),(a,a)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (T,a) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (T,a)) ^ (a,a) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set

(T,a) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ T) ^ a is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set

(q,T) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ q) ^ T is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(q,a) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ q) ^ a is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((q,T),(q,a)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (q,T) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (q,T)) ^ (q,a) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((T,a),((q,T),(q,a))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (T,a) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (T,a)) ^ ((q,T),(q,a)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(q,(T,a)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ q) ^ (T,a) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((q,(T,a)),((q,T),(q,a))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (q,(T,a)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (q,(T,a))) ^ ((q,T),(q,a)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((T,a),((q,(T,a)),((q,T),(q,a)))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ (T,a)) ^ ((q,(T,a)),((q,T),(q,a))) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((T,a),(q,(T,a))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ (T,a)) ^ (q,(T,a)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(((T,a),(q,(T,a))),((T,a),((q,T),(q,a)))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ ((T,a),(q,(T,a))) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ ((T,a),(q,(T,a)))) ^ ((T,a),((q,T),(q,a))) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(((T,a),((q,(T,a)),((q,T),(q,a)))),(((T,a),(q,(T,a))),((T,a),((q,T),(q,a))))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ ((T,a),((q,(T,a)),((q,T),(q,a)))) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ ((T,a),((q,(T,a)),((q,T),(q,a))))) ^ (((T,a),(q,(T,a))),((T,a),((q,T),(q,a)))) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(((q,(T,a)),((q,T),(q,a))),((T,a),((q,(T,a)),((q,T),(q,a))))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ ((q,(T,a)),((q,T),(q,a))) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ ((q,(T,a)),((q,T),(q,a)))) ^ ((T,a),((q,(T,a)),((q,T),(q,a)))) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set

(a,q) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ a) ^ q is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(T,(a,q)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ T) ^ (a,q) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(T,q) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ T) ^ q is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(a,(T,q)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ a) ^ (T,q) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(T,a) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ T) ^ a is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((T,a),(T,q)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (T,a) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (T,a)) ^ (T,q) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(a,(T,a)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ a) ^ (T,a) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((a,(T,a)),(a,(T,q))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (a,(T,a)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (a,(T,a))) ^ (a,(T,q)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(((T,a),(T,q)),((a,(T,a)),(a,(T,q)))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ ((T,a),(T,q)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ ((T,a),(T,q))) ^ ((a,(T,a)),(a,(T,q))) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((T,(a,q)),((T,a),(T,q))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (T,(a,q)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (T,(a,q))) ^ ((T,a),(T,q)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set

(T,a) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ T) ^ a is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set

(a,q) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ a) ^ q is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(T,q) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ T) ^ q is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((a,q),(T,q)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (a,q) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (a,q)) ^ (T,q) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((T,a),((a,q),(T,q))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (T,a) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (T,a)) ^ ((a,q),(T,q)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((T,a),(T,q)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ (T,a)) ^ (T,q) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((a,q),((T,a),(T,q))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ (a,q)) ^ ((T,a),(T,q)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set

(T,a) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ T) ^ a is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set

(a,q) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ a) ^ q is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(T,q) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ T) ^ q is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((a,q),(T,q)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (a,q) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (a,q)) ^ (T,q) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((T,a),((a,q),(T,q))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (T,a) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (T,a)) ^ ((a,q),(T,q)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set

(T,a) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ T) ^ a is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set

(a,q) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ a) ^ q is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(T,q) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ T) ^ q is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((a,q),(T,q)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (a,q) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (a,q)) ^ (T,q) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((T,a),((a,q),(T,q))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (T,a) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (T,a)) ^ ((a,q),(T,q)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set

(T,a) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ T) ^ a is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set

(q,a) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ q) ^ a is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((T,a),(q,a)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (T,a) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (T,a)) ^ (q,a) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(q,T) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ q) ^ T is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set

(((T,a),(q,a)),r) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ ((T,a),(q,a)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ ((T,a),(q,a))) ^ r is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((q,T),r) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (q,T) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (q,T)) ^ r is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((((T,a),(q,a)),r),((q,T),r)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (((T,a),(q,a)),r) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (((T,a),(q,a)),r)) ^ ((q,T),r) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((q,T),((T,a),(q,a))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ (q,T)) ^ ((T,a),(q,a)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set

(a,q) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ a) ^ q is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(T,(a,q)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ T) ^ (a,q) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set

(r,a) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ r) ^ a is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(r,q) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ r) ^ q is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(T,(r,q)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ T) ^ (r,q) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((r,a),(T,(r,q))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (r,a) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (r,a)) ^ (T,(r,q)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((T,(a,q)),((r,a),(T,(r,q)))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (T,(a,q)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (T,(a,q))) ^ ((r,a),(T,(r,q))) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((a,q),(r,q)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (a,q) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (a,q)) ^ (r,q) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(((a,q),(r,q)),(T,(r,q))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ ((a,q),(r,q)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ ((a,q),(r,q))) ^ (T,(r,q)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((((a,q),(r,q)),(T,(r,q))),((r,a),(T,(r,q)))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (((a,q),(r,q)),(T,(r,q))) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (((a,q),(r,q)),(T,(r,q)))) ^ ((r,a),(T,(r,q))) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(((((a,q),(r,q)),(T,(r,q))),((r,a),(T,(r,q)))),((T,(a,q)),((r,a),(T,(r,q))))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ ((((a,q),(r,q)),(T,(r,q))),((r,a),(T,(r,q)))) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ ((((a,q),(r,q)),(T,(r,q))),((r,a),(T,(r,q))))) ^ ((T,(a,q)),((r,a),(T,(r,q)))) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set

(T,a) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ T) ^ a is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set

((T,a),q) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (T,a) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (T,a)) ^ q is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(a,q) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ a) ^ q is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(((T,a),q),(a,q)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ ((T,a),q) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ ((T,a),q)) ^ (a,q) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(a,(T,a)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ a) ^ (T,a) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((a,(T,a)),(((T,a),q),(a,q))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (a,(T,a)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (a,(T,a))) ^ (((T,a),q),(a,q)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set

(a,q) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ a) ^ q is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(T,(a,q)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ T) ^ (a,q) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(T,q) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ T) ^ q is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(a,(T,q)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ a) ^ (T,q) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((T,(a,q)),(a,(T,q))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (T,(a,q)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (T,(a,q))) ^ (a,(T,q)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(T,a) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ T) ^ a is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(a,(T,a)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ a) ^ (T,a) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((T,a),(T,q)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (T,a) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (T,a)) ^ (T,q) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((T,(a,q)),((T,a),(T,q))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ (T,(a,q))) ^ ((T,a),(T,q)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((T,(a,q)),(T,q)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ (T,(a,q))) ^ (T,q) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((T,a),((T,(a,q)),(T,q))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ (T,a)) ^ ((T,(a,q)),(T,q)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(a,((T,(a,q)),(T,q))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ a) ^ ((T,(a,q)),(T,q)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((a,(T,a)),(a,((T,(a,q)),(T,q)))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (a,(T,a)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (a,(T,a))) ^ (a,((T,(a,q)),(T,q))) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(((T,a),((T,(a,q)),(T,q))),((a,(T,a)),(a,((T,(a,q)),(T,q))))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ ((T,a),((T,(a,q)),(T,q))) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ ((T,a),((T,(a,q)),(T,q)))) ^ ((a,(T,a)),(a,((T,(a,q)),(T,q)))) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set

(T,a) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ T) ^ a is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(T,(T,a)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ T) ^ (T,a) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((T,(T,a)),(T,a)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (T,(T,a)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (T,(T,a))) ^ (T,a) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(T,T) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ T) ^ T is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((T,T),(T,a)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (T,T) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (T,T)) ^ (T,a) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((T,(T,a)),((T,T),(T,a))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ (T,(T,a))) ^ ((T,T),(T,a)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((T,T),((T,(T,a)),(T,a))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ (T,T)) ^ ((T,(T,a)),(T,a)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set

(T,a) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ T) ^ a is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((T,a),a) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (T,a) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (T,a)) ^ a is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(T,((T,a),a)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ T) ^ ((T,a),a) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((T,a),(T,a)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ (T,a)) ^ (T,a) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(((T,a),(T,a)),(T,((T,a),a))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ ((T,a),(T,a)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ ((T,a),(T,a))) ^ (T,((T,a),a)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set

(a,q) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ a) ^ q is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(T,(a,q)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ T) ^ (a,q) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(T,q) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ T) ^ q is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(a,(T,q)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ a) ^ (T,q) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((T,(a,q)),(a,(T,q))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (T,(a,q)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (T,(a,q))) ^ (a,(T,q)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set

(T,T) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*2*> ^ T) ^ T is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(T,(T,T)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ T) ^ (T,T) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(T,(T,(T,T))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ T) ^ (T,(T,T)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((T,(T,(T,T))),(T,(T,T))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (T,(T,(T,T))) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (T,(T,(T,T)))) ^ (T,(T,T)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set

(T,a) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*2*> ^ T) ^ a is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((T,a),a) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (T,a) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (T,a)) ^ a is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((T,a),T) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ (T,a)) ^ T is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(a,(T,a)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ a) ^ (T,a) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(T,(a,(T,a))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ T) ^ (a,(T,a)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set

(T,a) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*2*> ^ T) ^ a is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(a,T) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*2*> ^ a) ^ T is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set

(T,a) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*2*> ^ T) ^ a is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set

((T,a),q) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (T,a) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (T,a)) ^ q is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(a,q) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ a) ^ q is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(T,(a,q)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ T) ^ (a,q) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(((T,a),q),(T,(a,q))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ ((T,a),q) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ ((T,a),q)) ^ (T,(a,q)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(a,(T,a)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ a) ^ (T,a) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(((T,a),q),(a,q)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ ((T,a),q)) ^ (a,q) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((a,(T,a)),(((T,a),q),(a,q))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (a,(T,a)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (a,(T,a))) ^ (((T,a),q),(a,q)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(T,((a,(T,a)),(((T,a),q),(a,q)))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ T) ^ ((a,(T,a)),(((T,a),q),(a,q))) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(T,(a,(T,a))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ T) ^ (a,(T,a)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(T,(((T,a),q),(a,q))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ T) ^ (((T,a),q),(a,q)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((T,(a,(T,a))),(T,(((T,a),q),(a,q)))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (T,(a,(T,a))) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (T,(a,(T,a)))) ^ (T,(((T,a),q),(a,q))) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((T,((a,(T,a)),(((T,a),q),(a,q)))),((T,(a,(T,a))),(T,(((T,a),q),(a,q))))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (T,((a,(T,a)),(((T,a),q),(a,q)))) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (T,((a,(T,a)),(((T,a),q),(a,q))))) ^ ((T,(a,(T,a))),(T,(((T,a),q),(a,q)))) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((T,(((T,a),q),(a,q))),(((T,a),q),(T,(a,q)))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (T,(((T,a),q),(a,q))) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (T,(((T,a),q),(a,q)))) ^ (((T,a),q),(T,(a,q))) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set

(T,a) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*2*> ^ T) ^ a is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set

(a,q) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ a) ^ q is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(T,(a,q)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()

(<*1*> ^ T) ^ (a,q) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((T,a),q) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (T,a) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (T,a)) ^ q is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((T,(a,q)),((T,a),q)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (T,(a,q)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (T,(a,q))) ^ ((T,a),q) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((T,a),a) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ (T,a)) ^ a is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((a,q),((T,a),q)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ (a,q) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ (a,q)) ^ ((T,a),q) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(((T,a),a),((a,q),((T,a),q))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
<*1*> ^ ((T,a),a) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(<*1*> ^ ((T,a),a)) ^ ((a,q),((T,a),q)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(T,((a,q),((T,a),q))) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ T) ^ ((a,q),((T,a),q)) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(T,((T,a),q)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ T) ^ ((T,a),q) is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
(T,q) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like Element of ()
(<*1*> ^ T) ^ q is non empty V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
((T,a),(T,q)) is V15() V18( NAT ) Function-like V32() FinSequence-like FinSubsequence-like