:: SCMFSA_1 semantic presentation

REAL is set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal V34() cardinal limit_cardinal countable denumerable Element of bool REAL
bool REAL is set
COMPLEX is set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real positive Element of NAT
[:1,1:] is Relation-like V34() countable 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
omega is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal V34() cardinal limit_cardinal countable denumerable set
bool omega is non trivial V34() set
bool NAT is non trivial V34() set
RAT is set
INT is set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() integer Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional Function-yielding V33() V34() V35() V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable ext-real V115() set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real positive Element of NAT
9 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real positive Element of NAT
Segm 9 is countable Element of bool omega
SCM-Data-Loc is non empty set
SCM-Memory is non empty set
{NAT} is non empty trivial V34() 1 -element countable set
{NAT} \/ SCM-Data-Loc is non empty set
bool SCM-Memory is set
[:SCM-Memory,2:] is Relation-like set
bool [:SCM-Memory,2:] is set
SCM-OK is non empty Relation-like SCM-Memory -defined 2 -valued Function-like total quasi_total Element of bool [:SCM-Memory,2:]
SCM-VAL is Relation-like 2 -defined Function-like total set
<%NAT,INT%> is T-Sequence-like Relation-like NAT -defined Function-like V34() 2 -element countable V115() set
SCM-OK * SCM-VAL is Relation-like non-empty SCM-Memory -defined SCM-Memory -defined Function-like set
product (SCM-OK * SCM-VAL) is non empty functional with_common_domain product-like set
SCM-Instr is non empty Relation-like V116() V117() V118() V120() set
Funcs ((product (SCM-OK * SCM-VAL)),(product (SCM-OK * SCM-VAL))) is non empty functional set
[:SCM-Instr,(Funcs ((product (SCM-OK * SCM-VAL)),(product (SCM-OK * SCM-VAL)))):] is Relation-like set
bool [:SCM-Instr,(Funcs ((product (SCM-OK * SCM-VAL)),(product (SCM-OK * SCM-VAL)))):] 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
INT \ NAT is Element of bool INT
bool INT is set
3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real positive Element of NAT
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() integer Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional Function-yielding V33() V34() V35() V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable ext-real V115() Element of NAT
SCM-Data-Loc is non empty Element of bool SCM-Memory
(SCM-OK * SCM-VAL) . NAT is set
proj1 (SCM-OK * SCM-VAL) is set
INT * is non empty functional FinSequence-membered FinSequenceSet of INT
{{}} is non empty trivial functional V34() V38() 1 -element with_common_domain countable set
[:{{}},omega:] is non trivial Relation-like V34() set
omega \/ [:{{}},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 non empty trivial Relation-like Function-like constant V34() 1 -element countable set
(omega \/ [:{{}},omega:]) \ {[{},{}]} is Element of bool (omega \/ [:{{}},omega:])
bool (omega \/ [:{{}},omega:]) is set
SCM+FSA-Instr is non empty Relation-like V116() V117() V118() V120() set
13 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real positive Element of NAT
Segm 13 is countable Element of bool omega
10 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real positive Element of NAT
{9,10} is non empty V34() V38() countable set
{ [b₁,{},<*b₂,b₄,b₃*>] where b₁ is Element of Segm 13, b₂, b₃ is Element of SCM-Data-Loc , b₄ is Element of SCM+FSA-Data*-Loc : b₁ in {9,10} } is set
SCM-Instr \/ { [b₁,{},<*b₂,b₄,b₃*>] where b₁ is Element of Segm 13, b₂, b₃ is Element of SCM-Data-Loc , b₄ is Element of SCM+FSA-Data*-Loc : b₁ in {9,10} } is non empty set
11 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real positive Element of NAT
12 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real positive Element of NAT
{11,12} is non empty V34() V38() countable set
{ [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 13, b₂ is Element of SCM-Data-Loc , b₃ is Element of SCM+FSA-Data*-Loc : b₁ in {11,12} } is set
(SCM-Instr \/ { [b₁,{},<*b₂,b₄,b₃*>] where b₁ is Element of Segm 13, b₂, b₃ is Element of SCM-Data-Loc , b₄ is Element of SCM+FSA-Data*-Loc : b₁ in {9,10} } ) \/ { [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 13, b₂ is Element of SCM-Data-Loc , b₃ is Element of SCM+FSA-Data*-Loc : b₁ in {11,12} } is non empty set
8 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real positive Element of NAT
SCM-Memory \/ SCM+FSA-Data*-Loc is non empty set
() is set
bool () is set
() is non empty Element of bool ()
() is non empty Element of bool ()
() --> 2 is non empty Relation-like non-empty () -defined NAT -valued Function-like constant total quasi_total Cardinal-yielding Element of bool [:(),NAT:]
[:(),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
(() --> 2) +* SCM-OK is Relation-like Function-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} \/ (proj2 SCM-OK) is non empty set
2 \/ {2} is non empty V34() countable set
succ 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of omega
proj1 ((() --> 2) +* SCM-OK) is set
proj1 (() --> 2) is non empty set
proj1 SCM-OK is non empty set
(proj1 (() --> 2)) \/ (proj1 SCM-OK) is non empty set
() \/ (proj1 SCM-OK) 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:]
{NAT} \/ SCM-Data-Loc is non empty set
{NAT} \/ () is non empty set
({NAT} \/ ()) \/ () is non empty set
<%NAT,INT,(INT *)%> is T-Sequence-like Relation-like NAT -defined Function-like V34() 3 -element countable V115() set
() is Relation-like 3 -defined Function-like total set
s is set
{NAT} \/ SCM-Data-Loc is non empty set
{0} is non empty trivial functional V34() V38() 1 -element with_common_domain countable set
[:{0},NAT:] is non trivial Relation-like V34() set
NAT \/ [:{0},NAT:] is non empty set
[0,0] is non natural V26() set
{0,0} is non empty functional V34() V38() countable set
{{0,0},{0}} is non empty V34() V38() countable set
{[0,0]} is non empty trivial Relation-like Function-like constant V34() 1 -element countable set
(NAT \/ [:{0},NAT:]) \ {[0,0]} is Element of bool (NAT \/ [:{0},NAT:])
bool (NAT \/ [:{0},NAT:]) 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
t is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of NAT
[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
mk is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of NAT
[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)) \/ (proj1 SCM-OK) is non empty set
() . NAT is set
((() --> 2) +* SCM-OK) . NAT is set
SCM-OK . NAT is set
() * () is Relation-like () -defined Function-like set
(() * ()) . NAT is set
() . (() . NAT) is set
s is Element of ()
() . s is epsilon-transitive epsilon-connected ordinal Element of 3
((() --> 2) +* SCM-OK) . s is set
SCM-OK . s is set
s is Element of ()
(() * ()) . s is set
() . s is epsilon-transitive epsilon-connected ordinal Element of 3
() . (() . s) is set
() . 1 is set
s is Element of ()
() . s is epsilon-transitive epsilon-connected ordinal Element of 3
((() --> 2) +* SCM-OK) . s is set
(() --> 2) . s is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of NAT
s is Element of ()
(() * ()) . s is set
() . s is epsilon-transitive epsilon-connected ordinal Element of 3
() . (() . s) is set
() . 2 is set
len <%NAT,INT,(INT *)%> is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of NAT
proj1 <%NAT,INT,(INT *)%> is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal 3 -element countable ext-real 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 (() * ())
s | SCM-Memory is Relation-like SCM-Memory -defined () -defined Function-like () * () -compatible Element of sproduct (() * ())
sproduct (() * ()) is non empty functional set
proj1 (s | SCM-Memory) is set
proj1 s is set
(proj1 s) /\ SCM-Memory is set
() /\ SCM-Memory is set
u is set
{NAT} \/ SCM-Data-Loc is non empty set
(s | SCM-Memory) . u is set
s . u is set
mk is Element of ()
s . mk is set
pi ((product (() * ())),mk) is set
(SCM-OK * SCM-VAL) . u is set
(s | SCM-Memory) . u is set
s . u is set
mk is Element of ()
pi ((product (() * ())),mk) is set
(() * ()) . mk is set
s . mk is set
(SCM-OK * SCM-VAL) . u is set
s is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
t is Relation-like SCM-Memory -defined Function-like SCM-OK * SCM-VAL -compatible Element of product (SCM-OK * SCM-VAL)
s +* t is Relation-like Function-like set
proj1 t is set
mk is set
{NAT} \/ SCM-Data-Loc is non empty set
fx is Element of SCM-Memory
t . fx is set
pi ((product (SCM-OK * SCM-VAL)),fx) is set
(SCM-OK * SCM-VAL) . fx is set
t . mk is set
u is Relation-like non-empty () -defined Function-like total set
u . mk is set
fx is Element of SCM-Memory
t . fx is set
pi ((product (SCM-OK * SCM-VAL)),fx) is set
(SCM-OK * SCM-VAL) . fx is set
(() * ()) . mk is set
t . mk is set
u is Relation-like non-empty () -defined Function-like total set
u . mk is set
u is Relation-like non-empty () -defined Function-like total set
u is Relation-like non-empty () -defined Function-like total set
s is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
t is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real set
NAT .--> t is Relation-like {NAT} -defined Function-like one-to-one V34() Cardinal-yielding countable set
{NAT} --> t is non empty Relation-like {NAT} -defined {t} -valued Function-like constant total quasi_total V34() Cardinal-yielding countable Element of bool [:{NAT},{t}:]
{t} is non empty trivial V34() V38() 1 -element countable set
[:{NAT},{t}:] is Relation-like V34() countable set
bool [:{NAT},{t}:] is V34() V38() countable set
s +* (NAT .--> t) is Relation-like Function-like set
u is set
proj1 (NAT .--> t) is V34() countable set
(s +* (NAT .--> t)) . NAT is set
(NAT .--> t) . NAT is set
(s +* (NAT .--> t)) . u is set
(() * ()) . u is set
proj1 (NAT .--> t) is V34() countable set
(s +* (NAT .--> t)) . u is set
s . u is set
(() * ()) . u is set
proj1 s is set
proj1 (s +* (NAT .--> t)) is set
proj1 (NAT .--> t) is V34() countable set
() \/ (proj1 (NAT .--> t)) is non empty set
() \/ {NAT} 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 .--> u is Relation-like () -defined {t} -defined Function-like one-to-one V34() countable set
{t} is non empty trivial V34() 1 -element countable set
{t} --> u is non empty Relation-like {t} -defined {u} -valued Function-like constant total quasi_total V34() countable Element of bool [:{t},{u}:]
{u} is non empty trivial V34() 1 -element countable set
[:{t},{u}:] is Relation-like V34() 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 ()
u is Relation-like NAT -defined INT -valued Function-like V34() FinSequence-like FinSubsequence-like countable FinSequence of INT
t .--> u is Relation-like () -defined {t} -defined Function-like one-to-one Function-yielding V33() V34() countable set
{t} is non empty trivial V34() 1 -element countable set
{t} --> u is non empty Relation-like {t} -defined {u} -valued Function-like constant total quasi_total Function-yielding V33() V34() countable Element of bool [:{t},{u}:]
{u} is non empty trivial functional V34() V38() 1 -element with_common_domain countable set
[:{t},{u}:] is Relation-like V34() 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
s `1_3 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real set
K90(s) is set
K90(K90(s)) is set
t is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
t | SCM-Memory is Relation-like SCM-Memory -defined () -defined Function-like () * () -compatible Element of sproduct (() * ())
sproduct (() * ()) is non empty functional set
s int_addr2 is Element of SCM-Data-Loc
t . (s int_addr2) is V11() V12() integer ext-real set
abs (t . (s int_addr2)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of NAT
s coll_addr1 is Element of SCM+FSA-Data*-Loc
(t,(s coll_addr1)) is Relation-like NAT -defined INT -valued Function-like V34() FinSequence-like FinSubsequence-like countable FinSequence of INT
s int_addr1 is Element of SCM-Data-Loc
(t) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of NAT
t . NAT is set
succ (t) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of omega
t . (s int_addr1) is V11() V12() integer ext-real set
s int_addr3 is Element of SCM-Data-Loc
s coll_addr2 is Element of SCM+FSA-Data*-Loc
(t,(s coll_addr2)) is Relation-like NAT -defined INT -valued Function-like V34() FinSequence-like FinSubsequence-like countable FinSequence of INT
len (t,(s coll_addr2)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of NAT
(t,(s int_addr3),(len (t,(s coll_addr2)))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(s int_addr3) .--> (len (t,(s coll_addr2))) is Relation-like SCM-Data-Loc -defined {(s int_addr3)} -defined NAT -valued Function-like one-to-one V34() Cardinal-yielding countable set
{(s int_addr3)} is non empty trivial V34() 1 -element countable set
{(s int_addr3)} --> (len (t,(s coll_addr2))) is non empty Relation-like {(s int_addr3)} -defined NAT -valued {(len (t,(s coll_addr2)))} -valued Function-like constant total quasi_total V34() Cardinal-yielding countable Element of bool [:{(s int_addr3)},{(len (t,(s coll_addr2)))}:]
{(len (t,(s coll_addr2)))} is non empty trivial V34() V38() 1 -element countable set
[:{(s int_addr3)},{(len (t,(s coll_addr2)))}:] is Relation-like V34() countable set
bool [:{(s int_addr3)},{(len (t,(s coll_addr2)))}:] is V34() V38() countable set
t +* ((s int_addr3) .--> (len (t,(s coll_addr2)))) is Relation-like Function-like set
((t,(s int_addr3),(len (t,(s coll_addr2)))),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
NAT .--> (succ (t)) is Relation-like {NAT} -defined omega -valued Function-like one-to-one V34() Cardinal-yielding countable set
{NAT} --> (succ (t)) is non empty Relation-like non-empty {NAT} -defined omega -valued {(succ (t))} -valued Function-like constant total quasi_total V34() Cardinal-yielding countable Element of bool [:{NAT},{(succ (t))}:]
{(succ (t))} is non empty trivial V34() V38() 1 -element countable set
[:{NAT},{(succ (t))}:] is Relation-like V34() countable set
bool [:{NAT},{(succ (t))}:] is V34() V38() countable set
(t,(s int_addr3),(len (t,(s coll_addr2)))) +* (NAT .--> (succ (t))) is Relation-like Function-like set
t . (s int_addr3) is V11() V12() integer ext-real set
abs (t . (s int_addr3)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of NAT
s int_addr is Element of SCM-Data-Loc
u is Element of SCM-Instr
mk is Relation-like SCM-Memory -defined Function-like SCM-OK * SCM-VAL -compatible Element of product (SCM-OK * SCM-VAL)
SCM-Exec-Res (u,mk) is Relation-like SCM-Memory -defined Function-like SCM-OK * SCM-VAL -compatible Element of product (SCM-OK * SCM-VAL)
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
f is Relation-like SCM-Memory -defined Function-like SCM-OK * SCM-VAL -compatible Element of product (SCM-OK * SCM-VAL)
y is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
SCM-Exec-Res (k,f) is Relation-like SCM-Memory -defined Function-like SCM-OK * SCM-VAL -compatible Element of product (SCM-OK * SCM-VAL)
t +* (SCM-Exec-Res (k,f)) is Relation-like Function-like set
u is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of NAT
(t,(s coll_addr1)) /. u is V11() V12() integer ext-real Element of INT
mk is V11() V12() integer ext-real set
(t,(s int_addr1),mk) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(s int_addr1) .--> mk is Relation-like SCM-Data-Loc -defined {(s int_addr1)} -defined Function-like one-to-one V34() countable set
{(s int_addr1)} is non empty trivial V34() 1 -element countable set
{(s int_addr1)} --> mk is non empty Relation-like {(s int_addr1)} -defined {mk} -valued Function-like constant total quasi_total V34() countable Element of bool [:{(s int_addr1)},{mk}:]
{mk} is non empty trivial V34() 1 -element countable set
[:{(s int_addr1)},{mk}:] is Relation-like V34() countable set
bool [:{(s int_addr1)},{mk}:] is V34() V38() countable set
t +* ((s int_addr1) .--> mk) is Relation-like Function-like set
((t,(s int_addr1),mk),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s int_addr1),mk) +* (NAT .--> (succ (t))) is Relation-like Function-like set
k is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of NAT
y is V11() V12() integer ext-real set
(t,(s coll_addr1)) /. k is V11() V12() integer ext-real Element of INT
fx is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s int_addr1),y) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(s int_addr1) .--> y is Relation-like SCM-Data-Loc -defined {(s int_addr1)} -defined Function-like one-to-one V34() countable set
{(s int_addr1)} --> y is non empty Relation-like {(s int_addr1)} -defined {y} -valued Function-like constant total quasi_total V34() countable Element of bool [:{(s int_addr1)},{y}:]
{y} is non empty trivial V34() 1 -element countable set
[:{(s int_addr1)},{y}:] is Relation-like V34() countable set
bool [:{(s int_addr1)},{y}:] is V34() V38() countable set
t +* ((s int_addr1) .--> y) is Relation-like Function-like set
((t,(s int_addr1),y),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s int_addr1),y) +* (NAT .--> (succ (t))) is Relation-like Function-like set
u is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of NAT
dom (t,(s coll_addr1)) is V34() countable Element of bool NAT
u .--> (t . (s int_addr1)) is Relation-like NAT -defined {u} -defined Function-like one-to-one V34() countable set
{u} is non empty trivial V34() V38() 1 -element countable set
{u} --> (t . (s int_addr1)) is non empty Relation-like {u} -defined {(t . (s int_addr1))} -valued Function-like constant total quasi_total V34() countable Element of bool [:{u},{(t . (s int_addr1))}:]
{(t . (s int_addr1))} is non empty trivial V34() 1 -element countable set
[:{u},{(t . (s int_addr1))}:] is Relation-like V34() countable set
bool [:{u},{(t . (s int_addr1))}:] is V34() V38() countable set
(t,(s coll_addr1)) +* (u .--> (t . (s int_addr1))) is Relation-like Function-like V34() countable set
proj1 ((t,(s coll_addr1)) +* (u .--> (t . (s int_addr1)))) is V34() countable set
proj1 (u .--> (t . (s int_addr1))) is V34() countable set
(dom (t,(s coll_addr1))) \/ (proj1 (u .--> (t . (s int_addr1)))) is V34() countable set
(dom (t,(s coll_addr1))) \/ {u} is non empty V34() countable set
len (t,(s coll_addr1)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of NAT
Seg (len (t,(s coll_addr1))) is V34() len (t,(s coll_addr1)) -element countable Element of bool NAT
proj2 (u .--> (t . (s int_addr1))) is V34() countable set
proj2 (t,(s coll_addr1)) is V34() countable set
fx is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like countable set
proj2 fx is V34() countable set
(proj2 (t,(s coll_addr1))) \/ (proj2 (u .--> (t . (s int_addr1)))) is V34() countable set
y is Relation-like NAT -defined INT -valued Function-like V34() FinSequence-like FinSubsequence-like countable FinSequence of INT
(t,(s coll_addr1),y) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(s coll_addr1) .--> y is Relation-like SCM+FSA-Data*-Loc -defined {(s coll_addr1)} -defined Function-like one-to-one Function-yielding V33() V34() countable set
{(s coll_addr1)} is non empty trivial V34() 1 -element countable set
{(s coll_addr1)} --> y is non empty Relation-like {(s coll_addr1)} -defined {y} -valued Function-like constant total quasi_total Function-yielding V33() V34() countable Element of bool [:{(s coll_addr1)},{y}:]
{y} is non empty trivial functional V34() V38() 1 -element with_common_domain countable set
[:{(s coll_addr1)},{y}:] is Relation-like V34() countable set
bool [:{(s coll_addr1)},{y}:] is V34() V38() countable set
t +* ((s coll_addr1) .--> y) is Relation-like Function-like set
((t,(s coll_addr1),y),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s coll_addr1),y) +* (NAT .--> (succ (t))) is Relation-like Function-like set
k is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of NAT
f is Relation-like NAT -defined INT -valued Function-like V34() FinSequence-like FinSubsequence-like countable FinSequence of INT
Replace ((t,(s coll_addr1)),k,(t . (s int_addr1))) is Relation-like Function-like set
k is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s coll_addr1),f) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(s coll_addr1) .--> f is Relation-like SCM+FSA-Data*-Loc -defined {(s coll_addr1)} -defined Function-like one-to-one Function-yielding V33() V34() countable set
{(s coll_addr1)} --> f is non empty Relation-like {(s coll_addr1)} -defined {f} -valued Function-like constant total quasi_total Function-yielding V33() V34() countable Element of bool [:{(s coll_addr1)},{f}:]
{f} is non empty trivial functional V34() V38() 1 -element with_common_domain countable set
[:{(s coll_addr1)},{f}:] is Relation-like V34() countable set
bool [:{(s coll_addr1)},{f}:] is V34() V38() countable set
t +* ((s coll_addr1) .--> f) is Relation-like Function-like set
((t,(s coll_addr1),f),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s coll_addr1),f) +* (NAT .--> (succ (t))) is Relation-like Function-like set
u is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of NAT
dom (t,(s coll_addr1)) is V34() countable Element of bool NAT
mk is Relation-like NAT -defined INT -valued Function-like V34() FinSequence-like FinSubsequence-like countable FinSequence of INT
(t,(s coll_addr1),mk) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(s coll_addr1) .--> mk is Relation-like SCM+FSA-Data*-Loc -defined {(s coll_addr1)} -defined Function-like one-to-one Function-yielding V33() V34() countable set
{(s coll_addr1)} is non empty trivial V34() 1 -element countable set
{(s coll_addr1)} --> mk is non empty Relation-like {(s coll_addr1)} -defined {mk} -valued Function-like constant total quasi_total Function-yielding V33() V34() countable Element of bool [:{(s coll_addr1)},{mk}:]
{mk} is non empty trivial functional V34() V38() 1 -element with_common_domain countable set
[:{(s coll_addr1)},{mk}:] is Relation-like V34() countable set
bool [:{(s coll_addr1)},{mk}:] is V34() V38() countable set
t +* ((s coll_addr1) .--> mk) is Relation-like Function-like set
((t,(s coll_addr1),mk),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s coll_addr1),mk) +* (NAT .--> (succ (t))) is Relation-like Function-like set
k is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of NAT
y is Relation-like NAT -defined INT -valued Function-like V34() FinSequence-like FinSubsequence-like countable FinSequence of INT
Replace ((t,(s coll_addr1)),k,(t . (s int_addr1))) is Relation-like Function-like set
fx is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s coll_addr1),y) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(s coll_addr1) .--> y is Relation-like SCM+FSA-Data*-Loc -defined {(s coll_addr1)} -defined Function-like one-to-one Function-yielding V33() V34() countable set
{(s coll_addr1)} --> y is non empty Relation-like {(s coll_addr1)} -defined {y} -valued Function-like constant total quasi_total Function-yielding V33() V34() countable Element of bool [:{(s coll_addr1)},{y}:]
{y} is non empty trivial functional V34() V38() 1 -element with_common_domain countable set
[:{(s coll_addr1)},{y}:] is Relation-like V34() countable set
bool [:{(s coll_addr1)},{y}:] is V34() V38() countable set
t +* ((s coll_addr1) .--> y) is Relation-like Function-like set
((t,(s coll_addr1),y),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s coll_addr1),y) +* (NAT .--> (succ (t))) is Relation-like Function-like set
u is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of NAT
dom (t,(s coll_addr1)) is V34() countable Element of bool NAT
{0} is non empty trivial functional V34() V38() 1 -element with_common_domain countable set
u is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of NAT
u |-> 0 is Relation-like NAT -defined NAT -valued Function-like V34() FinSequence-like FinSubsequence-like countable Element of u -tuples_on NAT
u -tuples_on NAT is FinSequenceSet of NAT
Seg u is V34() u -element countable Element of bool NAT
(Seg u) --> 0 is Relation-like Seg u -defined NAT -valued Function-like constant total quasi_total Function-yielding V33() V34() Cardinal-yielding countable Element of bool [:(Seg u),NAT:]
[:(Seg u),NAT:] is Relation-like set
bool [:(Seg u),NAT:] is set
[:(Seg u),{0}:] is Relation-like V34() countable set
proj2 (u |-> 0) is V34() countable set
mk is Relation-like NAT -defined INT -valued Function-like V34() FinSequence-like FinSubsequence-like countable FinSequence of INT
(t,(s coll_addr2),mk) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(s coll_addr2) .--> mk is Relation-like SCM+FSA-Data*-Loc -defined {(s coll_addr2)} -defined Function-like one-to-one Function-yielding V33() V34() countable set
{(s coll_addr2)} is non empty trivial V34() 1 -element countable set
{(s coll_addr2)} --> mk is non empty Relation-like {(s coll_addr2)} -defined {mk} -valued Function-like constant total quasi_total Function-yielding V33() V34() countable Element of bool [:{(s coll_addr2)},{mk}:]
{mk} is non empty trivial functional V34() V38() 1 -element with_common_domain countable set
[:{(s coll_addr2)},{mk}:] is Relation-like V34() countable set
bool [:{(s coll_addr2)},{mk}:] is V34() V38() countable set
t +* ((s coll_addr2) .--> mk) is Relation-like Function-like set
((t,(s coll_addr2),mk),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s coll_addr2),mk) +* (NAT .--> (succ (t))) is Relation-like Function-like set
k is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of NAT
y is Relation-like NAT -defined INT -valued Function-like V34() FinSequence-like FinSubsequence-like countable FinSequence of INT
k |-> 0 is Relation-like NAT -defined NAT -valued Function-like V34() FinSequence-like FinSubsequence-like countable Element of k -tuples_on NAT
k -tuples_on NAT is FinSequenceSet of NAT
fx is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s coll_addr2),y) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(s coll_addr2) .--> y is Relation-like SCM+FSA-Data*-Loc -defined {(s coll_addr2)} -defined Function-like one-to-one Function-yielding V33() V34() countable set
{(s coll_addr2)} --> y is non empty Relation-like {(s coll_addr2)} -defined {y} -valued Function-like constant total quasi_total Function-yielding V33() V34() countable Element of bool [:{(s coll_addr2)},{y}:]
{y} is non empty trivial functional V34() V38() 1 -element with_common_domain countable set
[:{(s coll_addr2)},{y}:] is Relation-like V34() countable set
bool [:{(s coll_addr2)},{y}:] is V34() V38() countable set
t +* ((s coll_addr2) .--> y) is Relation-like Function-like set
((t,(s coll_addr2),y),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s coll_addr2),y) +* (NAT .--> (succ (t))) is Relation-like Function-like set
u is V11() V12() integer ext-real set
(t,(s int_addr),u) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(s int_addr) .--> u is Relation-like SCM-Data-Loc -defined {(s int_addr)} -defined Function-like one-to-one V34() countable set
{(s int_addr)} is non empty trivial V34() 1 -element countable set
{(s int_addr)} --> u is non empty Relation-like {(s int_addr)} -defined {u} -valued Function-like constant total quasi_total V34() countable Element of bool [:{(s int_addr)},{u}:]
{u} is non empty trivial V34() 1 -element countable set
[:{(s int_addr)},{u}:] is Relation-like V34() countable set
bool [:{(s int_addr)},{u}:] is V34() V38() countable set
t +* ((s int_addr) .--> u) is Relation-like Function-like set
((t,(s int_addr),u),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s int_addr),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,(s int_addr),fx) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(s int_addr) .--> fx is Relation-like SCM-Data-Loc -defined {(s int_addr)} -defined Function-like one-to-one V34() countable set
{(s int_addr)} --> fx is non empty Relation-like {(s int_addr)} -defined {fx} -valued Function-like constant total quasi_total V34() countable Element of bool [:{(s int_addr)},{fx}:]
{fx} is non empty trivial V34() 1 -element countable set
[:{(s int_addr)},{fx}:] is Relation-like V34() countable set
bool [:{(s int_addr)},{fx}:] is V34() V38() countable set
t +* ((s int_addr) .--> fx) is Relation-like Function-like set
((t,(s int_addr),fx),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s int_addr),fx) +* (NAT .--> (succ (t))) is Relation-like Function-like set
fx is Element of SCM-Instr
y is Relation-like SCM-Memory -defined Function-like SCM-OK * SCM-VAL -compatible Element of product (SCM-OK * SCM-VAL)
u is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
SCM-Exec-Res (fx,y) is Relation-like SCM-Memory -defined Function-like SCM-OK * SCM-VAL -compatible Element of product (SCM-OK * SCM-VAL)
t +* (SCM-Exec-Res (fx,y)) is Relation-like Function-like set
k is Element of SCM-Instr
f is Relation-like SCM-Memory -defined Function-like SCM-OK * SCM-VAL -compatible Element of product (SCM-OK * SCM-VAL)
mk is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
SCM-Exec-Res (k,f) is Relation-like SCM-Memory -defined Function-like SCM-OK * SCM-VAL -compatible Element of product (SCM-OK * SCM-VAL)
t +* (SCM-Exec-Res (k,f)) is Relation-like Function-like set
c₁₂ is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of NAT
c₁₁ is V11() V12() integer ext-real set
(t,(s coll_addr1)) /. c₁₂ is V11() V12() integer ext-real Element of INT
k is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s int_addr1),c₁₁) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(s int_addr1) .--> c₁₁ is Relation-like SCM-Data-Loc -defined {(s int_addr1)} -defined Function-like one-to-one V34() countable set
{(s int_addr1)} is non empty trivial V34() 1 -element countable set
{(s int_addr1)} --> c₁₁ is non empty Relation-like {(s int_addr1)} -defined {c₁₁} -valued Function-like constant total quasi_total V34() countable Element of bool [:{(s int_addr1)},{c₁₁}:]
{c₁₁} is non empty trivial V34() 1 -element countable set
[:{(s int_addr1)},{c₁₁}:] is Relation-like V34() countable set
bool [:{(s int_addr1)},{c₁₁}:] is V34() V38() countable set
t +* ((s int_addr1) .--> c₁₁) is Relation-like Function-like set
((t,(s int_addr1),c₁₁),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s int_addr1),c₁₁) +* (NAT .--> (succ (t))) is Relation-like Function-like set
c₁₄ is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of NAT
c₁₃ is V11() V12() integer ext-real set
(t,(s coll_addr1)) /. c₁₄ is V11() V12() integer ext-real Element of INT
c₁₀ is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s int_addr1),c₁₃) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(s int_addr1) .--> c₁₃ is Relation-like SCM-Data-Loc -defined {(s int_addr1)} -defined Function-like one-to-one V34() countable set
{(s int_addr1)} --> c₁₃ is non empty Relation-like {(s int_addr1)} -defined {c₁₃} -valued Function-like constant total quasi_total V34() countable Element of bool [:{(s int_addr1)},{c₁₃}:]
{c₁₃} is non empty trivial V34() 1 -element countable set
[:{(s int_addr1)},{c₁₃}:] is Relation-like V34() countable set
bool [:{(s int_addr1)},{c₁₃}:] is V34() V38() countable set
t +* ((s int_addr1) .--> c₁₃) is Relation-like Function-like set
((t,(s int_addr1),c₁₃),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s int_addr1),c₁₃) +* (NAT .--> (succ (t))) is Relation-like Function-like set
c₁₈ is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of NAT
c₁₇ is Relation-like NAT -defined INT -valued Function-like V34() FinSequence-like FinSubsequence-like countable FinSequence of INT
Replace ((t,(s coll_addr1)),c₁₈,(t . (s int_addr1))) is Relation-like Function-like set
c₁₅ is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s coll_addr1),c₁₇) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(s coll_addr1) .--> c₁₇ is Relation-like SCM+FSA-Data*-Loc -defined {(s coll_addr1)} -defined Function-like one-to-one Function-yielding V33() V34() countable set
{(s coll_addr1)} is non empty trivial V34() 1 -element countable set
{(s coll_addr1)} --> c₁₇ is non empty Relation-like {(s coll_addr1)} -defined {c₁₇} -valued Function-like constant total quasi_total Function-yielding V33() V34() countable Element of bool [:{(s coll_addr1)},{c₁₇}:]
{c₁₇} is non empty trivial functional V34() V38() 1 -element with_common_domain countable set
[:{(s coll_addr1)},{c₁₇}:] is Relation-like V34() countable set
bool [:{(s coll_addr1)},{c₁₇}:] is V34() V38() countable set
t +* ((s coll_addr1) .--> c₁₇) is Relation-like Function-like set
((t,(s coll_addr1),c₁₇),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s coll_addr1),c₁₇) +* (NAT .--> (succ (t))) is Relation-like Function-like set
c₂₀ is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of NAT
c₁₉ is Relation-like NAT -defined INT -valued Function-like V34() FinSequence-like FinSubsequence-like countable FinSequence of INT
Replace ((t,(s coll_addr1)),c₂₀,(t . (s int_addr1))) is Relation-like Function-like set
c₁₆ is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s coll_addr1),c₁₉) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(s coll_addr1) .--> c₁₉ is Relation-like SCM+FSA-Data*-Loc -defined {(s coll_addr1)} -defined Function-like one-to-one Function-yielding V33() V34() countable set
{(s coll_addr1)} --> c₁₉ is non empty Relation-like {(s coll_addr1)} -defined {c₁₉} -valued Function-like constant total quasi_total Function-yielding V33() V34() countable Element of bool [:{(s coll_addr1)},{c₁₉}:]
{c₁₉} is non empty trivial functional V34() V38() 1 -element with_common_domain countable set
[:{(s coll_addr1)},{c₁₉}:] is Relation-like V34() countable set
bool [:{(s coll_addr1)},{c₁₉}:] is V34() V38() countable set
t +* ((s coll_addr1) .--> c₁₉) is Relation-like Function-like set
((t,(s coll_addr1),c₁₉),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s coll_addr1),c₁₉) +* (NAT .--> (succ (t))) is Relation-like Function-like set
c₂₁ is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
c₂₂ is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
c₂₆ is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of NAT
c₂₅ is Relation-like NAT -defined INT -valued Function-like V34() FinSequence-like FinSubsequence-like countable FinSequence of INT
c₂₆ |-> 0 is Relation-like NAT -defined NAT -valued Function-like V34() FinSequence-like FinSubsequence-like countable Element of c₂₆ -tuples_on NAT
c₂₆ -tuples_on NAT is FinSequenceSet of NAT
c₂₃ is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s coll_addr2),c₂₅) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(s coll_addr2) .--> c₂₅ is Relation-like SCM+FSA-Data*-Loc -defined {(s coll_addr2)} -defined Function-like one-to-one Function-yielding V33() V34() countable set
{(s coll_addr2)} is non empty trivial V34() 1 -element countable set
{(s coll_addr2)} --> c₂₅ is non empty Relation-like {(s coll_addr2)} -defined {c₂₅} -valued Function-like constant total quasi_total Function-yielding V33() V34() countable Element of bool [:{(s coll_addr2)},{c₂₅}:]
{c₂₅} is non empty trivial functional V34() V38() 1 -element with_common_domain countable set
[:{(s coll_addr2)},{c₂₅}:] is Relation-like V34() countable set
bool [:{(s coll_addr2)},{c₂₅}:] is V34() V38() countable set
t +* ((s coll_addr2) .--> c₂₅) is Relation-like Function-like set
((t,(s coll_addr2),c₂₅),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s coll_addr2),c₂₅) +* (NAT .--> (succ (t))) is Relation-like Function-like set
c₂₈ is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of NAT
c₂₇ is Relation-like NAT -defined INT -valued Function-like V34() FinSequence-like FinSubsequence-like countable FinSequence of INT
c₂₈ |-> 0 is Relation-like NAT -defined NAT -valued Function-like V34() FinSequence-like FinSubsequence-like countable Element of c₂₈ -tuples_on NAT
c₂₈ -tuples_on NAT is FinSequenceSet of NAT
c₂₄ is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s coll_addr2),c₂₇) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(s coll_addr2) .--> c₂₇ is Relation-like SCM+FSA-Data*-Loc -defined {(s coll_addr2)} -defined Function-like one-to-one Function-yielding V33() V34() countable set
{(s coll_addr2)} --> c₂₇ is non empty Relation-like {(s coll_addr2)} -defined {c₂₇} -valued Function-like constant total quasi_total Function-yielding V33() V34() countable Element of bool [:{(s coll_addr2)},{c₂₇}:]
{c₂₇} is non empty trivial functional V34() V38() 1 -element with_common_domain countable set
[:{(s coll_addr2)},{c₂₇}:] is Relation-like V34() countable set
bool [:{(s coll_addr2)},{c₂₇}:] is V34() V38() countable set
t +* ((s coll_addr2) .--> c₂₇) is Relation-like Function-like set
((t,(s coll_addr2),c₂₇),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s coll_addr2),c₂₇) +* (NAT .--> (succ (t))) is Relation-like Function-like set
c₃₁ is V11() V12() integer ext-real set
c₂₉ is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s int_addr),c₃₁) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(s int_addr) .--> c₃₁ is Relation-like SCM-Data-Loc -defined {(s int_addr)} -defined Function-like one-to-one V34() countable set
{(s int_addr)} is non empty trivial V34() 1 -element countable set
{(s int_addr)} --> c₃₁ is non empty Relation-like {(s int_addr)} -defined {c₃₁} -valued Function-like constant total quasi_total V34() countable Element of bool [:{(s int_addr)},{c₃₁}:]
{c₃₁} is non empty trivial V34() 1 -element countable set
[:{(s int_addr)},{c₃₁}:] is Relation-like V34() countable set
bool [:{(s int_addr)},{c₃₁}:] is V34() V38() countable set
t +* ((s int_addr) .--> c₃₁) is Relation-like Function-like set
((t,(s int_addr),c₃₁),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s int_addr),c₃₁) +* (NAT .--> (succ (t))) is Relation-like Function-like set
c₃₂ is V11() V12() integer ext-real set
c₃₀ is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s int_addr),c₃₂) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(s int_addr) .--> c₃₂ is Relation-like SCM-Data-Loc -defined {(s int_addr)} -defined Function-like one-to-one V34() countable set
{(s int_addr)} --> c₃₂ is non empty Relation-like {(s int_addr)} -defined {c₃₂} -valued Function-like constant total quasi_total V34() countable Element of bool [:{(s int_addr)},{c₃₂}:]
{c₃₂} is non empty trivial V34() 1 -element countable set
[:{(s int_addr)},{c₃₂}:] is Relation-like V34() countable set
bool [:{(s int_addr)},{c₃₂}:] is V34() V38() countable set
t +* ((s int_addr) .--> c₃₂) is Relation-like Function-like set
((t,(s int_addr),c₃₂),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s int_addr),c₃₂) +* (NAT .--> (succ (t))) is Relation-like Function-like set
c₃₃ is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
c₃₄ is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
mk is Element of SCM-Instr
fx is Relation-like SCM-Memory -defined Function-like SCM-OK * SCM-VAL -compatible Element of product (SCM-OK * SCM-VAL)
u is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
SCM-Exec-Res (mk,fx) is Relation-like SCM-Memory -defined Function-like SCM-OK * SCM-VAL -compatible Element of product (SCM-OK * SCM-VAL)
t +* (SCM-Exec-Res (mk,fx)) is Relation-like Function-like set
k is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of NAT
y is V11() V12() integer ext-real set
(t,(s coll_addr1)) /. k is V11() V12() integer ext-real Element of INT
(t,(s int_addr1),y) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(s int_addr1) .--> y is Relation-like SCM-Data-Loc -defined {(s int_addr1)} -defined Function-like one-to-one V34() countable set
{(s int_addr1)} is non empty trivial V34() 1 -element countable set
{(s int_addr1)} --> y is non empty Relation-like {(s int_addr1)} -defined {y} -valued Function-like constant total quasi_total V34() countable Element of bool [:{(s int_addr1)},{y}:]
{y} is non empty trivial V34() 1 -element countable set
[:{(s int_addr1)},{y}:] is Relation-like V34() countable set
bool [:{(s int_addr1)},{y}:] is V34() V38() countable set
t +* ((s int_addr1) .--> y) is Relation-like Function-like set
((t,(s int_addr1),y),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s int_addr1),y) +* (NAT .--> (succ (t))) is Relation-like Function-like set
k is Element of SCM-Instr
c₁₀ is Relation-like SCM-Memory -defined Function-like SCM-OK * SCM-VAL -compatible Element of product (SCM-OK * SCM-VAL)
f is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
SCM-Exec-Res (k,c₁₀) is Relation-like SCM-Memory -defined Function-like SCM-OK * SCM-VAL -compatible Element of product (SCM-OK * SCM-VAL)
t +* (SCM-Exec-Res (k,c₁₀)) is Relation-like Function-like set
c₁₂ is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of NAT
c₁₁ is Relation-like NAT -defined INT -valued Function-like V34() FinSequence-like FinSubsequence-like countable FinSequence of INT
Replace ((t,(s coll_addr1)),c₁₂,(t . (s int_addr1))) is Relation-like Function-like set
(t,(s coll_addr1),c₁₁) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(s coll_addr1) .--> c₁₁ is Relation-like SCM+FSA-Data*-Loc -defined {(s coll_addr1)} -defined Function-like one-to-one Function-yielding V33() V34() countable set
{(s coll_addr1)} is non empty trivial V34() 1 -element countable set
{(s coll_addr1)} --> c₁₁ is non empty Relation-like {(s coll_addr1)} -defined {c₁₁} -valued Function-like constant total quasi_total Function-yielding V33() V34() countable Element of bool [:{(s coll_addr1)},{c₁₁}:]
{c₁₁} is non empty trivial functional V34() V38() 1 -element with_common_domain countable set
[:{(s coll_addr1)},{c₁₁}:] is Relation-like V34() countable set
bool [:{(s coll_addr1)},{c₁₁}:] is V34() V38() countable set
t +* ((s coll_addr1) .--> c₁₁) is Relation-like Function-like set
((t,(s coll_addr1),c₁₁),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s coll_addr1),c₁₁) +* (NAT .--> (succ (t))) is Relation-like Function-like set
c₁₄ is Element of SCM-Instr
c₁₅ is Relation-like SCM-Memory -defined Function-like SCM-OK * SCM-VAL -compatible Element of product (SCM-OK * SCM-VAL)
c₁₃ is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
SCM-Exec-Res (c₁₄,c₁₅) is Relation-like SCM-Memory -defined Function-like SCM-OK * SCM-VAL -compatible Element of product (SCM-OK * SCM-VAL)
t +* (SCM-Exec-Res (c₁₄,c₁₅)) is Relation-like Function-like set
c₁₇ is Element of SCM-Instr
c₁₈ is Relation-like SCM-Memory -defined Function-like SCM-OK * SCM-VAL -compatible Element of product (SCM-OK * SCM-VAL)
c₁₆ is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
SCM-Exec-Res (c₁₇,c₁₈) is Relation-like SCM-Memory -defined Function-like SCM-OK * SCM-VAL -compatible Element of product (SCM-OK * SCM-VAL)
t +* (SCM-Exec-Res (c₁₇,c₁₈)) is Relation-like Function-like set
c₂₀ is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of NAT
c₁₉ is Relation-like NAT -defined INT -valued Function-like V34() FinSequence-like FinSubsequence-like countable FinSequence of INT
c₂₀ |-> 0 is Relation-like NAT -defined NAT -valued Function-like V34() FinSequence-like FinSubsequence-like countable Element of c₂₀ -tuples_on NAT
c₂₀ -tuples_on NAT is FinSequenceSet of NAT
(t,(s coll_addr2),c₁₉) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(s coll_addr2) .--> c₁₉ is Relation-like SCM+FSA-Data*-Loc -defined {(s coll_addr2)} -defined Function-like one-to-one Function-yielding V33() V34() countable set
{(s coll_addr2)} is non empty trivial V34() 1 -element countable set
{(s coll_addr2)} --> c₁₉ is non empty Relation-like {(s coll_addr2)} -defined {c₁₉} -valued Function-like constant total quasi_total Function-yielding V33() V34() countable Element of bool [:{(s coll_addr2)},{c₁₉}:]
{c₁₉} is non empty trivial functional V34() V38() 1 -element with_common_domain countable set
[:{(s coll_addr2)},{c₁₉}:] is Relation-like V34() countable set
bool [:{(s coll_addr2)},{c₁₉}:] is V34() V38() countable set
t +* ((s coll_addr2) .--> c₁₉) is Relation-like Function-like set
((t,(s coll_addr2),c₁₉),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s coll_addr2),c₁₉) +* (NAT .--> (succ (t))) is Relation-like Function-like set
c₂₂ is Element of SCM-Instr
c₂₃ is Relation-like SCM-Memory -defined Function-like SCM-OK * SCM-VAL -compatible Element of product (SCM-OK * SCM-VAL)
c₂₁ is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
SCM-Exec-Res (c₂₂,c₂₃) is Relation-like SCM-Memory -defined Function-like SCM-OK * SCM-VAL -compatible Element of product (SCM-OK * SCM-VAL)
t +* (SCM-Exec-Res (c₂₂,c₂₃)) is Relation-like Function-like set
c₂₄ is V11() V12() integer ext-real set
(t,(s int_addr),c₂₄) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(s int_addr) .--> c₂₄ is Relation-like SCM-Data-Loc -defined {(s int_addr)} -defined Function-like one-to-one V34() countable set
{(s int_addr)} is non empty trivial V34() 1 -element countable set
{(s int_addr)} --> c₂₄ is non empty Relation-like {(s int_addr)} -defined {c₂₄} -valued Function-like constant total quasi_total V34() countable Element of bool [:{(s int_addr)},{c₂₄}:]
{c₂₄} is non empty trivial V34() 1 -element countable set
[:{(s int_addr)},{c₂₄}:] is Relation-like V34() countable set
bool [:{(s int_addr)},{c₂₄}:] is V34() V38() countable set
t +* ((s int_addr) .--> c₂₄) is Relation-like Function-like set
((t,(s int_addr),c₂₄),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s int_addr),c₂₄) +* (NAT .--> (succ (t))) is Relation-like Function-like set
c₂₇ is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of NAT
c₂₆ is V11() V12() integer ext-real set
(t,(s coll_addr1)) /. c₂₇ is V11() V12() integer ext-real Element of INT
c₂₅ is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s int_addr1),c₂₆) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(s int_addr1) .--> c₂₆ is Relation-like SCM-Data-Loc -defined {(s int_addr1)} -defined Function-like one-to-one V34() countable set
{(s int_addr1)} --> c₂₆ is non empty Relation-like {(s int_addr1)} -defined {c₂₆} -valued Function-like constant total quasi_total V34() countable Element of bool [:{(s int_addr1)},{c₂₆}:]
{c₂₆} is non empty trivial V34() 1 -element countable set
[:{(s int_addr1)},{c₂₆}:] is Relation-like V34() countable set
bool [:{(s int_addr1)},{c₂₆}:] is V34() V38() countable set
t +* ((s int_addr1) .--> c₂₆) is Relation-like Function-like set
((t,(s int_addr1),c₂₆),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s int_addr1),c₂₆) +* (NAT .--> (succ (t))) is Relation-like Function-like set
c₂₉ is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of NAT
c₂₈ is Relation-like NAT -defined INT -valued Function-like V34() FinSequence-like FinSubsequence-like countable FinSequence of INT
Replace ((t,(s coll_addr1)),c₂₉,(t . (s int_addr1))) is Relation-like Function-like set
(t,(s coll_addr1),c₂₈) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(s coll_addr1) .--> c₂₈ is Relation-like SCM+FSA-Data*-Loc -defined {(s coll_addr1)} -defined Function-like one-to-one Function-yielding V33() V34() countable set
{(s coll_addr1)} --> c₂₈ is non empty Relation-like {(s coll_addr1)} -defined {c₂₈} -valued Function-like constant total quasi_total Function-yielding V33() V34() countable Element of bool [:{(s coll_addr1)},{c₂₈}:]
{c₂₈} is non empty trivial functional V34() V38() 1 -element with_common_domain countable set
[:{(s coll_addr1)},{c₂₈}:] is Relation-like V34() countable set
bool [:{(s coll_addr1)},{c₂₈}:] is V34() V38() countable set
t +* ((s coll_addr1) .--> c₂₈) is Relation-like Function-like set
((t,(s coll_addr1),c₂₈),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s coll_addr1),c₂₈) +* (NAT .--> (succ (t))) is Relation-like Function-like set
c₃₂ is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of NAT
c₃₁ is V11() V12() integer ext-real set
(t,(s coll_addr1)) /. c₃₂ is V11() V12() integer ext-real Element of INT
c₃₀ is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s int_addr1),c₃₁) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(s int_addr1) .--> c₃₁ is Relation-like SCM-Data-Loc -defined {(s int_addr1)} -defined Function-like one-to-one V34() countable set
{(s int_addr1)} --> c₃₁ is non empty Relation-like {(s int_addr1)} -defined {c₃₁} -valued Function-like constant total quasi_total V34() countable Element of bool [:{(s int_addr1)},{c₃₁}:]
{c₃₁} is non empty trivial V34() 1 -element countable set
[:{(s int_addr1)},{c₃₁}:] is Relation-like V34() countable set
bool [:{(s int_addr1)},{c₃₁}:] is V34() V38() countable set
t +* ((s int_addr1) .--> c₃₁) is Relation-like Function-like set
((t,(s int_addr1),c₃₁),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s int_addr1),c₃₁) +* (NAT .--> (succ (t))) is Relation-like Function-like set
c₃₅ is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of NAT
c₃₄ is V11() V12() integer ext-real set
(t,(s coll_addr1)) /. c₃₅ is V11() V12() integer ext-real Element of INT
c₃₃ is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s int_addr1),c₃₄) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(s int_addr1) .--> c₃₄ is Relation-like SCM-Data-Loc -defined {(s int_addr1)} -defined Function-like one-to-one V34() countable set
{(s int_addr1)} --> c₃₄ is non empty Relation-like {(s int_addr1)} -defined {c₃₄} -valued Function-like constant total quasi_total V34() countable Element of bool [:{(s int_addr1)},{c₃₄}:]
{c₃₄} is non empty trivial V34() 1 -element countable set
[:{(s int_addr1)},{c₃₄}:] is Relation-like V34() countable set
bool [:{(s int_addr1)},{c₃₄}:] is V34() V38() countable set
t +* ((s int_addr1) .--> c₃₄) is Relation-like Function-like set
((t,(s int_addr1),c₃₄),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s int_addr1),c₃₄) +* (NAT .--> (succ (t))) is Relation-like Function-like set
c₃₇ is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of NAT
c₃₆ is Relation-like NAT -defined INT -valued Function-like V34() FinSequence-like FinSubsequence-like countable FinSequence of INT
c₃₇ |-> 0 is Relation-like NAT -defined NAT -valued Function-like V34() FinSequence-like FinSubsequence-like countable Element of c₃₇ -tuples_on NAT
c₃₇ -tuples_on NAT is FinSequenceSet of NAT
(t,(s coll_addr2),c₃₆) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(s coll_addr2) .--> c₃₆ is Relation-like SCM+FSA-Data*-Loc -defined {(s coll_addr2)} -defined Function-like one-to-one Function-yielding V33() V34() countable set
{(s coll_addr2)} --> c₃₆ is non empty Relation-like {(s coll_addr2)} -defined {c₃₆} -valued Function-like constant total quasi_total Function-yielding V33() V34() countable Element of bool [:{(s coll_addr2)},{c₃₆}:]
{c₃₆} is non empty trivial functional V34() V38() 1 -element with_common_domain countable set
[:{(s coll_addr2)},{c₃₆}:] is Relation-like V34() countable set
bool [:{(s coll_addr2)},{c₃₆}:] is V34() V38() countable set
t +* ((s coll_addr2) .--> c₃₆) is Relation-like Function-like set
((t,(s coll_addr2),c₃₆),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s coll_addr2),c₃₆) +* (NAT .--> (succ (t))) is Relation-like Function-like set
c₄₀ is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of NAT
c₃₉ is V11() V12() integer ext-real set
(t,(s coll_addr1)) /. c₄₀ is V11() V12() integer ext-real Element of INT
c₃₈ is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s int_addr1),c₃₉) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(s int_addr1) .--> c₃₉ is Relation-like SCM-Data-Loc -defined {(s int_addr1)} -defined Function-like one-to-one V34() countable set
{(s int_addr1)} --> c₃₉ is non empty Relation-like {(s int_addr1)} -defined {c₃₉} -valued Function-like constant total quasi_total V34() countable Element of bool [:{(s int_addr1)},{c₃₉}:]
{c₃₉} is non empty trivial V34() 1 -element countable set
[:{(s int_addr1)},{c₃₉}:] is Relation-like V34() countable set
bool [:{(s int_addr1)},{c₃₉}:] is V34() V38() countable set
t +* ((s int_addr1) .--> c₃₉) is Relation-like Function-like set
((t,(s int_addr1),c₃₉),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s int_addr1),c₃₉) +* (NAT .--> (succ (t))) is Relation-like Function-like set
c₄₁ is V11() V12() integer ext-real set
(t,(s int_addr),c₄₁) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(s int_addr) .--> c₄₁ is Relation-like SCM-Data-Loc -defined {(s int_addr)} -defined Function-like one-to-one V34() countable set
{(s int_addr)} --> c₄₁ is non empty Relation-like {(s int_addr)} -defined {c₄₁} -valued Function-like constant total quasi_total V34() countable Element of bool [:{(s int_addr)},{c₄₁}:]
{c₄₁} is non empty trivial V34() 1 -element countable set
[:{(s int_addr)},{c₄₁}:] is Relation-like V34() countable set
bool [:{(s int_addr)},{c₄₁}:] is V34() V38() countable set
t +* ((s int_addr) .--> c₄₁) is Relation-like Function-like set
((t,(s int_addr),c₄₁),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s int_addr),c₄₁) +* (NAT .--> (succ (t))) is Relation-like Function-like set
c₄₄ is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of NAT
c₄₃ is Relation-like NAT -defined INT -valued Function-like V34() FinSequence-like FinSubsequence-like countable FinSequence of INT
Replace ((t,(s coll_addr1)),c₄₄,(t . (s int_addr1))) is Relation-like Function-like set
c₄₂ is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s coll_addr1),c₄₃) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(s coll_addr1) .--> c₄₃ is Relation-like SCM+FSA-Data*-Loc -defined {(s coll_addr1)} -defined Function-like one-to-one Function-yielding V33() V34() countable set
{(s coll_addr1)} --> c₄₃ is non empty Relation-like {(s coll_addr1)} -defined {c₄₃} -valued Function-like constant total quasi_total Function-yielding V33() V34() countable Element of bool [:{(s coll_addr1)},{c₄₃}:]
{c₄₃} is non empty trivial functional V34() V38() 1 -element with_common_domain countable set
[:{(s coll_addr1)},{c₄₃}:] is Relation-like V34() countable set
bool [:{(s coll_addr1)},{c₄₃}:] is V34() V38() countable set
t +* ((s coll_addr1) .--> c₄₃) is Relation-like Function-like set
((t,(s coll_addr1),c₄₃),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s coll_addr1),c₄₃) +* (NAT .--> (succ (t))) is Relation-like Function-like set
c₄₇ is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of NAT
c₄₆ is Relation-like NAT -defined INT -valued Function-like V34() FinSequence-like FinSubsequence-like countable FinSequence of INT
Replace ((t,(s coll_addr1)),c₄₇,(t . (s int_addr1))) is Relation-like Function-like set
c₄₅ is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s coll_addr1),c₄₆) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(s coll_addr1) .--> c₄₆ is Relation-like SCM+FSA-Data*-Loc -defined {(s coll_addr1)} -defined Function-like one-to-one Function-yielding V33() V34() countable set
{(s coll_addr1)} --> c₄₆ is non empty Relation-like {(s coll_addr1)} -defined {c₄₆} -valued Function-like constant total quasi_total Function-yielding V33() V34() countable Element of bool [:{(s coll_addr1)},{c₄₆}:]
{c₄₆} is non empty trivial functional V34() V38() 1 -element with_common_domain countable set
[:{(s coll_addr1)},{c₄₆}:] is Relation-like V34() countable set
bool [:{(s coll_addr1)},{c₄₆}:] is V34() V38() countable set
t +* ((s coll_addr1) .--> c₄₆) is Relation-like Function-like set
((t,(s coll_addr1),c₄₆),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s coll_addr1),c₄₆) +* (NAT .--> (succ (t))) is Relation-like Function-like set
c₄₉ is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of NAT
c₄₈ is Relation-like NAT -defined INT -valued Function-like V34() FinSequence-like FinSubsequence-like countable FinSequence of INT
c₄₉ |-> 0 is Relation-like NAT -defined NAT -valued Function-like V34() FinSequence-like FinSubsequence-like countable Element of c₄₉ -tuples_on NAT
c₄₉ -tuples_on NAT is FinSequenceSet of NAT
(t,(s coll_addr2),c₄₈) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(s coll_addr2) .--> c₄₈ is Relation-like SCM+FSA-Data*-Loc -defined {(s coll_addr2)} -defined Function-like one-to-one Function-yielding V33() V34() countable set
{(s coll_addr2)} --> c₄₈ is non empty Relation-like {(s coll_addr2)} -defined {c₄₈} -valued Function-like constant total quasi_total Function-yielding V33() V34() countable Element of bool [:{(s coll_addr2)},{c₄₈}:]
{c₄₈} is non empty trivial functional V34() V38() 1 -element with_common_domain countable set
[:{(s coll_addr2)},{c₄₈}:] is Relation-like V34() countable set
bool [:{(s coll_addr2)},{c₄₈}:] is V34() V38() countable set
t +* ((s coll_addr2) .--> c₄₈) is Relation-like Function-like set
((t,(s coll_addr2),c₄₈),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s coll_addr2),c₄₈) +* (NAT .--> (succ (t))) is Relation-like Function-like set
c₅₂ is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of NAT
c₅₁ is Relation-like NAT -defined INT -valued Function-like V34() FinSequence-like FinSubsequence-like countable FinSequence of INT
Replace ((t,(s coll_addr1)),c₅₂,(t . (s int_addr1))) is Relation-like Function-like set
c₅₀ is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s coll_addr1),c₅₁) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(s coll_addr1) .--> c₅₁ is Relation-like SCM+FSA-Data*-Loc -defined {(s coll_addr1)} -defined Function-like one-to-one Function-yielding V33() V34() countable set
{(s coll_addr1)} --> c₅₁ is non empty Relation-like {(s coll_addr1)} -defined {c₅₁} -valued Function-like constant total quasi_total Function-yielding V33() V34() countable Element of bool [:{(s coll_addr1)},{c₅₁}:]
{c₅₁} is non empty trivial functional V34() V38() 1 -element with_common_domain countable set
[:{(s coll_addr1)},{c₅₁}:] is Relation-like V34() countable set
bool [:{(s coll_addr1)},{c₅₁}:] is V34() V38() countable set
t +* ((s coll_addr1) .--> c₅₁) is Relation-like Function-like set
((t,(s coll_addr1),c₅₁),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s coll_addr1),c₅₁) +* (NAT .--> (succ (t))) is Relation-like Function-like set
c₅₃ is V11() V12() integer ext-real set
(t,(s int_addr),c₅₃) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(s int_addr) .--> c₅₃ is Relation-like SCM-Data-Loc -defined {(s int_addr)} -defined Function-like one-to-one V34() countable set
{(s int_addr)} --> c₅₃ is non empty Relation-like {(s int_addr)} -defined {c₅₃} -valued Function-like constant total quasi_total V34() countable Element of bool [:{(s int_addr)},{c₅₃}:]
{c₅₃} is non empty trivial V34() 1 -element countable set
[:{(s int_addr)},{c₅₃}:] is Relation-like V34() countable set
bool [:{(s int_addr)},{c₅₃}:] is V34() V38() countable set
t +* ((s int_addr) .--> c₅₃) is Relation-like Function-like set
((t,(s int_addr),c₅₃),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s int_addr),c₅₃) +* (NAT .--> (succ (t))) is Relation-like Function-like set
c₅₄ is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
c₅₆ is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of NAT
c₅₅ is Relation-like NAT -defined INT -valued Function-like V34() FinSequence-like FinSubsequence-like countable FinSequence of INT
c₅₆ |-> 0 is Relation-like NAT -defined NAT -valued Function-like V34() FinSequence-like FinSubsequence-like countable Element of c₅₆ -tuples_on NAT
c₅₆ -tuples_on NAT is FinSequenceSet of NAT
(t,(s coll_addr2),c₅₅) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(s coll_addr2) .--> c₅₅ is Relation-like SCM+FSA-Data*-Loc -defined {(s coll_addr2)} -defined Function-like one-to-one Function-yielding V33() V34() countable set
{(s coll_addr2)} --> c₅₅ is non empty Relation-like {(s coll_addr2)} -defined {c₅₅} -valued Function-like constant total quasi_total Function-yielding V33() V34() countable Element of bool [:{(s coll_addr2)},{c₅₅}:]
{c₅₅} is non empty trivial functional V34() V38() 1 -element with_common_domain countable set
[:{(s coll_addr2)},{c₅₅}:] is Relation-like V34() countable set
bool [:{(s coll_addr2)},{c₅₅}:] is V34() V38() countable set
t +* ((s coll_addr2) .--> c₅₅) is Relation-like Function-like set
((t,(s coll_addr2),c₅₅),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s coll_addr2),c₅₅) +* (NAT .--> (succ (t))) is Relation-like Function-like set
c₅₇ is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
c₅₈ is V11() V12() integer ext-real set
(t,(s int_addr),c₅₈) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(s int_addr) .--> c₅₈ is Relation-like SCM-Data-Loc -defined {(s int_addr)} -defined Function-like one-to-one V34() countable set
{(s int_addr)} --> c₅₈ is non empty Relation-like {(s int_addr)} -defined {c₅₈} -valued Function-like constant total quasi_total V34() countable Element of bool [:{(s int_addr)},{c₅₈}:]
{c₅₈} is non empty trivial V34() 1 -element countable set
[:{(s int_addr)},{c₅₈}:] is Relation-like V34() countable set
bool [:{(s int_addr)},{c₅₈}:] is V34() V38() countable set
t +* ((s int_addr) .--> c₅₈) is Relation-like Function-like set
((t,(s int_addr),c₅₈),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s int_addr),c₅₈) +* (NAT .--> (succ (t))) is Relation-like Function-like set
c₆₁ is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of NAT
c₆₀ is Relation-like NAT -defined INT -valued Function-like V34() FinSequence-like FinSubsequence-like countable FinSequence of INT
c₆₁ |-> 0 is Relation-like NAT -defined NAT -valued Function-like V34() FinSequence-like FinSubsequence-like countable Element of c₆₁ -tuples_on NAT
c₆₁ -tuples_on NAT is FinSequenceSet of NAT
c₅₉ is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s coll_addr2),c₆₀) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(s coll_addr2) .--> c₆₀ is Relation-like SCM+FSA-Data*-Loc -defined {(s coll_addr2)} -defined Function-like one-to-one Function-yielding V33() V34() countable set
{(s coll_addr2)} --> c₆₀ is non empty Relation-like {(s coll_addr2)} -defined {c₆₀} -valued Function-like constant total quasi_total Function-yielding V33() V34() countable Element of bool [:{(s coll_addr2)},{c₆₀}:]
{c₆₀} is non empty trivial functional V34() V38() 1 -element with_common_domain countable set
[:{(s coll_addr2)},{c₆₀}:] is Relation-like V34() countable set
bool [:{(s coll_addr2)},{c₆₀}:] is V34() V38() countable set
t +* ((s coll_addr2) .--> c₆₀) is Relation-like Function-like set
((t,(s coll_addr2),c₆₀),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s coll_addr2),c₆₀) +* (NAT .--> (succ (t))) is Relation-like Function-like set
c₆₂ is V11() V12() integer ext-real set
(t,(s int_addr),c₆₂) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(s int_addr) .--> c₆₂ is Relation-like SCM-Data-Loc -defined {(s int_addr)} -defined Function-like one-to-one V34() countable set
{(s int_addr)} --> c₆₂ is non empty Relation-like {(s int_addr)} -defined {c₆₂} -valued Function-like constant total quasi_total V34() countable Element of bool [:{(s int_addr)},{c₆₂}:]
{c₆₂} is non empty trivial V34() 1 -element countable set
[:{(s int_addr)},{c₆₂}:] is Relation-like V34() countable set
bool [:{(s int_addr)},{c₆₂}:] is V34() V38() countable set
t +* ((s int_addr) .--> c₆₂) is Relation-like Function-like set
((t,(s int_addr),c₆₂),(succ (t))) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(t,(s int_addr),c₆₂) +* (NAT .--> (succ (t))) is Relation-like Function-like set
Funcs ((product (() * ())),(product (() * ()))) is non empty functional set
[:SCM+FSA-Instr,(Funcs ((product (() * ())),(product (() * ())))):] is Relation-like set
bool [:SCM+FSA-Instr,(Funcs ((product (() * ())),(product (() * ())))):] is set
[:SCM+FSA-Instr,(product (() * ())):] is Relation-like set
[:[:SCM+FSA-Instr,(product (() * ())):],(product (() * ())):] is Relation-like set
bool [:[:SCM+FSA-Instr,(product (() * ())):],(product (() * ())):] is set
s is Relation-like [:SCM+FSA-Instr,(product (() * ())):] -defined product (() * ()) -valued Function-like total quasi_total Function-yielding V33() Element of bool [:[:SCM+FSA-Instr,(product (() * ())):],(product (() * ())):]
curry s is non empty Relation-like SCM+FSA-Instr -defined Funcs ((product (() * ())),(product (() * ()))) -valued Function-like total quasi_total Function-yielding V33() Element of bool [:SCM+FSA-Instr,(Funcs ((product (() * ())),(product (() * ())))):]
Funcs ((product (() * ())),(product (() * ()))) is non empty functional FUNCTION_DOMAIN of product (() * ()), product (() * ())
[:SCM+FSA-Instr,(Funcs ((product (() * ())),(product (() * ())))):] is Relation-like set
bool [:SCM+FSA-Instr,(Funcs ((product (() * ())),(product (() * ())))):] is set
t is Element of SCM+FSA-Instr
(curry s) . t is Relation-like Function-like Element of Funcs ((product (() * ())),(product (() * ())))
u is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
((curry s) . t) . u is set
(t,u) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(curry s) . t is Relation-like product (() * ()) -defined product (() * ()) -valued Function-like total quasi_total Function-yielding V33() Element of Funcs ((product (() * ())),(product (() * ())))
((curry s) . t) . u is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
s . (t,u) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
Funcs ((product (() * ())),(product (() * ()))) is non empty functional FUNCTION_DOMAIN of product (() * ()), product (() * ())
[:SCM+FSA-Instr,(Funcs ((product (() * ())),(product (() * ())))):] is Relation-like set
bool [:SCM+FSA-Instr,(Funcs ((product (() * ())),(product (() * ())))):] is set
s is non empty Relation-like SCM+FSA-Instr -defined Funcs ((product (() * ())),(product (() * ()))) -valued Function-like total quasi_total Function-yielding V33() Element of bool [:SCM+FSA-Instr,(Funcs ((product (() * ())),(product (() * ())))):]
t is non empty Relation-like SCM+FSA-Instr -defined Funcs ((product (() * ())),(product (() * ()))) -valued Function-like total quasi_total Function-yielding V33() Element of bool [:SCM+FSA-Instr,(Funcs ((product (() * ())),(product (() * ())))):]
[:(product (() * ())),(product (() * ())):] is Relation-like set
bool [:(product (() * ())),(product (() * ())):] is set
u is Element of SCM+FSA-Instr
t . u is Relation-like product (() * ()) -defined product (() * ()) -valued Function-like total quasi_total Function-yielding V33() Element of Funcs ((product (() * ())),(product (() * ())))
s . u is Relation-like product (() * ()) -defined product (() * ()) -valued Function-like total quasi_total Function-yielding V33() Element of Funcs ((product (() * ())),(product (() * ())))
fx is non empty Relation-like product (() * ()) -defined product (() * ()) -valued Function-like total quasi_total Function-yielding V33() Element of bool [:(product (() * ())),(product (() * ())):]
y is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
fx . y is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
(u,y) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
mk is non empty Relation-like product (() * ()) -defined product (() * ()) -valued Function-like total quasi_total Function-yielding V33() Element of bool [:(product (() * ())),(product (() * ())):]
mk . y is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
() is non empty Relation-like SCM+FSA-Instr -defined Funcs ((product (() * ())),(product (() * ()))) -valued Function-like total quasi_total Function-yielding V33() Element of bool [:SCM+FSA-Instr,(Funcs ((product (() * ())),(product (() * ())))):]
s is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
t is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of NAT
(s,t) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
NAT .--> t is Relation-like {NAT} -defined NAT -valued Function-like one-to-one V34() Cardinal-yielding countable set
{NAT} --> t is non empty Relation-like {NAT} -defined NAT -valued {t} -valued Function-like constant total quasi_total V34() Cardinal-yielding countable Element of bool [:{NAT},{t}:]
{t} is non empty trivial V34() V38() 1 -element countable set
[:{NAT},{t}:] is Relation-like V34() countable set
bool [:{NAT},{t}:] is V34() V38() countable set
s +* (NAT .--> t) is Relation-like Function-like set
(s,t) . NAT is set
proj1 (NAT .--> t) is V34() countable set
(NAT .--> t) . NAT is set
s is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
t is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of NAT
(s,t) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
NAT .--> t is Relation-like {NAT} -defined NAT -valued Function-like one-to-one V34() Cardinal-yielding countable set
{NAT} --> t is non empty Relation-like {NAT} -defined NAT -valued {t} -valued Function-like constant total quasi_total V34() Cardinal-yielding countable Element of bool [:{NAT},{t}:]
{t} is non empty trivial V34() V38() 1 -element countable set
[:{NAT},{t}:] is Relation-like V34() countable set
bool [:{NAT},{t}:] is V34() V38() countable set
s +* (NAT .--> t) is Relation-like Function-like set
u is Element of ()
(s,t) . u is V11() V12() integer ext-real set
s . u is V11() V12() integer ext-real set
(() * ()) . u is set
proj1 (NAT .--> t) is V34() countable set
s is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
t is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of NAT
(s,t) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
NAT .--> t is Relation-like {NAT} -defined NAT -valued Function-like one-to-one V34() Cardinal-yielding countable set
{NAT} --> t is non empty Relation-like {NAT} -defined NAT -valued {t} -valued Function-like constant total quasi_total V34() Cardinal-yielding countable Element of bool [:{NAT},{t}:]
{t} is non empty trivial V34() V38() 1 -element countable set
[:{NAT},{t}:] is Relation-like V34() countable set
bool [:{NAT},{t}:] is V34() V38() countable set
s +* (NAT .--> t) is Relation-like Function-like set
u is Element of ()
((s,t),u) is Relation-like NAT -defined INT -valued Function-like V34() FinSequence-like FinSubsequence-like countable FinSequence of INT
(s,u) is Relation-like NAT -defined INT -valued Function-like V34() FinSequence-like FinSubsequence-like countable FinSequence of INT
proj1 (NAT .--> t) is V34() countable set
() . u is epsilon-transitive epsilon-connected ordinal Element of 3
s is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
t is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of NAT
(s,t) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
NAT .--> t is Relation-like {NAT} -defined NAT -valued Function-like one-to-one V34() Cardinal-yielding countable set
{NAT} --> t is non empty Relation-like {NAT} -defined NAT -valued {t} -valued Function-like constant total quasi_total V34() Cardinal-yielding countable Element of bool [:{NAT},{t}:]
{t} is non empty trivial V34() V38() 1 -element countable set
[:{NAT},{t}:] is Relation-like V34() countable set
bool [:{NAT},{t}:] is V34() V38() countable set
s +* (NAT .--> t) is Relation-like Function-like set
u is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V34() cardinal countable ext-real Element of NAT
(s,t) . u is set
s . u is set
proj1 (NAT .--> t) is V34() countable set
s is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
s . NAT is set
t is Element of ()
u is V11() V12() integer ext-real set
(s,t,u) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
t .--> u is Relation-like () -defined {t} -defined Function-like one-to-one V34() countable set
{t} is non empty trivial V34() 1 -element countable set
{t} --> u is non empty Relation-like {t} -defined {u} -valued Function-like constant total quasi_total V34() countable Element of bool [:{t},{u}:]
{u} is non empty trivial V34() 1 -element countable set
[:{t},{u}:] is Relation-like V34() countable set
bool [:{t},{u}:] is V34() V38() countable set
s +* (t .--> u) is Relation-like Function-like set
(s,t,u) . NAT is set
(() * ()) . t is set
proj1 (t .--> u) is V34() countable set
s is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
t is Element of ()
u is V11() V12() integer ext-real set
(s,t,u) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
t .--> u is Relation-like () -defined {t} -defined Function-like one-to-one V34() countable set
{t} is non empty trivial V34() 1 -element countable set
{t} --> u is non empty Relation-like {t} -defined {u} -valued Function-like constant total quasi_total V34() countable Element of bool [:{t},{u}:]
{u} is non empty trivial V34() 1 -element countable set
[:{t},{u}:] is Relation-like V34() countable set
bool [:{t},{u}:] is V34() V38() countable set
s +* (t .--> u) is Relation-like Function-like set
(s,t,u) . t is V11() V12() integer ext-real set
proj1 (t .--> u) is V34() countable set
(t .--> u) . t is set
s is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
t is Element of ()
u is V11() V12() integer ext-real set
(s,t,u) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
t .--> u is Relation-like () -defined {t} -defined Function-like one-to-one V34() countable set
{t} is non empty trivial V34() 1 -element countable set
{t} --> u is non empty Relation-like {t} -defined {u} -valued Function-like constant total quasi_total V34() countable Element of bool [:{t},{u}:]
{u} is non empty trivial V34() 1 -element countable set
[:{t},{u}:] is Relation-like V34() countable set
bool [:{t},{u}:] is V34() V38() countable set
s +* (t .--> u) is Relation-like Function-like set
mk is Element of ()
(s,t,u) . mk is V11() V12() integer ext-real set
s . mk is V11() V12() integer ext-real set
proj1 (t .--> u) is V34() countable set
s is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
t is Element of ()
u is V11() V12() integer ext-real set
(s,t,u) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
t .--> u is Relation-like () -defined {t} -defined Function-like one-to-one V34() countable set
{t} is non empty trivial V34() 1 -element countable set
{t} --> u is non empty Relation-like {t} -defined {u} -valued Function-like constant total quasi_total V34() countable Element of bool [:{t},{u}:]
{u} is non empty trivial V34() 1 -element countable set
[:{t},{u}:] is Relation-like V34() countable set
bool [:{t},{u}:] is V34() V38() countable set
s +* (t .--> u) is Relation-like Function-like set
mk is Element of ()
((s,t,u),mk) is Relation-like NAT -defined INT -valued Function-like V34() FinSequence-like FinSubsequence-like countable FinSequence of INT
(s,mk) is Relation-like NAT -defined INT -valued Function-like V34() FinSequence-like FinSubsequence-like countable FinSequence of INT
proj1 (t .--> u) is V34() countable set
(() * ()) . t is set
(() * ()) . mk is set
s is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
t is Element of ()
u is Relation-like NAT -defined INT -valued Function-like V34() FinSequence-like FinSubsequence-like countable FinSequence of INT
(s,t,u) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
t .--> u is Relation-like () -defined {t} -defined Function-like one-to-one Function-yielding V33() V34() countable set
{t} is non empty trivial V34() 1 -element countable set
{t} --> u is non empty Relation-like {t} -defined {u} -valued Function-like constant total quasi_total Function-yielding V33() V34() countable Element of bool [:{t},{u}:]
{u} is non empty trivial functional V34() V38() 1 -element with_common_domain countable set
[:{t},{u}:] is Relation-like V34() countable set
bool [:{t},{u}:] is V34() V38() countable set
s +* (t .--> u) is Relation-like Function-like set
((s,t,u),t) is Relation-like NAT -defined INT -valued Function-like V34() FinSequence-like FinSubsequence-like countable FinSequence of INT
proj1 (t .--> u) is V34() countable set
(t .--> u) . t is Relation-like Function-like set
s is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
t is Element of ()
u is Relation-like NAT -defined INT -valued Function-like V34() FinSequence-like FinSubsequence-like countable FinSequence of INT
(s,t,u) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
t .--> u is Relation-like () -defined {t} -defined Function-like one-to-one Function-yielding V33() V34() countable set
{t} is non empty trivial V34() 1 -element countable set
{t} --> u is non empty Relation-like {t} -defined {u} -valued Function-like constant total quasi_total Function-yielding V33() V34() countable Element of bool [:{t},{u}:]
{u} is non empty trivial functional V34() V38() 1 -element with_common_domain countable set
[:{t},{u}:] is Relation-like V34() countable set
bool [:{t},{u}:] is V34() V38() countable set
s +* (t .--> u) is Relation-like Function-like set
mk is Element of ()
((s,t,u),mk) is Relation-like NAT -defined INT -valued Function-like V34() FinSequence-like FinSubsequence-like countable FinSequence of INT
(s,mk) is Relation-like NAT -defined INT -valued Function-like V34() FinSequence-like FinSubsequence-like countable FinSequence of INT
proj1 (t .--> u) is V34() countable set
s is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
t is Element of ()
u is Relation-like NAT -defined INT -valued Function-like V34() FinSequence-like FinSubsequence-like countable FinSequence of INT
(s,t,u) is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
t .--> u is Relation-like () -defined {t} -defined Function-like one-to-one Function-yielding V33() V34() countable set
{t} is non empty trivial V34() 1 -element countable set
{t} --> u is non empty Relation-like {t} -defined {u} -valued Function-like constant total quasi_total Function-yielding V33() V34() countable Element of bool [:{t},{u}:]
{u} is non empty trivial functional V34() V38() 1 -element with_common_domain countable set
[:{t},{u}:] is Relation-like V34() countable set
bool [:{t},{u}:] is V34() V38() countable set
s +* (t .--> u) is Relation-like Function-like set
mk is Element of ()
(s,t,u) . mk is V11() V12() integer ext-real set
s . mk is V11() V12() integer ext-real set
proj1 (t .--> u) is V34() countable set
(() * ()) . t is set
(() * ()) . mk is set
s is Relation-like () -defined Function-like () * () -compatible Element of product (() * ())
proj1 s is set