:: EXTPRO_1 semantic presentation

REAL is non empty non with_non-empty_elements set

bool omega is non empty non trivial non empty-membered non finite set
bool NAT is non empty non trivial non empty-membered non finite set

RAT is set
INT is set

N is non empty non with_non-empty_elements set

[0,{},{}] is V7() V8() set
is non empty V7() set
is non empty functional finite V40() countable set

is non empty V7() set
is non empty finite countable set

bool is set

product (() * ()) is non empty functional with_common_domain product-like set
id (product (() * ())) is non empty Relation-like product (() * ()) -defined product (() * ()) -valued Function-like one-to-one total V21( product (() * ()), product (() * ())) Function-yielding V35() Element of bool [:(product (() * ())),(product (() * ())):]
[:(product (() * ())),(product (() * ())):] is Relation-like set
bool [:(product (() * ())),(product (() * ())):] is set

--> (id (product (() * ()))) is non empty Relation-like non-empty non empty-yielding -defined {(id (product (() * ())))} -valued Function-like constant total V21(,{(id (product (() * ())))}) Function-yielding V35() finite countable V120() Element of bool [:,{(id (product (() * ())))}:]

[:,{(id (product (() * ())))}:] is Relation-like finite countable set
bool [:,{(id (product (() * ())))}:] is finite V40() countable set

bool [:,N:] is set

product (() * k) is non empty functional with_common_domain product-like set
K108((product (() * k)),(product (() * k))) is non empty functional set
[:,K108((product (() * k)),(product (() * k))):] is Relation-like set
bool [:,K108((product (() * k)),(product (() * k))):] is set
id (product (() * k)) is non empty Relation-like product (() * k) -defined product (() * k) -valued Function-like one-to-one total V21( product (() * k), product (() * k)) Function-yielding V35() Element of bool [:(product (() * k)),(product (() * k)):]
[:(product (() * k)),(product (() * k)):] is Relation-like set
bool [:(product (() * k)),(product (() * k)):] is set
--> (id (product (() * k))) is non empty Relation-like non-empty non empty-yielding -defined {(id (product (() * k)))} -valued Function-like constant total V21(,{(id (product (() * k)))}) Function-yielding V35() finite countable V120() Element of bool [:,{(id (product (() * k)))}:]

[:,{(id (product (() * k)))}:] is Relation-like finite countable set
bool [:,{(id (product (() * k)))}:] is finite V40() countable set

l is non empty Relation-like -defined K108((product (() * k)),(product (() * k))) -valued Function-like total V21(,K108((product (() * k)),(product (() * k)))) Function-yielding V35() finite countable V120() Element of bool [:,K108((product (() * k)),(product (() * k))):]
(N,,s2,,k,(),l) is (N) (N)
l is (N) (N)
the carrier of l is set
the ZeroF of l is Element of the carrier of l

the Object-Kind of l is Relation-like the carrier of l -defined N -valued Function-like total V21( the carrier of l,N) Element of bool [: the carrier of l,N:]
[: the carrier of l,N:] is Relation-like set
bool [: the carrier of l,N:] is set
the ValuesF of l is non empty Relation-like N -defined Function-like total set
the of l is non empty Relation-like the InstructionsF of l -defined K108((product ( the Object-Kind of l * the ValuesF of l)),(product ( the Object-Kind of l * the ValuesF of l))) -valued Function-like total V21( the InstructionsF of l,K108((product ( the Object-Kind of l * the ValuesF of l)),(product ( the Object-Kind of l * the ValuesF of l)))) Function-yielding V35() Element of bool [: the InstructionsF of l,K108((product ( the Object-Kind of l * the ValuesF of l)),(product ( the Object-Kind of l * the ValuesF of l))):]
the Object-Kind of l * the ValuesF of l is Relation-like the carrier of l -defined Function-like total set
product ( the Object-Kind of l * the ValuesF of l) is functional with_common_domain product-like set
K108((product ( the Object-Kind of l * the ValuesF of l)),(product ( the Object-Kind of l * the ValuesF of l))) is non empty functional set
[: the InstructionsF of l,K108((product ( the Object-Kind of l * the ValuesF of l)),(product ( the Object-Kind of l * the ValuesF of l))):] is Relation-like set
bool [: the InstructionsF of l,K108((product ( the Object-Kind of l * the ValuesF of l)),(product ( the Object-Kind of l * the ValuesF of l))):] is set
S is (N) (N)
the carrier of S is set
the ZeroF of S is Element of the carrier of S

the Object-Kind of S is Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]
[: the carrier of S,N:] is Relation-like set
bool [: the carrier of S,N:] is set
the ValuesF of S is non empty Relation-like N -defined Function-like total set
the of S is non empty Relation-like the InstructionsF of S -defined K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))) -valued Function-like total V21( the InstructionsF of S,K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))) Function-yielding V35() Element of bool [: the InstructionsF of S,K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))):]
the Object-Kind of S * the ValuesF of S is Relation-like the carrier of S -defined Function-like total set
product ( the Object-Kind of S * the ValuesF of S) is functional with_common_domain product-like set
K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))) is non empty functional set
[: the InstructionsF of S,K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))):] is Relation-like set
bool [: the InstructionsF of S,K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))):] is set
P is (N) (N)
the carrier of P is set
the ZeroF of P is Element of the carrier of P

the Object-Kind of P is Relation-like the carrier of P -defined N -valued Function-like total V21( the carrier of P,N) Element of bool [: the carrier of P,N:]
[: the carrier of P,N:] is Relation-like set
bool [: the carrier of P,N:] is set
the ValuesF of P is non empty Relation-like N -defined Function-like total set
the of P is non empty Relation-like the InstructionsF of P -defined K108((product ( the Object-Kind of P * the ValuesF of P)),(product ( the Object-Kind of P * the ValuesF of P))) -valued Function-like total V21( the InstructionsF of P,K108((product ( the Object-Kind of P * the ValuesF of P)),(product ( the Object-Kind of P * the ValuesF of P)))) Function-yielding V35() Element of bool [: the InstructionsF of P,K108((product ( the Object-Kind of P * the ValuesF of P)),(product ( the Object-Kind of P * the ValuesF of P))):]
the Object-Kind of P * the ValuesF of P is Relation-like the carrier of P -defined Function-like total set
product ( the Object-Kind of P * the ValuesF of P) is functional with_common_domain product-like set
K108((product ( the Object-Kind of P * the ValuesF of P)),(product ( the Object-Kind of P * the ValuesF of P))) is non empty functional set
[: the InstructionsF of P,K108((product ( the Object-Kind of P * the ValuesF of P)),(product ( the Object-Kind of P * the ValuesF of P))):] is Relation-like set
bool [: the InstructionsF of P,K108((product ( the Object-Kind of P * the ValuesF of P)),(product ( the Object-Kind of P * the ValuesF of P))):] is set
N is non empty non with_non-empty_elements set
(N) is (N) (N)
the carrier of (N) is set
N is non empty non with_non-empty_elements set
(N) is non empty trivial finite 1 -element (N) (N)
N is non empty non with_non-empty_elements set
(N) is non empty trivial finite 1 -element (N) (N)
S is set
the_Values_of (N) is non empty Relation-like the carrier of (N) -defined Function-like total V120() set
the carrier of (N) is non empty trivial finite 1 -element countable set
the Object-Kind of (N) is non empty Relation-like the carrier of (N) -defined N -valued Function-like total V21( the carrier of (N),N) finite countable V120() Element of bool [: the carrier of (N),N:]
[: the carrier of (N),N:] is Relation-like set
bool [: the carrier of (N),N:] is set
the ValuesF of (N) is non empty Relation-like N -defined Function-like total set
the Object-Kind of (N) * the ValuesF of (N) is non empty Relation-like the carrier of (N) -defined Function-like total finite countable V120() set
proj1 () is non empty set
() . S is set
the Object-Kind of (N) . S is set
proj1 the ValuesF of (N) is non empty set

bool is set
the ValuesF of (N) . ( the Object-Kind of (N) . S) is set
N is non empty non with_non-empty_elements set
(N) is non empty trivial finite 1 -element with_non-empty_values (N) (N)
N is non empty non with_non-empty_elements set
S is with_non-empty_values (N)

the carrier of S is set

the Object-Kind of S is Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]
[: the carrier of S,N:] is Relation-like set
bool [: the carrier of S,N:] is set
the ValuesF of S is non empty Relation-like N -defined Function-like total set
the Object-Kind of S * the ValuesF of S is Relation-like the carrier of S -defined Function-like total set
product ( the Object-Kind of S * the ValuesF of S) is functional with_common_domain product-like set
K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))) is non empty functional set
the of S is non empty Relation-like the InstructionsF of S -defined K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))) -valued Function-like total V21( the InstructionsF of S,K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))) Function-yielding V35() Element of bool [: the InstructionsF of S,K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))):]
[: the InstructionsF of S,K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))):] is Relation-like set
bool [: the InstructionsF of S,K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))):] is set
P is Element of the InstructionsF of S
the of S . P is Relation-like Function-like Element of K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))

( the of S . P) . s is set

proj1 k is set
proj2 k is set

( the of S . P) . s2 is set
N is non empty non with_non-empty_elements set
S is with_non-empty_values (N)

N is non empty non with_non-empty_elements set
N is non empty non with_non-empty_elements set
(N) is non empty trivial finite 1 -element with_non-empty_values (N) (N)

bool is set

the Object-Kind of (N) is non empty Relation-like the carrier of (N) -defined N -valued Function-like total V21( the carrier of (N),N) finite countable V120() Element of bool [: the carrier of (N),N:]
the carrier of (N) is non empty trivial finite 1 -element countable set
[: the carrier of (N),N:] is Relation-like set
bool [: the carrier of (N),N:] is set
the ValuesF of (N) is non empty Relation-like N -defined Function-like total set
halt (N) is Element of the InstructionsF of (N)
the InstructionsF of (N) is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
halt the InstructionsF of (N) is ins-loc-free Element of the InstructionsF of (N)
the_Values_of (N) is non empty Relation-like non-empty non empty-yielding the carrier of (N) -defined Function-like total V120() set
the Object-Kind of (N) * the ValuesF of (N) is non empty Relation-like the carrier of (N) -defined Function-like total finite countable V120() set
k is non empty Relation-like the carrier of (N) -defined Function-like the_Values_of (N) -compatible total V120() set
(N,(N),(halt (N)),k) is non empty Relation-like the carrier of (N) -defined Function-like the_Values_of (N) -compatible total V120() set
product ( the Object-Kind of (N) * the ValuesF of (N)) is functional with_common_domain product-like set
K108((product ( the Object-Kind of (N) * the ValuesF of (N))),(product ( the Object-Kind of (N) * the ValuesF of (N)))) is non empty functional set
the of (N) is non empty Relation-like the InstructionsF of (N) -defined K108((product ( the Object-Kind of (N) * the ValuesF of (N))),(product ( the Object-Kind of (N) * the ValuesF of (N)))) -valued Function-like total V21( the InstructionsF of (N),K108((product ( the Object-Kind of (N) * the ValuesF of (N))),(product ( the Object-Kind of (N) * the ValuesF of (N))))) Function-yielding V35() Element of bool [: the InstructionsF of (N),K108((product ( the Object-Kind of (N) * the ValuesF of (N))),(product ( the Object-Kind of (N) * the ValuesF of (N)))):]
[: the InstructionsF of (N),K108((product ( the Object-Kind of (N) * the ValuesF of (N))),(product ( the Object-Kind of (N) * the ValuesF of (N)))):] is Relation-like set
bool [: the InstructionsF of (N),K108((product ( the Object-Kind of (N) * the ValuesF of (N))),(product ( the Object-Kind of (N) * the ValuesF of (N)))):] is set
the of (N) . (halt (N)) is Relation-like Function-like Element of K108((product ( the Object-Kind of (N) * the ValuesF of (N))),(product ( the Object-Kind of (N) * the ValuesF of (N))))
( the of (N) . (halt (N))) . k is set

product (() * ()) is non empty functional with_common_domain product-like set
id (product (() * ())) is non empty Relation-like product (() * ()) -defined product (() * ()) -valued Function-like one-to-one total V21( product (() * ()), product (() * ())) Function-yielding V35() Element of bool [:(product (() * ())),(product (() * ())):]
[:(product (() * ())),(product (() * ())):] is Relation-like set
bool [:(product (() * ())),(product (() * ())):] is set
(halt (N)) .--> (id (product (() * ()))) is trivial Relation-like the InstructionsF of (N) -defined {(halt (N))} -defined Function-like one-to-one constant Function-yielding V35() finite countable V120() set
{(halt (N))} is non empty trivial finite 1 -element countable set
{(halt (N))} --> (id (product (() * ()))) is non empty Relation-like non-empty non empty-yielding {(halt (N))} -defined {(id (product (() * ())))} -valued Function-like constant total V21({(halt (N))},{(id (product (() * ())))}) Function-yielding V35() finite countable V120() Element of bool [:{(halt (N))},{(id (product (() * ())))}:]

[:{(halt (N))},{(id (product (() * ())))}:] is Relation-like finite countable set
bool [:{(halt (N))},{(id (product (() * ())))}:] is finite V40() countable set
((halt (N)) .--> (id (product (() * ())))) . (halt (N)) is Relation-like Function-like set
s2 is non empty Relation-like the carrier of (N) -defined Function-like the_Values_of (N) -compatible total V120() Element of product ()
(id (product (() * ()))) . s2 is Relation-like Function-like set
N is non empty non with_non-empty_elements set
(N) is non empty trivial finite 1 -element with_non-empty_values (N) (N) (N)
N is non empty non with_non-empty_elements set
S is with_non-empty_values (N) (N)
halt S is Element of the InstructionsF of S

halt the InstructionsF of S is ins-loc-free Element of the InstructionsF of S
N is non empty non with_non-empty_elements set
S is with_non-empty_values (N) (N)

halt S is (N,S) Element of the InstructionsF of S
halt the InstructionsF of S is ins-loc-free Element of the InstructionsF of S
N is non empty non with_non-empty_elements set
(N) is non empty trivial finite 1 -element with_non-empty_values (N) (N) (N)
the carrier of (N) is non empty trivial finite 1 -element countable set
the_Values_of (N) is non empty Relation-like non-empty non empty-yielding the carrier of (N) -defined Function-like total V120() set
the Object-Kind of (N) is non empty Relation-like the carrier of (N) -defined N -valued Function-like total V21( the carrier of (N),N) finite countable V120() Element of bool [: the carrier of (N),N:]
[: the carrier of (N),N:] is Relation-like set
bool [: the carrier of (N),N:] is set
the ValuesF of (N) is non empty Relation-like N -defined Function-like total set
the Object-Kind of (N) * the ValuesF of (N) is non empty Relation-like the carrier of (N) -defined Function-like total finite countable V120() set
the InstructionsF of (N) is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
P is non empty Relation-like the carrier of (N) -defined Function-like the_Values_of (N) -compatible total V120() set
s is Element of the InstructionsF of (N)
(N,(N),s,P) is non empty Relation-like the carrier of (N) -defined Function-like the_Values_of (N) -compatible total V120() set
product ( the Object-Kind of (N) * the ValuesF of (N)) is functional with_common_domain product-like set
K108((product ( the Object-Kind of (N) * the ValuesF of (N))),(product ( the Object-Kind of (N) * the ValuesF of (N)))) is non empty functional set
the of (N) is non empty Relation-like the InstructionsF of (N) -defined K108((product ( the Object-Kind of (N) * the ValuesF of (N))),(product ( the Object-Kind of (N) * the ValuesF of (N)))) -valued Function-like total V21( the InstructionsF of (N),K108((product ( the Object-Kind of (N) * the ValuesF of (N))),(product ( the Object-Kind of (N) * the ValuesF of (N))))) Function-yielding V35() Element of bool [: the InstructionsF of (N),K108((product ( the Object-Kind of (N) * the ValuesF of (N))),(product ( the Object-Kind of (N) * the ValuesF of (N)))):]
[: the InstructionsF of (N),K108((product ( the Object-Kind of (N) * the ValuesF of (N))),(product ( the Object-Kind of (N) * the ValuesF of (N)))):] is Relation-like set
bool [: the InstructionsF of (N),K108((product ( the Object-Kind of (N) * the ValuesF of (N))),(product ( the Object-Kind of (N) * the ValuesF of (N)))):] is set
the of (N) . s is Relation-like Function-like Element of K108((product ( the Object-Kind of (N) * the ValuesF of (N))),(product ( the Object-Kind of (N) * the ValuesF of (N))))
( the of (N) . s) . P is set

bool is set

product (() * ()) is non empty functional with_common_domain product-like set
id (product (() * ())) is non empty Relation-like product (() * ()) -defined product (() * ()) -valued Function-like one-to-one total V21( product (() * ()), product (() * ())) Function-yielding V35() Element of bool [:(product (() * ())),(product (() * ())):]
[:(product (() * ())),(product (() * ())):] is Relation-like set
bool [:(product (() * ())),(product (() * ())):] is set

{s} is non empty trivial finite 1 -element countable set
{s} --> (id (product (() * ()))) is non empty Relation-like non-empty non empty-yielding {s} -defined {(id (product (() * ())))} -valued Function-like constant total V21({s},{(id (product (() * ())))}) Function-yielding V35() finite countable V120() Element of bool [:{s},{(id (product (() * ())))}:]

[:{s},{(id (product (() * ())))}:] is Relation-like finite countable set
bool [:{s},{(id (product (() * ())))}:] is finite V40() countable set
(s .--> (id (product (() * ())))) . s is Relation-like Function-like set
s2 is non empty Relation-like the carrier of (N) -defined Function-like the_Values_of (N) -compatible total V120() Element of product ()
(id (product (() * ()))) . s2 is Relation-like Function-like set
N is non empty non with_non-empty_elements set
(N) is non empty trivial finite 1 -element with_non-empty_values (N) (N) (N)
the Object-Kind of (N) is non empty Relation-like the carrier of (N) -defined N -valued Function-like total V21( the carrier of (N),N) finite countable V120() Element of bool [: the carrier of (N),N:]
the carrier of (N) is non empty trivial finite 1 -element countable set
[: the carrier of (N),N:] is Relation-like set
bool [: the carrier of (N),N:] is set
the ValuesF of (N) is non empty Relation-like N -defined Function-like total set

bool is set

IC is V56((N)) Element of the carrier of (N)
the ZeroF of (N) is Element of the carrier of (N)
Values () is non empty set
the_Values_of (N) is non empty Relation-like non-empty non empty-yielding the carrier of (N) -defined Function-like total V120() set
the Object-Kind of (N) * the ValuesF of (N) is non empty Relation-like the carrier of (N) -defined Function-like total finite countable V120() set
() . () is non empty set
() . 0 is set

(() * ()) . 0 is set

() . (() . 0) is set
() . 0 is set
N is non empty non with_non-empty_elements set
(N) is non empty trivial finite 1 -element with_non-empty_values IC-Ins-separated (N) (N) (N)
N is non empty non with_non-empty_elements set
(N) is non empty trivial finite 1 -element with_non-empty_values IC-Ins-separated (N) (N) (N)
N is non empty non with_non-empty_elements set
S is non empty with_non-empty_values IC-Ins-separated (N)

the carrier of S is non empty set

the Object-Kind of S is non empty Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]
[: the carrier of S,N:] is Relation-like set
bool [: the carrier of S,N:] is set
the ValuesF of S is non empty Relation-like N -defined Function-like total set
the Object-Kind of S * the ValuesF of S is non empty Relation-like the carrier of S -defined Function-like total set

IC is V56(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
s . () is set
P /. (IC s) is Element of the InstructionsF of S
N is non empty non with_non-empty_elements set
S is non empty with_non-empty_values IC-Ins-separated (N)
the carrier of S is non empty set

the Object-Kind of S is non empty Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]
[: the carrier of S,N:] is Relation-like set
bool [: the carrier of S,N:] is set
the ValuesF of S is non empty Relation-like N -defined Function-like total set
the Object-Kind of S * the ValuesF of S is non empty Relation-like the carrier of S -defined Function-like total set

(N,S,s,P) is Element of the InstructionsF of S

IC is V56(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
P . () is set
s /. (IC P) is Element of the InstructionsF of S
(N,S,(N,S,s,P),P) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
product ( the Object-Kind of S * the ValuesF of S) is functional with_common_domain product-like set
K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))) is non empty functional set
the of S is non empty Relation-like the InstructionsF of S -defined K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))) -valued Function-like total V21( the InstructionsF of S,K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))) Function-yielding V35() Element of bool [: the InstructionsF of S,K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))):]
[: the InstructionsF of S,K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))):] is Relation-like set
bool [: the InstructionsF of S,K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))):] is set
the of S . (N,S,s,P) is Relation-like Function-like Element of K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))
( the of S . (N,S,s,P)) . P is set
N is non empty non with_non-empty_elements set
S is non empty with_non-empty_values IC-Ins-separated (N)

the carrier of S is non empty set

the Object-Kind of S is non empty Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]
[: the carrier of S,N:] is Relation-like set
bool [: the carrier of S,N:] is set
the ValuesF of S is non empty Relation-like N -defined Function-like total set
the Object-Kind of S * the ValuesF of S is non empty Relation-like the carrier of S -defined Function-like total set

[:NAT,():] is non empty non trivial non empty-membered Relation-like non finite set
bool [:NAT,():] is non empty non trivial non empty-membered non finite set

l . (l + 1) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total Element of product ()

(N,S,(l . l),P) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,P,(l . l)) is Element of the InstructionsF of S

IC is V56(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
(l . l) . () is set
P /. (IC (l . l)) is Element of the InstructionsF of S
(N,S,(N,S,P,(l . l)),(l . l)) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
product ( the Object-Kind of S * the ValuesF of S) is functional with_common_domain product-like set
K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))) is non empty functional set
the of S is non empty Relation-like the InstructionsF of S -defined K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))) -valued Function-like total V21( the InstructionsF of S,K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))) Function-yielding V35() Element of bool [: the InstructionsF of S,K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))):]
[: the InstructionsF of S,K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))):] is Relation-like set
bool [: the InstructionsF of S,K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))):] is set
the of S . (N,S,P,(l . l)) is Relation-like Function-like Element of K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))
( the of S . (N,S,P,(l . l))) . (l . l) is set
down (N,S,(l . l),P) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total Element of product ()

l . (k2 + 1) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total Element of product ()

(N,S,(l . k2),P) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,P,(l . k2)) is Element of the InstructionsF of S

IC is V56(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
(l . k2) . () is set
P /. (IC (l . k2)) is Element of the InstructionsF of S
(N,S,(N,S,P,(l . k2)),(l . k2)) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
product ( the Object-Kind of S * the ValuesF of S) is functional with_common_domain product-like set
K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))) is non empty functional set
the of S is non empty Relation-like the InstructionsF of S -defined K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))) -valued Function-like total V21( the InstructionsF of S,K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))) Function-yielding V35() Element of bool [: the InstructionsF of S,K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))):]
[: the InstructionsF of S,K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))):] is Relation-like set
bool [: the InstructionsF of S,K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))):] is set
the of S . (N,S,P,(l . k2)) is Relation-like Function-like Element of K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))
( the of S . (N,S,P,(l . k2))) . (l . k2) is set
down (N,S,(l . k2),P) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total Element of product ()

l . (k2 + 1) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total Element of product ()

(N,S,(l . k2),P) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,P,(l . k2)) is Element of the InstructionsF of S

IC is V56(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
(l . k2) . () is set
P /. (IC (l . k2)) is Element of the InstructionsF of S
(N,S,(N,S,P,(l . k2)),(l . k2)) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
product ( the Object-Kind of S * the ValuesF of S) is functional with_common_domain product-like set
K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))) is non empty functional set
the of S is non empty Relation-like the InstructionsF of S -defined K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))) -valued Function-like total V21( the InstructionsF of S,K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))) Function-yielding V35() Element of bool [: the InstructionsF of S,K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))):]
[: the InstructionsF of S,K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))):] is Relation-like set
bool [: the InstructionsF of S,K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))):] is set
the of S . (N,S,P,(l . k2)) is Relation-like Function-like Element of K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))
( the of S . (N,S,P,(l . k2))) . (l . k2) is set
down (N,S,(l . k2),P) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total Element of product ()
N is non empty non with_non-empty_elements set
S is non empty with_non-empty_values IC-Ins-separated (N) (N)

the carrier of S is non empty set

the Object-Kind of S is non empty Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]
[: the carrier of S,N:] is Relation-like set
bool [: the carrier of S,N:] is set
the ValuesF of S is non empty Relation-like N -defined Function-like total set
the Object-Kind of S * the ValuesF of S is non empty Relation-like the carrier of S -defined Function-like total set
N is non empty non with_non-empty_elements set
S is non empty with_non-empty_values IC-Ins-separated (N)

the carrier of S is non empty set

the Object-Kind of S is non empty Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]
[: the carrier of S,N:] is Relation-like set
bool [: the carrier of S,N:] is set
the ValuesF of S is non empty Relation-like N -defined Function-like total set
the Object-Kind of S * the ValuesF of S is non empty Relation-like the carrier of S -defined Function-like total set

(N,S,P,s,0) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set

[:NAT,():] is non empty non trivial non empty-membered Relation-like non finite set
bool [:NAT,():] is non empty non trivial non empty-membered non finite set

N is non empty non with_non-empty_elements set
S is non empty with_non-empty_values IC-Ins-separated (N)

the carrier of S is non empty set

the Object-Kind of S is non empty Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]
[: the carrier of S,N:] is Relation-like set
bool [: the carrier of S,N:] is set
the ValuesF of S is non empty Relation-like N -defined Function-like total set
the Object-Kind of S * the ValuesF of S is non empty Relation-like the carrier of S -defined Function-like total set

(N,S,P,s,0) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
N is non empty non with_non-empty_elements set
S is non empty with_non-empty_values IC-Ins-separated (N)

the carrier of S is non empty set

the Object-Kind of S is non empty Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]
[: the carrier of S,N:] is Relation-like set
bool [: the carrier of S,N:] is set
the ValuesF of S is non empty Relation-like N -defined Function-like total set
the Object-Kind of S * the ValuesF of S is non empty Relation-like the carrier of S -defined Function-like total set

(N,S,P,s,(k + 1)) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,P,s,k) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,(N,S,P,s,k),P) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,P,(N,S,P,s,k)) is Element of the InstructionsF of S

IC is V56(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
(N,S,P,s,k) . () is set
P /. (IC (N,S,P,s,k)) is Element of the InstructionsF of S
(N,S,(N,S,P,(N,S,P,s,k)),(N,S,P,s,k)) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
product ( the Object-Kind of S * the ValuesF of S) is functional with_common_domain product-like set
K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))) is non empty functional set
the of S is non empty Relation-like the InstructionsF of S -defined K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))) -valued Function-like total V21( the InstructionsF of S,K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))) Function-yielding V35() Element of bool [: the InstructionsF of S,K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))):]
[: the InstructionsF of S,K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))):] is Relation-like set
bool [: the InstructionsF of S,K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))):] is set
the of S . (N,S,P,(N,S,P,s,k)) is Relation-like Function-like Element of K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))
( the of S . (N,S,P,(N,S,P,s,k))) . (N,S,P,s,k) is set

[:NAT,():] is non empty non trivial non empty-membered Relation-like non finite set
bool [:NAT,():] is non empty non trivial non empty-membered non finite set

(N,S,P,s2,(k + 1)) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set

l . (k + 1) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total Element of product ()

(N,S,P,s2,k) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set

l . (l + 1) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total Element of product ()

(N,S,(l . l),P) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,P,(l . l)) is Element of the InstructionsF of S

(l . l) . () is set
P /. (IC (l . l)) is Element of the InstructionsF of S
(N,S,(N,S,P,(l . l)),(l . l)) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
the of S . (N,S,P,(l . l)) is Relation-like Function-like Element of K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))
( the of S . (N,S,P,(l . l))) . (l . l) is set
down (N,S,(l . l),P) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total Element of product ()

l . (l + 1) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total Element of product ()

(N,S,(l . l),P) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,P,(l . l)) is Element of the InstructionsF of S

(l . l) . () is set
P /. (IC (l . l)) is Element of the InstructionsF of S
(N,S,(N,S,P,(l . l)),(l . l)) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
the of S . (N,S,P,(l . l)) is Relation-like Function-like Element of K108((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))
( the of S . (N,S,P,(l . l))) . (l . l) is set
down (N,S,(l . l),P) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total Element of product ()

S is non empty non with_non-empty_elements set
P is non empty with_non-empty_values IC-Ins-separated (S)
the carrier of P is non empty set

the Object-Kind of P is non empty Relation-like the carrier of P -defined S -valued Function-like total V21( the carrier of P,S) Element of bool [: the carrier of P,S:]
[: the carrier of P,S:] is Relation-like set
bool [: the carrier of P,S:] is set
the ValuesF of P is non empty Relation-like S -defined Function-like total set
the Object-Kind of P * the ValuesF of P is non empty Relation-like the carrier of P -defined Function-like total set

(S,P,k,s,N) is non empty Relation-like the carrier of P -defined Function-like the_Values_of P -compatible total set

(S,P,k,s,(N + s2)) is non empty Relation-like the carrier of P -defined Function-like the_Values_of P -compatible total set
(S,P,k,(S,P,k,s,N),s2) is non empty Relation-like the carrier of P -defined Function-like the_Values_of P -compatible total set

(S,P,k,s,(N + (s2 + 1))) is non empty Relation-like the carrier of P -defined Function-like the_Values_of P -compatible total set

(S,P,k,s,((N + s2) + 1)) is non empty Relation-like the carrier of P -defined Function-like the_Values_of P -compatible total set
(S,P,(S,P,k,s,(N + s2)),k) is non empty Relation-like the carrier of P -defined Function-like the_Values_of P -compatible total set
(S,P,k,(S,P,k,s,(N + s2))) is Element of the InstructionsF of P
IC (S,P,k,s,(N + s2)) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
IC is V56(P) Element of the carrier of P
the ZeroF of P is Element of the carrier of P
(S,P,k,s,(N + s2)) . () is set
k /. (IC (S,P,k,s,(N + s2))) is Element of the InstructionsF of P
(S,P,(S,P,k,(S,P,k,s,(N + s2))),(S,P,k,s,(N + s2))) is non empty Relation-like the carrier of P -defined Function-like the_Values_of P -compatible total set
product ( the Object-Kind of P * the ValuesF of P) is functional with_common_domain product-like set
K108((product ( the Object-Kind of P * the ValuesF of P)),(product ( the Object-Kind of P * the ValuesF of P))) is non empty functional set
the of P is non empty Relation-like the InstructionsF of P -defined K108((product ( the Object-Kind of P * the ValuesF of P)),(product ( the Object-Kind of P * the ValuesF of P))) -valued Function-like total V21( the InstructionsF of P,K108((product ( the Object-Kind of P * the ValuesF of P)),(product ( the Object-Kind of P * the ValuesF of P)))) Function-yielding V35() Element of bool [: the InstructionsF of P,K108((product ( the Object-Kind of P * the ValuesF of P)),(product ( the Object-Kind of P * the ValuesF of P))):]
[: the InstructionsF of P,K108((product ( the Object-Kind of P * the ValuesF of P)),(product ( the Object-Kind of P * the ValuesF of P))):] is Relation-like set
bool [: the InstructionsF of P,K108((product ( the Object-Kind of P * the ValuesF of P)),(product ( the Object-Kind of P * the ValuesF of P))):] is set
the of P . (S,P,k,(S,P,k,s,(N + s2))) is Relation-like Function-like Element of K108((product ( the Object-Kind of P * the ValuesF of P)),(product ( the Object-Kind of P * the ValuesF of P)))
( the of P . (S,P,k,(S,P,k,s,(N + s2)))) . (S,P,k,s,(N + s2)) is set
(S,P,k,(S,P,k,s,N),(s2 + 1)) is non empty Relation-like the carrier of P -defined Function-like the_Values_of P -compatible total set

(S,P,k,s,(N + 0)) is non empty Relation-like the carrier of P -defined Function-like the_Values_of P -compatible total set
(S,P,k,(S,P,k,s,N),0) is non empty Relation-like the carrier of P -defined Function-like the_Values_of P -compatible total set

k is non empty non with_non-empty_elements set
s2 is non empty with_non-empty_values IC-Ins-separated (k) (k)

the carrier of s2 is non empty set

the Object-Kind of s2 is non empty Relation-like the carrier of s2 -defined k -valued Function-like total V21( the carrier of s2,k) Element of bool [: the carrier of s2,k:]
[: the carrier of s2,k:] is Relation-like set
bool [: the carrier of s2,k:] is set
the ValuesF of s2 is non empty Relation-like k -defined Function-like total set
the Object-Kind of s2 * the ValuesF of s2 is non empty Relation-like the carrier of s2 -defined Function-like total set
halt s2 is (k,s2) Element of the InstructionsF of s2
halt the InstructionsF of s2 is ins-loc-free Element of the InstructionsF of s2

(k,s2,l,l,N) is non empty Relation-like the carrier of s2 -defined Function-like the_Values_of s2 -compatible total set
(k,s2,l,(k,s2,l,l,N)) is Element of the InstructionsF of s2

IC is V56(s2) Element of the carrier of s2
the ZeroF of s2 is Element of the carrier of s2
(k,s2,l,l,N) . () is set
l /. (IC (k,s2,l,l,N)) is Element of the InstructionsF of s2
(k,s2,l,l,S) is non empty Relation-like the carrier of s2 -defined Function-like the_Values_of s2 -compatible total set

(k,s2,l,l,(N + l)) is non empty Relation-like the carrier of s2 -defined Function-like the_Values_of s2 -compatible total set

(k,s2,l,l,(N + (l + 1))) is non empty Relation-like the carrier of s2 -defined Function-like the_Values_of s2 -compatible total set

(k,s2,l,l,((N + l) + 1)) is non empty Relation-like the carrier of s2 -defined Function-like the_Values_of s2 -compatible total set
(k,s2,(k,s2,l,l,(N + l)),l) is non empty Relation-like the carrier of s2 -defined Function-like the_Values_of s2 -compatible total set
(k,s2,l,(k,s2,l,l,(N + l))) is Element of the InstructionsF of s2
IC (k,s2,l,l,(N + l)) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(k,s2,l,l,(N + l)) . () is set
l /. (IC (k,s2,l,l,(N + l))) is Element of the InstructionsF of s2
(k,s2,(k,s2,l,(k,s2,l,l,(N + l))),(k,s2,l,l,(N + l))) is non empty Relation-like the carrier of s2 -defined Function-like the_Values_of s2 -compatible total set
product ( the Object-Kind of s2 * the ValuesF of s2) is functional with_common_domain product-like set
K108((product ( the Object-Kind of s2 * the ValuesF of s2)),(product ( the Object-Kind of s2 * the ValuesF of s2))) is non empty functional set
the of s2 is non empty Relation-like the InstructionsF of s2 -defined K108((product ( the Object-Kind of s2 * the ValuesF of s2)),(product ( the Object-Kind of s2 * the ValuesF of s2))) -valued Function-like total V21( the InstructionsF of s2,K108((product ( the Object-Kind of s2 * the ValuesF of s2)),(product ( the Object-Kind of s2 * the ValuesF of s2)))) Function-yielding V35() Element of bool [: the InstructionsF of s2,K108((product ( the Object-Kind of s2 * the ValuesF of s2)),(product ( the Object-Kind of s2 * the ValuesF of s2))):]
[: the InstructionsF of s2,K108((product ( the Object-Kind of s2 * the ValuesF of s2)),(product ( the Object-Kind of s2 * the ValuesF of s2))):] is Relation-like set
bool [: the InstructionsF of s2,K108((product ( the Object-Kind of s2 * the ValuesF of s2)),(product ( the Object-Kind of s2 * the ValuesF of s2))):] is set
the of s2 . (k,s2,l,(k,s2,l,l,(N + l))) is Relation-like Function-like Element of K108((product ( the Object-Kind of s2 * the ValuesF of s2)),(product ( the Object-Kind of s2 * the ValuesF of s2)))
( the of s2 . (k,s2,l,(k,s2,l,l,(N + l)))) . (k,s2,l,l,(N + l)) is set

(k,s2,l,l,(N + 0)) is non empty Relation-like the carrier of s2 -defined Function-like the_Values_of s2 -compatible total set
N is non empty non with_non-empty_elements set
S is non empty with_non-empty_values IC-Ins-separated (N) (N)

the carrier of S is non empty set

the Object-Kind of S is non empty Relation-like the carrier of S -defined N -valued Function-like total V21( the carrier of S,N) Element of bool [: the carrier of S,N:]
[: the carrier of S,N:] is Relation-like set
bool [: the carrier of S,N:] is set
the ValuesF of S is non empty Relation-like N -defined Function-like total set
the Object-Kind of S * the ValuesF of S is non empty Relation-like the carrier of S -defined Function-like total set

halt S is (N,S) Element of the InstructionsF of S
halt the InstructionsF of S is ins-loc-free Element of the InstructionsF of S

(N,S,P,k) is Element of the InstructionsF of S

IC is V56(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
k . () is set
P /. (IC k) is Element of the InstructionsF of S

(N,S,P,s2) is Element of the InstructionsF of S