:: EXTPRO_1 semantic presentation

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