SCMPDS_9

:: SCMPDS_9 semantic presentation

REAL is V121() V122() V123() V127() set
NAT is non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() Element of K6(REAL)
K6(REAL) is set
COMPLEX is V121() V127() set
omega is non finite countable denumerable V121() V122() V123() V124() V125() V126() V127() set
K6(omega) is set
9 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
K153(9) is countable V121() V122() V123() V124() V125() V126() Element of K6(omega)
K168() is set
SCM-Memory is set
K6(SCM-Memory) is set
2 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
K7(SCM-Memory,2) is set
K6(K7(SCM-Memory,2)) is set
SCM-OK is Function-like V29( SCM-Memory ,2) Element of K6(K7(SCM-Memory,2))
SCM-VAL is Relation-like 2 -defined Function-like V25(2) set
SCM-VAL * SCM-OK is Relation-like set
product (SCM-VAL * SCM-OK) is set
K169() is non empty set
K137((product (SCM-VAL * SCM-OK)),(product (SCM-VAL * SCM-OK))) is set
K7(K169(),K137((product (SCM-VAL * SCM-OK)),(product (SCM-VAL * SCM-OK)))) is set
K6(K7(K169(),K137((product (SCM-VAL * SCM-OK)),(product (SCM-VAL * SCM-OK))))) is set
K6(NAT) is set
INT is V121() V122() V123() V124() V125() V127() set
K168() \/ INT is set
SCM-Data-Loc is Element of K6(SCM-Memory)
SCM-Data-Loc \/ INT is set
K202() is set
K7(K202(),K137((product (SCM-VAL * SCM-OK)),(product (SCM-VAL * SCM-OK)))) is set
K6(K7(K202(),K137((product (SCM-VAL * SCM-OK)),(product (SCM-VAL * SCM-OK))))) is set
SCMPDS is V50() with_non-empty_values IC-Ins-separated strict strict V91(2) AMI-Struct over 2
K501(NAT,SCM-Memory) is Element of SCM-Memory
K222() is Function-like V29(K202(),K137((product (SCM-VAL * SCM-OK)),(product (SCM-VAL * SCM-OK)))) Element of K6(K7(K202(),K137((product (SCM-VAL * SCM-OK)),(product (SCM-VAL * SCM-OK)))))
AMI-Struct(# SCM-Memory,K501(NAT,SCM-Memory),K202(),SCM-OK,SCM-VAL,K222() #) is strict AMI-Struct over 2
the U1 of SCMPDS is set
the InstructionsF of SCMPDS is V72() V73() V74() V76() set
the_Values_of SCMPDS is Relation-like non-empty the U1 of SCMPDS -defined Function-like V25( the U1 of SCMPDS) set
the Object-Kind of SCMPDS is Function-like V29( the U1 of SCMPDS,2) Element of K6(K7( the U1 of SCMPDS,2))
K7( the U1 of SCMPDS,2) is set
K6(K7( the U1 of SCMPDS,2)) is set
the ValuesF of SCMPDS is Relation-like 2 -defined Function-like V25(2) set
the ValuesF of SCMPDS * the Object-Kind of SCMPDS is Relation-like set
RAT is V121() V122() V123() V124() V127() set
1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
0 is empty ordinal natural V11() real integer Function-like functional ext-real non positive non negative V110() V121() V122() V123() V124() V125() V126() V127() Element of NAT
the empty Function-like functional V121() V122() V123() V124() V125() V126() V127() set is empty Function-like functional V121() V122() V123() V124() V125() V126() V127() set
{} is empty Function-like functional V121() V122() V123() V124() V125() V126() V127() set
IC is Element of the U1 of SCMPDS
K216() is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
K215() is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
l is Int-like Element of the U1 of SCMPDS
x is Int-like Element of the U1 of SCMPDS
X is V11() real integer ext-real set
x is V11() real integer ext-real set
(l,x) --> (X,x) is Relation-like Function-like set
Values l is non empty set
(the_Values_of SCMPDS) . l is set
Values x is non empty set
(the_Values_of SCMPDS) . x is set
xx is Element of Values l
i is Element of Values x
(l,x) --> (xx,i) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible set
l is V11() real integer ext-real set
goto l is Element of the InstructionsF of SCMPDS
14 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
K192(l) is Relation-like Function-like set
K109(14,{},K192(l)) is set
JUMP (goto l) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
{ (NIC ((goto l),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
meet { (NIC ((goto l),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
{ (NIC ((goto l),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
i is set
NIC ((goto l),1) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
product (the_Values_of SCMPDS) is non empty functional with_common_domain product-like set
{ (IC (Exec ((goto l),b₁))) where b₁ is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS) : IC b₁ = 1 } is set
x is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS)
Exec ((goto l),x) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
IC (Exec ((goto l),x)) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(Exec ((goto l),x)) . (IC ) is set
IC x is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
x . (IC ) is set
ICplusConst (x,l) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
x1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
x1 + l is V11() real integer ext-real set
abs (x1 + l) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
NIC ((goto l),0) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
{ (IC (Exec ((goto l),b₁))) where b₁ is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS) : IC b₁ = 0 } is set
nl1 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS)
Exec ((goto l),nl1) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
IC (Exec ((goto l),nl1)) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(Exec ((goto l),nl1)) . (IC ) is set
IC nl1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
nl1 . (IC ) is set
ICplusConst (nl1,l) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
nl2 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
nl2 + l is V11() real integer ext-real set
abs (nl2 + l) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
0 + l is V11() real integer ext-real set
1 + l is V11() real integer ext-real set
1 + l is V11() real integer ext-real set
- (1 + l) is V11() real integer ext-real set
1 / 2 is V11() real ext-real non negative Element of COMPLEX
- (1 / 2) is V11() real ext-real non positive Element of COMPLEX
- (- (1 / 2)) is V11() real ext-real non negative Element of COMPLEX
0 + l is V11() real integer ext-real set
1 + l is V11() real integer ext-real set
- (1 + l) is V11() real integer ext-real set
l is V11() real integer ext-real set
goto l is Element of the InstructionsF of SCMPDS
14 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
K192(l) is Relation-like Function-like set
K109(14,{},K192(l)) is set
JUMP (goto l) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
{ (NIC ((goto l),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
meet { (NIC ((goto l),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
l is Element of the InstructionsF of SCMPDS
x is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
NIC (l,x) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
product (the_Values_of SCMPDS) is non empty functional with_common_domain product-like set
{ (IC (Exec (l,b₁))) where b₁ is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS) : IC b₁ = x } is set
succ x is set
x + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
{(succ x)} is non empty set
xx is set
i is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS)
Exec (l,i) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
IC (Exec (l,i)) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(Exec (l,i)) . (IC ) is set
IC i is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
i . (IC ) is set
the Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) x -started set is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) x -started set
i is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS)
IC i is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
i . (IC ) is set
x is set
X is Element of the InstructionsF of SCMPDS
Exec (X,i) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
IC (Exec (X,i)) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(Exec (X,i)) . (IC ) is set
l is Element of the InstructionsF of SCMPDS
JUMP l is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
{ (NIC (l,b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
meet { (NIC (l,b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
{ (NIC (l,b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
meet { (NIC (l,b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
x is set
xx is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
NIC (l,xx) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
product (the_Values_of SCMPDS) is non empty functional with_common_domain product-like set
{ (IC (Exec (l,b₁))) where b₁ is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS) : IC b₁ = xx } is set
succ xx is set
xx + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
{(succ xx)} is non empty set
i is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
NIC (l,i) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
{ (IC (Exec (l,b₁))) where b₁ is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS) : IC b₁ = i } is set
succ i is set
i + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
{(succ i)} is non empty set
l is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
x is V11() real integer ext-real set
goto x is Element of the InstructionsF of SCMPDS
K192(x) is Relation-like Function-like set
K109(14,{},K192(x)) is set
NIC ((goto x),l) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
product (the_Values_of SCMPDS) is non empty functional with_common_domain product-like set
{ (IC (Exec ((goto x),b₁))) where b₁ is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS) : IC b₁ = l } is set
x + l is V11() real integer ext-real set
abs (x + l) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
{(abs (x + l))} is non empty V121() V122() V123() V124() V125() V126() set
the Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
x1 is set
nl1 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS)
Exec ((goto x),nl1) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
IC (Exec ((goto x),nl1)) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(Exec ((goto x),nl1)) . (IC ) is set
IC nl1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
nl1 . (IC ) is set
ICplusConst (nl1,x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
nl2 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
nl2 + x is V11() real integer ext-real set
abs (nl2 + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
x1 is set
x is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
the Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) x -started set is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) x -started set
nl1 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS)
IC nl1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
nl1 . (IC ) is set
ICplusConst (nl1,x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
nl2 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
nl2 + x is V11() real integer ext-real set
abs (nl2 + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
Exec ((goto x),nl1) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
IC (Exec ((goto x),nl1)) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(Exec ((goto x),nl1)) . (IC ) is set
l is ordinal natural V11() real integer ext-real non negative set
l - 2 is V11() real integer ext-real set
1 + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
2 - 2 is V11() real integer ext-real set
{ b₁ where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : not b₁ <= 1 } is set
l is Int-like Element of the U1 of SCMPDS
return l is Element of the InstructionsF of SCMPDS
K192(l) is Relation-like Function-like set
K109(1,{},K192(l)) is set
x is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
NIC ((return l),x) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
product (the_Values_of SCMPDS) is non empty functional with_common_domain product-like set
{ (IC (Exec ((return l),b₁))) where b₁ is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS) : IC b₁ = x } is set
the Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
i is set
x is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS)
Exec ((return l),x) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
IC (Exec ((return l),x)) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(Exec ((return l),x)) . (IC ) is set
IC x is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
x . (IC ) is set
0 + 2 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
x . l is V11() real integer ext-real set
DataLoc ((x . l),1) is Int-like Element of the U1 of SCMPDS
(x . l) + 1 is V11() real integer ext-real set
abs ((x . l) + 1) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((x . l) + 1))] is set
{1,(abs ((x . l) + 1))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((x . l) + 1))},{1}} is non empty set
x . (DataLoc ((x . l),1)) is V11() real integer ext-real set
abs (x . (DataLoc ((x . l),1))) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(abs (x . (DataLoc ((x . l),1)))) + 2 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
1 + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
x1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
i is set
nl1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
nl1 - 2 is V11() real integer ext-real set
x1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
the Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) x1 -started set is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) x1 -started set
l1 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS)
IC l1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
l1 . (IC ) is set
l2 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,l2] is set
{1,l2} is non empty V121() V122() V123() V124() V125() V126() set
{{1,l2},{1}} is non empty set
l2 + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(l2 + 1)] is set
{1,(l2 + 1)} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(l2 + 1)},{1}} is non empty set
DataLoc (l2,1) is Int-like Element of the U1 of SCMPDS
l2 + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative set
abs (l2 + 1) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs (l2 + 1))] is set
{1,(abs (l2 + 1))} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs (l2 + 1))},{1}} is non empty set
abs (l2 + 1) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs (l2 + 1))] is set
{1,(abs (l2 + 1))} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs (l2 + 1))},{1}} is non empty set
m1 is Int-like Element of the U1 of SCMPDS
nl2 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(l,m1,l2,nl2) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible set
l1 +* (l,m1,l2,nl2) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
dom (l,m1,l2,nl2) is set
{l,[1,(l2 + 1)]} is non empty set
m2 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS)
m2 . l is V11() real integer ext-real set
IC m2 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
m2 . (IC ) is set
m2 . [1,(l2 + 1)] is set
nl2 + 2 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
m2 . (DataLoc (l2,1)) is V11() real integer ext-real set
abs (m2 . (DataLoc (l2,1))) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(abs (m2 . (DataLoc (l2,1)))) + 2 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
Exec ((return l),m2) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
IC (Exec ((return l),m2)) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(Exec ((return l),m2)) . (IC ) is set
l is Int-like Element of the U1 of SCMPDS
x is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
succ x is set
x + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
{(succ x)} is non empty set
X is V11() real integer ext-real set
saveIC (l,X) is Element of the InstructionsF of SCMPDS
3 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
K193(l,X) is set
K109(3,{},K193(l,X)) is set
NIC ((saveIC (l,X)),x) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
product (the_Values_of SCMPDS) is non empty functional with_common_domain product-like set
{ (IC (Exec ((saveIC (l,X)),b₁))) where b₁ is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS) : IC b₁ = x } is set
xx is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
IC xx is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
xx . (IC ) is set
Exec ((saveIC (l,X)),xx) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
(Exec ((saveIC (l,X)),xx)) . (IC ) is set
succ (IC xx) is set
(IC xx) + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
l is Int-like Element of the U1 of SCMPDS
x is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
succ x is set
x + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
{(succ x)} is non empty set
X is V11() real integer ext-real set
l := X is Element of the InstructionsF of SCMPDS
K193(l,X) is set
K109(2,{},K193(l,X)) is set
NIC ((l := X),x) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
product (the_Values_of SCMPDS) is non empty functional with_common_domain product-like set
{ (IC (Exec ((l := X),b₁))) where b₁ is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS) : IC b₁ = x } is set
xx is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
IC xx is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
xx . (IC ) is set
Exec ((l := X),xx) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
(Exec ((l := X),xx)) . (IC ) is set
succ (IC xx) is set
(IC xx) + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
l is Int-like Element of the U1 of SCMPDS
x is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
succ x is set
x + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
{(succ x)} is non empty set
X is V11() real integer ext-real set
x is V11() real integer ext-real set
(l,X) := x is Element of the InstructionsF of SCMPDS
7 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
K194(l,X,x) is set
K109(7,{},K194(l,X,x)) is set
NIC (((l,X) := x),x) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
product (the_Values_of SCMPDS) is non empty functional with_common_domain product-like set
{ (IC (Exec (((l,X) := x),b₁))) where b₁ is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS) : IC b₁ = x } is set
i is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
IC i is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
i . (IC ) is set
Exec (((l,X) := x),i) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
(Exec (((l,X) := x),i)) . (IC ) is set
succ (IC i) is set
(IC i) + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
l is Int-like Element of the U1 of SCMPDS
x is Int-like Element of the U1 of SCMPDS
X is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
succ X is set
X + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
{(succ X)} is non empty set
x is V11() real integer ext-real set
xx is V11() real integer ext-real set
(l,x) := (x,xx) is Element of the InstructionsF of SCMPDS
NIC (((l,x) := (x,xx)),X) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
product (the_Values_of SCMPDS) is non empty functional with_common_domain product-like set
{ (IC (Exec (((l,x) := (x,xx)),b₁))) where b₁ is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS) : IC b₁ = X } is set
x is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
IC x is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
x . (IC ) is set
Exec (((l,x) := (x,xx)),x) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
(Exec (((l,x) := (x,xx)),x)) . (IC ) is set
succ (IC x) is set
(IC x) + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
l is Int-like Element of the U1 of SCMPDS
x is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
succ x is set
x + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
{(succ x)} is non empty set
X is V11() real integer ext-real set
x is V11() real integer ext-real set
AddTo (l,X,x) is Element of the InstructionsF of SCMPDS
8 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
K194(l,X,x) is set
K109(8,{},K194(l,X,x)) is set
NIC ((AddTo (l,X,x)),x) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
product (the_Values_of SCMPDS) is non empty functional with_common_domain product-like set
{ (IC (Exec ((AddTo (l,X,x)),b₁))) where b₁ is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS) : IC b₁ = x } is set
i is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
IC i is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
i . (IC ) is set
Exec ((AddTo (l,X,x)),i) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
(Exec ((AddTo (l,X,x)),i)) . (IC ) is set
succ (IC i) is set
(IC i) + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
l is Int-like Element of the U1 of SCMPDS
x is Int-like Element of the U1 of SCMPDS
X is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
succ X is set
X + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
{(succ X)} is non empty set
x is V11() real integer ext-real set
xx is V11() real integer ext-real set
AddTo (l,x,x,xx) is Element of the InstructionsF of SCMPDS
NIC ((AddTo (l,x,x,xx)),X) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
product (the_Values_of SCMPDS) is non empty functional with_common_domain product-like set
{ (IC (Exec ((AddTo (l,x,x,xx)),b₁))) where b₁ is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS) : IC b₁ = X } is set
x is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
IC x is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
x . (IC ) is set
Exec ((AddTo (l,x,x,xx)),x) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
(Exec ((AddTo (l,x,x,xx)),x)) . (IC ) is set
succ (IC x) is set
(IC x) + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
l is Int-like Element of the U1 of SCMPDS
x is Int-like Element of the U1 of SCMPDS
X is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
succ X is set
X + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
{(succ X)} is non empty set
x is V11() real integer ext-real set
xx is V11() real integer ext-real set
SubFrom (l,x,x,xx) is Element of the InstructionsF of SCMPDS
NIC ((SubFrom (l,x,x,xx)),X) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
product (the_Values_of SCMPDS) is non empty functional with_common_domain product-like set
{ (IC (Exec ((SubFrom (l,x,x,xx)),b₁))) where b₁ is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS) : IC b₁ = X } is set
x is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
IC x is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
x . (IC ) is set
Exec ((SubFrom (l,x,x,xx)),x) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
(Exec ((SubFrom (l,x,x,xx)),x)) . (IC ) is set
succ (IC x) is set
(IC x) + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
l is Int-like Element of the U1 of SCMPDS
x is Int-like Element of the U1 of SCMPDS
X is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
succ X is set
X + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
{(succ X)} is non empty set
x is V11() real integer ext-real set
xx is V11() real integer ext-real set
MultBy (l,x,x,xx) is Element of the InstructionsF of SCMPDS
NIC ((MultBy (l,x,x,xx)),X) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
product (the_Values_of SCMPDS) is non empty functional with_common_domain product-like set
{ (IC (Exec ((MultBy (l,x,x,xx)),b₁))) where b₁ is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS) : IC b₁ = X } is set
x is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
IC x is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
x . (IC ) is set
Exec ((MultBy (l,x,x,xx)),x) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
(Exec ((MultBy (l,x,x,xx)),x)) . (IC ) is set
succ (IC x) is set
(IC x) + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
l is Int-like Element of the U1 of SCMPDS
x is Int-like Element of the U1 of SCMPDS
X is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
succ X is set
X + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
{(succ X)} is non empty set
x is V11() real integer ext-real set
xx is V11() real integer ext-real set
Divide (l,x,x,xx) is Element of the InstructionsF of SCMPDS
NIC ((Divide (l,x,x,xx)),X) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
product (the_Values_of SCMPDS) is non empty functional with_common_domain product-like set
{ (IC (Exec ((Divide (l,x,x,xx)),b₁))) where b₁ is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS) : IC b₁ = X } is set
x is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
IC x is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
x . (IC ) is set
Exec ((Divide (l,x,x,xx)),x) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
(Exec ((Divide (l,x,x,xx)),x)) . (IC ) is set
succ (IC x) is set
(IC x) + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
l is Int-like Element of the U1 of SCMPDS
x is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
succ x is set
x + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
X is V11() real integer ext-real set
x is V11() real integer ext-real set
(l,X) <>0_goto x is Element of the InstructionsF of SCMPDS
4 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
K194(l,X,x) is set
K109(4,{},K194(l,X,x)) is set
NIC (((l,X) <>0_goto x),x) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
product (the_Values_of SCMPDS) is non empty functional with_common_domain product-like set
{ (IC (Exec (((l,X) <>0_goto x),b₁))) where b₁ is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS) : IC b₁ = x } is set
x + x is V11() real integer ext-real set
abs (x + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
{(succ x),(abs (x + x))} is non empty set
the Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
nl1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
the Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) nl1 -started set is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) nl1 -started set
l1 is set
l2 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS)
Exec (((l,X) <>0_goto x),l2) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
IC (Exec (((l,X) <>0_goto x),l2)) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(Exec (((l,X) <>0_goto x),l2)) . (IC ) is set
IC l2 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
l2 . (IC ) is set
ICplusConst (l2,x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
l2 . l is V11() real integer ext-real set
DataLoc ((l2 . l),X) is Int-like Element of the U1 of SCMPDS
(l2 . l) + X is V11() real integer ext-real set
abs ((l2 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((l2 . l) + X))] is set
{1,(abs ((l2 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((l2 . l) + X))},{1}} is non empty set
l2 . (DataLoc ((l2 . l),X)) is V11() real integer ext-real set
s1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
s1 + x is V11() real integer ext-real set
abs (s1 + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
l2 . l is V11() real integer ext-real set
DataLoc ((l2 . l),X) is Int-like Element of the U1 of SCMPDS
(l2 . l) + X is V11() real integer ext-real set
abs ((l2 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((l2 . l) + X))] is set
{1,(abs ((l2 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((l2 . l) + X))},{1}} is non empty set
l2 . (DataLoc ((l2 . l),X)) is V11() real integer ext-real set
l2 . l is V11() real integer ext-real set
DataLoc ((l2 . l),X) is Int-like Element of the U1 of SCMPDS
(l2 . l) + X is V11() real integer ext-real set
abs ((l2 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((l2 . l) + X))] is set
{1,(abs ((l2 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((l2 . l) + X))},{1}} is non empty set
l2 . (DataLoc ((l2 . l),X)) is V11() real integer ext-real set
l1 is set
nl2 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS)
l .--> 0 is V2() Relation-like the U1 of SCMPDS -defined Function-like constant the_Values_of SCMPDS -compatible finite countable set
nl2 +* (l .--> 0) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
l2 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
l2 . l is V11() real integer ext-real set
DataLoc ((l2 . l),X) is Int-like Element of the U1 of SCMPDS
(l2 . l) + X is V11() real integer ext-real set
abs ((l2 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((l2 . l) + X))] is set
{1,(abs ((l2 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((l2 . l) + X))},{1}} is non empty set
(DataLoc ((l2 . l),X)) .--> 0 is V2() Relation-like the U1 of SCMPDS -defined Function-like constant the_Values_of SCMPDS -compatible finite countable set
l2 +* ((DataLoc ((l2 . l),X)) .--> 0) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
s1 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS)
IC s1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
s1 . (IC ) is set
l2 . (IC ) is set
IC nl2 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
nl2 . (IC ) is set
s1 . (DataLoc ((l2 . l),X)) is V11() real integer ext-real set
s1 . l is V11() real integer ext-real set
DataLoc ((s1 . l),X) is Int-like Element of the U1 of SCMPDS
(s1 . l) + X is V11() real integer ext-real set
abs ((s1 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((s1 . l) + X))] is set
{1,(abs ((s1 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((s1 . l) + X))},{1}} is non empty set
s1 . (DataLoc ((s1 . l),X)) is V11() real integer ext-real set
Exec (((l,X) <>0_goto x),s1) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
IC (Exec (((l,X) <>0_goto x),s1)) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(Exec (((l,X) <>0_goto x),s1)) . (IC ) is set
nl2 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS)
l .--> 1 is V2() Relation-like the U1 of SCMPDS -defined Function-like constant the_Values_of SCMPDS -compatible finite countable set
nl2 +* (l .--> 1) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
l2 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
l2 . l is V11() real integer ext-real set
DataLoc ((l2 . l),X) is Int-like Element of the U1 of SCMPDS
(l2 . l) + X is V11() real integer ext-real set
abs ((l2 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((l2 . l) + X))] is set
{1,(abs ((l2 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((l2 . l) + X))},{1}} is non empty set
(DataLoc ((l2 . l),X)) .--> 1 is V2() Relation-like the U1 of SCMPDS -defined Function-like constant the_Values_of SCMPDS -compatible finite countable set
l2 +* ((DataLoc ((l2 . l),X)) .--> 1) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
s1 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS)
s1 . (DataLoc ((l2 . l),X)) is V11() real integer ext-real set
s1 . l is V11() real integer ext-real set
DataLoc ((s1 . l),X) is Int-like Element of the U1 of SCMPDS
(s1 . l) + X is V11() real integer ext-real set
abs ((s1 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((s1 . l) + X))] is set
{1,(abs ((s1 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((s1 . l) + X))},{1}} is non empty set
s1 . (DataLoc ((s1 . l),X)) is V11() real integer ext-real set
IC s1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
s1 . (IC ) is set
l2 . (IC ) is set
IC nl2 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
nl2 . (IC ) is set
ICplusConst (s1,x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
Exec (((l,X) <>0_goto x),s1) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
IC (Exec (((l,X) <>0_goto x),s1)) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(Exec (((l,X) <>0_goto x),s1)) . (IC ) is set
m1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
m1 + x is V11() real integer ext-real set
abs (m1 + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
l is Int-like Element of the U1 of SCMPDS
x is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
succ x is set
x + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
X is V11() real integer ext-real set
x is V11() real integer ext-real set
(l,X) <=0_goto x is Element of the InstructionsF of SCMPDS
5 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
K194(l,X,x) is set
K109(5,{},K194(l,X,x)) is set
NIC (((l,X) <=0_goto x),x) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
product (the_Values_of SCMPDS) is non empty functional with_common_domain product-like set
{ (IC (Exec (((l,X) <=0_goto x),b₁))) where b₁ is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS) : IC b₁ = x } is set
x + x is V11() real integer ext-real set
abs (x + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
{(succ x),(abs (x + x))} is non empty set
the Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
nl1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
the Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) nl1 -started set is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) nl1 -started set
l1 is set
l2 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS)
Exec (((l,X) <=0_goto x),l2) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
IC (Exec (((l,X) <=0_goto x),l2)) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(Exec (((l,X) <=0_goto x),l2)) . (IC ) is set
IC l2 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
l2 . (IC ) is set
ICplusConst (l2,x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
l2 . l is V11() real integer ext-real set
DataLoc ((l2 . l),X) is Int-like Element of the U1 of SCMPDS
(l2 . l) + X is V11() real integer ext-real set
abs ((l2 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((l2 . l) + X))] is set
{1,(abs ((l2 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((l2 . l) + X))},{1}} is non empty set
l2 . (DataLoc ((l2 . l),X)) is V11() real integer ext-real set
s1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
s1 + x is V11() real integer ext-real set
abs (s1 + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
l2 . l is V11() real integer ext-real set
DataLoc ((l2 . l),X) is Int-like Element of the U1 of SCMPDS
(l2 . l) + X is V11() real integer ext-real set
abs ((l2 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((l2 . l) + X))] is set
{1,(abs ((l2 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((l2 . l) + X))},{1}} is non empty set
l2 . (DataLoc ((l2 . l),X)) is V11() real integer ext-real set
l2 . l is V11() real integer ext-real set
DataLoc ((l2 . l),X) is Int-like Element of the U1 of SCMPDS
(l2 . l) + X is V11() real integer ext-real set
abs ((l2 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((l2 . l) + X))] is set
{1,(abs ((l2 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((l2 . l) + X))},{1}} is non empty set
l2 . (DataLoc ((l2 . l),X)) is V11() real integer ext-real set
l1 is set
nl2 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS)
l .--> 1 is V2() Relation-like the U1 of SCMPDS -defined Function-like constant the_Values_of SCMPDS -compatible finite countable set
nl2 +* (l .--> 1) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
l2 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
l2 . l is V11() real integer ext-real set
DataLoc ((l2 . l),X) is Int-like Element of the U1 of SCMPDS
(l2 . l) + X is V11() real integer ext-real set
abs ((l2 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((l2 . l) + X))] is set
{1,(abs ((l2 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((l2 . l) + X))},{1}} is non empty set
(DataLoc ((l2 . l),X)) .--> 1 is V2() Relation-like the U1 of SCMPDS -defined Function-like constant the_Values_of SCMPDS -compatible finite countable set
l2 +* ((DataLoc ((l2 . l),X)) .--> 1) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
s1 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS)
IC s1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
s1 . (IC ) is set
l2 . (IC ) is set
IC nl2 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
nl2 . (IC ) is set
s1 . (DataLoc ((l2 . l),X)) is V11() real integer ext-real set
s1 . l is V11() real integer ext-real set
DataLoc ((s1 . l),X) is Int-like Element of the U1 of SCMPDS
(s1 . l) + X is V11() real integer ext-real set
abs ((s1 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((s1 . l) + X))] is set
{1,(abs ((s1 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((s1 . l) + X))},{1}} is non empty set
s1 . (DataLoc ((s1 . l),X)) is V11() real integer ext-real set
Exec (((l,X) <=0_goto x),s1) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
IC (Exec (((l,X) <=0_goto x),s1)) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(Exec (((l,X) <=0_goto x),s1)) . (IC ) is set
nl2 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS)
l .--> 0 is V2() Relation-like the U1 of SCMPDS -defined Function-like constant the_Values_of SCMPDS -compatible finite countable set
nl2 +* (l .--> 0) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
l2 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
l2 . l is V11() real integer ext-real set
DataLoc ((l2 . l),X) is Int-like Element of the U1 of SCMPDS
(l2 . l) + X is V11() real integer ext-real set
abs ((l2 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((l2 . l) + X))] is set
{1,(abs ((l2 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((l2 . l) + X))},{1}} is non empty set
(DataLoc ((l2 . l),X)) .--> 0 is V2() Relation-like the U1 of SCMPDS -defined Function-like constant the_Values_of SCMPDS -compatible finite countable set
l2 +* ((DataLoc ((l2 . l),X)) .--> 0) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
s1 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS)
s1 . (DataLoc ((l2 . l),X)) is V11() real integer ext-real set
s1 . l is V11() real integer ext-real set
DataLoc ((s1 . l),X) is Int-like Element of the U1 of SCMPDS
(s1 . l) + X is V11() real integer ext-real set
abs ((s1 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((s1 . l) + X))] is set
{1,(abs ((s1 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((s1 . l) + X))},{1}} is non empty set
s1 . (DataLoc ((s1 . l),X)) is V11() real integer ext-real set
IC s1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
s1 . (IC ) is set
l2 . (IC ) is set
IC nl2 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
nl2 . (IC ) is set
ICplusConst (s1,x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
Exec (((l,X) <=0_goto x),s1) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
IC (Exec (((l,X) <=0_goto x),s1)) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(Exec (((l,X) <=0_goto x),s1)) . (IC ) is set
m1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
m1 + x is V11() real integer ext-real set
abs (m1 + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
l is Int-like Element of the U1 of SCMPDS
x is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
succ x is set
x + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
X is V11() real integer ext-real set
x is V11() real integer ext-real set
(l,X) >=0_goto x is Element of the InstructionsF of SCMPDS
6 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
K194(l,X,x) is set
K109(6,{},K194(l,X,x)) is set
NIC (((l,X) >=0_goto x),x) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
product (the_Values_of SCMPDS) is non empty functional with_common_domain product-like set
{ (IC (Exec (((l,X) >=0_goto x),b₁))) where b₁ is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS) : IC b₁ = x } is set
x + x is V11() real integer ext-real set
abs (x + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
{(succ x),(abs (x + x))} is non empty set
the Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
nl1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
the Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) nl1 -started set is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) nl1 -started set
l1 is set
l2 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS)
Exec (((l,X) >=0_goto x),l2) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
IC (Exec (((l,X) >=0_goto x),l2)) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(Exec (((l,X) >=0_goto x),l2)) . (IC ) is set
IC l2 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
l2 . (IC ) is set
ICplusConst (l2,x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
l2 . l is V11() real integer ext-real set
DataLoc ((l2 . l),X) is Int-like Element of the U1 of SCMPDS
(l2 . l) + X is V11() real integer ext-real set
abs ((l2 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((l2 . l) + X))] is set
{1,(abs ((l2 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((l2 . l) + X))},{1}} is non empty set
l2 . (DataLoc ((l2 . l),X)) is V11() real integer ext-real set
s1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
s1 + x is V11() real integer ext-real set
abs (s1 + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
l2 . l is V11() real integer ext-real set
DataLoc ((l2 . l),X) is Int-like Element of the U1 of SCMPDS
(l2 . l) + X is V11() real integer ext-real set
abs ((l2 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((l2 . l) + X))] is set
{1,(abs ((l2 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((l2 . l) + X))},{1}} is non empty set
l2 . (DataLoc ((l2 . l),X)) is V11() real integer ext-real set
l2 . l is V11() real integer ext-real set
DataLoc ((l2 . l),X) is Int-like Element of the U1 of SCMPDS
(l2 . l) + X is V11() real integer ext-real set
abs ((l2 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((l2 . l) + X))] is set
{1,(abs ((l2 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((l2 . l) + X))},{1}} is non empty set
l2 . (DataLoc ((l2 . l),X)) is V11() real integer ext-real set
l1 is set
- 1 is V11() real integer ext-real non positive set
nl2 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS)
l .--> (- 1) is V2() Relation-like the U1 of SCMPDS -defined Function-like constant the_Values_of SCMPDS -compatible finite countable set
nl2 +* (l .--> (- 1)) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
s1 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS)
s1 . l is V11() real integer ext-real set
DataLoc ((s1 . l),X) is Int-like Element of the U1 of SCMPDS
(s1 . l) + X is V11() real integer ext-real set
abs ((s1 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((s1 . l) + X))] is set
{1,(abs ((s1 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((s1 . l) + X))},{1}} is non empty set
(DataLoc ((s1 . l),X)) .--> (- 1) is V2() Relation-like the U1 of SCMPDS -defined Function-like constant the_Values_of SCMPDS -compatible finite countable set
s1 +* ((DataLoc ((s1 . l),X)) .--> (- 1)) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
m1 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS)
IC m1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
m1 . (IC ) is set
s1 . (IC ) is set
IC nl2 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
nl2 . (IC ) is set
m1 . (DataLoc ((s1 . l),X)) is V11() real integer ext-real set
m1 . l is V11() real integer ext-real set
DataLoc ((m1 . l),X) is Int-like Element of the U1 of SCMPDS
(m1 . l) + X is V11() real integer ext-real set
abs ((m1 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((m1 . l) + X))] is set
{1,(abs ((m1 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((m1 . l) + X))},{1}} is non empty set
m1 . (DataLoc ((m1 . l),X)) is V11() real integer ext-real set
Exec (((l,X) >=0_goto x),m1) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
IC (Exec (((l,X) >=0_goto x),m1)) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(Exec (((l,X) >=0_goto x),m1)) . (IC ) is set
nl2 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS)
- 1 is V11() real integer ext-real non positive set
l .--> (- 1) is V2() Relation-like the U1 of SCMPDS -defined Function-like constant the_Values_of SCMPDS -compatible finite countable set
nl2 +* (l .--> (- 1)) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
l .--> 0 is V2() Relation-like the U1 of SCMPDS -defined Function-like constant the_Values_of SCMPDS -compatible finite countable set
nl2 +* (l .--> 0) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
s1 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS)
s1 . l is V11() real integer ext-real set
DataLoc ((s1 . l),X) is Int-like Element of the U1 of SCMPDS
(s1 . l) + X is V11() real integer ext-real set
abs ((s1 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((s1 . l) + X))] is set
{1,(abs ((s1 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((s1 . l) + X))},{1}} is non empty set
(DataLoc ((s1 . l),X)) .--> 0 is V2() Relation-like the U1 of SCMPDS -defined Function-like constant the_Values_of SCMPDS -compatible finite countable set
s1 +* ((DataLoc ((s1 . l),X)) .--> 0) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
m1 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS)
m1 . (DataLoc ((s1 . l),X)) is V11() real integer ext-real set
m1 . l is V11() real integer ext-real set
DataLoc ((m1 . l),X) is Int-like Element of the U1 of SCMPDS
(m1 . l) + X is V11() real integer ext-real set
abs ((m1 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((m1 . l) + X))] is set
{1,(abs ((m1 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((m1 . l) + X))},{1}} is non empty set
m1 . (DataLoc ((m1 . l),X)) is V11() real integer ext-real set
IC m1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
m1 . (IC ) is set
s1 . (IC ) is set
IC nl2 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
nl2 . (IC ) is set
ICplusConst (m1,x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
Exec (((l,X) >=0_goto x),m1) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
IC (Exec (((l,X) >=0_goto x),m1)) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(Exec (((l,X) >=0_goto x),m1)) . (IC ) is set
s2 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
s2 + x is V11() real integer ext-real set
abs (s2 + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
l is Int-like Element of the U1 of SCMPDS
return l is Element of the InstructionsF of SCMPDS
K192(l) is Relation-like Function-like set
K109(1,{},K192(l)) is set
JUMP (return l) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
{ (NIC ((return l),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
meet { (NIC ((return l),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
{ (NIC ((return l),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
NIC ((return l),0) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
product (the_Values_of SCMPDS) is non empty functional with_common_domain product-like set
{ (IC (Exec ((return l),b₁))) where b₁ is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS) : IC b₁ = 0 } is set
xx is set
i is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
i - 2 is V11() real integer ext-real set
x1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,x1] is set
{1,x1} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,x1},{1}} is non empty set
x1 + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(x1 + 1)] is set
{1,(x1 + 1)} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(x1 + 1)},{1}} is non empty set
the Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
DataLoc (x1,1) is Int-like Element of the U1 of SCMPDS
x1 + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative set
abs (x1 + 1) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs (x1 + 1))] is set
{1,(abs (x1 + 1))} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs (x1 + 1))},{1}} is non empty set
abs (x1 + 1) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs (x1 + 1))] is set
{1,(abs (x1 + 1))} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs (x1 + 1))},{1}} is non empty set
l1 is set
s1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
NIC ((return l),s1) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
{ (IC (Exec ((return l),b₁))) where b₁ is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS) : IC b₁ = s1 } is set
m1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
the Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) m1 -started set is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) m1 -started set
m2 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS)
IC m2 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
m2 . (IC ) is set
l2 is Int-like Element of the U1 of SCMPDS
x is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(l,l2,x1,x) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible set
m2 +* (l,l2,x1,x) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
w2 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS)
w2 . l is V11() real integer ext-real set
w2 . l2 is V11() real integer ext-real set
dom (l,l2,x1,x) is set
{l,l2} is non empty set
IC w2 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
w2 . (IC ) is set
x + 2 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
w2 . (DataLoc (x1,1)) is V11() real integer ext-real set
abs (w2 . (DataLoc (x1,1))) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(abs (w2 . (DataLoc (x1,1)))) + 2 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
Exec ((return l),w2) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
IC (Exec ((return l),w2)) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(Exec ((return l),w2)) . (IC ) is set
l is Int-like Element of the U1 of SCMPDS
return l is Element of the InstructionsF of SCMPDS
K192(l) is Relation-like Function-like set
K109(1,{},K192(l)) is set
JUMP (return l) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
{ (NIC ((return l),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
meet { (NIC ((return l),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
l is Int-like Element of the U1 of SCMPDS
x is V11() real integer ext-real set
saveIC (l,x) is Element of the InstructionsF of SCMPDS
3 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
K193(l,x) is set
K109(3,{},K193(l,x)) is set
JUMP (saveIC (l,x)) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
{ (NIC ((saveIC (l,x)),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
meet { (NIC ((saveIC (l,x)),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
X is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
NIC ((saveIC (l,x)),X) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
product (the_Values_of SCMPDS) is non empty functional with_common_domain product-like set
{ (IC (Exec ((saveIC (l,x)),b₁))) where b₁ is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS) : IC b₁ = X } is set
succ X is set
X + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
{(succ X)} is non empty set
l is Int-like Element of the U1 of SCMPDS
x is V11() real integer ext-real set
l := x is Element of the InstructionsF of SCMPDS
K193(l,x) is set
K109(2,{},K193(l,x)) is set
JUMP (l := x) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
{ (NIC ((l := x),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
meet { (NIC ((l := x),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
X is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
NIC ((l := x),X) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
product (the_Values_of SCMPDS) is non empty functional with_common_domain product-like set
{ (IC (Exec ((l := x),b₁))) where b₁ is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS) : IC b₁ = X } is set
succ X is set
X + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
{(succ X)} is non empty set
l is Int-like Element of the U1 of SCMPDS
x is V11() real integer ext-real set
X is V11() real integer ext-real set
(l,x) := X is Element of the InstructionsF of SCMPDS
7 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
K194(l,x,X) is set
K109(7,{},K194(l,x,X)) is set
JUMP ((l,x) := X) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
{ (NIC (((l,x) := X),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
meet { (NIC (((l,x) := X),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
x is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
NIC (((l,x) := X),x) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
product (the_Values_of SCMPDS) is non empty functional with_common_domain product-like set
{ (IC (Exec (((l,x) := X),b₁))) where b₁ is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS) : IC b₁ = x } is set
succ x is set
x + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
{(succ x)} is non empty set
l is Int-like Element of the U1 of SCMPDS
x is Int-like Element of the U1 of SCMPDS
X is V11() real integer ext-real set
x is V11() real integer ext-real set
(l,X) := (x,x) is Element of the InstructionsF of SCMPDS
JUMP ((l,X) := (x,x)) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
{ (NIC (((l,X) := (x,x)),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
meet { (NIC (((l,X) := (x,x)),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
xx is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
NIC (((l,X) := (x,x)),xx) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
product (the_Values_of SCMPDS) is non empty functional with_common_domain product-like set
{ (IC (Exec (((l,X) := (x,x)),b₁))) where b₁ is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS) : IC b₁ = xx } is set
succ xx is set
xx + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
{(succ xx)} is non empty set
l is Int-like Element of the U1 of SCMPDS
x is V11() real integer ext-real set
X is V11() real integer ext-real set
AddTo (l,x,X) is Element of the InstructionsF of SCMPDS
8 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
K194(l,x,X) is set
K109(8,{},K194(l,x,X)) is set
JUMP (AddTo (l,x,X)) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
{ (NIC ((AddTo (l,x,X)),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
meet { (NIC ((AddTo (l,x,X)),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
x is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
NIC ((AddTo (l,x,X)),x) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
product (the_Values_of SCMPDS) is non empty functional with_common_domain product-like set
{ (IC (Exec ((AddTo (l,x,X)),b₁))) where b₁ is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS) : IC b₁ = x } is set
succ x is set
x + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
{(succ x)} is non empty set
l is Int-like Element of the U1 of SCMPDS
x is Int-like Element of the U1 of SCMPDS
X is V11() real integer ext-real set
x is V11() real integer ext-real set
AddTo (l,X,x,x) is Element of the InstructionsF of SCMPDS
JUMP (AddTo (l,X,x,x)) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
{ (NIC ((AddTo (l,X,x,x)),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
meet { (NIC ((AddTo (l,X,x,x)),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
xx is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
NIC ((AddTo (l,X,x,x)),xx) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
product (the_Values_of SCMPDS) is non empty functional with_common_domain product-like set
{ (IC (Exec ((AddTo (l,X,x,x)),b₁))) where b₁ is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS) : IC b₁ = xx } is set
succ xx is set
xx + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
{(succ xx)} is non empty set
SubFrom (l,X,x,x) is Element of the InstructionsF of SCMPDS
JUMP (SubFrom (l,X,x,x)) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
{ (NIC ((SubFrom (l,X,x,x)),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
meet { (NIC ((SubFrom (l,X,x,x)),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
xx is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
NIC ((SubFrom (l,X,x,x)),xx) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
product (the_Values_of SCMPDS) is non empty functional with_common_domain product-like set
{ (IC (Exec ((SubFrom (l,X,x,x)),b₁))) where b₁ is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS) : IC b₁ = xx } is set
succ xx is set
xx + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
{(succ xx)} is non empty set
MultBy (l,X,x,x) is Element of the InstructionsF of SCMPDS
JUMP (MultBy (l,X,x,x)) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
{ (NIC ((MultBy (l,X,x,x)),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
meet { (NIC ((MultBy (l,X,x,x)),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
xx is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
NIC ((MultBy (l,X,x,x)),xx) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
product (the_Values_of SCMPDS) is non empty functional with_common_domain product-like set
{ (IC (Exec ((MultBy (l,X,x,x)),b₁))) where b₁ is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS) : IC b₁ = xx } is set
succ xx is set
xx + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
{(succ xx)} is non empty set
Divide (l,X,x,x) is Element of the InstructionsF of SCMPDS
JUMP (Divide (l,X,x,x)) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
{ (NIC ((Divide (l,X,x,x)),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
meet { (NIC ((Divide (l,X,x,x)),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
xx is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
NIC ((Divide (l,X,x,x)),xx) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
product (the_Values_of SCMPDS) is non empty functional with_common_domain product-like set
{ (IC (Exec ((Divide (l,X,x,x)),b₁))) where b₁ is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS) : IC b₁ = xx } is set
succ xx is set
xx + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
{(succ xx)} is non empty set
5 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
5 / 3 is V11() real ext-real non negative Element of COMPLEX
5 mod 3 is V11() real integer ext-real set
3 * 1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(3 * 1) + 2 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
4 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
l is V11() real ext-real set
abs l is V11() real ext-real Element of REAL
- l is V11() real ext-real set
(- l) + (abs l) is V11() real ext-real set
((- l) + (abs l)) + 4 is V11() real ext-real set
(abs l) + (((- l) + (abs l)) + 4) is V11() real ext-real set
((abs l) + (((- l) + (abs l)) + 4)) + 2 is V11() real ext-real set
(((abs l) + (((- l) + (abs l)) + 4)) + 2) - 2 is V11() real ext-real set
((((abs l) + (((- l) + (abs l)) + 4)) + 2) - 2) + l is V11() real ext-real set
((abs l) + (((- l) + (abs l)) + 4)) + (((- l) + (abs l)) + 4) is V11() real ext-real set
(((abs l) + (((- l) + (abs l)) + 4)) + (((- l) + (abs l)) + 4)) + 2 is V11() real ext-real set
((((abs l) + (((- l) + (abs l)) + 4)) + (((- l) + (abs l)) + 4)) + 2) - 2 is V11() real ext-real set
(((((abs l) + (((- l) + (abs l)) + 4)) + (((- l) + (abs l)) + 4)) + 2) - 2) + l is V11() real ext-real set
- ((((((abs l) + (((- l) + (abs l)) + 4)) + (((- l) + (abs l)) + 4)) + 2) - 2) + l) is V11() real ext-real set
(((- l) + (abs l)) + 4) + (((- l) + (abs l)) + 4) is V11() real ext-real set
((((- l) + (abs l)) + 4) + (((- l) + (abs l)) + 4)) + (((- l) + (abs l)) + 4) is V11() real ext-real set
- 2 is V11() real integer ext-real non positive set
(- 2) * 0 is empty V11() real integer Function-like functional ext-real non positive non negative V121() V122() V123() V124() V125() V126() V127() set
(- 2) * (((((- l) + (abs l)) + 4) + (((- l) + (abs l)) + 4)) + (((- l) + (abs l)) + 4)) is V11() real ext-real set
0 / 4 is empty V11() real Function-like functional ext-real non positive non negative V121() V122() V123() V124() V125() V126() V127() Element of COMPLEX
((- 2) * (((((- l) + (abs l)) + 4) + (((- l) + (abs l)) + 4)) + (((- l) + (abs l)) + 4))) / 4 is V11() real ext-real Element of COMPLEX
l + (abs l) is V11() real ext-real set
l is V11() real ext-real set
l + 1 is V11() real ext-real set
x is V11() real ext-real set
- x is V11() real ext-real set
abs x is V11() real ext-real Element of REAL
(- x) + (abs x) is V11() real ext-real set
((- x) + (abs x)) + 4 is V11() real ext-real set
(((- x) + (abs x)) + 4) + x is V11() real ext-real set
l + ((((- x) + (abs x)) + 4) + x) is V11() real ext-real set
0 + 3 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(abs x) + 3 is V11() real ext-real set
l is V11() real ext-real set
x is V11() real ext-real set
abs x is V11() real ext-real Element of REAL
(abs x) + l is V11() real ext-real set
((abs x) + l) + 1 is V11() real ext-real set
((abs x) + l) + l is V11() real ext-real set
(((abs x) + l) + l) + x is V11() real ext-real set
- ((((abs x) + l) + l) + x) is V11() real ext-real set
- x is V11() real ext-real set
3 * l is V11() real ext-real set
(- x) + (3 * l) is V11() real ext-real set
((- x) + (3 * l)) + 1 is V11() real ext-real set
l is V11() real ext-real set
x is V11() real integer ext-real set
- x is V11() real integer ext-real set
abs x is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(- x) + (abs x) is V11() real integer ext-real set
((- x) + (abs x)) + 4 is V11() real integer ext-real set
l + (((- x) + (abs x)) + 4) is V11() real ext-real set
(l + (((- x) + (abs x)) + 4)) + 1 is V11() real ext-real set
l + x is V11() real ext-real set
l is V11() real ext-real set
x is V11() real ext-real set
abs x is V11() real ext-real Element of REAL
(abs x) + l is V11() real ext-real set
((abs x) + l) + l is V11() real ext-real set
(((abs x) + l) + l) + 1 is V11() real ext-real set
((abs x) + l) + x is V11() real ext-real set
- (((abs x) + l) + x) is V11() real ext-real set
- x is V11() real ext-real set
l is Int-like Element of the U1 of SCMPDS
x is V11() real integer ext-real set
(l,x) <>0_goto 5 is Element of the InstructionsF of SCMPDS
K194(l,x,5) is set
K109(4,{},K194(l,x,5)) is set
JUMP ((l,x) <>0_goto 5) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
{ (NIC (((l,x) <>0_goto 5),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
meet { (NIC (((l,x) <>0_goto 5),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
{ (NIC (((l,x) <>0_goto 5),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
x1 is set
NIC (((l,x) <>0_goto 5),8) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
product (the_Values_of SCMPDS) is non empty functional with_common_domain product-like set
{ (IC (Exec (((l,x) <>0_goto 5),b₁))) where b₁ is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS) : IC b₁ = 8 } is set
nl2 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS)
Exec (((l,x) <>0_goto 5),nl2) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
IC (Exec (((l,x) <>0_goto 5),nl2)) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(Exec (((l,x) <>0_goto 5),nl2)) . (IC ) is set
IC nl2 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
nl2 . (IC ) is set
NIC (((l,x) <>0_goto 5),5) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
{ (IC (Exec (((l,x) <>0_goto 5),b₁))) where b₁ is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS) : IC b₁ = 5 } is set
l2 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS)
Exec (((l,x) <>0_goto 5),l2) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
IC (Exec (((l,x) <>0_goto 5),l2)) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(Exec (((l,x) <>0_goto 5),l2)) . (IC ) is set
IC l2 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
l2 . (IC ) is set
ICplusConst (nl2,5) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
s1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
s1 + 5 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
abs (s1 + 5) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
ICplusConst (l2,5) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
m1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
m1 + 5 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
abs (m1 + 5) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
l2 . l is V11() real integer ext-real set
DataLoc ((l2 . l),x) is Int-like Element of the U1 of SCMPDS
(l2 . l) + x is V11() real integer ext-real set
abs ((l2 . l) + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((l2 . l) + x))] is set
{1,(abs ((l2 . l) + x))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((l2 . l) + x))},{1}} is non empty set
l2 . (DataLoc ((l2 . l),x)) is V11() real integer ext-real set
nl2 . l is V11() real integer ext-real set
DataLoc ((nl2 . l),x) is Int-like Element of the U1 of SCMPDS
(nl2 . l) + x is V11() real integer ext-real set
abs ((nl2 . l) + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((nl2 . l) + x))] is set
{1,(abs ((nl2 . l) + x))} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((nl2 . l) + x))},{1}} is non empty set
nl2 . (DataLoc ((nl2 . l),x)) is V11() real integer ext-real set
5 + 5 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
8 + 5 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
- (8 + 5) is V11() real integer ext-real non positive set
l2 . l is V11() real integer ext-real set
DataLoc ((l2 . l),x) is Int-like Element of the U1 of SCMPDS
(l2 . l) + x is V11() real integer ext-real set
abs ((l2 . l) + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((l2 . l) + x))] is set
{1,(abs ((l2 . l) + x))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((l2 . l) + x))},{1}} is non empty set
l2 . (DataLoc ((l2 . l),x)) is V11() real integer ext-real set
nl2 . l is V11() real integer ext-real set
DataLoc ((nl2 . l),x) is Int-like Element of the U1 of SCMPDS
(nl2 . l) + x is V11() real integer ext-real set
abs ((nl2 . l) + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((nl2 . l) + x))] is set
{1,(abs ((nl2 . l) + x))} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((nl2 . l) + x))},{1}} is non empty set
nl2 . (DataLoc ((nl2 . l),x)) is V11() real integer ext-real set
succ 8 is set
8 + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
succ 5 is set
5 + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
l2 . l is V11() real integer ext-real set
DataLoc ((l2 . l),x) is Int-like Element of the U1 of SCMPDS
(l2 . l) + x is V11() real integer ext-real set
abs ((l2 . l) + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((l2 . l) + x))] is set
{1,(abs ((l2 . l) + x))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((l2 . l) + x))},{1}} is non empty set
l2 . (DataLoc ((l2 . l),x)) is V11() real integer ext-real set
nl2 . l is V11() real integer ext-real set
DataLoc ((nl2 . l),x) is Int-like Element of the U1 of SCMPDS
(nl2 . l) + x is V11() real integer ext-real set
abs ((nl2 . l) + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((nl2 . l) + x))] is set
{1,(abs ((nl2 . l) + x))} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((nl2 . l) + x))},{1}} is non empty set
nl2 . (DataLoc ((nl2 . l),x)) is V11() real integer ext-real set
s2 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
succ s2 is set
s2 + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
s2 + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
- (s1 + 5) is V11() real integer ext-real non positive set
l2 . l is V11() real integer ext-real set
DataLoc ((l2 . l),x) is Int-like Element of the U1 of SCMPDS
(l2 . l) + x is V11() real integer ext-real set
abs ((l2 . l) + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((l2 . l) + x))] is set
{1,(abs ((l2 . l) + x))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((l2 . l) + x))},{1}} is non empty set
l2 . (DataLoc ((l2 . l),x)) is V11() real integer ext-real set
nl2 . l is V11() real integer ext-real set
DataLoc ((nl2 . l),x) is Int-like Element of the U1 of SCMPDS
(nl2 . l) + x is V11() real integer ext-real set
abs ((nl2 . l) + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((nl2 . l) + x))] is set
{1,(abs ((nl2 . l) + x))} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((nl2 . l) + x))},{1}} is non empty set
nl2 . (DataLoc ((nl2 . l),x)) is V11() real integer ext-real set
s2 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
succ s2 is set
s2 + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
s2 + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
- (m1 + 5) is V11() real integer ext-real non positive set
l2 . l is V11() real integer ext-real set
DataLoc ((l2 . l),x) is Int-like Element of the U1 of SCMPDS
(l2 . l) + x is V11() real integer ext-real set
abs ((l2 . l) + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((l2 . l) + x))] is set
{1,(abs ((l2 . l) + x))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((l2 . l) + x))},{1}} is non empty set
l2 . (DataLoc ((l2 . l),x)) is V11() real integer ext-real set
nl2 . l is V11() real integer ext-real set
DataLoc ((nl2 . l),x) is Int-like Element of the U1 of SCMPDS
(nl2 . l) + x is V11() real integer ext-real set
abs ((nl2 . l) + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((nl2 . l) + x))] is set
{1,(abs ((nl2 . l) + x))} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((nl2 . l) + x))},{1}} is non empty set
nl2 . (DataLoc ((nl2 . l),x)) is V11() real integer ext-real set
l is Int-like Element of the U1 of SCMPDS
x is V11() real integer ext-real set
X is V11() real integer ext-real set
(l,X) <>0_goto x is Element of the InstructionsF of SCMPDS
K194(l,X,x) is set
K109(4,{},K194(l,X,x)) is set
JUMP ((l,X) <>0_goto x) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
{ (NIC (((l,X) <>0_goto x),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
meet { (NIC (((l,X) <>0_goto x),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
{ (NIC (((l,X) <>0_goto x),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
- x is V11() real integer ext-real set
abs x is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(- x) + (abs x) is V11() real integer ext-real set
((- x) + (abs x)) + 4 is V11() real integer ext-real set
x is set
((- x) + (abs x)) + 0 is V11() real integer ext-real set
x1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(abs x) + x1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
((abs x) + x1) + x1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
NIC (((l,X) <>0_goto x),((abs x) + x1)) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
product (the_Values_of SCMPDS) is non empty functional with_common_domain product-like set
{ (IC (Exec (((l,X) <>0_goto x),b₁))) where b₁ is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS) : IC b₁ = (abs x) + x1 } is set
s1 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS)
Exec (((l,X) <>0_goto x),s1) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
IC (Exec (((l,X) <>0_goto x),s1)) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(Exec (((l,X) <>0_goto x),s1)) . (IC ) is set
IC s1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
s1 . (IC ) is set
ICplusConst (s1,x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
m1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
m1 + x is V11() real integer ext-real set
abs (m1 + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
NIC (((l,X) <>0_goto x),(((abs x) + x1) + x1)) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
{ (IC (Exec (((l,X) <>0_goto x),b₁))) where b₁ is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS) : IC b₁ = ((abs x) + x1) + x1 } is set
s2 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS)
Exec (((l,X) <>0_goto x),s2) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
IC (Exec (((l,X) <>0_goto x),s2)) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(Exec (((l,X) <>0_goto x),s2)) . (IC ) is set
IC s2 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
s2 . (IC ) is set
ICplusConst (s2,x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
m2 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
m2 + x is V11() real integer ext-real set
abs (m2 + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
s1 . l is V11() real integer ext-real set
DataLoc ((s1 . l),X) is Int-like Element of the U1 of SCMPDS
(s1 . l) + X is V11() real integer ext-real set
abs ((s1 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((s1 . l) + X))] is set
{1,(abs ((s1 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((s1 . l) + X))},{1}} is non empty set
s1 . (DataLoc ((s1 . l),X)) is V11() real integer ext-real set
s2 . l is V11() real integer ext-real set
DataLoc ((s2 . l),X) is Int-like Element of the U1 of SCMPDS
(s2 . l) + X is V11() real integer ext-real set
abs ((s2 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((s2 . l) + X))] is set
{1,(abs ((s2 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((s2 . l) + X))},{1}} is non empty set
s2 . (DataLoc ((s2 . l),X)) is V11() real integer ext-real set
((abs x) + x1) + 2 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(((abs x) + x1) + 2) - 2 is V11() real integer ext-real set
((((abs x) + x1) + 2) - 2) + x is V11() real integer ext-real set
(((abs x) + x1) + x1) + 2 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
((((abs x) + x1) + x1) + 2) - 2 is V11() real integer ext-real set
(((((abs x) + x1) + x1) + 2) - 2) + x is V11() real integer ext-real set
((abs x) + x1) + 2 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(((abs x) + x1) + 2) - 2 is V11() real integer ext-real set
((((abs x) + x1) + 2) - 2) + x is V11() real integer ext-real set
(((abs x) + x1) + x1) + 2 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
((((abs x) + x1) + x1) + 2) - 2 is V11() real integer ext-real set
(((((abs x) + x1) + x1) + 2) - 2) + x is V11() real integer ext-real set
- ((((((abs x) + x1) + x1) + 2) - 2) + x) is V11() real integer ext-real set
((abs x) + x1) + 2 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(((abs x) + x1) + 2) - 2 is V11() real integer ext-real set
((((abs x) + x1) + 2) - 2) + x is V11() real integer ext-real set
(((abs x) + x1) + x1) + 2 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
((((abs x) + x1) + x1) + 2) - 2 is V11() real integer ext-real set
(((((abs x) + x1) + x1) + 2) - 2) + x is V11() real integer ext-real set
- ((((((abs x) + x1) + x1) + 2) - 2) + x) is V11() real integer ext-real set
s1 . l is V11() real integer ext-real set
DataLoc ((s1 . l),X) is Int-like Element of the U1 of SCMPDS
(s1 . l) + X is V11() real integer ext-real set
abs ((s1 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((s1 . l) + X))] is set
{1,(abs ((s1 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((s1 . l) + X))},{1}} is non empty set
s1 . (DataLoc ((s1 . l),X)) is V11() real integer ext-real set
s2 . l is V11() real integer ext-real set
DataLoc ((s2 . l),X) is Int-like Element of the U1 of SCMPDS
(s2 . l) + X is V11() real integer ext-real set
abs ((s2 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((s2 . l) + X))] is set
{1,(abs ((s2 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((s2 . l) + X))},{1}} is non empty set
s2 . (DataLoc ((s2 . l),X)) is V11() real integer ext-real set
succ (((abs x) + x1) + x1) is set
(((abs x) + x1) + x1) + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
succ ((abs x) + x1) is set
((abs x) + x1) + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
s1 . l is V11() real integer ext-real set
DataLoc ((s1 . l),X) is Int-like Element of the U1 of SCMPDS
(s1 . l) + X is V11() real integer ext-real set
abs ((s1 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((s1 . l) + X))] is set
{1,(abs ((s1 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((s1 . l) + X))},{1}} is non empty set
s1 . (DataLoc ((s1 . l),X)) is V11() real integer ext-real set
s2 . l is V11() real integer ext-real set
DataLoc ((s2 . l),X) is Int-like Element of the U1 of SCMPDS
(s2 . l) + X is V11() real integer ext-real set
abs ((s2 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((s2 . l) + X))] is set
{1,(abs ((s2 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((s2 . l) + X))},{1}} is non empty set
s2 . (DataLoc ((s2 . l),X)) is V11() real integer ext-real set
n2 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
succ n2 is set
n2 + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
n2 + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
((abs x) + x1) + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
x1 + x is V11() real integer ext-real set
((abs x) + x1) + (x1 + x) is V11() real integer ext-real set
- (m2 + x) is V11() real integer ext-real set
- (m2 + x) is V11() real integer ext-real set
s1 . l is V11() real integer ext-real set
DataLoc ((s1 . l),X) is Int-like Element of the U1 of SCMPDS
(s1 . l) + X is V11() real integer ext-real set
abs ((s1 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((s1 . l) + X))] is set
{1,(abs ((s1 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((s1 . l) + X))},{1}} is non empty set
s1 . (DataLoc ((s1 . l),X)) is V11() real integer ext-real set
s2 . l is V11() real integer ext-real set
DataLoc ((s2 . l),X) is Int-like Element of the U1 of SCMPDS
(s2 . l) + X is V11() real integer ext-real set
abs ((s2 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((s2 . l) + X))] is set
{1,(abs ((s2 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((s2 . l) + X))},{1}} is non empty set
s2 . (DataLoc ((s2 . l),X)) is V11() real integer ext-real set
n2 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
succ n2 is set
n2 + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
n2 + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
- (m1 + x) is V11() real integer ext-real set
- (m1 + x) is V11() real integer ext-real set
s1 . l is V11() real integer ext-real set
DataLoc ((s1 . l),X) is Int-like Element of the U1 of SCMPDS
(s1 . l) + X is V11() real integer ext-real set
abs ((s1 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((s1 . l) + X))] is set
{1,(abs ((s1 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((s1 . l) + X))},{1}} is non empty set
s1 . (DataLoc ((s1 . l),X)) is V11() real integer ext-real set
s2 . l is V11() real integer ext-real set
DataLoc ((s2 . l),X) is Int-like Element of the U1 of SCMPDS
(s2 . l) + X is V11() real integer ext-real set
abs ((s2 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((s2 . l) + X))] is set
{1,(abs ((s2 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((s2 . l) + X))},{1}} is non empty set
s2 . (DataLoc ((s2 . l),X)) is V11() real integer ext-real set
l is Int-like Element of the U1 of SCMPDS
x is V11() real integer ext-real set
(l,x) <=0_goto 5 is Element of the InstructionsF of SCMPDS
K194(l,x,5) is set
K109(5,{},K194(l,x,5)) is set
JUMP ((l,x) <=0_goto 5) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
{ (NIC (((l,x) <=0_goto 5),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
meet { (NIC (((l,x) <=0_goto 5),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
{ (NIC (((l,x) <=0_goto 5),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
x1 is set
NIC (((l,x) <=0_goto 5),8) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
product (the_Values_of SCMPDS) is non empty functional with_common_domain product-like set
{ (IC (Exec (((l,x) <=0_goto 5),b₁))) where b₁ is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS) : IC b₁ = 8 } is set
nl2 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS)
Exec (((l,x) <=0_goto 5),nl2) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
IC (Exec (((l,x) <=0_goto 5),nl2)) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(Exec (((l,x) <=0_goto 5),nl2)) . (IC ) is set
IC nl2 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
nl2 . (IC ) is set
NIC (((l,x) <=0_goto 5),5) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
{ (IC (Exec (((l,x) <=0_goto 5),b₁))) where b₁ is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS) : IC b₁ = 5 } is set
l2 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS)
Exec (((l,x) <=0_goto 5),l2) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
IC (Exec (((l,x) <=0_goto 5),l2)) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(Exec (((l,x) <=0_goto 5),l2)) . (IC ) is set
IC l2 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
l2 . (IC ) is set
ICplusConst (nl2,5) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
s1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
s1 + 5 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
abs (s1 + 5) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
ICplusConst (l2,5) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
m1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
m1 + 5 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
abs (m1 + 5) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
l2 . l is V11() real integer ext-real set
DataLoc ((l2 . l),x) is Int-like Element of the U1 of SCMPDS
(l2 . l) + x is V11() real integer ext-real set
abs ((l2 . l) + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((l2 . l) + x))] is set
{1,(abs ((l2 . l) + x))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((l2 . l) + x))},{1}} is non empty set
l2 . (DataLoc ((l2 . l),x)) is V11() real integer ext-real set
nl2 . l is V11() real integer ext-real set
DataLoc ((nl2 . l),x) is Int-like Element of the U1 of SCMPDS
(nl2 . l) + x is V11() real integer ext-real set
abs ((nl2 . l) + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((nl2 . l) + x))] is set
{1,(abs ((nl2 . l) + x))} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((nl2 . l) + x))},{1}} is non empty set
nl2 . (DataLoc ((nl2 . l),x)) is V11() real integer ext-real set
5 + 5 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
8 + 5 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
- (8 + 5) is V11() real integer ext-real non positive set
l2 . l is V11() real integer ext-real set
DataLoc ((l2 . l),x) is Int-like Element of the U1 of SCMPDS
(l2 . l) + x is V11() real integer ext-real set
abs ((l2 . l) + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((l2 . l) + x))] is set
{1,(abs ((l2 . l) + x))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((l2 . l) + x))},{1}} is non empty set
l2 . (DataLoc ((l2 . l),x)) is V11() real integer ext-real set
nl2 . l is V11() real integer ext-real set
DataLoc ((nl2 . l),x) is Int-like Element of the U1 of SCMPDS
(nl2 . l) + x is V11() real integer ext-real set
abs ((nl2 . l) + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((nl2 . l) + x))] is set
{1,(abs ((nl2 . l) + x))} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((nl2 . l) + x))},{1}} is non empty set
nl2 . (DataLoc ((nl2 . l),x)) is V11() real integer ext-real set
succ 8 is set
8 + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
succ 5 is set
5 + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
l2 . l is V11() real integer ext-real set
DataLoc ((l2 . l),x) is Int-like Element of the U1 of SCMPDS
(l2 . l) + x is V11() real integer ext-real set
abs ((l2 . l) + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((l2 . l) + x))] is set
{1,(abs ((l2 . l) + x))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((l2 . l) + x))},{1}} is non empty set
l2 . (DataLoc ((l2 . l),x)) is V11() real integer ext-real set
nl2 . l is V11() real integer ext-real set
DataLoc ((nl2 . l),x) is Int-like Element of the U1 of SCMPDS
(nl2 . l) + x is V11() real integer ext-real set
abs ((nl2 . l) + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((nl2 . l) + x))] is set
{1,(abs ((nl2 . l) + x))} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((nl2 . l) + x))},{1}} is non empty set
nl2 . (DataLoc ((nl2 . l),x)) is V11() real integer ext-real set
s2 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
succ s2 is set
s2 + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
s2 + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
- (s1 + 5) is V11() real integer ext-real non positive set
l2 . l is V11() real integer ext-real set
DataLoc ((l2 . l),x) is Int-like Element of the U1 of SCMPDS
(l2 . l) + x is V11() real integer ext-real set
abs ((l2 . l) + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((l2 . l) + x))] is set
{1,(abs ((l2 . l) + x))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((l2 . l) + x))},{1}} is non empty set
l2 . (DataLoc ((l2 . l),x)) is V11() real integer ext-real set
nl2 . l is V11() real integer ext-real set
DataLoc ((nl2 . l),x) is Int-like Element of the U1 of SCMPDS
(nl2 . l) + x is V11() real integer ext-real set
abs ((nl2 . l) + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((nl2 . l) + x))] is set
{1,(abs ((nl2 . l) + x))} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((nl2 . l) + x))},{1}} is non empty set
nl2 . (DataLoc ((nl2 . l),x)) is V11() real integer ext-real set
s2 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
succ s2 is set
s2 + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
s2 + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
- (m1 + 5) is V11() real integer ext-real non positive set
l2 . l is V11() real integer ext-real set
DataLoc ((l2 . l),x) is Int-like Element of the U1 of SCMPDS
(l2 . l) + x is V11() real integer ext-real set
abs ((l2 . l) + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((l2 . l) + x))] is set
{1,(abs ((l2 . l) + x))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((l2 . l) + x))},{1}} is non empty set
l2 . (DataLoc ((l2 . l),x)) is V11() real integer ext-real set
nl2 . l is V11() real integer ext-real set
DataLoc ((nl2 . l),x) is Int-like Element of the U1 of SCMPDS
(nl2 . l) + x is V11() real integer ext-real set
abs ((nl2 . l) + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((nl2 . l) + x))] is set
{1,(abs ((nl2 . l) + x))} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((nl2 . l) + x))},{1}} is non empty set
nl2 . (DataLoc ((nl2 . l),x)) is V11() real integer ext-real set
l is Int-like Element of the U1 of SCMPDS
x is V11() real integer ext-real set
X is V11() real integer ext-real set
(l,X) <=0_goto x is Element of the InstructionsF of SCMPDS
K194(l,X,x) is set
K109(5,{},K194(l,X,x)) is set
JUMP ((l,X) <=0_goto x) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
{ (NIC (((l,X) <=0_goto x),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
meet { (NIC (((l,X) <=0_goto x),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
{ (NIC (((l,X) <=0_goto x),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
- x is V11() real integer ext-real set
abs x is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(- x) + (abs x) is V11() real integer ext-real set
((- x) + (abs x)) + 4 is V11() real integer ext-real set
x is set
((- x) + (abs x)) + 0 is V11() real integer ext-real set
x1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(abs x) + x1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
((abs x) + x1) + x1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
NIC (((l,X) <=0_goto x),((abs x) + x1)) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
product (the_Values_of SCMPDS) is non empty functional with_common_domain product-like set
{ (IC (Exec (((l,X) <=0_goto x),b₁))) where b₁ is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS) : IC b₁ = (abs x) + x1 } is set
s1 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS)
Exec (((l,X) <=0_goto x),s1) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
IC (Exec (((l,X) <=0_goto x),s1)) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(Exec (((l,X) <=0_goto x),s1)) . (IC ) is set
IC s1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
s1 . (IC ) is set
ICplusConst (s1,x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
m1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
m1 + x is V11() real integer ext-real set
abs (m1 + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
NIC (((l,X) <=0_goto x),(((abs x) + x1) + x1)) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
{ (IC (Exec (((l,X) <=0_goto x),b₁))) where b₁ is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS) : IC b₁ = ((abs x) + x1) + x1 } is set
s2 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS)
Exec (((l,X) <=0_goto x),s2) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
IC (Exec (((l,X) <=0_goto x),s2)) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(Exec (((l,X) <=0_goto x),s2)) . (IC ) is set
IC s2 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
s2 . (IC ) is set
ICplusConst (s2,x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
m2 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
m2 + x is V11() real integer ext-real set
abs (m2 + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
s1 . l is V11() real integer ext-real set
DataLoc ((s1 . l),X) is Int-like Element of the U1 of SCMPDS
(s1 . l) + X is V11() real integer ext-real set
abs ((s1 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((s1 . l) + X))] is set
{1,(abs ((s1 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((s1 . l) + X))},{1}} is non empty set
s1 . (DataLoc ((s1 . l),X)) is V11() real integer ext-real set
s2 . l is V11() real integer ext-real set
DataLoc ((s2 . l),X) is Int-like Element of the U1 of SCMPDS
(s2 . l) + X is V11() real integer ext-real set
abs ((s2 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((s2 . l) + X))] is set
{1,(abs ((s2 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((s2 . l) + X))},{1}} is non empty set
s2 . (DataLoc ((s2 . l),X)) is V11() real integer ext-real set
((abs x) + x1) + x is V11() real integer ext-real set
(((abs x) + x1) + x1) + x is V11() real integer ext-real set
((abs x) + x1) + 2 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(((abs x) + x1) + 2) - 2 is V11() real integer ext-real set
((((abs x) + x1) + 2) - 2) + x is V11() real integer ext-real set
(((abs x) + x1) + x1) + 2 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
((((abs x) + x1) + x1) + 2) - 2 is V11() real integer ext-real set
(((((abs x) + x1) + x1) + 2) - 2) + x is V11() real integer ext-real set
- ((((((abs x) + x1) + x1) + 2) - 2) + x) is V11() real integer ext-real set
((abs x) + x1) + x is V11() real integer ext-real set
(((abs x) + x1) + x1) + x is V11() real integer ext-real set
((abs x) + x1) + 2 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(((abs x) + x1) + 2) - 2 is V11() real integer ext-real set
((((abs x) + x1) + 2) - 2) + x is V11() real integer ext-real set
(((abs x) + x1) + x1) + 2 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
((((abs x) + x1) + x1) + 2) - 2 is V11() real integer ext-real set
(((((abs x) + x1) + x1) + 2) - 2) + x is V11() real integer ext-real set
- ((((((abs x) + x1) + x1) + 2) - 2) + x) is V11() real integer ext-real set
s1 . l is V11() real integer ext-real set
DataLoc ((s1 . l),X) is Int-like Element of the U1 of SCMPDS
(s1 . l) + X is V11() real integer ext-real set
abs ((s1 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((s1 . l) + X))] is set
{1,(abs ((s1 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((s1 . l) + X))},{1}} is non empty set
s1 . (DataLoc ((s1 . l),X)) is V11() real integer ext-real set
s2 . l is V11() real integer ext-real set
DataLoc ((s2 . l),X) is Int-like Element of the U1 of SCMPDS
(s2 . l) + X is V11() real integer ext-real set
abs ((s2 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((s2 . l) + X))] is set
{1,(abs ((s2 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((s2 . l) + X))},{1}} is non empty set
s2 . (DataLoc ((s2 . l),X)) is V11() real integer ext-real set
succ (((abs x) + x1) + x1) is set
(((abs x) + x1) + x1) + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
succ ((abs x) + x1) is set
((abs x) + x1) + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
s1 . l is V11() real integer ext-real set
DataLoc ((s1 . l),X) is Int-like Element of the U1 of SCMPDS
(s1 . l) + X is V11() real integer ext-real set
abs ((s1 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((s1 . l) + X))] is set
{1,(abs ((s1 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((s1 . l) + X))},{1}} is non empty set
s1 . (DataLoc ((s1 . l),X)) is V11() real integer ext-real set
s2 . l is V11() real integer ext-real set
DataLoc ((s2 . l),X) is Int-like Element of the U1 of SCMPDS
(s2 . l) + X is V11() real integer ext-real set
abs ((s2 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((s2 . l) + X))] is set
{1,(abs ((s2 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((s2 . l) + X))},{1}} is non empty set
s2 . (DataLoc ((s2 . l),X)) is V11() real integer ext-real set
n2 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
succ n2 is set
n2 + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
n2 + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
((abs x) + x1) + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
x1 + x is V11() real integer ext-real set
((abs x) + x1) + (x1 + x) is V11() real integer ext-real set
- (m2 + x) is V11() real integer ext-real set
- (m2 + x) is V11() real integer ext-real set
s1 . l is V11() real integer ext-real set
DataLoc ((s1 . l),X) is Int-like Element of the U1 of SCMPDS
(s1 . l) + X is V11() real integer ext-real set
abs ((s1 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((s1 . l) + X))] is set
{1,(abs ((s1 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((s1 . l) + X))},{1}} is non empty set
s1 . (DataLoc ((s1 . l),X)) is V11() real integer ext-real set
s2 . l is V11() real integer ext-real set
DataLoc ((s2 . l),X) is Int-like Element of the U1 of SCMPDS
(s2 . l) + X is V11() real integer ext-real set
abs ((s2 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((s2 . l) + X))] is set
{1,(abs ((s2 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((s2 . l) + X))},{1}} is non empty set
s2 . (DataLoc ((s2 . l),X)) is V11() real integer ext-real set
n2 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
succ n2 is set
n2 + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
n2 + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
- (m1 + x) is V11() real integer ext-real set
- (m1 + x) is V11() real integer ext-real set
s1 . l is V11() real integer ext-real set
DataLoc ((s1 . l),X) is Int-like Element of the U1 of SCMPDS
(s1 . l) + X is V11() real integer ext-real set
abs ((s1 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((s1 . l) + X))] is set
{1,(abs ((s1 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((s1 . l) + X))},{1}} is non empty set
s1 . (DataLoc ((s1 . l),X)) is V11() real integer ext-real set
s2 . l is V11() real integer ext-real set
DataLoc ((s2 . l),X) is Int-like Element of the U1 of SCMPDS
(s2 . l) + X is V11() real integer ext-real set
abs ((s2 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((s2 . l) + X))] is set
{1,(abs ((s2 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((s2 . l) + X))},{1}} is non empty set
s2 . (DataLoc ((s2 . l),X)) is V11() real integer ext-real set
l is Int-like Element of the U1 of SCMPDS
x is V11() real integer ext-real set
(l,x) >=0_goto 5 is Element of the InstructionsF of SCMPDS
6 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
K194(l,x,5) is set
K109(6,{},K194(l,x,5)) is set
JUMP ((l,x) >=0_goto 5) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
{ (NIC (((l,x) >=0_goto 5),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
meet { (NIC (((l,x) >=0_goto 5),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
{ (NIC (((l,x) >=0_goto 5),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
x1 is set
NIC (((l,x) >=0_goto 5),8) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
product (the_Values_of SCMPDS) is non empty functional with_common_domain product-like set
{ (IC (Exec (((l,x) >=0_goto 5),b₁))) where b₁ is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS) : IC b₁ = 8 } is set
nl2 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS)
Exec (((l,x) >=0_goto 5),nl2) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
IC (Exec (((l,x) >=0_goto 5),nl2)) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(Exec (((l,x) >=0_goto 5),nl2)) . (IC ) is set
IC nl2 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
nl2 . (IC ) is set
NIC (((l,x) >=0_goto 5),5) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
{ (IC (Exec (((l,x) >=0_goto 5),b₁))) where b₁ is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS) : IC b₁ = 5 } is set
l2 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS)
Exec (((l,x) >=0_goto 5),l2) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
IC (Exec (((l,x) >=0_goto 5),l2)) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(Exec (((l,x) >=0_goto 5),l2)) . (IC ) is set
IC l2 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
l2 . (IC ) is set
ICplusConst (nl2,5) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
s1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
s1 + 5 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
abs (s1 + 5) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
ICplusConst (l2,5) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
m1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
m1 + 5 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
abs (m1 + 5) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
l2 . l is V11() real integer ext-real set
DataLoc ((l2 . l),x) is Int-like Element of the U1 of SCMPDS
(l2 . l) + x is V11() real integer ext-real set
abs ((l2 . l) + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((l2 . l) + x))] is set
{1,(abs ((l2 . l) + x))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((l2 . l) + x))},{1}} is non empty set
l2 . (DataLoc ((l2 . l),x)) is V11() real integer ext-real set
nl2 . l is V11() real integer ext-real set
DataLoc ((nl2 . l),x) is Int-like Element of the U1 of SCMPDS
(nl2 . l) + x is V11() real integer ext-real set
abs ((nl2 . l) + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((nl2 . l) + x))] is set
{1,(abs ((nl2 . l) + x))} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((nl2 . l) + x))},{1}} is non empty set
nl2 . (DataLoc ((nl2 . l),x)) is V11() real integer ext-real set
5 + 2 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(5 + 2) - 2 is V11() real integer ext-real set
((5 + 2) - 2) + 5 is V11() real integer ext-real set
8 + 2 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(8 + 2) - 2 is V11() real integer ext-real set
((8 + 2) - 2) + 5 is V11() real integer ext-real set
- (((8 + 2) - 2) + 5) is V11() real integer ext-real set
l2 . l is V11() real integer ext-real set
DataLoc ((l2 . l),x) is Int-like Element of the U1 of SCMPDS
(l2 . l) + x is V11() real integer ext-real set
abs ((l2 . l) + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((l2 . l) + x))] is set
{1,(abs ((l2 . l) + x))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((l2 . l) + x))},{1}} is non empty set
l2 . (DataLoc ((l2 . l),x)) is V11() real integer ext-real set
nl2 . l is V11() real integer ext-real set
DataLoc ((nl2 . l),x) is Int-like Element of the U1 of SCMPDS
(nl2 . l) + x is V11() real integer ext-real set
abs ((nl2 . l) + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((nl2 . l) + x))] is set
{1,(abs ((nl2 . l) + x))} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((nl2 . l) + x))},{1}} is non empty set
nl2 . (DataLoc ((nl2 . l),x)) is V11() real integer ext-real set
succ 8 is set
8 + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
succ 5 is set
5 + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
l2 . l is V11() real integer ext-real set
DataLoc ((l2 . l),x) is Int-like Element of the U1 of SCMPDS
(l2 . l) + x is V11() real integer ext-real set
abs ((l2 . l) + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((l2 . l) + x))] is set
{1,(abs ((l2 . l) + x))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((l2 . l) + x))},{1}} is non empty set
l2 . (DataLoc ((l2 . l),x)) is V11() real integer ext-real set
nl2 . l is V11() real integer ext-real set
DataLoc ((nl2 . l),x) is Int-like Element of the U1 of SCMPDS
(nl2 . l) + x is V11() real integer ext-real set
abs ((nl2 . l) + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((nl2 . l) + x))] is set
{1,(abs ((nl2 . l) + x))} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((nl2 . l) + x))},{1}} is non empty set
nl2 . (DataLoc ((nl2 . l),x)) is V11() real integer ext-real set
s2 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
succ s2 is set
s2 + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
s2 + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
- (s1 + 5) is V11() real integer ext-real non positive set
l2 . l is V11() real integer ext-real set
DataLoc ((l2 . l),x) is Int-like Element of the U1 of SCMPDS
(l2 . l) + x is V11() real integer ext-real set
abs ((l2 . l) + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((l2 . l) + x))] is set
{1,(abs ((l2 . l) + x))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((l2 . l) + x))},{1}} is non empty set
l2 . (DataLoc ((l2 . l),x)) is V11() real integer ext-real set
nl2 . l is V11() real integer ext-real set
DataLoc ((nl2 . l),x) is Int-like Element of the U1 of SCMPDS
(nl2 . l) + x is V11() real integer ext-real set
abs ((nl2 . l) + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((nl2 . l) + x))] is set
{1,(abs ((nl2 . l) + x))} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((nl2 . l) + x))},{1}} is non empty set
nl2 . (DataLoc ((nl2 . l),x)) is V11() real integer ext-real set
s2 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
succ s2 is set
s2 + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
s2 + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
- (m1 + 5) is V11() real integer ext-real non positive set
l2 . l is V11() real integer ext-real set
DataLoc ((l2 . l),x) is Int-like Element of the U1 of SCMPDS
(l2 . l) + x is V11() real integer ext-real set
abs ((l2 . l) + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((l2 . l) + x))] is set
{1,(abs ((l2 . l) + x))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((l2 . l) + x))},{1}} is non empty set
l2 . (DataLoc ((l2 . l),x)) is V11() real integer ext-real set
nl2 . l is V11() real integer ext-real set
DataLoc ((nl2 . l),x) is Int-like Element of the U1 of SCMPDS
(nl2 . l) + x is V11() real integer ext-real set
abs ((nl2 . l) + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((nl2 . l) + x))] is set
{1,(abs ((nl2 . l) + x))} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((nl2 . l) + x))},{1}} is non empty set
nl2 . (DataLoc ((nl2 . l),x)) is V11() real integer ext-real set
l is Int-like Element of the U1 of SCMPDS
x is V11() real integer ext-real set
X is V11() real integer ext-real set
(l,X) >=0_goto x is Element of the InstructionsF of SCMPDS
6 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
K194(l,X,x) is set
K109(6,{},K194(l,X,x)) is set
JUMP ((l,X) >=0_goto x) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
{ (NIC (((l,X) >=0_goto x),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
meet { (NIC (((l,X) >=0_goto x),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
{ (NIC (((l,X) >=0_goto x),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
- x is V11() real integer ext-real set
abs x is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(- x) + (abs x) is V11() real integer ext-real set
((- x) + (abs x)) + 4 is V11() real integer ext-real set
x is set
((- x) + (abs x)) + 0 is V11() real integer ext-real set
x1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(abs x) + x1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
((abs x) + x1) + x1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
NIC (((l,X) >=0_goto x),((abs x) + x1)) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
product (the_Values_of SCMPDS) is non empty functional with_common_domain product-like set
{ (IC (Exec (((l,X) >=0_goto x),b₁))) where b₁ is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS) : IC b₁ = (abs x) + x1 } is set
s1 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS)
Exec (((l,X) >=0_goto x),s1) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
IC (Exec (((l,X) >=0_goto x),s1)) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(Exec (((l,X) >=0_goto x),s1)) . (IC ) is set
IC s1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
s1 . (IC ) is set
ICplusConst (s1,x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
m1 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
m1 + x is V11() real integer ext-real set
abs (m1 + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
NIC (((l,X) >=0_goto x),(((abs x) + x1) + x1)) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
{ (IC (Exec (((l,X) >=0_goto x),b₁))) where b₁ is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS) : IC b₁ = ((abs x) + x1) + x1 } is set
s2 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS)
Exec (((l,X) >=0_goto x),s2) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) set
IC (Exec (((l,X) >=0_goto x),s2)) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(Exec (((l,X) >=0_goto x),s2)) . (IC ) is set
IC s2 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
s2 . (IC ) is set
ICplusConst (s2,x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
m2 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
m2 + x is V11() real integer ext-real set
abs (m2 + x) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
s1 . l is V11() real integer ext-real set
DataLoc ((s1 . l),X) is Int-like Element of the U1 of SCMPDS
(s1 . l) + X is V11() real integer ext-real set
abs ((s1 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((s1 . l) + X))] is set
{1,(abs ((s1 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((s1 . l) + X))},{1}} is non empty set
s1 . (DataLoc ((s1 . l),X)) is V11() real integer ext-real set
s2 . l is V11() real integer ext-real set
DataLoc ((s2 . l),X) is Int-like Element of the U1 of SCMPDS
(s2 . l) + X is V11() real integer ext-real set
abs ((s2 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((s2 . l) + X))] is set
{1,(abs ((s2 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((s2 . l) + X))},{1}} is non empty set
s2 . (DataLoc ((s2 . l),X)) is V11() real integer ext-real set
((abs x) + x1) + 2 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(((abs x) + x1) + 2) - 2 is V11() real integer ext-real set
((((abs x) + x1) + 2) - 2) + x is V11() real integer ext-real set
(((abs x) + x1) + x1) + 2 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
((((abs x) + x1) + x1) + 2) - 2 is V11() real integer ext-real set
(((((abs x) + x1) + x1) + 2) - 2) + x is V11() real integer ext-real set
((abs x) + x1) + 2 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(((abs x) + x1) + 2) - 2 is V11() real integer ext-real set
((((abs x) + x1) + 2) - 2) + x is V11() real integer ext-real set
(((abs x) + x1) + x1) + 2 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
((((abs x) + x1) + x1) + 2) - 2 is V11() real integer ext-real set
(((((abs x) + x1) + x1) + 2) - 2) + x is V11() real integer ext-real set
- ((((((abs x) + x1) + x1) + 2) - 2) + x) is V11() real integer ext-real set
((abs x) + x1) + 2 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
(((abs x) + x1) + 2) - 2 is V11() real integer ext-real set
((((abs x) + x1) + 2) - 2) + x is V11() real integer ext-real set
(((abs x) + x1) + x1) + 2 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
((((abs x) + x1) + x1) + 2) - 2 is V11() real integer ext-real set
(((((abs x) + x1) + x1) + 2) - 2) + x is V11() real integer ext-real set
- ((((((abs x) + x1) + x1) + 2) - 2) + x) is V11() real integer ext-real set
s1 . l is V11() real integer ext-real set
DataLoc ((s1 . l),X) is Int-like Element of the U1 of SCMPDS
(s1 . l) + X is V11() real integer ext-real set
abs ((s1 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((s1 . l) + X))] is set
{1,(abs ((s1 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((s1 . l) + X))},{1}} is non empty set
s1 . (DataLoc ((s1 . l),X)) is V11() real integer ext-real set
s2 . l is V11() real integer ext-real set
DataLoc ((s2 . l),X) is Int-like Element of the U1 of SCMPDS
(s2 . l) + X is V11() real integer ext-real set
abs ((s2 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((s2 . l) + X))] is set
{1,(abs ((s2 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((s2 . l) + X))},{1}} is non empty set
s2 . (DataLoc ((s2 . l),X)) is V11() real integer ext-real set
succ (((abs x) + x1) + x1) is set
(((abs x) + x1) + x1) + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
succ ((abs x) + x1) is set
((abs x) + x1) + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
s1 . l is V11() real integer ext-real set
DataLoc ((s1 . l),X) is Int-like Element of the U1 of SCMPDS
(s1 . l) + X is V11() real integer ext-real set
abs ((s1 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((s1 . l) + X))] is set
{1,(abs ((s1 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((s1 . l) + X))},{1}} is non empty set
s1 . (DataLoc ((s1 . l),X)) is V11() real integer ext-real set
s2 . l is V11() real integer ext-real set
DataLoc ((s2 . l),X) is Int-like Element of the U1 of SCMPDS
(s2 . l) + X is V11() real integer ext-real set
abs ((s2 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((s2 . l) + X))] is set
{1,(abs ((s2 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((s2 . l) + X))},{1}} is non empty set
s2 . (DataLoc ((s2 . l),X)) is V11() real integer ext-real set
n2 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
succ n2 is set
n2 + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
n2 + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
((abs x) + x1) + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
x1 + x is V11() real integer ext-real set
((abs x) + x1) + (x1 + x) is V11() real integer ext-real set
- (m2 + x) is V11() real integer ext-real set
- (m2 + x) is V11() real integer ext-real set
s1 . l is V11() real integer ext-real set
DataLoc ((s1 . l),X) is Int-like Element of the U1 of SCMPDS
(s1 . l) + X is V11() real integer ext-real set
abs ((s1 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((s1 . l) + X))] is set
{1,(abs ((s1 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((s1 . l) + X))},{1}} is non empty set
s1 . (DataLoc ((s1 . l),X)) is V11() real integer ext-real set
s2 . l is V11() real integer ext-real set
DataLoc ((s2 . l),X) is Int-like Element of the U1 of SCMPDS
(s2 . l) + X is V11() real integer ext-real set
abs ((s2 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((s2 . l) + X))] is set
{1,(abs ((s2 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((s2 . l) + X))},{1}} is non empty set
s2 . (DataLoc ((s2 . l),X)) is V11() real integer ext-real set
n2 is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
succ n2 is set
n2 + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
n2 + 1 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
- (m1 + x) is V11() real integer ext-real set
- (m1 + x) is V11() real integer ext-real set
s1 . l is V11() real integer ext-real set
DataLoc ((s1 . l),X) is Int-like Element of the U1 of SCMPDS
(s1 . l) + X is V11() real integer ext-real set
abs ((s1 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((s1 . l) + X))] is set
{1,(abs ((s1 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{1} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((s1 . l) + X))},{1}} is non empty set
s1 . (DataLoc ((s1 . l),X)) is V11() real integer ext-real set
s2 . l is V11() real integer ext-real set
DataLoc ((s2 . l),X) is Int-like Element of the U1 of SCMPDS
(s2 . l) + X is V11() real integer ext-real set
abs ((s2 . l) + X) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
[1,(abs ((s2 . l) + X))] is set
{1,(abs ((s2 . l) + X))} is non empty V121() V122() V123() V124() V125() V126() set
{{1,(abs ((s2 . l) + X))},{1}} is non empty set
s2 . (DataLoc ((s2 . l),X)) is V11() real integer ext-real set
l is Int-like Element of the U1 of SCMPDS
x is V11() real integer ext-real set
X is V11() real integer ext-real set
(l,x) <>0_goto X is Element of the InstructionsF of SCMPDS
K194(l,x,X) is set
K109(4,{},K194(l,x,X)) is set
JUMP ((l,x) <>0_goto X) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
{ (NIC (((l,x) <>0_goto X),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
meet { (NIC (((l,x) <>0_goto X),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
(l,x) <=0_goto X is Element of the InstructionsF of SCMPDS
K109(5,{},K194(l,x,X)) is set
JUMP ((l,x) <=0_goto X) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
{ (NIC (((l,x) <=0_goto X),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
meet { (NIC (((l,x) <=0_goto X),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
(l,x) >=0_goto X is Element of the InstructionsF of SCMPDS
6 is non empty ordinal natural V11() real integer non with_non-empty_elements ext-real positive non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
K109(6,{},K194(l,x,X)) is set
JUMP ((l,x) >=0_goto X) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
{ (NIC (((l,x) >=0_goto X),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
meet { (NIC (((l,x) >=0_goto X),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
l is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
SUCC (l,SCMPDS) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
{ ((NIC (b₁,l)) \ (JUMP b₁)) where b₁ is Element of the InstructionsF of SCMPDS : verum } is set
union { ((NIC (b₁,l)) \ (JUMP b₁)) where b₁ is Element of the InstructionsF of SCMPDS : verum } is set
x is set
x is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
xx is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
xx - l is V11() real integer ext-real set
goto (xx - l) is Element of the InstructionsF of SCMPDS
K192((xx - l)) is Relation-like Function-like set
K109(14,{},K192((xx - l))) is set
NIC ((goto (xx - l)),l) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
product (the_Values_of SCMPDS) is non empty functional with_common_domain product-like set
{ (IC (Exec ((goto (xx - l)),b₁))) where b₁ is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V25( the U1 of SCMPDS) Element of product (the_Values_of SCMPDS) : IC b₁ = l } is set
(xx - l) + l is V11() real integer ext-real set
abs ((xx - l) + l) is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT
{(abs ((xx - l) + l))} is non empty V121() V122() V123() V124() V125() V126() set
{x} is non empty V121() V122() V123() V124() V125() V126() set
JUMP (goto (xx - l)) is empty Function-like functional countable V121() V122() V123() V124() V125() V126() V127() Element of K6(NAT)
{ (NIC ((goto (xx - l)),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
meet { (NIC ((goto (xx - l)),b₁)) where b₁ is ordinal natural V11() real integer ext-real non negative V110() V121() V122() V123() V124() V125() V126() Element of NAT : verum } is set
(NIC ((goto (xx - l)),l)) \ (JUMP (goto (xx - l))) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
SUCC (2,SCMPDS) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
{ ((NIC (b₁,2)) \ (JUMP b₁)) where b₁ is Element of the InstructionsF of SCMPDS : verum } is set
union { ((NIC (b₁,2)) \ (JUMP b₁)) where b₁ is Element of the InstructionsF of SCMPDS : verum } is set
SUCC (1,SCMPDS) is countable V121() V122() V123() V124() V125() V126() Element of K6(NAT)
{ ((NIC (b₁,1)) \ (JUMP b₁)) where b₁ is Element of the InstructionsF of SCMPDS : verum } is set
union { ((NIC (b₁,1)) \ (JUMP b₁)) where b₁ is Element of the InstructionsF of SCMPDS : verum } is set