:: 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

<*k,c

[1,{},<*k,c

[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

{[1,{}],<*k,c

{[1,{}]} is non empty trivial Function-like V31() 1 -element countable set

{{[1,{}],<*k,c

y is Element of ()

c

<*y,c

[2,{},<*y,c

[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

{[2,{}],<*y,c

{[2,{}]} is non empty trivial Function-like V31() 1 -element countable set

{{[2,{}],<*y,c

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

c

c

<*c

[1,{},<*c

[[1,{}],<*c

{[1,{}],<*c

{{[1,{}],<*c

c

c

<*c

[3,{},<*c

[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

{[3,{}],<*c

{[3,{}]} is non empty trivial Function-like V31() 1 -element countable set

{{[3,{}],<*c

c

c

c

<*c

[1,{},<*c

[[1,{}],<*c

{[1,{}],<*c

{{[1,{}],<*c

c

c

<*c

[4,{},<*c

[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

{[4,{}],<*c

{[4,{}]} is non empty trivial Function-like V31() 1 -element countable set

{{[4,{}],<*c

c

c

c

<*c

[1,{},<*c

[[1,{}],<*c

{[1,{}],<*c

{{[1,{}],<*c

c

c

<*c

[5,{},<*c

[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

{[5,{}],<*c

{[5,{}]} is non empty trivial Function-like V31() 1 -element countable set

{{[5,{}],<*c

c

c

c

<*c

[1,{},<*c

[[1,{}],<*c

{[1,{}],<*c

{{[1,{}],<*c

c

<*c

[6,<*c

[6,<*c

{6,<*c

{6} is non empty trivial V31() V35() 1 -element countable set

{{6,<*c

[[6,<*c

{[6,<*c

{[6,<*c

{{[6,<*c

c

c

c

<*c

[1,{},<*c

[[1,{}],<*c

{[1,{}],<*c

{{[1,{}],<*c

c

<*c

c

<*c

[7,<*c

[7,<*c

{7,<*c

{7} is non empty trivial V31() V35() 1 -element countable set

{{7,<*c

[[7,<*c

{[7,<*c

{[7,<*c

{{[7,<*c

c

c

c

<*c

[1,{},<*c

[[1,{}],<*c

{[1,{}],<*c

{{[1,{}],<*c

c

<*c

c

<*c

[8,<*c

[8,<*c

{8,<*c

{8} is non empty trivial V31() V35() 1 -element countable set

{{8,<*c

[[8,<*c

{[8,<*c

{[8,<*c

{{[8,<*c

c

c

c

<*c

[2,{},<*c

[[2,{}],<*c

{[2,{}],<*c

{{[2,{}],<*c

c

c

<*c

[3,{},<*c

[[3,{}],<*c

{[3,{}],<*c

{{[3,{}],<*c

c

c

c

<*c

[2,{},<*c

[[2,{}],<*c

{[2,{}],<*c

{{[2,{}],<*c

c

c

<*c

[4,{},<*c

[[4,{}],<*c

{[4,{}],<*c

{{[4,{}],<*c

c

c

c

<*c

[2,{},<*c

[[2,{}],<*c

{[2,{}],<*c

{{[2,{}],<*c

c

c

<*c

[5,{},<*c

[[5,{}],<*c

{[5,{}],<*c

{{[5,{}],<*c

c

c

c

<*c

[2,{},<*c

[[2,{}],<*c

{[2,{}],<*c

{{[2,{}],<*c

c

<*c

[6,<*c

[6,<*c

{6,<*c

{{6,<*c

[[6,<*c

{[6,<*c

{[6,<*c

{{[6,<*c

c

c

c

<*c

[2,{},<*c

[[2,{}],<*c

{[2,{}],<*c

{{[2,{}],<*c

c

<*c

c

<*c

[7,<*c

[7,<*c

{7,<*c

{{7,<*c

[[7,<*c

{[7,<*c

{[7,<*c

{{[7,<*c

c

c

c

<*c

[2,{},<*c

[[2,{}],<*c

{[2,{}],<*c

{{[2,{}],<*c

c

<*c

c

<*c

[8,<*c

[8,<*c

{8,<*c

{{8,<*c

[[8,<*c

{[8,<*c

{[8,<*c

{{[8,<*c

c

c

c

<*c

[3,{},<*c

[[3,{}],<*c

{[3,{}],<*c

{{[3,{}],<*c

c

c

<*c

[4,{},<*c

[[4,{}],<*c

{[4,{}],<*c

{{[4,{}],<*c

c

c

c

<*c

[3,{},<*c

[[3,{}],<*c

{[3,{}],<*c

{{[3,{}],<*c

c

c

<*c

[5,{},<*c

[[5,{}],<*c

{[5,{}],<*c

{{[5,{}],<*c

c

c

c

<*c

[3,{},<*c

[[3,{}],<*c

{[3,{}],<*c

{{[3,{}],<*c

c

<*c

[6,<*c

[6,<*c

{6,<*c

{{6,<*c

[[6,<*c

{[6,<*c

{[6,<*c

{{[6,<*c

c

c

c

<*c

[3,{},<*c

[[3,{}],<*c

{[3,{}],<*c

{{[3,{}],<*c

c

<*c

c

<*c

[7,<*c

[7,<*c

{7,<*c

{{7,<*c

[[7,<*c

{[7,<*c

{[7,<*c

{{[7,<*c

c

c

c

<*c

[3,{},<*c

[[3,{}],<*c

{[3,{}],<*c

{{[3,{}],<*c

c

<*c

c

<*c

[8,<*c

[8,<*c

{8,<*c

{{8,<*c

[[8,<*c

{[8,<*c

{[8,<*c

{{[8,<*c

c

c

c

<*c

[4,{},<*c

[[4,{}],<*c

{[4,{}],<*c

{{[4,{}],<*c

c

c

<*c

[5,{},<*c

[[5,{}],<*c

{[5,{}],<*c

{{[5,{}],<*c

c

c

c

<*c

[4,{},<*c

[[4,{}],<*c

{[4,{}],<*c

{{[4,{}],<*c

c

<*c

[6,<*c

[6,<*c

{6,<*c

{{6,<*c

[[6,<*c

{[6,<*c

{[6,<*c

{{[6,<*c

c

c

c

<*c

[4,{},<*c

[[4,{}],<*c

{[4,{}],<*c

{{[4,{}],<*c

c

<*c

c

<*c

[7,<*c

[7,<*c

{7,<*c

{{7,<*c

[[7,<*c

{[7,<*c

{[7,<*c

{{[7,<*c

c

c

c

<*c

[4,{},<*c

[[4,{}],<*c

{[4,{}],<*c

{{[4,{}],<*c

c

<*c

c

<*c

[8,<*c

[8,<*c

{8,<*c

{{8,<*c

[[8,<*c

{[8,<*c

{[8,<*c

{{[8,<*c

c

c

c

<*c

[5,{},<*c

[[5,{}],<*c

{[5,{}],<*c

{{[5,{}],<*c

c

<*c

[6,<*c

[6,<*c

{6,<*c

{{6,<*c

[[6,<*c

{[6,<*c

{[6,<*c

{{[6,<*c

c

c

c

<*c

[5,{},<*c

[[5,{}],<*c

{[5,{}],<*c

{{[5,{}],<*c

c

<*c

c

<*c

[7,<*c

[7,<*c

{7,<*c