:: AMI_2 semantic presentation

REAL is non empty non trivial V31() set
NAT is non trivial ordinal V31() cardinal limit_cardinal countable denumerable Element of bool REAL
bool REAL is non trivial V31() set
{} is empty Function-like functional ordinal natural V31() V35() cardinal {} -element countable V86() integer V111() ext-real non positive non negative set
1 is non empty ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT
{{},1} is non empty V31() V35() countable set
omega is non trivial ordinal V31() cardinal limit_cardinal countable denumerable set
bool omega is non trivial V31() set
bool NAT is non trivial V31() set
COMPLEX is non empty non trivial V31() set
RAT is non empty non trivial V31() set
INT is non empty non trivial V31() set
9 is non empty ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT
Segm 9 is countable Element of bool omega
SCM-Data-Loc is non empty set
K80(NAT,1) is non empty trivial V31() V35() 1 -element countable Element of bool NAT
[:K80(NAT,1),NAT:] is non trivial Relation-like NAT -defined REAL -valued V31() Element of bool [:NAT,REAL:]
[:NAT,REAL:] is non trivial V31() set
bool [:NAT,REAL:] is non trivial V31() set
[:1,1:] is V31() countable set
bool [:1,1:] is V31() V35() countable set
[:[:1,1:],1:] is V31() countable set
bool [:[:1,1:],1:] is V31() V35() countable set
2 is non empty ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT
3 is non empty ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT
0 is empty Function-like functional ordinal natural V31() V35() cardinal {} -element countable V86() integer V111() ext-real non positive non negative Element of NAT
{NAT} is non empty trivial V31() 1 -element countable set
{NAT} \/ SCM-Data-Loc is non empty set
() is set
bool () is set
() is non empty Element of bool ()
x is Element of ()
x is set
y is set
[x,y] is V1() set
{x,y} is non empty V31() countable set
{x} is non empty trivial V31() 1 -element countable set
{{x,y},{x}} is non empty V31() V35() countable set
[:(),2:] is set
bool [:(),2:] is set
{0} is non empty trivial V31() V35() 1 -element countable set
{1} is non empty trivial V31() V35() 1 -element countable set
{0} \/ {1} is non empty V31() V35() countable set
{0,1} is non empty V31() V35() countable set
{1} \/ {0} is non empty V31() V35() countable set
x is Element of ()
x is non empty Relation-like () -defined 2 -valued Function-like V17(()) V18((),2) Element of bool [:(),2:]
y is Element of ()
x . y is ordinal Element of 2
x is non empty Relation-like () -defined 2 -valued Function-like V17(()) V18((),2) Element of bool [:(),2:]
y is non empty Relation-like () -defined 2 -valued Function-like V17(()) V18((),2) Element of bool [:(),2:]
z is Element of ()
x . z is ordinal Element of 2
y . z is ordinal Element of 2
z is Element of ()
x . z is ordinal Element of 2
y . z is ordinal Element of 2
z is Element of ()
x . z is ordinal Element of 2
y . z is ordinal Element of 2
z is Element of ()
x . z is ordinal Element of 2
y . z is ordinal Element of 2
() is non empty Relation-like () -defined 2 -valued Function-like V17(()) V18((),2) Element of bool [:(),2:]
<%NAT,INT%> is Relation-like NAT -defined Function-like T-Sequence-like V31() 2 -element countable V109() set
() is Relation-like 2 -defined Function-like V17(2) set
() * () is Relation-like Function-like set
(() * ()) . NAT is set
proj1 () is set
() . NAT is set
() . (() . NAT) is set
() . 0 is set
x is Element of ()
(() * ()) . x is set
proj1 () is set
() . x is ordinal Element of 2
() . (() . x) is set
() . 1 is set
proj1 () is set
len <%NAT,INT%> is ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT
proj1 <%NAT,INT%> is ordinal natural V31() cardinal 2 -element countable V86() integer V111() ext-real set
proj2 () is set
proj1 () is set
proj1 (() * ()) is set
y is set
(() * ()) . y is set
x is Element of ()
(() * ()) . x is set
product (() * ()) is non empty functional with_common_domain product-like set
pi ((product (() * ())),NAT) is set
x is Element of ()
pi ((product (() * ())),x) is set
(() * ()) . x is set
x is Relation-like Function-like () * () -compatible Element of product (() * ())
x . NAT is set
x is Relation-like Function-like () * () -compatible Element of product (() * ())
y is ordinal natural V31() cardinal countable V86() integer V111() ext-real set
NAT .--> y is Relation-like {NAT} -defined Function-like one-to-one V31() Cardinal-yielding countable set
{NAT} --> y is non empty Relation-like {NAT} -defined {y} -valued Function-like constant V17({NAT}) V18({NAT},{y}) V31() Cardinal-yielding countable V102() Element of bool [:{NAT},{y}:]
{y} is non empty trivial V31() V35() 1 -element countable set
[:{NAT},{y}:] is V31() countable set
bool [:{NAT},{y}:] is V31() V35() countable set
x +* (NAT .--> y) is Relation-like Function-like set
z is set
proj1 (NAT .--> y) is V31() countable set
(x +* (NAT .--> y)) . NAT is set
(NAT .--> y) . NAT is set
(x +* (NAT .--> y)) . z is set
(() * ()) . z is set
proj1 (NAT .--> y) is V31() countable set
(x +* (NAT .--> y)) . z is set
x . z is set
(() * ()) . z is set
proj1 x is set
proj1 (x +* (NAT .--> y)) is set
proj1 (NAT .--> y) is V31() countable set
() \/ (proj1 (NAT .--> y)) is non empty set
() \/ {NAT} is non empty set
x is Relation-like Function-like () * () -compatible Element of product (() * ())
y is ordinal natural V31() cardinal countable V86() integer V111() ext-real set
(x,y) is Relation-like Function-like () * () -compatible Element of product (() * ())
NAT .--> y is Relation-like {NAT} -defined Function-like one-to-one V31() Cardinal-yielding countable set
{NAT} --> y is non empty Relation-like {NAT} -defined {y} -valued Function-like constant V17({NAT}) V18({NAT},{y}) V31() Cardinal-yielding countable V102() Element of bool [:{NAT},{y}:]
{y} is non empty trivial V31() V35() 1 -element countable set
[:{NAT},{y}:] is V31() countable set
bool [:{NAT},{y}:] is V31() V35() countable set
x +* (NAT .--> y) is Relation-like Function-like set
(x,y) . NAT is set
proj1 (NAT .--> y) is V31() countable set
(NAT .--> y) . NAT is set
x is Relation-like Function-like () * () -compatible Element of product (() * ())
y is ordinal natural V31() cardinal countable V86() integer V111() ext-real set
(x,y) is Relation-like Function-like () * () -compatible Element of product (() * ())
NAT .--> y is Relation-like {NAT} -defined Function-like one-to-one V31() Cardinal-yielding countable set
{NAT} --> y is non empty Relation-like {NAT} -defined {y} -valued Function-like constant V17({NAT}) V18({NAT},{y}) V31() Cardinal-yielding countable V102() Element of bool [:{NAT},{y}:]
{y} is non empty trivial V31() V35() 1 -element countable set
[:{NAT},{y}:] is V31() countable set
bool [:{NAT},{y}:] is V31() V35() countable set
x +* (NAT .--> y) is Relation-like Function-like set
z is Element of ()
(x,y) . z is set
x . z is set
proj1 (NAT .--> y) is V31() countable set
(() * ()) . z is set
x is Relation-like Function-like () * () -compatible Element of product (() * ())
y is ordinal natural V31() cardinal countable V86() integer V111() ext-real set
(x,y) is Relation-like Function-like () * () -compatible Element of product (() * ())
NAT .--> y is Relation-like {NAT} -defined Function-like one-to-one V31() Cardinal-yielding countable set
{NAT} --> y is non empty Relation-like {NAT} -defined {y} -valued Function-like constant V17({NAT}) V18({NAT},{y}) V31() Cardinal-yielding countable V102() Element of bool [:{NAT},{y}:]
{y} is non empty trivial V31() V35() 1 -element countable set
[:{NAT},{y}:] is V31() countable set
bool [:{NAT},{y}:] is V31() V35() countable set
x +* (NAT .--> y) is Relation-like Function-like set
z is ordinal natural V31() cardinal countable V86() integer V111() ext-real set
(x,y) . z is set
x . z is set
proj1 (NAT .--> y) is V31() countable set
x is Relation-like Function-like () * () -compatible Element of product (() * ())
y is Element of ()
z is V86() integer V111() ext-real set
y .--> z is Relation-like () -defined {y} -defined Function-like one-to-one V31() countable set
{y} is non empty trivial V31() 1 -element countable set
{y} --> z is non empty Relation-like {y} -defined {z} -valued Function-like constant V17({y}) V18({y},{z}) V31() countable Element of bool [:{y},{z}:]
{z} is non empty trivial V31() 1 -element countable set
[:{y},{z}:] is V31() countable set
bool [:{y},{z}:] is V31() V35() countable set
x +* (y .--> z) is Relation-like Function-like set
k is set
proj1 (y .--> z) is V31() countable set
(x +* (y .--> z)) . y is set
(y .--> z) . y is set
(x +* (y .--> z)) . k is set
(() * ()) . k is set
proj1 (y .--> z) is V31() countable set
(x +* (y .--> z)) . k is set
x . k is set
(() * ()) . k is set
proj1 x is set
proj1 (x +* (y .--> z)) is set
proj1 (y .--> z) is V31() countable set
() \/ (proj1 (y .--> z)) is non empty set
() \/ {y} is non empty set
x is Relation-like Function-like () * () -compatible Element of product (() * ())
x . NAT is set
y is Element of ()
z is V86() integer V111() ext-real set
(x,y,z) is Relation-like Function-like () * () -compatible Element of product (() * ())
y .--> z is Relation-like () -defined {y} -defined Function-like one-to-one V31() countable set
{y} is non empty trivial V31() 1 -element countable set
{y} --> z is non empty Relation-like {y} -defined {z} -valued Function-like constant V17({y}) V18({y},{z}) V31() countable Element of bool [:{y},{z}:]
{z} is non empty trivial V31() 1 -element countable set
[:{y},{z}:] is V31() countable set
bool [:{y},{z}:] is V31() V35() countable set
x +* (y .--> z) is Relation-like Function-like set
(x,y,z) . NAT is set
proj1 (y .--> z) is V31() countable set
(() * ()) . y is set
x is Relation-like Function-like () * () -compatible Element of product (() * ())
y is Element of ()
z is V86() integer V111() ext-real set
(x,y,z) is Relation-like Function-like () * () -compatible Element of product (() * ())
y .--> z is Relation-like () -defined {y} -defined Function-like one-to-one V31() countable set
{y} is non empty trivial V31() 1 -element countable set
{y} --> z is non empty Relation-like {y} -defined {z} -valued Function-like constant V17({y}) V18({y},{z}) V31() countable Element of bool [:{y},{z}:]
{z} is non empty trivial V31() 1 -element countable set
[:{y},{z}:] is V31() countable set
bool [:{y},{z}:] is V31() V35() countable set
x +* (y .--> z) is Relation-like Function-like set
(x,y,z) . y is set
proj1 (y .--> z) is V31() countable set
(y .--> z) . y is set
x is Relation-like Function-like () * () -compatible Element of product (() * ())
y is Element of ()
z is V86() integer V111() ext-real set
(x,y,z) is Relation-like Function-like () * () -compatible Element of product (() * ())
y .--> z is Relation-like () -defined {y} -defined Function-like one-to-one V31() countable set
{y} is non empty trivial V31() 1 -element countable set
{y} --> z is non empty Relation-like {y} -defined {z} -valued Function-like constant V17({y}) V18({y},{z}) V31() countable Element of bool [:{y},{z}:]
{z} is non empty trivial V31() 1 -element countable set
[:{y},{z}:] is V31() countable set
bool [:{y},{z}:] is V31() V35() countable set
x +* (y .--> z) is Relation-like Function-like set
k is Element of ()
(x,y,z) . k is set
x . k is set
proj1 (y .--> z) is V31() countable set
x is Relation-like Function-like () * () -compatible Element of product (() * ())
y is Element of ()
x . y is set
pi ((product (() * ())),y) is set
SCM-Instr is non empty set
x is Element of SCM-Instr
y is Relation-like Function-like () * () -compatible Element of product (() * ())
x address_1 is Element of SCM-Data-Loc
x address_2 is Element of SCM-Data-Loc
y . (x address_2) is V86() integer V111() ext-real set
(y,(x address_1),(y . (x address_2))) is Relation-like Function-like () * () -compatible Element of product (() * ())
(x address_1) .--> (y . (x address_2)) is Relation-like SCM-Data-Loc -defined {(x address_1)} -defined Function-like one-to-one V31() countable set
{(x address_1)} is non empty trivial V31() 1 -element countable set
{(x address_1)} --> (y . (x address_2)) is non empty Relation-like {(x address_1)} -defined {(y . (x address_2))} -valued Function-like constant V17({(x address_1)}) V18({(x address_1)},{(y . (x address_2))}) V31() countable Element of bool [:{(x address_1)},{(y . (x address_2))}:]
{(y . (x address_2))} is non empty trivial V31() 1 -element countable set
[:{(x address_1)},{(y . (x address_2))}:] is V31() countable set
bool [:{(x address_1)},{(y . (x address_2))}:] is V31() V35() countable set
y +* ((x address_1) .--> (y . (x address_2))) is Relation-like Function-like set
(y) is ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT
y . NAT is set
succ (y) is ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of omega
((y,(x address_1),(y . (x address_2))),(succ (y))) is Relation-like Function-like () * () -compatible Element of product (() * ())
NAT .--> (succ (y)) is Relation-like {NAT} -defined Function-like one-to-one V31() Cardinal-yielding countable set
{NAT} --> (succ (y)) is non empty Relation-like {NAT} -defined {(succ (y))} -valued Function-like constant V17({NAT}) V18({NAT},{(succ (y))}) V31() Cardinal-yielding countable V102() Element of bool [:{NAT},{(succ (y))}:]
{(succ (y))} is non empty trivial V31() V35() 1 -element countable set
[:{NAT},{(succ (y))}:] is V31() countable set
bool [:{NAT},{(succ (y))}:] is V31() V35() countable set
(y,(x address_1),(y . (x address_2))) +* (NAT .--> (succ (y))) is Relation-like Function-like set
y . (x address_1) is V86() integer V111() ext-real set
(y . (x address_1)) + (y . (x address_2)) is V86() integer V111() ext-real set
(y,(x address_1),((y . (x address_1)) + (y . (x address_2)))) is Relation-like Function-like () * () -compatible Element of product (() * ())
(x address_1) .--> ((y . (x address_1)) + (y . (x address_2))) is Relation-like SCM-Data-Loc -defined {(x address_1)} -defined Function-like one-to-one V31() countable set
{(x address_1)} --> ((y . (x address_1)) + (y . (x address_2))) is non empty Relation-like {(x address_1)} -defined {((y . (x address_1)) + (y . (x address_2)))} -valued Function-like constant V17({(x address_1)}) V18({(x address_1)},{((y . (x address_1)) + (y . (x address_2)))}) V31() countable Element of bool [:{(x address_1)},{((y . (x address_1)) + (y . (x address_2)))}:]
{((y . (x address_1)) + (y . (x address_2)))} is non empty trivial V31() 1 -element countable set
[:{(x address_1)},{((y . (x address_1)) + (y . (x address_2)))}:] is V31() countable set
bool [:{(x address_1)},{((y . (x address_1)) + (y . (x address_2)))}:] is V31() V35() countable set
y +* ((x address_1) .--> ((y . (x address_1)) + (y . (x address_2)))) is Relation-like Function-like set
((y,(x address_1),((y . (x address_1)) + (y . (x address_2)))),(succ (y))) is Relation-like Function-like () * () -compatible Element of product (() * ())
(y,(x address_1),((y . (x address_1)) + (y . (x address_2)))) +* (NAT .--> (succ (y))) is Relation-like Function-like set
(y . (x address_1)) - (y . (x address_2)) is V86() integer V111() ext-real set
(y,(x address_1),((y . (x address_1)) - (y . (x address_2)))) is Relation-like Function-like () * () -compatible Element of product (() * ())
(x address_1) .--> ((y . (x address_1)) - (y . (x address_2))) is Relation-like SCM-Data-Loc -defined {(x address_1)} -defined Function-like one-to-one V31() countable set
{(x address_1)} --> ((y . (x address_1)) - (y . (x address_2))) is non empty Relation-like {(x address_1)} -defined {((y . (x address_1)) - (y . (x address_2)))} -valued Function-like constant V17({(x address_1)}) V18({(x address_1)},{((y . (x address_1)) - (y . (x address_2)))}) V31() countable Element of bool [:{(x address_1)},{((y . (x address_1)) - (y . (x address_2)))}:]
{((y . (x address_1)) - (y . (x address_2)))} is non empty trivial V31() 1 -element countable set
[:{(x address_1)},{((y . (x address_1)) - (y . (x address_2)))}:] is V31() countable set
bool [:{(x address_1)},{((y . (x address_1)) - (y . (x address_2)))}:] is V31() V35() countable set
y +* ((x address_1) .--> ((y . (x address_1)) - (y . (x address_2)))) is Relation-like Function-like set
((y,(x address_1),((y . (x address_1)) - (y . (x address_2)))),(succ (y))) is Relation-like Function-like () * () -compatible Element of product (() * ())
(y,(x address_1),((y . (x address_1)) - (y . (x address_2)))) +* (NAT .--> (succ (y))) is Relation-like Function-like set
4 is non empty ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT
(y . (x address_1)) * (y . (x address_2)) is V86() integer V111() ext-real set
(y,(x address_1),((y . (x address_1)) * (y . (x address_2)))) is Relation-like Function-like () * () -compatible Element of product (() * ())
(x address_1) .--> ((y . (x address_1)) * (y . (x address_2))) is Relation-like SCM-Data-Loc -defined {(x address_1)} -defined Function-like one-to-one V31() countable set
{(x address_1)} --> ((y . (x address_1)) * (y . (x address_2))) is non empty Relation-like {(x address_1)} -defined {((y . (x address_1)) * (y . (x address_2)))} -valued Function-like constant V17({(x address_1)}) V18({(x address_1)},{((y . (x address_1)) * (y . (x address_2)))}) V31() countable Element of bool [:{(x address_1)},{((y . (x address_1)) * (y . (x address_2)))}:]
{((y . (x address_1)) * (y . (x address_2)))} is non empty trivial V31() 1 -element countable set
[:{(x address_1)},{((y . (x address_1)) * (y . (x address_2)))}:] is V31() countable set
bool [:{(x address_1)},{((y . (x address_1)) * (y . (x address_2)))}:] is V31() V35() countable set
y +* ((x address_1) .--> ((y . (x address_1)) * (y . (x address_2)))) is Relation-like Function-like set
((y,(x address_1),((y . (x address_1)) * (y . (x address_2)))),(succ (y))) is Relation-like Function-like () * () -compatible Element of product (() * ())
(y,(x address_1),((y . (x address_1)) * (y . (x address_2)))) +* (NAT .--> (succ (y))) is Relation-like Function-like set
5 is non empty ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT
(y . (x address_1)) div (y . (x address_2)) is V86() integer V111() ext-real set
(y,(x address_1),((y . (x address_1)) div (y . (x address_2)))) is Relation-like Function-like () * () -compatible Element of product (() * ())
(x address_1) .--> ((y . (x address_1)) div (y . (x address_2))) is Relation-like SCM-Data-Loc -defined {(x address_1)} -defined Function-like one-to-one V31() countable set
{(x address_1)} --> ((y . (x address_1)) div (y . (x address_2))) is non empty Relation-like {(x address_1)} -defined {((y . (x address_1)) div (y . (x address_2)))} -valued Function-like constant V17({(x address_1)}) V18({(x address_1)},{((y . (x address_1)) div (y . (x address_2)))}) V31() countable Element of bool [:{(x address_1)},{((y . (x address_1)) div (y . (x address_2)))}:]
{((y . (x address_1)) div (y . (x address_2)))} is non empty trivial V31() 1 -element countable set
[:{(x address_1)},{((y . (x address_1)) div (y . (x address_2)))}:] is V31() countable set
bool [:{(x address_1)},{((y . (x address_1)) div (y . (x address_2)))}:] is V31() V35() countable set
y +* ((x address_1) .--> ((y . (x address_1)) div (y . (x address_2)))) is Relation-like Function-like set
(y . (x address_1)) mod (y . (x address_2)) is V86() integer V111() ext-real set
((y,(x address_1),((y . (x address_1)) div (y . (x address_2)))),(x address_2),((y . (x address_1)) mod (y . (x address_2)))) is Relation-like Function-like () * () -compatible Element of product (() * ())
(x address_2) .--> ((y . (x address_1)) mod (y . (x address_2))) is Relation-like SCM-Data-Loc -defined {(x address_2)} -defined Function-like one-to-one V31() countable set
{(x address_2)} is non empty trivial V31() 1 -element countable set
{(x address_2)} --> ((y . (x address_1)) mod (y . (x address_2))) is non empty Relation-like {(x address_2)} -defined {((y . (x address_1)) mod (y . (x address_2)))} -valued Function-like constant V17({(x address_2)}) V18({(x address_2)},{((y . (x address_1)) mod (y . (x address_2)))}) V31() countable Element of bool [:{(x address_2)},{((y . (x address_1)) mod (y . (x address_2)))}:]
{((y . (x address_1)) mod (y . (x address_2)))} is non empty trivial V31() 1 -element countable set
[:{(x address_2)},{((y . (x address_1)) mod (y . (x address_2)))}:] is V31() countable set
bool [:{(x address_2)},{((y . (x address_1)) mod (y . (x address_2)))}:] is V31() V35() countable set
(y,(x address_1),((y . (x address_1)) div (y . (x address_2)))) +* ((x address_2) .--> ((y . (x address_1)) mod (y . (x address_2)))) is Relation-like Function-like set
(((y,(x address_1),((y . (x address_1)) div (y . (x address_2)))),(x address_2),((y . (x address_1)) mod (y . (x address_2)))),(succ (y))) is Relation-like Function-like () * () -compatible Element of product (() * ())
((y,(x address_1),((y . (x address_1)) div (y . (x address_2)))),(x address_2),((y . (x address_1)) mod (y . (x address_2)))) +* (NAT .--> (succ (y))) is Relation-like Function-like set
6 is non empty ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT
x jump_address is ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT
(y,(x jump_address)) is Relation-like Function-like () * () -compatible Element of product (() * ())
NAT .--> (x jump_address) is Relation-like {NAT} -defined Function-like one-to-one V31() Cardinal-yielding countable set
{NAT} --> (x jump_address) is non empty Relation-like {NAT} -defined {(x jump_address)} -valued Function-like constant V17({NAT}) V18({NAT},{(x jump_address)}) V31() Cardinal-yielding countable V102() Element of bool [:{NAT},{(x jump_address)}:]
{(x jump_address)} is non empty trivial V31() V35() 1 -element countable set
[:{NAT},{(x jump_address)}:] is V31() countable set
bool [:{NAT},{(x jump_address)}:] is V31() V35() countable set
y +* (NAT .--> (x jump_address)) is Relation-like Function-like set
7 is non empty ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT
x cond_address is Element of SCM-Data-Loc
y . (x cond_address) is V86() integer V111() ext-real set
x cjump_address is ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT
IFEQ ((y . (x cond_address)),0,(x cjump_address),(succ (y))) is ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of omega
(y,(IFEQ ((y . (x cond_address)),0,(x cjump_address),(succ (y))))) is Relation-like Function-like () * () -compatible Element of product (() * ())
NAT .--> (IFEQ ((y . (x cond_address)),0,(x cjump_address),(succ (y)))) is Relation-like {NAT} -defined Function-like one-to-one V31() Cardinal-yielding countable set
{NAT} --> (IFEQ ((y . (x cond_address)),0,(x cjump_address),(succ (y)))) is non empty Relation-like {NAT} -defined {(IFEQ ((y . (x cond_address)),0,(x cjump_address),(succ (y))))} -valued Function-like constant V17({NAT}) V18({NAT},{(IFEQ ((y . (x cond_address)),0,(x cjump_address),(succ (y))))}) V31() Cardinal-yielding countable V102() Element of bool [:{NAT},{(IFEQ ((y . (x cond_address)),0,(x cjump_address),(succ (y))))}:]
{(IFEQ ((y . (x cond_address)),0,(x cjump_address),(succ (y))))} is non empty trivial V31() V35() 1 -element countable set
[:{NAT},{(IFEQ ((y . (x cond_address)),0,(x cjump_address),(succ (y))))}:] is V31() countable set
bool [:{NAT},{(IFEQ ((y . (x cond_address)),0,(x cjump_address),(succ (y))))}:] is V31() V35() countable set
y +* (NAT .--> (IFEQ ((y . (x cond_address)),0,(x cjump_address),(succ (y))))) is Relation-like Function-like set
8 is non empty ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT
IFGT ((y . (x cond_address)),0,(x cjump_address),(succ (y))) is ordinal natural V31() cardinal countable V86() integer V111() ext-real set
(y,(IFGT ((y . (x cond_address)),0,(x cjump_address),(succ (y))))) is Relation-like Function-like () * () -compatible Element of product (() * ())
NAT .--> (IFGT ((y . (x cond_address)),0,(x cjump_address),(succ (y)))) is Relation-like {NAT} -defined Function-like one-to-one V31() Cardinal-yielding countable set
{NAT} --> (IFGT ((y . (x cond_address)),0,(x cjump_address),(succ (y)))) is non empty Relation-like {NAT} -defined {(IFGT ((y . (x cond_address)),0,(x cjump_address),(succ (y))))} -valued Function-like constant V17({NAT}) V18({NAT},{(IFGT ((y . (x cond_address)),0,(x cjump_address),(succ (y))))}) V31() Cardinal-yielding countable V102() Element of bool [:{NAT},{(IFGT ((y . (x cond_address)),0,(x cjump_address),(succ (y))))}:]
{(IFGT ((y . (x cond_address)),0,(x cjump_address),(succ (y))))} is non empty trivial V31() V35() 1 -element countable set
[:{NAT},{(IFGT ((y . (x cond_address)),0,(x cjump_address),(succ (y))))}:] is V31() countable set
bool [:{NAT},{(IFGT ((y . (x cond_address)),0,(x cjump_address),(succ (y))))}:] is V31() V35() countable set
y +* (NAT .--> (IFGT ((y . (x cond_address)),0,(x cjump_address),(succ (y))))) is Relation-like Function-like set
k is Element of ()
c₅ is Element of ()
<*k,c₅*> is set
[1,{},<*k,c₅*>] is V1() V2() set
[1,{}] is V1() set
{1,{}} is non empty V31() V35() countable set
{1} is non empty trivial V31() V35() 1 -element countable set
{{1,{}},{1}} is non empty V31() V35() countable set
[[1,{}],<*k,c₅*>] is V1() set
{[1,{}],<*k,c₅*>} is non empty V31() countable set
{[1,{}]} is non empty trivial Function-like V31() 1 -element countable set
{{[1,{}],<*k,c₅*>},{[1,{}]}} is non empty V31() V35() countable set
y is Element of ()
c₇ is Element of ()
<*y,c₇*> is set
[2,{},<*y,c₇*>] is V1() V2() set
[2,{}] is V1() set
{2,{}} is non empty V31() V35() countable set
{2} is non empty trivial V31() V35() 1 -element countable set
{{2,{}},{2}} is non empty V31() V35() countable set
[[2,{}],<*y,c₇*>] is V1() set
{[2,{}],<*y,c₇*>} is non empty V31() countable set
{[2,{}]} is non empty trivial Function-like V31() 1 -element countable set
{{[2,{}],<*y,c₇*>},{[2,{}]}} is non empty V31() V35() countable set
z is Relation-like Function-like () * () -compatible Element of product (() * ())
c₉ is Element of ()
c₁₀ is Element of ()
<*c₉,c₁₀*> is set
[1,{},<*c₉,c₁₀*>] is V1() V2() set
[[1,{}],<*c₉,c₁₀*>] is V1() set
{[1,{}],<*c₉,c₁₀*>} is non empty V31() countable set
{{[1,{}],<*c₉,c₁₀*>},{[1,{}]}} is non empty V31() V35() countable set
c₁₁ is Element of ()
c₁₂ is Element of ()
<*c₁₁,c₁₂*> is set
[3,{},<*c₁₁,c₁₂*>] is V1() V2() set
[3,{}] is V1() set
{3,{}} is non empty V31() V35() countable set
{3} is non empty trivial V31() V35() 1 -element countable set
{{3,{}},{3}} is non empty V31() V35() countable set
[[3,{}],<*c₁₁,c₁₂*>] is V1() set
{[3,{}],<*c₁₁,c₁₂*>} is non empty V31() countable set
{[3,{}]} is non empty trivial Function-like V31() 1 -element countable set
{{[3,{}],<*c₁₁,c₁₂*>},{[3,{}]}} is non empty V31() V35() countable set
c₈ is Relation-like Function-like () * () -compatible Element of product (() * ())
c₁₄ is Element of ()
c₁₅ is Element of ()
<*c₁₄,c₁₅*> is set
[1,{},<*c₁₄,c₁₅*>] is V1() V2() set
[[1,{}],<*c₁₄,c₁₅*>] is V1() set
{[1,{}],<*c₁₄,c₁₅*>} is non empty V31() countable set
{{[1,{}],<*c₁₄,c₁₅*>},{[1,{}]}} is non empty V31() V35() countable set
c₁₆ is Element of ()
c₁₇ is Element of ()
<*c₁₆,c₁₇*> is set
[4,{},<*c₁₆,c₁₇*>] is V1() V2() set
[4,{}] is V1() set
{4,{}} is non empty V31() V35() countable set
{4} is non empty trivial V31() V35() 1 -element countable set
{{4,{}},{4}} is non empty V31() V35() countable set
[[4,{}],<*c₁₆,c₁₇*>] is V1() set
{[4,{}],<*c₁₆,c₁₇*>} is non empty V31() countable set
{[4,{}]} is non empty trivial Function-like V31() 1 -element countable set
{{[4,{}],<*c₁₆,c₁₇*>},{[4,{}]}} is non empty V31() V35() countable set
c₁₃ is Relation-like Function-like () * () -compatible Element of product (() * ())
c₁₉ is Element of ()
c₂₀ is Element of ()
<*c₁₉,c₂₀*> is set
[1,{},<*c₁₉,c₂₀*>] is V1() V2() set
[[1,{}],<*c₁₉,c₂₀*>] is V1() set
{[1,{}],<*c₁₉,c₂₀*>} is non empty V31() countable set
{{[1,{}],<*c₁₉,c₂₀*>},{[1,{}]}} is non empty V31() V35() countable set
c₂₁ is Element of ()
c₂₂ is Element of ()
<*c₂₁,c₂₂*> is set
[5,{},<*c₂₁,c₂₂*>] is V1() V2() set
[5,{}] is V1() set
{5,{}} is non empty V31() V35() countable set
{5} is non empty trivial V31() V35() 1 -element countable set
{{5,{}},{5}} is non empty V31() V35() countable set
[[5,{}],<*c₂₁,c₂₂*>] is V1() set
{[5,{}],<*c₂₁,c₂₂*>} is non empty V31() countable set
{[5,{}]} is non empty trivial Function-like V31() 1 -element countable set
{{[5,{}],<*c₂₁,c₂₂*>},{[5,{}]}} is non empty V31() V35() countable set
c₁₈ is Relation-like Function-like () * () -compatible Element of product (() * ())
c₂₄ is Element of ()
c₂₅ is Element of ()
<*c₂₄,c₂₅*> is set
[1,{},<*c₂₄,c₂₅*>] is V1() V2() set
[[1,{}],<*c₂₄,c₂₅*>] is V1() set
{[1,{}],<*c₂₄,c₂₅*>} is non empty V31() countable set
{{[1,{}],<*c₂₄,c₂₅*>},{[1,{}]}} is non empty V31() V35() countable set
c₂₆ is ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT
<*c₂₆*> is Relation-like Function-like set
[6,<*c₂₆*>,{}] is V1() V2() set
[6,<*c₂₆*>] is V1() set
{6,<*c₂₆*>} is non empty V31() countable set
{6} is non empty trivial V31() V35() 1 -element countable set
{{6,<*c₂₆*>},{6}} is non empty V31() V35() countable set
[[6,<*c₂₆*>],{}] is V1() set
{[6,<*c₂₆*>],{}} is non empty V31() countable set
{[6,<*c₂₆*>]} is non empty trivial Function-like V31() 1 -element countable set
{{[6,<*c₂₆*>],{}},{[6,<*c₂₆*>]}} is non empty V31() V35() countable set
c₂₃ is Relation-like Function-like () * () -compatible Element of product (() * ())
c₂₈ is Element of ()
c₂₉ is Element of ()
<*c₂₈,c₂₉*> is set
[1,{},<*c₂₈,c₂₉*>] is V1() V2() set
[[1,{}],<*c₂₈,c₂₉*>] is V1() set
{[1,{}],<*c₂₈,c₂₉*>} is non empty V31() countable set
{{[1,{}],<*c₂₈,c₂₉*>},{[1,{}]}} is non empty V31() V35() countable set
c₃₀ is ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT
<*c₃₀*> is Relation-like Function-like set
c₃₁ is Element of ()
<*c₃₁*> is Relation-like NAT -defined () -valued Function-like FinSequence-like FinSequence of ()
[7,<*c₃₀*>,<*c₃₁*>] is V1() V2() set
[7,<*c₃₀*>] is V1() set
{7,<*c₃₀*>} is non empty V31() countable set
{7} is non empty trivial V31() V35() 1 -element countable set
{{7,<*c₃₀*>},{7}} is non empty V31() V35() countable set
[[7,<*c₃₀*>],<*c₃₁*>] is V1() set
{[7,<*c₃₀*>],<*c₃₁*>} is non empty V31() countable set
{[7,<*c₃₀*>]} is non empty trivial Function-like V31() 1 -element countable set
{{[7,<*c₃₀*>],<*c₃₁*>},{[7,<*c₃₀*>]}} is non empty V31() V35() countable set
c₂₇ is Relation-like Function-like () * () -compatible Element of product (() * ())
c₃₃ is Element of ()
c₃₄ is Element of ()
<*c₃₃,c₃₄*> is set
[1,{},<*c₃₃,c₃₄*>] is V1() V2() set
[[1,{}],<*c₃₃,c₃₄*>] is V1() set
{[1,{}],<*c₃₃,c₃₄*>} is non empty V31() countable set
{{[1,{}],<*c₃₃,c₃₄*>},{[1,{}]}} is non empty V31() V35() countable set
c₃₅ is ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT
<*c₃₅*> is Relation-like Function-like set
c₃₆ is Element of ()
<*c₃₆*> is Relation-like NAT -defined () -valued Function-like FinSequence-like FinSequence of ()
[8,<*c₃₅*>,<*c₃₆*>] is V1() V2() set
[8,<*c₃₅*>] is V1() set
{8,<*c₃₅*>} is non empty V31() countable set
{8} is non empty trivial V31() V35() 1 -element countable set
{{8,<*c₃₅*>},{8}} is non empty V31() V35() countable set
[[8,<*c₃₅*>],<*c₃₆*>] is V1() set
{[8,<*c₃₅*>],<*c₃₆*>} is non empty V31() countable set
{[8,<*c₃₅*>]} is non empty trivial Function-like V31() 1 -element countable set
{{[8,<*c₃₅*>],<*c₃₆*>},{[8,<*c₃₅*>]}} is non empty V31() V35() countable set
c₃₂ is Relation-like Function-like () * () -compatible Element of product (() * ())
c₃₈ is Element of ()
c₃₉ is Element of ()
<*c₃₈,c₃₉*> is set
[2,{},<*c₃₈,c₃₉*>] is V1() V2() set
[[2,{}],<*c₃₈,c₃₉*>] is V1() set
{[2,{}],<*c₃₈,c₃₉*>} is non empty V31() countable set
{{[2,{}],<*c₃₈,c₃₉*>},{[2,{}]}} is non empty V31() V35() countable set
c₄₀ is Element of ()
c₄₁ is Element of ()
<*c₄₀,c₄₁*> is set
[3,{},<*c₄₀,c₄₁*>] is V1() V2() set
[[3,{}],<*c₄₀,c₄₁*>] is V1() set
{[3,{}],<*c₄₀,c₄₁*>} is non empty V31() countable set
{{[3,{}],<*c₄₀,c₄₁*>},{[3,{}]}} is non empty V31() V35() countable set
c₃₇ is Relation-like Function-like () * () -compatible Element of product (() * ())
c₄₃ is Element of ()
c₄₄ is Element of ()
<*c₄₃,c₄₄*> is set
[2,{},<*c₄₃,c₄₄*>] is V1() V2() set
[[2,{}],<*c₄₃,c₄₄*>] is V1() set
{[2,{}],<*c₄₃,c₄₄*>} is non empty V31() countable set
{{[2,{}],<*c₄₃,c₄₄*>},{[2,{}]}} is non empty V31() V35() countable set
c₄₅ is Element of ()
c₄₆ is Element of ()
<*c₄₅,c₄₆*> is set
[4,{},<*c₄₅,c₄₆*>] is V1() V2() set
[[4,{}],<*c₄₅,c₄₆*>] is V1() set
{[4,{}],<*c₄₅,c₄₆*>} is non empty V31() countable set
{{[4,{}],<*c₄₅,c₄₆*>},{[4,{}]}} is non empty V31() V35() countable set
c₄₂ is Relation-like Function-like () * () -compatible Element of product (() * ())
c₄₈ is Element of ()
c₄₉ is Element of ()
<*c₄₈,c₄₉*> is set
[2,{},<*c₄₈,c₄₉*>] is V1() V2() set
[[2,{}],<*c₄₈,c₄₉*>] is V1() set
{[2,{}],<*c₄₈,c₄₉*>} is non empty V31() countable set
{{[2,{}],<*c₄₈,c₄₉*>},{[2,{}]}} is non empty V31() V35() countable set
c₅₀ is Element of ()
c₅₁ is Element of ()
<*c₅₀,c₅₁*> is set
[5,{},<*c₅₀,c₅₁*>] is V1() V2() set
[[5,{}],<*c₅₀,c₅₁*>] is V1() set
{[5,{}],<*c₅₀,c₅₁*>} is non empty V31() countable set
{{[5,{}],<*c₅₀,c₅₁*>},{[5,{}]}} is non empty V31() V35() countable set
c₄₇ is Relation-like Function-like () * () -compatible Element of product (() * ())
c₅₃ is Element of ()
c₅₄ is Element of ()
<*c₅₃,c₅₄*> is set
[2,{},<*c₅₃,c₅₄*>] is V1() V2() set
[[2,{}],<*c₅₃,c₅₄*>] is V1() set
{[2,{}],<*c₅₃,c₅₄*>} is non empty V31() countable set
{{[2,{}],<*c₅₃,c₅₄*>},{[2,{}]}} is non empty V31() V35() countable set
c₅₅ is ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT
<*c₅₅*> is Relation-like Function-like set
[6,<*c₅₅*>,{}] is V1() V2() set
[6,<*c₅₅*>] is V1() set
{6,<*c₅₅*>} is non empty V31() countable set
{{6,<*c₅₅*>},{6}} is non empty V31() V35() countable set
[[6,<*c₅₅*>],{}] is V1() set
{[6,<*c₅₅*>],{}} is non empty V31() countable set
{[6,<*c₅₅*>]} is non empty trivial Function-like V31() 1 -element countable set
{{[6,<*c₅₅*>],{}},{[6,<*c₅₅*>]}} is non empty V31() V35() countable set
c₅₂ is Relation-like Function-like () * () -compatible Element of product (() * ())
c₅₇ is Element of ()
c₅₈ is Element of ()
<*c₅₇,c₅₈*> is set
[2,{},<*c₅₇,c₅₈*>] is V1() V2() set
[[2,{}],<*c₅₇,c₅₈*>] is V1() set
{[2,{}],<*c₅₇,c₅₈*>} is non empty V31() countable set
{{[2,{}],<*c₅₇,c₅₈*>},{[2,{}]}} is non empty V31() V35() countable set
c₅₉ is ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT
<*c₅₉*> is Relation-like Function-like set
c₆₀ is Element of ()
<*c₆₀*> is Relation-like NAT -defined () -valued Function-like FinSequence-like FinSequence of ()
[7,<*c₅₉*>,<*c₆₀*>] is V1() V2() set
[7,<*c₅₉*>] is V1() set
{7,<*c₅₉*>} is non empty V31() countable set
{{7,<*c₅₉*>},{7}} is non empty V31() V35() countable set
[[7,<*c₅₉*>],<*c₆₀*>] is V1() set
{[7,<*c₅₉*>],<*c₆₀*>} is non empty V31() countable set
{[7,<*c₅₉*>]} is non empty trivial Function-like V31() 1 -element countable set
{{[7,<*c₅₉*>],<*c₆₀*>},{[7,<*c₅₉*>]}} is non empty V31() V35() countable set
c₅₆ is Relation-like Function-like () * () -compatible Element of product (() * ())
c₆₂ is Element of ()
c₆₃ is Element of ()
<*c₆₂,c₆₃*> is set
[2,{},<*c₆₂,c₆₃*>] is V1() V2() set
[[2,{}],<*c₆₂,c₆₃*>] is V1() set
{[2,{}],<*c₆₂,c₆₃*>} is non empty V31() countable set
{{[2,{}],<*c₆₂,c₆₃*>},{[2,{}]}} is non empty V31() V35() countable set
c₆₄ is ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT
<*c₆₄*> is Relation-like Function-like set
c₆₅ is Element of ()
<*c₆₅*> is Relation-like NAT -defined () -valued Function-like FinSequence-like FinSequence of ()
[8,<*c₆₄*>,<*c₆₅*>] is V1() V2() set
[8,<*c₆₄*>] is V1() set
{8,<*c₆₄*>} is non empty V31() countable set
{{8,<*c₆₄*>},{8}} is non empty V31() V35() countable set
[[8,<*c₆₄*>],<*c₆₅*>] is V1() set
{[8,<*c₆₄*>],<*c₆₅*>} is non empty V31() countable set
{[8,<*c₆₄*>]} is non empty trivial Function-like V31() 1 -element countable set
{{[8,<*c₆₄*>],<*c₆₅*>},{[8,<*c₆₄*>]}} is non empty V31() V35() countable set
c₆₁ is Relation-like Function-like () * () -compatible Element of product (() * ())
c₆₇ is Element of ()
c₆₈ is Element of ()
<*c₆₇,c₆₈*> is set
[3,{},<*c₆₇,c₆₈*>] is V1() V2() set
[[3,{}],<*c₆₇,c₆₈*>] is V1() set
{[3,{}],<*c₆₇,c₆₈*>} is non empty V31() countable set
{{[3,{}],<*c₆₇,c₆₈*>},{[3,{}]}} is non empty V31() V35() countable set
c₆₉ is Element of ()
c₇₀ is Element of ()
<*c₆₉,c₇₀*> is set
[4,{},<*c₆₉,c₇₀*>] is V1() V2() set
[[4,{}],<*c₆₉,c₇₀*>] is V1() set
{[4,{}],<*c₆₉,c₇₀*>} is non empty V31() countable set
{{[4,{}],<*c₆₉,c₇₀*>},{[4,{}]}} is non empty V31() V35() countable set
c₆₆ is Relation-like Function-like () * () -compatible Element of product (() * ())
c₇₂ is Element of ()
c₇₃ is Element of ()
<*c₇₂,c₇₃*> is set
[3,{},<*c₇₂,c₇₃*>] is V1() V2() set
[[3,{}],<*c₇₂,c₇₃*>] is V1() set
{[3,{}],<*c₇₂,c₇₃*>} is non empty V31() countable set
{{[3,{}],<*c₇₂,c₇₃*>},{[3,{}]}} is non empty V31() V35() countable set
c₇₄ is Element of ()
c₇₅ is Element of ()
<*c₇₄,c₇₅*> is set
[5,{},<*c₇₄,c₇₅*>] is V1() V2() set
[[5,{}],<*c₇₄,c₇₅*>] is V1() set
{[5,{}],<*c₇₄,c₇₅*>} is non empty V31() countable set
{{[5,{}],<*c₇₄,c₇₅*>},{[5,{}]}} is non empty V31() V35() countable set
c₇₁ is Relation-like Function-like () * () -compatible Element of product (() * ())
c₇₇ is Element of ()
c₇₈ is Element of ()
<*c₇₇,c₇₈*> is set
[3,{},<*c₇₇,c₇₈*>] is V1() V2() set
[[3,{}],<*c₇₇,c₇₈*>] is V1() set
{[3,{}],<*c₇₇,c₇₈*>} is non empty V31() countable set
{{[3,{}],<*c₇₇,c₇₈*>},{[3,{}]}} is non empty V31() V35() countable set
c₇₉ is ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT
<*c₇₉*> is Relation-like Function-like set
[6,<*c₇₉*>,{}] is V1() V2() set
[6,<*c₇₉*>] is V1() set
{6,<*c₇₉*>} is non empty V31() countable set
{{6,<*c₇₉*>},{6}} is non empty V31() V35() countable set
[[6,<*c₇₉*>],{}] is V1() set
{[6,<*c₇₉*>],{}} is non empty V31() countable set
{[6,<*c₇₉*>]} is non empty trivial Function-like V31() 1 -element countable set
{{[6,<*c₇₉*>],{}},{[6,<*c₇₉*>]}} is non empty V31() V35() countable set
c₇₆ is Relation-like Function-like () * () -compatible Element of product (() * ())
c₈₁ is Element of ()
c₈₂ is Element of ()
<*c₈₁,c₈₂*> is set
[3,{},<*c₈₁,c₈₂*>] is V1() V2() set
[[3,{}],<*c₈₁,c₈₂*>] is V1() set
{[3,{}],<*c₈₁,c₈₂*>} is non empty V31() countable set
{{[3,{}],<*c₈₁,c₈₂*>},{[3,{}]}} is non empty V31() V35() countable set
c₈₃ is ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT
<*c₈₃*> is Relation-like Function-like set
c₈₄ is Element of ()
<*c₈₄*> is Relation-like NAT -defined () -valued Function-like FinSequence-like FinSequence of ()
[7,<*c₈₃*>,<*c₈₄*>] is V1() V2() set
[7,<*c₈₃*>] is V1() set
{7,<*c₈₃*>} is non empty V31() countable set
{{7,<*c₈₃*>},{7}} is non empty V31() V35() countable set
[[7,<*c₈₃*>],<*c₈₄*>] is V1() set
{[7,<*c₈₃*>],<*c₈₄*>} is non empty V31() countable set
{[7,<*c₈₃*>]} is non empty trivial Function-like V31() 1 -element countable set
{{[7,<*c₈₃*>],<*c₈₄*>},{[7,<*c₈₃*>]}} is non empty V31() V35() countable set
c₈₀ is Relation-like Function-like () * () -compatible Element of product (() * ())
c₈₆ is Element of ()
c₈₇ is Element of ()
<*c₈₆,c₈₇*> is set
[3,{},<*c₈₆,c₈₇*>] is V1() V2() set
[[3,{}],<*c₈₆,c₈₇*>] is V1() set
{[3,{}],<*c₈₆,c₈₇*>} is non empty V31() countable set
{{[3,{}],<*c₈₆,c₈₇*>},{[3,{}]}} is non empty V31() V35() countable set
c₈₈ is ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT
<*c₈₈*> is Relation-like Function-like set
c₈₉ is Element of ()
<*c₈₉*> is Relation-like NAT -defined () -valued Function-like FinSequence-like FinSequence of ()
[8,<*c₈₈*>,<*c₈₉*>] is V1() V2() set
[8,<*c₈₈*>] is V1() set
{8,<*c₈₈*>} is non empty V31() countable set
{{8,<*c₈₈*>},{8}} is non empty V31() V35() countable set
[[8,<*c₈₈*>],<*c₈₉*>] is V1() set
{[8,<*c₈₈*>],<*c₈₉*>} is non empty V31() countable set
{[8,<*c₈₈*>]} is non empty trivial Function-like V31() 1 -element countable set
{{[8,<*c₈₈*>],<*c₈₉*>},{[8,<*c₈₈*>]}} is non empty V31() V35() countable set
c₈₅ is Relation-like Function-like () * () -compatible Element of product (() * ())
c₉₁ is Element of ()
c₉₂ is Element of ()
<*c₉₁,c₉₂*> is set
[4,{},<*c₉₁,c₉₂*>] is V1() V2() set
[[4,{}],<*c₉₁,c₉₂*>] is V1() set
{[4,{}],<*c₉₁,c₉₂*>} is non empty V31() countable set
{{[4,{}],<*c₉₁,c₉₂*>},{[4,{}]}} is non empty V31() V35() countable set
c₉₃ is Element of ()
c₉₄ is Element of ()
<*c₉₃,c₉₄*> is set
[5,{},<*c₉₃,c₉₄*>] is V1() V2() set
[[5,{}],<*c₉₃,c₉₄*>] is V1() set
{[5,{}],<*c₉₃,c₉₄*>} is non empty V31() countable set
{{[5,{}],<*c₉₃,c₉₄*>},{[5,{}]}} is non empty V31() V35() countable set
c₉₀ is Relation-like Function-like () * () -compatible Element of product (() * ())
c₉₆ is Element of ()
c₉₇ is Element of ()
<*c₉₆,c₉₇*> is set
[4,{},<*c₉₆,c₉₇*>] is V1() V2() set
[[4,{}],<*c₉₆,c₉₇*>] is V1() set
{[4,{}],<*c₉₆,c₉₇*>} is non empty V31() countable set
{{[4,{}],<*c₉₆,c₉₇*>},{[4,{}]}} is non empty V31() V35() countable set
c₉₈ is ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT
<*c₉₈*> is Relation-like Function-like set
[6,<*c₉₈*>,{}] is V1() V2() set
[6,<*c₉₈*>] is V1() set
{6,<*c₉₈*>} is non empty V31() countable set
{{6,<*c₉₈*>},{6}} is non empty V31() V35() countable set
[[6,<*c₉₈*>],{}] is V1() set
{[6,<*c₉₈*>],{}} is non empty V31() countable set
{[6,<*c₉₈*>]} is non empty trivial Function-like V31() 1 -element countable set
{{[6,<*c₉₈*>],{}},{[6,<*c₉₈*>]}} is non empty V31() V35() countable set
c₉₅ is Relation-like Function-like () * () -compatible Element of product (() * ())
c₁₀₀ is Element of ()
c₁₀₁ is Element of ()
<*c₁₀₀,c₁₀₁*> is set
[4,{},<*c₁₀₀,c₁₀₁*>] is V1() V2() set
[[4,{}],<*c₁₀₀,c₁₀₁*>] is V1() set
{[4,{}],<*c₁₀₀,c₁₀₁*>} is non empty V31() countable set
{{[4,{}],<*c₁₀₀,c₁₀₁*>},{[4,{}]}} is non empty V31() V35() countable set
c₁₀₂ is ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT
<*c₁₀₂*> is Relation-like Function-like set
c₁₀₃ is Element of ()
<*c₁₀₃*> is Relation-like NAT -defined () -valued Function-like FinSequence-like FinSequence of ()
[7,<*c₁₀₂*>,<*c₁₀₃*>] is V1() V2() set
[7,<*c₁₀₂*>] is V1() set
{7,<*c₁₀₂*>} is non empty V31() countable set
{{7,<*c₁₀₂*>},{7}} is non empty V31() V35() countable set
[[7,<*c₁₀₂*>],<*c₁₀₃*>] is V1() set
{[7,<*c₁₀₂*>],<*c₁₀₃*>} is non empty V31() countable set
{[7,<*c₁₀₂*>]} is non empty trivial Function-like V31() 1 -element countable set
{{[7,<*c₁₀₂*>],<*c₁₀₃*>},{[7,<*c₁₀₂*>]}} is non empty V31() V35() countable set
c₉₉ is Relation-like Function-like () * () -compatible Element of product (() * ())
c₁₀₅ is Element of ()
c₁₀₆ is Element of ()
<*c₁₀₅,c₁₀₆*> is set
[4,{},<*c₁₀₅,c₁₀₆*>] is V1() V2() set
[[4,{}],<*c₁₀₅,c₁₀₆*>] is V1() set
{[4,{}],<*c₁₀₅,c₁₀₆*>} is non empty V31() countable set
{{[4,{}],<*c₁₀₅,c₁₀₆*>},{[4,{}]}} is non empty V31() V35() countable set
c₁₀₇ is ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT
<*c₁₀₇*> is Relation-like Function-like set
c₁₀₈ is Element of ()
<*c₁₀₈*> is Relation-like NAT -defined () -valued Function-like FinSequence-like FinSequence of ()
[8,<*c₁₀₇*>,<*c₁₀₈*>] is V1() V2() set
[8,<*c₁₀₇*>] is V1() set
{8,<*c₁₀₇*>} is non empty V31() countable set
{{8,<*c₁₀₇*>},{8}} is non empty V31() V35() countable set
[[8,<*c₁₀₇*>],<*c₁₀₈*>] is V1() set
{[8,<*c₁₀₇*>],<*c₁₀₈*>} is non empty V31() countable set
{[8,<*c₁₀₇*>]} is non empty trivial Function-like V31() 1 -element countable set
{{[8,<*c₁₀₇*>],<*c₁₀₈*>},{[8,<*c₁₀₇*>]}} is non empty V31() V35() countable set
c₁₀₄ is Relation-like Function-like () * () -compatible Element of product (() * ())
c₁₁₀ is Element of ()
c₁₁₁ is Element of ()
<*c₁₁₀,c₁₁₁*> is set
[5,{},<*c₁₁₀,c₁₁₁*>] is V1() V2() set
[[5,{}],<*c₁₁₀,c₁₁₁*>] is V1() set
{[5,{}],<*c₁₁₀,c₁₁₁*>} is non empty V31() countable set
{{[5,{}],<*c₁₁₀,c₁₁₁*>},{[5,{}]}} is non empty V31() V35() countable set
c₁₁₂ is ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT
<*c₁₁₂*> is Relation-like Function-like set
[6,<*c₁₁₂*>,{}] is V1() V2() set
[6,<*c₁₁₂*>] is V1() set
{6,<*c₁₁₂*>} is non empty V31() countable set
{{6,<*c₁₁₂*>},{6}} is non empty V31() V35() countable set
[[6,<*c₁₁₂*>],{}] is V1() set
{[6,<*c₁₁₂*>],{}} is non empty V31() countable set
{[6,<*c₁₁₂*>]} is non empty trivial Function-like V31() 1 -element countable set
{{[6,<*c₁₁₂*>],{}},{[6,<*c₁₁₂*>]}} is non empty V31() V35() countable set
c₁₀₉ is Relation-like Function-like () * () -compatible Element of product (() * ())
c₁₁₄ is Element of ()
c₁₁₅ is Element of ()
<*c₁₁₄,c₁₁₅*> is set
[5,{},<*c₁₁₄,c₁₁₅*>] is V1() V2() set
[[5,{}],<*c₁₁₄,c₁₁₅*>] is V1() set
{[5,{}],<*c₁₁₄,c₁₁₅*>} is non empty V31() countable set
{{[5,{}],<*c₁₁₄,c₁₁₅*>},{[5,{}]}} is non empty V31() V35() countable set
c₁₁₆ is ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT
<*c₁₁₆*> is Relation-like Function-like set
c₁₁₇ is Element of ()
<*c₁₁₇*> is Relation-like NAT -defined () -valued Function-like FinSequence-like FinSequence of ()
[7,<*c₁₁₆*>,<*c₁₁₇*>] is V1() V2() set
[7,<*c₁₁₆*>] is V1() set
{7,<*c₁₁₆*>} is non empty V31() countable set
{{7,<*c₁₁₆*>},{7}} is non empty V31() V35() countable set
[[7,<*c₁₁₆*>],<*c₁₁₇*>] is V1() set
{[7,<*c₁₁₆*>],<*c₁₁₇*>} is non empty V31() countable set
{[7,<*c₁₁₆*>]} is non empty trivial Function-like V31() 1 -element countable set
{{[7,<*c₁₁₆*>],<*c₁₁₇*>},{[7,<*c₁₁₆*>]}} is non empty V31() V35() countable set
c₁₁₃ is Relation-like Function-like () * () -compatible Element of product (() * ())
c₁₁₉ is Element of ()
c₁₂₀ is Element of ()
<*c₁₁₉,c₁₂₀*> is set
[5,{},<*c₁₁₉,c₁₂₀*>] is V1() V2() set
[[5,{}],<*c₁₁₉,c₁₂₀*>] is V1() set
{[5,{}],<*c₁₁₉,c₁₂₀*>} is non empty V31() countable set
{{[5,{}],<*c₁₁₉,c₁₂₀*>},{[5,{}]}} is non empty V31() V35() countable set
c₁₂₁ is ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT
<*c₁₂₁*> is Relation-like Function-like set
c₁₂₂ is Element of ()
<*c₁₂₂*> is Relation-like NAT -defined () -valued Function-like FinSequence-like FinSequence of ()
[8,<*c₁₂₁*>,<*c₁₂₂*>] is V1() V2() set
[8,<*c₁₂₁*>] is V1() set
{8,<*c₁₂₁*>} is non empty V31() countable set
{{8,<*c₁₂₁*>},{8}} is non empty V31() V35() countable set
[[8,<*c₁₂₁*>],<*c₁₂₂*>] is V1() set
{[8,<*c₁₂₁*>],<*c₁₂₂*>} is non empty V31() countable set
{[8,<*c₁₂₁*>]} is non empty trivial Function-like V31() 1 -element countable set
{{[8,<*c₁₂₁*>],<*c₁₂₂*>},{[8,<*c₁₂₁*>]}} is non empty V31() V35() countable set
c₁₁₈ is Relation-like Function-like () * () -compatible Element of product (() * ())
c₁₂₄ is ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT
<*c₁₂₄*> is Relation-like Function-like set
[6,<*c₁₂₄*>,{}] is V1() V2() set
[6,<*c₁₂₄*>] is V1() set
{6,<*c₁₂₄*>} is non empty V31() countable set
{{6,<*c₁₂₄*>},{6}} is non empty V31() V35() countable set
[[6,<*c₁₂₄*>],{}] is V1() set
{[6,<*c₁₂₄*>],{}} is non empty V31() countable set
{[6,<*c₁₂₄*>]} is non empty trivial Function-like V31() 1 -element countable set
{{[6,<*c₁₂₄*>],{}},{[6,<*c₁₂₄*>]}} is non empty V31() V35() countable set
c₁₂₅ is ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT
<*c₁₂₅*> is Relation-like Function-like set
c₁₂₆ is Element of ()
<*c₁₂₆*> is Relation-like NAT -defined () -valued Function-like FinSequence-like FinSequence of ()
[7,<*c₁₂₅*>,<*c₁₂₆*>] is V1() V2() set
[7,<*c₁₂₅*>] is V1() set
{7,<*c₁₂₅*>} is non empty V31() countable set
{{7,<*c₁₂₅*>},{7}} is non empty V31() V35() countable set
[[7,<*c₁₂₅*>],<*c₁₂₆*>] is V1() set
{[7,<*c₁₂₅*>],<*c₁₂₆*>} is non empty V31() countable set
{[7,<*c₁₂₅*>]} is non empty trivial Function-like V31() 1 -element countable set
{{[7,<*c₁₂₅*>],<*c₁₂₆*>},{[7,<*c₁₂₅*>]}} is non empty V31() V35() countable set
c₁₂₃ is Relation-like Function-like () * () -compatible Element of product (() * ())
c₁₂₈ is ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT
<*c₁₂₈*> is Relation-like Function-like set
[6,<*c₁₂₈*>,{}] is V1() V2() set
[6,<*c₁₂₈*>] is V1() set
{6,<*c₁₂₈*>} is non empty V31() countable set
{{6,<*c₁₂₈*>},{6}} is non empty V31() V35() countable set
[[6,<*c₁₂₈*>],{}] is V1() set
{[6,<*c₁₂₈*>],{}} is non empty V31() countable set
{[6,<*c₁₂₈*>]} is non empty trivial Function-like V31() 1 -element countable set
{{[6,<*c₁₂₈*>],{}},{[6,<*c₁₂₈*>]}} is non empty V31() V35() countable set
c₁₂₉ is ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT
<*c₁₂₉*> is Relation-like Function-like set
c₁₃₀ is Element of ()
<*c₁₃₀*> is Relation-like NAT -defined () -valued Function-like FinSequence-like FinSequence of ()
[8,<*c₁₂₉*>,<*c₁₃₀*>] is V1() V2() set
[8,<*c₁₂₉*>] is V1() set
{8,<*c₁₂₉*>} is non empty V31() countable set
{{8,<*c₁₂₉*>},{8}} is non empty V31() V35() countable set
[[8,<*c₁₂₉*>],<*c₁₃₀*>] is V1() set
{[8,<*c₁₂₉*>],<*c₁₃₀*>} is non empty V31() countable set
{[8,<*c₁₂₉*>]} is non empty trivial Function-like V31() 1 -element countable set
{{[8,<*c₁₂₉*>],<*c₁₃₀*>},{[8,<*c₁₂₉*>]}} is non empty V31() V35() countable set
c₁₂₇ is Relation-like Function-like () * () -compatible Element of product (() * ())
c₁₃₂ is ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT
<*c₁₃₂*> is Relation-like Function-like set
c₁₃₃ is Element of ()
<*c₁₃₃*> is Relation-like NAT -defined () -valued Function-like FinSequence-like FinSequence of ()
[7,<*c₁₃₂*>,<*c₁₃₃*>] is V1() V2() set
[7,<*c₁₃₂*>] is V1() set
{7,<*c₁₃₂*>} is non empty V31() countable set
{{7,<*c₁₃₂*>},{7}} is non empty V31() V35() countable set
[[7,<*c₁₃₂*>],<*c₁₃₃*>] is V1() set
{[7,<*c₁₃₂*>],<*c₁₃₃*>} is non empty V31() countable set
{[7,<*c₁₃₂*>]} is non empty trivial Function-like V31() 1 -element countable set
{{[7,<*c₁₃₂*>],<*c₁₃₃*>},{[7,<*c₁₃₂*>]}} is non empty V31() V35() countable set
c₁₃₄ is ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT
<*c₁₃₄*> is Relation-like Function-like set
c₁₃₅ is Element of ()
<*c₁₃₅*> is Relation-like NAT -defined () -valued Function-like FinSequence-like FinSequence of ()
[8,<*c₁₃₄*>,<*c₁₃₅*>] is V1() V2() set
[8,<*c₁₃₄*>] is V1() set
{8,<*c₁₃₄*>} is non empty V31() countable set
{{8,<*c₁₃₄*>},{8}} is non empty V31() V35() countable set
[[8,<*c₁₃₄*>],<*c₁₃₅*>] is V1() set
{[8,<*c₁₃₄*>],<*c₁₃₅*>} is non empty V31() countable set
{[8,<*c₁₃₄*>]} is non empty trivial Function-like V31() 1 -element countable set
{{[8,<*c₁₃₄*>],<*c₁₃₅*>},{[8,<*c₁₃₄*>]}} is non empty V31() V35() countable set
c₁₃₁ is Relation-like Function-like () * () -compatible Element of product (() * ())
z is Element of ()
k is Element of ()
<*z,k*> is set
[1,{},<*z,k*>] is V1() V2() set
[1,{}] is V1() set
{1,{}} is non empty V31() V35() countable set
{1} is non empty trivial V31() V35() 1 -element countable set
{{1,{}},{1}} is non empty V31() V35() countable set
[[1,{}],<*z,k*>] is V1() set
{[1,{}],<*z,k*>} is non empty V31() countable set
{[1,{}]} is non empty trivial Function-like V31() 1 -element countable set
{{[1,{}],<*z,k*>},{[1,{}]}} is non empty V31() V35() countable set
c₅ is Element of ()
y is Element of ()
<*c₅,y*> is set
[2,{},<*c₅,y*>] is V1() V2() set
[2,{}] is V1() set
{2,{}} is non empty V31() V35() countable set
{2} is non empty trivial V31() V35() 1 -element countable set
{{2,{}},{2}} is non empty V31() V35() countable set
[[2,{}],<*c₅,y*>] is V1() set
{[2,{}],<*c₅,y*>} is non empty V31() countable set
{[2,{}]} is non empty trivial Function-like V31() 1 -element countable set
{{[2,{}],<*c₅,y*>},{[2,{}]}} is non empty V31() V35() countable set
c₇ is Element of ()
c₈ is Element of ()
<*c₇,c₈*> is set
[3,{},<*c₇,c₈*>] is V1() V2() set
[3,{}] is V1() set
{3,{}} is non empty V31() V35() countable set
{3} is non empty trivial V31() V35() 1 -element countable set
{{3,{}},{3}} is non empty V31() V35() countable set
[[3,{}],<*c₇,c₈*>] is V1() set
{[3,{}],<*c₇,c₈*>} is non empty V31() countable set
{[3,{}]} is non empty trivial Function-like V31() 1 -element countable set
{{[3,{}],<*c₇,c₈*>},{[3,{}]}} is non empty V31() V35() countable set
c₉ is Element of ()
c₁₀ is Element of ()
<*c₉,c₁₀*> is set
[4,{},<*c₉,c₁₀*>] is V1() V2() set
[4,{}] is V1() set
{4,{}} is non empty V31() V35() countable set
{4} is non empty trivial V31() V35() 1 -element countable set
{{4,{}},{4}} is non empty V31() V35() countable set
[[4,{}],<*c₉,c₁₀*>] is V1() set
{[4,{}],<*c₉,c₁₀*>} is non empty V31() countable set
{[4,{}]} is non empty trivial Function-like V31() 1 -element countable set
{{[4,{}],<*c₉,c₁₀*>},{[4,{}]}} is non empty V31() V35() countable set
c₁₁ is Element of ()
c₁₂ is Element of ()
<*c₁₁,c₁₂*> is set
[5,{},<*c₁₁,c₁₂*>] is V1() V2() set
[5,{}] is V1() set
{5,{}} is non empty V31() V35() countable set
{5} is non empty trivial V31() V35() 1 -element countable set
{{5,{}},{5}} is non empty V31() V35() countable set
[[5,{}],<*c₁₁,c₁₂*>] is V1() set
{[5,{}],<*c₁₁,c₁₂*>} is non empty V31() countable set
{[5,{}]} is non empty trivial Function-like V31() 1 -element countable set
{{[5,{}],<*c₁₁,c₁₂*>},{[5,{}]}} is non empty V31() V35() countable set
c₁₃ is ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT
<*c₁₃*> is Relation-like Function-like set
[6,<*c₁₃*>,{}] is V1() V2() set
[6,<*c₁₃*>] is V1() set
{6,<*c₁₃*>} is non empty V31() countable set
{6} is non empty trivial V31() V35() 1 -element countable set
{{6,<*c₁₃*>},{6}} is non empty V31() V35() countable set
[[6,<*c₁₃*>],{}] is V1() set
{[6,<*c₁₃*>],{}} is non empty V31() countable set
{[6,<*c₁₃*>]} is non empty trivial Function-like V31() 1 -element countable set
{{[6,<*c₁₃*>],{}},{[6,<*c₁₃*>]}} is non empty V31() V35() countable set
c₁₄ is ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT
<*c₁₄*> is Relation-like Function-like set
c₁₅ is Element of ()
<*c₁₅*> is Relation-like NAT -defined () -valued Function-like FinSequence-like FinSequence of ()
[7,<*c₁₄*>,<*c₁₅*>] is V1() V2() set
[7,<*c₁₄*>] is V1() set
{7,<*c₁₄*>} is non empty V31() countable set
{7} is non empty trivial V31() V35() 1 -element countable set
{{7,<*c₁₄*>},{7}} is non empty V31() V35() countable set
[[7,<*c₁₄*>],<*c₁₅*>] is V1() set
{[7,<*c₁₄*>],<*c₁₅*>} is non empty V31() countable set
{[7,<*c₁₄*>]} is non empty trivial Function-like V31() 1 -element countable set
{{[7,<*c₁₄*>],<*c₁₅*>},{[7,<*c₁₄*>]}} is non empty V31() V35() countable set
c₁₆ is ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT
<*c₁₆*> is Relation-like Function-like set
c₁₇ is Element of ()
<*c₁₇*> is Relation-like NAT -defined () -valued Function-like FinSequence-like FinSequence of ()
[8,<*c₁₆*>,<*c₁₇*>] is V1() V2() set
[8,<*c₁₆*>] is V1() set
{8,<*c₁₆*>} is non empty V31() countable set
{8} is non empty trivial V31() V35() 1 -element countable set
{{8,<*c₁₆*>},{8}} is non empty V31() V35() countable set
[[8,<*c₁₆*>],<*c₁₇*>] is V1() set
{[8,<*c₁₆*>],<*c₁₇*>} is non empty V31() countable set
{[8,<*c₁₆*>]} is non empty trivial Function-like V31() 1 -element countable set
{{[8,<*c₁₆*>],<*c₁₇*>},{[8,<*c₁₆*>]}} is non empty V31() V35() countable set
K99((product (() * ())),(product (() * ()))) is non empty functional set
[:SCM-Instr,K99((product (() * ())),(product (() * ()))):] is set
bool [:SCM-Instr,K99((product (() * ())),(product (() * ()))):] is set
[:SCM-Instr,(product (() * ())):] is set
[:[:SCM-Instr,(product (() * ())):],(product (() * ())):] is set
bool [:[:SCM-Instr,(product (() * ())):],(product (() * ())):] is set
x is Relation-like [:SCM-Instr,(product (() * ())):] -defined product (() * ()) -valued Function-like V17([:SCM-Instr,(product (() * ())):]) V18([:SCM-Instr,(product (() * ())):], product (() * ())) Function-yielding V97() Element of bool [:[:SCM-Instr,(product (() * ())):],(product (() * ())):]
curry x is non empty Relation-like SCM-Instr -defined K107((product (() * ())),(product (() * ()))) -valued Function-like V17( SCM-Instr ) V18( SCM-Instr ,K107((product (() * ())),(product (() * ())))) Function-yielding V97() Element of bool [:SCM-Instr,K107((product (() * ())),(product (() * ()))):]
K107((product (() * ())),(product (() * ()))) is non empty functional M4( product (() * ()), product (() * ()))
[:SCM-Instr,K107((product (() * ())),(product (() * ()))):] is set
bool [:SCM-Instr,K107((product (() * ())),(product (() * ()))):] is set
y is Element of SCM-Instr
(curry x) . y is Relation-like Function-like Element of K99((product (() * ())),(product (() * ())))
z is Relation-like Function-like () * () -compatible Element of product (() * ())
((curry x) . y) . z is set
(y,z) is Relation-like Function-like () * () -compatible Element of product (() * ())
(curry x) . y is Relation-like product (() * ()) -defined product (() * ()) -valued Function-like V17( product (() * ())) V18( product (() * ()), product (() * ())) Function-yielding V97() Element of K107((product (() * ())),(product (() * ())))
((curry x) . y) . z is Relation-like Function-like () * () -compatible Element of product (() * ())
x . (y,z) is Relation-like Function-like () * () -compatible Element of product (() * ())
x is non empty Relation-like SCM-Instr -defined K99((product (() * ())),(product (() * ()))) -valued Function-like V17( SCM-Instr ) V18( SCM-Instr ,K99((product (() * ())),(product (() * ())))) Function-yielding V97() Element of bool [:SCM-Instr,K99((product (() * ())),(product (() * ()))):]
y is non empty Relation-like SCM-Instr -defined K99((product (() * ())),(product (() * ()))) -valued Function-like V17( SCM-Instr ) V18( SCM-Instr ,K99((product (() * ())),(product (() * ())))) Function-yielding V97() Element of bool [:SCM-Instr,K99((product (() * ())),(product (() * ()))):]
[:(product (() * ())),(product (() * ())):] is set
bool [:(product (() * ())),(product (() * ())):] is set
z is Element of SCM-Instr
y . z is Relation-like Function-like Element of K99((product (() * ())),(product (() * ())))
x . z is Relation-like Function-like Element of K99((product (() * ())),(product (() * ())))
c₅ is non empty Relation-like product (() * ()) -defined product (() * ()) -valued Function-like V17( product (() * ())) V18( product (() * ()), product (() * ())) Function-yielding V97() Element of bool [:(product (() * ())),(product (() * ())):]
y is Relation-like Function-like () * () -compatible Element of product (() * ())
c₅ . y is Relation-like Function-like () * () -compatible Element of product (() * ())
(z,y) is Relation-like Function-like () * () -compatible Element of product (() * ())
k is non empty Relation-like product (() * ()) -defined product (() * ()) -valued Function-like V17( product (() * ())) V18( product (() * ()), product (() * ())) Function-yielding V97() Element of bool [:(product (() * ())),(product (() * ())):]
k . y is Relation-like Function-like () * () -compatible Element of product (() * ())
() is non empty Relation-like SCM-Instr -defined K99((product (() * ())),(product (() * ()))) -valued Function-like V17( SCM-Instr ) V18( SCM-Instr ,K99((product (() * ())),(product (() * ())))) Function-yielding V97() Element of bool [:SCM-Instr,K99((product (() * ())),(product (() * ()))):]
x is set
{1} is non empty trivial V31() V35() 1 -element countable set
y is set
z is set
[y,z] is V1() set
{y,z} is non empty V31() countable set
{y} is non empty trivial V31() 1 -element countable set
{{y,z},{y}} is non empty V31() V35() countable set
k is ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT
[1,k] is V1() set
{1,k} is non empty V31() V35() countable set
{{1,k},{1}} is non empty V31() V35() countable set
x is ordinal natural V31() cardinal countable V86() integer V111() ext-real set
[1,x] is V1() set
{1,x} is non empty V31() V35() countable set
{1} is non empty trivial V31() V35() 1 -element countable set
{{1,x},{1}} is non empty V31() V35() countable set
x is Element of ()
x is Relation-like Function-like () * () -compatible Element of product (() * ())
proj1 x is set