:: SCMFSA_4 semantic presentation

REAL is non empty V5() V27() V66() set
NAT is non empty V5() V20() V21() V22() V27() V60() V61() V66() Element of K32(REAL)
K32(REAL) is set
SCM+FSA is non empty V84(3) IC-Ins-separated strict V92(3) with_explicit_jumps IC-relocable AMI-Struct over 3
3 is non empty V17() V18() V19() V20() V21() V22() V26() V62() integer V65() V97() Element of NAT
the U1 of SCM+FSA is set
NAT is non empty V5() V20() V21() V22() V27() V60() V61() V66() set
K32(NAT) is set
K32(NAT) is set
9 is non empty V17() V18() V19() V20() V21() V22() V26() V62() integer V65() V97() Element of NAT
K114(9) is V60() Element of K32(NAT)
Int-Locations is set
K193() is set
K32(K193()) is set
2 is non empty V17() V18() V19() V20() V21() V22() V26() V62() integer V65() V97() Element of NAT
K33(K193(),2) is Relation-like set
K32(K33(K193(),2)) is set
K195() is Relation-like K193() -defined 2 -valued Function-like V39(K193(),2) Element of K32(K33(K193(),2))
K196() is Relation-like 2 -defined Function-like total set
K195() * K196() is Relation-like K193() -defined Function-like set
K168((K195() * K196())) is functional V58() V59() set
K187() is non empty set
K140(K168((K195() * K196())),K168((K195() * K196()))) is set
K33(K187(),K140(K168((K195() * K196())),K168((K195() * K196())))) is Relation-like set
K32(K33(K187(),K140(K168((K195() * K196())),K168((K195() * K196()))))) is set
SCM is non empty V84(2) IC-Ins-separated strict strict V92(2) with_explicit_jumps IC-relocable relocable V129(2) V130(2) AMI-Struct over 2
K477(NAT,K193()) is Element of K193()
K201() is Relation-like K187() -defined K140(K168((K195() * K196())),K168((K195() * K196()))) -valued Function-like V39(K187(),K140(K168((K195() * K196())),K168((K195() * K196())))) Element of K32(K33(K187(),K140(K168((K195() * K196())),K168((K195() * K196())))))
AMI-Struct(# K193(),K477(NAT,K193()),K187(),K195(),K196(),K201() #) is strict AMI-Struct over 2
the InstructionsF of SCM is non empty Relation-like standard-ins V74() J/A-independent V77() set
the U1 of SCM is set
K281(2,SCM) is Relation-like non-empty the U1 of SCM -defined Function-like total set
the Object-Kind of SCM is Relation-like the U1 of SCM -defined 2 -valued Function-like V39( the U1 of SCM,2) Element of K32(K33( the U1 of SCM,2))
K33( the U1 of SCM,2) is Relation-like set
K32(K33( the U1 of SCM,2)) is set
the U7 of SCM is Relation-like 2 -defined Function-like total set
the Object-Kind of SCM * the U7 of SCM is Relation-like the U1 of SCM -defined Function-like set
K32( the U1 of SCM+FSA) is set
the InstructionsF of SCM+FSA is non empty Relation-like standard-ins V74() J/A-independent V77() set
INT is non empty V5() V27() V66() set
COMPLEX is non empty V5() V27() V66() set
RAT is non empty V5() V27() V66() set
1 is non empty V17() V18() V19() V20() V21() V22() V26() V62() integer V65() V97() Element of NAT
{} is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V17() V18() V19() V20() V21() V22() V24() V25() V26() V27() V28() V31() FinSequence-like FinSubsequence-like FinSequence-membered V57() V60() V62() integer V95() V96() V97() V100() V101() V102() V103() set
K281(3,SCM+FSA) is Relation-like non-empty the U1 of SCM+FSA -defined Function-like total set
the Object-Kind of SCM+FSA is Relation-like the U1 of SCM+FSA -defined 3 -valued Function-like V39( the U1 of SCM+FSA,3) Element of K32(K33( the U1 of SCM+FSA,3))
K33( the U1 of SCM+FSA,3) is Relation-like set
K32(K33( the U1 of SCM+FSA,3)) is set
the U7 of SCM+FSA is Relation-like 3 -defined Function-like total set
the Object-Kind of SCM+FSA * the U7 of SCM+FSA is Relation-like the U1 of SCM+FSA -defined Function-like set
0 is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V17() V18() V19() V20() V21() V22() V24() V25() V26() V27() V28() V31() FinSequence-like FinSubsequence-like FinSequence-membered V57() V60() V62() integer V95() V96() V97() V100() V101() V102() V103() Element of NAT
12 is non empty V17() V18() V19() V20() V21() V22() V26() V62() integer V65() V97() Element of NAT
4 is non empty V17() V18() V19() V20() V21() V22() V26() V62() integer V65() V97() Element of NAT
5 is non empty V17() V18() V19() V20() V21() V22() V26() V62() integer V65() V97() Element of NAT
6 is non empty V17() V18() V19() V20() V21() V22() V26() V62() integer V65() V97() Element of NAT
7 is non empty V17() V18() V19() V20() V21() V22() V26() V62() integer V65() V97() Element of NAT
8 is non empty V17() V18() V19() V20() V21() V22() V26() V62() integer V65() V97() Element of NAT
10 is non empty V17() V18() V19() V20() V21() V22() V26() V62() integer V65() V97() Element of NAT
11 is non empty V17() V18() V19() V20() V21() V22() V26() V62() integer V65() V97() Element of NAT
IC is Element of the U1 of SCM+FSA
halt SCM+FSA is ins-loc-free V91(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
halt the InstructionsF of SCM+FSA is ins-loc-free with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
[0,{},{}] is V1() V2() set
[0,{}] is V1() set
{0,{}} is non empty functional V27() V31() V60() set
{0} is non empty functional V27() V31() V58() V60() set
{{0,{}},{0}} is non empty V27() V31() V60() V65() V66() set
[[0,{}],{}] is V1() set
Seg 1 is non empty V27() V34(1) V60() Element of K32(NAT)
{1} is non empty V27() V60() V65() V66() set
Seg 2 is non empty V27() V34(2) V60() Element of K32(NAT)
{1,2} is non empty V27() V60() V65() V66() set
k is V64() Element of the U1 of SCM+FSA
i is V64() Element of the U1 of SCM+FSA
k := i is V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
<*k,i*> is non empty Relation-like NAT -defined Function-like V27() V34(2) FinSequence-like FinSubsequence-like V60() set
[1,{},<*k,i*>] is V1() V2() set
[1,{}] is V1() set
{1,{}} is non empty V27() V60() set
{{1,{}},{1}} is non empty V27() V31() V60() V65() V66() set
[[1,{}],<*k,i*>] is V1() set
{[1,{}],<*k,i*>} is non empty V27() V60() set
{[1,{}]} is non empty Relation-like Function-like V27() V60() set
{{[1,{}],<*k,i*>},{[1,{}]}} is non empty V27() V31() V60() V65() V66() set
JumpPart (k := i) is Relation-like NAT -defined NAT -valued RAT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() V103() set
K13((k := i)) is set
AddressPart K13((k := i)) is set
AddTo (k,i) is V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
<*k,i*> is non empty Relation-like NAT -defined Function-like V27() V34(2) FinSequence-like FinSubsequence-like V60() set
[2,{},<*k,i*>] is V1() V2() set
[2,{}] is V1() set
{2,{}} is non empty V27() V60() set
{2} is non empty V27() V60() V65() V66() set
{{2,{}},{2}} is non empty V27() V31() V60() V65() V66() set
[[2,{}],<*k,i*>] is V1() set
{[2,{}],<*k,i*>} is non empty V27() V60() set
{[2,{}]} is non empty Relation-like Function-like V27() V60() set
{{[2,{}],<*k,i*>},{[2,{}]}} is non empty V27() V31() V60() V65() V66() set
JumpPart (AddTo (k,i)) is Relation-like NAT -defined NAT -valued RAT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() V103() set
K13((AddTo (k,i))) is set
AddressPart K13((AddTo (k,i))) is set
SubFrom (k,i) is V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
<*k,i*> is non empty Relation-like NAT -defined Function-like V27() V34(2) FinSequence-like FinSubsequence-like V60() set
[3,{},<*k,i*>] is V1() V2() set
[3,{}] is V1() set
{3,{}} is non empty V27() V60() set
{3} is non empty V27() V60() V65() V66() set
{{3,{}},{3}} is non empty V27() V31() V60() V65() V66() set
[[3,{}],<*k,i*>] is V1() set
{[3,{}],<*k,i*>} is non empty V27() V60() set
{[3,{}]} is non empty Relation-like Function-like V27() V60() set
{{[3,{}],<*k,i*>},{[3,{}]}} is non empty V27() V31() V60() V65() V66() set
JumpPart (SubFrom (k,i)) is Relation-like NAT -defined NAT -valued RAT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() V103() set
K13((SubFrom (k,i))) is set
AddressPart K13((SubFrom (k,i))) is set
MultBy (k,i) is V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
<*k,i*> is non empty Relation-like NAT -defined Function-like V27() V34(2) FinSequence-like FinSubsequence-like V60() set
[4,{},<*k,i*>] is V1() V2() set
[4,{}] is V1() set
{4,{}} is non empty V27() V60() set
{4} is non empty V27() V60() V65() V66() set
{{4,{}},{4}} is non empty V27() V31() V60() V65() V66() set
[[4,{}],<*k,i*>] is V1() set
{[4,{}],<*k,i*>} is non empty V27() V60() set
{[4,{}]} is non empty Relation-like Function-like V27() V60() set
{{[4,{}],<*k,i*>},{[4,{}]}} is non empty V27() V31() V60() V65() V66() set
JumpPart (MultBy (k,i)) is Relation-like NAT -defined NAT -valued RAT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() V103() set
K13((MultBy (k,i))) is set
AddressPart K13((MultBy (k,i))) is set
Divide (k,i) is V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
<*k,i*> is non empty Relation-like NAT -defined Function-like V27() V34(2) FinSequence-like FinSubsequence-like V60() set
[5,{},<*k,i*>] is V1() V2() set
[5,{}] is V1() set
{5,{}} is non empty V27() V60() set
{5} is non empty V27() V60() V65() V66() set
{{5,{}},{5}} is non empty V27() V31() V60() V65() V66() set
[[5,{}],<*k,i*>] is V1() set
{[5,{}],<*k,i*>} is non empty V27() V60() set
{[5,{}]} is non empty Relation-like Function-like V27() V60() set
{{[5,{}],<*k,i*>},{[5,{}]}} is non empty V27() V31() V60() V65() V66() set
JumpPart (Divide (k,i)) is Relation-like NAT -defined NAT -valued RAT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() V103() set
K13((Divide (k,i))) is set
AddressPart K13((Divide (k,i))) is set
i is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
goto i is V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
SCM-goto i is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of SCM
<*i*> is non empty Relation-like NAT -defined Function-like V27() V34(1) FinSequence-like FinSubsequence-like V60() set
[6,<*i*>,{}] is V1() V2() set
[6,<*i*>] is V1() set
{6,<*i*>} is non empty V27() V60() V65() V66() set
{6} is non empty V27() V60() V65() V66() set
{{6,<*i*>},{6}} is non empty V27() V31() V60() V65() V66() set
[[6,<*i*>],{}] is V1() set
k is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
IncAddr ((goto i),k) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
i + k is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
goto (i + k) is V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
SCM-goto (i + k) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of SCM
<*(i + k)*> is non empty Relation-like NAT -defined Function-like V27() V34(1) FinSequence-like FinSubsequence-like V60() set
[6,<*(i + k)*>,{}] is V1() V2() set
[6,<*(i + k)*>] is V1() set
{6,<*(i + k)*>} is non empty V27() V60() V65() V66() set
{{6,<*(i + k)*>},{6}} is non empty V27() V31() V60() V65() V66() set
[[6,<*(i + k)*>],{}] is V1() set
InsCode (IncAddr ((goto i),k)) is V17() V20() V21() V22() V26() V62() integer V97() Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
K23( the InstructionsF of SCM+FSA) is set
proj1 the InstructionsF of SCM+FSA is non empty set
proj1 (proj1 the InstructionsF of SCM+FSA) is set
K13((IncAddr ((goto i),k))) is set
K13(K13((IncAddr ((goto i),k)))) is set
InsCode (goto i) is V17() V20() V21() V22() V26() V62() integer V97() Element of InsCodes the InstructionsF of SCM+FSA
K13((goto i)) is set
K13(K13((goto i))) is set
InsCode (goto (i + k)) is V17() V20() V21() V22() V26() V62() integer V97() Element of InsCodes the InstructionsF of SCM+FSA
K13((goto (i + k))) is set
K13(K13((goto (i + k)))) is set
AddressPart (IncAddr ((goto i),k)) is Relation-like NAT -defined Function-like V27() FinSequence-like FinSubsequence-like V60() set
AddressPart (goto i) is Relation-like NAT -defined Function-like V27() FinSequence-like FinSubsequence-like V60() set
AddressPart (goto (i + k)) is Relation-like NAT -defined Function-like V27() FinSequence-like FinSubsequence-like V60() set
JumpPart (IncAddr ((goto i),k)) is Relation-like NAT -defined NAT -valued RAT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() V103() set
AddressPart K13((IncAddr ((goto i),k))) is set
JumpPart (goto i) is Relation-like NAT -defined NAT -valued RAT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() V103() set
AddressPart K13((goto i)) is set
k + (JumpPart (goto i)) is Relation-like NAT -defined RAT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() V103() set
JumpPart (goto (i + k)) is Relation-like NAT -defined NAT -valued RAT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() V103() set
AddressPart K13((goto (i + k))) is set
dom (JumpPart (IncAddr ((goto i),k))) is V27() V60() V115() Element of K32(NAT)
dom (JumpPart (goto (i + k))) is V27() V60() V115() Element of K32(NAT)
proj1 (JumpPart (IncAddr ((goto i),k))) is V27() V60() V115() set
<*i*> is non empty Relation-like NAT -defined NAT -valued Function-like V27() V34(1) FinSequence-like FinSubsequence-like V60() V100() V101() V102() V103() FinSequence of NAT
<*(i + k)*> is non empty Relation-like NAT -defined NAT -valued Function-like V27() V34(1) FinSequence-like FinSubsequence-like V60() V100() V101() V102() V103() FinSequence of NAT
da is set
(JumpPart (IncAddr ((goto i),k))) . da is V17() V20() V21() V22() V26() V62() integer V97() V99() set
(JumpPart (goto (i + k))) . da is V17() V20() V21() V22() V26() V62() integer V97() V99() set
dom <*(i + k)*> is non empty V27() V60() V115() Element of K32(NAT)
(JumpPart (goto i)) . da is V17() V20() V21() V22() V26() V62() integer V97() V99() set
k + ((JumpPart (goto i)) . da) is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
i is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
k is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
i + k is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
da is V64() Element of the U1 of SCM+FSA
da =0_goto i is V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IncAddr ((da =0_goto i),k) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
da =0_goto (i + k) is V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
<*i*> is non empty Relation-like NAT -defined NAT -valued Function-like V27() V34(1) FinSequence-like FinSubsequence-like V60() V100() V101() V102() V103() FinSequence of NAT
<*da*> is non empty Relation-like NAT -defined Function-like V27() V34(1) FinSequence-like FinSubsequence-like V60() set
[7,<*i*>,<*da*>] is V1() V2() set
[7,<*i*>] is V1() set
{7,<*i*>} is non empty V27() V60() V65() V66() set
{7} is non empty V27() V60() V65() V66() set
{{7,<*i*>},{7}} is non empty V27() V31() V60() V65() V66() set
[[7,<*i*>],<*da*>] is V1() set
{[7,<*i*>],<*da*>} is non empty V27() V60() set
{[7,<*i*>]} is non empty Relation-like Function-like V27() V60() set
{{[7,<*i*>],<*da*>},{[7,<*i*>]}} is non empty V27() V31() V60() V65() V66() set
<*(i + k)*> is non empty Relation-like NAT -defined NAT -valued Function-like V27() V34(1) FinSequence-like FinSubsequence-like V60() V100() V101() V102() V103() FinSequence of NAT
[7,<*(i + k)*>,<*da*>] is V1() V2() set
[7,<*(i + k)*>] is V1() set
{7,<*(i + k)*>} is non empty V27() V60() V65() V66() set
{{7,<*(i + k)*>},{7}} is non empty V27() V31() V60() V65() V66() set
[[7,<*(i + k)*>],<*da*>] is V1() set
{[7,<*(i + k)*>],<*da*>} is non empty V27() V60() set
{[7,<*(i + k)*>]} is non empty Relation-like Function-like V27() V60() set
{{[7,<*(i + k)*>],<*da*>},{[7,<*(i + k)*>]}} is non empty V27() V31() V60() V65() V66() set
InsCode (IncAddr ((da =0_goto i),k)) is V17() V20() V21() V22() V26() V62() integer V97() Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
K23( the InstructionsF of SCM+FSA) is set
proj1 the InstructionsF of SCM+FSA is non empty set
proj1 (proj1 the InstructionsF of SCM+FSA) is set
K13((IncAddr ((da =0_goto i),k))) is set
K13(K13((IncAddr ((da =0_goto i),k)))) is set
InsCode (da =0_goto i) is V17() V20() V21() V22() V26() V62() integer V97() Element of InsCodes the InstructionsF of SCM+FSA
K13((da =0_goto i)) is set
K13(K13((da =0_goto i))) is set
InsCode (da =0_goto (i + k)) is V17() V20() V21() V22() V26() V62() integer V97() Element of InsCodes the InstructionsF of SCM+FSA
K13((da =0_goto (i + k))) is set
K13(K13((da =0_goto (i + k)))) is set
AddressPart (IncAddr ((da =0_goto i),k)) is Relation-like NAT -defined Function-like V27() FinSequence-like FinSubsequence-like V60() set
AddressPart (da =0_goto i) is Relation-like NAT -defined Function-like V27() FinSequence-like FinSubsequence-like V60() set
AddressPart (da =0_goto (i + k)) is Relation-like NAT -defined Function-like V27() FinSequence-like FinSubsequence-like V60() set
JumpPart (IncAddr ((da =0_goto i),k)) is Relation-like NAT -defined NAT -valued RAT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() V103() set
AddressPart K13((IncAddr ((da =0_goto i),k))) is set
JumpPart (da =0_goto i) is Relation-like NAT -defined NAT -valued RAT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() V103() set
AddressPart K13((da =0_goto i)) is set
k + (JumpPart (da =0_goto i)) is Relation-like NAT -defined RAT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() V103() set
JumpPart (da =0_goto (i + k)) is Relation-like NAT -defined NAT -valued RAT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() V103() set
AddressPart K13((da =0_goto (i + k))) is set
dom (JumpPart (IncAddr ((da =0_goto i),k))) is V27() V60() V115() Element of K32(NAT)
dom (JumpPart (da =0_goto (i + k))) is V27() V60() V115() Element of K32(NAT)
proj1 (JumpPart (IncAddr ((da =0_goto i),k))) is V27() V60() V115() set
f is set
(JumpPart (IncAddr ((da =0_goto i),k))) . f is V17() V20() V21() V22() V26() V62() integer V97() V99() set
(JumpPart (da =0_goto (i + k))) . f is V17() V20() V21() V22() V26() V62() integer V97() V99() set
dom <*(i + k)*> is non empty V27() V60() V115() Element of K32(NAT)
(JumpPart (da =0_goto i)) . f is V17() V20() V21() V22() V26() V62() integer V97() V99() set
k + ((JumpPart (da =0_goto i)) . f) is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
i is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
k is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
i + k is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
da is V64() Element of the U1 of SCM+FSA
da >0_goto i is V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IncAddr ((da >0_goto i),k) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
da >0_goto (i + k) is V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
<*i*> is non empty Relation-like NAT -defined NAT -valued Function-like V27() V34(1) FinSequence-like FinSubsequence-like V60() V100() V101() V102() V103() FinSequence of NAT
<*da*> is non empty Relation-like NAT -defined Function-like V27() V34(1) FinSequence-like FinSubsequence-like V60() set
[8,<*i*>,<*da*>] is V1() V2() set
[8,<*i*>] is V1() set
{8,<*i*>} is non empty V27() V60() V65() V66() set
{8} is non empty V27() V60() V65() V66() set
{{8,<*i*>},{8}} is non empty V27() V31() V60() V65() V66() set
[[8,<*i*>],<*da*>] is V1() set
{[8,<*i*>],<*da*>} is non empty V27() V60() set
{[8,<*i*>]} is non empty Relation-like Function-like V27() V60() set
{{[8,<*i*>],<*da*>},{[8,<*i*>]}} is non empty V27() V31() V60() V65() V66() set
<*(i + k)*> is non empty Relation-like NAT -defined NAT -valued Function-like V27() V34(1) FinSequence-like FinSubsequence-like V60() V100() V101() V102() V103() FinSequence of NAT
[8,<*(i + k)*>,<*da*>] is V1() V2() set
[8,<*(i + k)*>] is V1() set
{8,<*(i + k)*>} is non empty V27() V60() V65() V66() set
{{8,<*(i + k)*>},{8}} is non empty V27() V31() V60() V65() V66() set
[[8,<*(i + k)*>],<*da*>] is V1() set
{[8,<*(i + k)*>],<*da*>} is non empty V27() V60() set
{[8,<*(i + k)*>]} is non empty Relation-like Function-like V27() V60() set
{{[8,<*(i + k)*>],<*da*>},{[8,<*(i + k)*>]}} is non empty V27() V31() V60() V65() V66() set
InsCode (IncAddr ((da >0_goto i),k)) is V17() V20() V21() V22() V26() V62() integer V97() Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
K23( the InstructionsF of SCM+FSA) is set
proj1 the InstructionsF of SCM+FSA is non empty set
proj1 (proj1 the InstructionsF of SCM+FSA) is set
K13((IncAddr ((da >0_goto i),k))) is set
K13(K13((IncAddr ((da >0_goto i),k)))) is set
InsCode (da >0_goto i) is V17() V20() V21() V22() V26() V62() integer V97() Element of InsCodes the InstructionsF of SCM+FSA
K13((da >0_goto i)) is set
K13(K13((da >0_goto i))) is set
InsCode (da >0_goto (i + k)) is V17() V20() V21() V22() V26() V62() integer V97() Element of InsCodes the InstructionsF of SCM+FSA
K13((da >0_goto (i + k))) is set
K13(K13((da >0_goto (i + k)))) is set
AddressPart (IncAddr ((da >0_goto i),k)) is Relation-like NAT -defined Function-like V27() FinSequence-like FinSubsequence-like V60() set
AddressPart (da >0_goto i) is Relation-like NAT -defined Function-like V27() FinSequence-like FinSubsequence-like V60() set
AddressPart (da >0_goto (i + k)) is Relation-like NAT -defined Function-like V27() FinSequence-like FinSubsequence-like V60() set
JumpPart (IncAddr ((da >0_goto i),k)) is Relation-like NAT -defined NAT -valued RAT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() V103() set
AddressPart K13((IncAddr ((da >0_goto i),k))) is set
JumpPart (da >0_goto i) is Relation-like NAT -defined NAT -valued RAT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() V103() set
AddressPart K13((da >0_goto i)) is set
k + (JumpPart (da >0_goto i)) is Relation-like NAT -defined RAT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() V103() set
JumpPart (da >0_goto (i + k)) is Relation-like NAT -defined NAT -valued RAT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() V103() set
AddressPart K13((da >0_goto (i + k))) is set
dom (JumpPart (IncAddr ((da >0_goto i),k))) is V27() V60() V115() Element of K32(NAT)
dom (JumpPart (da >0_goto (i + k))) is V27() V60() V115() Element of K32(NAT)
proj1 (JumpPart (IncAddr ((da >0_goto i),k))) is V27() V60() V115() set
f is set
(JumpPart (IncAddr ((da >0_goto i),k))) . f is V17() V20() V21() V22() V26() V62() integer V97() V99() set
(JumpPart (da >0_goto (i + k))) . f is V17() V20() V21() V22() V26() V62() integer V97() V99() set
dom <*(i + k)*> is non empty V27() V60() V115() Element of K32(NAT)
(JumpPart (da >0_goto i)) . f is V17() V20() V21() V22() V26() V62() integer V97() V99() set
k + ((JumpPart (da >0_goto i)) . f) is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
i is V64() Element of the U1 of SCM+FSA
k is V64() Element of the U1 of SCM+FSA
da is FinSeq-Location
i := (da,k) is V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
<*i,da,k*> is non empty Relation-like NAT -defined Function-like V27() V34(3) FinSequence-like FinSubsequence-like V60() set
[9,{},<*i,da,k*>] is V1() V2() set
[9,{}] is V1() set
{9,{}} is non empty V27() V60() set
{9} is non empty V27() V60() V65() V66() set
{{9,{}},{9}} is non empty V27() V31() V60() V65() V66() set
[[9,{}],<*i,da,k*>] is V1() set
{[9,{}],<*i,da,k*>} is non empty V27() V60() set
{[9,{}]} is non empty Relation-like Function-like V27() V60() set
{{[9,{}],<*i,da,k*>},{[9,{}]}} is non empty V27() V31() V60() V65() V66() set
JumpPart (i := (da,k)) is Relation-like NAT -defined NAT -valued RAT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() V103() set
K13((i := (da,k))) is set
AddressPart K13((i := (da,k))) is set
(da,k) := i is V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
[10,{},<*i,da,k*>] is V1() V2() set
[10,{}] is V1() set
{10,{}} is non empty V27() V60() set
{10} is non empty V27() V60() V65() V66() set
{{10,{}},{10}} is non empty V27() V31() V60() V65() V66() set
[[10,{}],<*i,da,k*>] is V1() set
{[10,{}],<*i,da,k*>} is non empty V27() V60() set
{[10,{}]} is non empty Relation-like Function-like V27() V60() set
{{[10,{}],<*i,da,k*>},{[10,{}]}} is non empty V27() V31() V60() V65() V66() set
JumpPart ((da,k) := i) is Relation-like NAT -defined NAT -valued RAT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() V103() set
K13(((da,k) := i)) is set
AddressPart K13(((da,k) := i)) is set
k is V64() Element of the U1 of SCM+FSA
i is FinSeq-Location
k :=len i is V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
<*k,i*> is non empty Relation-like NAT -defined Function-like V27() V34(2) FinSequence-like FinSubsequence-like V60() set
[11,{},<*k,i*>] is V1() V2() set
[11,{}] is V1() set
{11,{}} is non empty V27() V60() set
{11} is non empty V27() V60() V65() V66() set
{{11,{}},{11}} is non empty V27() V31() V60() V65() V66() set
[[11,{}],<*k,i*>] is V1() set
{[11,{}],<*k,i*>} is non empty V27() V60() set
{[11,{}]} is non empty Relation-like Function-like V27() V60() set
{{[11,{}],<*k,i*>},{[11,{}]}} is non empty V27() V31() V60() V65() V66() set
JumpPart (k :=len i) is Relation-like NAT -defined NAT -valued RAT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() V103() set
K13((k :=len i)) is set
AddressPart K13((k :=len i)) is set
i :=<0,...,0> k is V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
[12,{},<*k,i*>] is V1() V2() set
[12,{}] is V1() set
{12,{}} is non empty V27() V60() set
{12} is non empty V27() V60() V65() V66() set
{{12,{}},{12}} is non empty V27() V31() V60() V65() V66() set
[[12,{}],<*k,i*>] is V1() set
{[12,{}],<*k,i*>} is non empty V27() V60() set
{[12,{}]} is non empty Relation-like Function-like V27() V60() set
{{[12,{}],<*k,i*>},{[12,{}]}} is non empty V27() V31() V60() V65() V66() set
JumpPart (i :=<0,...,0> k) is Relation-like NAT -defined NAT -valued RAT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() V103() set
K13((i :=<0,...,0> k)) is set
AddressPart K13((i :=<0,...,0> k)) is set
k is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
i is V17() V20() V21() V22() V26() V62() integer V97() set
da is V17() V20() V21() V22() V26() V62() integer V97() set
i + da is V17() V62() integer V97() set
IncAddr (k,(i + da)) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IncAddr (k,i) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
f is Relation-like the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible total set
IncIC (f,da) is Relation-like the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible total set
IC f is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
f . (IC ) is set
(IC f) + da is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
Start-At (((IC f) + da),SCM+FSA) is non empty Relation-like the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible V27() V60() (IC f) + da -started set
K314((IC ),((IC f) + da)) is V5() Relation-like {(IC )} -defined NAT -valued INT -valued RAT -valued Function-like one-to-one constant V27() V60() V100() V101() V102() V103() V104() V105() V106() V107() set
{(IC )} is non empty V27() V60() set
K305({(IC )},((IC f) + da)) is non empty Relation-like {(IC )} -defined NAT -valued INT -valued RAT -valued {((IC f) + da)} -valued Function-like constant V27() total V39({(IC )},{((IC f) + da)}) V60() V100() V101() V102() V103() Element of K32(K33({(IC )},{((IC f) + da)}))
{((IC f) + da)} is non empty V27() V60() set
K33({(IC )},{((IC f) + da)}) is Relation-like V27() V60() set
K32(K33({(IC )},{((IC f) + da)})) is V27() V31() V60() set
f +* (Start-At (((IC f) + da),SCM+FSA)) is non empty Relation-like the U1 of SCM+FSA -defined the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible K281(3,SCM+FSA) -compatible total (IC f) + da -started set
Exec ((IncAddr (k,(i + da))),(IncIC (f,da))) is Relation-like the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible total set
K168(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)) is functional V58() V59() set
K140(K168(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K168(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like the InstructionsF of SCM+FSA -defined K140(K168(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K168(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) -valued Function-like V39( the InstructionsF of SCM+FSA,K140(K168(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K168(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) Element of K32(K33( the InstructionsF of SCM+FSA,K140(K168(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K168(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))))
K33( the InstructionsF of SCM+FSA,K140(K168(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K168(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) is Relation-like set
K32(K33( the InstructionsF of SCM+FSA,K140(K168(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K168(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))))) is set
the Execution of SCM+FSA . (IncAddr (k,(i + da))) is Element of K140(K168(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K168(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
( the Execution of SCM+FSA . (IncAddr (k,(i + da)))) . (IncIC (f,da)) is set
Exec ((IncAddr (k,i)),f) is Relation-like the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible total set
the Execution of SCM+FSA . (IncAddr (k,i)) is Element of K140(K168(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K168(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
( the Execution of SCM+FSA . (IncAddr (k,i))) . f is set
IncIC ((Exec ((IncAddr (k,i)),f)),da) is Relation-like the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible total set
IC (Exec ((IncAddr (k,i)),f)) is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
(Exec ((IncAddr (k,i)),f)) . (IC ) is set
(IC (Exec ((IncAddr (k,i)),f))) + da is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
Start-At (((IC (Exec ((IncAddr (k,i)),f))) + da),SCM+FSA) is non empty Relation-like the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible V27() V60() (IC (Exec ((IncAddr (k,i)),f))) + da -started set
K314((IC ),((IC (Exec ((IncAddr (k,i)),f))) + da)) is V5() Relation-like {(IC )} -defined NAT -valued INT -valued RAT -valued Function-like one-to-one constant V27() V60() V100() V101() V102() V103() V104() V105() V106() V107() set
K305({(IC )},((IC (Exec ((IncAddr (k,i)),f))) + da)) is non empty Relation-like {(IC )} -defined NAT -valued INT -valued RAT -valued {((IC (Exec ((IncAddr (k,i)),f))) + da)} -valued Function-like constant V27() total V39({(IC )},{((IC (Exec ((IncAddr (k,i)),f))) + da)}) V60() V100() V101() V102() V103() Element of K32(K33({(IC )},{((IC (Exec ((IncAddr (k,i)),f))) + da)}))
{((IC (Exec ((IncAddr (k,i)),f))) + da)} is non empty V27() V60() set
K33({(IC )},{((IC (Exec ((IncAddr (k,i)),f))) + da)}) is Relation-like V27() V60() set
K32(K33({(IC )},{((IC (Exec ((IncAddr (k,i)),f))) + da)})) is V27() V31() V60() set
(Exec ((IncAddr (k,i)),f)) +* (Start-At (((IC (Exec ((IncAddr (k,i)),f))) + da),SCM+FSA)) is non empty Relation-like the U1 of SCM+FSA -defined the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible K281(3,SCM+FSA) -compatible total (IC (Exec ((IncAddr (k,i)),f))) + da -started set
f is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
IncIC ((Exec ((IncAddr (k,i)),f)),f) is Relation-like the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible total set
(IC (Exec ((IncAddr (k,i)),f))) + f is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
Start-At (((IC (Exec ((IncAddr (k,i)),f))) + f),SCM+FSA) is non empty Relation-like the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible V27() V60() (IC (Exec ((IncAddr (k,i)),f))) + f -started set
K314((IC ),((IC (Exec ((IncAddr (k,i)),f))) + f)) is V5() Relation-like {(IC )} -defined NAT -valued INT -valued RAT -valued Function-like one-to-one constant V27() V60() V100() V101() V102() V103() V104() V105() V106() V107() set
K305({(IC )},((IC (Exec ((IncAddr (k,i)),f))) + f)) is non empty Relation-like {(IC )} -defined NAT -valued INT -valued RAT -valued {((IC (Exec ((IncAddr (k,i)),f))) + f)} -valued Function-like constant V27() total V39({(IC )},{((IC (Exec ((IncAddr (k,i)),f))) + f)}) V60() V100() V101() V102() V103() Element of K32(K33({(IC )},{((IC (Exec ((IncAddr (k,i)),f))) + f)}))
{((IC (Exec ((IncAddr (k,i)),f))) + f)} is non empty V27() V60() set
K33({(IC )},{((IC (Exec ((IncAddr (k,i)),f))) + f)}) is Relation-like V27() V60() set
K32(K33({(IC )},{((IC (Exec ((IncAddr (k,i)),f))) + f)})) is V27() V31() V60() set
(Exec ((IncAddr (k,i)),f)) +* (Start-At (((IC (Exec ((IncAddr (k,i)),f))) + f),SCM+FSA)) is non empty Relation-like the U1 of SCM+FSA -defined the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible K281(3,SCM+FSA) -compatible total (IC (Exec ((IncAddr (k,i)),f))) + f -started set
IC (IncIC ((Exec ((IncAddr (k,i)),f)),f)) is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
(IncIC ((Exec ((IncAddr (k,i)),f)),f)) . (IC ) is set
i + f is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
IncAddr (k,(i + f)) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IncIC (f,f) is Relation-like the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible total set
(IC f) + f is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
Start-At (((IC f) + f),SCM+FSA) is non empty Relation-like the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible V27() V60() (IC f) + f -started set
K314((IC ),((IC f) + f)) is V5() Relation-like {(IC )} -defined NAT -valued INT -valued RAT -valued Function-like one-to-one constant V27() V60() V100() V101() V102() V103() V104() V105() V106() V107() set
K305({(IC )},((IC f) + f)) is non empty Relation-like {(IC )} -defined NAT -valued INT -valued RAT -valued {((IC f) + f)} -valued Function-like constant V27() total V39({(IC )},{((IC f) + f)}) V60() V100() V101() V102() V103() Element of K32(K33({(IC )},{((IC f) + f)}))
{((IC f) + f)} is non empty V27() V60() set
K33({(IC )},{((IC f) + f)}) is Relation-like V27() V60() set
K32(K33({(IC )},{((IC f) + f)})) is V27() V31() V60() set
f +* (Start-At (((IC f) + f),SCM+FSA)) is non empty Relation-like the U1 of SCM+FSA -defined the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible K281(3,SCM+FSA) -compatible total (IC f) + f -started set
Exec ((IncAddr (k,(i + f))),(IncIC (f,f))) is Relation-like the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible total set
the Execution of SCM+FSA . (IncAddr (k,(i + f))) is Element of K140(K168(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K168(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
( the Execution of SCM+FSA . (IncAddr (k,(i + f)))) . (IncIC (f,f)) is set
IC (Exec ((IncAddr (k,(i + f))),(IncIC (f,f)))) is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
(Exec ((IncAddr (k,(i + f))),(IncIC (f,f)))) . (IC ) is set
InsCode k is V17() V20() V21() V22() V26() V62() integer V97() Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
K23( the InstructionsF of SCM+FSA) is set
proj1 the InstructionsF of SCM+FSA is non empty set
proj1 (proj1 the InstructionsF of SCM+FSA) is set
K13(k) is set
K13(K13(k)) is set
Exec (k,(IncIC (f,f))) is Relation-like the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible total set
the Execution of SCM+FSA . k is Element of K140(K168(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K168(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
( the Execution of SCM+FSA . k) . (IncIC (f,f)) is set
InsCode k is V17() V20() V21() V22() V26() V62() integer V97() Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
K23( the InstructionsF of SCM+FSA) is set
proj1 the InstructionsF of SCM+FSA is non empty set
proj1 (proj1 the InstructionsF of SCM+FSA) is set
K13(k) is set
K13(K13(k)) is set
da is V64() Element of the U1 of SCM+FSA
f is V64() Element of the U1 of SCM+FSA
da := f is ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
d is FinSeq-Location
(Exec ((IncAddr (k,(i + f))),(IncIC (f,f)))) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
Exec (k,(IncIC (f,f))) is Relation-like the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible total set
the Execution of SCM+FSA . k is Element of K140(K168(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K168(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
( the Execution of SCM+FSA . k) . (IncIC (f,f)) is set
(Exec (k,(IncIC (f,f)))) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(IncIC (f,f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
f . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
Exec (k,f) is Relation-like the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible total set
( the Execution of SCM+FSA . k) . f is set
(Exec (k,f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(Exec ((IncAddr (k,i)),f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(IncIC ((Exec ((IncAddr (k,i)),f)),f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
d is V64() Element of the U1 of SCM+FSA
(Exec ((IncAddr (k,(i + f))),(IncIC (f,f)))) . d is V17() V62() integer V97() set
(Exec (k,(IncIC (f,f)))) . d is V17() V62() integer V97() set
(IncIC (f,f)) . f is V17() V62() integer V97() set
f . f is V17() V62() integer V97() set
(Exec (k,f)) . d is V17() V62() integer V97() set
(Exec ((IncAddr (k,i)),f)) . d is V17() V62() integer V97() set
(IncIC ((Exec ((IncAddr (k,i)),f)),f)) . d is V17() V62() integer V97() set
d is V64() Element of the U1 of SCM+FSA
(Exec ((IncAddr (k,(i + f))),(IncIC (f,f)))) . d is V17() V62() integer V97() set
(Exec (k,(IncIC (f,f)))) . d is V17() V62() integer V97() set
(IncIC (f,f)) . d is V17() V62() integer V97() set
f . d is V17() V62() integer V97() set
(Exec (k,f)) . d is V17() V62() integer V97() set
(Exec ((IncAddr (k,i)),f)) . d is V17() V62() integer V97() set
(IncIC ((Exec ((IncAddr (k,i)),f)),f)) . d is V17() V62() integer V97() set
d is V64() Element of the U1 of SCM+FSA
InsCode k is V17() V20() V21() V22() V26() V62() integer V97() Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
K23( the InstructionsF of SCM+FSA) is set
proj1 the InstructionsF of SCM+FSA is non empty set
proj1 (proj1 the InstructionsF of SCM+FSA) is set
K13(k) is set
K13(K13(k)) is set
da is V64() Element of the U1 of SCM+FSA
f is V64() Element of the U1 of SCM+FSA
AddTo (da,f) is ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
d is FinSeq-Location
(Exec ((IncAddr (k,(i + f))),(IncIC (f,f)))) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
Exec (k,(IncIC (f,f))) is Relation-like the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible total set
the Execution of SCM+FSA . k is Element of K140(K168(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K168(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
( the Execution of SCM+FSA . k) . (IncIC (f,f)) is set
(Exec (k,(IncIC (f,f)))) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(IncIC (f,f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
f . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
Exec (k,f) is Relation-like the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible total set
( the Execution of SCM+FSA . k) . f is set
(Exec (k,f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(Exec ((IncAddr (k,i)),f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(IncIC ((Exec ((IncAddr (k,i)),f)),f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
d is V64() Element of the U1 of SCM+FSA
(Exec ((IncAddr (k,(i + f))),(IncIC (f,f)))) . d is V17() V62() integer V97() set
(Exec (k,(IncIC (f,f)))) . d is V17() V62() integer V97() set
(IncIC (f,f)) . da is V17() V62() integer V97() set
(IncIC (f,f)) . f is V17() V62() integer V97() set
((IncIC (f,f)) . da) + ((IncIC (f,f)) . f) is V17() V62() integer V97() set
f . da is V17() V62() integer V97() set
(f . da) + ((IncIC (f,f)) . f) is V17() V62() integer V97() set
f . f is V17() V62() integer V97() set
(f . da) + (f . f) is V17() V62() integer V97() set
(Exec (k,f)) . d is V17() V62() integer V97() set
(Exec ((IncAddr (k,i)),f)) . d is V17() V62() integer V97() set
(IncIC ((Exec ((IncAddr (k,i)),f)),f)) . d is V17() V62() integer V97() set
d is V64() Element of the U1 of SCM+FSA
(Exec ((IncAddr (k,(i + f))),(IncIC (f,f)))) . d is V17() V62() integer V97() set
(Exec (k,(IncIC (f,f)))) . d is V17() V62() integer V97() set
(IncIC (f,f)) . d is V17() V62() integer V97() set
f . d is V17() V62() integer V97() set
(Exec (k,f)) . d is V17() V62() integer V97() set
(Exec ((IncAddr (k,i)),f)) . d is V17() V62() integer V97() set
(IncIC ((Exec ((IncAddr (k,i)),f)),f)) . d is V17() V62() integer V97() set
d is V64() Element of the U1 of SCM+FSA
InsCode k is V17() V20() V21() V22() V26() V62() integer V97() Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
K23( the InstructionsF of SCM+FSA) is set
proj1 the InstructionsF of SCM+FSA is non empty set
proj1 (proj1 the InstructionsF of SCM+FSA) is set
K13(k) is set
K13(K13(k)) is set
da is V64() Element of the U1 of SCM+FSA
f is V64() Element of the U1 of SCM+FSA
SubFrom (da,f) is ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
d is FinSeq-Location
(Exec ((IncAddr (k,(i + f))),(IncIC (f,f)))) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
Exec (k,(IncIC (f,f))) is Relation-like the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible total set
the Execution of SCM+FSA . k is Element of K140(K168(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K168(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
( the Execution of SCM+FSA . k) . (IncIC (f,f)) is set
(Exec (k,(IncIC (f,f)))) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(IncIC (f,f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
f . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
Exec (k,f) is Relation-like the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible total set
( the Execution of SCM+FSA . k) . f is set
(Exec (k,f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(Exec ((IncAddr (k,i)),f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(IncIC ((Exec ((IncAddr (k,i)),f)),f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
d is V64() Element of the U1 of SCM+FSA
(Exec ((IncAddr (k,(i + f))),(IncIC (f,f)))) . d is V17() V62() integer V97() set
(Exec (k,(IncIC (f,f)))) . d is V17() V62() integer V97() set
(IncIC (f,f)) . da is V17() V62() integer V97() set
(IncIC (f,f)) . f is V17() V62() integer V97() set
((IncIC (f,f)) . da) - ((IncIC (f,f)) . f) is V17() V62() integer V97() set
f . da is V17() V62() integer V97() set
(f . da) - ((IncIC (f,f)) . f) is V17() V62() integer V97() set
f . f is V17() V62() integer V97() set
(f . da) - (f . f) is V17() V62() integer V97() set
(Exec (k,f)) . d is V17() V62() integer V97() set
(Exec ((IncAddr (k,i)),f)) . d is V17() V62() integer V97() set
(IncIC ((Exec ((IncAddr (k,i)),f)),f)) . d is V17() V62() integer V97() set
d is V64() Element of the U1 of SCM+FSA
(Exec ((IncAddr (k,(i + f))),(IncIC (f,f)))) . d is V17() V62() integer V97() set
(Exec (k,(IncIC (f,f)))) . d is V17() V62() integer V97() set
(IncIC (f,f)) . d is V17() V62() integer V97() set
f . d is V17() V62() integer V97() set
(Exec (k,f)) . d is V17() V62() integer V97() set
(Exec ((IncAddr (k,i)),f)) . d is V17() V62() integer V97() set
(IncIC ((Exec ((IncAddr (k,i)),f)),f)) . d is V17() V62() integer V97() set
d is V64() Element of the U1 of SCM+FSA
InsCode k is V17() V20() V21() V22() V26() V62() integer V97() Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
K23( the InstructionsF of SCM+FSA) is set
proj1 the InstructionsF of SCM+FSA is non empty set
proj1 (proj1 the InstructionsF of SCM+FSA) is set
K13(k) is set
K13(K13(k)) is set
da is V64() Element of the U1 of SCM+FSA
f is V64() Element of the U1 of SCM+FSA
MultBy (da,f) is ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
d is FinSeq-Location
(Exec ((IncAddr (k,(i + f))),(IncIC (f,f)))) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
Exec (k,(IncIC (f,f))) is Relation-like the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible total set
the Execution of SCM+FSA . k is Element of K140(K168(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K168(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
( the Execution of SCM+FSA . k) . (IncIC (f,f)) is set
(Exec (k,(IncIC (f,f)))) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(IncIC (f,f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
f . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
Exec (k,f) is Relation-like the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible total set
( the Execution of SCM+FSA . k) . f is set
(Exec (k,f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(Exec ((IncAddr (k,i)),f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(IncIC ((Exec ((IncAddr (k,i)),f)),f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
d is V64() Element of the U1 of SCM+FSA
(Exec ((IncAddr (k,(i + f))),(IncIC (f,f)))) . d is V17() V62() integer V97() set
(Exec (k,(IncIC (f,f)))) . d is V17() V62() integer V97() set
(IncIC (f,f)) . da is V17() V62() integer V97() set
(IncIC (f,f)) . f is V17() V62() integer V97() set
((IncIC (f,f)) . da) * ((IncIC (f,f)) . f) is V17() V62() integer V97() set
f . da is V17() V62() integer V97() set
(f . da) * ((IncIC (f,f)) . f) is V17() V62() integer V97() set
f . f is V17() V62() integer V97() set
(f . da) * (f . f) is V17() V62() integer V97() set
(Exec (k,f)) . d is V17() V62() integer V97() set
(Exec ((IncAddr (k,i)),f)) . d is V17() V62() integer V97() set
(IncIC ((Exec ((IncAddr (k,i)),f)),f)) . d is V17() V62() integer V97() set
d is V64() Element of the U1 of SCM+FSA
(Exec ((IncAddr (k,(i + f))),(IncIC (f,f)))) . d is V17() V62() integer V97() set
(Exec (k,(IncIC (f,f)))) . d is V17() V62() integer V97() set
(IncIC (f,f)) . d is V17() V62() integer V97() set
f . d is V17() V62() integer V97() set
(Exec (k,f)) . d is V17() V62() integer V97() set
(Exec ((IncAddr (k,i)),f)) . d is V17() V62() integer V97() set
(IncIC ((Exec ((IncAddr (k,i)),f)),f)) . d is V17() V62() integer V97() set
d is V64() Element of the U1 of SCM+FSA
InsCode k is V17() V20() V21() V22() V26() V62() integer V97() Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
K23( the InstructionsF of SCM+FSA) is set
proj1 the InstructionsF of SCM+FSA is non empty set
proj1 (proj1 the InstructionsF of SCM+FSA) is set
K13(k) is set
K13(K13(k)) is set
da is V64() Element of the U1 of SCM+FSA
f is V64() Element of the U1 of SCM+FSA
Divide (da,f) is ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
d is FinSeq-Location
(Exec ((IncAddr (k,(i + f))),(IncIC (f,f)))) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
Exec (k,(IncIC (f,f))) is Relation-like the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible total set
the Execution of SCM+FSA . k is Element of K140(K168(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K168(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
( the Execution of SCM+FSA . k) . (IncIC (f,f)) is set
(Exec (k,(IncIC (f,f)))) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(IncIC (f,f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
f . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
Exec (k,f) is Relation-like the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible total set
( the Execution of SCM+FSA . k) . f is set
(Exec (k,f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(Exec ((IncAddr (k,i)),f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(IncIC ((Exec ((IncAddr (k,i)),f)),f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
d is V64() Element of the U1 of SCM+FSA
(Exec ((IncAddr (k,(i + f))),(IncIC (f,f)))) . d is V17() V62() integer V97() set
(Exec (k,(IncIC (f,f)))) . d is V17() V62() integer V97() set
(IncIC (f,f)) . da is V17() V62() integer V97() set
(IncIC (f,f)) . f is V17() V62() integer V97() set
((IncIC (f,f)) . da) div ((IncIC (f,f)) . f) is V17() V62() integer V97() set
f . da is V17() V62() integer V97() set
(f . da) div ((IncIC (f,f)) . f) is V17() V62() integer V97() set
f . f is V17() V62() integer V97() set
(f . da) div (f . f) is V17() V62() integer V97() set
(Exec (k,f)) . d is V17() V62() integer V97() set
(Exec ((IncAddr (k,i)),f)) . d is V17() V62() integer V97() set
(IncIC ((Exec ((IncAddr (k,i)),f)),f)) . d is V17() V62() integer V97() set
d is V64() Element of the U1 of SCM+FSA
(Exec ((IncAddr (k,(i + f))),(IncIC (f,f)))) . d is V17() V62() integer V97() set
(Exec (k,(IncIC (f,f)))) . d is V17() V62() integer V97() set
(IncIC (f,f)) . da is V17() V62() integer V97() set
(IncIC (f,f)) . f is V17() V62() integer V97() set
((IncIC (f,f)) . da) mod ((IncIC (f,f)) . f) is V17() V62() integer V97() set
f . da is V17() V62() integer V97() set
(f . da) mod ((IncIC (f,f)) . f) is V17() V62() integer V97() set
f . f is V17() V62() integer V97() set
(f . da) mod (f . f) is V17() V62() integer V97() set
(Exec (k,f)) . d is V17() V62() integer V97() set
(Exec ((IncAddr (k,i)),f)) . d is V17() V62() integer V97() set
(IncIC ((Exec ((IncAddr (k,i)),f)),f)) . d is V17() V62() integer V97() set
d is V64() Element of the U1 of SCM+FSA
(Exec ((IncAddr (k,(i + f))),(IncIC (f,f)))) . d is V17() V62() integer V97() set
(Exec (k,(IncIC (f,f)))) . d is V17() V62() integer V97() set
(IncIC (f,f)) . d is V17() V62() integer V97() set
f . d is V17() V62() integer V97() set
(Exec (k,f)) . d is V17() V62() integer V97() set
(Exec ((IncAddr (k,i)),f)) . d is V17() V62() integer V97() set
(IncIC ((Exec ((IncAddr (k,i)),f)),f)) . d is V17() V62() integer V97() set
d is V64() Element of the U1 of SCM+FSA
(Exec ((IncAddr (k,(i + f))),(IncIC (f,f)))) . d is V17() V62() integer V97() set
(IncIC ((Exec ((IncAddr (k,i)),f)),f)) . d is V17() V62() integer V97() set
d is V64() Element of the U1 of SCM+FSA
(Exec ((IncAddr (k,(i + f))),(IncIC (f,f)))) . d is V17() V62() integer V97() set
(IncIC ((Exec ((IncAddr (k,i)),f)),f)) . d is V17() V62() integer V97() set
d is V64() Element of the U1 of SCM+FSA
(Exec ((IncAddr (k,(i + f))),(IncIC (f,f)))) . d is V17() V62() integer V97() set
(Exec (k,(IncIC (f,f)))) . d is V17() V62() integer V97() set
(IncIC (f,f)) . da is V17() V62() integer V97() set
(IncIC (f,f)) . f is V17() V62() integer V97() set
((IncIC (f,f)) . da) mod ((IncIC (f,f)) . f) is V17() V62() integer V97() set
f . da is V17() V62() integer V97() set
(f . da) mod ((IncIC (f,f)) . f) is V17() V62() integer V97() set
f . f is V17() V62() integer V97() set
(f . da) mod (f . f) is V17() V62() integer V97() set
(Exec (k,f)) . d is V17() V62() integer V97() set
(Exec ((IncAddr (k,i)),f)) . d is V17() V62() integer V97() set
(IncIC ((Exec ((IncAddr (k,i)),f)),f)) . d is V17() V62() integer V97() set
d is V64() Element of the U1 of SCM+FSA
(Exec ((IncAddr (k,(i + f))),(IncIC (f,f)))) . d is V17() V62() integer V97() set
(Exec (k,(IncIC (f,f)))) . d is V17() V62() integer V97() set
(IncIC (f,f)) . d is V17() V62() integer V97() set
f . d is V17() V62() integer V97() set
(Exec (k,f)) . d is V17() V62() integer V97() set
(Exec ((IncAddr (k,i)),f)) . d is V17() V62() integer V97() set
(IncIC ((Exec ((IncAddr (k,i)),f)),f)) . d is V17() V62() integer V97() set
d is V64() Element of the U1 of SCM+FSA
InsCode k is V17() V20() V21() V22() V26() V62() integer V97() Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
K23( the InstructionsF of SCM+FSA) is set
proj1 the InstructionsF of SCM+FSA is non empty set
proj1 (proj1 the InstructionsF of SCM+FSA) is set
K13(k) is set
K13(K13(k)) is set
da is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
goto da is V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
SCM-goto da is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of SCM
<*da*> is non empty Relation-like NAT -defined Function-like V27() V34(1) FinSequence-like FinSubsequence-like V60() set
[6,<*da*>,{}] is V1() V2() set
[6,<*da*>] is V1() set
{6,<*da*>} is non empty V27() V60() V65() V66() set
{6} is non empty V27() V60() V65() V66() set
{{6,<*da*>},{6}} is non empty V27() V31() V60() V65() V66() set
[[6,<*da*>],{}] is V1() set
da + (i + f) is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
goto (da + (i + f)) is V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
SCM-goto (da + (i + f)) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of SCM
<*(da + (i + f))*> is non empty Relation-like NAT -defined Function-like V27() V34(1) FinSequence-like FinSubsequence-like V60() set
[6,<*(da + (i + f))*>,{}] is V1() V2() set
[6,<*(da + (i + f))*>] is V1() set
{6,<*(da + (i + f))*>} is non empty V27() V60() V65() V66() set
{{6,<*(da + (i + f))*>},{6}} is non empty V27() V31() V60() V65() V66() set
[[6,<*(da + (i + f))*>],{}] is V1() set
f is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
IncAddr (k,f) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
da + f is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
goto (da + f) is V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
SCM-goto (da + f) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of SCM
<*(da + f)*> is non empty Relation-like NAT -defined Function-like V27() V34(1) FinSequence-like FinSubsequence-like V60() set
[6,<*(da + f)*>,{}] is V1() V2() set
[6,<*(da + f)*>] is V1() set
{6,<*(da + f)*>} is non empty V27() V60() V65() V66() set
{{6,<*(da + f)*>},{6}} is non empty V27() V31() V60() V65() V66() set
[[6,<*(da + f)*>],{}] is V1() set
d is FinSeq-Location
(Exec ((IncAddr (k,(i + f))),(IncIC (f,f)))) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(IncIC (f,f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
f . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(Exec ((IncAddr (k,i)),f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(IncIC ((Exec ((IncAddr (k,i)),f)),f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
d is V64() Element of the U1 of SCM+FSA
(Exec ((IncAddr (k,(i + f))),(IncIC (f,f)))) . d is V17() V62() integer V97() set
(IncIC (f,f)) . d is V17() V62() integer V97() set
f . d is V17() V62() integer V97() set
(Exec ((IncAddr (k,i)),f)) . d is V17() V62() integer V97() set
(IncIC ((Exec ((IncAddr (k,i)),f)),f)) . d is V17() V62() integer V97() set
InsCode k is V17() V20() V21() V22() V26() V62() integer V97() Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
K23( the InstructionsF of SCM+FSA) is set
proj1 the InstructionsF of SCM+FSA is non empty set
proj1 (proj1 the InstructionsF of SCM+FSA) is set
K13(k) is set
K13(K13(k)) is set
da is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
f is V64() Element of the U1 of SCM+FSA
f =0_goto da is V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
da + (i + f) is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
f =0_goto (da + (i + f)) is V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
d is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
IncAddr (k,d) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
da + d is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
f =0_goto (da + d) is V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
d is FinSeq-Location
(Exec ((IncAddr (k,(i + f))),(IncIC (f,f)))) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(IncIC (f,f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
f . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(Exec ((IncAddr (k,i)),f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(IncIC ((Exec ((IncAddr (k,i)),f)),f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
d is V64() Element of the U1 of SCM+FSA
(Exec ((IncAddr (k,(i + f))),(IncIC (f,f)))) . d is V17() V62() integer V97() set
(IncIC (f,f)) . d is V17() V62() integer V97() set
f . d is V17() V62() integer V97() set
(Exec ((IncAddr (k,i)),f)) . d is V17() V62() integer V97() set
(IncIC ((Exec ((IncAddr (k,i)),f)),f)) . d is V17() V62() integer V97() set
InsCode k is V17() V20() V21() V22() V26() V62() integer V97() Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
K23( the InstructionsF of SCM+FSA) is set
proj1 the InstructionsF of SCM+FSA is non empty set
proj1 (proj1 the InstructionsF of SCM+FSA) is set
K13(k) is set
K13(K13(k)) is set
da is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
f is V64() Element of the U1 of SCM+FSA
f >0_goto da is V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
da + (i + f) is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
f >0_goto (da + (i + f)) is V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
d is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
IncAddr (k,d) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
da + d is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
f >0_goto (da + d) is V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
d is FinSeq-Location
(Exec ((IncAddr (k,(i + f))),(IncIC (f,f)))) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(IncIC (f,f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
f . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(Exec ((IncAddr (k,i)),f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(IncIC ((Exec ((IncAddr (k,i)),f)),f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
d is V64() Element of the U1 of SCM+FSA
(Exec ((IncAddr (k,(i + f))),(IncIC (f,f)))) . d is V17() V62() integer V97() set
(IncIC (f,f)) . d is V17() V62() integer V97() set
f . d is V17() V62() integer V97() set
(Exec ((IncAddr (k,i)),f)) . d is V17() V62() integer V97() set
(IncIC ((Exec ((IncAddr (k,i)),f)),f)) . d is V17() V62() integer V97() set
InsCode k is V17() V20() V21() V22() V26() V62() integer V97() Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
K23( the InstructionsF of SCM+FSA) is set
proj1 the InstructionsF of SCM+FSA is non empty set
proj1 (proj1 the InstructionsF of SCM+FSA) is set
K13(k) is set
K13(K13(k)) is set
f is V64() Element of the U1 of SCM+FSA
da is V64() Element of the U1 of SCM+FSA
d is FinSeq-Location
f := (d,da) is ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
<*f,d,da*> is non empty Relation-like NAT -defined Function-like V27() V34(3) FinSequence-like FinSubsequence-like V60() set
[9,{},<*f,d,da*>] is V1() V2() set
[[9,{}],<*f,d,da*>] is V1() set
{[9,{}],<*f,d,da*>} is non empty V27() V60() set
{{[9,{}],<*f,d,da*>},{[9,{}]}} is non empty V27() V31() V60() V65() V66() set
d is FinSeq-Location
(Exec ((IncAddr (k,(i + f))),(IncIC (f,f)))) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
Exec (k,(IncIC (f,f))) is Relation-like the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible total set
the Execution of SCM+FSA . k is Element of K140(K168(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K168(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
( the Execution of SCM+FSA . k) . (IncIC (f,f)) is set
(Exec (k,(IncIC (f,f)))) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(IncIC (f,f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
f . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
Exec (k,f) is Relation-like the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible total set
( the Execution of SCM+FSA . k) . f is set
(Exec (k,f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(Exec ((IncAddr (k,i)),f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(IncIC ((Exec ((IncAddr (k,i)),f)),f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
d is V64() Element of the U1 of SCM+FSA
f . da is V17() V62() integer V97() set
abs (f . da) is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
(Exec (k,f)) . f is V17() V62() integer V97() set
f . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
m is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
(f . d) /. m is V17() V62() integer V97() Element of INT
(IncIC (f,f)) . da is V17() V62() integer V97() set
abs ((IncIC (f,f)) . da) is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
(Exec (k,(IncIC (f,f)))) . f is V17() V62() integer V97() set
(IncIC (f,f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(Exec ((IncAddr (k,(i + f))),(IncIC (f,f)))) . d is V17() V62() integer V97() set
(Exec (k,(IncIC (f,f)))) . d is V17() V62() integer V97() set
IncIC ((Exec (k,f)),f) is Relation-like the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible total set
IC (Exec (k,f)) is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
(Exec (k,f)) . (IC ) is set
(IC (Exec (k,f))) + f is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
Start-At (((IC (Exec (k,f))) + f),SCM+FSA) is non empty Relation-like the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible V27() V60() (IC (Exec (k,f))) + f -started set
K314((IC ),((IC (Exec (k,f))) + f)) is V5() Relation-like {(IC )} -defined NAT -valued INT -valued RAT -valued Function-like one-to-one constant V27() V60() V100() V101() V102() V103() V104() V105() V106() V107() set
K305({(IC )},((IC (Exec (k,f))) + f)) is non empty Relation-like {(IC )} -defined NAT -valued INT -valued RAT -valued {((IC (Exec (k,f))) + f)} -valued Function-like constant V27() total V39({(IC )},{((IC (Exec (k,f))) + f)}) V60() V100() V101() V102() V103() Element of K32(K33({(IC )},{((IC (Exec (k,f))) + f)}))
{((IC (Exec (k,f))) + f)} is non empty V27() V60() set
K33({(IC )},{((IC (Exec (k,f))) + f)}) is Relation-like V27() V60() set
K32(K33({(IC )},{((IC (Exec (k,f))) + f)})) is V27() V31() V60() set
(Exec (k,f)) +* (Start-At (((IC (Exec (k,f))) + f),SCM+FSA)) is non empty Relation-like the U1 of SCM+FSA -defined the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible K281(3,SCM+FSA) -compatible total (IC (Exec (k,f))) + f -started set
(IncIC ((Exec (k,f)),f)) . d is V17() V62() integer V97() set
(IncIC ((Exec ((IncAddr (k,i)),f)),f)) . d is V17() V62() integer V97() set
c₁₁ is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
((IncIC (f,f)) . d) /. c₁₁ is V17() V62() integer V97() Element of INT
d is V64() Element of the U1 of SCM+FSA
(Exec ((IncAddr (k,(i + f))),(IncIC (f,f)))) . d is V17() V62() integer V97() set
(Exec (k,(IncIC (f,f)))) . d is V17() V62() integer V97() set
(IncIC (f,f)) . d is V17() V62() integer V97() set
f . d is V17() V62() integer V97() set
(Exec (k,f)) . d is V17() V62() integer V97() set
(Exec ((IncAddr (k,i)),f)) . d is V17() V62() integer V97() set
(IncIC ((Exec ((IncAddr (k,i)),f)),f)) . d is V17() V62() integer V97() set
d is V64() Element of the U1 of SCM+FSA
InsCode k is V17() V20() V21() V22() V26() V62() integer V97() Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
K23( the InstructionsF of SCM+FSA) is set
proj1 the InstructionsF of SCM+FSA is non empty set
proj1 (proj1 the InstructionsF of SCM+FSA) is set
K13(k) is set
K13(K13(k)) is set
f is V64() Element of the U1 of SCM+FSA
da is V64() Element of the U1 of SCM+FSA
d is FinSeq-Location
(d,da) := f is ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
<*f,d,da*> is non empty Relation-like NAT -defined Function-like V27() V34(3) FinSequence-like FinSubsequence-like V60() set
[10,{},<*f,d,da*>] is V1() V2() set
[[10,{}],<*f,d,da*>] is V1() set
{[10,{}],<*f,d,da*>} is non empty V27() V60() set
{{[10,{}],<*f,d,da*>},{[10,{}]}} is non empty V27() V31() V60() V65() V66() set
f . da is V17() V62() integer V97() set
abs (f . da) is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
Exec (k,f) is Relation-like the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible total set
the Execution of SCM+FSA . k is Element of K140(K168(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K168(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
( the Execution of SCM+FSA . k) . f is set
(Exec (k,f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
f . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
f . f is V17() V62() integer V97() set
m is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
(f . d) +* (m,(f . f)) is Relation-like Function-like set
(IncIC (f,f)) . da is V17() V62() integer V97() set
abs ((IncIC (f,f)) . da) is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
Exec (k,(IncIC (f,f))) is Relation-like the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible total set
( the Execution of SCM+FSA . k) . (IncIC (f,f)) is set
(Exec (k,(IncIC (f,f)))) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(IncIC (f,f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(IncIC (f,f)) . f is V17() V62() integer V97() set
d is FinSeq-Location
(Exec ((IncAddr (k,(i + f))),(IncIC (f,f)))) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(Exec (k,(IncIC (f,f)))) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
IncIC ((Exec (k,f)),f) is Relation-like the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible total set
IC (Exec (k,f)) is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
(Exec (k,f)) . (IC ) is set
(IC (Exec (k,f))) + f is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
Start-At (((IC (Exec (k,f))) + f),SCM+FSA) is non empty Relation-like the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible V27() V60() (IC (Exec (k,f))) + f -started set
K314((IC ),((IC (Exec (k,f))) + f)) is V5() Relation-like {(IC )} -defined NAT -valued INT -valued RAT -valued Function-like one-to-one constant V27() V60() V100() V101() V102() V103() V104() V105() V106() V107() set
K305({(IC )},((IC (Exec (k,f))) + f)) is non empty Relation-like {(IC )} -defined NAT -valued INT -valued RAT -valued {((IC (Exec (k,f))) + f)} -valued Function-like constant V27() total V39({(IC )},{((IC (Exec (k,f))) + f)}) V60() V100() V101() V102() V103() Element of K32(K33({(IC )},{((IC (Exec (k,f))) + f)}))
{((IC (Exec (k,f))) + f)} is non empty V27() V60() set
K33({(IC )},{((IC (Exec (k,f))) + f)}) is Relation-like V27() V60() set
K32(K33({(IC )},{((IC (Exec (k,f))) + f)})) is V27() V31() V60() set
(Exec (k,f)) +* (Start-At (((IC (Exec (k,f))) + f),SCM+FSA)) is non empty Relation-like the U1 of SCM+FSA -defined the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible K281(3,SCM+FSA) -compatible total (IC (Exec (k,f))) + f -started set
(IncIC ((Exec (k,f)),f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(IncIC ((Exec ((IncAddr (k,i)),f)),f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
c₁₁ is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
((IncIC (f,f)) . d) +* (c₁₁,((IncIC (f,f)) . f)) is Relation-like Function-like set
d is FinSeq-Location
(Exec ((IncAddr (k,(i + f))),(IncIC (f,f)))) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(Exec (k,(IncIC (f,f)))) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(IncIC (f,f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
f . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(Exec (k,f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(Exec ((IncAddr (k,i)),f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(IncIC ((Exec ((IncAddr (k,i)),f)),f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
d is FinSeq-Location
d is V64() Element of the U1 of SCM+FSA
(Exec ((IncAddr (k,(i + f))),(IncIC (f,f)))) . d is V17() V62() integer V97() set
(Exec (k,(IncIC (f,f)))) . d is V17() V62() integer V97() set
(IncIC (f,f)) . d is V17() V62() integer V97() set
f . d is V17() V62() integer V97() set
(Exec (k,f)) . d is V17() V62() integer V97() set
(Exec ((IncAddr (k,i)),f)) . d is V17() V62() integer V97() set
(IncIC ((Exec ((IncAddr (k,i)),f)),f)) . d is V17() V62() integer V97() set
InsCode k is V17() V20() V21() V22() V26() V62() integer V97() Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
K23( the InstructionsF of SCM+FSA) is set
proj1 the InstructionsF of SCM+FSA is non empty set
proj1 (proj1 the InstructionsF of SCM+FSA) is set
K13(k) is set
K13(K13(k)) is set
da is V64() Element of the U1 of SCM+FSA
f is FinSeq-Location
da :=len f is ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
<*da,f*> is non empty Relation-like NAT -defined Function-like V27() V34(2) FinSequence-like FinSubsequence-like V60() set
[11,{},<*da,f*>] is V1() V2() set
[[11,{}],<*da,f*>] is V1() set
{[11,{}],<*da,f*>} is non empty V27() V60() set
{{[11,{}],<*da,f*>},{[11,{}]}} is non empty V27() V31() V60() V65() V66() set
d is FinSeq-Location
(Exec ((IncAddr (k,(i + f))),(IncIC (f,f)))) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
Exec (k,(IncIC (f,f))) is Relation-like the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible total set
the Execution of SCM+FSA . k is Element of K140(K168(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K168(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
( the Execution of SCM+FSA . k) . (IncIC (f,f)) is set
(Exec (k,(IncIC (f,f)))) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(IncIC (f,f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
f . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
Exec (k,f) is Relation-like the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible total set
( the Execution of SCM+FSA . k) . f is set
(Exec (k,f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(Exec ((IncAddr (k,i)),f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(IncIC ((Exec ((IncAddr (k,i)),f)),f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
d is V64() Element of the U1 of SCM+FSA
(Exec ((IncAddr (k,(i + f))),(IncIC (f,f)))) . d is V17() V62() integer V97() set
(Exec (k,(IncIC (f,f)))) . d is V17() V62() integer V97() set
(IncIC (f,f)) . f is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
len ((IncIC (f,f)) . f) is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
f . f is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
len (f . f) is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
(Exec (k,f)) . d is V17() V62() integer V97() set
IncIC ((Exec (k,f)),f) is Relation-like the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible total set
IC (Exec (k,f)) is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
(Exec (k,f)) . (IC ) is set
(IC (Exec (k,f))) + f is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
Start-At (((IC (Exec (k,f))) + f),SCM+FSA) is non empty Relation-like the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible V27() V60() (IC (Exec (k,f))) + f -started set
K314((IC ),((IC (Exec (k,f))) + f)) is V5() Relation-like {(IC )} -defined NAT -valued INT -valued RAT -valued Function-like one-to-one constant V27() V60() V100() V101() V102() V103() V104() V105() V106() V107() set
K305({(IC )},((IC (Exec (k,f))) + f)) is non empty Relation-like {(IC )} -defined NAT -valued INT -valued RAT -valued {((IC (Exec (k,f))) + f)} -valued Function-like constant V27() total V39({(IC )},{((IC (Exec (k,f))) + f)}) V60() V100() V101() V102() V103() Element of K32(K33({(IC )},{((IC (Exec (k,f))) + f)}))
{((IC (Exec (k,f))) + f)} is non empty V27() V60() set
K33({(IC )},{((IC (Exec (k,f))) + f)}) is Relation-like V27() V60() set
K32(K33({(IC )},{((IC (Exec (k,f))) + f)})) is V27() V31() V60() set
(Exec (k,f)) +* (Start-At (((IC (Exec (k,f))) + f),SCM+FSA)) is non empty Relation-like the U1 of SCM+FSA -defined the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible K281(3,SCM+FSA) -compatible total (IC (Exec (k,f))) + f -started set
(IncIC ((Exec (k,f)),f)) . d is V17() V62() integer V97() set
(IncIC ((Exec ((IncAddr (k,i)),f)),f)) . d is V17() V62() integer V97() set
d is V64() Element of the U1 of SCM+FSA
(Exec ((IncAddr (k,(i + f))),(IncIC (f,f)))) . d is V17() V62() integer V97() set
(Exec (k,(IncIC (f,f)))) . d is V17() V62() integer V97() set
(IncIC (f,f)) . d is V17() V62() integer V97() set
f . d is V17() V62() integer V97() set
(Exec (k,f)) . d is V17() V62() integer V97() set
(Exec ((IncAddr (k,i)),f)) . d is V17() V62() integer V97() set
(IncIC ((Exec ((IncAddr (k,i)),f)),f)) . d is V17() V62() integer V97() set
d is V64() Element of the U1 of SCM+FSA
InsCode k is V17() V20() V21() V22() V26() V62() integer V97() Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
K23( the InstructionsF of SCM+FSA) is set
proj1 the InstructionsF of SCM+FSA is non empty set
proj1 (proj1 the InstructionsF of SCM+FSA) is set
K13(k) is set
K13(K13(k)) is set
da is V64() Element of the U1 of SCM+FSA
f is FinSeq-Location
f :=<0,...,0> da is ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
<*da,f*> is non empty Relation-like NAT -defined Function-like V27() V34(2) FinSequence-like FinSubsequence-like V60() set
[12,{},<*da,f*>] is V1() V2() set
[[12,{}],<*da,f*>] is V1() set
{[12,{}],<*da,f*>} is non empty V27() V60() set
{{[12,{}],<*da,f*>},{[12,{}]}} is non empty V27() V31() V60() V65() V66() set
f . da is V17() V62() integer V97() set
abs (f . da) is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
Exec (k,f) is Relation-like the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible total set
the Execution of SCM+FSA . k is Element of K140(K168(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K168(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
( the Execution of SCM+FSA . k) . f is set
(Exec (k,f)) . f is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(IncIC (f,f)) . da is V17() V62() integer V97() set
abs ((IncIC (f,f)) . da) is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
Exec (k,(IncIC (f,f))) is Relation-like the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible total set
( the Execution of SCM+FSA . k) . (IncIC (f,f)) is set
(Exec (k,(IncIC (f,f)))) . f is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
d is FinSeq-Location
(Exec ((IncAddr (k,(i + f))),(IncIC (f,f)))) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(Exec (k,(IncIC (f,f)))) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
IncIC ((Exec (k,f)),f) is Relation-like the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible total set
IC (Exec (k,f)) is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
(Exec (k,f)) . (IC ) is set
(IC (Exec (k,f))) + f is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
Start-At (((IC (Exec (k,f))) + f),SCM+FSA) is non empty Relation-like the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible V27() V60() (IC (Exec (k,f))) + f -started set
K314((IC ),((IC (Exec (k,f))) + f)) is V5() Relation-like {(IC )} -defined NAT -valued INT -valued RAT -valued Function-like one-to-one constant V27() V60() V100() V101() V102() V103() V104() V105() V106() V107() set
K305({(IC )},((IC (Exec (k,f))) + f)) is non empty Relation-like {(IC )} -defined NAT -valued INT -valued RAT -valued {((IC (Exec (k,f))) + f)} -valued Function-like constant V27() total V39({(IC )},{((IC (Exec (k,f))) + f)}) V60() V100() V101() V102() V103() Element of K32(K33({(IC )},{((IC (Exec (k,f))) + f)}))
{((IC (Exec (k,f))) + f)} is non empty V27() V60() set
K33({(IC )},{((IC (Exec (k,f))) + f)}) is Relation-like V27() V60() set
K32(K33({(IC )},{((IC (Exec (k,f))) + f)})) is V27() V31() V60() set
(Exec (k,f)) +* (Start-At (((IC (Exec (k,f))) + f),SCM+FSA)) is non empty Relation-like the U1 of SCM+FSA -defined the U1 of SCM+FSA -defined Function-like K281(3,SCM+FSA) -compatible K281(3,SCM+FSA) -compatible total (IC (Exec (k,f))) + f -started set
(IncIC ((Exec (k,f)),f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(IncIC ((Exec ((IncAddr (k,i)),f)),f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
d is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
d |-> 0 is Relation-like NAT -defined NAT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() V103() Element of d -tuples_on NAT
d -tuples_on NAT is FinSequenceSet of NAT
m is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
m |-> 0 is Relation-like NAT -defined NAT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() V103() Element of m -tuples_on NAT
m -tuples_on NAT is FinSequenceSet of NAT
d is FinSeq-Location
(Exec ((IncAddr (k,(i + f))),(IncIC (f,f)))) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(Exec (k,(IncIC (f,f)))) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(IncIC (f,f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
f . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(Exec (k,f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(Exec ((IncAddr (k,i)),f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
(IncIC ((Exec ((IncAddr (k,i)),f)),f)) . d is Relation-like NAT -defined INT -valued Function-like V27() FinSequence-like FinSubsequence-like V60() V100() V101() V102() FinSequence of INT
d is FinSeq-Location
d is V64() Element of the U1 of SCM+FSA
(Exec ((IncAddr (k,(i + f))),(IncIC (f,f)))) . d is V17() V62() integer V97() set
(Exec (k,(IncIC (f,f)))) . d is V17() V62() integer V97() set
(IncIC (f,f)) . d is V17() V62() integer V97() set
f . d is V17() V62() integer V97() set
(Exec (k,f)) . d is V17() V62() integer V97() set
(Exec ((IncAddr (k,i)),f)) . d is V17() V62() integer V97() set
(IncIC ((Exec ((IncAddr (k,i)),f)),f)) . d is V17() V62() integer V97() set
InsCode k is V17() V20() V21() V22() V26() V62() integer V97() Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
K23( the InstructionsF of SCM+FSA) is set
proj1 the InstructionsF of SCM+FSA is non empty set
proj1 (proj1 the InstructionsF of SCM+FSA) is set
K13(k) is set
K13(K13(k)) is set
{6,7,8} is V27() V60() V65() set
k is V17() V20() V21() V22() V26() V62() integer V97() Element of NAT
i is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of SCM+FSA
InsCode i is V17() V20() V21() V22() V26() V62() integer V97() Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
K23( the InstructionsF of SCM+FSA) is set
proj1 the InstructionsF of SCM+FSA is non empty set
proj1 (proj1 the InstructionsF of SCM+FSA) is set
K13(i) is set
K13(K13(i)) is set
IncAddr (i,k) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of SCM+FSA
da is V64() Element of the U1 of SCM+FSA
f is V64() Element of the U1 of SCM+FSA
da := f is ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable relocable Element of the InstructionsF of SCM+FSA
da is V64() Element of the U1 of SCM+FSA
f is V64() Element of the U1 of SCM+FSA
AddTo (da,f) is ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable relocable Element of the InstructionsF of SCM+FSA
da is V64() Element of the U1 of SCM+FSA
f is V64() Element of the U1 of SCM+FSA
SubFrom (da,f) is ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable relocable Element of the InstructionsF of SCM+FSA
da is V64() Element of the U1 of SCM+FSA
f is V64() Element of the U1 of SCM+FSA
MultBy (da,f) is ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable relocable Element of the InstructionsF of SCM+FSA
da is V64() Element of the U1 of SCM+FSA
f is V64() Element of the U1 of SCM+FSA
Divide (da,f) is ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable relocable Element of the InstructionsF of SCM+FSA
f is V64() Element of the U1 of SCM+FSA
da is V64() Element of the U1 of SCM+FSA
f is FinSeq-Location
f := (f,da) is ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable relocable Element of the InstructionsF of SCM+FSA
<*f,f,da*> is non empty Relation-like NAT -defined Function-like V27() V34(3) FinSequence-like FinSubsequence-like V60() set
[9,{},<*f,f,da*>] is V1() V2() set
[[9,{}],<*f,f,da*>] is V1() set
{[9,{}],<*f,f,da*>} is non empty V27() V60() set
{{[9,{}],<*f,f,da*>},{[9,{}]}} is non empty V27() V31() V60() V65() V66() set
f is V64() Element of the U1 of SCM+FSA
da is V64() Element of the U1 of SCM+FSA
f is FinSeq-Location
(f,da) := f is ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable relocable Element of the InstructionsF of SCM+FSA
<*f,f,da*> is non empty Relation-like NAT -defined Function-like V27() V34(3) FinSequence-like FinSubsequence-like V60() set
[10,{},<*f,f,da*>] is V1() V2() set
[[10,{}],<*f,f,da*>] is V1() set
{[10,{}],<*f,f,da*>} is non empty V27() V60() set
{{[10,{}],<*f,f,da*>},{[10,{}]}} is non empty V27() V31() V60() V65() V66() set
da is V64() Element of the U1 of SCM+FSA
f is FinSeq-Location
da :=len f is ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable relocable Element of the InstructionsF of SCM+FSA
<*da,f*> is non empty Relation-like NAT -defined Function-like V27() V34(2) FinSequence-like FinSubsequence-like V60() set
[11,{},<*da,f*>] is V1() V2() set
[[11,{}],<*da,f*>] is V1() set
{[11,{}],<*da,f*>} is non empty V27() V60() set
{{[11,{}],<*da,f*>},{[11,{}]}} is non empty V27() V31() V60() V65() V66() set
da is V64() Element of the U1 of SCM+FSA
f is FinSeq-Location
f :=<0,...,0> da is ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable relocable Element of the InstructionsF of SCM+FSA
<*da,f*> is non empty Relation-like NAT -defined Function-like V27() V34(2) FinSequence-like FinSubsequence-like V60() set
[12,{},<*da,f*>] is V1() V2() set
[[12,{}],<*da,f*>] is V1() set
{[12,{}],<*da,f*>} is non empty V27() V60() set
{{[12,{}],<*da,f*>},{[12,{}]}} is non empty V27() V31() V60() V65() V66() set