REAL is non empty non with_non-empty_elements V103() V104() V105() V109() V112() V113() V115() set
NAT is epsilon-transitive epsilon-connected ordinal non empty V19() non finite cardinal limit_cardinal non with_non-empty_elements non empty-membered countable denumerable V103() V104() V105() V106() V107() V108() V109() V110() V112() Element of K29(REAL)
K29(REAL) is set
COMPLEX is V103() V109() set
omega is epsilon-transitive epsilon-connected ordinal non empty V19() non finite cardinal limit_cardinal non with_non-empty_elements non empty-membered countable denumerable V103() V104() V105() V106() V107() V108() V109() V110() V112() set
K29(omega) is non empty V19() non finite non empty-membered set
K29(NAT) is non empty V19() non finite non empty-membered set
RAT is V103() V104() V105() V106() V109() set
INT is V103() V104() V105() V106() V107() V109() set
{} is Relation-like non-empty empty-yielding NAT -defined RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty V28() V29() finite finite-yielding V36() cardinal {} -element V40() V41() V42() initial Cardinal-yielding countable ext-real non positive non negative V103() V104() V105() V106() V107() V108() V109() V112() V113() V114() V115() V121() V122() V123() V124() Function-yielding V148() FuncSeq-like set
the Relation-like non-empty empty-yielding NAT -defined RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty V28() V29() finite finite-yielding V36() cardinal {} -element V40() V41() V42() initial Cardinal-yielding countable ext-real non positive non negative V103() V104() V105() V106() V107() V108() V109() V112() V113() V114() V115() V121() V122() V123() V124() Function-yielding V148() FuncSeq-like set is Relation-like non-empty empty-yielding NAT -defined RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty V28() V29() finite finite-yielding V36() cardinal {} -element V40() V41() V42() initial Cardinal-yielding countable ext-real non positive non negative V103() V104() V105() V106() V107() V108() V109() V112() V113() V114() V115() V121() V122() V123() V124() Function-yielding V148() FuncSeq-like set
2 is epsilon-transitive epsilon-connected ordinal natural non empty V28() V29() V30() finite cardinal countable ext-real positive non negative V103() V104() V105() V106() V107() V108() V110() V111() V112() V113() V114() V120() Element of NAT
ExtREAL is V104() V115() set
1 is epsilon-transitive epsilon-connected ordinal natural non empty V28() V29() V30() finite cardinal countable ext-real positive non negative V103() V104() V105() V106() V107() V108() V110() V111() V112() V113() V114() V120() Element of NAT
3 is epsilon-transitive epsilon-connected ordinal natural non empty V28() V29() V30() finite cardinal countable ext-real positive non negative V103() V104() V105() V106() V107() V108() V110() V111() V112() V113() V114() V120() Element of NAT
0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty V28() V29() V30() finite finite-yielding V36() cardinal {} -element V40() V41() V42() initial Cardinal-yielding countable ext-real non positive non negative V103() V104() V105() V106() V107() V108() V109() V112() V113() V114() V115() V120() V121() V122() V123() V124() Function-yielding V148() FuncSeq-like Element of NAT
K103(NAT,0) is functional non empty V19() finite V36() 1 -element with_common_domain countable V103() V104() V105() V106() V107() V108() V110() V111() V112() V113() V114() Element of K29(NAT)
K31(NAT,NAT,NAT) is set
K101(NAT,NAT,NAT,0,0,0) is V22() V23() Element of K31(NAT,NAT,NAT)
[0,0] is V22() set
{0,0} is functional non empty finite V36() countable V103() V104() V105() V106() V107() V108() V110() V111() V112() V113() V114() set
{0} is functional non empty V19() finite V36() 1 -element with_common_domain countable V103() V104() V105() V106() V107() V108() V110() V111() V112() V113() V114() set
{{0,0},{0}} is non empty finite V36() with_non-empty_elements non empty-membered countable set
[[0,0],0] is V22() set
{[0,0],0} is non empty finite countable set
{[0,0]} is Relation-like Function-like constant non empty V19() finite 1 -element countable set
{{[0,0],0},{[0,0]}} is non empty finite V36() with_non-empty_elements non empty-membered countable set
K101(NAT,NAT,NAT,1,0,0) is V22() V23() Element of K31(NAT,NAT,NAT)
[1,0] is V22() set
{1,0} is non empty finite V36() countable V103() V104() V105() V106() V107() V108() V110() V111() V112() V113() V114() set
{1} is non empty V19() finite V36() 1 -element with_non-empty_elements non empty-membered countable V103() V104() V105() V106() V107() V108() V110() V111() V112() V113() V114() set
{{1,0},{1}} is non empty finite V36() with_non-empty_elements non empty-membered countable set
[[1,0],0] is V22() set
{[1,0],0} is non empty finite countable set
{[1,0]} is Relation-like Function-like constant non empty V19() finite 1 -element countable set
{{[1,0],0},{[1,0]}} is non empty finite V36() with_non-empty_elements non empty-membered countable set
K104(K31(NAT,NAT,NAT),K101(NAT,NAT,NAT,0,0,0),K101(NAT,NAT,NAT,1,0,0)) is Relation-like non empty finite standard-ins homogeneous J/A-independent V55() countable Element of K29(K31(NAT,NAT,NAT))
K29(K31(NAT,NAT,NAT)) is set
0 .--> 0 is Relation-like NAT -defined {0} -defined NAT -valued RAT -valued INT -valued Function-like one-to-one constant non empty V19() finite 1 -element Cardinal-yielding countable V121() V122() V123() V124() V125() V126() V127() V128() Function-yielding V148() set
{0} --> 0 is Relation-like {0} -defined NAT -valued RAT -valued INT -valued {0} -valued Function-like constant non empty total V25({0},{0}) finite Cardinal-yielding countable V121() V122() V123() V124() Function-yielding V148() Element of K29(K30({0},{0}))
K30({0},{0}) is Relation-like RAT -valued INT -valued finite countable V121() V122() V123() V124() set
K29(K30({0},{0})) is finite V36() countable set
proj1 {} is Relation-like non-empty empty-yielding NAT -defined RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty V28() V29() finite finite-yielding V36() cardinal {} -element V40() V41() V42() initial Cardinal-yielding countable ext-real non positive non negative V103() V104() V105() V106() V107() V108() V109() V112() V113() V114() V115() V121() V122() V123() V124() Function-yielding V148() FuncSeq-like set
proj2 {} is Relation-like non-empty empty-yielding NAT -defined RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty V19() V28() V29() finite finite-yielding V36() cardinal {} -element V40() V41() V42() with_non-empty_elements initial Cardinal-yielding countable ext-real non positive non negative V103() V104() V105() V106() V107() V108() V109() V112() V113() V114() V115() V121() V122() V123() V124() V125() V126() V127() V128() Function-yielding V148() FuncSeq-like set
[0,{},{}] is V22() V23() set
[0,{}] is V22() set
{0,{}} is functional non empty finite V36() countable V103() V104() V105() V106() V107() V108() V110() V111() V112() V113() V114() set
{{0,{}},{0}} is non empty finite V36() with_non-empty_elements non empty-membered countable set
[[0,{}],{}] is V22() set
{[0,{}],{}} is non empty finite countable set
{[0,{}]} is Relation-like Function-like constant non empty V19() finite 1 -element countable set
{{[0,{}],{}},{[0,{}]}} is non empty finite V36() with_non-empty_elements non empty-membered countable set
{[0,{},{}]} is Relation-like non empty V19() finite 1 -element standard-ins homogeneous J/A-independent V55() countable set
N is non empty non with_non-empty_elements set
STC N is non empty finite with_non-empty_values IC-Ins-separated strict halting standard AMI-Struct over N
the InstructionsF of (STC N) is Relation-like non empty standard-ins homogeneous J/A-independent V55() set
S is ins-loc-free Element of the InstructionsF of (STC N)
JumpPart S is Relation-like non-empty empty-yielding NAT -defined NAT -valued RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty V28() V29() finite finite-yielding V36() cardinal {} -element V40() V41() V42() initial Cardinal-yielding countable ext-real non positive non negative V103() V104() V105() V106() V107() V108() V109() V112() V113() V114() V115() V121() V122() V123() V124() Function-yielding V148() FuncSeq-like set
K50(S) is set
AddressPart K50(S) is set
N is non empty non with_non-empty_elements set
S is non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
the InstructionsF of S is Relation-like non empty standard-ins homogeneous J/A-independent V55() set
N is non empty non with_non-empty_elements set
N is non empty non with_non-empty_elements set
STC N is non empty finite with_non-empty_values IC-Ins-separated strict halting standard AMI-Struct over N
N is non empty non with_non-empty_elements set
S is non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N
the InstructionsF of S is Relation-like non empty standard-ins homogeneous J/A-independent V55() set
P is Element of the InstructionsF of S
JUMP P is countable V103() V104() V105() V106() V107() V108() V112() Element of K29(NAT)
{ (NIC (P,b1)) where b1 is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT : verum } is set
meet { (NIC (P,b1)) where b1 is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT : verum } is set
s2 is set
P1 is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
NIC (P,P1) is non empty countable V103() V104() V105() V106() V107() V108() V110() V112() Element of K29(NAT)
the carrier of S is non empty set
the_Values_of S is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
the Object-Kind of S is Relation-like the carrier of S -defined N -valued Function-like non empty total V25( the carrier of S,N) Element of K29(K30( the carrier of S,N))
K30( the carrier of S,N) is Relation-like set
K29(K30( the carrier of S,N)) is set
the ValuesF of S is Relation-like N -defined Function-like non empty total set
the Object-Kind of S (#) the ValuesF of S is Relation-like the carrier of S -defined Function-like non empty total set
product (the_Values_of S) is functional non empty with_common_domain product-like set
{ (IC (Exec (P,b1))) where b1 is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible non empty total Element of product (the_Values_of S) : IC b1 = P1 } is set
succ P1 is epsilon-transitive epsilon-connected ordinal natural non empty V28() V29() finite cardinal countable ext-real positive non negative set
P1 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V28() V29() V30() finite cardinal countable ext-real positive non negative V103() V104() V105() V106() V107() V108() V110() V111() V112() V113() V114() V120() Element of NAT
{(succ P1)} is non empty V19() finite V36() 1 -element with_non-empty_elements non empty-membered countable V103() V104() V105() V106() V107() V108() V110() V111() V112() V113() V114() set
P2 is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
NIC (P,P2) is non empty countable V103() V104() V105() V106() V107() V108() V110() V112() Element of K29(NAT)
{ (IC (Exec (P,b1))) where b1 is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible non empty total Element of product (the_Values_of S) : IC b1 = P2 } is set
succ P2 is epsilon-transitive epsilon-connected ordinal natural non empty V28() V29() finite cardinal countable ext-real positive non negative set
P2 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V28() V29() V30() finite cardinal countable ext-real positive non negative V103() V104() V105() V106() V107() V108() V110() V111() V112() V113() V114() V120() Element of NAT
{(succ P2)} is non empty V19() finite V36() 1 -element with_non-empty_elements non empty-membered countable V103() V104() V105() V106() V107() V108() V110() V111() V112() V113() V114() set
N is non empty non with_non-empty_elements set
STC N is non empty finite with_non-empty_values IC-Ins-separated strict halting standard AMI-Struct over N
the InstructionsF of (STC N) is Relation-like non empty standard-ins homogeneous J/A-independent V55() set
S is ins-loc-free Element of the InstructionsF of (STC N)
JUMP S is countable V103() V104() V105() V106() V107() V108() V112() Element of K29(NAT)
{ (NIC (S,b1)) where b1 is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT : verum } is set
meet { (NIC (S,b1)) where b1 is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT : verum } is set
InsCode S is epsilon-transitive epsilon-connected ordinal natural V28() V29() finite cardinal countable ext-real non negative Element of InsCodes the InstructionsF of (STC N)
InsCodes the InstructionsF of (STC N) is non empty set
K60( the InstructionsF of (STC N)) is set
proj1 the InstructionsF of (STC N) is non empty set
proj1 (proj1 the InstructionsF of (STC N)) is set
K50(S) is set
K50(K50(S)) is set
P is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
NIC (S,P) is non empty countable V103() V104() V105() V106() V107() V108() V110() V112() Element of K29(NAT)
the carrier of (STC N) is non empty finite countable set
the_Values_of (STC N) is Relation-like non-empty non empty-yielding the carrier of (STC N) -defined Function-like non empty total set
the Object-Kind of (STC N) is Relation-like the carrier of (STC N) -defined N -valued Function-like non empty total V25( the carrier of (STC N),N) finite countable Element of K29(K30( the carrier of (STC N),N))
K30( the carrier of (STC N),N) is Relation-like set
K29(K30( the carrier of (STC N),N)) is set
the ValuesF of (STC N) is Relation-like N -defined Function-like non empty total set
the Object-Kind of (STC N) (#) the ValuesF of (STC N) is Relation-like the carrier of (STC N) -defined Function-like non empty total finite countable set
product (the_Values_of (STC N)) is functional non empty with_common_domain product-like set
{ (IC (Exec (S,b1))) where b1 is Relation-like the carrier of (STC N) -defined Function-like the_Values_of (STC N) -compatible non empty total Element of product (the_Values_of (STC N)) : IC b1 = P } is set
{P} is non empty V19() finite V36() 1 -element countable V103() V104() V105() V106() V107() V108() V110() V111() V112() V113() V114() set
InsCode S is epsilon-transitive epsilon-connected ordinal natural V28() V29() finite cardinal countable ext-real non negative Element of InsCodes the InstructionsF of (STC N)
InsCodes the InstructionsF of (STC N) is non empty set
K60( the InstructionsF of (STC N)) is set
proj1 the InstructionsF of (STC N) is non empty set
proj1 (proj1 the InstructionsF of (STC N)) is set
K50(S) is set
K50(K50(S)) is set
P is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
NIC (S,P) is non empty countable V103() V104() V105() V106() V107() V108() V110() V112() Element of K29(NAT)
the carrier of (STC N) is non empty finite countable set
the_Values_of (STC N) is Relation-like non-empty non empty-yielding the carrier of (STC N) -defined Function-like non empty total set
the Object-Kind of (STC N) is Relation-like the carrier of (STC N) -defined N -valued Function-like non empty total V25( the carrier of (STC N),N) finite countable Element of K29(K30( the carrier of (STC N),N))
K30( the carrier of (STC N),N) is Relation-like set
K29(K30( the carrier of (STC N),N)) is set
the ValuesF of (STC N) is Relation-like N -defined Function-like non empty total set
the Object-Kind of (STC N) (#) the ValuesF of (STC N) is Relation-like the carrier of (STC N) -defined Function-like non empty total finite countable set
product (the_Values_of (STC N)) is functional non empty with_common_domain product-like set
{ (IC (Exec (S,b1))) where b1 is Relation-like the carrier of (STC N) -defined Function-like the_Values_of (STC N) -compatible non empty total Element of product (the_Values_of (STC N)) : IC b1 = P } is set
succ P is epsilon-transitive epsilon-connected ordinal natural non empty V28() V29() finite cardinal countable ext-real positive non negative set
P + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V28() V29() V30() finite cardinal countable ext-real positive non negative V103() V104() V105() V106() V107() V108() V110() V111() V112() V113() V114() V120() Element of NAT
{(succ P)} is non empty V19() finite V36() 1 -element with_non-empty_elements non empty-membered countable V103() V104() V105() V106() V107() V108() V110() V111() V112() V113() V114() set
InsCode S is epsilon-transitive epsilon-connected ordinal natural V28() V29() finite cardinal countable ext-real non negative Element of InsCodes the InstructionsF of (STC N)
InsCodes the InstructionsF of (STC N) is non empty set
K60( the InstructionsF of (STC N)) is set
proj1 the InstructionsF of (STC N) is non empty set
proj1 (proj1 the InstructionsF of (STC N)) is set
K50(S) is set
K50(K50(S)) is set
N is non empty non with_non-empty_elements set
STC N is non empty finite with_non-empty_values IC-Ins-separated strict halting standard AMI-Struct over N
the InstructionsF of (STC N) is Relation-like non empty standard-ins homogeneous J/A-independent V55() set
InsCodes the InstructionsF of (STC N) is non empty set
K60( the InstructionsF of (STC N)) is set
proj1 the InstructionsF of (STC N) is non empty set
proj1 (proj1 the InstructionsF of (STC N)) is set
S is Element of InsCodes the InstructionsF of (STC N)
JumpParts S is functional non empty with_common_domain product-like set
{ (JumpPart b1) where b1 is Element of the InstructionsF of (STC N) : InsCode b1 = S } is set
s is set
[0,0,0] is V22() V23() set
[1,0,0] is V22() V23() set
{[0,0,0],[1,0,0]} is Relation-like non empty finite standard-ins homogeneous J/A-independent V55() countable set
{0,1} is non empty finite V36() countable V103() V104() V105() V106() V107() V108() V110() V111() V112() V113() V114() set
I is ins-loc-free Element of the InstructionsF of (STC N)
JumpPart I is Relation-like non-empty empty-yielding NAT -defined NAT -valued RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty V28() V29() finite finite-yielding V36() cardinal {} -element V40() V41() V42() initial Cardinal-yielding countable ext-real non positive non negative V103() V104() V105() V106() V107() V108() V109() V112() V113() V114() V115() V121() V122() V123() V124() Function-yielding V148() FuncSeq-like set
K50(I) is set
AddressPart K50(I) is set
InsCode I is epsilon-transitive epsilon-connected ordinal natural V28() V29() finite cardinal countable ext-real non negative Element of InsCodes the InstructionsF of (STC N)
K50(K50(I)) is set
{ (JumpPart b2) where b1 is ins-loc-free Element of the InstructionsF of (STC N) : InsCode b2 = S } is set
I is ins-loc-free Element of the InstructionsF of (STC N)
JumpPart I is Relation-like non-empty empty-yielding NAT -defined NAT -valued RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty V28() V29() finite finite-yielding V36() cardinal {} -element V40() V41() V42() initial Cardinal-yielding countable ext-real non positive non negative V103() V104() V105() V106() V107() V108() V109() V112() V113() V114() V115() V121() V122() V123() V124() Function-yielding V148() FuncSeq-like set
K50(I) is set
AddressPart K50(I) is set
InsCode I is epsilon-transitive epsilon-connected ordinal natural V28() V29() finite cardinal countable ext-real non negative Element of InsCodes the InstructionsF of (STC N)
K50(K50(I)) is set
{ (JumpPart b2) where b1 is ins-loc-free Element of the InstructionsF of (STC N) : InsCode b2 = S } is set
{ (JumpPart b2) where b1 is ins-loc-free Element of the InstructionsF of (STC N) : InsCode b2 = S } is set
s is set
I is ins-loc-free Element of the InstructionsF of (STC N)
JumpPart I is Relation-like non-empty empty-yielding NAT -defined NAT -valued RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty V28() V29() finite finite-yielding V36() cardinal {} -element V40() V41() V42() initial Cardinal-yielding countable ext-real non positive non negative V103() V104() V105() V106() V107() V108() V109() V112() V113() V114() V115() V121() V122() V123() V124() Function-yielding V148() FuncSeq-like set
K50(I) is set
AddressPart K50(I) is set
InsCode I is epsilon-transitive epsilon-connected ordinal natural V28() V29() finite cardinal countable ext-real non negative Element of InsCodes the InstructionsF of (STC N)
K50(K50(I)) is set
N is non empty non with_non-empty_elements set
Trivial-AMI N is non empty V67() finite 1 -element with_non-empty_values IC-Ins-separated strict halting AMI-Struct over N
the InstructionsF of (Trivial-AMI N) is Relation-like non empty standard-ins homogeneous J/A-independent V55() set
S is Element of the InstructionsF of (Trivial-AMI N)
JumpPart S is Relation-like NAT -defined NAT -valued RAT -valued Function-like finite V40() V41() countable V121() V122() V123() V124() set
K50(S) is set
AddressPart K50(S) is set
[0,0,{}] is V22() V23() set
[[0,0],{}] is V22() set
{[0,0],{}} is non empty finite countable set
{{[0,0],{}},{[0,0]}} is non empty finite V36() with_non-empty_elements non empty-membered countable set
{[0,0,{}]} is Relation-like non empty V19() finite 1 -element standard-ins homogeneous J/A-independent V55() countable set
[0,0,0] is V22() V23() set
N is non empty non with_non-empty_elements set
Trivial-AMI N is non empty V67() finite 1 -element with_non-empty_values IC-Ins-separated strict halting AMI-Struct over N
the InstructionsF of (Trivial-AMI N) is Relation-like non empty standard-ins homogeneous J/A-independent V55() set
InsCodes the InstructionsF of (Trivial-AMI N) is non empty set
K60( the InstructionsF of (Trivial-AMI N)) is set
proj1 the InstructionsF of (Trivial-AMI N) is non empty set
proj1 (proj1 the InstructionsF of (Trivial-AMI N)) is set
S is Element of InsCodes the InstructionsF of (Trivial-AMI N)
JumpParts S is functional non empty with_common_domain product-like set
{ (JumpPart b1) where b1 is Element of the InstructionsF of (Trivial-AMI N) : InsCode b1 = S } is set
s is set
[0,0,{}] is V22() V23() set
[[0,0],{}] is V22() set
{[0,0],{}} is non empty finite countable set
{{[0,0],{}},{[0,0]}} is non empty finite V36() with_non-empty_elements non empty-membered countable set
{[0,0,{}]} is Relation-like non empty V19() finite 1 -element standard-ins homogeneous J/A-independent V55() countable set
[0,0,0] is V22() V23() set
I is Element of the InstructionsF of (Trivial-AMI N)
JumpPart I is Relation-like NAT -defined NAT -valued RAT -valued Function-like finite V40() V41() countable V121() V122() V123() V124() set
K50(I) is set
AddressPart K50(I) is set
InsCode I is epsilon-transitive epsilon-connected ordinal natural V28() V29() finite cardinal countable ext-real non negative Element of InsCodes the InstructionsF of (Trivial-AMI N)
K50(K50(I)) is set
s is set
I is Element of the InstructionsF of (Trivial-AMI N)
JumpPart I is Relation-like NAT -defined NAT -valued RAT -valued Function-like finite V40() V41() countable V121() V122() V123() V124() set
K50(I) is set
AddressPart K50(I) is set
InsCode I is epsilon-transitive epsilon-connected ordinal natural V28() V29() finite cardinal countable ext-real non negative Element of InsCodes the InstructionsF of (Trivial-AMI N)
K50(K50(I)) is set
N is non empty non with_non-empty_elements set
STC N is non empty finite with_non-empty_values IC-Ins-separated strict halting standard AMI-Struct over N
the InstructionsF of (STC N) is Relation-like non empty standard-ins homogeneous J/A-independent V55() set
S is ins-loc-free Element of the InstructionsF of (STC N)
JUMP S is Relation-like non-empty empty-yielding NAT -defined RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty V28() V29() finite finite-yielding V36() cardinal {} -element V40() V41() V42() initial Cardinal-yielding countable ext-real non positive non negative V103() V104() V105() V106() V107() V108() V109() V112() V113() V114() V115() V121() V122() V123() V124() Function-yielding V148() FuncSeq-like Element of K29(NAT)
{ (NIC (S,b1)) where b1 is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT : verum } is set
meet { (NIC (S,b1)) where b1 is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT : verum } is set
JumpPart S is Relation-like non-empty empty-yielding NAT -defined NAT -valued RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty V28() V29() finite finite-yielding V36() cardinal {} -element V40() V41() V42() initial Cardinal-yielding countable ext-real non positive non negative V103() V104() V105() V106() V107() V108() V109() V112() V113() V114() V115() V121() V122() V123() V124() Function-yielding V148() FuncSeq-like set
K50(S) is set
AddressPart K50(S) is set
proj2 (JumpPart S) is Relation-like non-empty empty-yielding NAT -defined RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty V19() V28() V29() finite finite-yielding V36() cardinal {} -element V40() V41() V42() with_non-empty_elements initial Cardinal-yielding countable ext-real non positive non negative V103() V104() V105() V106() V107() V108() V109() V112() V113() V114() V115() V121() V122() V123() V124() V125() V126() V127() V128() Function-yielding V148() FuncSeq-like set
N is non empty non with_non-empty_elements set
STC N is non empty finite with_non-empty_values IC-Ins-separated strict halting standard (N) AMI-Struct over N
N is non empty non with_non-empty_elements set
Trivial-AMI N is non empty V67() finite 1 -element with_non-empty_values IC-Ins-separated strict halting AMI-Struct over N
the InstructionsF of (Trivial-AMI N) is Relation-like non empty standard-ins homogeneous J/A-independent V55() set
S is Element of the InstructionsF of (Trivial-AMI N)
JUMP S is countable V103() V104() V105() V106() V107() V108() V112() Element of K29(NAT)
{ (NIC (S,b1)) where b1 is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT : verum } is set
meet { (NIC (S,b1)) where b1 is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT : verum } is set
P is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
NIC (S,P) is non empty countable V103() V104() V105() V106() V107() V108() V110() V112() Element of K29(NAT)
the carrier of (Trivial-AMI N) is non empty V19() finite 1 -element countable set
the_Values_of (Trivial-AMI N) is Relation-like non-empty non empty-yielding the carrier of (Trivial-AMI N) -defined Function-like non empty total set
the Object-Kind of (Trivial-AMI N) is Relation-like the carrier of (Trivial-AMI N) -defined N -valued Function-like non empty total V25( the carrier of (Trivial-AMI N),N) finite countable Element of K29(K30( the carrier of (Trivial-AMI N),N))
K30( the carrier of (Trivial-AMI N),N) is Relation-like set
K29(K30( the carrier of (Trivial-AMI N),N)) is set
the ValuesF of (Trivial-AMI N) is Relation-like N -defined Function-like non empty total set
the Object-Kind of (Trivial-AMI N) (#) the ValuesF of (Trivial-AMI N) is Relation-like the carrier of (Trivial-AMI N) -defined Function-like non empty total finite countable set
product (the_Values_of (Trivial-AMI N)) is functional non empty with_common_domain product-like set
{ (IC (Exec (S,b1))) where b1 is Relation-like the carrier of (Trivial-AMI N) -defined Function-like the_Values_of (Trivial-AMI N) -compatible non empty total Element of product (the_Values_of (Trivial-AMI N)) : IC b1 = P } is set
{P} is non empty V19() finite V36() 1 -element countable V103() V104() V105() V106() V107() V108() V110() V111() V112() V113() V114() set
N is non empty non with_non-empty_elements set
Trivial-AMI N is non empty V67() finite 1 -element with_non-empty_values IC-Ins-separated strict halting AMI-Struct over N
the InstructionsF of (Trivial-AMI N) is Relation-like non empty standard-ins homogeneous J/A-independent V55() set
S is Element of the InstructionsF of (Trivial-AMI N)
[0,0,{}] is V22() V23() set
[[0,0],{}] is V22() set
{[0,0],{}} is non empty finite countable set
{{[0,0],{}},{[0,0]}} is non empty finite V36() with_non-empty_elements non empty-membered countable set
{[0,0,{}]} is Relation-like non empty V19() finite 1 -element standard-ins homogeneous J/A-independent V55() countable set
[0,0,0] is V22() V23() set
JUMP S is Relation-like non-empty empty-yielding NAT -defined RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty V28() V29() finite finite-yielding V36() cardinal {} -element V40() V41() V42() initial Cardinal-yielding countable ext-real non positive non negative V103() V104() V105() V106() V107() V108() V109() V112() V113() V114() V115() V121() V122() V123() V124() Function-yielding V148() FuncSeq-like Element of K29(NAT)
{ (NIC (S,b1)) where b1 is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT : verum } is set
meet { (NIC (S,b1)) where b1 is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT : verum } is set
JumpPart S is Relation-like NAT -defined NAT -valued RAT -valued Function-like finite V40() V41() countable V121() V122() V123() V124() set
K50(S) is set
AddressPart K50(S) is set
proj2 (JumpPart S) is finite countable V103() V104() V105() V106() V107() V108() V112() V113() V114() set
N is non empty non with_non-empty_elements set
Trivial-AMI N is non empty V67() finite 1 -element with_non-empty_values IC-Ins-separated strict halting (N) AMI-Struct over N
N is non empty non with_non-empty_elements set
S is non empty with_non-empty_values IC-Ins-separated (N) AMI-Struct over N
the InstructionsF of S is Relation-like non empty standard-ins homogeneous J/A-independent V55() set
P 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 AMI-Struct over N
the InstructionsF of S is Relation-like non empty standard-ins homogeneous J/A-independent V55() set
P is Element of the InstructionsF of S
JUMP P is countable V103() V104() V105() V106() V107() V108() V112() Element of K29(NAT)
{ (NIC (P,b1)) where b1 is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT : verum } is set
meet { (NIC (P,b1)) where b1 is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT : verum } is set
s is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
NIC (P,s) is non empty countable V103() V104() V105() V106() V107() V108() V110() V112() Element of K29(NAT)
the carrier of S is non empty set
the_Values_of S is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
the Object-Kind of S is Relation-like the carrier of S -defined N -valued Function-like non empty total V25( the carrier of S,N) Element of K29(K30( the carrier of S,N))
K30( the carrier of S,N) is Relation-like set
K29(K30( the carrier of S,N)) is set
the ValuesF of S is Relation-like N -defined Function-like non empty total set
the Object-Kind of S (#) the ValuesF of S is Relation-like the carrier of S -defined Function-like non empty total set
product (the_Values_of S) is functional non empty with_common_domain product-like set
{ (IC (Exec (P,b1))) where b1 is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible non empty total Element of product (the_Values_of S) : IC b1 = s } is set
{s} is non empty V19() finite V36() 1 -element countable V103() V104() V105() V106() V107() V108() V110() V111() V112() V113() V114() set
N is non empty non with_non-empty_elements set
S is non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
the InstructionsF of S is Relation-like non empty standard-ins homogeneous J/A-independent V55() set
P is halting non sequential Element of the InstructionsF of S
JUMP P is countable V103() V104() V105() V106() V107() V108() V112() Element of K29(NAT)
{ (NIC (P,b1)) where b1 is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT : verum } is set
meet { (NIC (P,b1)) where b1 is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT : verum } is set
N is non empty non with_non-empty_elements set
S is non empty with_non-empty_values IC-Ins-separated halting (N) AMI-Struct over N
the InstructionsF of S is Relation-like non empty standard-ins homogeneous J/A-independent V55() set
P is (N,S) Element of the InstructionsF of S
JUMP P is countable V103() V104() V105() V106() V107() V108() V112() Element of K29(NAT)
{ (NIC (P,b1)) where b1 is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT : verum } is set
meet { (NIC (P,b1)) where b1 is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT : verum } is set
JumpPart P is Relation-like NAT -defined NAT -valued RAT -valued Function-like finite V40() V41() countable V121() V122() V123() V124() set
K50(P) is set
AddressPart K50(P) is set
proj2 (JumpPart P) is finite countable V103() V104() V105() V106() V107() V108() V112() V113() V114() set
N is non empty non with_non-empty_elements set
S is non empty with_non-empty_values IC-Ins-separated (N) AMI-Struct over N
the InstructionsF of S is Relation-like non empty standard-ins homogeneous J/A-independent V55() set
P is (N,S) Element of the InstructionsF of S
JUMP P is countable V103() V104() V105() V106() V107() V108() V112() Element of K29(NAT)
{ (NIC (P,b1)) where b1 is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT : verum } is set
meet { (NIC (P,b1)) where b1 is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT : verum } is set
JumpPart P is Relation-like NAT -defined NAT -valued RAT -valued Function-like finite V40() V41() countable V121() V122() V123() V124() set
K50(P) is set
AddressPart K50(P) is set
proj2 (JumpPart P) is finite countable V103() V104() V105() V106() V107() V108() V112() V113() V114() set
N is non empty non with_non-empty_elements set
S is non empty with_non-empty_values IC-Ins-separated (N) AMI-Struct over N
the InstructionsF of S is Relation-like non empty standard-ins homogeneous J/A-independent V55() set
P is (N,S) Element of the InstructionsF of S
JUMP P is countable V103() V104() V105() V106() V107() V108() V112() Element of K29(NAT)
{ (NIC (P,b1)) where b1 is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT : verum } is set
meet { (NIC (P,b1)) where b1 is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT : verum } is set
JumpPart P is Relation-like NAT -defined NAT -valued RAT -valued Function-like finite V40() V41() countable V121() V122() V123() V124() set
K50(P) is set
AddressPart K50(P) is set
proj2 (JumpPart P) is finite countable V103() V104() V105() V106() V107() V108() V112() V113() V114() set
N is non empty non with_non-empty_elements set
S is non empty with_non-empty_values IC-Ins-separated halting standard AMI-Struct over N
Stop S is Relation-like NAT -defined the InstructionsF of S -valued T-Sequence-like Function-like constant non empty V19() finite 1 -element initial non halt-free halt-ending unique-halt countable set
the InstructionsF of S is Relation-like non empty standard-ins homogeneous J/A-independent V55() set
halt S is halting non sequential Element of the InstructionsF of S
halt the InstructionsF of S is ins-loc-free Element of the InstructionsF of S
K240((halt S)) is Relation-like NAT -defined the InstructionsF of S -valued the InstructionsF of S -valued T-Sequence-like Function-like constant non empty V19() finite 1 -element initial unique-halt countable set
0 .--> (halt S) is Relation-like NAT -defined {0} -defined the InstructionsF of S -valued the InstructionsF of S -valued Function-like one-to-one constant non empty V19() finite 1 -element unique-halt countable set
{0} --> (halt S) is Relation-like {0} -defined the InstructionsF of S -valued {(halt S)} -valued Function-like constant non empty total V25({0},{(halt S)}) finite countable Element of K29(K30({0},{(halt S)}))
{(halt S)} is non empty V19() finite 1 -element countable set
K30({0},{(halt S)}) is Relation-like finite countable set
K29(K30({0},{(halt S)})) is finite V36() countable set
N is non empty non with_non-empty_elements set
S is non empty with_non-empty_values IC-Ins-separated halting (N) AMI-Struct over N
the InstructionsF of S is Relation-like non empty standard-ins homogeneous J/A-independent V55() set
P is ins-loc-free halting non sequential (N,S) Element of the InstructionsF of S
s is epsilon-transitive epsilon-connected ordinal natural V28() V29() finite cardinal countable ext-real non negative set
IncAddr (P,s) is (N,S) Element of the InstructionsF of S
S is non empty non with_non-empty_elements set
P is non empty with_non-empty_values IC-Ins-separated halting standard (S) AMI-Struct over S
the InstructionsF of P is Relation-like non empty standard-ins homogeneous J/A-independent V55() set
s is (S,P) Element of the InstructionsF of P
N is epsilon-transitive epsilon-connected ordinal natural V28() V29() finite cardinal countable ext-real non negative set
IncAddr (s,N) is (S,P) 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 halting AMI-Struct over N
the InstructionsF of S is Relation-like non empty standard-ins homogeneous J/A-independent V55() set
N is non empty non with_non-empty_elements set
N is non empty non with_non-empty_elements set
S is non empty with_non-empty_values IC-Ins-separated halting (N) AMI-Struct over N
the InstructionsF of S is Relation-like non empty standard-ins homogeneous J/A-independent V55() set
P is (N,S) Element of the InstructionsF of S
the carrier of S is non empty set
the_Values_of S is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
the Object-Kind of S is Relation-like the carrier of S -defined N -valued Function-like non empty total V25( the carrier of S,N) Element of K29(K30( the carrier of S,N))
K30( the carrier of S,N) is Relation-like set
K29(K30( the carrier of S,N)) is set
the ValuesF of S is Relation-like N -defined Function-like non empty total set
the Object-Kind of S (#) the ValuesF of S is Relation-like the carrier of S -defined Function-like non empty total set
s is epsilon-transitive epsilon-connected ordinal natural V28() V29() finite cardinal countable ext-real non negative set
IncAddr (P,s) is (N,S) Element of the InstructionsF of S
I is epsilon-transitive epsilon-connected ordinal natural V28() V29() finite cardinal countable ext-real non negative set
s + I is epsilon-transitive epsilon-connected ordinal natural V28() V29() finite cardinal countable ext-real non negative set
IncAddr (P,(s + I)) is (N,S) Element of the InstructionsF of S
P1 is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible non empty total set
Exec ((IncAddr (P,s)),P1) is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible non empty total set
product ( the Object-Kind of S (#) the ValuesF of S) is functional with_common_domain product-like set
K80((product ( the Object-Kind of S (#) the ValuesF of S)),(product ( the Object-Kind of S (#) the ValuesF of S))) is functional non empty set
the Execution of S is Relation-like the InstructionsF of S -defined K80((product ( the Object-Kind of S (#) the ValuesF of S)),(product ( the Object-Kind of S (#) the ValuesF of S))) -valued Function-like non empty total V25( the InstructionsF of S,K80((product ( the Object-Kind of S (#) the ValuesF of S)),(product ( the Object-Kind of S (#) the ValuesF of S)))) Function-yielding V148() Element of K29(K30( the InstructionsF of S,K80((product ( the Object-Kind of S (#) the ValuesF of S)),(product ( the Object-Kind of S (#) the ValuesF of S)))))
K30( the InstructionsF of S,K80((product ( the Object-Kind of S (#) the ValuesF of S)),(product ( the Object-Kind of S (#) the ValuesF of S)))) is Relation-like set
K29(K30( the InstructionsF of S,K80((product ( the Object-Kind of S (#) the ValuesF of S)),(product ( the Object-Kind of S (#) the ValuesF of S))))) is set
the Execution of S . (IncAddr (P,s)) is Relation-like Function-like Element of K80((product ( the Object-Kind of S (#) the ValuesF of S)),(product ( the Object-Kind of S (#) the ValuesF of S)))
( the Execution of S . (IncAddr (P,s))) . P1 is Relation-like Function-like set
IC (Exec ((IncAddr (P,s)),P1)) is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
IC is V69(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
(Exec ((IncAddr (P,s)),P1)) . (IC ) is set
(IC (Exec ((IncAddr (P,s)),P1))) + I is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
IncIC (P1,I) is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible non empty total set
IC P1 is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
P1 . (IC ) is set
(IC P1) + I is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
Start-At (((IC P1) + I),S) is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible non empty finite countable (IC P1) + I -started set
(IC ) .--> ((IC P1) + I) is Relation-like the carrier of S -defined {(IC )} -defined NAT -valued RAT -valued INT -valued Function-like one-to-one constant non empty V19() finite 1 -element Cardinal-yielding countable V121() V122() V123() V124() V125() V126() V127() V128() set
{(IC )} is non empty V19() finite 1 -element countable set
{(IC )} --> ((IC P1) + I) is Relation-like {(IC )} -defined NAT -valued RAT -valued INT -valued {((IC P1) + I)} -valued Function-like constant non empty total V25({(IC )},{((IC P1) + I)}) finite Cardinal-yielding countable V121() V122() V123() V124() Element of K29(K30({(IC )},{((IC P1) + I)}))
{((IC P1) + I)} is non empty V19() finite V36() 1 -element countable V103() V104() V105() V106() V107() V108() V110() V111() V112() V113() V114() set
K30({(IC )},{((IC P1) + I)}) is Relation-like RAT -valued INT -valued finite countable V121() V122() V123() V124() set
K29(K30({(IC )},{((IC P1) + I)})) is finite V36() countable set
P1 +* (Start-At (((IC P1) + I),S)) is Relation-like the carrier of S -defined the carrier of S -defined Function-like the_Values_of S -compatible the_Values_of S -compatible non empty total (IC P1) + I -started set
Exec ((IncAddr (P,(s + I))),(IncIC (P1,I))) is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible non empty total set
the Execution of S . (IncAddr (P,(s + I))) is Relation-like Function-like Element of K80((product ( the Object-Kind of S (#) the ValuesF of S)),(product ( the Object-Kind of S (#) the ValuesF of S)))
( the Execution of S . (IncAddr (P,(s + I)))) . (IncIC (P1,I)) is Relation-like Function-like set
IC (Exec ((IncAddr (P,(s + I))),(IncIC (P1,I)))) is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
(Exec ((IncAddr (P,(s + I))),(IncIC (P1,I)))) . (IC ) is set
proj1 ((IC ) .--> ((IC P1) + I)) is non empty V19() finite 1 -element countable set
IC (IncIC (P1,I)) is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
(IncIC (P1,I)) . (IC ) is set
((IC ) .--> ((IC P1) + I)) . (IC ) is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V120() set
Exec (P,(IncIC (P1,I))) is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible non empty total set
the Execution of S . P is Relation-like Function-like Element of K80((product ( the Object-Kind of S (#) the ValuesF of S)),(product ( the Object-Kind of S (#) the ValuesF of S)))
( the Execution of S . P) . (IncIC (P1,I)) is Relation-like Function-like set
IC (Exec (P,(IncIC (P1,I)))) is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
(Exec (P,(IncIC (P1,I)))) . (IC ) is set
succ (IC (IncIC (P1,I))) is epsilon-transitive epsilon-connected ordinal natural non empty V28() V29() finite cardinal countable ext-real positive non negative set
(IC (IncIC (P1,I))) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V28() V29() V30() finite cardinal countable ext-real positive non negative V103() V104() V105() V106() V107() V108() V110() V111() V112() V113() V114() V120() Element of NAT
(IC P1) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V28() V29() V30() finite cardinal countable ext-real positive non negative V103() V104() V105() V106() V107() V108() V110() V111() V112() V113() V114() V120() Element of NAT
((IC P1) + 1) + I is epsilon-transitive epsilon-connected ordinal natural non empty V28() V29() V30() finite cardinal countable ext-real positive non negative V103() V104() V105() V106() V107() V108() V110() V111() V112() V113() V114() V120() Element of NAT
Exec (P,P1) is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible non empty total set
( the Execution of S . P) . P1 is Relation-like Function-like set
IC (Exec (P,P1)) is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
(Exec (P,P1)) . (IC ) is set
succ (IC P1) is epsilon-transitive epsilon-connected ordinal natural non empty V28() V29() finite cardinal countable ext-real positive non negative set
(IC P1) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V28() V29() V30() finite cardinal countable ext-real positive non negative V103() V104() V105() V106() V107() V108() V110() V111() V112() V113() V114() V120() Element of NAT
IncAddr ((IncAddr (P,s)),I) is (N,S) Element of the InstructionsF of S
Exec ((IncAddr ((IncAddr (P,s)),I)),(IncIC (P1,I))) is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible non empty total set
the Execution of S . (IncAddr ((IncAddr (P,s)),I)) is Relation-like Function-like Element of K80((product ( the Object-Kind of S (#) the ValuesF of S)),(product ( the Object-Kind of S (#) the ValuesF of S)))
( the Execution of S . (IncAddr ((IncAddr (P,s)),I))) . (IncIC (P1,I)) is Relation-like Function-like set
IC (Exec ((IncAddr ((IncAddr (P,s)),I)),(IncIC (P1,I)))) is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
(Exec ((IncAddr ((IncAddr (P,s)),I)),(IncIC (P1,I)))) . (IC ) is set
N is non empty non with_non-empty_elements set
S is non empty with_non-empty_values IC-Ins-separated halting (N) AMI-Struct over N
the InstructionsF of S is Relation-like non empty standard-ins homogeneous J/A-independent V55() set
P is (N,S) Element of the InstructionsF of S
the carrier of S is non empty set
the_Values_of S is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
the Object-Kind of S is Relation-like the carrier of S -defined N -valued Function-like non empty total V25( the carrier of S,N) Element of K29(K30( the carrier of S,N))
K30( the carrier of S,N) is Relation-like set
K29(K30( the carrier of S,N)) is set
the ValuesF of S is Relation-like N -defined Function-like non empty total set
the Object-Kind of S (#) the ValuesF of S is Relation-like the carrier of S -defined Function-like non empty total set
s is epsilon-transitive epsilon-connected ordinal natural V28() V29() finite cardinal countable ext-real non negative set
IncAddr (P,s) is (N,S) Element of the InstructionsF of S
I is epsilon-transitive epsilon-connected ordinal natural V28() V29() finite cardinal countable ext-real non negative set
s + I is epsilon-transitive epsilon-connected ordinal natural V28() V29() finite cardinal countable ext-real non negative set
IncAddr (P,(s + I)) is (N,S) Element of the InstructionsF of S
P1 is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible non empty total set
Exec ((IncAddr (P,s)),P1) is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible non empty total set
product ( the Object-Kind of S (#) the ValuesF of S) is functional with_common_domain product-like set
K80((product ( the Object-Kind of S (#) the ValuesF of S)),(product ( the Object-Kind of S (#) the ValuesF of S))) is functional non empty set
the Execution of S is Relation-like the InstructionsF of S -defined K80((product ( the Object-Kind of S (#) the ValuesF of S)),(product ( the Object-Kind of S (#) the ValuesF of S))) -valued Function-like non empty total V25( the InstructionsF of S,K80((product ( the Object-Kind of S (#) the ValuesF of S)),(product ( the Object-Kind of S (#) the ValuesF of S)))) Function-yielding V148() Element of K29(K30( the InstructionsF of S,K80((product ( the Object-Kind of S (#) the ValuesF of S)),(product ( the Object-Kind of S (#) the ValuesF of S)))))
K30( the InstructionsF of S,K80((product ( the Object-Kind of S (#) the ValuesF of S)),(product ( the Object-Kind of S (#) the ValuesF of S)))) is Relation-like set
K29(K30( the InstructionsF of S,K80((product ( the Object-Kind of S (#) the ValuesF of S)),(product ( the Object-Kind of S (#) the ValuesF of S))))) is set
the Execution of S . (IncAddr (P,s)) is Relation-like Function-like Element of K80((product ( the Object-Kind of S (#) the ValuesF of S)),(product ( the Object-Kind of S (#) the ValuesF of S)))
( the Execution of S . (IncAddr (P,s))) . P1 is Relation-like Function-like set
IC (Exec ((IncAddr (P,s)),P1)) is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
IC is V69(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
(Exec ((IncAddr (P,s)),P1)) . (IC ) is set
(IC (Exec ((IncAddr (P,s)),P1))) + I is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
IncIC (P1,I) is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible non empty total set
IC P1 is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
P1 . (IC ) is set
(IC P1) + I is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
Start-At (((IC P1) + I),S) is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible non empty finite countable (IC P1) + I -started set
(IC ) .--> ((IC P1) + I) is Relation-like the carrier of S -defined {(IC )} -defined NAT -valued RAT -valued INT -valued Function-like one-to-one constant non empty V19() finite 1 -element Cardinal-yielding countable V121() V122() V123() V124() V125() V126() V127() V128() set
{(IC )} is non empty V19() finite 1 -element countable set
{(IC )} --> ((IC P1) + I) is Relation-like {(IC )} -defined NAT -valued RAT -valued INT -valued {((IC P1) + I)} -valued Function-like constant non empty total V25({(IC )},{((IC P1) + I)}) finite Cardinal-yielding countable V121() V122() V123() V124() Element of K29(K30({(IC )},{((IC P1) + I)}))
{((IC P1) + I)} is non empty V19() finite V36() 1 -element countable V103() V104() V105() V106() V107() V108() V110() V111() V112() V113() V114() set
K30({(IC )},{((IC P1) + I)}) is Relation-like RAT -valued INT -valued finite countable V121() V122() V123() V124() set
K29(K30({(IC )},{((IC P1) + I)})) is finite V36() countable set
P1 +* (Start-At (((IC P1) + I),S)) is Relation-like the carrier of S -defined the carrier of S -defined Function-like the_Values_of S -compatible the_Values_of S -compatible non empty total (IC P1) + I -started set
Exec ((IncAddr (P,(s + I))),(IncIC (P1,I))) is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible non empty total set
the Execution of S . (IncAddr (P,(s + I))) is Relation-like Function-like Element of K80((product ( the Object-Kind of S (#) the ValuesF of S)),(product ( the Object-Kind of S (#) the ValuesF of S)))
( the Execution of S . (IncAddr (P,(s + I)))) . (IncIC (P1,I)) is Relation-like Function-like set
IC (Exec ((IncAddr (P,(s + I))),(IncIC (P1,I)))) is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
(Exec ((IncAddr (P,(s + I))),(IncIC (P1,I)))) . (IC ) is set
proj1 ((IC ) .--> ((IC P1) + I)) is non empty V19() finite 1 -element countable set
((IC ) .--> ((IC P1) + I)) . (IC ) is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V120() set
IC (IncIC (P1,I)) is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
(IncIC (P1,I)) . (IC ) is set
N is non empty non with_non-empty_elements set
STC N is non empty finite with_non-empty_values IC-Ins-separated strict halting standard (N) AMI-Struct over N
the InstructionsF of (STC N) is Relation-like non empty standard-ins homogeneous J/A-independent V55() set
S is ins-loc-free (N, STC N) Element of the InstructionsF of (STC N)
the carrier of (STC N) is non empty finite countable set
the_Values_of (STC N) is Relation-like non-empty non empty-yielding the carrier of (STC N) -defined Function-like non empty total set
the Object-Kind of (STC N) is Relation-like the carrier of (STC N) -defined N -valued Function-like non empty total V25( the carrier of (STC N),N) finite countable Element of K29(K30( the carrier of (STC N),N))
K30( the carrier of (STC N),N) is Relation-like set
K29(K30( the carrier of (STC N),N)) is set
the ValuesF of (STC N) is Relation-like N -defined Function-like non empty total set
the Object-Kind of (STC N) (#) the ValuesF of (STC N) is Relation-like the carrier of (STC N) -defined Function-like non empty total finite countable set
P is epsilon-transitive epsilon-connected ordinal natural V28() V29() finite cardinal countable ext-real non negative set
IncAddr (S,P) is ins-loc-free (N, STC N) Element of the InstructionsF of (STC N)
s is epsilon-transitive epsilon-connected ordinal natural V28() V29() finite cardinal countable ext-real non negative set
P + s is epsilon-transitive epsilon-connected ordinal natural V28() V29() finite cardinal countable ext-real non negative set
IncAddr (S,(P + s)) is ins-loc-free (N, STC N) Element of the InstructionsF of (STC N)
I is Relation-like the carrier of (STC N) -defined Function-like the_Values_of (STC N) -compatible non empty total set
Exec ((IncAddr (S,P)),I) is Relation-like the carrier of (STC N) -defined Function-like the_Values_of (STC N) -compatible non empty total set
product ( the Object-Kind of (STC N) (#) the ValuesF of (STC N)) is functional with_common_domain product-like set
K80((product ( the Object-Kind of (STC N) (#) the ValuesF of (STC N))),(product ( the Object-Kind of (STC N) (#) the ValuesF of (STC N)))) is functional non empty set
the Execution of (STC N) is Relation-like the InstructionsF of (STC N) -defined K80((product ( the Object-Kind of (STC N) (#) the ValuesF of (STC N))),(product ( the Object-Kind of (STC N) (#) the ValuesF of (STC N)))) -valued Function-like non empty total V25( the InstructionsF of (STC N),K80((product ( the Object-Kind of (STC N) (#) the ValuesF of (STC N))),(product ( the Object-Kind of (STC N) (#) the ValuesF of (STC N))))) Function-yielding V148() Element of K29(K30( the InstructionsF of (STC N),K80((product ( the Object-Kind of (STC N) (#) the ValuesF of (STC N))),(product ( the Object-Kind of (STC N) (#) the ValuesF of (STC N))))))
K30( the InstructionsF of (STC N),K80((product ( the Object-Kind of (STC N) (#) the ValuesF of (STC N))),(product ( the Object-Kind of (STC N) (#) the ValuesF of (STC N))))) is Relation-like set
K29(K30( the InstructionsF of (STC N),K80((product ( the Object-Kind of (STC N) (#) the ValuesF of (STC N))),(product ( the Object-Kind of (STC N) (#) the ValuesF of (STC N)))))) is set
the Execution of (STC N) . (IncAddr (S,P)) is Relation-like Function-like Element of K80((product ( the Object-Kind of (STC N) (#) the ValuesF of (STC N))),(product ( the Object-Kind of (STC N) (#) the ValuesF of (STC N))))
( the Execution of (STC N) . (IncAddr (S,P))) . I is Relation-like Function-like set
IC (Exec ((IncAddr (S,P)),I)) is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
IC is V69( STC N) Element of the carrier of (STC N)
the ZeroF of (STC N) is Element of the carrier of (STC N)
(Exec ((IncAddr (S,P)),I)) . (IC ) is set
(IC (Exec ((IncAddr (S,P)),I))) + s is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
IncIC (I,s) is Relation-like the carrier of (STC N) -defined Function-like the_Values_of (STC N) -compatible non empty total set
IC I is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
I . (IC ) is set
(IC I) + s is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
Start-At (((IC I) + s),(STC N)) is Relation-like the carrier of (STC N) -defined Function-like the_Values_of (STC N) -compatible non empty finite countable (IC I) + s -started set
(IC ) .--> ((IC I) + s) is Relation-like the carrier of (STC N) -defined {(IC )} -defined NAT -valued RAT -valued INT -valued Function-like one-to-one constant non empty V19() finite 1 -element Cardinal-yielding countable V121() V122() V123() V124() V125() V126() V127() V128() set
{(IC )} is non empty V19() finite 1 -element countable set
{(IC )} --> ((IC I) + s) is Relation-like {(IC )} -defined NAT -valued RAT -valued INT -valued {((IC I) + s)} -valued Function-like constant non empty total V25({(IC )},{((IC I) + s)}) finite Cardinal-yielding countable V121() V122() V123() V124() Element of K29(K30({(IC )},{((IC I) + s)}))
{((IC I) + s)} is non empty V19() finite V36() 1 -element countable V103() V104() V105() V106() V107() V108() V110() V111() V112() V113() V114() set
K30({(IC )},{((IC I) + s)}) is Relation-like RAT -valued INT -valued finite countable V121() V122() V123() V124() set
K29(K30({(IC )},{((IC I) + s)})) is finite V36() countable set
I +* (Start-At (((IC I) + s),(STC N))) is Relation-like the carrier of (STC N) -defined the carrier of (STC N) -defined Function-like the_Values_of (STC N) -compatible the_Values_of (STC N) -compatible non empty total (IC I) + s -started set
Exec ((IncAddr (S,(P + s))),(IncIC (I,s))) is Relation-like the carrier of (STC N) -defined Function-like the_Values_of (STC N) -compatible non empty total set
the Execution of (STC N) . (IncAddr (S,(P + s))) is Relation-like Function-like Element of K80((product ( the Object-Kind of (STC N) (#) the ValuesF of (STC N))),(product ( the Object-Kind of (STC N) (#) the ValuesF of (STC N))))
( the Execution of (STC N) . (IncAddr (S,(P + s)))) . (IncIC (I,s)) is Relation-like Function-like set
IC (Exec ((IncAddr (S,(P + s))),(IncIC (I,s)))) is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
(Exec ((IncAddr (S,(P + s))),(IncIC (I,s)))) . (IC ) is set
proj1 ((IC ) .--> ((IC I) + s)) is non empty V19() finite 1 -element countable set
IC (IncIC (I,s)) is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
(IncIC (I,s)) . (IC ) is set
((IC ) .--> ((IC I) + s)) . (IC ) is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V120() set
InsCode S is epsilon-transitive epsilon-connected ordinal natural V28() V29() finite cardinal countable ext-real non negative Element of InsCodes the InstructionsF of (STC N)
InsCodes the InstructionsF of (STC N) is non empty set
K60( the InstructionsF of (STC N)) is set
proj1 the InstructionsF of (STC N) is non empty set
proj1 (proj1 the InstructionsF of (STC N)) is set
K50(S) is set
K50(K50(S)) is set
IncAddr (S,s) is ins-loc-free (N, STC N) Element of the InstructionsF of (STC N)
InsCode (IncAddr (S,s)) is epsilon-transitive epsilon-connected ordinal natural V28() V29() finite cardinal countable ext-real non negative Element of InsCodes the InstructionsF of (STC N)
K50((IncAddr (S,s))) is set
K50(K50((IncAddr (S,s)))) is set
Exec (S,I) is Relation-like the carrier of (STC N) -defined Function-like the_Values_of (STC N) -compatible non empty total set
the Execution of (STC N) . S is Relation-like Function-like Element of K80((product ( the Object-Kind of (STC N) (#) the ValuesF of (STC N))),(product ( the Object-Kind of (STC N) (#) the ValuesF of (STC N))))
( the Execution of (STC N) . S) . I is Relation-like Function-like set
IC (Exec (S,I)) is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
(Exec (S,I)) . (IC ) is set
succ (IC I) is epsilon-transitive epsilon-connected ordinal natural non empty V28() V29() finite cardinal countable ext-real positive non negative set
(IC I) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V28() V29() V30() finite cardinal countable ext-real positive non negative V103() V104() V105() V106() V107() V108() V110() V111() V112() V113() V114() V120() Element of NAT
(IC I) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V28() V29() V30() finite cardinal countable ext-real positive non negative V103() V104() V105() V106() V107() V108() V110() V111() V112() V113() V114() V120() Element of NAT
succ (IC (IncIC (I,s))) is epsilon-transitive epsilon-connected ordinal natural non empty V28() V29() finite cardinal countable ext-real positive non negative set
(IC (IncIC (I,s))) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V28() V29() V30() finite cardinal countable ext-real positive non negative V103() V104() V105() V106() V107() V108() V110() V111() V112() V113() V114() V120() Element of NAT
IncAddr ((IncAddr (S,P)),s) is ins-loc-free (N, STC N) Element of the InstructionsF of (STC N)
Exec ((IncAddr ((IncAddr (S,P)),s)),(IncIC (I,s))) is Relation-like the carrier of (STC N) -defined Function-like the_Values_of (STC N) -compatible non empty total set
the Execution of (STC N) . (IncAddr ((IncAddr (S,P)),s)) is Relation-like Function-like Element of K80((product ( the Object-Kind of (STC N) (#) the ValuesF of (STC N))),(product ( the Object-Kind of (STC N) (#) the ValuesF of (STC N))))
( the Execution of (STC N) . (IncAddr ((IncAddr (S,P)),s))) . (IncIC (I,s)) is Relation-like Function-like set
IC (Exec ((IncAddr ((IncAddr (S,P)),s)),(IncIC (I,s)))) is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
(Exec ((IncAddr ((IncAddr (S,P)),s)),(IncIC (I,s)))) . (IC ) is set
InsCode S is epsilon-transitive epsilon-connected ordinal natural V28() V29() finite cardinal countable ext-real non negative Element of InsCodes the InstructionsF of (STC N)
InsCodes the InstructionsF of (STC N) is non empty set
K60( the InstructionsF of (STC N)) is set
proj1 the InstructionsF of (STC N) is non empty set
proj1 (proj1 the InstructionsF of (STC N)) is set
K50(S) is set
K50(K50(S)) is set
IncAddr ((IncAddr (S,P)),s) is ins-loc-free (N, STC N) Element of the InstructionsF of (STC N)
Exec ((IncAddr ((IncAddr (S,P)),s)),(IncIC (I,s))) is Relation-like the carrier of (STC N) -defined Function-like the_Values_of (STC N) -compatible non empty total set
the Execution of (STC N) . (IncAddr ((IncAddr (S,P)),s)) is Relation-like Function-like Element of K80((product ( the Object-Kind of (STC N) (#) the ValuesF of (STC N))),(product ( the Object-Kind of (STC N) (#) the ValuesF of (STC N))))
( the Execution of (STC N) . (IncAddr ((IncAddr (S,P)),s))) . (IncIC (I,s)) is Relation-like Function-like set
IC (Exec ((IncAddr ((IncAddr (S,P)),s)),(IncIC (I,s)))) is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
(Exec ((IncAddr ((IncAddr (S,P)),s)),(IncIC (I,s)))) . (IC ) is set
InsCode S is epsilon-transitive epsilon-connected ordinal natural V28() V29() finite cardinal countable ext-real non negative Element of InsCodes the InstructionsF of (STC N)
InsCodes the InstructionsF of (STC N) is non empty set
K60( the InstructionsF of (STC N)) is set
proj1 the InstructionsF of (STC N) is non empty set
proj1 (proj1 the InstructionsF of (STC N)) is set
K50(S) is set
K50(K50(S)) is set
N is non empty non with_non-empty_elements set
STC N is non empty finite with_non-empty_values IC-Ins-separated strict halting standard (N) (N) AMI-Struct over N
N is non empty non with_non-empty_elements set
STC N is non empty finite with_non-empty_values IC-Ins-separated strict halting standard (N) (N) AMI-Struct over N
N is non empty non with_non-empty_elements set
S is non empty with_non-empty_values IC-Ins-separated halting (N) AMI-Struct over N
the InstructionsF of S is Relation-like non empty standard-ins homogeneous J/A-independent V55() set
P 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 halting (N) AMI-Struct over N
the InstructionsF of S is Relation-like non empty standard-ins homogeneous J/A-independent V55() set
the ins-loc-free halting non sequential (N,S) (N,S) Element of the InstructionsF of S is ins-loc-free halting non sequential (N,S) (N,S) 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 halting (N) AMI-Struct over N
the InstructionsF of S is Relation-like non empty standard-ins homogeneous J/A-independent V55() set
the carrier of S is non empty set
the_Values_of S is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
the Object-Kind of S is Relation-like the carrier of S -defined N -valued Function-like non empty total V25( the carrier of S,N) Element of K29(K30( the carrier of S,N))
K30( the carrier of S,N) is Relation-like set
K29(K30( the carrier of S,N)) is set
the ValuesF of S is Relation-like N -defined Function-like non empty total set
the Object-Kind of S (#) the ValuesF of S is Relation-like the carrier of S -defined Function-like non empty total set
P is (N,S) (N,S) Element of the InstructionsF of S
s is epsilon-transitive epsilon-connected ordinal natural V28() V29() finite cardinal countable ext-real non negative set
IncAddr (P,s) is (N,S) Element of the InstructionsF of S
I is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible non empty total set
Exec (P,I) is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible non empty total set
product ( the Object-Kind of S (#) the ValuesF of S) is functional with_common_domain product-like set
K80((product ( the Object-Kind of S (#) the ValuesF of S)),(product ( the Object-Kind of S (#) the ValuesF of S))) is functional non empty set
the Execution of S is Relation-like the InstructionsF of S -defined K80((product ( the Object-Kind of S (#) the ValuesF of S)),(product ( the Object-Kind of S (#) the ValuesF of S))) -valued Function-like non empty total V25( the InstructionsF of S,K80((product ( the Object-Kind of S (#) the ValuesF of S)),(product ( the Object-Kind of S (#) the ValuesF of S)))) Function-yielding V148() Element of K29(K30( the InstructionsF of S,K80((product ( the Object-Kind of S (#) the ValuesF of S)),(product ( the Object-Kind of S (#) the ValuesF of S)))))
K30( the InstructionsF of S,K80((product ( the Object-Kind of S (#) the ValuesF of S)),(product ( the Object-Kind of S (#) the ValuesF of S)))) is Relation-like set
K29(K30( the InstructionsF of S,K80((product ( the Object-Kind of S (#) the ValuesF of S)),(product ( the Object-Kind of S (#) the ValuesF of S))))) is set
the Execution of S . P is Relation-like Function-like Element of K80((product ( the Object-Kind of S (#) the ValuesF of S)),(product ( the Object-Kind of S (#) the ValuesF of S)))
( the Execution of S . P) . I is Relation-like Function-like set
IC (Exec (P,I)) is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
IC is V69(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
(Exec (P,I)) . (IC ) is set
(IC (Exec (P,I))) + s is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
IncIC (I,s) is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible non empty total set
IC I is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
I . (IC ) is set
(IC I) + s is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
Start-At (((IC I) + s),S) is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible non empty finite countable (IC I) + s -started set
(IC ) .--> ((IC I) + s) is Relation-like the carrier of S -defined {(IC )} -defined NAT -valued RAT -valued INT -valued Function-like one-to-one constant non empty V19() finite 1 -element Cardinal-yielding countable V121() V122() V123() V124() V125() V126() V127() V128() set
{(IC )} is non empty V19() finite 1 -element countable set
{(IC )} --> ((IC I) + s) is Relation-like {(IC )} -defined NAT -valued RAT -valued INT -valued {((IC I) + s)} -valued Function-like constant non empty total V25({(IC )},{((IC I) + s)}) finite Cardinal-yielding countable V121() V122() V123() V124() Element of K29(K30({(IC )},{((IC I) + s)}))
{((IC I) + s)} is non empty V19() finite V36() 1 -element countable V103() V104() V105() V106() V107() V108() V110() V111() V112() V113() V114() set
K30({(IC )},{((IC I) + s)}) is Relation-like RAT -valued INT -valued finite countable V121() V122() V123() V124() set
K29(K30({(IC )},{((IC I) + s)})) is finite V36() countable set
I +* (Start-At (((IC I) + s),S)) is Relation-like the carrier of S -defined the carrier of S -defined Function-like the_Values_of S -compatible the_Values_of S -compatible non empty total (IC I) + s -started set
Exec ((IncAddr (P,s)),(IncIC (I,s))) is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible non empty total set
the Execution of S . (IncAddr (P,s)) is Relation-like Function-like Element of K80((product ( the Object-Kind of S (#) the ValuesF of S)),(product ( the Object-Kind of S (#) the ValuesF of S)))
( the Execution of S . (IncAddr (P,s))) . (IncIC (I,s)) is Relation-like Function-like set
IC (Exec ((IncAddr (P,s)),(IncIC (I,s)))) is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
(Exec ((IncAddr (P,s)),(IncIC (I,s)))) . (IC ) is set
s + 0 is epsilon-transitive epsilon-connected ordinal natural V28() V29() finite cardinal countable ext-real non negative set
IncAddr (P,0) is (N,S) Element of the InstructionsF of S
Exec ((IncAddr (P,0)),I) is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible non empty total set
the Execution of S . (IncAddr (P,0)) is Relation-like Function-like Element of K80((product ( the Object-Kind of S (#) the ValuesF of S)),(product ( the Object-Kind of S (#) the ValuesF of S)))
( the Execution of S . (IncAddr (P,0))) . I is Relation-like Function-like set
IC (Exec ((IncAddr (P,0)),I)) is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
(Exec ((IncAddr (P,0)),I)) . (IC ) is set
(IC (Exec ((IncAddr (P,0)),I))) + s is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
N is non empty non with_non-empty_elements set
S is non empty with_non-empty_values IC-Ins-separated halting standard (N) (N) AMI-Struct over N
the InstructionsF of S is Relation-like non empty standard-ins homogeneous J/A-independent V55() set
P is Relation-like NAT -defined the InstructionsF of S -valued T-Sequence-like Function-like non empty finite initial countable really-closed V98(N,S) set
s is Relation-like NAT -defined the InstructionsF of S -valued T-Sequence-like Function-like non empty finite initial countable really-closed V98(N,S) set
P ';' s is Relation-like NAT -defined the InstructionsF of S -valued T-Sequence-like Function-like non empty finite initial countable set
CutLastLoc P is Relation-like NAT -defined the InstructionsF of S -valued T-Sequence-like Function-like finite initial countable set
LastLoc P is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
K485(NAT,P) is epsilon-transitive epsilon-connected ordinal natural non empty V28() V29() finite cardinal countable ext-real positive non negative V103() V104() V105() V106() V107() V108() V110() V111() V112() V113() V114() Element of K29(NAT)
K320(K485(NAT,P)) is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V120() set
P . (LastLoc P) is set
(LastLoc P) .--> (P . (LastLoc P)) is Relation-like NAT -defined {(LastLoc P)} -defined Function-like one-to-one constant non empty V19() finite 1 -element countable set
{(LastLoc P)} is non empty V19() finite V36() 1 -element countable V103() V104() V105() V106() V107() V108() V110() V111() V112() V113() V114() set
{(LastLoc P)} --> (P . (LastLoc P)) is Relation-like {(LastLoc P)} -defined {(P . (LastLoc P))} -valued Function-like constant non empty total V25({(LastLoc P)},{(P . (LastLoc P))}) finite countable Element of K29(K30({(LastLoc P)},{(P . (LastLoc P))}))
{(P . (LastLoc P))} is non empty V19() finite 1 -element countable set
K30({(LastLoc P)},{(P . (LastLoc P))}) is Relation-like finite countable set
K29(K30({(LastLoc P)},{(P . (LastLoc P))})) is finite V36() countable set
P \ ((LastLoc P) .--> (P . (LastLoc P))) is Relation-like NAT -defined the InstructionsF of S -valued Function-like finite countable Element of K29(P)
K29(P) is finite V36() countable set
card P is epsilon-transitive epsilon-connected ordinal natural non empty V28() V29() V30() finite cardinal countable ext-real positive non negative V103() V104() V105() V106() V107() V108() V110() V111() V112() V113() V114() V120() Element of omega
proj1 P is epsilon-transitive epsilon-connected ordinal natural non empty V28() V29() finite cardinal countable ext-real positive non negative V103() V104() V105() V106() V107() V108() V110() V111() V112() V113() V114() set
(card P) -' 1 is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
Reloc (s,((card P) -' 1)) is Relation-like NAT -defined the InstructionsF of S -valued Function-like finite countable set
IncAddr (s,((card P) -' 1)) is Relation-like NAT -defined the InstructionsF of S -valued T-Sequence-like Function-like non empty finite initial countable set
Shift ((IncAddr (s,((card P) -' 1))),((card P) -' 1)) is Relation-like NAT -defined the InstructionsF of S -valued Function-like non empty finite countable set
(CutLastLoc P) +* (Reloc (s,((card P) -' 1))) is Relation-like NAT -defined the InstructionsF of S -valued Function-like finite countable set
P2 is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
K485(NAT,(P ';' s)) is epsilon-transitive epsilon-connected ordinal natural non empty V28() V29() finite cardinal countable ext-real positive non negative V103() V104() V105() V106() V107() V108() V110() V111() V112() V113() V114() Element of K29(NAT)
(P ';' s) /. P2 is (N,S) (N,S) Element of the InstructionsF of S
NIC (((P ';' s) /. P2),P2) is non empty countable V103() V104() V105() V106() V107() V108() V110() V112() Element of K29(NAT)
the carrier of S is non empty set
the_Values_of S is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
the Object-Kind of S is Relation-like the carrier of S -defined N -valued Function-like non empty total V25( the carrier of S,N) Element of K29(K30( the carrier of S,N))
K30( the carrier of S,N) is Relation-like set
K29(K30( the carrier of S,N)) is set
the ValuesF of S is Relation-like N -defined Function-like non empty total set
the Object-Kind of S (#) the ValuesF of S is Relation-like the carrier of S -defined Function-like non empty total set
product (the_Values_of S) is functional non empty with_common_domain product-like set
{ (IC (Exec (((P ';' s) /. P2),b1))) where b1 is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible non empty total Element of product (the_Values_of S) : IC b1 = P2 } is set
dom (P ';' s) is epsilon-transitive epsilon-connected ordinal natural non empty V28() V29() finite cardinal countable ext-real positive non negative V103() V104() V105() V106() V107() V108() V110() V111() V112() V113() V114() Element of K29(NAT)
dom (CutLastLoc P) is epsilon-transitive epsilon-connected ordinal natural V28() V29() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() Element of K29(NAT)
proj1 (Reloc (s,((card P) -' 1))) is finite countable V103() V104() V105() V106() V107() V108() V112() V113() V114() set
(dom (CutLastLoc P)) \/ (proj1 (Reloc (s,((card P) -' 1)))) is finite countable V103() V104() V105() V106() V107() V108() V112() V113() V114() set
dom P is epsilon-transitive epsilon-connected ordinal natural non empty V28() V29() finite cardinal countable ext-real positive non negative V103() V104() V105() V106() V107() V108() V110() V111() V112() V113() V114() Element of K29(NAT)
dom (IncAddr (s,((card P) -' 1))) is epsilon-transitive epsilon-connected ordinal natural non empty V28() V29() finite cardinal countable ext-real positive non negative V103() V104() V105() V106() V107() V108() V110() V111() V112() V113() V114() Element of K29(NAT)
{ (b1 + ((card P) -' 1)) where b1 is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT : b1 in dom (IncAddr (s,((card P) -' 1))) } is set
m is set
s2 is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible non empty total Element of product (the_Values_of S)
Exec (((P ';' s) /. P2),s2) is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible non empty total set
product ( the Object-Kind of S (#) the ValuesF of S) is functional with_common_domain product-like set
K80((product ( the Object-Kind of S (#) the ValuesF of S)),(product ( the Object-Kind of S (#) the ValuesF of S))) is functional non empty set
the Execution of S is Relation-like the InstructionsF of S -defined K80((product ( the Object-Kind of S (#) the ValuesF of S)),(product ( the Object-Kind of S (#) the ValuesF of S))) -valued Function-like non empty total V25( the InstructionsF of S,K80((product ( the Object-Kind of S (#) the ValuesF of S)),(product ( the Object-Kind of S (#) the ValuesF of S)))) Function-yielding V148() Element of K29(K30( the InstructionsF of S,K80((product ( the Object-Kind of S (#) the ValuesF of S)),(product ( the Object-Kind of S (#) the ValuesF of S)))))
K30( the InstructionsF of S,K80((product ( the Object-Kind of S (#) the ValuesF of S)),(product ( the Object-Kind of S (#) the ValuesF of S)))) is Relation-like set
K29(K30( the InstructionsF of S,K80((product ( the Object-Kind of S (#) the ValuesF of S)),(product ( the Object-Kind of S (#) the ValuesF of S))))) is set
the Execution of S . ((P ';' s) /. P2) is Relation-like Function-like Element of K80((product ( the Object-Kind of S (#) the ValuesF of S)),(product ( the Object-Kind of S (#) the ValuesF of S)))
( the Execution of S . ((P ';' s) /. P2)) . s2 is Relation-like Function-like set
IC (Exec (((P ';' s) /. P2),s2)) is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
IC is V69(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
(Exec (((P ';' s) /. P2),s2)) . (IC ) is set
IC s2 is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
s2 . (IC ) is set
(P ';' s) . P2 is set
P /. P2 is (N,S) (N,S) Element of the InstructionsF of S
NIC ((P /. P2),P2) is non empty countable V103() V104() V105() V106() V107() V108() V110() V112() Element of K29(NAT)
{ (IC (Exec ((P /. P2),b1))) where b1 is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible non empty total Element of product (the_Values_of S) : IC b1 = P2 } is set
(dom P) \ {(LastLoc P)} is finite countable V103() V104() V105() V106() V107() V108() V112() V113() V114() Element of K29(NAT)
(CutLastLoc P) . P2 is set
P . P2 is set
Exec ((P /. P2),s2) is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible non empty total set
the Execution of S . (P /. P2) is Relation-like Function-like Element of K80((product ( the Object-Kind of S (#) the ValuesF of S)),(product ( the Object-Kind of S (#) the ValuesF of S)))
( the Execution of S . (P /. P2)) . s2 is Relation-like Function-like set
IC (Exec ((P /. P2),s2)) is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
(Exec ((P /. P2),s2)) . (IC ) is set
m is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
m + ((card P) -' 1) is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
dom s is epsilon-transitive epsilon-connected ordinal natural non empty V28() V29() finite cardinal countable ext-real positive non negative V103() V104() V105() V106() V107() V108() V110() V111() V112() V113() V114() Element of K29(NAT)
s /. m is (N,S) (N,S) Element of the InstructionsF of S
NIC ((s /. m),m) is non empty countable V103() V104() V105() V106() V107() V108() V110() V112() Element of K29(NAT)
{ (IC (Exec ((s /. m),b1))) where b1 is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible non empty total Element of product (the_Values_of S) : IC b1 = m } is set
Values (IC ) is non empty set
(the_Values_of S) . (IC ) is non empty set
(IC ) .--> m is Relation-like the carrier of S -defined {(IC )} -defined NAT -valued RAT -valued INT -valued Function-like one-to-one constant non empty V19() finite 1 -element Cardinal-yielding countable V121() V122() V123() V124() V125() V126() V127() V128() set
{(IC )} is non empty V19() finite 1 -element countable set
{(IC )} --> m is Relation-like {(IC )} -defined NAT -valued RAT -valued INT -valued {m} -valued Function-like constant non empty total V25({(IC )},{m}) finite Cardinal-yielding countable V121() V122() V123() V124() Element of K29(K30({(IC )},{m}))
{m} is non empty V19() finite V36() 1 -element countable V103() V104() V105() V106() V107() V108() V110() V111() V112() V113() V114() set
K30({(IC )},{m}) is Relation-like RAT -valued INT -valued finite countable V121() V122() V123() V124() set
K29(K30({(IC )},{m})) is finite V36() countable set
v is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible finite countable set
s2 +* v is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible non empty total set
(Reloc (s,((card P) -' 1))) . P2 is set
(IncAddr (s,((card P) -' 1))) . m is set
((IC ) .--> m) . (IC ) is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V120() set
proj1 ((IC ) .--> m) is non empty V19() finite 1 -element countable set
IC (s2 +* v) is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
(s2 +* v) . (IC ) is set
(IC (s2 +* v)) + ((card P) -' 1) is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
(IC ) .--> ((IC (s2 +* v)) + ((card P) -' 1)) is Relation-like the carrier of S -defined {(IC )} -defined NAT -valued RAT -valued INT -valued Function-like one-to-one constant non empty V19() finite 1 -element Cardinal-yielding countable V121() V122() V123() V124() V125() V126() V127() V128() set
{(IC )} --> ((IC (s2 +* v)) + ((card P) -' 1)) is Relation-like {(IC )} -defined NAT -valued RAT -valued INT -valued {((IC (s2 +* v)) + ((card P) -' 1))} -valued Function-like constant non empty total V25({(IC )},{((IC (s2 +* v)) + ((card P) -' 1))}) finite Cardinal-yielding countable V121() V122() V123() V124() Element of K29(K30({(IC )},{((IC (s2 +* v)) + ((card P) -' 1))}))
{((IC (s2 +* v)) + ((card P) -' 1))} is non empty V19() finite V36() 1 -element countable V103() V104() V105() V106() V107() V108() V110() V111() V112() V113() V114() set
K30({(IC )},{((IC (s2 +* v)) + ((card P) -' 1))}) is Relation-like RAT -valued INT -valued finite countable V121() V122() V123() V124() set
K29(K30({(IC )},{((IC (s2 +* v)) + ((card P) -' 1))})) is finite V36() countable set
(s2 +* v) +* ((IC ) .--> ((IC (s2 +* v)) + ((card P) -' 1))) is Relation-like the carrier of S -defined Function-like non empty total set
proj1 ((s2 +* v) +* ((IC ) .--> ((IC (s2 +* v)) + ((card P) -' 1)))) is non empty set
proj1 s2 is non empty set
s3 is set
s2 . s3 is set
((s2 +* v) +* ((IC ) .--> ((IC (s2 +* v)) + ((card P) -' 1)))) . s3 is set
proj1 ((IC ) .--> ((IC (s2 +* v)) + ((card P) -' 1))) is non empty V19() finite 1 -element countable set
((IC ) .--> ((IC (s2 +* v)) + ((card P) -' 1))) . s3 is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V120() set
(s2 +* v) . s3 is set
IncIC ((s2 +* v),((card P) -' 1)) is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible non empty total set
Start-At (((IC (s2 +* v)) + ((card P) -' 1)),S) is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible non empty finite countable (IC (s2 +* v)) + ((card P) -' 1) -started set
(s2 +* v) +* (Start-At (((IC (s2 +* v)) + ((card P) -' 1)),S)) is Relation-like the carrier of S -defined the carrier of S -defined Function-like the_Values_of S -compatible the_Values_of S -compatible non empty total (IC (s2 +* v)) + ((card P) -' 1) -started set
m is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
s /. m is (N,S) (N,S) Element of the InstructionsF of S
k is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
IncAddr ((s /. m),k) is (N,S) (N,S) Element of the InstructionsF of S
Exec ((IncAddr ((s /. m),k)),s2) is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible non empty total set
the Execution of S . (IncAddr ((s /. m),k)) is Relation-like Function-like Element of K80((product ( the Object-Kind of S (#) the ValuesF of S)),(product ( the Object-Kind of S (#) the ValuesF of S)))
( the Execution of S . (IncAddr ((s /. m),k))) . s2 is Relation-like Function-like set
IC (Exec ((IncAddr ((s /. m),k)),s2)) is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
(Exec ((IncAddr ((s /. m),k)),s2)) . (IC ) is set
Exec ((s /. m),(s2 +* v)) is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible non empty total set
the Execution of S . (s /. m) is Relation-like Function-like Element of K80((product ( the Object-Kind of S (#) the ValuesF of S)),(product ( the Object-Kind of S (#) the ValuesF of S)))
( the Execution of S . (s /. m)) . (s2 +* v) is Relation-like Function-like set
IC (Exec ((s /. m),(s2 +* v))) is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
(Exec ((s /. m),(s2 +* v))) . (IC ) is set
(IC (Exec ((s /. m),(s2 +* v)))) + k is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
s3 is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible non empty total Element of product (the_Values_of S)
Exec ((s /. m),s3) is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible non empty total set
( the Execution of S . (s /. m)) . s3 is Relation-like Function-like set
IC (Exec ((s /. m),s3)) is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
(Exec ((s /. m),s3)) . (IC ) is set
(IC (Exec ((s /. m),s3))) + k is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
NIC ((s /. m),m) is non empty countable V103() V104() V105() V106() V107() V108() V110() V112() Element of K29(NAT)
{ (IC (Exec ((s /. m),b1))) where b1 is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible non empty total Element of product (the_Values_of S) : IC b1 = m } is set
IncAddr (s,k) is Relation-like NAT -defined the InstructionsF of S -valued T-Sequence-like Function-like non empty finite initial countable set
dom (IncAddr (s,k)) is epsilon-transitive epsilon-connected ordinal natural non empty V28() V29() finite cardinal countable ext-real positive non negative V103() V104() V105() V106() V107() V108() V110() V111() V112() V113() V114() Element of K29(NAT)
Reloc (s,k) is Relation-like NAT -defined the InstructionsF of S -valued Function-like finite countable set
Shift ((IncAddr (s,k)),k) is Relation-like NAT -defined the InstructionsF of S -valued Function-like non empty finite countable set
proj1 (Reloc (s,k)) is finite countable V103() V104() V105() V106() V107() V108() V112() V113() V114() set
N is non empty non with_non-empty_elements set
Trivial-AMI N is non empty V67() finite 1 -element with_non-empty_values IC-Ins-separated strict halting (N) AMI-Struct over N
the InstructionsF of (Trivial-AMI N) is Relation-like non empty standard-ins homogeneous J/A-independent V55() set
S is (N, Trivial-AMI N) Element of the InstructionsF of (Trivial-AMI N)
JumpPart S is Relation-like NAT -defined NAT -valued RAT -valued Function-like finite V40() V41() countable V121() V122() V123() V124() set
K50(S) is set
AddressPart K50(S) is set
N is non empty non with_non-empty_elements set
Trivial-AMI N is non empty V67() finite 1 -element with_non-empty_values IC-Ins-separated strict halting (N) AMI-Struct over N
the InstructionsF of (Trivial-AMI N) is Relation-like non empty standard-ins homogeneous J/A-independent V55() set
InsCodes the InstructionsF of (Trivial-AMI N) is non empty set
K60( the InstructionsF of (Trivial-AMI N)) is set
proj1 the InstructionsF of (Trivial-AMI N) is non empty set
proj1 (proj1 the InstructionsF of (Trivial-AMI N)) is set
S is Element of InsCodes the InstructionsF of (Trivial-AMI N)
JumpParts S is functional non empty with_common_domain product-like set
{ (JumpPart b1) where b1 is Element of the InstructionsF of (Trivial-AMI N) : InsCode b1 = S } is set
N is non empty non with_non-empty_elements set
S is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
P is non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
the carrier of P is non empty set
the_Values_of P is Relation-like non-empty non empty-yielding the carrier of P -defined Function-like non empty total set
the Object-Kind of P is Relation-like the carrier of P -defined N -valued Function-like non empty total V25( the carrier of P,N) Element of K29(K30( the carrier of P,N))
K30( the carrier of P,N) is Relation-like set
K29(K30( the carrier of P,N)) is set
the ValuesF of P is Relation-like N -defined Function-like non empty total set
the Object-Kind of P (#) the ValuesF of P is Relation-like the carrier of P -defined Function-like non empty total set
the InstructionsF of P is Relation-like non empty standard-ins homogeneous J/A-independent V55() set
s is Relation-like the carrier of P -defined Function-like the_Values_of P -compatible non empty total set
I is Relation-like NAT -defined the InstructionsF of P -valued T-Sequence-like Function-like non empty finite initial countable set
dom I is epsilon-transitive epsilon-connected ordinal natural non empty V28() V29() finite cardinal countable ext-real positive non negative V103() V104() V105() V106() V107() V108() V110() V111() V112() V113() V114() Element of K29(NAT)
P1 is Relation-like NAT -defined the InstructionsF of P -valued Function-like non empty total set
P2 is Relation-like NAT -defined the InstructionsF of P -valued Function-like non empty total set
m is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
Comput (P1,s,m) is Relation-like the carrier of P -defined Function-like the_Values_of P -compatible non empty total set
Comput (P2,s,m) is Relation-like the carrier of P -defined Function-like the_Values_of P -compatible non empty total set
m + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V28() V29() V30() finite cardinal countable ext-real positive non negative V103() V104() V105() V106() V107() V108() V110() V111() V112() V113() V114() V120() Element of NAT
Comput (P1,s,(m + 1)) is Relation-like the carrier of P -defined Function-like the_Values_of P -compatible non empty total set
Comput (P2,s,(m + 1)) is Relation-like the carrier of P -defined Function-like the_Values_of P -compatible non empty total set
Following (P2,(Comput (P2,s,m))) is Relation-like the carrier of P -defined Function-like the_Values_of P -compatible non empty total set
CurInstr (P2,(Comput (P2,s,m))) is Element of the InstructionsF of P
IC (Comput (P2,s,m)) is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
IC is V69(P) Element of the carrier of P
the ZeroF of P is Element of the carrier of P
(Comput (P2,s,m)) . (IC ) is set
P2 /. (IC (Comput (P2,s,m))) is Element of the InstructionsF of P
Exec ((CurInstr (P2,(Comput (P2,s,m)))),(Comput (P2,s,m))) is Relation-like the carrier of P -defined Function-like the_Values_of P -compatible non empty total set
product ( the Object-Kind of P (#) the ValuesF of P) is functional with_common_domain product-like set
K80((product ( the Object-Kind of P (#) the ValuesF of P)),(product ( the Object-Kind of P (#) the ValuesF of P))) is functional non empty set
the Execution of P is Relation-like the InstructionsF of P -defined K80((product ( the Object-Kind of P (#) the ValuesF of P)),(product ( the Object-Kind of P (#) the ValuesF of P))) -valued Function-like non empty total V25( the InstructionsF of P,K80((product ( the Object-Kind of P (#) the ValuesF of P)),(product ( the Object-Kind of P (#) the ValuesF of P)))) Function-yielding V148() Element of K29(K30( the InstructionsF of P,K80((product ( the Object-Kind of P (#) the ValuesF of P)),(product ( the Object-Kind of P (#) the ValuesF of P)))))
K30( the InstructionsF of P,K80((product ( the Object-Kind of P (#) the ValuesF of P)),(product ( the Object-Kind of P (#) the ValuesF of P)))) is Relation-like set
K29(K30( the InstructionsF of P,K80((product ( the Object-Kind of P (#) the ValuesF of P)),(product ( the Object-Kind of P (#) the ValuesF of P))))) is set
the Execution of P . (CurInstr (P2,(Comput (P2,s,m)))) is Relation-like Function-like Element of K80((product ( the Object-Kind of P (#) the ValuesF of P)),(product ( the Object-Kind of P (#) the ValuesF of P)))
( the Execution of P . (CurInstr (P2,(Comput (P2,s,m))))) . (Comput (P2,s,m)) is Relation-like Function-like set
Following (P1,(Comput (P1,s,m))) is Relation-like the carrier of P -defined Function-like the_Values_of P -compatible non empty total set
CurInstr (P1,(Comput (P1,s,m))) is Element of the InstructionsF of P
IC (Comput (P1,s,m)) is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
(Comput (P1,s,m)) . (IC ) is set
P1 /. (IC (Comput (P1,s,m))) is Element of the InstructionsF of P
Exec ((CurInstr (P1,(Comput (P1,s,m)))),(Comput (P1,s,m))) is Relation-like the carrier of P -defined Function-like the_Values_of P -compatible non empty total set
the Execution of P . (CurInstr (P1,(Comput (P1,s,m)))) is Relation-like Function-like Element of K80((product ( the Object-Kind of P (#) the ValuesF of P)),(product ( the Object-Kind of P (#) the ValuesF of P)))
( the Execution of P . (CurInstr (P1,(Comput (P1,s,m))))) . (Comput (P1,s,m)) is Relation-like Function-like set
proj1 P2 is non empty V103() V104() V105() V106() V107() V108() V110() V112() set
proj1 P1 is non empty V103() V104() V105() V106() V107() V108() V110() V112() set
P1 . (IC (Comput (P1,s,m))) is Element of the InstructionsF of P
I . (IC (Comput (P1,s,m))) is set
P2 . (IC (Comput (P2,s,m))) is Element of the InstructionsF of P
Comput (P1,s,0) is Relation-like the carrier of P -defined Function-like the_Values_of P -compatible non empty total set
Comput (P2,s,0) is Relation-like the carrier of P -defined Function-like the_Values_of P -compatible non empty total set
N is non empty non with_non-empty_elements set
S is non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
the InstructionsF of S is Relation-like non empty standard-ins homogeneous J/A-independent V55() set
the carrier of S is non empty set
the_Values_of S is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
the Object-Kind of S is Relation-like the carrier of S -defined N -valued Function-like non empty total V25( the carrier of S,N) Element of K29(K30( the carrier of S,N))
K30( the carrier of S,N) is Relation-like set
K29(K30( the carrier of S,N)) is set
the ValuesF of S is Relation-like N -defined Function-like non empty total set
the Object-Kind of S (#) the ValuesF of S is Relation-like the carrier of S -defined Function-like non empty total set
P is Relation-like NAT -defined the InstructionsF of S -valued Function-like non empty total set
s is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible non empty total set
Following (P,s) is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible non empty total set
CurInstr (P,s) is Element of the InstructionsF of S
IC s is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
IC is V69(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
Exec ((CurInstr (P,s)),s) is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible non empty total set
product ( the Object-Kind of S (#) the ValuesF of S) is functional with_common_domain product-like set
K80((product ( the Object-Kind of S (#) the ValuesF of S)),(product ( the Object-Kind of S (#) the ValuesF of S))) is functional non empty set
the Execution of S is Relation-like the InstructionsF of S -defined K80((product ( the Object-Kind of S (#) the ValuesF of S)),(product ( the Object-Kind of S (#) the ValuesF of S))) -valued Function-like non empty total V25( the InstructionsF of S,K80((product ( the Object-Kind of S (#) the ValuesF of S)),(product ( the Object-Kind of S (#) the ValuesF of S)))) Function-yielding V148() Element of K29(K30( the InstructionsF of S,K80((product ( the Object-Kind of S (#) the ValuesF of S)),(product ( the Object-Kind of S (#) the ValuesF of S)))))
K30( the InstructionsF of S,K80((product ( the Object-Kind of S (#) the ValuesF of S)),(product ( the Object-Kind of S (#) the ValuesF of S)))) is Relation-like set
K29(K30( the InstructionsF of S,K80((product ( the Object-Kind of S (#) the ValuesF of S)),(product ( the Object-Kind of S (#) the ValuesF of S))))) is set
the Execution of S . (CurInstr (P,s)) is Relation-like Function-like Element of K80((product ( the Object-Kind of S (#) the ValuesF of S)),(product ( the Object-Kind of S (#) the ValuesF of S)))
( the Execution of S . (CurInstr (P,s))) . s is Relation-like Function-like set
I is epsilon-transitive epsilon-connected ordinal natural V28() V29() V30() finite cardinal countable ext-real non negative V103() V104() V105() V106() V107() V108() V112() V113() V114() V120() Element of NAT
Comput (P,s,I) is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible non empty total set
I + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V28() V29() V30() finite cardinal countable ext-real positive non negative V103() V104() V105() V106() V107() V108() V110() V111() V112() V113() V114() V120() Element of NAT
Comput (P,s,(I + 1)) is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible non empty total set
Comput (P,s,0) is Relation-like the carrier of S -defined Function-like the_Values_of S -compatible non empty total set