begin
theorem Th17:
:: deftheorem Def6 defines with_explicit_jumps AMISTD_2:def 1 :
for N being non empty with_non-empty_elements set
for S being standard-ins non empty IC-Ins-separated AMI-Struct of N
for I being Instruction of S holds
( I is with_explicit_jumps iff JUMP I = rng (JumpPart I) );
:: deftheorem Def8 defines with_explicit_jumps AMISTD_2:def 2 :
for N being non empty with_non-empty_elements set
for S being standard-ins non empty IC-Ins-separated AMI-Struct of N holds
( S is with_explicit_jumps iff for I being Instruction of S holds I is with_explicit_jumps );
theorem Th18:
theorem Th19:
Lm1:
for N being non empty with_non-empty_elements set
for I being Instruction of (Trivial-AMI N) holds JumpPart I = 0
Lm2:
for N being non empty with_non-empty_elements set
for T being InsType of (Trivial-AMI N) holds JumpParts T = {0}
theorem Th21:
theorem
begin
theorem
:: deftheorem Def18 defines IC-relocable AMISTD_2:def 3 :
for N being non empty with_non-empty_elements set
for S being standard-ins homogeneous regular J/A-independent non empty IC-Ins-separated halting AMI-Struct of N
for I being Instruction of S holds
( I is IC-relocable iff for j, k being natural number
for s being State of S holds (IC (Exec ((IncAddr (I,j)),s))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s,k)))) );
:: deftheorem Def19 defines IC-relocable AMISTD_2:def 4 :
for N being non empty with_non-empty_elements set
for S being standard-ins homogeneous regular J/A-independent non empty IC-Ins-separated halting AMI-Struct of N holds
( S is IC-relocable iff for I being Instruction of S holds I is IC-relocable );
theorem Th47:
theorem
theorem
theorem
theorem