:: 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
K530() is Relation-like 3 -defined Function-like total 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()))):]
K529() * K530() is Relation-like K526() -defined Function-like set
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
SCM-Memory is 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
[:SCM-Memory,2:] is Relation-like set
bool [:SCM-Memory,2:] is V121() V123() V124() set
SCM-OK is Relation-like SCM-Memory -defined 2 -valued Function-like V43( SCM-Memory ,2) Element of bool [:SCM-Memory,2:]
SCM-VAL is Relation-like 2 -defined Function-like total set
SCM-OK * SCM-VAL is Relation-like SCM-Memory -defined Function-like set
product (SCM-OK * SCM-VAL) is set
K210() is Relation-like non empty V75() V76() V77() V79() set
K177((product (SCM-OK * SCM-VAL)),(product (SCM-OK * SCM-VAL))) is set
[:K210(),K177((product (SCM-OK * SCM-VAL)),(product (SCM-OK * SCM-VAL))):] is Relation-like set
bool [:K210(),K177((product (SCM-OK * SCM-VAL)),(product (SCM-OK * SCM-VAL))):] 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
SCM is non empty with_non-empty_values IC-Ins-separated strict strict V94(2) AMI-Struct over 2
the U5 of SCM is Relation-like non empty V75() V76() V77() V79() set
the carrier of SCM is non empty set
the_Values_of SCM is Relation-like non-empty the carrier of SCM -defined Function-like total 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
the ValuesF of SCM is Relation-like 2 -defined Function-like total set
the Object-Kind of SCM * the ValuesF of SCM is Relation-like the carrier of SCM -defined Function-like set
{} is Relation-like non-empty empty-yielding NAT -defined V6() V7() V8() V10() V11() V12() empty Function-like one-to-one constant functional ext-real non negative V27() V28() integer finite finite-yielding V35() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V108() V109() V110() V111() V112() V113() V114() Function-yielding V120() V147() V148() V149() V150() set
the Relation-like non-empty empty-yielding NAT -defined V6() V7() V8() V10() V11() V12() empty Function-like one-to-one constant functional ext-real non negative V27() V28() integer finite finite-yielding V35() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V108() V109() V110() V111() V112() V113() V114() Function-yielding V120() V147() V148() V149() V150() set is Relation-like non-empty empty-yielding NAT -defined V6() V7() V8() V10() V11() V12() empty Function-like one-to-one constant functional ext-real non negative V27() V28() integer finite finite-yielding V35() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V108() V109() V110() V111() V112() V113() V114() Function-yielding V120() V147() V148() V149() V150() set
K518() is set
bool K526() is V121() V123() V124() set
[:COMPLEX,COMPLEX:] is Relation-like non empty non trivial non finite V68() set
bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite V68() V121() V123() V124() set
[:COMPLEX,REAL:] is Relation-like non empty non trivial non finite V68() set
bool [:COMPLEX,REAL:] 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_Values_of SCM+FSA is Relation-like non-empty the carrier of SCM+FSA -defined Function-like total set
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
the ValuesF of SCM+FSA is Relation-like 3 -defined Function-like total set
the Object-Kind of SCM+FSA * the ValuesF of SCM+FSA is Relation-like the carrier of SCM+FSA -defined Function-like set
0 is Relation-like non-empty empty-yielding NAT -defined V6() V7() V8() V10() V11() V12() empty Function-like one-to-one constant functional ext-real non negative V27() V28() integer finite finite-yielding V35() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V97() V108() V109() V110() V111() V112() V113() V114() Function-yielding V120() V147() V148() V149() V150() Element of NAT
K528() is Element of bool K526()
INT * is non empty functional FinSequence-membered M13( INT )
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
NonZero SCM+FSA is Element of bool the carrier of SCM+FSA
Int-Locations \/ FinSeq-Locations is non empty Element of bool 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
K72(NAT,REAL,{1},NAT) is Relation-like NAT -defined REAL -valued non empty non trivial non finite V68() Element of bool [:NAT,REAL:]
[:NAT,REAL:] is Relation-like non empty non trivial non finite V68() set
bool [:NAT,REAL:] is non empty non trivial non finite V68() V121() V123() V124() set
Start-At (0,SCM+FSA) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible finite 0 -started set
(IC ) .--> 0 is Relation-like the carrier of SCM+FSA -defined {(IC )} -defined NAT -valued trivial Function-like one-to-one constant finite Function-yielding V120() set
{(IC )} is non empty trivial finite 1 -element set
{(IC )} --> 0 is Relation-like {(IC )} -defined NAT -valued {0} -valued non empty Function-like constant finite total V43({(IC )},{0}) Function-yielding V120() Element of bool [:{(IC )},{0}:]
{0} is non empty trivial functional finite V35() 1 -element V108() V109() V110() V111() V112() V113() V145() V146() V147() V148() V149() set
[:{(IC )},{0}:] is Relation-like finite set
bool [:{(IC )},{0}:] 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
(intloc 0) .--> 1 is Relation-like the carrier of SCM+FSA -defined {(intloc 0)} -defined NAT -valued trivial Function-like one-to-one constant finite set
{(intloc 0)} is non empty trivial finite 1 -element set
{(intloc 0)} --> 1 is Relation-like non-empty {(intloc 0)} -defined NAT -valued {1} -valued non empty Function-like constant finite total V43({(intloc 0)},{1}) Element of bool [:{(intloc 0)},{1}:]
{1} is non empty trivial finite V35() 1 -element V67() V68() V108() V109() V110() V111() V112() V113() V145() V146() V147() V148() V149() set
[:{(intloc 0)},{1}:] is Relation-like finite set
bool [:{(intloc 0)},{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
(intloc s) .--> f is Relation-like the carrier of SCM+FSA -defined {(intloc s)} -defined trivial Function-like one-to-one constant finite set
{(intloc s)} is non empty trivial finite 1 -element set
{(intloc s)} --> f is Relation-like {(intloc s)} -defined {f} -valued non empty Function-like constant finite total V43({(intloc s)},{f}) Element of bool [:{(intloc s)},{f}:]
{f} is non empty trivial finite 1 -element V108() V109() V110() V111() V112() V145() V146() V147() V148() V149() set
[:{(intloc s)},{f}:] is Relation-like finite set
bool [:{(intloc s)},{f}:] is finite V35() V121() V123() V124() set
dom ((intloc s) .--> f) is trivial finite set
{(intloc s)} is non empty trivial finite 1 -element Element of bool the carrier of SCM+FSA
rng ((intloc s) .--> 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
((intloc s) .--> f) . p is set
(the_Values_of SCM+FSA) . p is set
q is Int-like Element of the carrier of SCM+FSA
(the_Values_of SCM+FSA) . q is set
Values q is non empty set
s is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
Initialize ((intloc 0) .--> 1) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible finite 0 -started set
((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible finite 0 -started set
s +* (Initialize ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible 0 -started set
f is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
u is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
u +* (Initialize ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible 0 -started set
f +* (Initialize ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible 0 -started set
dom (Start-At (0,SCM+FSA)) is non empty finite set
{(IC )} is non empty trivial finite 1 -element Element of bool the carrier of SCM+FSA
u +* ((intloc 0) .--> 1) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
Initialize (u +* ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible 0 -started set
(u +* ((intloc 0) .--> 1)) +* (Start-At (0,SCM+FSA)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible 0 -started set
dom ((intloc 0) .--> 1) is trivial finite set
{(intloc 0)} is non empty trivial finite 1 -element Element of bool the carrier of SCM+FSA
(u +* (Initialize ((intloc 0) .--> 1))) . (intloc 0) is set
(Initialize (u +* ((intloc 0) .--> 1))) . (intloc 0) is set
(u +* ((intloc 0) .--> 1)) . (intloc 0) is set
((intloc 0) .--> 1) . (intloc 0) is set
(Start-At (0,SCM+FSA)) . (IC ) 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 . (IC ) is set
dom f is set
dom u is set
dom (Initialize ((intloc 0) .--> 1)) is finite set
(dom u) \/ (dom (Initialize ((intloc 0) .--> 1))) is set
(dom ((intloc 0) .--> 1)) \/ (dom (Start-At (0,SCM+FSA))) is non empty finite set
f +* ((intloc 0) .--> 1) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
Initialize (f +* ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible 0 -started set
(f +* ((intloc 0) .--> 1)) +* (Start-At (0,SCM+FSA)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible 0 -started set
f +* ((IC ) .--> 0) is Relation-like the carrier of SCM+FSA -defined Function-like set
s is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
(s) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
s +* (Initialize ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible 0 -started set
s is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible finite set
(s) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible 0 -started set
s +* (Initialize ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible finite 0 -started 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 is set
{(IC )} is non empty trivial finite 1 -element Element of bool the carrier of SCM+FSA
(NonZero SCM+FSA) \/ {(IC )} 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
fsloc u is FinSeq-Location
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
fsloc f is FinSeq-Location
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
F₁(f) is ext-real V27() V28() integer set
u is ext-real V27() V28() integer set
F₂(f) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
u is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
s is Relation-like Function-like 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
F₁(u) is ext-real V27() V28() integer set
fsloc u is FinSeq-Location
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₂(u) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
{(IC )} is non empty trivial finite 1 -element Element of bool the carrier of SCM+FSA
(NonZero SCM+FSA) \/ {(IC )} is non empty Element of bool the carrier of SCM+FSA
(the_Values_of SCM+FSA) . f is set
Values (intloc u) is non empty set
(the_Values_of SCM+FSA) . (intloc u) is set
(the_Values_of SCM+FSA) . f is set
Values (fsloc u) is non empty set
(the_Values_of SCM+FSA) . (fsloc u) is set
(the_Values_of SCM+FSA) . f is set
Values (IC ) is non empty set
(the_Values_of SCM+FSA) . (IC ) is set
f is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total 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 . (IC ) 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
F₁(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
fsloc p is FinSeq-Location
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
F₂(p) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
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 . (intloc u) is ext-real V27() V28() integer set
F₁(u) is ext-real V27() V28() integer set
fsloc u is FinSeq-Location
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 . (fsloc u) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
F₂(u) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
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
F₁(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
fsloc q is FinSeq-Location
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
F₂(q) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
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
F₁(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
fsloc q is FinSeq-Location
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
F₂(q) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
s is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
dom s is set
f is set
{(IC )} is non empty trivial finite 1 -element Element of bool the carrier of SCM+FSA
(NonZero SCM+FSA) \/ {(IC )} is non empty Element of bool the carrier of SCM+FSA
s is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
f is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
DataPart s is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
s | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
DataPart f is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
f | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
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
u is FinSeq-Location
s . u is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
f . u is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
dom f is set
{(IC )} is non empty trivial finite 1 -element Element of bool the carrier of SCM+FSA
(NonZero SCM+FSA) \/ {(IC )} 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
p is FinSeq-Location
s . p is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
f . p is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
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
q is FinSeq-Location
s . q is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
f . q is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
u2 is set
s . u2 is set
f . u2 is set
{(intloc 0)} is non empty trivial finite 1 -element Element of bool the carrier of SCM+FSA
{(IC )} is non empty trivial finite 1 -element Element of bool the carrier of SCM+FSA
s is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
(s) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible 0 -started set
s +* (Initialize ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible 0 -started set
dom (s) is set
dom s is set
(dom s) \/ {(intloc 0)} is non empty set
((dom s) \/ {(intloc 0)}) \/ {(IC )} is non empty set
dom ((intloc 0) .--> 1) is trivial finite set
dom (Start-At (0,SCM+FSA)) is non empty finite set
s +* ((intloc 0) .--> 1) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
Initialize (s +* ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible 0 -started set
(s +* ((intloc 0) .--> 1)) +* (Start-At (0,SCM+FSA)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible 0 -started set
dom (s +* ((intloc 0) .--> 1)) is set
(dom (s +* ((intloc 0) .--> 1))) \/ (dom (Start-At (0,SCM+FSA))) is non empty set
s is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
(s) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible 0 -started set
s +* (Initialize ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total 0 -started set
s is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
(s) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible 0 -started set
s +* (Initialize ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible 0 -started set
dom (s) is set
dom ((intloc 0) .--> 1) is trivial finite set
dom (Start-At (0,SCM+FSA)) is non empty finite set
dom s is set
(dom s) \/ {(intloc 0)} is non empty set
s +* ((intloc 0) .--> 1) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
Initialize (s +* ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible 0 -started set
(s +* ((intloc 0) .--> 1)) +* (Start-At (0,SCM+FSA)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible 0 -started set
dom (s +* ((intloc 0) .--> 1)) is set
(dom (s +* ((intloc 0) .--> 1))) \/ (dom (Start-At (0,SCM+FSA))) is non empty set
((dom s) \/ {(intloc 0)}) \/ {(IC )} is non empty set
s is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
(s) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible 0 -started set
s +* (Initialize ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible 0 -started set
(s) . (intloc 0) is set
(s) . (IC ) is set
dom ((intloc 0) .--> 1) is trivial finite set
s +* ((intloc 0) .--> 1) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
Initialize (s +* ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible 0 -started set
(s +* ((intloc 0) .--> 1)) +* (Start-At (0,SCM+FSA)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible 0 -started set
dom (Start-At (0,SCM+FSA)) is non empty finite set
(s +* ((intloc 0) .--> 1)) . (intloc 0) is set
((intloc 0) .--> 1) . (intloc 0) is set
(Start-At (0,SCM+FSA)) . (IC ) is set
s is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
dom s is set
(s) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible 0 -started set
s +* (Initialize ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible 0 -started set
dom (s) is set
f is Int-like Element of the carrier of SCM+FSA
(dom s) \/ {(intloc 0)} is non empty set
((dom s) \/ {(intloc 0)}) \/ {(IC )} is non empty set
s is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
dom s is set
(s) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible 0 -started set
s +* (Initialize ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible 0 -started set
dom (s) is set
f is FinSeq-Location
(dom s) \/ {(intloc 0)} is non empty set
((dom s) \/ {(intloc 0)}) \/ {(IC )} is non empty set
s is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
s . (intloc 0) 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 . (IC ) is set
(s) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total 0 -started set
s +* (Initialize ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total 0 -started set
dom s is set
s +* ((intloc 0) .--> 1) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
Initialize (s +* ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total 0 -started set
(s +* ((intloc 0) .--> 1)) +* (Start-At (0,SCM+FSA)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total 0 -started set
s +* ((IC ) .--> 0) is Relation-like the carrier of SCM+FSA -defined Function-like total set
s is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
(s) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible 0 -started set
s +* (Initialize ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible 0 -started set
(s) . (intloc 0) is set
((intloc 0) .--> 1) . (intloc 0) is set
s +* ((intloc 0) .--> 1) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
Initialize (s +* ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible 0 -started set
(s +* ((intloc 0) .--> 1)) +* (Start-At (0,SCM+FSA)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible 0 -started set
dom ((intloc 0) .--> 1) is trivial finite set
dom (Start-At (0,SCM+FSA)) is non empty finite set
(s +* ((intloc 0) .--> 1)) . (intloc 0) is set
dom (Initialize ((intloc 0) .--> 1)) is finite set
dom (Start-At (0,SCM+FSA)) is non empty finite set
dom ((intloc 0) .--> 1) is trivial finite set
(dom (Start-At (0,SCM+FSA))) \/ (dom ((intloc 0) .--> 1)) is non empty finite set
{(intloc 0),(IC )} is non empty finite Element of bool the carrier of SCM+FSA
dom ((intloc 0) .--> 1) is trivial finite set
dom (Start-At (0,SCM+FSA)) is non empty finite set
(dom ((intloc 0) .--> 1)) \/ (dom (Start-At (0,SCM+FSA))) is non empty finite set
(dom ((intloc 0) .--> 1)) \/ {(IC )} is non empty finite set
{(intloc 0)} \/ {(IC )} is non empty finite Element of bool the carrier of SCM+FSA
(Initialize ((intloc 0) .--> 1)) . (intloc 0) is set
dom (Start-At (0,SCM+FSA)) is non empty finite set
((intloc 0) .--> 1) . (intloc 0) is set
s is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
(s) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible 0 -started set
s +* (Initialize ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible 0 -started 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
s is finite Element of bool Int-Locations
{ b₁ where b₁ 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 b₁ in s } is set
{ b₁ where b₁ 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₁[b₁] } is set
[:{1},NAT:] 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 finite Element of bool Int-Locations
(s) is Int-like Element of the carrier of SCM+FSA
{ b₁ where b₁ 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 b₁ 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 finite Element of bool Int-Locations
(u) is Int-like Element of the carrier of SCM+FSA
{ b₁ where b₁ 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 b₁ 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
s is finite Element of bool FinSeq-Locations
{ b₁ where b₁ 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 b₁ in s } is set
{ b₁ where b₁ 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₁[b₁] } is set
u is set
p is FinSeq-Location
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 q is FinSeq-Location
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
f is FinSeq-Location
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
u is FinSeq-Location
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 finite Element of bool FinSeq-Locations
(s) is FinSeq-Location
{ b₁ where b₁ 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 b₁ 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
fsloc p is FinSeq-Location
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
fsloc s is FinSeq-Location
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
fsloc f is FinSeq-Location
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 finite Element of bool FinSeq-Locations
(u) is FinSeq-Location
{ b₁ where b₁ 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 b₁ 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
s is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total 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
(the_Values_of SCM+FSA) . p is set
dom s is set
Values f is non empty set
(the_Values_of SCM+FSA) . 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 .--> f is Relation-like the carrier of SCM+FSA -defined {s} -defined trivial Function-like one-to-one constant finite set
{s} is non empty trivial finite 1 -element set
{s} --> f is Relation-like {s} -defined {f} -valued non empty Function-like constant finite total V43({s},{f}) Element of bool [:{s},{f}:]
{f} is non empty trivial finite V35() 1 -element V108() V109() V110() V111() V112() V113() V145() V146() V147() V148() V149() set
[:{s},{f}:] is Relation-like finite set
bool [:{s},{f}:] is finite V35() V121() V123() V124() set
u is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
s is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
s . (intloc 0) is ext-real V27() V28() integer set
Initialize s is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total 0 -started set
s +* (Start-At (0,SCM+FSA)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total 0 -started set
(s) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total 0 -started set
s +* (Initialize ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total 0 -started set
dom s is set
s +* ((intloc 0) .--> 1) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
s is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
s . (intloc 0) is ext-real V27() V28() integer set
(s) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total 0 -started set
s +* (Initialize ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total 0 -started set
DataPart (s) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
(s) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
DataPart s is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
s | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
dom s is set
s +* ((intloc 0) .--> 1) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
Initialize (s +* ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total 0 -started set
(s +* ((intloc 0) .--> 1)) +* (Start-At (0,SCM+FSA)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total 0 -started set
Initialize s is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total 0 -started set
s +* (Start-At (0,SCM+FSA)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total 0 -started set
s is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
s . (intloc 0) is ext-real V27() V28() integer set
f is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
f . (intloc 0) is ext-real V27() V28() integer set
DataPart s is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
s | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
DataPart f is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
f | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
dom (DataPart s) is set
dom s is set
(dom s) /\ (NonZero SCM+FSA) is Element of bool the carrier of SCM+FSA
(NonZero SCM+FSA) \/ {(IC )} is non empty Element of bool the carrier of SCM+FSA
((NonZero SCM+FSA) \/ {(IC )}) /\ (NonZero SCM+FSA) is Element of bool the carrier of SCM+FSA
dom f is set
(dom f) /\ (NonZero SCM+FSA) is Element of bool the carrier of SCM+FSA
dom (DataPart f) is set
p is set
(DataPart s) . p is set
s . p is set
f . p is set
(DataPart f) . p is set
q is Int-like Element of the carrier of SCM+FSA
(DataPart s) . p is set
f . q is ext-real V27() V28() integer set
(DataPart f) . p is set
(DataPart s) . p is set
(DataPart f) . p is set
(DataPart s) . p is set
(DataPart f) . p is set
(DataPart s) . p is set
s . p is set
f . p is set
(DataPart f) . p is set
(DataPart s) . p is set
(DataPart f) . p is set
s is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total 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
Start-At (u,SCM+FSA) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible finite u -started set
(IC ) .--> u is Relation-like the carrier of SCM+FSA -defined {(IC )} -defined NAT -valued trivial Function-like one-to-one constant finite set
{(IC )} --> u is Relation-like {(IC )} -defined NAT -valued {u} -valued non empty Function-like constant finite total V43({(IC )},{u}) Element of bool [:{(IC )},{u}:]
{u} is non empty trivial finite V35() 1 -element V108() V109() V110() V111() V112() V113() V145() V146() V147() V148() V149() set
[:{(IC )},{u}:] is Relation-like finite set
bool [:{(IC )},{u}:] is finite V35() V121() V123() V124() set
s +* (Start-At (u,SCM+FSA)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total u -started 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,(bool NAT):] is Relation-like non empty non trivial non finite V68() set
bool [:NAT,(bool NAT):] is non empty non trivial non finite V68() V121() V123() V124() set
s is finite Element of bool Int-Locations
{ b₁ where b₁ 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 b₁ in s & not b₁ = 0 ) } is set
((intloc 0)) is non empty trivial finite 1 -element Element of bool Int-Locations
s \/ ((intloc 0)) is non empty finite Element of bool Int-Locations
{ b₁ where b₁ 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₁[b₁] } 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 is Relation-like NAT -defined bool NAT -valued Function-like V43( NAT , bool NAT) Element of bool [:NAT,(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
{ H₁(b₁) where b₁ 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 : b₁ in u2 } is set
sn1 is set
sn is finite set
(s \/ ((intloc 0))) \/ 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 is Relation-like NAT -defined bool NAT -valued Function-like V43( NAT , bool NAT) Element of bool [:NAT,(bool NAT):]
f . 0 is V108() V109() V110() V111() V112() V113() V147() Element of bool NAT
u is Relation-like NAT -defined bool NAT -valued Function-like V43( NAT , bool NAT) Element of bool [:NAT,(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
s is finite Element of bool Int-Locations
(s) is Relation-like NAT -defined bool NAT -valued Function-like V43( NAT , bool NAT) Element of bool [:NAT,(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
(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 is finite Element of bool Int-Locations
(f) is Relation-like NAT -defined bool NAT -valued Function-like V43( NAT , bool NAT) Element of bool [:NAT,(bool 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
{ b₁ where b₁ 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 b₁ in f & not b₁ = 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() 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
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 non empty V108() V109() V110() V111() V112() V113() V145() 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 non empty V108() V109() V110() V111() V112() V113() V145() 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
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
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
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
f is finite Element of bool Int-Locations
(f) is Relation-like NAT -defined bool NAT -valued Function-like V43( NAT , bool NAT) Element of bool [:NAT,(bool NAT):]
(f) . (s + 1) is non empty V108() V109() V110() V111() V112() V113() V145() V147() Element of bool NAT
min ((f) . (s + 1)) 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
min ((f) . 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
{(min ((f) . s))} is non empty trivial finite V35() 1 -element V108() V109() V110() V111() V112() V113() V145() V146() V147() V148() V149() Element of bool NAT
((f) . s) \ {(min ((f) . s))} 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 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 finite Element of bool Int-Locations
(u) is Relation-like NAT -defined bool NAT -valued Function-like V43( NAT , bool NAT) Element of bool [:NAT,(bool NAT):]
(u) . f is non empty V108() V109() V110() V111() V112() V113() V145() V147() Element of bool NAT
min ((u) . 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
(u) . s is non empty V108() V109() V110() V111() V112() V113() V145() V147() Element of bool NAT
min ((u) . 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
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
(u) . q is non empty V108() V109() V110() V111() V112() V113() V145() V147() Element of bool NAT
min ((u) . 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 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) . q is non empty V108() V109() V110() V111() V112() V113() V145() V147() Element of bool NAT
min ((u) . 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
(u) . (q + 1) is non empty V108() V109() V110() V111() V112() V113() V145() V147() Element of bool NAT
min ((u) . (q + 1)) 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) . 0 is non empty V108() V109() V110() V111() V112() V113() V145() V147() Element of bool NAT
min ((u) . 0) 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 finite Element of bool Int-Locations
(f) is Relation-like NAT -defined bool NAT -valued Function-like V43( NAT , bool NAT) Element of bool [:NAT,(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
min ((f) . 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 (min ((f) . s)) is Int-like Element of the carrier of SCM+FSA
dl. (min ((f) . s)) 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
f is finite Element of bool Int-Locations
(s,f) is Int-like Element of the carrier of SCM+FSA
(f) is Relation-like NAT -defined bool NAT -valued Function-like V43( NAT , bool NAT) Element of bool [:NAT,(bool NAT):]
(f) . s is non empty V108() V109() V110() V111() V112() V113() V145() V147() Element of bool NAT
min ((f) . 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 (min ((f) . s)) is Int-like Element of the carrier of SCM+FSA
dl. (min ((f) . s)) 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
f is finite Element of bool Int-Locations
(s,f) is Int-like () Element of the carrier of SCM+FSA
(f) is Relation-like NAT -defined bool NAT -valued Function-like V43( NAT , bool NAT) Element of bool [:NAT,(bool NAT):]
(f) . s is non empty V108() V109() V110() V111() V112() V113() V145() V147() Element of bool NAT
min ((f) . 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 (min ((f) . s)) is Int-like Element of the carrier of SCM+FSA
dl. (min ((f) . s)) 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
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
u is finite Element of bool Int-Locations
(s,u) is Int-like () Element of the carrier of SCM+FSA
(u) is Relation-like NAT -defined bool NAT -valued Function-like V43( NAT , bool NAT) Element of bool [:NAT,(bool NAT):]
(u) . s is non empty V108() V109() V110() V111() V112() V113() V145() V147() Element of bool NAT
min ((u) . 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 (min ((u) . s)) is Int-like Element of the carrier of SCM+FSA
dl. (min ((u) . s)) is Int-like Element of the carrier of SCM
(f,u) is Int-like () Element of the carrier of SCM+FSA
(u) . f is non empty V108() V109() V110() V111() V112() V113() V145() V147() Element of bool NAT
min ((u) . 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 (min ((u) . f)) is Int-like Element of the carrier of SCM+FSA
dl. (min ((u) . f)) is Int-like Element of the carrier of SCM
s is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
f is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
u is Element of bool Int-Locations
p is Element of bool FinSeq-Locations
u \/ p is set
s | (u \/ p) is Relation-like the carrier of SCM+FSA -defined u \/ p -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
f | (u \/ p) is Relation-like the carrier of SCM+FSA -defined u \/ p -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
dom s is set
dom f is 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
q is FinSeq-Location
s . q is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
f . q is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
q is set
s . q is set
q is Int-like Element of the carrier of SCM+FSA
f . q is ext-real V27() V28() integer set
f . q is set
q is set
s . q is set
q is FinSeq-Location
f . q is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
f . q is set
s | p is Relation-like the carrier of SCM+FSA -defined p -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
f | p is Relation-like the carrier of SCM+FSA -defined p -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
s | u is Relation-like the carrier of SCM+FSA -defined u -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
f | u is Relation-like the carrier of SCM+FSA -defined u -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
s is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
f is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
p is Element of bool Int-Locations
p \/ FinSeq-Locations is non empty set
s | (p \/ FinSeq-Locations) is Relation-like the carrier of SCM+FSA -defined p \/ FinSeq-Locations -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
f | (p \/ FinSeq-Locations) is Relation-like the carrier of SCM+FSA -defined p \/ FinSeq-Locations -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
q is FinSeq-Location
s . q is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
f . q is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
q is FinSeq-Location
s . q is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
f . q is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
[#] FinSeq-Locations is Element of bool FinSeq-Locations
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
q is FinSeq-Location
s . q is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
f . q is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
u2 is FinSeq-Location
s . u2 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
f . u2 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
f is FinSeq-Location
s . f is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
f . f is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
s 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
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
(intloc f) .--> u is Relation-like the carrier of SCM+FSA -defined {(intloc f)} -defined {(intloc f)} -defined NAT -valued trivial Function-like one-to-one constant the_Values_of SCM+FSA -compatible finite data-only set
{(intloc f)} is non empty trivial finite 1 -element set
{(intloc f)} --> u is Relation-like {(intloc f)} -defined NAT -valued {u} -valued non empty Function-like constant finite total V43({(intloc f)},{u}) Element of bool [:{(intloc f)},{u}:]
{u} is non empty trivial finite V35() 1 -element V108() V109() V110() V111() V112() V113() V145() V146() V147() V148() V149() set
[:{(intloc f)},{u}:] is Relation-like finite set
bool [:{(intloc f)},{u}:] is finite V35() V121() V123() V124() 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
Start-At (p,SCM+FSA) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible finite p -started set
(IC ) .--> p is Relation-like the carrier of SCM+FSA -defined {(IC )} -defined NAT -valued trivial Function-like one-to-one constant finite set
{(IC )} --> p is Relation-like {(IC )} -defined NAT -valued {p} -valued non empty Function-like constant finite total V43({(IC )},{p}) Element of bool [:{(IC )},{p}:]
{p} is non empty trivial finite V35() 1 -element V108() V109() V110() V111() V112() V113() V145() V146() V147() V148() V149() set
[:{(IC )},{p}:] is Relation-like finite set
bool [:{(IC )},{p}:] is finite V35() V121() V123() V124() set
((intloc f) .--> u) +* (Start-At (p,SCM+FSA)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible finite p -started set
dom (((intloc f) .--> u) +* (Start-At (p,SCM+FSA))) is non empty finite set
dom ((intloc f) .--> u) is trivial finite set
((intloc f)) is non empty trivial finite 1 -element Element of bool Int-Locations
dom (Start-At (p,SCM+FSA)) is non empty finite set
((intloc f)) \/ {(IC )} is non empty finite set
s is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
s . (intloc 0) is ext-real V27() V28() integer set
dom ((intloc 0) .--> 1) is trivial finite set
dom (Start-At (0,SCM+FSA)) is non empty finite set
(dom ((intloc 0) .--> 1)) \/ (dom (Start-At (0,SCM+FSA))) is non empty finite set
((intloc 0) .--> 1) . (intloc 0) is 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
intloc (s + 1) is Int-like Element of the carrier of SCM+FSA
dl. (s + 1) is Int-like Element of the carrier of SCM
[:NAT,INT:] is Relation-like non empty non trivial non finite V68() set
bool [:NAT,INT:] is non empty non trivial non finite V68() V121() V123() V124() set
s is FinSeq-Location
f is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
s .--> f is Relation-like the carrier of SCM+FSA -defined {s} -defined bool [:NAT,INT:] -valued trivial Function-like one-to-one constant finite Function-yielding V120() set
{s} is non empty trivial finite 1 -element set
{s} --> f is Relation-like {s} -defined {f} -valued bool [:NAT,INT:] -valued non empty Function-like constant finite total V43({s},{f}) Function-yielding V120() Element of bool [:{s},{f}:]
{f} is non empty trivial functional finite V35() 1 -element set
[:{s},{f}:] is Relation-like finite set
bool [:{s},{f}:] is finite V35() V121() V123() V124() set
Values s is non empty set
(the_Values_of SCM+FSA) . s is set
s is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
f is FinSeq-Location
f .--> s is Relation-like the carrier of SCM+FSA -defined {f} -defined bool [:NAT,INT:] -valued bool [:NAT,INT:] -valued trivial Function-like one-to-one constant the_Values_of SCM+FSA -compatible finite Function-yielding V120() set
{f} is non empty trivial finite 1 -element set
{f} --> s is Relation-like {f} -defined {s} -valued bool [:NAT,INT:] -valued non empty Function-like constant finite total V43({f},{s}) Function-yielding V120() Element of bool [:{f},{s}:]
{s} is non empty trivial functional finite V35() 1 -element set
[:{f},{s}:] is Relation-like finite set
bool [:{f},{s}:] is finite V35() V121() V123() V124() set
((f .--> s)) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible finite 0 -started set
(f .--> s) +* (Initialize ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible finite 0 -started set
dom ((f .--> s)) is finite set
{(intloc 0),(IC ),f} is finite Element of bool the carrier of SCM+FSA
dom (f .--> s) is trivial finite set
(dom (Initialize ((intloc 0) .--> 1))) \/ (dom (f .--> s)) is finite set
{f} is non empty trivial finite 1 -element Element of bool the carrier of SCM+FSA
{(intloc 0),(IC )} \/ {f} is non empty finite Element of bool the carrier of SCM+FSA
s is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
f is FinSeq-Location
f .--> s is Relation-like the carrier of SCM+FSA -defined {f} -defined bool [:NAT,INT:] -valued bool [:NAT,INT:] -valued trivial Function-like one-to-one constant the_Values_of SCM+FSA -compatible finite Function-yielding V120() set
{f} is non empty trivial finite 1 -element set
{f} --> s is Relation-like {f} -defined {s} -valued bool [:NAT,INT:] -valued non empty Function-like constant finite total V43({f},{s}) Function-yielding V120() Element of bool [:{f},{s}:]
{s} is non empty trivial functional finite V35() 1 -element set
[:{f},{s}:] is Relation-like finite set
bool [:{f},{s}:] is finite V35() V121() V123() V124() set
dom (f .--> s) is trivial finite set
{f} is non empty trivial finite 1 -element Element of bool the carrier of SCM+FSA
(dom (Initialize ((intloc 0) .--> 1))) /\ (dom (f .--> s)) is finite set
q is set
s is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
f is FinSeq-Location
f .--> s is Relation-like the carrier of SCM+FSA -defined {f} -defined bool [:NAT,INT:] -valued bool [:NAT,INT:] -valued trivial Function-like one-to-one constant the_Values_of SCM+FSA -compatible finite Function-yielding V120() set
{f} is non empty trivial finite 1 -element set
{f} --> s is Relation-like {f} -defined {s} -valued bool [:NAT,INT:] -valued non empty Function-like constant finite total V43({f},{s}) Function-yielding V120() Element of bool [:{f},{s}:]
{s} is non empty trivial functional finite V35() 1 -element set
[:{f},{s}:] is Relation-like finite set
bool [:{f},{s}:] is finite V35() V121() V123() V124() set
((f .--> s)) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible finite 0 -started set
(f .--> s) +* (Initialize ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible finite 0 -started set
u is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
u . f is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
u . (intloc 0) is ext-real V27() V28() integer set
dom (f .--> s) is trivial finite set
{f} is non empty trivial finite 1 -element Element of bool the carrier of SCM+FSA
q is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
dom q is set
u2 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 u2 is FinSeq-Location
u2 + 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((u2 + 1)) is ext-real non positive V27() V28() integer set
((intloc 0)) is non empty trivial finite 1 -element Element of bool Int-Locations
dom ((intloc 0) .--> 1) is trivial finite set
dom (Start-At (0,SCM+FSA)) is non empty finite set
(dom ((intloc 0) .--> 1)) \/ (dom (Start-At (0,SCM+FSA))) is non empty finite set
q . f is set
(f .--> s) . f is Relation-like Function-like set
((f .--> s)) . (intloc 0) is set
s is FinSeq-Location
f is Int-like Element of the carrier of SCM+FSA
{f,(IC ),s} is finite Element of bool the carrier of SCM+FSA
u is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
dom u is set
{f,(IC )} is non empty finite Element of bool the carrier of SCM+FSA
{s} is non empty trivial finite 1 -element Element of bool the carrier of SCM+FSA
{f,(IC )} \/ {s} is non empty finite Element of bool the carrier of SCM+FSA
FinPartSt SCM+FSA is non empty Element of bool (sproduct (the_Values_of SCM+FSA))
sproduct (the_Values_of SCM+FSA) is set
bool (sproduct (the_Values_of SCM+FSA)) is V121() V123() V124() set
{ b₁ where b₁ is Element of sproduct (the_Values_of SCM+FSA) : b₁ is finite } is set
[:(FinPartSt SCM+FSA),(FinPartSt SCM+FSA):] is Relation-like set
bool [:(FinPartSt SCM+FSA),(FinPartSt SCM+FSA):] is V121() V123() V124() set
fsloc 0 is FinSeq-Location
0 + 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((0 + 1)) is ext-real non positive V27() V28() integer set
s is set
f is set
u is set
p is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
q is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of REAL
(fsloc 0) .--> p is Relation-like the carrier of SCM+FSA -defined {(fsloc 0)} -defined bool [:NAT,INT:] -valued bool [:NAT,INT:] -valued trivial Function-like one-to-one constant the_Values_of SCM+FSA -compatible finite Function-yielding V120() set
{(fsloc 0)} is non empty trivial finite 1 -element set
{(fsloc 0)} --> p is Relation-like {(fsloc 0)} -defined {p} -valued bool [:NAT,INT:] -valued non empty Function-like constant finite total V43({(fsloc 0)},{p}) Function-yielding V120() Element of bool [:{(fsloc 0)},{p}:]
{p} is non empty trivial functional finite V35() 1 -element set
[:{(fsloc 0)},{p}:] is Relation-like finite set
bool [:{(fsloc 0)},{p}:] is finite V35() V121() V123() V124() set
(fsloc 0) .--> q is Relation-like the carrier of SCM+FSA -defined {(fsloc 0)} -defined bool [:NAT,REAL:] -valued trivial Function-like one-to-one constant finite Function-yielding V120() set
{(fsloc 0)} --> q is Relation-like {(fsloc 0)} -defined {q} -valued bool [:NAT,REAL:] -valued non empty Function-like constant finite total V43({(fsloc 0)},{q}) Function-yielding V120() Element of bool [:{(fsloc 0)},{q}:]
{q} is non empty trivial functional finite V35() 1 -element set
[:{(fsloc 0)},{q}:] is Relation-like finite set
bool [:{(fsloc 0)},{q}:] is finite V35() V121() V123() V124() set
q is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
u2 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of REAL
(fsloc 0) .--> q is Relation-like the carrier of SCM+FSA -defined {(fsloc 0)} -defined bool [:NAT,INT:] -valued bool [:NAT,INT:] -valued trivial Function-like one-to-one constant the_Values_of SCM+FSA -compatible finite Function-yielding V120() set
{(fsloc 0)} --> q is Relation-like {(fsloc 0)} -defined {q} -valued bool [:NAT,INT:] -valued non empty Function-like constant finite total V43({(fsloc 0)},{q}) Function-yielding V120() Element of bool [:{(fsloc 0)},{q}:]
{q} is non empty trivial functional finite V35() 1 -element set
[:{(fsloc 0)},{q}:] is Relation-like finite set
bool [:{(fsloc 0)},{q}:] is finite V35() V121() V123() V124() set
(fsloc 0) .--> u2 is Relation-like the carrier of SCM+FSA -defined {(fsloc 0)} -defined bool [:NAT,REAL:] -valued trivial Function-like one-to-one constant finite Function-yielding V120() set
{(fsloc 0)} --> u2 is Relation-like {(fsloc 0)} -defined {u2} -valued bool [:NAT,REAL:] -valued non empty Function-like constant finite total V43({(fsloc 0)},{u2}) Function-yielding V120() Element of bool [:{(fsloc 0)},{u2}:]
{u2} is non empty trivial functional finite V35() 1 -element set
[:{(fsloc 0)},{u2}:] is Relation-like finite set
bool [:{(fsloc 0)},{u2}:] is finite V35() V121() V123() V124() set
((fsloc 0) .--> p) . (fsloc 0) is Relation-like Function-like set
s is Relation-like Function-like set
dom s is set
f is set
s . f is set
[f,(s . f)] is set
{f,(s . f)} is non empty finite set
{f} is non empty trivial finite 1 -element set
{{f,(s . f)},{f}} is non empty finite V35() V67() V68() set
rng s is set
f is set
u is set
[u,f] is set
{u,f} is non empty finite set
{u} is non empty trivial finite 1 -element set
{{u,f},{u}} is non empty finite V35() V67() V68() set
p is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
q is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of REAL
(fsloc 0) .--> p is Relation-like the carrier of SCM+FSA -defined {(fsloc 0)} -defined bool [:NAT,INT:] -valued bool [:NAT,INT:] -valued trivial Function-like one-to-one constant the_Values_of SCM+FSA -compatible finite Function-yielding V120() set
{(fsloc 0)} is non empty trivial finite 1 -element set
{(fsloc 0)} --> p is Relation-like {(fsloc 0)} -defined {p} -valued bool [:NAT,INT:] -valued non empty Function-like constant finite total V43({(fsloc 0)},{p}) Function-yielding V120() Element of bool [:{(fsloc 0)},{p}:]
{p} is non empty trivial functional finite V35() 1 -element set
[:{(fsloc 0)},{p}:] is Relation-like finite set
bool [:{(fsloc 0)},{p}:] is finite V35() V121() V123() V124() set
(fsloc 0) .--> q is Relation-like the carrier of SCM+FSA -defined {(fsloc 0)} -defined bool [:NAT,REAL:] -valued trivial Function-like one-to-one constant finite Function-yielding V120() set
{(fsloc 0)} --> q is Relation-like {(fsloc 0)} -defined {q} -valued bool [:NAT,REAL:] -valued non empty Function-like constant finite total V43({(fsloc 0)},{q}) Function-yielding V120() Element of bool [:{(fsloc 0)},{q}:]
{q} is non empty trivial functional finite V35() 1 -element set
[:{(fsloc 0)},{q}:] is Relation-like finite set
bool [:{(fsloc 0)},{q}:] is finite V35() V121() V123() V124() set
q is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
(fsloc 0) .--> q is Relation-like the carrier of SCM+FSA -defined {(fsloc 0)} -defined bool [:NAT,INT:] -valued bool [:NAT,INT:] -valued trivial Function-like one-to-one constant the_Values_of SCM+FSA -compatible finite Function-yielding V120() set
{(fsloc 0)} --> q is Relation-like {(fsloc 0)} -defined {q} -valued bool [:NAT,INT:] -valued non empty Function-like constant finite total V43({(fsloc 0)},{q}) Function-yielding V120() Element of bool [:{(fsloc 0)},{q}:]
{q} is non empty trivial functional finite V35() 1 -element set
[:{(fsloc 0)},{q}:] is Relation-like finite set
bool [:{(fsloc 0)},{q}:] is finite V35() V121() V123() V124() set
f is Relation-like FinPartSt SCM+FSA -defined FinPartSt SCM+FSA -valued Function-like Element of bool [:(FinPartSt SCM+FSA),(FinPartSt SCM+FSA):]
u is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible finite set
p is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible finite set
[u,p] is set
{u,p} is non empty functional finite V35() set
{u} is non empty trivial functional finite V35() 1 -element set
{{u,p},{u}} is non empty finite V35() V67() V68() set
q is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
q is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of REAL
(fsloc 0) .--> q is Relation-like the carrier of SCM+FSA -defined {(fsloc 0)} -defined bool [:NAT,INT:] -valued bool [:NAT,INT:] -valued trivial Function-like one-to-one constant the_Values_of SCM+FSA -compatible finite Function-yielding V120() set
{(fsloc 0)} is non empty trivial finite 1 -element set
{(fsloc 0)} --> q is Relation-like {(fsloc 0)} -defined {q} -valued bool [:NAT,INT:] -valued non empty Function-like constant finite total V43({(fsloc 0)},{q}) Function-yielding V120() Element of bool [:{(fsloc 0)},{q}:]
{q} is non empty trivial functional finite V35() 1 -element set
[:{(fsloc 0)},{q}:] is Relation-like finite set
bool [:{(fsloc 0)},{q}:] is finite V35() V121() V123() V124() set
(fsloc 0) .--> q is Relation-like the carrier of SCM+FSA -defined {(fsloc 0)} -defined bool [:NAT,REAL:] -valued trivial Function-like one-to-one constant finite Function-yielding V120() set
{(fsloc 0)} --> q is Relation-like {(fsloc 0)} -defined {q} -valued bool [:NAT,REAL:] -valued non empty Function-like constant finite total V43({(fsloc 0)},{q}) Function-yielding V120() Element of bool [:{(fsloc 0)},{q}:]
{q} is non empty trivial functional finite V35() 1 -element set
[:{(fsloc 0)},{q}:] is Relation-like finite set
bool [:{(fsloc 0)},{q}:] is finite V35() V121() V123() V124() set
s is Relation-like FinPartSt SCM+FSA -defined FinPartSt SCM+FSA -valued Function-like Element of bool [:(FinPartSt SCM+FSA),(FinPartSt SCM+FSA):]
f is Relation-like FinPartSt SCM+FSA -defined FinPartSt SCM+FSA -valued Function-like Element of bool [:(FinPartSt SCM+FSA),(FinPartSt SCM+FSA):]
u is Element of FinPartSt SCM+FSA
p is Element of FinPartSt SCM+FSA
[u,p] is Element of [:(FinPartSt SCM+FSA),(FinPartSt SCM+FSA):]
{u,p} is non empty finite set
{u} is non empty trivial finite 1 -element set
{{u,p},{u}} is non empty finite V35() V67() V68() set
q is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible finite set
q is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible finite set
[q,q] is set
{q,q} is non empty functional finite V35() set
{q} is non empty trivial functional finite V35() 1 -element set
{{q,q},{q}} is non empty finite V35() V67() V68() set
u2 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
f is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of REAL
(fsloc 0) .--> u2 is Relation-like the carrier of SCM+FSA -defined {(fsloc 0)} -defined bool [:NAT,INT:] -valued bool [:NAT,INT:] -valued trivial Function-like one-to-one constant the_Values_of SCM+FSA -compatible finite Function-yielding V120() set
{(fsloc 0)} is non empty trivial finite 1 -element set
{(fsloc 0)} --> u2 is Relation-like {(fsloc 0)} -defined {u2} -valued bool [:NAT,INT:] -valued non empty Function-like constant finite total V43({(fsloc 0)},{u2}) Function-yielding V120() Element of bool [:{(fsloc 0)},{u2}:]
{u2} is non empty trivial functional finite V35() 1 -element set
[:{(fsloc 0)},{u2}:] is Relation-like finite set
bool [:{(fsloc 0)},{u2}:] is finite V35() V121() V123() V124() set
(fsloc 0) .--> f is Relation-like the carrier of SCM+FSA -defined {(fsloc 0)} -defined bool [:NAT,REAL:] -valued trivial Function-like one-to-one constant finite Function-yielding V120() set
{(fsloc 0)} --> f is Relation-like {(fsloc 0)} -defined {f} -valued bool [:NAT,REAL:] -valued non empty Function-like constant finite total V43({(fsloc 0)},{f}) Function-yielding V120() Element of bool [:{(fsloc 0)},{f}:]
{f} is non empty trivial functional finite V35() 1 -element set
[:{(fsloc 0)},{f}:] is Relation-like finite set
bool [:{(fsloc 0)},{f}:] is finite V35() V121() V123() V124() set
u2 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
f is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of REAL
(fsloc 0) .--> u2 is Relation-like the carrier of SCM+FSA -defined {(fsloc 0)} -defined bool [:NAT,INT:] -valued bool [:NAT,INT:] -valued trivial Function-like one-to-one constant the_Values_of SCM+FSA -compatible finite Function-yielding V120() set
{(fsloc 0)} is non empty trivial finite 1 -element set
{(fsloc 0)} --> u2 is Relation-like {(fsloc 0)} -defined {u2} -valued bool [:NAT,INT:] -valued non empty Function-like constant finite total V43({(fsloc 0)},{u2}) Function-yielding V120() Element of bool [:{(fsloc 0)},{u2}:]
{u2} is non empty trivial functional finite V35() 1 -element set
[:{(fsloc 0)},{u2}:] is Relation-like finite set
bool [:{(fsloc 0)},{u2}:] is finite V35() V121() V123() V124() set
(fsloc 0) .--> f is Relation-like the carrier of SCM+FSA -defined {(fsloc 0)} -defined bool [:NAT,REAL:] -valued trivial Function-like one-to-one constant finite Function-yielding V120() set
{(fsloc 0)} --> f is Relation-like {(fsloc 0)} -defined {f} -valued bool [:NAT,REAL:] -valued non empty Function-like constant finite total V43({(fsloc 0)},{f}) Function-yielding V120() Element of bool [:{(fsloc 0)},{f}:]
{f} is non empty trivial functional finite V35() 1 -element set
[:{(fsloc 0)},{f}:] is Relation-like finite set
bool [:{(fsloc 0)},{f}:] is finite V35() V121() V123() V124() set
n is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
sn is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of REAL
(fsloc 0) .--> n is Relation-like the carrier of SCM+FSA -defined {(fsloc 0)} -defined bool [:NAT,INT:] -valued bool [:NAT,INT:] -valued trivial Function-like one-to-one constant the_Values_of SCM+FSA -compatible finite Function-yielding V120() set
{(fsloc 0)} --> n is Relation-like {(fsloc 0)} -defined {n} -valued bool [:NAT,INT:] -valued non empty Function-like constant finite total V43({(fsloc 0)},{n}) Function-yielding V120() Element of bool [:{(fsloc 0)},{n}:]
{n} is non empty trivial functional finite V35() 1 -element set
[:{(fsloc 0)},{n}:] is Relation-like finite set
bool [:{(fsloc 0)},{n}:] is finite V35() V121() V123() V124() set
(fsloc 0) .--> sn is Relation-like the carrier of SCM+FSA -defined {(fsloc 0)} -defined bool [:NAT,REAL:] -valued trivial Function-like one-to-one constant finite Function-yielding V120() set
{(fsloc 0)} --> sn is Relation-like {(fsloc 0)} -defined {sn} -valued bool [:NAT,REAL:] -valued non empty Function-like constant finite total V43({(fsloc 0)},{sn}) Function-yielding V120() Element of bool [:{(fsloc 0)},{sn}:]
{sn} is non empty trivial functional finite V35() 1 -element set
[:{(fsloc 0)},{sn}:] is Relation-like finite set
bool [:{(fsloc 0)},{sn}:] is finite V35() V121() V123() V124() set
u is Element of FinPartSt SCM+FSA
p is Element of FinPartSt SCM+FSA
[u,p] is Element of [:(FinPartSt SCM+FSA),(FinPartSt SCM+FSA):]
{u,p} is non empty finite set
{u} is non empty trivial finite 1 -element set
{{u,p},{u}} is non empty finite V35() V67() V68() set
q is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible finite set
q is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible finite set
[q,q] is set
{q,q} is non empty functional finite V35() set
{q} is non empty trivial functional finite V35() 1 -element set
{{q,q},{q}} is non empty finite V35() V67() V68() set
u2 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
f is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of REAL
(fsloc 0) .--> u2 is Relation-like the carrier of SCM+FSA -defined {(fsloc 0)} -defined bool [:NAT,INT:] -valued bool [:NAT,INT:] -valued trivial Function-like one-to-one constant the_Values_of SCM+FSA -compatible finite Function-yielding V120() set
{(fsloc 0)} is non empty trivial finite 1 -element set
{(fsloc 0)} --> u2 is Relation-like {(fsloc 0)} -defined {u2} -valued bool [:NAT,INT:] -valued non empty Function-like constant finite total V43({(fsloc 0)},{u2}) Function-yielding V120() Element of bool [:{(fsloc 0)},{u2}:]
{u2} is non empty trivial functional finite V35() 1 -element set
[:{(fsloc 0)},{u2}:] is Relation-like finite set
bool [:{(fsloc 0)},{u2}:] is finite V35() V121() V123() V124() set
(fsloc 0) .--> f is Relation-like the carrier of SCM+FSA -defined {(fsloc 0)} -defined bool [:NAT,REAL:] -valued trivial Function-like one-to-one constant finite Function-yielding V120() set
{(fsloc 0)} --> f is Relation-like {(fsloc 0)} -defined {f} -valued bool [:NAT,REAL:] -valued non empty Function-like constant finite total V43({(fsloc 0)},{f}) Function-yielding V120() Element of bool [:{(fsloc 0)},{f}:]
{f} is non empty trivial functional finite V35() 1 -element set
[:{(fsloc 0)},{f}:] is Relation-like finite set
bool [:{(fsloc 0)},{f}:] is finite V35() V121() V123() V124() set
u2 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
f is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of REAL
(fsloc 0) .--> u2 is Relation-like the carrier of SCM+FSA -defined {(fsloc 0)} -defined bool [:NAT,INT:] -valued bool [:NAT,INT:] -valued trivial Function-like one-to-one constant the_Values_of SCM+FSA -compatible finite Function-yielding V120() set
{(fsloc 0)} is non empty trivial finite 1 -element set
{(fsloc 0)} --> u2 is Relation-like {(fsloc 0)} -defined {u2} -valued bool [:NAT,INT:] -valued non empty Function-like constant finite total V43({(fsloc 0)},{u2}) Function-yielding V120() Element of bool [:{(fsloc 0)},{u2}:]
{u2} is non empty trivial functional finite V35() 1 -element set
[:{(fsloc 0)},{u2}:] is Relation-like finite set
bool [:{(fsloc 0)},{u2}:] is finite V35() V121() V123() V124() set
(fsloc 0) .--> f is Relation-like the carrier of SCM+FSA -defined {(fsloc 0)} -defined bool [:NAT,REAL:] -valued trivial Function-like one-to-one constant finite Function-yielding V120() set
{(fsloc 0)} --> f is Relation-like {(fsloc 0)} -defined {f} -valued bool [:NAT,REAL:] -valued non empty Function-like constant finite total V43({(fsloc 0)},{f}) Function-yielding V120() Element of bool [:{(fsloc 0)},{f}:]
{f} is non empty trivial functional finite V35() 1 -element set
[:{(fsloc 0)},{f}:] is Relation-like finite set
bool [:{(fsloc 0)},{f}:] is finite V35() V121() V123() V124() set
n is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
sn is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of REAL
(fsloc 0) .--> n is Relation-like the carrier of SCM+FSA -defined {(fsloc 0)} -defined bool [:NAT,INT:] -valued bool [:NAT,INT:] -valued trivial Function-like one-to-one constant the_Values_of SCM+FSA -compatible finite Function-yielding V120() set
{(fsloc 0)} --> n is Relation-like {(fsloc 0)} -defined {n} -valued bool [:NAT,INT:] -valued non empty Function-like constant finite total V43({(fsloc 0)},{n}) Function-yielding V120() Element of bool [:{(fsloc 0)},{n}:]
{n} is non empty trivial functional finite V35() 1 -element set
[:{(fsloc 0)},{n}:] is Relation-like finite set
bool [:{(fsloc 0)},{n}:] is finite V35() V121() V123() V124() set
(fsloc 0) .--> sn is Relation-like the carrier of SCM+FSA -defined {(fsloc 0)} -defined bool [:NAT,REAL:] -valued trivial Function-like one-to-one constant finite Function-yielding V120() set
{(fsloc 0)} --> sn is Relation-like {(fsloc 0)} -defined {sn} -valued bool [:NAT,REAL:] -valued non empty Function-like constant finite total V43({(fsloc 0)},{sn}) Function-yielding V120() Element of bool [:{(fsloc 0)},{sn}:]
{sn} is non empty trivial functional finite V35() 1 -element set
[:{(fsloc 0)},{sn}:] is Relation-like finite set
bool [:{(fsloc 0)},{sn}:] is finite V35() V121() V123() V124() set
() is Relation-like FinPartSt SCM+FSA -defined FinPartSt SCM+FSA -valued Function-like Element of bool [:(FinPartSt SCM+FSA),(FinPartSt SCM+FSA):]
dom () is set
f is set
() . f is set
[f,(() . f)] is set
{f,(() . f)} is non empty finite set
{f} is non empty trivial finite 1 -element set
{{f,(() . f)},{f}} is non empty finite V35() V67() V68() set
p is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
q is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of REAL
(fsloc 0) .--> p is Relation-like the carrier of SCM+FSA -defined {(fsloc 0)} -defined bool [:NAT,INT:] -valued bool [:NAT,INT:] -valued trivial Function-like one-to-one constant the_Values_of SCM+FSA -compatible finite Function-yielding V120() set
{(fsloc 0)} is non empty trivial finite 1 -element set
{(fsloc 0)} --> p is Relation-like {(fsloc 0)} -defined {p} -valued bool [:NAT,INT:] -valued non empty Function-like constant finite total V43({(fsloc 0)},{p}) Function-yielding V120() Element of bool [:{(fsloc 0)},{p}:]
{p} is non empty trivial functional finite V35() 1 -element set
[:{(fsloc 0)},{p}:] is Relation-like finite set
bool [:{(fsloc 0)},{p}:] is finite V35() V121() V123() V124() set
(fsloc 0) .--> q is Relation-like the carrier of SCM+FSA -defined {(fsloc 0)} -defined bool [:NAT,REAL:] -valued trivial Function-like one-to-one constant finite Function-yielding V120() set
{(fsloc 0)} --> q is Relation-like {(fsloc 0)} -defined {q} -valued bool [:NAT,REAL:] -valued non empty Function-like constant finite total V43({(fsloc 0)},{q}) Function-yielding V120() Element of bool [:{(fsloc 0)},{q}:]
{q} is non empty trivial functional finite V35() 1 -element set
[:{(fsloc 0)},{q}:] is Relation-like finite set
bool [:{(fsloc 0)},{q}:] is finite V35() V121() V123() V124() set
q is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
(fsloc 0) .--> q is Relation-like the carrier of SCM+FSA -defined {(fsloc 0)} -defined bool [:NAT,INT:] -valued bool [:NAT,INT:] -valued trivial Function-like one-to-one constant the_Values_of SCM+FSA -compatible finite Function-yielding V120() set
{(fsloc 0)} --> q is Relation-like {(fsloc 0)} -defined {q} -valued bool [:NAT,INT:] -valued non empty Function-like constant finite total V43({(fsloc 0)},{q}) Function-yielding V120() Element of bool [:{(fsloc 0)},{q}:]
{q} is non empty trivial functional finite V35() 1 -element set
[:{(fsloc 0)},{q}:] is Relation-like finite set
bool [:{(fsloc 0)},{q}:] is finite V35() V121() V123() V124() set
u is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
(fsloc 0) .--> u is Relation-like the carrier of SCM+FSA -defined {(fsloc 0)} -defined bool [:NAT,INT:] -valued bool [:NAT,INT:] -valued trivial Function-like one-to-one constant the_Values_of SCM+FSA -compatible finite Function-yielding V120() set
{(fsloc 0)} --> u is Relation-like {(fsloc 0)} -defined {u} -valued bool [:NAT,INT:] -valued non empty Function-like constant finite total V43({(fsloc 0)},{u}) Function-yielding V120() Element of bool [:{(fsloc 0)},{u}:]
{u} is non empty trivial functional finite V35() 1 -element set
[:{(fsloc 0)},{u}:] is Relation-like finite set
bool [:{(fsloc 0)},{u}:] is finite V35() V121() V123() V124() set
p is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of REAL
q is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
(fsloc 0) .--> q is Relation-like the carrier of SCM+FSA -defined {(fsloc 0)} -defined bool [:NAT,INT:] -valued bool [:NAT,INT:] -valued trivial Function-like one-to-one constant the_Values_of SCM+FSA -compatible finite Function-yielding V120() set
{(fsloc 0)} --> q is Relation-like {(fsloc 0)} -defined {q} -valued bool [:NAT,INT:] -valued non empty Function-like constant finite total V43({(fsloc 0)},{q}) Function-yielding V120() Element of bool [:{(fsloc 0)},{q}:]
{q} is non empty trivial functional finite V35() 1 -element set
[:{(fsloc 0)},{q}:] is Relation-like finite set
bool [:{(fsloc 0)},{q}:] is finite V35() V121() V123() V124() set
[f,((fsloc 0) .--> q)] is set
{f,((fsloc 0) .--> q)} is non empty finite set
{{f,((fsloc 0) .--> q)},{f}} is non empty finite V35() V67() V68() set
s is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
(fsloc 0) .--> s is Relation-like the carrier of SCM+FSA -defined {(fsloc 0)} -defined bool [:NAT,INT:] -valued bool [:NAT,INT:] -valued trivial Function-like one-to-one constant the_Values_of SCM+FSA -compatible finite Function-yielding V120() set
{(fsloc 0)} is non empty trivial finite 1 -element set
{(fsloc 0)} --> s is Relation-like {(fsloc 0)} -defined {s} -valued bool [:NAT,INT:] -valued non empty Function-like constant finite total V43({(fsloc 0)},{s}) Function-yielding V120() Element of bool [:{(fsloc 0)},{s}:]
{s} is non empty trivial functional finite V35() 1 -element set
[:{(fsloc 0)},{s}:] is Relation-like finite set
bool [:{(fsloc 0)},{s}:] is finite V35() V121() V123() V124() set
() . ((fsloc 0) .--> s) is set
f is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of REAL
u is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
(fsloc 0) .--> u is Relation-like the carrier of SCM+FSA -defined {(fsloc 0)} -defined bool [:NAT,INT:] -valued bool [:NAT,INT:] -valued trivial Function-like one-to-one constant the_Values_of SCM+FSA -compatible finite Function-yielding V120() set
{(fsloc 0)} --> u is Relation-like {(fsloc 0)} -defined {u} -valued bool [:NAT,INT:] -valued non empty Function-like constant finite total V43({(fsloc 0)},{u}) Function-yielding V120() Element of bool [:{(fsloc 0)},{u}:]
{u} is non empty trivial functional finite V35() 1 -element set
[:{(fsloc 0)},{u}:] is Relation-like finite set
bool [:{(fsloc 0)},{u}:] is finite V35() V121() V123() V124() set
[((fsloc 0) .--> s),((fsloc 0) .--> u)] is set
{((fsloc 0) .--> s),((fsloc 0) .--> u)} is non empty functional finite V35() set
{((fsloc 0) .--> s)} is non empty trivial functional finite V35() 1 -element set
{{((fsloc 0) .--> s),((fsloc 0) .--> u)},{((fsloc 0) .--> s)}} is non empty finite V35() V67() V68() set
s is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
(s) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total 0 -started set
s +* (Initialize ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total 0 -started set
s +* ((intloc 0) .--> 1) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
Initialize (s +* ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total 0 -started set
(s +* ((intloc 0) .--> 1)) +* (Start-At (0,SCM+FSA)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total 0 -started set
dom ((intloc 0) .--> 1) is trivial finite set
((intloc 0)) is non empty trivial finite 1 -element Element of bool Int-Locations
f is Int-like () Element of the carrier of SCM+FSA
dom (Start-At (0,SCM+FSA)) is non empty finite set
(s) . f is ext-real V27() V28() integer set
(s +* ((intloc 0) .--> 1)) . f is ext-real V27() V28() integer set
s . f is ext-real V27() V28() integer set
f is FinSeq-Location
(s) . f is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
(s +* ((intloc 0) .--> 1)) . f is set
s . f is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT