:: SCMFSA_1 semantic presentation

REAL is set

bool [:1,1:] is V34() V38() countable set
[:[:1,1:],1:] is Relation-like V34() countable set
bool [:[:1,1:],1:] is V34() V38() countable set

bool omega is non trivial V34() set
bool NAT is non trivial V34() set
RAT is set
INT is set

SCM-Data-Loc is non empty set
SCM-Memory is non empty set
is non empty trivial V34() 1 -element countable set
\/ SCM-Data-Loc is non empty set

SCM-Instr is non empty Relation-like V116() V117() V118() V120() set
Funcs ((),()) is non empty functional set
[:SCM-Instr,(Funcs ((),())):] is Relation-like set
bool [:SCM-Instr,(Funcs ((),())):] is set
K470() is V133(2) L8(2)
the U5 of K470() is non empty Relation-like V116() V117() V118() V120() set
the U1 of K470() is set
K452(2,K470()) is Relation-like the U1 of K470() -defined Function-like total set
SCM+FSA-Data*-Loc is non empty set

SCM-Data-Loc is non empty Element of bool SCM-Memory
() . NAT is set
proj1 () is set

is non trivial Relation-like V34() set
omega \/ is non empty set
is non natural V26() set
is non empty functional V34() V38() countable set
is non empty V34() V38() countable set

() \ is Element of bool ()
bool () is set
SCM+FSA-Instr is non empty Relation-like V116() V117() V118() V120() set

{9,10} is non empty V34() V38() countable set
{ [b1,{},<*b2,b4,b3*>] where b1 is Element of Segm 13, b2, b3 is Element of SCM-Data-Loc , b4 is Element of SCM+FSA-Data*-Loc : b1 in {9,10} } is set
SCM-Instr \/ { [b1,{},<*b2,b4,b3*>] where b1 is Element of Segm 13, b2, b3 is Element of SCM-Data-Loc , b4 is Element of SCM+FSA-Data*-Loc : b1 in {9,10} } is non empty set

{11,12} is non empty V34() V38() countable set
{ [b1,{},<*b2,b3*>] where b1 is Element of Segm 13, b2 is Element of SCM-Data-Loc , b3 is Element of SCM+FSA-Data*-Loc : b1 in {11,12} } is set
(SCM-Instr \/ { [b1,{},<*b2,b4,b3*>] where b1 is Element of Segm 13, b2, b3 is Element of SCM-Data-Loc , b4 is Element of SCM+FSA-Data*-Loc : b1 in {9,10} } ) \/ { [b1,{},<*b2,b3*>] where b1 is Element of Segm 13, b2 is Element of SCM-Data-Loc , b3 is Element of SCM+FSA-Data*-Loc : b1 in {11,12} } is non empty set

() is set
bool () is set
() is non empty Element of bool ()
() is non empty Element of bool ()

[:(),NAT:] is non trivial Relation-like V34() set
bool [:(),NAT:] is non trivial V34() set
{2} is non empty trivial V34() V38() 1 -element countable set
[:(),{2}:] is Relation-like set

[:(),3:] is Relation-like set
bool [:(),3:] is set
proj2 ((() --> 2) +* SCM-OK) is set
proj2 (() --> 2) is non empty trivial V34() 1 -element countable V108() set
proj2 SCM-OK is non empty set
{2} \/ () is non empty set
2 \/ {2} is non empty V34() countable set

proj1 ((() --> 2) +* SCM-OK) is set
proj1 (() --> 2) is non empty set
proj1 SCM-OK is non empty set
(proj1 (() --> 2)) \/ () is non empty set
() \/ () is non empty set
() \/ SCM-Memory is non empty set
() is non empty Relation-like () -defined 3 -valued Function-like total quasi_total Element of bool [:(),3:]
\/ SCM-Data-Loc is non empty set
\/ () is non empty set
( \/ ()) \/ () is non empty set

s is set
\/ SCM-Data-Loc is non empty set

is non trivial Relation-like V34() set
NAT \/ is non empty set
[0,0] is non natural V26() set
{0,0} is non empty functional V34() V38() countable set
is non empty V34() V38() countable set

() \ is Element of bool ()
bool () is set
t is set
u is set
[t,u] is non natural V26() set
{t,u} is non empty V34() countable set
{t} is non empty trivial V34() 1 -element countable set
{{t,u},{t}} is non empty V34() V38() countable set

[1,t] is non natural V26() set
{1,t} is non empty V34() V38() countable set
{1} is non empty trivial V34() V38() 1 -element countable set
{{1,t},{1}} is non empty V34() V38() countable set
t is set
u is set
[t,u] is non natural V26() set
{t,u} is non empty V34() countable set
{t} is non empty trivial V34() 1 -element countable set
{{t,u},{t}} is non empty V34() V38() countable set

[1,mk] is non natural V26() set
{1,mk} is non empty V34() V38() countable set
{1} is non empty trivial V34() V38() 1 -element countable set
{{1,mk},{1}} is non empty V34() V38() countable set
proj1 SCM-OK is non empty set
proj1 () is non empty set
proj1 (() --> 2) is non empty set
(proj1 (() --> 2)) \/ () is non empty set
() . NAT is set
((() --> 2) +* SCM-OK) . NAT is set

(() * ()) . NAT is set
() . (() . NAT) is set
s is Element of ()

((() --> 2) +* SCM-OK) . s is set
SCM-OK . s is set
s is Element of ()
(() * ()) . s is set

() . (() . s) is set
() . 1 is set
s is Element of ()

((() --> 2) +* SCM-OK) . s is set

s is Element of ()
(() * ()) . s is set

() . (() . s) is set
() . 2 is set

proj2 () is non empty set
proj1 () is set
proj1 (() * ()) is set
t is set
(() * ()) . t is set
product (() * ()) is non empty functional with_common_domain product-like set
s is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())

sproduct (() * ()) is non empty functional set
proj1 () is set
proj1 s is set
() /\ SCM-Memory is set
() /\ SCM-Memory is set
u is set
\/ SCM-Data-Loc is non empty set
() . u is set
s . u is set
mk is Element of ()
s . mk is set
pi ((product (() * ())),mk) is set
() . u is set
() . u is set
s . u is set
mk is Element of ()
pi ((product (() * ())),mk) is set
(() * ()) . mk is set
s . mk is set
() . u is set
s is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())

proj1 t is set
mk is set
\/ SCM-Data-Loc is non empty set
fx is Element of SCM-Memory
t . fx is set
pi ((),fx) is set
() . fx is set
t . mk is set

u . mk is set
fx is Element of SCM-Memory
t . fx is set
pi ((),fx) is set
() . fx is set
(() * ()) . mk is set
t . mk is set

u . mk is set

s is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())

{t} is non empty trivial V34() V38() 1 -element countable set

u is set
proj1 () is V34() countable set
(s +* ()) . NAT is set
() . NAT is set
(s +* ()) . u is set
(() * ()) . u is set
proj1 () is V34() countable set
(s +* ()) . u is set
s . u is set
(() * ()) . u is set
proj1 s is set
proj1 (s +* ()) is set
proj1 () is V34() countable set
() \/ (proj1 ()) is non empty set
() \/ is non empty set
s is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
t is Element of ()
u is V11() V12() integer ext-real set

{t} is non empty trivial V34() 1 -element countable set

{u} is non empty trivial V34() 1 -element countable set

bool [:{t},{u}:] is V34() V38() countable set
s +* (t .--> u) is Relation-like Function-like set
mk is set
proj1 (t .--> u) is V34() countable set
(s +* (t .--> u)) . t is set
(t .--> u) . t is set
(s +* (t .--> u)) . mk is set
(() * ()) . mk is set
proj1 (t .--> u) is V34() countable set
(s +* (t .--> u)) . mk is set
s . mk is set
(() * ()) . mk is set
proj1 s is set
proj1 (s +* (t .--> u)) is set
proj1 (t .--> u) is V34() countable set
() \/ (proj1 (t .--> u)) is non empty set
() \/ {t} is non empty set
s is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
t is Element of ()

{t} is non empty trivial V34() 1 -element countable set

bool [:{t},{u}:] is V34() V38() countable set
s +* (t .--> u) is Relation-like Function-like set
mk is set
proj1 (t .--> u) is V34() countable set
(s +* (t .--> u)) . t is set
(t .--> u) . t is Relation-like Function-like set
(s +* (t .--> u)) . mk is set
(() * ()) . mk is set
proj1 (t .--> u) is V34() countable set
(s +* (t .--> u)) . mk is set
s . mk is set
(() * ()) . mk is set
proj1 s is set
proj1 (s +* (t .--> u)) is set
proj1 (t .--> u) is V34() countable set
() \/ (proj1 (t .--> u)) is non empty set
() \/ {t} is non empty set
s is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
t is Element of ()
s . t is set
pi ((product (() * ())),t) is set
(() * ()) . t is set
s is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
t is Element of ()
s . t is set
pi ((product (() * ())),t) is set
(() * ()) . t is set
s is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
s . NAT is set
pi ((product (() * ())),NAT) is set
t is Element of ()
(() * ()) . t is set
s is Element of SCM+FSA-Instr

K90(s) is set
K90(K90(s)) is set
t is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())

sproduct (() * ()) is non empty functional set

t . () is V11() V12() integer ext-real set

t . NAT is set

t . () is V11() V12() integer ext-real set

(t,(),(len (t,()))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())

{()} is non empty trivial V34() 1 -element countable set
{()} --> (len (t,())) is non empty Relation-like {()} -defined NAT -valued {(len (t,()))} -valued Function-like constant total quasi_total V34() Cardinal-yielding countable Element of bool [:{()},{(len (t,()))}:]
{(len (t,()))} is non empty trivial V34() V38() 1 -element countable set
[:{()},{(len (t,()))}:] is Relation-like V34() countable set
bool [:{()},{(len (t,()))}:] is V34() V38() countable set
t +* (() .--> (len (t,()))) is Relation-like Function-like set
((t,(),(len (t,()))),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())

{(succ (t))} is non empty trivial V34() V38() 1 -element countable set
[:,{(succ (t))}:] is Relation-like V34() countable set
bool [:,{(succ (t))}:] is V34() V38() countable set
(t,(),(len (t,()))) +* (NAT .--> (succ (t))) is Relation-like Function-like set
t . () is V11() V12() integer ext-real set

u is Element of SCM-Instr

t +* (SCM-Exec-Res (u,mk)) is Relation-like Function-like set
fx is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
k is Element of SCM-Instr

y is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())

t +* (SCM-Exec-Res (k,f)) is Relation-like Function-like set

(t,()) /. u is V11() V12() integer ext-real Element of INT
mk is V11() V12() integer ext-real set
(t,(),mk) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())

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

{mk} is non empty trivial V34() 1 -element countable set

bool [:{()},{mk}:] is V34() V38() countable set
t +* (() .--> mk) is Relation-like Function-like set
((t,(),mk),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(),mk) +* (NAT .--> (succ (t))) is Relation-like Function-like set

y is V11() V12() integer ext-real set
(t,()) /. k is V11() V12() integer ext-real Element of INT
fx is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(),y) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())

{y} is non empty trivial V34() 1 -element countable set

bool [:{()},{y}:] is V34() V38() countable set
t +* (() .--> y) is Relation-like Function-like set
((t,(),y),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(),y) +* (NAT .--> (succ (t))) is Relation-like Function-like set

dom (t,()) is V34() countable Element of bool NAT

{u} is non empty trivial V34() V38() 1 -element countable set
{u} --> (t . ()) is non empty Relation-like {u} -defined {(t . ())} -valued Function-like constant total quasi_total V34() countable Element of bool [:{u},{(t . ())}:]
{(t . ())} is non empty trivial V34() 1 -element countable set
[:{u},{(t . ())}:] is Relation-like V34() countable set
bool [:{u},{(t . ())}:] is V34() V38() countable set
(t,()) +* (u .--> (t . ())) is Relation-like Function-like V34() countable set
proj1 ((t,()) +* (u .--> (t . ()))) is V34() countable set
proj1 (u .--> (t . ())) is V34() countable set
(dom (t,())) \/ (proj1 (u .--> (t . ()))) is V34() countable set
(dom (t,())) \/ {u} is non empty V34() countable set

Seg (len (t,())) is V34() len (t,()) -element countable Element of bool NAT
proj2 (u .--> (t . ())) is V34() countable set
proj2 (t,()) is V34() countable set

proj2 fx is V34() countable set
(proj2 (t,())) \/ (proj2 (u .--> (t . ()))) is V34() countable set

(t,(),y) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())

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

bool [:{()},{y}:] is V34() V38() countable set
t +* (() .--> y) is Relation-like Function-like set
((t,(),y),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(),y) +* (NAT .--> (succ (t))) is Relation-like Function-like set

Replace ((t,()),k,(t . ())) is Relation-like Function-like set
k is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(),f) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())

bool [:{()},{f}:] is V34() V38() countable set
t +* (() .--> f) is Relation-like Function-like set
((t,(),f),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(),f) +* (NAT .--> (succ (t))) is Relation-like Function-like set

dom (t,()) is V34() countable Element of bool NAT

(t,(),mk) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())

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

bool [:{()},{mk}:] is V34() V38() countable set
t +* (() .--> mk) is Relation-like Function-like set
((t,(),mk),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(),mk) +* (NAT .--> (succ (t))) is Relation-like Function-like set

Replace ((t,()),k,(t . ())) is Relation-like Function-like set
fx is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(),y) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())

bool [:{()},{y}:] is V34() V38() countable set
t +* (() .--> y) is Relation-like Function-like set
((t,(),y),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(),y) +* (NAT .--> (succ (t))) is Relation-like Function-like set

dom (t,()) is V34() countable Element of bool NAT

[:(Seg u),NAT:] is Relation-like set
bool [:(Seg u),NAT:] is set

proj2 (u |-> 0) is V34() countable set

(t,(),mk) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())

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

bool [:{()},{mk}:] is V34() V38() countable set
t +* (() .--> mk) is Relation-like Function-like set
((t,(),mk),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(),mk) +* (NAT .--> (succ (t))) is Relation-like Function-like set

fx is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(),y) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())

bool [:{()},{y}:] is V34() V38() countable set
t +* (() .--> y) is Relation-like Function-like set
((t,(),y),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(),y) +* (NAT .--> (succ (t))) is Relation-like Function-like set
u is V11() V12() integer ext-real set
(t,(),u) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())

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

{u} is non empty trivial V34() 1 -element countable set

bool [:{()},{u}:] is V34() V38() countable set
t +* (() .--> u) is Relation-like Function-like set
((t,(),u),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(),u) +* (NAT .--> (succ (t))) is Relation-like Function-like set
fx is V11() V12() integer ext-real set
mk is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(),fx) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())

{fx} is non empty trivial V34() 1 -element countable set
[:{()},{fx}:] is Relation-like V34() countable set
bool [:{()},{fx}:] is V34() V38() countable set
t +* (() .--> fx) is Relation-like Function-like set
((t,(),fx),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(),fx) +* (NAT .--> (succ (t))) is Relation-like Function-like set
fx is Element of SCM-Instr

u is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())

t +* (SCM-Exec-Res (fx,y)) is Relation-like Function-like set
k is Element of SCM-Instr

mk is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())

t +* (SCM-Exec-Res (k,f)) is Relation-like Function-like set

c11 is V11() V12() integer ext-real set
(t,()) /. c12 is V11() V12() integer ext-real Element of INT
k is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(),c11) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())

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

{c11} is non empty trivial V34() 1 -element countable set
[:{()},{c11}:] is Relation-like V34() countable set
bool [:{()},{c11}:] is V34() V38() countable set
t +* (() .--> c11) is Relation-like Function-like set
((t,(),c11),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(),c11) +* (NAT .--> (succ (t))) is Relation-like Function-like set

c13 is V11() V12() integer ext-real set
(t,()) /. c14 is V11() V12() integer ext-real Element of INT
c10 is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(),c13) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())

{c13} is non empty trivial V34() 1 -element countable set
[:{()},{c13}:] is Relation-like V34() countable set
bool [:{()},{c13}:] is V34() V38() countable set
t +* (() .--> c13) is Relation-like Function-like set
((t,(),c13),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(),c13) +* (NAT .--> (succ (t))) is Relation-like Function-like set

Replace ((t,()),c18,(t . ())) is Relation-like Function-like set
c15 is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(),c17) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())

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

{c17} is non empty trivial functional V34() V38() 1 -element with_common_domain countable set
[:{()},{c17}:] is Relation-like V34() countable set
bool [:{()},{c17}:] is V34() V38() countable set
t +* (() .--> c17) is Relation-like Function-like set
((t,(),c17),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(),c17) +* (NAT .--> (succ (t))) is Relation-like Function-like set

Replace ((t,()),c20,(t . ())) is Relation-like Function-like set
c16 is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(),c19) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())

{c19} is non empty trivial functional V34() V38() 1 -element with_common_domain countable set
[:{()},{c19}:] is Relation-like V34() countable set
bool [:{()},{c19}:] is V34() V38() countable set
t +* (() .--> c19) is Relation-like Function-like set
((t,(),c19),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(),c19) +* (NAT .--> (succ (t))) is Relation-like Function-like set
c21 is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
c22 is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())

c23 is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(),c25) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())

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

{c25} is non empty trivial functional V34() V38() 1 -element with_common_domain countable set
[:{()},{c25}:] is Relation-like V34() countable set
bool [:{()},{c25}:] is V34() V38() countable set
t +* (() .--> c25) is Relation-like Function-like set
((t,(),c25),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(),c25) +* (NAT .--> (succ (t))) is Relation-like Function-like set

c24 is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(),c27) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())

{c27} is non empty trivial functional V34() V38() 1 -element with_common_domain countable set
[:{()},{c27}:] is Relation-like V34() countable set
bool [:{()},{c27}:] is V34() V38() countable set
t +* (() .--> c27) is Relation-like Function-like set
((t,(),c27),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(),c27) +* (NAT .--> (succ (t))) is Relation-like Function-like set
c31 is V11() V12() integer ext-real set
c29 is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(),c31) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())

{()} is non empty trivial V34() 1 -element countable set
{()} --> c31 is non empty Relation-like {()} -defined {c31} -valued Function-like constant total quasi_total V34() countable Element of bool [:{()},{c31}:]
{c31} is non empty trivial V34() 1 -element countable set
[:{()},{c31}:] is Relation-like V34() countable set
bool [:{()},{c31}:] is V34() V38() countable set
t +* (() .--> c31) is Relation-like Function-like set
((t,(),c31),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(),c31) +* (NAT .--> (succ (t))) is Relation-like Function-like set
c32 is V11() V12() integer ext-real set
c30 is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(),c32) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())

{()} --> c32 is non empty Relation-like {()} -defined {c32} -valued Function-like constant total quasi_total V34() countable Element of bool [:{()},{c32}:]
{c32} is non empty trivial V34() 1 -element countable set
[:{()},{c32}:] is Relation-like V34() countable set
bool [:{()},{c32}:] is V34() V38() countable set
t +* (() .--> c32) is Relation-like Function-like set
((t,(),c32),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(),c32) +* (NAT .--> (succ (t))) is Relation-like Function-like set
c33 is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
c34 is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
mk is Element of SCM-Instr

u is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())

t +* (SCM-Exec-Res (mk,fx)) is Relation-like Function-like set

y is V11() V12() integer ext-real set
(t,()) /. k is V11() V12() integer ext-real Element of INT
(t,(),y) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())

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

{y} is non empty trivial V34() 1 -element countable set

bool [:{()},{y}:] is V34() V38() countable set
t +* (() .--> y) is Relation-like Function-like set
((t,(),y),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(),y) +* (NAT .--> (succ (t))) is Relation-like Function-like set
k is Element of SCM-Instr

f is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())

t +* (SCM-Exec-Res (k,c10)) is Relation-like Function-like set

Replace ((t,()),c12,(t . ())) is Relation-like Function-like set
(t,(),c11) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())

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

{c11} is non empty trivial functional V34() V38() 1 -element with_common_domain countable set
[:{()},{c11}:] is Relation-like V34() countable set
bool [:{()},{c11}:] is V34() V38() countable set
t +* (() .--> c11) is Relation-like Function-like set
((t,(),c11),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(),c11) +* (NAT .--> (succ (t))) is Relation-like Function-like set
c14 is Element of SCM-Instr

c13 is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())

t +* (SCM-Exec-Res (c14,c15)) is Relation-like Function-like set
c17 is Element of SCM-Instr

c16 is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())

t +* (SCM-Exec-Res (c17,c18)) is Relation-like Function-like set

(t,(),c19) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())

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

{c19} is non empty trivial functional V34() V38() 1 -element with_common_domain countable set
[:{()},{c19}:] is Relation-like V34() countable set
bool [:{()},{c19}:] is V34() V38() countable set
t +* (() .--> c19) is Relation-like Function-like set
((t,(),c19),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(),c19) +* (NAT .--> (succ (t))) is Relation-like Function-like set
c22 is Element of SCM-Instr

c21 is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())

t +* (SCM-Exec-Res (c22,c23)) is Relation-like Function-like set
c24 is V11() V12() integer ext-real set
(t,(),c24) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())

{()} is non empty trivial V34() 1 -element countable set
{()} --> c24 is non empty Relation-like {()} -defined {c24} -valued Function-like constant total quasi_total V34() countable Element of bool [:{()},{c24}:]
{c24} is non empty trivial V34() 1 -element countable set
[:{()},{c24}:] is Relation-like V34() countable set
bool [:{()},{c24}:] is V34() V38() countable set
t +* (() .--> c24) is Relation-like Function-like set
((t,(),c24),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(),c24) +* (NAT .--> (succ (t))) is Relation-like Function-like set

c26 is V11() V12() integer ext-real set
(t,()) /. c27 is V11() V12() integer ext-real Element of INT
c25 is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(),c26) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())

{c26} is non empty trivial V34() 1 -element countable set
[:{()},{c26}:] is Relation-like V34() countable set
bool [:{()},{c26}:] is V34() V38() countable set
t +* (() .--> c26) is Relation-like Function-like set
((t,(),c26),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(),c26) +* (NAT .--> (succ (t))) is Relation-like Function-like set

Replace ((t,()),c29,(t . ())) is Relation-like Function-like set
(t,(),c28) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())

{c28} is non empty trivial functional V34() V38() 1 -element with_common_domain countable set
[:{()},{c28}:] is Relation-like V34() countable set
bool [:{()},{c28}:] is V34() V38() countable set
t +* (() .--> c28) is Relation-like Function-like set
((t,(),c28),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(),c28) +* (NAT .--> (succ (t))) is Relation-like Function-like set

c31 is V11() V12() integer ext-real set
(t,()) /. c32 is V11() V12() integer ext-real Element of INT
c30 is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(),c31) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())

{c31} is non empty trivial V34() 1 -element countable set
[:{()},{c31}:] is Relation-like V34() countable set
bool [:{()},{c31}:] is V34() V38() countable set
t +* (() .--> c31) is Relation-like Function-like set
((t,(),c31),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(),c31) +* (NAT .--> (succ (t))) is Relation-like Function-like set

c34 is V11() V12() integer ext-real set
(t,()) /. c35 is V11() V12() integer ext-real Element of INT
c33 is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(),c34) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())

{c34} is non empty trivial V34() 1 -element countable set
[:{()},{c34}:] is Relation-like V34() countable set
bool [:{()},{c34}:] is V34() V38() countable set
t +* (() .--> c34) is Relation-like Function-like set
((t,(),c34),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(),c34) +* (NAT .--> (succ (t))) is Relation-like Function-like set

(t,(),c36) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())

{c36} is non empty trivial functional V34() V38() 1 -element with_common_domain countable set
[:{()},{c36}:] is Relation-like V34() countable set
bool [:{()},{c36}:] is V34() V38() countable set
t +* (() .--> c36) is Relation-like Function-like set
((t,(),c36),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(),c36) +* (NAT .--> (succ (t))) is Relation-like Function-like set

c39 is V11() V12() integer ext-real set
(t,()) /. c40 is V11() V12() integer ext-real Element of INT
c38 is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(),c39) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())