REAL is set
NAT is non empty V4() V5() V6() V35() countable denumerable Element of bool REAL
bool REAL is set
COMPLEX is set
1 is non empty V4() V5() V6() V10() V11() ext-real V32() integer Element of NAT
[:1,1:] is set
bool [:1,1:] is set
[:[:1,1:],1:] is set
bool [:[:1,1:],1:] is set
NAT is non empty V4() V5() V6() V35() countable denumerable set
bool NAT is set
9 is non empty V4() V5() V6() V10() V11() ext-real V32() integer Element of NAT
Segm 9 is countable Element of bool NAT
K186() is non empty set
SCM-Memory is non empty set
bool SCM-Memory is set
2 is non empty V4() V5() V6() V10() V11() ext-real V32() integer Element of NAT
[:SCM-Memory,2:] is set
bool [:SCM-Memory,2:] is set
SCM-OK is non empty V15() V18( SCM-Memory ) V19(2) Function-like V25( SCM-Memory ) V29( SCM-Memory ,2) Element of bool [:SCM-Memory,2:]
SCM-VAL is V15() V18(2) Function-like V25(2) set
SCM-VAL * SCM-OK is V15() non-empty Function-like set
product (SCM-VAL * SCM-OK) is non empty functional with_common_domain product-like set
K187() is non empty standard-ins V52() V53() V55() set
K97((product (SCM-VAL * SCM-OK)),(product (SCM-VAL * SCM-OK))) is non empty functional set
[:K187(),K97((product (SCM-VAL * SCM-OK)),(product (SCM-VAL * SCM-OK))):] is set
bool [:K187(),K97((product (SCM-VAL * SCM-OK)),(product (SCM-VAL * SCM-OK))):] is set
bool NAT is set
INT is set
K186() \/ INT is set
3 is non empty V4() V5() V6() V10() V11() ext-real V32() integer Element of NAT
SCM-Data-Loc is non empty Element of bool SCM-Memory
Seg 1 is non empty V35() 1 -element countable Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real V32() integer Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set
{1} is set
Seg 2 is non empty V35() 2 -element countable Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() ext-real V32() integer Element of NAT : ( 1 <= b1 & b1 <= 2 ) } is set
{1,2} is set
15 is non empty V4() V5() V6() V10() V11() ext-real V32() integer Element of NAT
Segm 15 is countable Element of bool NAT
SCM-Data-Loc \/ INT is set
f is Element of SCM-Data-Loc
f is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
g is Element of SCM-Data-Loc
f . g is V11() ext-real V32() integer set
x is V11() ext-real V32() integer set
(f . g) + x is V11() ext-real V32() integer set
abs ((f . g) + x) is V4() V5() V6() V10() V11() ext-real V32() integer Element of NAT
[1,(abs ((f . g) + x))] is set
{1,(abs ((f . g) + x))} is set
{{1,(abs ((f . g) + x))},{1}} is set
f is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
IC f is V4() V5() V6() V10() V11() ext-real V32() integer Element of NAT
g is V11() ext-real V32() integer set
(IC f) + g is V11() ext-real V32() integer set
abs ((IC f) + g) is V4() V5() V6() V10() V11() ext-real V32() integer Element of NAT
f is Element of SCM-Data-Loc
g is V11() ext-real V32() integer set
<*f,g*> is non empty V15() V18( NAT ) Function-like V35() 2 -element countable FinSequence-like FinSubsequence-like set
<*f*> is non empty V15() V18( NAT ) Function-like V35() 1 -element countable FinSequence-like FinSubsequence-like set
[1,f] is set
{1,f} is set
{{1,f},{1}} is set
{[1,f]} is Function-like set
<*g*> is non empty V15() V18( NAT ) Function-like V35() 1 -element countable FinSequence-like FinSubsequence-like set
[1,g] is set
{1,g} is set
{{1,g},{1}} is set
{[1,g]} is Function-like set
K240(<*f*>,<*g*>) is non empty V15() V18( NAT ) Function-like V35() 1 + 1 -element countable FinSequence-like FinSubsequence-like set
1 + 1 is V4() V5() V6() V10() V11() ext-real V32() integer Element of NAT
x is set
rng <*f,g*> is set
<*f,g*> is non empty V15() V18( NAT ) V19(K186() \/ INT) Function-like V35() 2 -element countable FinSequence-like FinSubsequence-like FinSequence of K186() \/ INT
dom <*f,g*> is countable Element of bool NAT
rng <*f,g*> is set
gx is set
<*f,g*> . gx is set
f is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
g is Element of SCM-Data-Loc
f . g is V11() ext-real V32() integer set
abs (f . g) is V4() V5() V6() V10() V11() ext-real V32() integer Element of NAT
(abs (f . g)) + 2 is V4() V5() V6() V10() V11() ext-real V32() integer Element of NAT
SCMPDS-Instr is non empty standard-ins V52() V53() V55() set
f is Element of SCMPDS-Instr
InsCode f is Element of InsCodes SCMPDS-Instr
InsCodes SCMPDS-Instr is set
14 is non empty V4() V5() V6() V10() V11() ext-real V32() integer Element of NAT
g is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
f const_INT is V11() ext-real V32() integer set
(g,(f const_INT)) is V4() V5() V6() V10() V11() ext-real V32() integer Element of NAT
IC g is V4() V5() V6() V10() V11() ext-real V32() integer Element of NAT
(IC g) + (f const_INT) is V11() ext-real V32() integer set
abs ((IC g) + (f const_INT)) is V4() V5() V6() V10() V11() ext-real V32() integer Element of NAT
SCM-Chg (g,(g,(f const_INT))) is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
f P21address is Element of K186()
f P22const is V11() ext-real V32() integer set
SCM-Chg (g,(f P21address),(f P22const)) is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
succ (IC g) is non empty V4() V5() V6() V10() V11() ext-real V32() integer set
SCM-Chg ((SCM-Chg (g,(f P21address),(f P22const))),(succ (IC g))) is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
(g,(f P21address),(f P22const)) is Element of SCM-Data-Loc
g . (f P21address) is V11() ext-real V32() integer set
(g . (f P21address)) + (f P22const) is V11() ext-real V32() integer set
abs ((g . (f P21address)) + (f P22const)) is V4() V5() V6() V10() V11() ext-real V32() integer Element of NAT
[1,(abs ((g . (f P21address)) + (f P22const)))] is set
{1,(abs ((g . (f P21address)) + (f P22const)))} is set
{{1,(abs ((g . (f P21address)) + (f P22const)))},{1}} is set
SCM-Chg (g,(g,(f P21address),(f P22const)),(IC g)) is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
SCM-Chg ((SCM-Chg (g,(g,(f P21address),(f P22const)),(IC g))),(succ (IC g))) is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
f address_1 is Element of K186()
RetSP is V4() V5() V6() V10() V11() ext-real V32() integer Element of NAT
(g,(f address_1),RetSP) is Element of SCM-Data-Loc
g . (f address_1) is V11() ext-real V32() integer set
(g . (f address_1)) + RetSP is V11() ext-real V32() integer set
abs ((g . (f address_1)) + RetSP) is V4() V5() V6() V10() V11() ext-real V32() integer Element of NAT
[1,(abs ((g . (f address_1)) + RetSP))] is set
{1,(abs ((g . (f address_1)) + RetSP))} is set
{{1,(abs ((g . (f address_1)) + RetSP))},{1}} is set
g . (g,(f address_1),RetSP) is V11() ext-real V32() integer set
SCM-Chg (g,(f address_1),(g . (g,(f address_1),RetSP))) is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
RetIC is V4() V5() V6() V10() V11() ext-real V32() integer Element of NAT
(g,(f address_1),RetIC) is Element of SCM-Data-Loc
(g . (f address_1)) + RetIC is V11() ext-real V32() integer set
abs ((g . (f address_1)) + RetIC) is V4() V5() V6() V10() V11() ext-real V32() integer Element of NAT
[1,(abs ((g . (f address_1)) + RetIC))] is set
{1,(abs ((g . (f address_1)) + RetIC))} is set
{{1,(abs ((g . (f address_1)) + RetIC))},{1}} is set
(g,(g,(f address_1),RetIC)) is V4() V5() V6() V10() V11() ext-real V32() integer Element of NAT
g . (g,(f address_1),RetIC) is V11() ext-real V32() integer set
abs (g . (g,(f address_1),RetIC)) is V4() V5() V6() V10() V11() ext-real V32() integer Element of NAT
(abs (g . (g,(f address_1),RetIC))) + 2 is V4() V5() V6() V10() V11() ext-real V32() integer Element of NAT
SCM-Chg ((SCM-Chg (g,(f address_1),(g . (g,(f address_1),RetSP)))),(g,(g,(f address_1),RetIC))) is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
4 is non empty V4() V5() V6() V10() V11() ext-real V32() integer Element of NAT
f P31address is Element of K186()
f P32const is V11() ext-real V32() integer set
(g,(f P31address),(f P32const)) is Element of SCM-Data-Loc
g . (f P31address) is V11() ext-real V32() integer set
(g . (f P31address)) + (f P32const) is V11() ext-real V32() integer set
abs ((g . (f P31address)) + (f P32const)) is V4() V5() V6() V10() V11() ext-real V32() integer Element of NAT
[1,(abs ((g . (f P31address)) + (f P32const)))] is set
{1,(abs ((g . (f P31address)) + (f P32const)))} is set
{{1,(abs ((g . (f P31address)) + (f P32const)))},{1}} is set
g . (g,(f P31address),(f P32const)) is V11() ext-real V32() integer set
0 is V4() V5() V6() V10() V11() ext-real V32() integer Element of NAT
f P33const is V11() ext-real V32() integer set
(g,(f P33const)) is V4() V5() V6() V10() V11() ext-real V32() integer Element of NAT
(IC g) + (f P33const) is V11() ext-real V32() integer set
abs ((IC g) + (f P33const)) is V4() V5() V6() V10() V11() ext-real V32() integer Element of NAT
IFEQ ((g . (g,(f P31address),(f P32const))),0,(succ (IC g)),(g,(f P33const))) is V4() V5() V6() V10() V11() ext-real V32() integer set
SCM-Chg (g,(IFEQ ((g . (g,(f P31address),(f P32const))),0,(succ (IC g)),(g,(f P33const))))) is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
5 is non empty V4() V5() V6() V10() V11() ext-real V32() integer Element of NAT
IFGT ((g . (g,(f P31address),(f P32const))),0,(succ (IC g)),(g,(f P33const))) is V4() V5() V6() V10() V11() ext-real V32() integer set
SCM-Chg (g,(IFGT ((g . (g,(f P31address),(f P32const))),0,(succ (IC g)),(g,(f P33const))))) is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
6 is non empty V4() V5() V6() V10() V11() ext-real V32() integer Element of NAT
IFGT (0,(g . (g,(f P31address),(f P32const))),(succ (IC g)),(g,(f P33const))) is V4() V5() V6() V10() V11() ext-real V32() integer set
SCM-Chg (g,(IFGT (0,(g . (g,(f P31address),(f P32const))),(succ (IC g)),(g,(f P33const))))) is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
7 is non empty V4() V5() V6() V10() V11() ext-real V32() integer Element of NAT
SCM-Chg (g,(g,(f P31address),(f P32const)),(f P33const)) is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
SCM-Chg ((SCM-Chg (g,(g,(f P31address),(f P32const)),(f P33const))),(succ (IC g))) is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
8 is non empty V4() V5() V6() V10() V11() ext-real V32() integer Element of NAT
(g . (g,(f P31address),(f P32const))) + (f P33const) is V11() ext-real V32() integer set
SCM-Chg (g,(g,(f P31address),(f P32const)),((g . (g,(f P31address),(f P32const))) + (f P33const))) is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
SCM-Chg ((SCM-Chg (g,(g,(f P31address),(f P32const)),((g . (g,(f P31address),(f P32const))) + (f P33const)))),(succ (IC g))) is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
f P41address is Element of K186()
f P43const is V11() ext-real V32() integer set
(g,(f P41address),(f P43const)) is Element of SCM-Data-Loc
g . (f P41address) is V11() ext-real V32() integer set
(g . (f P41address)) + (f P43const) is V11() ext-real V32() integer set
abs ((g . (f P41address)) + (f P43const)) is V4() V5() V6() V10() V11() ext-real V32() integer Element of NAT
[1,(abs ((g . (f P41address)) + (f P43const)))] is set
{1,(abs ((g . (f P41address)) + (f P43const)))} is set
{{1,(abs ((g . (f P41address)) + (f P43const)))},{1}} is set
g . (g,(f P41address),(f P43const)) is V11() ext-real V32() integer set
f P42address is Element of K186()
f P44const is V11() ext-real V32() integer set
(g,(f P42address),(f P44const)) is Element of SCM-Data-Loc
g . (f P42address) is V11() ext-real V32() integer set
(g . (f P42address)) + (f P44const) is V11() ext-real V32() integer set
abs ((g . (f P42address)) + (f P44const)) is V4() V5() V6() V10() V11() ext-real V32() integer Element of NAT
[1,(abs ((g . (f P42address)) + (f P44const)))] is set
{1,(abs ((g . (f P42address)) + (f P44const)))} is set
{{1,(abs ((g . (f P42address)) + (f P44const)))},{1}} is set
g . (g,(f P42address),(f P44const)) is V11() ext-real V32() integer set
(g . (g,(f P41address),(f P43const))) + (g . (g,(f P42address),(f P44const))) is V11() ext-real V32() integer set
SCM-Chg (g,(g,(f P41address),(f P43const)),((g . (g,(f P41address),(f P43const))) + (g . (g,(f P42address),(f P44const))))) is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
SCM-Chg ((SCM-Chg (g,(g,(f P41address),(f P43const)),((g . (g,(f P41address),(f P43const))) + (g . (g,(f P42address),(f P44const)))))),(succ (IC g))) is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
10 is non empty V4() V5() V6() V10() V11() ext-real V32() integer Element of NAT
(g . (g,(f P41address),(f P43const))) - (g . (g,(f P42address),(f P44const))) is V11() ext-real V32() integer set
SCM-Chg (g,(g,(f P41address),(f P43const)),((g . (g,(f P41address),(f P43const))) - (g . (g,(f P42address),(f P44const))))) is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
SCM-Chg ((SCM-Chg (g,(g,(f P41address),(f P43const)),((g . (g,(f P41address),(f P43const))) - (g . (g,(f P42address),(f P44const)))))),(succ (IC g))) is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
11 is non empty V4() V5() V6() V10() V11() ext-real V32() integer Element of NAT
(g . (g,(f P41address),(f P43const))) * (g . (g,(f P42address),(f P44const))) is V11() ext-real V32() integer set
SCM-Chg (g,(g,(f P41address),(f P43const)),((g . (g,(f P41address),(f P43const))) * (g . (g,(f P42address),(f P44const))))) is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
SCM-Chg ((SCM-Chg (g,(g,(f P41address),(f P43const)),((g . (g,(f P41address),(f P43const))) * (g . (g,(f P42address),(f P44const)))))),(succ (IC g))) is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
13 is non empty V4() V5() V6() V10() V11() ext-real V32() integer Element of NAT
SCM-Chg (g,(g,(f P41address),(f P43const)),(g . (g,(f P42address),(f P44const)))) is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
SCM-Chg ((SCM-Chg (g,(g,(f P41address),(f P43const)),(g . (g,(f P42address),(f P44const))))),(succ (IC g))) is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
12 is non empty V4() V5() V6() V10() V11() ext-real V32() integer Element of NAT
(g . (g,(f P41address),(f P43const))) div (g . (g,(f P42address),(f P44const))) is V11() ext-real V32() integer set
SCM-Chg (g,(g,(f P41address),(f P43const)),((g . (g,(f P41address),(f P43const))) div (g . (g,(f P42address),(f P44const))))) is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
(g . (g,(f P41address),(f P43const))) mod (g . (g,(f P42address),(f P44const))) is V11() ext-real V32() integer set
SCM-Chg ((SCM-Chg (g,(g,(f P41address),(f P43const)),((g . (g,(f P41address),(f P43const))) div (g . (g,(f P42address),(f P44const)))))),(g,(f P42address),(f P44const)),((g . (g,(f P41address),(f P43const))) mod (g . (g,(f P42address),(f P44const))))) is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
SCM-Chg ((SCM-Chg ((SCM-Chg (g,(g,(f P41address),(f P43const)),((g . (g,(f P41address),(f P43const))) div (g . (g,(f P42address),(f P44const)))))),(g,(f P42address),(f P44const)),((g . (g,(f P41address),(f P43const))) mod (g . (g,(f P42address),(f P44const)))))),(succ (IC g))) is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
x is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
gx is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
fx is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
y is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c7 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c8 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c9 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c10 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c11 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c12 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c13 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c14 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c15 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c16 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c17 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c18 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c19 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c20 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c21 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c22 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c23 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c24 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c25 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c26 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c27 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c28 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c29 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c30 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c31 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c32 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c33 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c34 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c35 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c36 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c37 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c38 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c39 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c40 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c41 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c42 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c43 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c44 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c45 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c46 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c47 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c48 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c49 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c50 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c51 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c52 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c53 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c54 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c55 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c56 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c57 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c58 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c59 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c60 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c61 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c62 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c63 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c64 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c65 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c66 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c67 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c68 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c69 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c70 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c71 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c72 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c73 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c74 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c75 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c76 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c77 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c78 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c79 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c80 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c81 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c82 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c83 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c84 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c85 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c86 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c87 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c88 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c89 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c90 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c91 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c92 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
c93 is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
[:SCMPDS-Instr,K97((product (SCM-VAL * SCM-OK)),(product (SCM-VAL * SCM-OK))):] is set
bool [:SCMPDS-Instr,K97((product (SCM-VAL * SCM-OK)),(product (SCM-VAL * SCM-OK))):] is set
[:SCMPDS-Instr,(product (SCM-VAL * SCM-OK)):] is set
[:[:SCMPDS-Instr,(product (SCM-VAL * SCM-OK)):],(product (SCM-VAL * SCM-OK)):] is set
bool [:[:SCMPDS-Instr,(product (SCM-VAL * SCM-OK)):],(product (SCM-VAL * SCM-OK)):] is set
f is V15() V18([:SCMPDS-Instr,(product (SCM-VAL * SCM-OK)):]) V19( product (SCM-VAL * SCM-OK)) Function-like V25([:SCMPDS-Instr,(product (SCM-VAL * SCM-OK)):]) V29([:SCMPDS-Instr,(product (SCM-VAL * SCM-OK)):], product (SCM-VAL * SCM-OK)) Element of bool [:[:SCMPDS-Instr,(product (SCM-VAL * SCM-OK)):],(product (SCM-VAL * SCM-OK)):]
curry f is non empty V15() V18( SCMPDS-Instr ) V19(K105((product (SCM-VAL * SCM-OK)),(product (SCM-VAL * SCM-OK)))) Function-like V25( SCMPDS-Instr ) V29( SCMPDS-Instr ,K105((product (SCM-VAL * SCM-OK)),(product (SCM-VAL * SCM-OK)))) Element of bool [:SCMPDS-Instr,K105((product (SCM-VAL * SCM-OK)),(product (SCM-VAL * SCM-OK))):]
K105((product (SCM-VAL * SCM-OK)),(product (SCM-VAL * SCM-OK))) is non empty functional M4( product (SCM-VAL * SCM-OK), product (SCM-VAL * SCM-OK))
[:SCMPDS-Instr,K105((product (SCM-VAL * SCM-OK)),(product (SCM-VAL * SCM-OK))):] is set
bool [:SCMPDS-Instr,K105((product (SCM-VAL * SCM-OK)),(product (SCM-VAL * SCM-OK))):] is set
g is Element of SCMPDS-Instr
(curry f) . g is V15() Function-like Element of K97((product (SCM-VAL * SCM-OK)),(product (SCM-VAL * SCM-OK)))
x is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
((curry f) . g) . x is set
(g,x) is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
(curry f) . g is V15() V18( product (SCM-VAL * SCM-OK)) V19( product (SCM-VAL * SCM-OK)) Function-like V25( product (SCM-VAL * SCM-OK)) V29( product (SCM-VAL * SCM-OK), product (SCM-VAL * SCM-OK)) Element of K105((product (SCM-VAL * SCM-OK)),(product (SCM-VAL * SCM-OK)))
((curry f) . g) . x is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
f . (g,x) is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
f is non empty V15() V18( SCMPDS-Instr ) V19(K97((product (SCM-VAL * SCM-OK)),(product (SCM-VAL * SCM-OK)))) Function-like V25( SCMPDS-Instr ) V29( SCMPDS-Instr ,K97((product (SCM-VAL * SCM-OK)),(product (SCM-VAL * SCM-OK)))) Element of bool [:SCMPDS-Instr,K97((product (SCM-VAL * SCM-OK)),(product (SCM-VAL * SCM-OK))):]
g is non empty V15() V18( SCMPDS-Instr ) V19(K97((product (SCM-VAL * SCM-OK)),(product (SCM-VAL * SCM-OK)))) Function-like V25( SCMPDS-Instr ) V29( SCMPDS-Instr ,K97((product (SCM-VAL * SCM-OK)),(product (SCM-VAL * SCM-OK)))) Element of bool [:SCMPDS-Instr,K97((product (SCM-VAL * SCM-OK)),(product (SCM-VAL * SCM-OK))):]
[:(product (SCM-VAL * SCM-OK)),(product (SCM-VAL * SCM-OK)):] is set
bool [:(product (SCM-VAL * SCM-OK)),(product (SCM-VAL * SCM-OK)):] is set
x is Element of SCMPDS-Instr
g . x is V15() Function-like Element of K97((product (SCM-VAL * SCM-OK)),(product (SCM-VAL * SCM-OK)))
f . x is V15() Function-like Element of K97((product (SCM-VAL * SCM-OK)),(product (SCM-VAL * SCM-OK)))
fx is non empty V15() V18( product (SCM-VAL * SCM-OK)) V19( product (SCM-VAL * SCM-OK)) Function-like V25( product (SCM-VAL * SCM-OK)) V29( product (SCM-VAL * SCM-OK), product (SCM-VAL * SCM-OK)) Element of bool [:(product (SCM-VAL * SCM-OK)),(product (SCM-VAL * SCM-OK)):]
y is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
fx . y is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
(x,y) is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
gx is non empty V15() V18( product (SCM-VAL * SCM-OK)) V19( product (SCM-VAL * SCM-OK)) Function-like V25( product (SCM-VAL * SCM-OK)) V29( product (SCM-VAL * SCM-OK), product (SCM-VAL * SCM-OK)) Element of bool [:(product (SCM-VAL * SCM-OK)),(product (SCM-VAL * SCM-OK)):]
gx . y is V15() Function-like SCM-VAL * SCM-OK -compatible Element of product (SCM-VAL * SCM-OK)
() is non empty V15() V18( SCMPDS-Instr ) V19(K97((product (SCM-VAL * SCM-OK)),(product (SCM-VAL * SCM-OK)))) Function-like V25( SCMPDS-Instr ) V29( SCMPDS-Instr ,K97((product (SCM-VAL * SCM-OK)),(product (SCM-VAL * SCM-OK)))) Element of bool [:SCMPDS-Instr,K97((product (SCM-VAL * SCM-OK)),(product (SCM-VAL * SCM-OK))):]