begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th17:
:: deftheorem AMISTD_2:def 1 :
canceled;
:: deftheorem AMISTD_2:def 2 :
canceled;
:: deftheorem AMISTD_2:def 3 :
canceled;
:: deftheorem AMISTD_2:def 4 :
canceled;
:: deftheorem AMISTD_2:def 5 :
canceled;
:: deftheorem Def6 defines with_explicit_jumps AMISTD_2:def 6 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins AMI-Struct of N
for I being Instruction of S holds
( I is with_explicit_jumps iff JUMP I = rng (JumpPart I) );
:: deftheorem AMISTD_2:def 7 :
canceled;
:: deftheorem Def8 defines with_explicit_jumps AMISTD_2:def 8 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins AMI-Struct of N holds
( S is with_explicit_jumps iff for I being Instruction of S holds I is with_explicit_jumps );
:: deftheorem AMISTD_2:def 9 :
canceled;
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
canceled;
theorem Th21:
theorem
begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
:: deftheorem AMISTD_2:def 10 :
canceled;
:: deftheorem AMISTD_2:def 11 :
canceled;
:: deftheorem AMISTD_2:def 12 :
canceled;
:: deftheorem AMISTD_2:def 13 :
canceled;
:: deftheorem AMISTD_2:def 14 :
canceled;
:: deftheorem AMISTD_2:def 15 :
canceled;
:: deftheorem AMISTD_2:def 16 :
canceled;
:: deftheorem AMISTD_2:def 17 :
canceled;
:: deftheorem Def18 defines IC-relocable AMISTD_2:def 18 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent 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 19 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent halting AMI-Struct of N holds
( S is IC-relocable iff for I being Instruction of S holds I is IC-relocable );
:: deftheorem Def20 defines Exec-preserving AMISTD_2:def 20 :
for N being with_non-empty_elements set
for S being stored-program AMI-Struct of N
for I being Instruction of S holds
( I is Exec-preserving iff for s1, s2 being State of S st s1,s2 equal_outside NAT holds
Exec (I,s1), Exec (I,s2) equal_outside NAT );
:: deftheorem Def21 defines Exec-preserving AMISTD_2:def 21 :
for N being with_non-empty_elements set
for S being stored-program AMI-Struct of N holds
( S is Exec-preserving iff for I being Instruction of S holds I is Exec-preserving );
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th46:
theorem Th47:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem
for
N being non
empty with_non-empty_elements set for
n being
Element of
NAT for
S being non
empty stored-program IC-Ins-separated definite realistic Exec-preserving AMI-Struct of
N for
s1,
s2 being
State of
S for
I being
Program of
N for
P1,
P2 being the
Instructions of
b3 -valued ManySortedSet of
NAT st
I c= P1 &
I c= P2 &
s1,
s2 equal_outside NAT & ( for
m being
Element of
NAT st
m < n holds
IC (Comput (P2,s2,m)) in dom I ) holds
for
m being
Element of
NAT st
m <= n holds
Comput (
P1,
s1,
m),
Comput (
P2,
s2,
m)
equal_outside NAT