:: SCMFSA_M semantic presentation

REAL is non empty non trivial non finite V68() V108() V109() V110() V114() V147() V148() V150() set
NAT is V6() V7() V8() non empty non trivial non finite cardinal limit_cardinal V68() V108() V109() V110() V111() V112() V113() V114() V145() V147() Element of bool REAL
bool REAL is non empty non trivial non finite V68() V121() V123() V124() set
SCM+FSA is non empty with_non-empty_values IC-Ins-separated strict V94(3) V139(3) AMI-Struct over 3
3 is V6() V7() V8() V12() non empty ext-real positive non negative V27() V28() integer finite cardinal V67() V97() V108() V109() V110() V111() V112() V113() V145() V146() V147() V148() V149() Element of NAT
K526() is set
K503(NAT,K526()) is Element of K526()
K519() is non empty set
K529() is Relation-like K526() -defined 3 -valued Function-like V43(K526(),3) Element of bool [:K526(),3:]
[:K526(),3:] is Relation-like set
bool [:K526(),3:] is V121() V123() V124() set

K537() is Relation-like K519() -defined K177((product (K529() * K530())),(product (K529() * K530()))) -valued Function-like V43(K519(),K177((product (K529() * K530())),(product (K529() * K530())))) Element of bool [:K519(),K177((product (K529() * K530())),(product (K529() * K530()))):]

product (K529() * K530()) is set
K177((product (K529() * K530())),(product (K529() * K530()))) is set
[:K519(),K177((product (K529() * K530())),(product (K529() * K530()))):] is Relation-like set
bool [:K519(),K177((product (K529() * K530())),(product (K529() * K530()))):] is V121() V123() V124() set
AMI-Struct(# K526(),K503(NAT,K526()),K519(),K529(),K530(),K537() #) is strict AMI-Struct over 3
the carrier of SCM+FSA is non empty set
COMPLEX is non empty non trivial non finite V68() V108() V114() set
NAT is V6() V7() V8() non empty non trivial non finite cardinal limit_cardinal V68() V108() V109() V110() V111() V112() V113() V114() V145() V147() set
bool NAT is non empty non trivial non finite V68() V121() V123() V124() set
bool NAT is non empty non trivial non finite V68() V121() V123() V124() set
9 is V6() V7() V8() V12() non empty ext-real positive non negative V27() V28() integer finite cardinal V67() V97() V108() V109() V110() V111() V112() V113() V145() V146() V147() V148() V149() Element of NAT
Segm 9 is V108() V109() V110() V111() V112() V113() V147() Element of bool NAT
Int-Locations is non empty set

bool SCM-Memory is V121() V123() V124() set
2 is V6() V7() V8() V12() non empty ext-real positive non negative V27() V28() integer finite cardinal V67() V97() V108() V109() V110() V111() V112() V113() V145() V146() V147() V148() V149() Element of NAT

bool is V121() V123() V124() set

product () is set
K210() is Relation-like non empty V75() V76() V77() V79() set
K177((),()) is set
[:K210(),K177((),()):] is Relation-like set
bool [:K210(),K177((),()):] is V121() V123() V124() set
bool the carrier of SCM+FSA is V121() V123() V124() set
the U5 of SCM+FSA is Relation-like non empty V75() V76() V77() V79() set
INT is non empty non trivial non finite V68() V108() V109() V110() V111() V112() V114() set
RAT is non empty non trivial non finite V68() V108() V109() V110() V111() V114() set

the U5 of SCM is Relation-like non empty V75() V76() V77() V79() set
the carrier of SCM is non empty set

the Object-Kind of SCM is Relation-like the carrier of SCM -defined 2 -valued Function-like V43( the carrier of SCM,2) Element of bool [: the carrier of SCM,2:]
[: the carrier of SCM,2:] is Relation-like set
bool [: the carrier of SCM,2:] is V121() V123() V124() set

K518() is set
bool K526() is V121() V123() V124() set
is Relation-like non empty non trivial non finite V68() set
bool is non empty non trivial non finite V68() V121() V123() V124() set
is Relation-like non empty non trivial non finite V68() set
bool is non empty non trivial non finite V68() V121() V123() V124() set
1 is V6() V7() V8() V12() non empty ext-real positive non negative V27() V28() integer finite cardinal V67() V97() V108() V109() V110() V111() V112() V113() V145() V146() V147() V148() V149() Element of NAT

the Object-Kind of SCM+FSA is Relation-like the carrier of SCM+FSA -defined 3 -valued Function-like V43( the carrier of SCM+FSA,3) Element of bool [: the carrier of SCM+FSA,3:]
[: the carrier of SCM+FSA,3:] is Relation-like set
bool [: the carrier of SCM+FSA,3:] is V121() V123() V124() set

K528() is Element of bool K526()

Int-Locations is non empty Element of bool the carrier of SCM+FSA
FinSeq-Locations is non empty non trivial non finite V68() Element of bool the carrier of SCM+FSA
IC is V54( SCM+FSA ) Element of the carrier of SCM+FSA

SCM-Data-Loc is non empty Element of bool SCM-Memory
NonZero SCM is non empty non trivial non finite V68() Element of bool the carrier of SCM
bool the carrier of SCM is V121() V123() V124() set
{1} is non empty trivial finite V35() 1 -element V67() V68() V108() V109() V110() V111() V112() V113() V145() V146() V147() V148() V149() Element of bool NAT

is Relation-like non empty non trivial non finite V68() set
bool is non empty non trivial non finite V68() V121() V123() V124() set

{()} is non empty trivial finite 1 -element set

is non empty trivial functional finite V35() 1 -element V108() V109() V110() V111() V112() V113() V145() V146() V147() V148() V149() set

bool [:{()},:] is finite V35() V121() V123() V124() set
intloc 0 is Int-like Element of the carrier of SCM+FSA
dl. 0 is Int-like Element of the carrier of SCM

{()} is non empty trivial finite 1 -element set

{1} is non empty trivial finite V35() 1 -element V67() V68() V108() V109() V110() V111() V112() V113() V145() V146() V147() V148() V149() set

bool [:{()},{1}:] is finite V35() V121() V123() V124() set
s is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal set
intloc s is Int-like Element of the carrier of SCM+FSA
dl. s is Int-like Element of the carrier of SCM
f is ext-real V27() V28() integer set

{()} is non empty trivial finite 1 -element set
{()} --> f is Relation-like {()} -defined {f} -valued non empty Function-like constant finite total V43({()},{f}) Element of bool [:{()},{f}:]
{f} is non empty trivial finite 1 -element V108() V109() V110() V111() V112() V145() V146() V147() V148() V149() set

bool [:{()},{f}:] is finite V35() V121() V123() V124() set
dom (() .--> f) is trivial finite set
{()} is non empty trivial finite 1 -element Element of bool the carrier of SCM+FSA
rng (() .--> f) is trivial finite set
{f} is non empty trivial finite 1 -element V108() V109() V110() V111() V112() V145() V146() V147() V148() V149() Element of bool REAL
p is set
(() .--> f) . p is set
. p is set
q is Int-like Element of the carrier of SCM+FSA
. q is set
Values q is non empty set

dom () is non empty finite set
{()} is non empty trivial finite 1 -element Element of bool the carrier of SCM+FSA

dom (() .--> 1) is trivial finite set
{()} is non empty trivial finite 1 -element Element of bool the carrier of SCM+FSA
(u +* (Initialize (() .--> 1))) . () is set
(Initialize (u +* (() .--> 1))) . () is set
(u +* (() .--> 1)) . () is set
(() .--> 1) . () is set
() . () is set
IC f is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT
f . () is set
dom f is set
dom u is set
dom (Initialize (() .--> 1)) is finite set
(dom u) \/ (dom (Initialize (() .--> 1))) is set
(dom (() .--> 1)) \/ (dom ()) is non empty finite set

f +* (() .--> 0) is Relation-like the carrier of SCM+FSA -defined Function-like set

F3() is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT
s is set
{()} is non empty trivial finite 1 -element Element of bool the carrier of SCM+FSA
\/ {()} is non empty Element of bool the carrier of SCM+FSA
f is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT
intloc f is Int-like Element of the carrier of SCM+FSA
dl. f is Int-like Element of the carrier of SCM
u is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT

u + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V27() V28() integer finite cardinal V67() V97() V108() V109() V110() V111() V112() V113() V145() V146() V147() V148() V149() Element of NAT
K113((u + 1)) is ext-real non positive V27() V28() integer set
f is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT
intloc f is Int-like Element of the carrier of SCM+FSA
dl. f is Int-like Element of the carrier of SCM

f + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V27() V28() integer finite cardinal V67() V97() V108() V109() V110() V111() V112() V113() V145() V146() V147() V148() V149() Element of NAT
K113((f + 1)) is ext-real non positive V27() V28() integer set
u is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT
F1(f) is ext-real V27() V28() integer set
u is ext-real V27() V28() integer set

dom s is set
dom the Object-Kind of SCM+FSA is set
f is set
s . f is set
u is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT
intloc u is Int-like Element of the carrier of SCM+FSA
dl. u is Int-like Element of the carrier of SCM
F1(u) is ext-real V27() V28() integer set

u + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V27() V28() integer finite cardinal V67() V97() V108() V109() V110() V111() V112() V113() V145() V146() V147() V148() V149() Element of NAT
K113((u + 1)) is ext-real non positive V27() V28() integer set

{()} is non empty trivial finite 1 -element Element of bool the carrier of SCM+FSA
\/ {()} is non empty Element of bool the carrier of SCM+FSA
. f is set
Values () is non empty set
. () is set
. f is set
Values () is non empty set
. () is set
. f is set
Values () is non empty set
. () is set

IC f is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT
f . () is set
u is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT
intloc u is Int-like Element of the carrier of SCM+FSA
dl. u is Int-like Element of the carrier of SCM
F1(u) is ext-real V27() V28() integer set
p is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT

p + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V27() V28() integer finite cardinal V67() V97() V108() V109() V110() V111() V112() V113() V145() V146() V147() V148() V149() Element of NAT
K113((p + 1)) is ext-real non positive V27() V28() integer set

u is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT
intloc u is Int-like Element of the carrier of SCM+FSA
dl. u is Int-like Element of the carrier of SCM
f . () is ext-real V27() V28() integer set
F1(u) is ext-real V27() V28() integer set

u + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V27() V28() integer finite cardinal V67() V97() V108() V109() V110() V111() V112() V113() V145() V146() V147() V148() V149() Element of NAT
K113((u + 1)) is ext-real non positive V27() V28() integer set

p is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT
intloc p is Int-like Element of the carrier of SCM+FSA
dl. p is Int-like Element of the carrier of SCM
F1(p) is ext-real V27() V28() integer set
q is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT

q + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V27() V28() integer finite cardinal V67() V97() V108() V109() V110() V111() V112() V113() V145() V146() V147() V148() V149() Element of NAT
K113((q + 1)) is ext-real non positive V27() V28() integer set

p is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT
intloc p is Int-like Element of the carrier of SCM+FSA
dl. p is Int-like Element of the carrier of SCM
F1(p) is ext-real V27() V28() integer set
q is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT

q + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V27() V28() integer finite cardinal V67() V97() V108() V109() V110() V111() V112() V113() V145() V146() V147() V148() V149() Element of NAT
K113((q + 1)) is ext-real non positive V27() V28() integer set

dom s is set
f is set
{()} is non empty trivial finite 1 -element Element of bool the carrier of SCM+FSA
\/ {()} is non empty Element of bool the carrier of SCM+FSA

u is set
s . u is set
f . u is set
s . u is set
f . u is set
u is Int-like Element of the carrier of SCM+FSA
s . u is ext-real V27() V28() integer set
f . u is ext-real V27() V28() integer set

dom f is set
{()} is non empty trivial finite 1 -element Element of bool the carrier of SCM+FSA
\/ {()} is non empty Element of bool the carrier of SCM+FSA
dom s is set
u is Int-like Element of the carrier of SCM+FSA
s . u is ext-real V27() V28() integer set
f . u is ext-real V27() V28() integer set

q is Int-like Element of the carrier of SCM+FSA
s . q is ext-real V27() V28() integer set
f . q is ext-real V27() V28() integer set

u2 is set
s . u2 is set
f . u2 is set
{()} is non empty trivial finite 1 -element Element of bool the carrier of SCM+FSA
{()} is non empty trivial finite 1 -element Element of bool the carrier of SCM+FSA

dom (s) is set
dom s is set
(dom s) \/ {()} is non empty set
((dom s) \/ {()}) \/ {()} is non empty set
dom (() .--> 1) is trivial finite set
dom () is non empty finite set

dom (s +* (() .--> 1)) is set
(dom (s +* (() .--> 1))) \/ (dom ()) is non empty set

dom (s) is set
dom (() .--> 1) is trivial finite set
dom () is non empty finite set
dom s is set
(dom s) \/ {()} is non empty set

dom (s +* (() .--> 1)) is set
(dom (s +* (() .--> 1))) \/ (dom ()) is non empty set
((dom s) \/ {()}) \/ {()} is non empty set

(s) . () is set
(s) . () is set
dom (() .--> 1) is trivial finite set

dom () is non empty finite set
(s +* (() .--> 1)) . () is set
(() .--> 1) . () is set
() . () is set

dom s is set

dom (s) is set
f is Int-like Element of the carrier of SCM+FSA
(dom s) \/ {()} is non empty set
((dom s) \/ {()}) \/ {()} is non empty set

dom s is set

dom (s) is set

(dom s) \/ {()} is non empty set
((dom s) \/ {()}) \/ {()} is non empty set

s . () is ext-real V27() V28() integer set
IC s is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT
s . () is set

dom s is set

(s) . () is set
(() .--> 1) . () is set

dom (() .--> 1) is trivial finite set
dom () is non empty finite set
(s +* (() .--> 1)) . () is set
dom (Initialize (() .--> 1)) is finite set
dom () is non empty finite set
dom (() .--> 1) is trivial finite set
(dom ()) \/ (dom (() .--> 1)) is non empty finite set
{(),()} is non empty finite Element of bool the carrier of SCM+FSA
dom (() .--> 1) is trivial finite set
dom () is non empty finite set
(dom (() .--> 1)) \/ (dom ()) is non empty finite set
(dom (() .--> 1)) \/ {()} is non empty finite set
{()} \/ {()} is non empty finite Element of bool the carrier of SCM+FSA
(Initialize (() .--> 1)) . () is set
dom () is non empty finite set
(() .--> 1) . () is set

intloc 1 is Int-like Element of the carrier of SCM+FSA
dl. 1 is Int-like Element of the carrier of SCM
bool Int-Locations is V121() V123() V124() set

{ b1 where b1 is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT : not intloc b1 in s } is set
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT : S1[b1] } is set
is Relation-like non empty non trivial non finite V68() set
u is set
p is Int-like Element of the carrier of SCM+FSA
q is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT
intloc q is Int-like Element of the carrier of SCM+FSA
dl. q is Int-like Element of the carrier of SCM
q is non empty V108() V109() V110() V111() V112() V113() V145() V147() Element of bool NAT
min q is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT
intloc (min q) is Int-like Element of the carrier of SCM+FSA
dl. (min q) is Int-like Element of the carrier of SCM
f is Int-like Element of the carrier of SCM+FSA
p is non empty V108() V109() V110() V111() V112() V113() V145() V147() Element of bool NAT
min p is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT
intloc (min p) is Int-like Element of the carrier of SCM+FSA
dl. (min p) is Int-like Element of the carrier of SCM
u is Int-like Element of the carrier of SCM+FSA
q is non empty V108() V109() V110() V111() V112() V113() V145() V147() Element of bool NAT
min q is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT
intloc (min q) is Int-like Element of the carrier of SCM+FSA
dl. (min q) is Int-like Element of the carrier of SCM

(s) is Int-like Element of the carrier of SCM+FSA
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT : not intloc b1 in s } is set
u is non empty V108() V109() V110() V111() V112() V113() V145() V147() Element of bool NAT
min u is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT
intloc (min u) is Int-like Element of the carrier of SCM+FSA
dl. (min u) is Int-like Element of the carrier of SCM
p is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT
intloc p is Int-like Element of the carrier of SCM+FSA
dl. p is Int-like Element of the carrier of SCM
s is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT
intloc s is Int-like Element of the carrier of SCM+FSA
dl. s is Int-like Element of the carrier of SCM
f is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT
intloc f is Int-like Element of the carrier of SCM+FSA
dl. f is Int-like Element of the carrier of SCM

(u) is Int-like Element of the carrier of SCM+FSA
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT : not intloc b1 in u } is set
p is non empty V108() V109() V110() V111() V112() V113() V145() V147() Element of bool NAT
min p is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT
intloc (min p) is Int-like Element of the carrier of SCM+FSA
dl. (min p) is Int-like Element of the carrier of SCM
bool FinSeq-Locations is non empty non trivial non finite V68() V121() V123() V124() set

{ b1 where b1 is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT : not fsloc b1 in s } is set
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT : S1[b1] } is set
u is set

q is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT

q + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V27() V28() integer finite cardinal V67() V97() V108() V109() V110() V111() V112() V113() V145() V146() V147() V148() V149() Element of NAT
K113((q + 1)) is ext-real non positive V27() V28() integer set
q is non empty V108() V109() V110() V111() V112() V113() V145() V147() Element of bool NAT
min q is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT
fsloc (min q) is FinSeq-Location
(min q) + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V27() V28() integer finite cardinal V67() V97() V108() V109() V110() V111() V112() V113() V145() V146() V147() V148() V149() Element of NAT
K113(((min q) + 1)) is ext-real non positive V27() V28() integer set

p is non empty V108() V109() V110() V111() V112() V113() V145() V147() Element of bool NAT
min p is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT
fsloc (min p) is FinSeq-Location
(min p) + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V27() V28() integer finite cardinal V67() V97() V108() V109() V110() V111() V112() V113() V145() V146() V147() V148() V149() Element of NAT
K113(((min p) + 1)) is ext-real non positive V27() V28() integer set

q is non empty V108() V109() V110() V111() V112() V113() V145() V147() Element of bool NAT
min q is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT
fsloc (min q) is FinSeq-Location
(min q) + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V27() V28() integer finite cardinal V67() V97() V108() V109() V110() V111() V112() V113() V145() V146() V147() V148() V149() Element of NAT
K113(((min q) + 1)) is ext-real non positive V27() V28() integer set

(s) is FinSeq-Location
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT : not fsloc b1 in s } is set
u is non empty V108() V109() V110() V111() V112() V113() V145() V147() Element of bool NAT
min u is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT
fsloc (min u) is FinSeq-Location
(min u) + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V27() V28() integer finite cardinal V67() V97() V108() V109() V110() V111() V112() V113() V145() V146() V147() V148() V149() Element of NAT
K113(((min u) + 1)) is ext-real non positive V27() V28() integer set
p is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT

p + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V27() V28() integer finite cardinal V67() V97() V108() V109() V110() V111() V112() V113() V145() V146() V147() V148() V149() Element of NAT
K113((p + 1)) is ext-real non positive V27() V28() integer set
s is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT

s + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V27() V28() integer finite cardinal V67() V97() V108() V109() V110() V111() V112() V113() V145() V146() V147() V148() V149() Element of NAT
K113((s + 1)) is ext-real non positive V27() V28() integer set
f is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT

f + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V27() V28() integer finite cardinal V67() V97() V108() V109() V110() V111() V112() V113() V145() V146() V147() V148() V149() Element of NAT
K113((f + 1)) is ext-real non positive V27() V28() integer set

(u) is FinSeq-Location
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT : not fsloc b1 in u } is set
p is non empty V108() V109() V110() V111() V112() V113() V145() V147() Element of bool NAT
min p is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT
fsloc (min p) is FinSeq-Location
(min p) + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V27() V28() integer finite cardinal V67() V97() V108() V109() V110() V111() V112() V113() V145() V146() V147() V148() V149() Element of NAT
K113(((min p) + 1)) is ext-real non positive V27() V28() integer set

f is Int-like Element of the carrier of SCM+FSA
u is ext-real V27() V28() integer set
s +* (f,u) is Relation-like Function-like set
p is set
dom (s +* (f,u)) is set
(s +* (f,u)) . p is set
. p is set
dom s is set
Values f is non empty set
. f is set
s . p is set
s is Int-like Element of the carrier of SCM+FSA
f is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal set

{s} is non empty trivial finite 1 -element set

{f} is non empty trivial finite V35() 1 -element V108() V109() V110() V111() V112() V113() V145() V146() V147() V148() V149() set

bool [:{s},{f}:] is finite V35() V121() V123() V124() set

s . () is ext-real V27() V28() integer set

dom s is set

s . () is ext-real V27() V28() integer set

dom s is set

s . () is ext-real V27() V28() integer set

f . () is ext-real V27() V28() integer set

dom () is set
dom s is set
(dom s) /\ is Element of bool the carrier of SCM+FSA
\/ {()} is non empty Element of bool the carrier of SCM+FSA
( \/ {()}) /\ is Element of bool the carrier of SCM+FSA
dom f is set
(dom f) /\ is Element of bool the carrier of SCM+FSA
dom () is set
p is set
() . p is set
s . p is set
f . p is set
() . p is set
q is Int-like Element of the carrier of SCM+FSA
() . p is set
f . q is ext-real V27() V28() integer set
() . p is set
() . p is set
() . p is set
() . p is set
() . p is set
() . p is set
s . p is set
f . p is set
() . p is set
() . p is set
() . p is set

f is Int-like Element of the carrier of SCM+FSA
s . f is ext-real V27() V28() integer set
u is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT

{u} is non empty trivial finite V35() 1 -element V108() V109() V110() V111() V112() V113() V145() V146() V147() V148() V149() set

bool [:{()},{u}:] is finite V35() V121() V123() V124() set

(s +* (Start-At (u,SCM+FSA))) . f is ext-real V27() V28() integer set
dom (Start-At (u,SCM+FSA)) is non empty finite set
s is Int-like Element of the carrier of SCM+FSA
{s} is non empty trivial finite 1 -element set
f is Int-like Element of the carrier of SCM+FSA
{s,f} is non empty finite set
u is Int-like Element of the carrier of SCM+FSA
{s,f,u} is finite set
p is Int-like Element of the carrier of SCM+FSA
{s,f,u,p} is finite set
[:NAT,():] is Relation-like non empty non trivial non finite V68() set
bool [:NAT,():] is non empty non trivial non finite V68() V121() V123() V124() set

{ b1 where b1 is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT : ( not intloc b1 in s & not b1 = 0 ) } is set
(()) is non empty trivial finite 1 -element Element of bool Int-Locations
s \/ (()) is non empty finite Element of bool Int-Locations
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT : S1[b1] } is set
p is set
q is Int-like Element of the carrier of SCM+FSA
q is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT
intloc q is Int-like Element of the carrier of SCM+FSA
dl. q is Int-like Element of the carrier of SCM
n is V108() V109() V110() V111() V112() V113() V147() Element of bool NAT
f is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT
{} NAT is V108() V109() V110() V111() V112() V113() V147() Element of bool NAT
sn is non empty V108() V109() V110() V111() V112() V113() V145() V147() Element of bool NAT
min sn is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT
{(min sn)} is non empty trivial finite V35() 1 -element V108() V109() V110() V111() V112() V113() V145() V146() V147() V148() V149() Element of bool NAT
n \ {(min sn)} is V108() V109() V110() V111() V112() V113() V147() Element of bool NAT
n is V108() V109() V110() V111() V112() V113() V147() Element of bool NAT
sn is non empty V108() V109() V110() V111() V112() V113() V145() V147() Element of bool NAT
min sn is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT
{(min sn)} is non empty trivial finite V35() 1 -element V108() V109() V110() V111() V112() V113() V145() V146() V147() V148() V149() Element of bool NAT
sn1 is V108() V109() V110() V111() V112() V113() V147() Element of bool NAT
sn \ sn1 is V108() V109() V110() V111() V112() V113() V147() Element of bool NAT
x9 is V108() V109() V110() V111() V112() V113() V147() Element of bool NAT
N is non empty V108() V109() V110() V111() V112() V113() V145() V147() Element of bool NAT
i is V108() V109() V110() V111() V112() V113() V147() Element of bool NAT
min N is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT
{(min N)} is non empty trivial finite V35() 1 -element V108() V109() V110() V111() V112() V113() V145() V146() V147() V148() V149() Element of bool NAT
n \ {(min N)} is V108() V109() V110() V111() V112() V113() V147() Element of bool NAT
f is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT
sn1 is V108() V109() V110() V111() V112() V113() V147() Element of bool NAT
n is V108() V109() V110() V111() V112() V113() V147() Element of bool NAT
u2 is non empty V108() V109() V110() V111() V112() V113() V145() V147() Element of bool NAT

f . 0 is V108() V109() V110() V111() V112() V113() V147() Element of bool NAT
n is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT
f . n is V108() V109() V110() V111() V112() V113() V147() Element of bool NAT
sn is non empty V108() V109() V110() V111() V112() V113() V145() V147() Element of bool NAT
n + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V27() V28() integer finite cardinal V67() V97() V108() V109() V110() V111() V112() V113() V145() V146() V147() V148() V149() Element of NAT
f . (n + 1) is V108() V109() V110() V111() V112() V113() V147() Element of bool NAT
min sn is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT
{(min sn)} is non empty trivial finite V35() 1 -element V108() V109() V110() V111() V112() V113() V145() V146() V147() V148() V149() Element of bool NAT
sn \ {(min sn)} is V108() V109() V110() V111() V112() V113() V147() Element of bool NAT
{ H1(b1) where b1 is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT : b1 in u2 } is set
sn1 is set
sn is finite set
(s \/ (())) \/ sn is non empty finite set
x9 is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT
intloc x9 is Int-like Element of the carrier of SCM+FSA
dl. x9 is Int-like Element of the carrier of SCM
x9 is Int-like Element of the carrier of SCM+FSA
i is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT
intloc i is Int-like Element of the carrier of SCM+FSA
dl. i is Int-like Element of the carrier of SCM
n is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT
f . n is V108() V109() V110() V111() V112() V113() V147() Element of bool NAT
n + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V27() V28() integer finite cardinal V67() V97() V108() V109() V110() V111() V112() V113() V145() V146() V147() V148() V149() Element of NAT
f . (n + 1) is V108() V109() V110() V111() V112() V113() V147() Element of bool NAT
sn is non empty V108() V109() V110() V111() V112() V113() V145() V147() Element of bool NAT
min sn is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT
{(min sn)} is non empty trivial finite V35() 1 -element V108() V109() V110() V111() V112() V113() V145() V146() V147() V148() V149() Element of bool NAT
sn1 is finite set
sn1 \/ {(min sn)} is non empty finite set
sn \ {(min sn)} is V108() V109() V110() V111() V112() V113() V147() Element of bool NAT

f . 0 is V108() V109() V110() V111() V112() V113() V147() Element of bool NAT

u . 0 is V108() V109() V110() V111() V112() V113() V147() Element of bool NAT
dom f is V108() V109() V110() V111() V112() V113() V147() set
dom u is V108() V109() V110() V111() V112() V113() V147() set
p is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT
f . p is V108() V109() V110() V111() V112() V113() V147() Element of bool NAT
u . p is V108() V109() V110() V111() V112() V113() V147() Element of bool NAT
p + 1 is V6() V7() V8() V12() non empty ext-real positive non negative V27() V28() integer finite cardinal V67() V97() V108() V109() V110() V111() V112() V113() V145() V146() V147() V148() V149() Element of NAT
f . (p + 1) is V108() V109() V110() V111() V112() V113() V147() Element of bool NAT
u . (p + 1) is V108() V109() V110() V111() V112() V113() V147() Element of bool NAT
q is non empty V108() V109() V110() V111() V112() V113() V145() V147() Element of bool NAT
min q is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT
{(min q)} is non empty trivial finite V35() 1 -element V108() V109() V110() V111() V112() V113() V145() V146() V147() V148() V149() Element of bool NAT
q \ {(min q)} is V108() V109() V110() V111() V112() V113() V147() Element of bool NAT
p is set
f . p is set
u . p is set

f is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT
(s) . f is V108() V109() V110() V111() V112() V113() V147() Element of bool NAT
s is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT

(f) . s is non empty V108() V109() V110() V111() V112() V113() V145() V147() Element of bool NAT
(f) . 0 is non empty V108() V109() V110() V111() V112() V113() V145() V147() Element of bool NAT
{ b1 where b1 is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT : ( not intloc b1 in f & not b1 = 0 ) } is set
p is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT
intloc p is Int-like Element of the carrier of SCM+FSA
dl. p is Int-like Element of the carrier of SCM
p is V6() V7() V8() V12() ext-real non negative V27() V28() integer finite cardinal V97() V108() V109() V110() V111() V112() V113() V147() V148() V149() Element of NAT
intloc p is Int-like Element of the carrier of SCM+FSA
dl. p is Int-like Element of the carrier of SCM
q is V6() V7</