REAL is non empty non with_non-empty_elements set
NAT is non empty non trivial non with_non-empty_elements non empty-membered epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal countable denumerable Element of bool REAL
bool REAL is set
omega is non empty non trivial non with_non-empty_elements non empty-membered epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal countable denumerable 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
COMPLEX is set
RAT is set
INT is set
{} is empty trivial Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional ext-real epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-yielding V35() finite finite-yielding V40() cardinal {} -element V44() V45() V46() Cardinal-yielding countable V84() V85() V86() V119() V120() set
2 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
ExtREAL is set
1 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
3 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
0 is empty trivial Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional ext-real epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-yielding V35() finite finite-yielding V40() cardinal {} -element V44() V45() V46() Cardinal-yielding countable V84() V85() V86() V119() V120() Element of NAT
N is non empty non with_non-empty_elements set
{0} is non empty trivial functional finite V40() 1 -element with_common_domain countable Element of bool NAT
[0,{},{}] is V7() V8() set
[0,{}] is non empty V7() set
{0,{}} is non empty functional finite V40() countable set
{0} is non empty trivial functional finite V40() 1 -element with_common_domain countable set
{{0,{}},{0}} is non empty with_non-empty_elements non empty-membered finite V40() countable set
[[0,{}],{}] is non empty V7() set
{[0,{}],{}} is non empty finite countable set
{[0,{}]} is non empty trivial with_non-empty_elements non empty-membered Relation-like Function-like constant finite 1 -element countable V120() set
{{[0,{}],{}},{[0,{}]}} is non empty with_non-empty_elements non empty-membered finite V40() countable set
{[0,{},{}]} is non empty trivial Relation-like finite 1 -element countable standard-ins homogeneous J/A-independent V132() set
0 .--> 0 is trivial Relation-like NAT -defined {0} -defined NAT -valued Function-like one-to-one constant Function-yielding V35() finite Cardinal-yielding countable V120() set
{0} --> 0 is non empty Relation-like {0} -defined NAT -valued {0} -valued Function-like constant total V21({0},{0}) Function-yielding V35() finite Cardinal-yielding countable V120() Element of bool [:{0},{0}:]
[:{0},{0}:] is Relation-like finite countable set
bool [:{0},{0}:] is finite V40() countable set
N --> NAT is non empty Relation-like non-empty non empty-yielding N -defined {NAT} -valued Function-like constant total V21(N,{NAT}) Cardinal-yielding Element of bool [:N,{NAT}:]
{NAT} is non empty trivial with_non-empty_elements non empty-membered finite 1 -element countable set
[:N,{NAT}:] is Relation-like set
bool [:N,{NAT}:] is set
(0 .--> 0) * (N --> NAT) is Relation-like non-empty NAT -defined {NAT} -valued Function-like finite countable V120() set
product ((0 .--> 0) * (N --> NAT)) is non empty functional with_common_domain product-like set
id (product ((0 .--> 0) * (N --> NAT))) is non empty Relation-like product ((0 .--> 0) * (N --> NAT)) -defined product ((0 .--> 0) * (N --> NAT)) -valued Function-like one-to-one total V21( product ((0 .--> 0) * (N --> NAT)), product ((0 .--> 0) * (N --> NAT))) Function-yielding V35() Element of bool [:(product ((0 .--> 0) * (N --> NAT))),(product ((0 .--> 0) * (N --> NAT))):]
[:(product ((0 .--> 0) * (N --> NAT))),(product ((0 .--> 0) * (N --> NAT))):] is Relation-like set
bool [:(product ((0 .--> 0) * (N --> NAT))),(product ((0 .--> 0) * (N --> NAT))):] is set
[0,{},{}] .--> (id (product ((0 .--> 0) * (N --> NAT)))) is trivial Relation-like {[0,{},{}]} -defined Function-like one-to-one constant Function-yielding V35() finite countable V120() set
{[0,{},{}]} --> (id (product ((0 .--> 0) * (N --> NAT)))) is non empty Relation-like non-empty non empty-yielding {[0,{},{}]} -defined {(id (product ((0 .--> 0) * (N --> NAT))))} -valued Function-like constant total V21({[0,{},{}]},{(id (product ((0 .--> 0) * (N --> NAT))))}) Function-yielding V35() finite countable V120() Element of bool [:{[0,{},{}]},{(id (product ((0 .--> 0) * (N --> NAT))))}:]
{(id (product ((0 .--> 0) * (N --> NAT))))} is non empty trivial with_non-empty_elements non empty-membered functional finite 1 -element with_common_domain countable set
[:{[0,{},{}]},{(id (product ((0 .--> 0) * (N --> NAT))))}:] is Relation-like finite countable set
bool [:{[0,{},{}]},{(id (product ((0 .--> 0) * (N --> NAT))))}:] is finite V40() countable set
proj1 (0 .--> 0) is trivial finite countable set
proj2 (0 .--> 0) is trivial finite countable set
[:{0},N:] is Relation-like set
bool [:{0},N:] is set
k is non empty Relation-like {0} -defined N -valued Function-like total V21({0},N) finite countable V120() Element of bool [:{0},N:]
(N --> NAT) * k is non empty Relation-like non-empty non empty-yielding {0} -defined {NAT} -valued Function-like total V21({0},{NAT}) finite countable V120() Element of bool [:{0},{NAT}:]
[:{0},{NAT}:] is Relation-like finite countable set
bool [:{0},{NAT}:] is finite V40() countable set
product ((N --> NAT) * k) is non empty functional with_common_domain product-like set
K108((product ((N --> NAT) * k)),(product ((N --> NAT) * k))) is non empty functional set
[:{[0,{},{}]},K108((product ((N --> NAT) * k)),(product ((N --> NAT) * k))):] is Relation-like set
bool [:{[0,{},{}]},K108((product ((N --> NAT) * k)),(product ((N --> NAT) * k))):] is set
id (product ((N --> NAT) * k)) is non empty Relation-like product ((N --> NAT) * k) -defined product ((N --> NAT) * k) -valued Function-like one-to-one total V21( product ((N --> NAT) * k), product ((N --> NAT) * k)) Function-yielding V35() Element of bool [:(product ((N --> NAT) * k)),(product ((N --> NAT) * k)):]
[:(product ((N --> NAT) * k)),(product ((N --> NAT) * k)):] is Relation-like set
bool [:(product ((N --> NAT) * k)),(product ((N --> NAT) * k)):] is set
{[0,{},{}]} --> (id (product ((N --> NAT) * k))) is non empty Relation-like non-empty non empty-yielding {[0,{},{}]} -defined {(id (product ((N --> NAT) * k)))} -valued Function-like constant total V21({[0,{},{}]},{(id (product ((N --> NAT) * k)))}) Function-yielding V35() finite countable V120() Element of bool [:{[0,{},{}]},{(id (product ((N --> NAT) * k)))}:]
{(id (product ((N --> NAT) * k)))} is non empty trivial with_non-empty_elements non empty-membered functional finite 1 -element with_common_domain countable set
[:{[0,{},{}]},{(id (product ((N --> NAT) * k)))}:] is Relation-like finite countable set
bool [:{[0,{},{}]},{(id (product ((N --> NAT) * k)))}:] is finite V40() countable set
s2 is Relation-like Function-like finite countable V120() Element of {0}
l is non empty Relation-like {[0,{},{}]} -defined K108((product ((N --> NAT) * k)),(product ((N --> NAT) * k))) -valued Function-like total V21({[0,{},{}]},K108((product ((N --> NAT) * k)),(product ((N --> NAT) * k)))) Function-yielding V35() finite countable V120() Element of bool [:{[0,{},{}]},K108((product ((N --> NAT) * k)),(product ((N --> NAT) * k))):]
(N,{0},s2,{[0,{},{}]},k,(N --> NAT),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 InstructionsF of l is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
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 InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() 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 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 InstructionsF of P is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
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 (the_Values_of (N)) is non empty set
(the_Values_of (N)) . S is set
the Object-Kind of (N) . S is set
proj1 the ValuesF of (N) is non empty set
N --> NAT is non empty Relation-like non-empty non empty-yielding N -defined {NAT} -valued Function-like constant total V21(N,{NAT}) Cardinal-yielding Element of bool [:N,{NAT}:]
[:N,{NAT}:] is Relation-like set
bool [:N,{NAT}:] 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 InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
the carrier of S is set
the_Values_of S is Relation-like non-empty the carrier of S -defined Function-like total 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)))
s is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
( the of S . P) . s is set
product (the_Values_of S) is non empty functional with_common_domain product-like set
k is Relation-like Function-like set
proj1 k is set
proj2 k is set
s2 is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total Element of product (the_Values_of S)
( the of S . P) . s2 is set
N is non empty non with_non-empty_elements set
S is with_non-empty_values (N)
the InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
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)
N --> NAT is non empty Relation-like non-empty non empty-yielding N -defined {NAT} -valued Function-like constant total V21(N,{NAT}) Cardinal-yielding Element of bool [:N,{NAT}:]
[:N,{NAT}:] is Relation-like set
bool [:N,{NAT}:] is set
(0 .--> 0) * (N --> NAT) is Relation-like non-empty NAT -defined {NAT} -valued Function-like finite countable 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) 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 (the_Values_of (N)) is non empty functional with_common_domain product-like set
product ((0 .--> 0) * (N --> NAT)) is non empty functional with_common_domain product-like set
id (product ((0 .--> 0) * (N --> NAT))) is non empty Relation-like product ((0 .--> 0) * (N --> NAT)) -defined product ((0 .--> 0) * (N --> NAT)) -valued Function-like one-to-one total V21( product ((0 .--> 0) * (N --> NAT)), product ((0 .--> 0) * (N --> NAT))) Function-yielding V35() Element of bool [:(product ((0 .--> 0) * (N --> NAT))),(product ((0 .--> 0) * (N --> NAT))):]
[:(product ((0 .--> 0) * (N --> NAT))),(product ((0 .--> 0) * (N --> NAT))):] is Relation-like set
bool [:(product ((0 .--> 0) * (N --> NAT))),(product ((0 .--> 0) * (N --> NAT))):] is set
(halt (N)) .--> (id (product ((0 .--> 0) * (N --> NAT)))) 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 ((0 .--> 0) * (N --> NAT)))) is non empty Relation-like non-empty non empty-yielding {(halt (N))} -defined {(id (product ((0 .--> 0) * (N --> NAT))))} -valued Function-like constant total V21({(halt (N))},{(id (product ((0 .--> 0) * (N --> NAT))))}) Function-yielding V35() finite countable V120() Element of bool [:{(halt (N))},{(id (product ((0 .--> 0) * (N --> NAT))))}:]
{(id (product ((0 .--> 0) * (N --> NAT))))} is non empty trivial with_non-empty_elements non empty-membered functional finite 1 -element with_common_domain countable set
[:{(halt (N))},{(id (product ((0 .--> 0) * (N --> NAT))))}:] is Relation-like finite countable set
bool [:{(halt (N))},{(id (product ((0 .--> 0) * (N --> NAT))))}:] is finite V40() countable set
((halt (N)) .--> (id (product ((0 .--> 0) * (N --> NAT))))) . (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 (the_Values_of (N))
(id (product ((0 .--> 0) * (N --> NAT)))) . 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
the InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
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)
the InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() 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 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
N --> NAT is non empty Relation-like non-empty non empty-yielding N -defined {NAT} -valued Function-like constant total V21(N,{NAT}) Cardinal-yielding Element of bool [:N,{NAT}:]
[:N,{NAT}:] is Relation-like set
bool [:N,{NAT}:] is set
(0 .--> 0) * (N --> NAT) is Relation-like non-empty NAT -defined {NAT} -valued Function-like finite countable V120() set
product (the_Values_of (N)) is non empty functional with_common_domain product-like set
product ((0 .--> 0) * (N --> NAT)) is non empty functional with_common_domain product-like set
id (product ((0 .--> 0) * (N --> NAT))) is non empty Relation-like product ((0 .--> 0) * (N --> NAT)) -defined product ((0 .--> 0) * (N --> NAT)) -valued Function-like one-to-one total V21( product ((0 .--> 0) * (N --> NAT)), product ((0 .--> 0) * (N --> NAT))) Function-yielding V35() Element of bool [:(product ((0 .--> 0) * (N --> NAT))),(product ((0 .--> 0) * (N --> NAT))):]
[:(product ((0 .--> 0) * (N --> NAT))),(product ((0 .--> 0) * (N --> NAT))):] is Relation-like set
bool [:(product ((0 .--> 0) * (N --> NAT))),(product ((0 .--> 0) * (N --> NAT))):] is set
s .--> (id (product ((0 .--> 0) * (N --> NAT)))) is trivial Relation-like the InstructionsF of (N) -defined {s} -defined Function-like one-to-one constant Function-yielding V35() finite countable V120() set
{s} is non empty trivial finite 1 -element countable set
{s} --> (id (product ((0 .--> 0) * (N --> NAT)))) is non empty Relation-like non-empty non empty-yielding {s} -defined {(id (product ((0 .--> 0) * (N --> NAT))))} -valued Function-like constant total V21({s},{(id (product ((0 .--> 0) * (N --> NAT))))}) Function-yielding V35() finite countable V120() Element of bool [:{s},{(id (product ((0 .--> 0) * (N --> NAT))))}:]
{(id (product ((0 .--> 0) * (N --> NAT))))} is non empty trivial with_non-empty_elements non empty-membered functional finite 1 -element with_common_domain countable set
[:{s},{(id (product ((0 .--> 0) * (N --> NAT))))}:] is Relation-like finite countable set
bool [:{s},{(id (product ((0 .--> 0) * (N --> NAT))))}:] is finite V40() countable set
(s .--> (id (product ((0 .--> 0) * (N --> NAT))))) . 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 (the_Values_of (N))
(id (product ((0 .--> 0) * (N --> NAT)))) . 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
N --> NAT is non empty Relation-like non-empty non empty-yielding N -defined {NAT} -valued Function-like constant total V21(N,{NAT}) Cardinal-yielding Element of bool [:N,{NAT}:]
[:N,{NAT}:] is Relation-like set
bool [:N,{NAT}:] is set
proj1 (0 .--> 0) is trivial finite countable set
IC is V56((N)) Element of the carrier of (N)
the ZeroF of (N) is Element of the carrier of (N)
Values (IC ) 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
(the_Values_of (N)) . (IC ) is non empty set
(the_Values_of (N)) . 0 is set
(0 .--> 0) * (N --> NAT) is Relation-like non-empty NAT -defined {NAT} -valued Function-like finite countable V120() set
((0 .--> 0) * (N --> NAT)) . 0 is set
(0 .--> 0) . 0 is Relation-like Function-like set
(N --> NAT) . ((0 .--> 0) . 0) is set
(N --> NAT) . 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 InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
the carrier of S is non empty set
the_Values_of S is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total 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
P is Relation-like the InstructionsF of S -valued Function-like set
s is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
IC s is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
IC is V56(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
s . (IC ) 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_Values_of S is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total 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
the InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
s is Relation-like the InstructionsF of S -valued Function-like set
P is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,s,P) is Element of the InstructionsF of S
IC P is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
IC is V56(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
P . (IC ) 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 InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
the carrier of S is non empty set
the_Values_of S is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total 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
P is Relation-like NAT -defined the InstructionsF of S -valued Function-like set
product (the_Values_of S) is non empty functional with_common_domain product-like set
[:NAT,(product (the_Values_of S)):] is non empty non trivial non empty-membered Relation-like non finite set
bool [:NAT,(product (the_Values_of S)):] is non empty non trivial non empty-membered non finite set
k is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() set
s is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
s2 is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total Element of product (the_Values_of S)
l is non empty Relation-like NAT -defined product (the_Values_of S) -valued Function-like total V21( NAT , product (the_Values_of S)) Function-yielding V35() Element of bool [:NAT,(product (the_Values_of S)):]
l . 0 is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total Element of product (the_Values_of S)
l . k is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total Element of product (the_Values_of S)
l is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() set
l + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
l . (l + 1) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total Element of product (the_Values_of S)
l . l is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total Element of product (the_Values_of S)
(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 (l . l) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
IC is V56(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
(l . l) . (IC ) 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 (the_Values_of S)
s2 is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
l is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
l is non empty Relation-like NAT -defined product (the_Values_of S) -valued Function-like total V21( NAT , product (the_Values_of S)) Function-yielding V35() Element of bool [:NAT,(product (the_Values_of S)):]
l . k is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total Element of product (the_Values_of S)
l . 0 is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total Element of product (the_Values_of S)
l is non empty Relation-like NAT -defined product (the_Values_of S) -valued Function-like total V21( NAT , product (the_Values_of S)) Function-yielding V35() Element of bool [:NAT,(product (the_Values_of S)):]
l . k is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total Element of product (the_Values_of S)
l . 0 is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total Element of product (the_Values_of S)
s is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total Element of product (the_Values_of S)
k2 is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() set
k2 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
l . (k2 + 1) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total Element of product (the_Values_of S)
l . k2 is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total Element of product (the_Values_of S)
(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 (l . k2) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
IC is V56(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
(l . k2) . (IC ) 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 (the_Values_of S)
k2 is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() set
k2 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
l . (k2 + 1) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total Element of product (the_Values_of S)
l . k2 is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total Element of product (the_Values_of S)
(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 (l . k2) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
IC is V56(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
(l . k2) . (IC ) 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 (the_Values_of S)
N is non empty non with_non-empty_elements set
S is non empty with_non-empty_values IC-Ins-separated (N) (N)
the InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
the carrier of S is non empty set
the_Values_of S is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total 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 InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
the carrier of S is non empty set
the_Values_of S is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total 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
P is Relation-like NAT -defined the InstructionsF of S -valued Function-like set
s is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible 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
product (the_Values_of S) is non empty functional with_common_domain product-like set
[:NAT,(product (the_Values_of S)):] is non empty non trivial non empty-membered Relation-like non finite set
bool [:NAT,(product (the_Values_of S)):] is non empty non trivial non empty-membered non finite set
k is non empty Relation-like NAT -defined product (the_Values_of S) -valued Function-like total V21( NAT , product (the_Values_of S)) Function-yielding V35() Element of bool [:NAT,(product (the_Values_of S)):]
k . 0 is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total Element of product (the_Values_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 InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
the carrier of S is non empty set
the_Values_of S is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total 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
P is Relation-like NAT -defined the InstructionsF of S -valued Function-like set
s is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible 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 InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
the carrier of S is non empty set
the_Values_of S is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total 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
P is Relation-like NAT -defined the InstructionsF of S -valued Function-like set
s is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
k is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() set
k + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(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 (N,S,P,s,k) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
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) . (IC ) 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
product (the_Values_of S) is non empty functional with_common_domain product-like set
[:NAT,(product (the_Values_of S)):] is non empty non trivial non empty-membered Relation-like non finite set
bool [:NAT,(product (the_Values_of S)):] is non empty non trivial non empty-membered non finite set
s2 is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total Element of product (the_Values_of S)
(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 is non empty Relation-like NAT -defined product (the_Values_of S) -valued Function-like total V21( NAT , product (the_Values_of S)) Function-yielding V35() Element of bool [:NAT,(product (the_Values_of S)):]
l . (k + 1) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total Element of product (the_Values_of S)
l . 0 is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total Element of product (the_Values_of S)
(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 is non empty Relation-like NAT -defined product (the_Values_of S) -valued Function-like total V21( NAT , product (the_Values_of S)) Function-yielding V35() Element of bool [:NAT,(product (the_Values_of S)):]
l . k is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total Element of product (the_Values_of S)
l . 0 is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total Element of product (the_Values_of S)
l is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() set
l + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
l . (l + 1) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total Element of product (the_Values_of S)
l . l is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total Element of product (the_Values_of S)
(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 (l . l) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(l . l) . (IC ) 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 (the_Values_of S)
l is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() set
l + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
l . (l + 1) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total Element of product (the_Values_of S)
l . l is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total Element of product (the_Values_of S)
(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 (l . l) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(l . l) . (IC ) 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 (the_Values_of S)
N is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
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_Values_of P is non empty Relation-like non-empty non empty-yielding the carrier of P -defined Function-like total 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
the InstructionsF of P is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
s is non empty Relation-like the carrier of P -defined Function-like the_Values_of P -compatible total set
k is Relation-like NAT -defined the InstructionsF of P -valued Function-like 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
s2 is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
N + s2 is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(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
s2 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
N + (s2 + 1) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(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
(N + s2) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(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)) . (IC ) 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
N + 0 is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(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
N is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
S is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
P is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() set
N + P is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
s is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
N + s is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
k is non empty non with_non-empty_elements set
s2 is non empty with_non-empty_values IC-Ins-separated (k) (k)
the InstructionsF of s2 is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
the carrier of s2 is non empty set
the_Values_of s2 is non empty Relation-like non-empty non empty-yielding the carrier of s2 -defined Function-like total 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
l is Relation-like NAT -defined the InstructionsF of s2 -valued Function-like set
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) 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 (k,s2,l,l,N) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
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) . (IC ) 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
l is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
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 non empty Relation-like the carrier of s2 -defined Function-like the_Values_of s2 -compatible total set
l + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
N + (l + 1) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(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
(N + l) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(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)) . (IC ) 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
N + 0 is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(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 InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
the carrier of S is non empty set
the_Values_of S is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total 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
P is Relation-like NAT -defined the InstructionsF of S -valued Function-like set
s is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible 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
k is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,P,k) is Element of the InstructionsF of S
IC k is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
IC is V56(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
k . (IC ) is set
P /. (IC k) is Element of the InstructionsF of S
s2 is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,P,s2) is Element of the InstructionsF of S
IC s2 is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
s2 . (IC ) is set
P /. (IC s2) is Element of the InstructionsF of S
l is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,l) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
l is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,l) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
proj1 P is set
k is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() 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
IC (N,S,P,s,k) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
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) . (IC ) is set
(N,S,P,(N,S,P,s,k)) is Element of the InstructionsF of S
P /. (IC (N,S,P,s,k)) is Element of the InstructionsF of S
N is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
N + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
S is non empty non with_non-empty_elements set
P is non empty with_non-empty_values IC-Ins-separated (S)
the InstructionsF of P is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
the carrier of P is non empty set
the_Values_of P is non empty Relation-like non-empty non empty-yielding the carrier of P -defined Function-like total 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 is non empty Relation-like NAT -defined the InstructionsF of P -valued Function-like total set
k is non empty Relation-like the carrier of P -defined Function-like the_Values_of P -compatible total set
(S,P,s,k,(N + 1)) is non empty Relation-like the carrier of P -defined Function-like the_Values_of P -compatible total set
(S,P,s,k,N) is non empty Relation-like the carrier of P -defined Function-like the_Values_of P -compatible total set
IC (S,P,s,k,N) 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,s,k,N) . (IC ) is set
s . (IC (S,P,s,k,N)) is Element of the InstructionsF of P
(S,P,(s . (IC (S,P,s,k,N))),(S,P,s,k,N)) 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 . (IC (S,P,s,k,N))) 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 . (IC (S,P,s,k,N)))) . (S,P,s,k,N) is set
proj1 s is non empty set
(S,P,(S,P,s,k,N),s) is non empty Relation-like the carrier of P -defined Function-like the_Values_of P -compatible total set
(S,P,s,(S,P,s,k,N)) is Element of the InstructionsF of P
s /. (IC (S,P,s,k,N)) is Element of the InstructionsF of P
(S,P,(S,P,s,(S,P,s,k,N)),(S,P,s,k,N)) is non empty Relation-like the carrier of P -defined Function-like the_Values_of P -compatible total set
the of P . (S,P,s,(S,P,s,k,N)) 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,s,(S,P,s,k,N))) . (S,P,s,k,N) is 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 InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
the carrier of S is non empty set
the_Values_of S is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total 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
P is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like total set
s is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,P,s) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
k is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,k) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
IC (N,S,P,s,k) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
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) . (IC ) is set
P . (IC (N,S,P,s,k)) is Element of the InstructionsF of S
proj1 P is non empty set
(N,S,P,(N,S,P,s,k)) is Element of the InstructionsF of S
P /. (IC (N,S,P,s,k)) 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) (N)
the InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
the carrier of S is non empty set
the_Values_of S is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total 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
P is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like total set
s is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,P,s) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
k is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,k) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
IC (N,S,P,s,k) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
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) . (IC ) is set
P . (IC (N,S,P,s,k)) is Element of the InstructionsF of S
s2 is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,s2) 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,s2)) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
proj1 P is non empty set
(N,S,P,(N,S,P,s,k)) is Element of the InstructionsF of S
P /. (IC (N,S,P,s,k)) is Element of the InstructionsF of S
l is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() set
s2 + l is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
l is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,(N,S,P,s,s2),l) 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),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 InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
the carrier of S is non empty set
the_Values_of S is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total 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) (N)
the InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
the carrier of S is non empty set
the_Values_of S is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total 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
(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 InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
the carrier of S is non empty set
the_Values_of S is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total 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
P is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(IC ) .--> P is trivial Relation-like the carrier of S -defined {(IC )} -defined NAT -valued Function-like one-to-one constant finite Cardinal-yielding countable V120() set
{(IC )} is non empty trivial finite 1 -element countable set
{(IC )} --> P is non empty Relation-like {(IC )} -defined NAT -valued {P} -valued Function-like constant total V21({(IC )},{P}) finite Cardinal-yielding countable V120() Element of bool [:{(IC )},{P}:]
{P} is non empty trivial finite V40() 1 -element countable set
[:{(IC )},{P}:] is Relation-like finite countable set
bool [:{(IC )},{P}:] is finite V40() countable set
s is Element of the InstructionsF of S
P .--> s is trivial Relation-like NAT -defined {P} -defined the InstructionsF of S -valued Function-like one-to-one constant finite countable V120() set
{P} --> s is non empty Relation-like {P} -defined the InstructionsF of S -valued {s} -valued Function-like constant total V21({P},{s}) finite countable V120() Element of bool [:{P},{s}:]
{s} is non empty trivial finite 1 -element countable set
[:{P},{s}:] is Relation-like finite countable set
bool [:{P},{s}:] is finite V40() countable set
k is Relation-like NAT -defined the InstructionsF of S -valued Function-like set
s2 is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,k,s2) is Element of the InstructionsF of S
IC s2 is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
s2 . (IC ) is set
k /. (IC s2) is Element of the InstructionsF of S
proj1 ((IC ) .--> P) is trivial finite countable set
{(IC )} is non empty trivial finite 1 -element countable Element of bool the carrier of S
bool the carrier of S is set
((IC ) .--> P) . (IC ) is set
proj1 (P .--> s) is trivial finite countable set
{P} is non empty trivial finite V40() 1 -element countable Element of bool NAT
proj1 k is set
k . (IC s2) is set
(P .--> s) . (IC s2) is 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 InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() 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
the carrier of S is non empty set
the_Values_of S is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total 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
P is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
P .--> (halt S) is trivial Relation-like NAT -defined {P} -defined the InstructionsF of S -valued Function-like one-to-one constant finite countable V120() set
{P} is non empty trivial finite V40() 1 -element countable set
{P} --> (halt S) is non empty Relation-like {P} -defined the InstructionsF of S -valued {(halt S)} -valued Function-like constant total V21({P},{(halt S)}) finite countable V120() Element of bool [:{P},{(halt S)}:]
{(halt S)} is non empty trivial finite 1 -element countable set
[:{P},{(halt S)}:] is Relation-like finite countable set
bool [:{P},{(halt S)}:] is finite V40() countable set
s is Relation-like NAT -defined the InstructionsF of S -valued Function-like set
k is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible P -started set
k +* s is Relation-like Function-like set
l is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
l is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like total set
(N,S,l,l,0) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
IC (N,S,l,l,0) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
IC is V56(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
(N,S,l,l,0) . (IC ) is set
proj1 l is non empty set
(N,S,l,(N,S,l,l,0)) is Element of the InstructionsF of S
l /. (IC (N,S,l,l,0)) is Element of the InstructionsF of S
Start-At (P,S) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible finite countable V120() P -started set
(IC ) .--> P is trivial Relation-like the carrier of S -defined {(IC )} -defined NAT -valued Function-like one-to-one constant finite Cardinal-yielding countable V120() set
{(IC )} is non empty trivial finite 1 -element countable set
{(IC )} --> P is non empty Relation-like {(IC )} -defined NAT -valued {P} -valued Function-like constant total V21({(IC )},{P}) finite Cardinal-yielding countable V120() Element of bool [:{(IC )},{P}:]
[:{(IC )},{P}:] is Relation-like finite countable set
bool [:{(IC )},{P}:] is finite V40() countable set
proj1 (P .--> (halt S)) is trivial finite countable set
{P} is non empty trivial finite V40() 1 -element countable Element of bool NAT
proj1 (Start-At (P,S)) is non empty finite countable set
IC l is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
l . (IC ) is set
IC (Start-At (P,S)) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(Start-At (P,S)) . (IC ) is set
(N,S,l,l) is Element of the InstructionsF of S
l /. (IC l) is Element of the InstructionsF of S
l . (IC l) is Element of the InstructionsF of S
(P .--> (halt S)) . (IC l) is set
(N,S,(P .--> (halt S)),l) is Element of the InstructionsF of S
(P .--> (halt S)) /. (IC l) 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) (N)
the InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() 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
the carrier of S is non empty set
the_Values_of S is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total 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
P is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
P .--> (halt S) is trivial Relation-like NAT -defined {P} -defined the InstructionsF of S -valued Function-like one-to-one constant finite countable V120() set
{P} is non empty trivial finite V40() 1 -element countable set
{P} --> (halt S) is non empty Relation-like {P} -defined the InstructionsF of S -valued {(halt S)} -valued Function-like constant total V21({P},{(halt S)}) finite countable V120() Element of bool [:{P},{(halt S)}:]
{(halt S)} is non empty trivial finite 1 -element countable set
[:{P},{(halt S)}:] is Relation-like finite countable set
bool [:{P},{(halt S)}:] is finite V40() countable set
s is Relation-like NAT -defined the InstructionsF of S -valued Function-like set
k is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible P -started set
l is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
Start-At (P,S) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible finite countable V120() P -started set
IC is V56(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
(IC ) .--> P is trivial Relation-like the carrier of S -defined {(IC )} -defined NAT -valued Function-like one-to-one constant finite Cardinal-yielding countable V120() set
{(IC )} is non empty trivial finite 1 -element countable set
{(IC )} --> P is non empty Relation-like {(IC )} -defined NAT -valued {P} -valued Function-like constant total V21({(IC )},{P}) finite Cardinal-yielding countable V120() Element of bool [:{(IC )},{P}:]
[:{(IC )},{P}:] is Relation-like finite countable set
bool [:{(IC )},{P}:] is finite V40() countable set
l is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,s,l,l) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
l + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,s,l,(l + 1)) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,l,s) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,s,l) is Element of the InstructionsF of S
IC l is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
l . (IC ) is set
s /. (IC l) is Element of the InstructionsF of S
(N,S,(N,S,s,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,s,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,s,l)) . l is set
(N,S,(halt S),l) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
the of S . (halt S) 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 . (halt S)) . l is set
(N,S,s,l,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) (N)
the InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() 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
the carrier of S is non empty set
the_Values_of S is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total 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
P is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
P .--> (halt S) is trivial Relation-like NAT -defined {P} -defined the InstructionsF of S -valued Function-like one-to-one constant finite countable V120() set
{P} is non empty trivial finite V40() 1 -element countable set
{P} --> (halt S) is non empty Relation-like {P} -defined the InstructionsF of S -valued {(halt S)} -valued Function-like constant total V21({P},{(halt S)}) finite countable V120() Element of bool [:{P},{(halt S)}:]
{(halt S)} is non empty trivial finite 1 -element countable set
[:{P},{(halt S)}:] is Relation-like finite countable set
bool [:{P},{(halt S)}:] is finite V40() countable set
Start-At (P,S) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible finite countable V120() P -started set
IC is V56(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
(IC ) .--> P is trivial Relation-like the carrier of S -defined {(IC )} -defined NAT -valued Function-like one-to-one constant finite Cardinal-yielding countable V120() set
{(IC )} is non empty trivial finite 1 -element countable set
{(IC )} --> P is non empty Relation-like {(IC )} -defined NAT -valued {P} -valued Function-like constant total V21({(IC )},{P}) finite Cardinal-yielding countable V120() Element of bool [:{(IC )},{P}:]
[:{(IC )},{P}:] is Relation-like finite countable set
bool [:{(IC )},{P}:] is finite V40() countable set
s2 is Relation-like NAT -defined the InstructionsF of S -valued Function-like set
l is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible P -started set
l +* s2 is Relation-like Function-like set
l is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like total set
s is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like total set
proj1 l is set
k2 is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
s2 is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
i is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,l,k2,i) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,l,k2,i) | (proj1 l) is Relation-like proj1 l -defined the carrier of S -defined Function-like the_Values_of S -compatible set
(N,S,s,s2,i) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,s,s2,i) | (proj1 l) is Relation-like proj1 l -defined the carrier of S -defined Function-like the_Values_of S -compatible set
k2 | (proj1 l) is Relation-like proj1 l -defined the carrier of S -defined Function-like the_Values_of S -compatible set
s2 | (proj1 l) is Relation-like proj1 l -defined the carrier of S -defined Function-like the_Values_of S -compatible 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 InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
the carrier of S is non empty set
the_Values_of S is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total 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
P is Relation-like NAT -defined the InstructionsF of S -valued Function-like non halt-free 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
proj2 P is set
proj1 P is set
s is set
P . s is set
k is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
Start-At (k,S) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible finite countable V120() k -started set
IC is V56(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
(IC ) .--> k is trivial Relation-like the carrier of S -defined {(IC )} -defined NAT -valued Function-like one-to-one constant finite Cardinal-yielding countable V120() set
{(IC )} is non empty trivial finite 1 -element countable set
{(IC )} --> k is non empty Relation-like {(IC )} -defined NAT -valued {k} -valued Function-like constant total V21({(IC )},{k}) finite Cardinal-yielding countable V120() Element of bool [:{(IC )},{k}:]
{k} is non empty trivial finite V40() 1 -element countable set
[:{(IC )},{k}:] is Relation-like finite countable set
bool [:{(IC )},{k}:] is finite V40() countable set
s2 is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible finite countable V120() k -started set
k .--> (halt S) is trivial Relation-like NAT -defined {k} -defined the InstructionsF of S -valued Function-like one-to-one constant finite countable V120() set
{k} --> (halt S) is non empty Relation-like {k} -defined the InstructionsF of S -valued {(halt S)} -valued Function-like constant total V21({k},{(halt S)}) finite countable V120() Element of bool [:{k},{(halt S)}:]
{(halt S)} is non empty trivial finite 1 -element countable set
[:{k},{(halt S)}:] is Relation-like finite countable set
bool [:{k},{(halt S)}:] is finite V40() countable 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 InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
the carrier of S is non empty set
the_Values_of S is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total 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
P is Relation-like NAT -defined the InstructionsF of S -valued Function-like non halt-free 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
proj2 P is set
proj1 P is set
s is set
P . s is set
k is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
[k,(halt S)] is non empty V7() Element of [:NAT, the InstructionsF of S:]
[:NAT, the InstructionsF of S:] is non empty non trivial non empty-membered Relation-like non finite set
{k,(halt S)} is non empty finite countable set
{k} is non empty trivial finite V40() 1 -element countable set
{{k,(halt S)},{k}} is non empty with_non-empty_elements non empty-membered finite V40() countable set
{[k,(halt S)]} is non empty trivial with_non-empty_elements non empty-membered Relation-like NAT -defined the InstructionsF of S -valued the InstructionsF of S -valued Function-like constant finite 1 -element countable V120() V137(S) Element of bool [:NAT, the InstructionsF of S:]
bool [:NAT, the InstructionsF of S:] is non empty non trivial non empty-membered non finite set
k .--> (halt S) is trivial Relation-like NAT -defined {k} -defined the InstructionsF of S -valued Function-like one-to-one constant finite countable V120() set
{k} --> (halt S) is non empty Relation-like {k} -defined the InstructionsF of S -valued {(halt S)} -valued Function-like constant total V21({k},{(halt S)}) finite countable V120() Element of bool [:{k},{(halt S)}:]
{(halt S)} is non empty trivial finite 1 -element countable set
[:{k},{(halt S)}:] is Relation-like finite countable set
bool [:{k},{(halt S)}:] is finite V40() countable set
Start-At (k,S) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible finite countable V120() k -started set
IC is V56(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
(IC ) .--> k is trivial Relation-like the carrier of S -defined {(IC )} -defined NAT -valued Function-like one-to-one constant finite Cardinal-yielding countable V120() set
{(IC )} is non empty trivial finite 1 -element countable set
{(IC )} --> k is non empty Relation-like {(IC )} -defined NAT -valued {k} -valued Function-like constant total V21({(IC )},{k}) finite Cardinal-yielding countable V120() Element of bool [:{(IC )},{k}:]
[:{(IC )},{k}:] is Relation-like finite countable set
bool [:{(IC )},{k}:] is finite V40() countable set
s2 is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible finite countable V120() k -started 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 InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
the carrier of S is non empty set
the_Values_of S is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total 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
s is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible finite countable V120() set
P is Relation-like NAT -defined the InstructionsF of S -valued Function-like non halt-free set
proj1 s is finite countable set
k is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
s2 is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like total set
(N,S,s2,k) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,s2,(N,S,s2,k)) is Element of the InstructionsF of S
IC (N,S,s2,k) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
IC is V56(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
(N,S,s2,k) . (IC ) is set
s2 /. (IC (N,S,s2,k)) is Element of the InstructionsF of S
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
l is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,s2,k,l) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,s2,k) | (proj1 s) is Relation-like proj1 s -defined the carrier of S -defined Function-like the_Values_of S -compatible finite countable V120() set
l is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible finite countable V120() set
l is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like total set
s is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,l,s) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,l,s) | (proj1 s) is Relation-like proj1 s -defined the carrier of S -defined Function-like the_Values_of S -compatible finite countable V120() set
(N,S,l,(N,S,l,s)) is Element of the InstructionsF of S
IC (N,S,l,s) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,l,s) . (IC ) is set
l /. (IC (N,S,l,s)) is Element of the InstructionsF of S
k2 is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,l,s,k2) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,s2,k,k2) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,l,s,l) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
k is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
s2 is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like total set
l is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible finite countable V120() set
l is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible finite countable V120() set
(N,S,s2,k) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,s2,k) | (proj1 s) is Relation-like proj1 s -defined the carrier of S -defined Function-like the_Values_of S -compatible finite countable V120() 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 InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
the carrier of S is non empty set
the_Values_of S is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total 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) (N)
the InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
the carrier of S is non empty set
the_Values_of S is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total 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
P is Relation-like NAT -defined the InstructionsF of S -valued Function-like non halt-free set
s is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible finite countable V120() set
k is set
proj1 {} is empty trivial Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional ext-real epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-yielding V35() finite finite-yielding V40() cardinal {} -element V44() V45() V46() Cardinal-yielding countable V84() V85() V86() V119() V120() set
dom {} is empty trivial Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional ext-real epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-yielding V35() finite finite-yielding V40() cardinal {} -element V44() V45() V46() Cardinal-yielding countable V84() V85() V86() V119() V120() Element of bool NAT
s2 is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible finite countable V120() set
s +* s2 is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible finite countable V120() set
{} . s2 is empty trivial Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional ext-real epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-yielding V35() finite finite-yielding V40() cardinal {} -element V44() V45() V46() Cardinal-yielding countable V84() V85() V86() V119() V120() set
(N,S,P,(s +* s2)) is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible finite countable V120() 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 InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
the carrier of S is non empty set
the_Values_of S is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total 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
P is Relation-like NAT -defined the InstructionsF of S -valued Function-like non halt-free set
s is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible finite countable V120() set
(N,S,P,s) is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible finite countable V120() set
{} .--> (N,S,P,s) is trivial Relation-like {{}} -defined Function-like one-to-one constant Function-yielding V35() finite countable V120() set
{{}} is non empty trivial functional finite V40() 1 -element with_common_domain countable set
{{}} --> (N,S,P,s) is non empty Relation-like {{}} -defined {(N,S,P,s)} -valued Function-like constant total V21({{}},{(N,S,P,s)}) Function-yielding V35() finite countable V120() Element of bool [:{{}},{(N,S,P,s)}:]
{(N,S,P,s)} is non empty trivial functional finite V40() 1 -element with_common_domain countable set
[:{{}},{(N,S,P,s)}:] is Relation-like finite countable set
bool [:{{}},{(N,S,P,s)}:] is finite V40() countable set
proj1 ({} .--> (N,S,P,s)) is trivial finite countable set
k is set
s2 is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible finite countable V120() set
s +* s2 is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible finite countable V120() set
({} .--> (N,S,P,s)) . s2 is Relation-like Function-like set
(N,S,P,(s +* s2)) is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible finite countable V120() set
s +* {} is Relation-like Function-like finite countable V120() set
proj1 ({} .--> (N,S,P,s)) is trivial finite countable set
s +* {} is Relation-like Function-like finite countable V120() set
k is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible finite countable V120() set
s +* k is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible finite countable V120() set
({} .--> (N,S,P,s)) . k is Relation-like Function-like set
(N,S,P,(s +* k)) is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible finite countable V120() set
{} .--> {} is trivial Relation-like {{}} -defined Function-like one-to-one constant Function-yielding V35() finite Cardinal-yielding countable V120() set
{{}} is non empty trivial functional finite V40() 1 -element with_common_domain countable set
{{}} --> {} is non empty Relation-like {{}} -defined {{}} -valued Function-like constant total V21({{}},{{}}) Function-yielding V35() finite Cardinal-yielding countable V120() Element of bool [:{{}},{{}}:]
[:{{}},{{}}:] is Relation-like finite countable set
bool [:{{}},{{}}:] is finite V40() countable 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 InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
the carrier of S is non empty set
the_Values_of S is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total 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
P is Relation-like NAT -defined the InstructionsF of S -valued Function-like non halt-free set
s is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible finite countable V120() set
proj1 ({} .--> {}) is trivial finite countable set
k is set
s2 is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible finite countable V120() set
s +* s2 is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible finite countable V120() set
({} .--> {}) . s2 is Relation-like Function-like set
(N,S,P,(s +* s2)) is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible finite countable V120() set
s +* {} is Relation-like Function-like finite countable V120() set
proj1 ({} .--> {}) is trivial finite countable set
s +* {} is Relation-like Function-like finite countable V120() set
k is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible finite countable V120() set
s +* k is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible finite countable V120() set
({} .--> {}) . k is Relation-like Function-like set
(N,S,P,(s +* k)) is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible finite countable V120() 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
S is non empty with_non-empty_values IC-Ins-separated (N) (N)
the InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
the carrier of S is non empty set
the_Values_of S is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total 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
P is Relation-like NAT -defined the InstructionsF of S -valued Function-like set
s is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
proj1 P is 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
k is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() 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
IC (N,S,P,s,k) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
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) . (IC ) is set
(N,S,P,(N,S,P,s,k)) is Element of the InstructionsF of S
P /. (IC (N,S,P,s,k)) is Element of the InstructionsF of S
s2 is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
l is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,l) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
IC (N,S,P,s,l) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,l) . (IC ) is set
P . (IC (N,S,P,s,l)) is set
k is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,k) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
IC (N,S,P,s,k) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,k) . (IC ) is set
P . (IC (N,S,P,s,k)) is set
(N,S,P,(N,S,P,s,k)) is Element of the InstructionsF of S
P /. (IC (N,S,P,s,k)) 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) (N)
the InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
the carrier of S is non empty set
the_Values_of S is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total 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
P is Relation-like NAT -defined the InstructionsF of S -valued Function-like set
s is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,P,s) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
k is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() 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
IC (N,S,P,s,k) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
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) . (IC ) is set
proj1 P is 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
s2 is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() set
(N,S,P,s,s2) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
IC (N,S,P,s,s2) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,s2) . (IC ) is set
(N,S,P,(N,S,P,s,s2)) is Element of the InstructionsF of S
P /. (IC (N,S,P,s,s2)) is Element of the InstructionsF of S
(N,S,P,(N,S,P,s)) is Element of the InstructionsF of S
IC (N,S,P,s) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s) . (IC ) is set
P /. (IC (N,S,P,s)) is Element of the InstructionsF of S
l is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,l) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
l is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
l is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,l) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,P,s,l) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
l is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
l is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,l) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,P,s,l) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
l is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
l is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,l) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,P,s,l) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
l is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,l) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
l is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,l) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
P . (IC (N,S,P,s,k)) is set
(N,S,P,(N,S,P,s,k)) is Element of the InstructionsF of S
P /. (IC (N,S,P,s,k)) is Element of the InstructionsF of S
l is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
l is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,l) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,P,s,l) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
l is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
l is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,l) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,P,s,l) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
l is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
l is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,l) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,P,s,l) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
l is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,l) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
l is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,l) 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) (N)
the InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
the carrier of S is non empty set
the_Values_of S is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total 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
P is Relation-like NAT -defined the InstructionsF of S -valued Function-like set
s is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,P,s) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
k is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,k) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
IC (N,S,P,s,k) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
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) . (IC ) is set
N is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
S is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
P is non empty non with_non-empty_elements set
s is non empty with_non-empty_values IC-Ins-separated (P) (P)
the InstructionsF of s is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
the carrier of s is non empty set
the_Values_of s is non empty Relation-like non-empty non empty-yielding the carrier of s -defined Function-like total set
the Object-Kind of s is non empty Relation-like the carrier of s -defined P -valued Function-like total V21( the carrier of s,P) Element of bool [: the carrier of s,P:]
[: the carrier of s,P:] is Relation-like set
bool [: the carrier of s,P:] is set
the ValuesF of s is non empty Relation-like P -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
k is Relation-like NAT -defined the InstructionsF of s -valued Function-like set
s2 is non empty Relation-like the carrier of s -defined Function-like the_Values_of s -compatible total set
(P,s,k,s2,N) is non empty Relation-like the carrier of s -defined Function-like the_Values_of s -compatible total set
IC (P,s,k,s2,N) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
IC is V56(s) Element of the carrier of s
the ZeroF of s is Element of the carrier of s
(P,s,k,s2,N) . (IC ) is set
(P,s,k,s2,S) is non empty Relation-like the carrier of s -defined Function-like the_Values_of s -compatible total set
IC (P,s,k,s2,S) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(P,s,k,s2,S) . (IC ) is set
proj1 k is set
k . (IC (P,s,k,s2,N)) is set
halt s is (P,s) Element of the InstructionsF of s
halt the InstructionsF of s is ins-loc-free Element of the InstructionsF of s
(P,s,k,(P,s,k,s2,N)) is Element of the InstructionsF of s
k /. (IC (P,s,k,s2,N)) is Element of the InstructionsF of s
k . (IC (P,s,k,s2,S)) is set
N is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
S is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
P is non empty non with_non-empty_elements set
s is non empty with_non-empty_values IC-Ins-separated (P) (P)
the InstructionsF of s is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
the carrier of s is non empty set
the_Values_of s is non empty Relation-like non-empty non empty-yielding the carrier of s -defined Function-like total set
the Object-Kind of s is non empty Relation-like the carrier of s -defined P -valued Function-like total V21( the carrier of s,P) Element of bool [: the carrier of s,P:]
[: the carrier of s,P:] is Relation-like set
bool [: the carrier of s,P:] is set
the ValuesF of s is non empty Relation-like P -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
k is Relation-like NAT -defined the InstructionsF of s -valued Function-like set
s2 is non empty Relation-like the carrier of s -defined Function-like the_Values_of s -compatible total set
(P,s,k,s2,N) is non empty Relation-like the carrier of s -defined Function-like the_Values_of s -compatible total set
IC (P,s,k,s2,N) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
IC is V56(s) Element of the carrier of s
the ZeroF of s is Element of the carrier of s
(P,s,k,s2,N) . (IC ) is set
(P,s,k,s2,S) is non empty Relation-like the carrier of s -defined Function-like the_Values_of s -compatible total set
IC (P,s,k,s2,S) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(P,s,k,s2,S) . (IC ) is set
(P,s,k,s2) 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) (N)
the InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
the carrier of S is non empty set
the_Values_of S is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total 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
P is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like total set
s is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,P,s) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
k is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,k) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
IC (N,S,P,s,k) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
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) . (IC ) is set
s2 is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,s2) 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,s2)) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
P . (IC (N,S,P,s,k)) is Element of the InstructionsF of S
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
S is non empty with_non-empty_values IC-Ins-separated (N) (N)
the InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
the carrier of S is non empty set
the_Values_of S is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total 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
P is Relation-like NAT -defined the InstructionsF of S -valued Function-like set
s is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible 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
proj1 P is set
k is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() 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
IC (N,S,P,s,k) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
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) . (IC ) is set
(N,S,P,(N,S,P,s,k)) is Element of the InstructionsF of S
P /. (IC (N,S,P,s,k)) is Element of the InstructionsF of S
s2 is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() set
(N,S,P,s,s2) 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,s2)) is Element of the InstructionsF of S
IC (N,S,P,s,s2) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,s2) . (IC ) is set
P /. (IC (N,S,P,s,s2)) is Element of the InstructionsF of S
l is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,l) 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,l)) is Element of the InstructionsF of S
IC (N,S,P,s,l) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,l) . (IC ) is set
P /. (IC (N,S,P,s,l)) is Element of the InstructionsF of S
l is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,l) 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,l)) is Element of the InstructionsF of S
IC (N,S,P,s,l) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,l) . (IC ) is set
P /. (IC (N,S,P,s,l)) is Element of the InstructionsF of S
k is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(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,P,(N,S,P,s,k)) is Element of the InstructionsF of S
IC (N,S,P,s,k) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
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) . (IC ) is set
P /. (IC (N,S,P,s,k)) is Element of the InstructionsF of S
s2 is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,s2) 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,s2)) is Element of the InstructionsF of S
IC (N,S,P,s,s2) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,s2) . (IC ) is set
P /. (IC (N,S,P,s,s2)) 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) (N)
the InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
the carrier of S is non empty set
the_Values_of S is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total 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
P is Relation-like NAT -defined the InstructionsF of S -valued Function-like set
s is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
k is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,k) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
proj1 P is 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
s2 is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() set
(N,S,P,s,s2) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
IC (N,S,P,s,s2) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
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,s2) . (IC ) is set
(N,S,P,(N,S,P,s,s2)) is Element of the InstructionsF of S
P /. (IC (N,S,P,s,s2)) is Element of the InstructionsF of S
l is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,l) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
k + 0 is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,(k + 0)) 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),0) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
l is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
l - k is ext-real V84() V85() V86() set
l is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,(N,S,P,s,k),l) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
k + l is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,(k + l)) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,P,s,l) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
l is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
s2 is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() set
(N,S,P,(N,S,P,s,k),s2) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
IC (N,S,P,(N,S,P,s,k),s2) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,(N,S,P,s,k),s2) . (IC ) is set
(N,S,P,(N,S,P,(N,S,P,s,k),s2)) is Element of the InstructionsF of S
P /. (IC (N,S,P,(N,S,P,s,k),s2)) is Element of the InstructionsF of S
l is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
k + l is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,(k + l)) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
IC (N,S,P,s,(k + l)) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,(k + l)) . (IC ) is set
(N,S,P,(N,S,P,s,(k + l))) is Element of the InstructionsF of S
P /. (IC (N,S,P,s,(k + l))) 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) (N)
the InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
the carrier of S is non empty set
the_Values_of S is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total 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
P is Relation-like NAT -defined the InstructionsF of S -valued Function-like set
s is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,P,s) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,P,s) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,(N,S,P,s)) 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,(N,S,P,s))) is Element of the InstructionsF of S
IC (N,S,P,s,(N,S,P,s)) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
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,(N,S,P,s)) . (IC ) is set
P /. (IC (N,S,P,s,(N,S,P,s))) is Element of the InstructionsF of S
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,(N,S,P,s)) is Element of the InstructionsF of S
IC (N,S,P,s) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s) . (IC ) is set
P /. (IC (N,S,P,s)) is Element of the InstructionsF of S
k is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(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 is non empty non with_non-empty_elements set
S is non empty with_non-empty_values IC-Ins-separated (N) (N)
the InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
the carrier of S is non empty set
the_Values_of S is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total 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
P is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like total set
s is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,P,s) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,(N,S,P,s)) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
k is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(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,P,(N,S,P,s,k)) is Element of the InstructionsF of S
IC (N,S,P,s,k) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
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) . (IC ) is set
P /. (IC (N,S,P,s,k)) is Element of the InstructionsF of S
proj1 P is non empty set
(N,S,P,(N,S,P,s,(N,S,P,s))) is Element of the InstructionsF of S
IC (N,S,P,s,(N,S,P,s)) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,(N,S,P,s)) . (IC ) is set
P /. (IC (N,S,P,s,(N,S,P,s))) is Element of the InstructionsF of S
N is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
S is non empty non with_non-empty_elements set
P is non empty with_non-empty_values IC-Ins-separated (S) (S)
the InstructionsF of P is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
the carrier of P is non empty set
the_Values_of P is non empty Relation-like non-empty non empty-yielding the carrier of P -defined Function-like total 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 is Relation-like NAT -defined the InstructionsF of P -valued Function-like set
k is non empty Relation-like the carrier of P -defined Function-like the_Values_of P -compatible total set
(S,P,s,k) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(S,P,s,k,N) is non empty Relation-like the carrier of P -defined Function-like the_Values_of P -compatible total set
(S,P,s,k,(S,P,s,k)) is non empty Relation-like the carrier of P -defined Function-like the_Values_of P -compatible total set
(S,P,s,(S,P,s,k,(S,P,s,k))) is Element of the InstructionsF of P
IC (S,P,s,k,(S,P,s,k)) 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,s,k,(S,P,s,k)) . (IC ) is set
s /. (IC (S,P,s,k,(S,P,s,k))) is Element of the InstructionsF of P
halt P is (S,P) Element of the InstructionsF of P
halt the InstructionsF of P is ins-loc-free Element of the InstructionsF of P
N is non empty non with_non-empty_elements set
S is non empty with_non-empty_values IC-Ins-separated (N)
the InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
the carrier of S is non empty set
the_Values_of S is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total 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
P is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() set
s is Element of the InstructionsF of S
P .--> s is trivial Relation-like {P} -defined the InstructionsF of S -valued Function-like one-to-one constant finite countable V120() set
{P} is non empty trivial finite V40() 1 -element countable set
{P} --> s is non empty Relation-like {P} -defined the InstructionsF of S -valued {s} -valued Function-like constant total V21({P},{s}) finite countable V120() Element of bool [:{P},{s}:]
{s} is non empty trivial finite 1 -element countable set
[:{P},{s}:] is Relation-like finite countable set
bool [:{P},{s}:] is finite V40() countable set
k is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total P -started set
(N,S,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 . s 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 . s) . k is set
s2 is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like total set
(N,S,k,s2) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,s2,k) is Element of the InstructionsF of S
IC k is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
IC is V56(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
k . (IC ) is set
s2 /. (IC k) is Element of the InstructionsF of S
(N,S,(N,S,s2,k),k) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
the of S . (N,S,s2,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,s2,k)) . k is set
proj1 (P .--> s) is trivial finite countable set
s2 . P is Element of the InstructionsF of S
(P .--> s) . 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) (N)
the InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
the carrier of S is non empty set
the_Values_of S is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total 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
P is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like total set
s is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,s,P) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,P,s) is Element of the InstructionsF of S
IC s is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
IC is V56(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
s . (IC ) is set
P /. (IC s) is Element of the InstructionsF of S
(N,S,(N,S,P,s),s) 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,s) 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,s)) . s is set
k is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,k) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
k + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(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,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 InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
the carrier of S is non empty set
the_Values_of S is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total 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
P is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like total set
s is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
IC s is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
s . (IC ) is set
P . (IC s) is Element of the InstructionsF of S
(N,S,(P . (IC s)),s) 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 . (P . (IC s)) 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 . (IC s))) . s is set
(N,S,(P . (IC s)),s) . (IC ) is set
(N,S,s,P) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,P,s) is Element of the InstructionsF of S
P /. (IC s) is Element of the InstructionsF of S
(N,S,(N,S,P,s),s) 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,s) 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,s)) . s is set
IC (N,S,s,P) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,s,P) . (IC ) is set
proj1 P is non empty 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 InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
the carrier of S is non empty set
the_Values_of S is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total 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
P is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like total set
s is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
proj1 P is non empty set
k is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() 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
IC (N,S,P,s,k) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
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) . (IC ) is set
(N,S,P,(N,S,P,s,k)) is Element of the InstructionsF of S
P /. (IC (N,S,P,s,k)) is Element of the InstructionsF of S
s2 is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,s2) 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,s2)) is Element of the InstructionsF of S
IC (N,S,P,s,s2) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,s2) . (IC ) is set
P /. (IC (N,S,P,s,s2)) is Element of the InstructionsF of S
k is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(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,P,(N,S,P,s,k)) is Element of the InstructionsF of S
IC (N,S,P,s,k) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
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) . (IC ) is set
P /. (IC (N,S,P,s,k)) is Element of the InstructionsF of S
proj1 P is non empty 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 InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
the carrier of S is non empty set
the_Values_of S is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total 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
P is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like total set
s is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
k is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,k) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
IC (N,S,P,s,k) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
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) . (IC ) is set
P . (IC (N,S,P,s,k)) is Element of the InstructionsF of S
proj1 P is non empty set
(N,S,P,(N,S,P,s,k)) is Element of the InstructionsF of S
P /. (IC (N,S,P,s,k)) 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) (N)
the InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
the carrier of S is non empty set
the_Values_of S is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total 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
P is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like total set
s is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,P,s) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
k is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,k) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
IC (N,S,P,s,k) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
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) . (IC ) is set
P . (IC (N,S,P,s,k)) is Element of the InstructionsF of S
proj1 P is non empty set
(N,S,P,(N,S,P,s,k)) is Element of the InstructionsF of S
P /. (IC (N,S,P,s,k)) 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) (N)
the InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
the carrier of S is non empty set
the_Values_of S is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total 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
P is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like total set
s is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,P,s) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
k is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,k) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
IC (N,S,P,s,k) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
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) . (IC ) is set
P . (IC (N,S,P,s,k)) is Element of the InstructionsF of S
k + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(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
IC (N,S,P,s,(k + 1)) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,(k + 1)) . (IC ) is set
P . (IC (N,S,P,s,(k + 1))) is Element of the InstructionsF of S
proj1 P is non empty set
(N,S,P,(N,S,P,s,k)) is Element of the InstructionsF of S
P /. (IC (N,S,P,s,k)) is Element of the InstructionsF of S
s2 is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,s2) 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,s2)) is Element of the InstructionsF of S
IC (N,S,P,s,s2) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,s2) . (IC ) is set
P /. (IC (N,S,P,s,s2)) is Element of the InstructionsF of S
(N,S,P,(N,S,P,s,(k + 1))) is Element of the InstructionsF of S
P /. (IC (N,S,P,s,(k + 1))) 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) (N)
the InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
the carrier of S is non empty set
the_Values_of S is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total 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
P is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like total set
s is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,P,s) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
k is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,k) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
IC (N,S,P,s,k) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
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) . (IC ) is set
k + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(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
IC (N,S,P,s,(k + 1)) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,(k + 1)) . (IC ) is set
P . (IC (N,S,P,s,(k + 1))) is Element of the InstructionsF of S
proj1 P is non empty set
P . (IC (N,S,P,s,k)) is Element of the InstructionsF of S
(N,S,P,(N,S,P,s,k)) is Element of the InstructionsF of S
P /. (IC (N,S,P,s,k)) 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) (N)
the InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
the carrier of S is non empty set
the_Values_of S is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total 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
P is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like total set
s is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,P,s) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
k is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(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,P,(N,S,P,s,k)) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
k + (N,S,P,(N,S,P,s,k)) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
l is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() set
l + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
l is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
l + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,(N,S,P,s,k),(l + 1)) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
IC (N,S,P,(N,S,P,s,k),(l + 1)) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
IC is V56(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
(N,S,P,(N,S,P,s,k),(l + 1)) . (IC ) is set
P . (IC (N,S,P,(N,S,P,s,k),(l + 1))) is Element of the InstructionsF of S
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
k + (l + 1) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,(k + (l + 1))) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
IC (N,S,P,s,(k + (l + 1))) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,(k + (l + 1))) . (IC ) is set
P . (IC (N,S,P,s,(k + (l + 1)))) is Element of the InstructionsF of S
(N,S,P,(N,S,P,s,k),l) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
IC (N,S,P,(N,S,P,s,k),l) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,(N,S,P,s,k),l) . (IC ) is set
P . (IC (N,S,P,(N,S,P,s,k),l)) is Element of the InstructionsF of S
k + l is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,(k + l)) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
IC (N,S,P,s,(k + l)) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,(k + l)) . (IC ) is set
P . (IC (N,S,P,s,(k + l))) is Element of the InstructionsF of S
(k + l) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
N is non empty non with_non-empty_elements set
S is non empty with_non-empty_values IC-Ins-separated (N) (N)
the InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
the carrier of S is non empty set
the_Values_of S is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total 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
P is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like total set
s is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,P,s) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
k is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(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,P,(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,P,(N,S,P,(N,S,P,s,k))) is Element of the InstructionsF of S
IC (N,S,P,(N,S,P,s,k)) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
IC is V56(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
(N,S,P,(N,S,P,s,k)) . (IC ) is set
P /. (IC (N,S,P,(N,S,P,s,k))) is Element of the InstructionsF of S
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
l is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,(N,S,P,s,k),l) is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
k + l is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,(k + l)) 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) (N)
the InstructionsF of S is non empty Relation-like standard-ins homogeneous J/A-independent V132() set
the carrier of S is non empty set
the_Values_of S is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total 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
P is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like total set
s is non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total set
(N,S,P,s) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,(N,S,P,s)) 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,(N,S,P,s))) is Element of the InstructionsF of S
IC (N,S,P,s,(N,S,P,s)) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
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,(N,S,P,s)) . (IC ) is set
P /. (IC (N,S,P,s,(N,S,P,s))) is Element of the InstructionsF of S
k is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(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,P,(N,S,P,s,k)) is Element of the InstructionsF of S
IC (N,S,P,s,k) is ext-real epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V84() V85() V86() Element of NAT
(N,S,P,s,k) . (IC ) is set
P /. (IC (N,S,P,s,k)) is Element of the InstructionsF of S