:: MODELC_1 semantic presentation

REAL is set
NAT is non empty V24() V25() V26() V38() V43() V44() Element of bool REAL
bool REAL is non empty set
{} is Function-like functional empty V24() V25() V26() V28() V29() V30() V31() V32() ext-real non positive non negative V38() V43() V45( {} ) V51() V60() set
1 is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
{{},1} is non empty set
NAT is non empty V24() V25() V26() V38() V43() V44() set
bool NAT is non empty V38() set
bool NAT is non empty V38() set
BOOLEAN is non empty set
0 is Function-like functional empty V24() V25() V26() V28() V29() V30() V31() V32() ext-real non positive non negative V38() V43() V45( {} ) V51() V60() Element of NAT
{0,1} is non empty set
[:1,1:] is non empty set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty set
bool [:[:1,1:],1:] is non empty set
{{}} is non empty trivial V45(1) set
K192() is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() boolean V60() set
K193() is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() boolean V60() set
R is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() set
S is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() set
BASSIGN is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() set
BASSIGN + 1 is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
S + 1 is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
R is set
S is set
BASSIGN is Element of R
S is set
R is set
S is Relation-like Function-like set
dom S is set
S . R is set
BASSIGN is set
S is set
FALSE is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() boolean V60() Element of BOOLEAN
R is set
S is set
bool S is non empty set
5 is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
S is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
5 + S is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
<*(5 + S)*> is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
<*0*> is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
S is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
<*0*> ^ S is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
<*1*> is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
<*1*> ^ S is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(<*1*> ^ S) ^ R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
2 is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
<*2*> is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
S is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
<*2*> ^ S is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
3 is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
<*3*> is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
<*3*> ^ S is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
4 is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
<*4*> is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
<*4*> ^ S is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(<*4*> ^ S) ^ R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
S is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
<*S*> is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
<*S*> ^ R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
len R is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
1 + (len R) is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(<*S*> ^ R) ^ BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
len ((<*S*> ^ R) ^ BASSIGN) is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
len BASSIGN is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
(1 + (len R)) + (len BASSIGN) is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
R ^ BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
len (R ^ BASSIGN) is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
(len R) + (len BASSIGN) is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
len <*S*> is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
(len <*S*>) + (len (R ^ BASSIGN)) is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
(len <*S*>) + (len R) is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
((len <*S*>) + (len R)) + (len BASSIGN) is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
<*S*> ^ (R ^ BASSIGN) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
len (<*S*> ^ (R ^ BASSIGN)) is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
NAT * is set
S is set
(0) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
5 + 0 is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
<*(5 + 0)*> is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
BASSIGN is non empty set
BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
R is non empty set
BASSIGN is set
BASSIGN is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
(BASSIGN) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
5 + BASSIGN is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
<*(5 + BASSIGN)*> is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
f is non empty set
BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(BASSIGN) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
<*0*> ^ BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
f is non empty set
BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
f is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(BASSIGN,f) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
<*1*> ^ BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(<*1*> ^ BASSIGN) ^ f is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
g is non empty set
BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(BASSIGN) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
<*2*> ^ BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
f is non empty set
BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(BASSIGN) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
<*3*> ^ BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
f is non empty set
BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
f is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(BASSIGN,f) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
<*4*> ^ BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(<*4*> ^ BASSIGN) ^ f is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
g is non empty set
BASSIGN is non empty set
f is set
S is non empty set
R is non empty set
() is non empty set
the Element of () is Element of ()
R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
S is set
S is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
(S) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
5 + S is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
<*(5 + S)*> is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
S is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(S) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
<*0*> ^ S is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(S) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
<*2*> ^ S is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(S) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
<*3*> ^ S is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(S,R) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
<*1*> ^ S is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(<*1*> ^ S) ^ R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(S,R) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
<*4*> ^ S is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(<*4*> ^ S) ^ R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
S is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(S) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*0*> ^ S is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(R) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*0*> ^ R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
((S),(R)) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*1*> ^ (S) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(<*1*> ^ (S)) ^ (R) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(((S),(R))) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*0*> ^ ((S),(R)) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
S is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(0) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
5 + 0 is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
<*(5 + 0)*> is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
{S} is functional non empty trivial V45(1) set
R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
() \ {S} is Element of bool ()
bool () is non empty set
BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(BASSIGN) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*3*> ^ BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(R) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
<*3*> ^ R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(BASSIGN) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*2*> ^ BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(R) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
<*2*> ^ R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
f is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
g is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(f,g) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*1*> ^ f is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(<*1*> ^ f) ^ g is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(R,BASSIGN) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
<*1*> ^ R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(<*1*> ^ R) ^ BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(BASSIGN) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*0*> ^ BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(R) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
<*0*> ^ R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
f is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
g is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(f,g) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*4*> ^ f is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(<*4*> ^ f) ^ g is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(R,BASSIGN) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
<*4*> ^ R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(<*4*> ^ R) ^ BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
R is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
(R) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
5 + R is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
<*(5 + R)*> is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
R is set
S is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
S . 1 is set
R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(R) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*0*> ^ R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
S is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
S . 1 is set
R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(R,BASSIGN) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*1*> ^ R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(<*1*> ^ R) ^ BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
R ^ BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
<*1*> ^ (R ^ BASSIGN) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
S is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
S . 1 is set
R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(R) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*2*> ^ R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
S is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
S . 1 is set
R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(R) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*3*> ^ R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
S is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
S . 1 is set
R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(R,BASSIGN) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*4*> ^ R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(<*4*> ^ R) ^ BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
R ^ BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
<*4*> ^ (R ^ BASSIGN) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
S is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
S . 1 is set
R is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
(R) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
5 + R is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
<*(5 + R)*> is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
3 + R is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
2 + (3 + R) is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
2 + 0 is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
1 + R is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
4 + (1 + R) is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
4 + 0 is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
2 + R is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
3 + (2 + R) is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
3 + 0 is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
4 + R is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
1 + (4 + R) is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
1 + 0 is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
S is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
S . 1 is set
S is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
len S is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
R is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
(R) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
5 + R is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
<*(5 + R)*> is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(R) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*0*> ^ R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
len R is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
1 + (len R) is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(R,BASSIGN) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*1*> ^ R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(<*1*> ^ R) ^ BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
len R is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
1 + (len R) is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
len BASSIGN is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
(1 + (len R)) + (len BASSIGN) is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(R) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*2*> ^ R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
len R is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
1 + (len R) is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(R) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*3*> ^ R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
len R is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
1 + (len R) is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(R,BASSIGN) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*4*> ^ R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(<*4*> ^ R) ^ BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
len R is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
1 + (len R) is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
len BASSIGN is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
(1 + (len R)) + (len BASSIGN) is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
S is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
BASSIGN is Relation-like Function-like FinSequence-like set
R ^ BASSIGN is Relation-like Function-like FinSequence-like set
f is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() set
g is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
len g is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
X is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
h is Relation-like Function-like FinSequence-like set
X ^ h is Relation-like Function-like FinSequence-like set
dom X is Element of bool NAT
len X is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
Seg (len X) is Element of bool NAT
len <*0*> is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
s is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(s) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*0*> ^ s is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(X ^ h) . 1 is set
X . 1 is set
s1 is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(s1) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*0*> ^ s1 is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
len s is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
(len <*0*>) + (len s) is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
(<*0*> ^ s1) ^ h is Relation-like Function-like FinSequence-like set
s1 ^ h is Relation-like Function-like FinSequence-like set
<*0*> ^ (s1 ^ h) is Relation-like Function-like FinSequence-like set
len <*4*> is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
s is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
s1 is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(s,s1) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*4*> ^ s is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(<*4*> ^ s) ^ s1 is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
s is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
j1 is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(s,j1) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*4*> ^ s is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(<*4*> ^ s) ^ j1 is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
len s1 is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
len s is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
1 + (len s) is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
(len s1) + (1 + (len s)) is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
(len s1) + 1 is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
((len s1) + 1) + (len s) is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
len (<*4*> ^ s) is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
(len <*4*>) + (len s) is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
(len (<*4*> ^ s)) + (len s1) is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
s ^ j1 is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(s ^ j1) ^ h is Relation-like Function-like FinSequence-like set
j1 ^ h is Relation-like Function-like FinSequence-like set
s ^ (j1 ^ h) is Relation-like Function-like FinSequence-like set
k is Relation-like Function-like FinSequence-like set
s ^ k is Relation-like Function-like FinSequence-like set
(len s) + 1 is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
<*4*> ^ (s ^ j1) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(<*4*> ^ (s ^ j1)) ^ h is Relation-like Function-like FinSequence-like set
<*4*> ^ ((s ^ j1) ^ h) is Relation-like Function-like FinSequence-like set
len (<*4*> ^ s) is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
len s is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
(len <*4*>) + (len s) is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
(len s) + 1 is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
len j1 is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
((len s) + 1) + (len j1) is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
len h is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
(((len s) + 1) + (len j1)) + (len h) is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
(len j1) + (len h) is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
((len s) + 1) + ((len j1) + (len h)) is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
k is Relation-like Function-like FinSequence-like set
s ^ k is Relation-like Function-like FinSequence-like set
len (X ^ h) is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
(len X) + (len h) is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
(len (<*4*> ^ s)) + (len j1) is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
s ^ s1 is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
<*4*> ^ (s ^ s1) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
k is Relation-like Function-like FinSequence-like set
s ^ k is Relation-like Function-like FinSequence-like set
len <*1*> is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
s is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
s1 is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(s,s1) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*1*> ^ s is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(<*1*> ^ s) ^ s1 is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
s is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
j1 is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(s,j1) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*1*> ^ s is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(<*1*> ^ s) ^ j1 is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
len s1 is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
len s is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
1 + (len s) is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
(len s1) + (1 + (len s)) is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
(len s1) + 1 is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
((len s1) + 1) + (len s) is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
len (<*1*> ^ s) is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
(len <*1*>) + (len s) is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
(len (<*1*> ^ s)) + (len s1) is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
s ^ j1 is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(s ^ j1) ^ h is Relation-like Function-like FinSequence-like set
j1 ^ h is Relation-like Function-like FinSequence-like set
s ^ (j1 ^ h) is Relation-like Function-like FinSequence-like set
k is Relation-like Function-like FinSequence-like set
s ^ k is Relation-like Function-like FinSequence-like set
(len s) + 1 is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
<*1*> ^ (s ^ j1) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(<*1*> ^ (s ^ j1)) ^ h is Relation-like Function-like FinSequence-like set
<*1*> ^ ((s ^ j1) ^ h) is Relation-like Function-like FinSequence-like set
len (<*1*> ^ s) is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
len s is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
(len <*1*>) + (len s) is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
(len s) + 1 is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
len j1 is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
((len s) + 1) + (len j1) is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
(((len s) + 1) + (len j1)) + (len h) is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
(len j1) + (len h) is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
((len s) + 1) + ((len j1) + (len h)) is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
k is Relation-like Function-like FinSequence-like set
s ^ k is Relation-like Function-like FinSequence-like set
(len (<*1*> ^ s)) + (len j1) is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
s ^ s1 is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
<*1*> ^ (s ^ s1) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
k is Relation-like Function-like FinSequence-like set
s ^ k is Relation-like Function-like FinSequence-like set
len <*3*> is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
s is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(s) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*3*> ^ s is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
s1 is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(s1) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*3*> ^ s1 is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
len s is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
(len <*3*>) + (len s) is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
(<*3*> ^ s1) ^ h is Relation-like Function-like FinSequence-like set
s1 ^ h is Relation-like Function-like FinSequence-like set
<*3*> ^ (s1 ^ h) is Relation-like Function-like FinSequence-like set
len <*2*> is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
s is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(s) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*2*> ^ s is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
s1 is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(s1) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*2*> ^ s1 is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
len s is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
(len <*2*>) + (len s) is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
(<*2*> ^ s1) ^ h is Relation-like Function-like FinSequence-like set
s1 ^ h is Relation-like Function-like FinSequence-like set
<*2*> ^ (s1 ^ h) is Relation-like Function-like FinSequence-like set
s is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
(s) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
5 + s is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
<*(5 + s)*> is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
1 + (len h) is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
1 + 0 is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
f is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() set
g is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
len g is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
X is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
h is Relation-like Function-like FinSequence-like set
X ^ h is Relation-like Function-like FinSequence-like set
len S is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
S is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(S,R) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*1*> ^ S is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(<*1*> ^ S) ^ R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
f is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(BASSIGN,f) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*1*> ^ BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(<*1*> ^ BASSIGN) ^ f is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
BASSIGN ^ f is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
<*1*> ^ (BASSIGN ^ f) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
S ^ R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
<*1*> ^ (S ^ R) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
len BASSIGN is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
len S is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
g is Relation-like Function-like FinSequence-like set
S ^ g is Relation-like Function-like FinSequence-like set
X is Relation-like Function-like FinSequence-like set
BASSIGN ^ X is Relation-like Function-like FinSequence-like set
g is Relation-like Function-like FinSequence-like set
S ^ g is Relation-like Function-like FinSequence-like set
g is Relation-like Function-like FinSequence-like set
BASSIGN ^ g is Relation-like Function-like FinSequence-like set
X is Relation-like Function-like FinSequence-like set
S ^ X is Relation-like Function-like FinSequence-like set
S is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(S,R) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*4*> ^ S is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(<*4*> ^ S) ^ R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
f is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(BASSIGN,f) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*4*> ^ BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(<*4*> ^ BASSIGN) ^ f is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
BASSIGN ^ f is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
<*4*> ^ (BASSIGN ^ f) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
S ^ R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
<*4*> ^ (S ^ R) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
len BASSIGN is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
len S is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
g is Relation-like Function-like FinSequence-like set
S ^ g is Relation-like Function-like FinSequence-like set
X is Relation-like Function-like FinSequence-like set
BASSIGN ^ X is Relation-like Function-like FinSequence-like set
g is Relation-like Function-like FinSequence-like set
S ^ g is Relation-like Function-like FinSequence-like set
g is Relation-like Function-like FinSequence-like set
BASSIGN ^ g is Relation-like Function-like FinSequence-like set
X is Relation-like Function-like FinSequence-like set
S ^ X is Relation-like Function-like FinSequence-like set
S is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
S . 1 is set
S is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
S . 1 is set
S is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
S . 1 is set
S is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
S . 1 is set
S is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
S . 1 is set
S is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(R) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*0*> ^ R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(BASSIGN) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*0*> ^ BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
f is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(f) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*2*> ^ f is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
g is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(g) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*2*> ^ g is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
X is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(X) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*3*> ^ X is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
h is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(h) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*3*> ^ h is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(R) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*0*> ^ R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(R) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*2*> ^ R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
S is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
f is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(R,f) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*1*> ^ R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(<*1*> ^ R) ^ f is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
g is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(BASSIGN,g) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*1*> ^ BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(<*1*> ^ BASSIGN) ^ g is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
X is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
s is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(X,s) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*4*> ^ X is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(<*4*> ^ X) ^ s is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
h is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
s1 is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(h,s1) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*4*> ^ h is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(<*4*> ^ h) ^ s1 is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(R,BASSIGN) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*1*> ^ R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(<*1*> ^ R) ^ BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(R,BASSIGN) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*4*> ^ R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(<*4*> ^ R) ^ BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
f is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(f,R) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*1*> ^ f is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(<*1*> ^ f) ^ R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
g is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(g,BASSIGN) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*1*> ^ g is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(<*1*> ^ g) ^ BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
s is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
X is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(s,X) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*4*> ^ s is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(<*4*> ^ s) ^ X is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
s1 is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
h is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(s1,h) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*4*> ^ s1 is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(<*4*> ^ s1) ^ h is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
S is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(S) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
((S)) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*3*> ^ (S) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
S is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(S) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(S) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
((S),(S)) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*1*> ^ (S) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(<*1*> ^ (S)) ^ (S) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(R,(S)) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*1*> ^ R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(<*1*> ^ R) ^ (S) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
S is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(S) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(S) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
((S),(S)) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*4*> ^ (S) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(<*4*> ^ (S)) ^ (S) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
S . 1 is set
R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
(R,(S)) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*4*> ^ R is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(<*4*> ^ R) ^ (S) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
S is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
len S is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
(S) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
len (S) is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
((S)) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*0*> ^ (S) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
1 + (len (S)) is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
((S)) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*2*> ^ (S) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
1 + (len (S)) is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
((S)) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*3*> ^ (S) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
1 + (len (S)) is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
S is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
len S is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
(S) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
len (S) is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
(S) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
len (S) is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
(len (S)) + 1 is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
((S),(S)) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*1*> ^ (S) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(<*1*> ^ (S)) ^ (S) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
1 + (len (S)) is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
(1 + (len (S))) + (len (S)) is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
(len (S)) + ((len (S)) + 1) is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
((S),(S)) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
<*4*> ^ (S) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
(<*4*> ^ (S)) ^ (S) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
1 + (len (S)) is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
(1 + (len (S))) + (len (S)) is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
(len (S)) + ((len (S)) + 1) is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
S is set
(0) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
5 + 0 is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
<*(5 + 0)*> is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT : b₁ is () } is set
bool () is non empty set
R is set
BASSIGN is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
() is Element of bool ()
S is ()
the of S is Element of bool the carrier of S
the carrier of S is set
bool the carrier of S is non empty set
[:(), the of S:] is set
bool [:(), the of S:] is non empty set
[:(), the carrier of S:] is set
bool [:(), the carrier of S:] is non empty set
S is ()
the of S is Element of bool the carrier of S
the carrier of S is set
bool the carrier of S is non empty set
[:(), the of S:] is set
bool [:(), the of S:] is non empty set
[:(), the carrier of S:] is set
bool [:(), the carrier of S:] is non empty set
S is ()
the of S is Element of bool the carrier of S
the carrier of S is set
bool the carrier of S is non empty set
[:(), the of S:] is set
bool [:(), the of S:] is non empty set
[:(), the carrier of S:] is set
bool [:(), the carrier of S:] is non empty set
X is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
len X is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
g is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
g + 1 is non empty V24() V25() V26() V30() V31() V32() ext-real positive non negative V38() V43() V60() Element of NAT
BASSIGN is Relation-like () -defined the carrier of S -valued Function-like quasi_total Element of bool [:(), the carrier of S:]
BASSIGN . X is set
R is Relation-like () -defined the of S -valued Function-like quasi_total Element of bool [:(), the of S:]
R . X is set
the Compl of S is Relation-like the carrier of S -defined the carrier of S -valued Function-like quasi_total Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is set
bool [: the carrier of S, the carrier of S:] is non empty set
f is Relation-like () -defined the carrier of S -valued Function-like quasi_total Element of bool [:(), the carrier of S:]
(X) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
f . (X) is set
the Compl of S . (f . (X)) is set
the L_meet of S is Relation-like [: the carrier of S, the carrier of S:] -defined the carrier of S -valued Function-like quasi_total Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]
[:[: the carrier of S, the carrier of S:], the carrier of S:] is set
bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
(X) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
f . (X) is set
(X) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
f . (X) is set
the L_meet of S . ((f . (X)),(f . (X))) is set
[(f . (X)),(f . (X))] is set
{(f . (X)),(f . (X))} is non empty set
{(f . (X))} is non empty trivial V45(1) set
{{(f . (X)),(f . (X))},{(f . (X))}} is non empty set
the L_meet of S . [(f . (X)),(f . (X))] is set
the of S is Relation-like the carrier of S -defined the carrier of S -valued Function-like quasi_total Element of bool [: the carrier of S, the carrier of S:]
the of S . (f . (X)) is set
the of S is Relation-like the carrier of S -defined the carrier of S -valued Function-like quasi_total Element of bool [: the carrier of S, the carrier of S:]
the of S . (f . (X)) is set
the of S is Relation-like [: the carrier of S, the carrier of S:] -defined the carrier of S -valued Function-like quasi_total Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]
the of S . ((f . (X)),(f . (X))) is set
the of S . [(f . (X)),(f . (X))] is set
f . X is set
h is set
s is set
s1 is set
s is set
j1 is set
k is set
k is set
pai1 is set
k0 is set
k0 is set
pai01 is set
x1 is set
pai02 is set
x2 is set
c₂₁ is set
c₂₂ is set
c₂₃ is set
c₂₄ is set
c₂₅ is set
c₂₆ is set
c₂₇ is set
c₂₈ is set
c₂₉ is set
c₃₀ is set
c₃₁ is set
c₃₂ is set
c₃₃ is set
c₃₄ is set
[#] 1 is non empty non proper Element of bool 1
bool 1 is non empty set
op2 is Relation-like [:1,1:] -defined 1 -valued Function-like quasi_total Element of bool [:[:1,1:],1:]
op1 is Relation-like 1 -defined 1 -valued Function-like quasi_total Element of bool [:1,1:]
(1,([#] 1),op2,op1,op1,op1,op2) is () ()
() is ()
the of () is Element of bool the carrier of ()
the carrier of () is set
bool the carrier of () is non empty set
S is non empty () ()
the of S is Element of bool the carrier of S
the carrier of S is non empty set
bool the carrier of S is non empty set
S is non empty () ()
the of S is non empty Element of bool the carrier of S
the carrier of S is non empty set
bool the carrier of S is non empty set
[:(), the of S:] is set
bool [:(), the of S:] is non empty set
[:(), the carrier of S:] is non empty set
bool [:(), the carrier of S:] is non empty set
R is Relation-like () -defined the of S -valued Function-like quasi_total Element of bool [:(), the of S:]
BASSIGN is Relation-like () -defined the carrier of S -valued Function-like quasi_total Element of bool [:(), the carrier of S:]
the Compl of S is Relation-like the carrier of S -defined the carrier of S -valued Function-like quasi_total Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
bool [: the carrier of S, the carrier of S:] is non empty set
the L_meet of S is Relation-like [: the carrier of S, the carrier of S:] -defined the carrier of S -valued Function-like quasi_total Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]
[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
the of S is Relation-like the carrier of S -defined the carrier of S -valued Function-like quasi_total Element of bool [: the carrier of S, the carrier of S:]
the of S is Relation-like the carrier of S -defined the carrier of S -valued Function-like quasi_total Element of bool [: the carrier of S, the carrier of S:]
the of S is Relation-like [: the carrier of S, the carrier of S:] -defined the carrier of S -valued Function-like quasi_total Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]
f is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
len f is V24() V25() V26() V30() V31() V32() ext-real non negative V38() V43() V60() Element of NAT
BASSIGN . f is set
R . f is set
(f) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
BASSIGN . (f) is set
the Compl of S . (BASSIGN . (f)) is set
(f) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
BASSIGN . (f) is set
(f) is Relation-like NAT -defined NAT -valued Function-like FinSequence-like () FinSequence of NAT
BASSIGN . (f) is set
the L_meet of S . ((BASSIGN . (f)),(BASSIGN . (f))) is set
[(BASSIGN . (f)),(BASSIGN . (f))] is set
{(BASSIGN . (f)),(BASSIGN . (f))} is non empty set
{(BASSIGN . (f))} is non empty trivial V45(1) set