:: On the Composition of Macro Instructions of Standard Computers
:: by Artur Korni{\l}owicz
::
:: Received April 14, 2000
:: Copyright (c) 2000 Association of Mizar Users

begin

Lm1: for k being natural number holds - 1 < k

proof end;

Lm2: for k being natural number
for a, b, c being Element of NAT st 1 <= a & 2 <= b & not k < a - 1 & not ( a <= k & k <= (a + b) - 3 ) & not k = (a + b) - 2 & not (a + b) - 2 < k holds
k = a - 1

proof end;

begin

definition

canceled;
canceled;
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of N;
let i1, i2 be Element of NAT ;
let I1, I2 be Element of the Instructions of S;
:: original: -->
redefine func i1,i2 --> I1,I2 -> FinPartState of S;
coherence
i1,i2 --> I1,I2 is FinPartState of S

proof end;

end;

:: deftheorem AMISTD_2:def 1 :
canceled;

:: deftheorem AMISTD_2:def 2 :
canceled;

registration

let N be with_non-empty_elements set ;
let S be stored-program halting AMI-Struct of N;
cluster halting Element of the Instructions of S;
existence
ex b₁ being Instruction of S st b₁ is halting

proof end;

end;

definition

let N be set ;
let S be standard-ins AMI-Struct of N;
let T be InsType of S;
func JumpParts T -> set equals :: AMISTD_2:def 3
{ (JumpPart I) where I is Instruction of S : InsCode I = T } ;
coherence
{ (JumpPart I) where I is Instruction of S : InsCode I = T } is set ;

end;

:: deftheorem defines JumpParts AMISTD_2:def 3 :
for N being set
for S being standard-ins AMI-Struct of N
for T being InsType of S holds JumpParts T = { (JumpPart I) where I is Instruction of S : InsCode I = T } ;

registration

let N be set ;
let S be standard-ins AMI-Struct of N;
let I be Element of the Instructions of S;
cluster AddressPart I -> Relation-like Function-like ;
coherence
( AddressPart I is Function-like & AddressPart I is Relation-like )

proof end;

cluster JumpPart I -> Relation-like Function-like ;
coherence
( JumpPart I is Function-like & JumpPart I is Relation-like )

proof end;

end;

registration

let N be set ;
let S be standard-ins AMI-Struct of N;
let I be Element of the Instructions of S;
cluster AddressPart I -> FinSequence-like ;
coherence
AddressPart I is FinSequence-like

proof end;

cluster JumpPart I -> FinSequence-like ;
coherence
JumpPart I is FinSequence-like

proof end;

end;

definition

let N be set ;
let S be standard-ins AMI-Struct of N;
attr S is homogeneous means :Def4: :: AMISTD_2:def 4
for I, J being Instruction of S st InsCode I = InsCode J holds
dom (JumpPart I) = dom (JumpPart J);

end;

:: deftheorem Def4 defines homogeneous AMISTD_2:def 4 :
for N being set
for S being standard-ins AMI-Struct of N holds
( S is homogeneous iff for I, J being Instruction of S st InsCode I = InsCode J holds
dom (JumpPart I) = dom (JumpPart J) );

theorem :: AMISTD_2:1

canceled;

theorem :: AMISTD_2:2

canceled;

theorem :: AMISTD_2:3

canceled;

theorem :: AMISTD_2:4

canceled;

theorem :: AMISTD_2:5

canceled;

theorem :: AMISTD_2:6

canceled;

theorem :: AMISTD_2:7

canceled;

theorem :: AMISTD_2:8

canceled;

theorem :: AMISTD_2:9

canceled;

theorem :: AMISTD_2:10

canceled;

theorem :: AMISTD_2:11

canceled;

theorem :: AMISTD_2:12

canceled;

theorem :: AMISTD_2:13

canceled;

theorem :: AMISTD_2:14

canceled;

theorem :: AMISTD_2:15

canceled;

theorem :: AMISTD_2:16

canceled;

theorem Th17: :: AMISTD_2:17

for N being non empty with_non-empty_elements set
for I being Instruction of (STC N) holds JumpPart I = 0

proof end;

definition

let N be set ;
let S be standard-ins AMI-Struct of N;
let T be InsType of S;
func AddressParts T -> set equals :: AMISTD_2:def 5
{ (AddressPart I) where I is Instruction of S : InsCode I = T } ;
coherence
{ (AddressPart I) where I is Instruction of S : InsCode I = T } is set ;

end;

:: deftheorem defines AddressParts AMISTD_2:def 5 :
for N being set
for S being standard-ins AMI-Struct of N
for T being InsType of S holds AddressParts T = { (AddressPart I) where I is Instruction of S : InsCode I = T } ;

registration

let N be set ;
let S be standard-ins AMI-Struct of N;
let T be InsType of S;
cluster AddressParts T -> functional ;
coherence
AddressParts T is functional

proof end;

cluster JumpParts T -> functional non empty ;
coherence
( not JumpParts T is empty & JumpParts T is functional )

proof end;

end;

definition

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard-ins AMI-Struct of N;
let I be Instruction of S;
attr I is with_explicit_jumps means :Def6: :: AMISTD_2:def 6
JUMP I c= rng (JumpPart I);
attr I is without_implicit_jumps means :Def7: :: AMISTD_2:def 7
rng (JumpPart I) c= JUMP I;

end;

:: 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 c= rng (JumpPart I) );

:: deftheorem Def7 defines without_implicit_jumps AMISTD_2:def 7 :
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 without_implicit_jumps iff rng (JumpPart I) c= JUMP I );

definition

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard-ins AMI-Struct of N;
attr S is with_explicit_jumps means :Def8: :: AMISTD_2:def 8
for I being Instruction of S holds I is with_explicit_jumps ;
attr S is without_implicit_jumps means :Def9: :: AMISTD_2:def 9
for I being Instruction of S holds I is without_implicit_jumps ;

end;

:: 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 Def9 defines without_implicit_jumps AMISTD_2:def 9 :
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 without_implicit_jumps iff for I being Instruction of S holds I is without_implicit_jumps );

registration

let N be non empty with_non-empty_elements set ;
cluster non empty stored-program IC-Ins-separated definite standard -> non empty stored-program IC-Ins-separated definite AMI-Struct of N;
coherence
for b₁ being non empty stored-program IC-Ins-separated definite AMI-Struct of N st b₁ is standard holds
verum ;

end;

registration

let N be non empty with_non-empty_elements set ;
cluster non empty stored-program IC-Ins-separated definite standard-ins standard AMI-Struct of N;
existence
ex b₁ being non empty stored-program IC-Ins-separated definite AMI-Struct of N st
( b₁ is standard & b₁ is standard-ins )

proof end;

end;

theorem Th18: :: AMISTD_2:18

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of N
for I being Instruction of S st ( for f being Element of NAT holds NIC I,f = {(succ f)} ) holds
JUMP I is empty

proof end;

registration

let N be non empty with_non-empty_elements set ;
let I be Instruction of (STC N);
cluster JUMP I -> empty ;
coherence
JUMP I is empty

proof end;

end;

definition

let N be set ;
let S be standard-ins AMI-Struct of N;
canceled;
attr S is regular means :Def11: :: AMISTD_2:def 11
for I being Instruction of S
for k being set st k in dom (JumpPart I) holds
(product" (JumpParts (InsCode I))) . k = NAT ;
attr S is J/A-independent means :Dfs: :: AMISTD_2:def 12
for T being InsType of S
for f1, f2 being Function
for p being set st f1 in JumpParts T & f2 in product (product" (JumpParts T)) & [T,f1,p] in the Instructions of S holds
[T,f2,p] in the Instructions of S;

end;

:: deftheorem AMISTD_2:def 10 :
canceled;

:: deftheorem Def11 defines regular AMISTD_2:def 11 :
for N being set
for S being standard-ins AMI-Struct of N holds
( S is regular iff for I being Instruction of S
for k being set st k in dom (JumpPart I) holds
(product" (JumpParts (InsCode I))) . k = NAT );

:: deftheorem Dfs defines J/A-independent AMISTD_2:def 12 :
for N being set
for S being standard-ins AMI-Struct of N holds
( S is J/A-independent iff for T being InsType of S
for f1, f2 being Function
for p being set st f1 in JumpParts T & f2 in product (product" (JumpParts T)) & [T,f1,p] in the Instructions of S holds
[T,f2,p] in the Instructions of S );

theorem Th19: :: AMISTD_2:19

for N being non empty with_non-empty_elements set
for T being InsType of (STC N) holds JumpParts T = {0 }

proof end;

Lm3: for N being non empty with_non-empty_elements set
for I being Instruction of (Trivial-AMI N) holds JumpPart I = 0

proof end;

Lm4: for N being non empty with_non-empty_elements set
for T being InsType of (Trivial-AMI N) holds JumpParts T = {0 }

proof end;

registration

let N be non empty with_non-empty_elements set ;
cluster STC N -> homogeneous with_explicit_jumps without_implicit_jumps regular J/A-independent ;
coherence
( STC N is with_explicit_jumps & STC N is without_implicit_jumps & STC N is homogeneous & STC N is regular & STC N is J/A-independent )

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
cluster non empty stored-program IC-Ins-separated definite realistic standard-ins halting steady-programmed standard homogeneous with_explicit_jumps without_implicit_jumps regular J/A-independent AMI-Struct of N;
existence
ex b₁ being non empty stored-program IC-Ins-separated definite standard-ins AMI-Struct of N st
( b₁ is standard & b₁ is regular & b₁ is J/A-independent & b₁ is homogeneous & b₁ is halting & b₁ is realistic & b₁ is steady-programmed & b₁ is with_explicit_jumps & b₁ is without_implicit_jumps )

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
let S be standard-ins homogeneous regular AMI-Struct of N;
let T be InsType of S;
cluster JumpParts T -> with_common_domain ;
coherence
JumpParts T is with_common_domain

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
let S be standard-ins homogeneous regular AMI-Struct of N;
let I be Instruction of S;
cluster JumpPart I -> NAT -valued Function;
coherence
for b₁ being Function st b₁ = JumpPart I holds
b₁ is NAT -valued

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
let S be standard-ins homogeneous regular J/A-independent AMI-Struct of N;
let T be InsType of S;
cluster JumpParts T -> product-like ;
coherence
JumpParts T is product-like

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
cluster Trivial-AMI N -> regular J/A-independent ;
coherence
( Trivial-AMI N is regular & Trivial-AMI N is J/A-independent )

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
cluster standard-ins regular J/A-independent AMI-Struct of N;
existence
ex b₁ being standard-ins AMI-Struct of N st
( b₁ is regular & b₁ is J/A-independent )

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
let S be standard-ins homogeneous AMI-Struct of N;
let T be InsType of S;
cluster JumpParts T -> with_common_domain ;
coherence
JumpParts T is with_common_domain

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
let I be Instruction of (Trivial-AMI N);
cluster JUMP I -> empty ;
coherence
JUMP I is empty

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
cluster Trivial-AMI N -> with_explicit_jumps without_implicit_jumps ;
coherence
( Trivial-AMI N is with_explicit_jumps & Trivial-AMI N is without_implicit_jumps )

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
cluster non empty stored-program standard-ins regular J/A-independent AMI-Struct of N;
existence
ex b₁ being non empty stored-program standard-ins AMI-Struct of N st
( b₁ is regular & b₁ is J/A-independent )

proof end;

end;

theorem :: AMISTD_2:20

for N being non empty with_non-empty_elements set
for S being non empty stored-program standard-ins homogeneous regular AMI-Struct of N
for I being Instruction of S
for x being set st x in dom (JumpPart I) holds
(JumpPart I) . x is Element of NAT

proof end;

registration

let N be non empty with_non-empty_elements set ;
cluster non empty stored-program IC-Ins-separated definite realistic standard-ins halting with_explicit_jumps without_implicit_jumps AMI-Struct of N;
existence
ex b₁ being non empty stored-program IC-Ins-separated definite standard-ins AMI-Struct of N st
( b₁ is without_implicit_jumps & b₁ is with_explicit_jumps & b₁ is halting & b₁ is realistic )

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard-ins with_explicit_jumps AMI-Struct of N;
cluster -> with_explicit_jumps Element of the Instructions of S;
coherence
for b₁ being Instruction of S holds b₁ is with_explicit_jumps by Def8;

end;

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard-ins without_implicit_jumps AMI-Struct of N;
cluster -> without_implicit_jumps Element of the Instructions of S;
coherence
for b₁ being Instruction of S holds b₁ is without_implicit_jumps by Def9;

end;

theorem Th21: :: AMISTD_2:21

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic steady-programmed AMI-Struct of N
for I being Instruction of S st I is halting holds
JUMP I is empty

proof end;

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic halting steady-programmed AMI-Struct of N;
let I be halting Instruction of S;
cluster JUMP I -> empty ;
coherence
JUMP I is empty by Th21;

end;

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of N;
cluster Relation-like NAT -defined the carrier of S -defined Function-like the Object-Kind of S -compatible non trivial finite countable set ;
existence
ex b₁ being FinPartState of S st
( not b₁ is trivial & b₁ is NAT -defined )

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite halting standard AMI-Struct of N;
cluster Relation-like NAT -defined the carrier of S -defined Function-like the Object-Kind of S -compatible non empty trivial finite -> NAT -defined non empty unique-halt set ;
coherence
for b₁ being NAT -defined non empty FinPartState of st b₁ is trivial holds
b₁ is unique-halt

proof end;

end;

definition

let N be set ;
let S be standard-ins AMI-Struct of N;
let I be Instruction of S;
attr I is ins-loc-free means :: AMISTD_2:def 13
JumpPart I is empty ;

end;

:: deftheorem defines ins-loc-free AMISTD_2:def 13 :
for N being set
for S being standard-ins AMI-Struct of N
for I being Instruction of S holds
( I is ins-loc-free iff JumpPart I is empty );

theorem :: AMISTD_2:22

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins halting with_explicit_jumps AMI-Struct of N
for I being Instruction of S st I is ins-loc-free holds
JUMP I is empty

proof end;

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins steady-programmed without_implicit_jumps AMI-Struct of N;
cluster halting -> ins-loc-free Element of the Instructions of S;
coherence
for b₁ being Instruction of S st b₁ is halting holds
b₁ is ins-loc-free

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard-ins standard without_implicit_jumps AMI-Struct of N;
cluster sequential -> ins-loc-free Element of the Instructions of S;
coherence
for b₁ being Instruction of S st b₁ is sequential holds
b₁ is ins-loc-free

proof end;

end;

Lm5: now

let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite halting standard AMI-Struct of N holds
( dom (Stop S) = {0 } & 0 in dom (Stop S) )
let S be non empty stored-program IC-Ins-separated definite halting standard AMI-Struct of N; :: thesis: ( dom (Stop S) = {0 } & 0 in dom (Stop S) )
thus dom (Stop S) = {0 } by FUNCOP_1:19; :: thesis: 0 in dom (Stop S)
hence 0 in dom (Stop S) by TARSKI:def 1; :: thesis: verum

end;

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite halting standard AMI-Struct of N;
cluster Stop S -> non empty trivial ;
coherence
( Stop S is initial & not Stop S is empty & Stop S is NAT -defined & Stop S is the Instructions of S -valued & Stop S is trivial ) ;

end;

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic halting steady-programmed standard AMI-Struct of N;
cluster Stop S -> closed ;
coherence
Stop S is closed by AMISTD_1:46;

end;

theorem :: AMISTD_2:23

canceled;

theorem :: AMISTD_2:24

canceled;

theorem Th25: :: AMISTD_2:25

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting standard AMI-Struct of N holds card (Stop S) = 1

proof end;

theorem Th26: :: AMISTD_2:26

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting standard AMI-Struct of N
for F being pre-Macro of S st card F = 1 holds
F = Stop S

proof end;

Lm6: for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting standard AMI-Struct of N holds (card (Stop S)) -' 1 = 0

proof end;

theorem Th27: :: AMISTD_2:27

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting standard AMI-Struct of N holds LastLoc (Stop S) = 0

proof end;

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite halting standard AMI-Struct of N;
cluster Stop S -> halt-ending unique-halt ;
coherence
( Stop S is halt-ending & Stop S is unique-halt )

proof end;

end;

begin

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard-ins standard homogeneous regular J/A-independent AMI-Struct of N;
let I be Element of the Instructions of S;
cluster JumpPart I -> natural-valued Function;
coherence
for b₁ being Function st b₁ = JumpPart I holds
b₁ is natural-valued ;

end;

definition

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard-ins standard homogeneous regular J/A-independent AMI-Struct of N;
let I be Element of the Instructions of S;
let k be natural number ;
func IncAddr I,k -> Instruction of S means :Def14: :: AMISTD_2:def 14
( InsCode it = InsCode I & AddressPart it = AddressPart I & JumpPart it = k + (JumpPart I) );
existence
ex b₁ being Instruction of S st
( InsCode b₁ = InsCode I & AddressPart b₁ = AddressPart I & JumpPart b₁ = k + (JumpPart I) )

proof end;

uniqueness
for b₁, b₂ being Instruction of S st InsCode b₁ = InsCode I & AddressPart b₁ = AddressPart I & JumpPart b₁ = k + (JumpPart I) & InsCode b₂ = InsCode I & AddressPart b₂ = AddressPart I & JumpPart b₂ = k + (JumpPart I) holds
b₁ = b₂ by COMPOS_1:7;

end;

:: deftheorem Def14 defines IncAddr AMISTD_2:def 14 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard homogeneous regular J/A-independent AMI-Struct of N
for I being Element of the Instructions of S
for k being natural number
for b₅ being Instruction of S holds
( b₅ = IncAddr I,k iff ( InsCode b₅ = InsCode I & AddressPart b₅ = AddressPart I & JumpPart b₅ = k + (JumpPart I) ) );

theorem Th28: :: AMISTD_2:28

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard homogeneous regular J/A-independent AMI-Struct of N
for I being Element of the Instructions of S holds IncAddr I,0 = I

proof end;

theorem Th29: :: AMISTD_2:29

for k being natural number
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard homogeneous regular J/A-independent AMI-Struct of N
for I being Instruction of S st I is ins-loc-free holds
IncAddr I,k = I

proof end;

theorem :: AMISTD_2:30

for k being natural number
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins halting steady-programmed standard homogeneous without_implicit_jumps regular J/A-independent AMI-Struct of N holds IncAddr (halt S),k = halt S by Th29;

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins halting steady-programmed standard homogeneous without_implicit_jumps regular J/A-independent AMI-Struct of N;
let I be halting Instruction of S;
let k be natural number ;
cluster IncAddr I,k -> halting ;
coherence
IncAddr I,k is halting by Th29;

end;

theorem :: AMISTD_2:31

for k being natural number
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard homogeneous regular J/A-independent AMI-Struct of N
for I being Instruction of S holds JumpParts (InsCode I) = JumpParts (InsCode (IncAddr I,k))

proof end;

theorem :: AMISTD_2:32

canceled;

theorem :: AMISTD_2:33

canceled;

theorem Th34: :: AMISTD_2:34

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard homogeneous regular J/A-independent AMI-Struct of N
for I, J being Instruction of S st ex k being natural number st IncAddr I,k = IncAddr J,k holds
I = J

proof end;

theorem Th35: :: AMISTD_2:35

for k being natural number
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins halting steady-programmed standard homogeneous without_implicit_jumps regular J/A-independent AMI-Struct of N
for I being Instruction of S st IncAddr I,k = halt S holds
I = halt S

proof end;

theorem :: AMISTD_2:36

for k being natural number
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins halting standard homogeneous without_implicit_jumps regular J/A-independent AMI-Struct of N
for I being Instruction of S st I is sequential holds
IncAddr I,k is sequential by Th29;

theorem Th37: :: AMISTD_2:37

for k, m being natural number
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard homogeneous regular J/A-independent AMI-Struct of N
for I being Instruction of S holds IncAddr (IncAddr I,k),m = IncAddr I,(k + m)

proof end;

definition

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard-ins standard homogeneous regular J/A-independent AMI-Struct of N;
let p be NAT -defined the Instructions of S -valued finite Function;
let k be natural number ;
A1: dom p c= NAT by RELAT_1:def 18;
func IncAddr p,k -> FinPartState of S means :Def15: :: AMISTD_2:def 15
( dom it = dom p & ( for m being natural number st m in dom p holds
it . m = IncAddr (p /. m),k ) );
existence
ex b₁ being FinPartState of S st
( dom b₁ = dom p & ( for m being natural number st m in dom p holds
b₁ . m = IncAddr (p /. m),k ) )

proof end;

uniqueness
for b₁, b₂ being FinPartState of S st dom b₁ = dom p & ( for m being natural number st m in dom p holds
b₁ . m = IncAddr (p /. m),k ) & dom b₂ = dom p & ( for m being natural number st m in dom p holds
b₂ . m = IncAddr (p /. m),k ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def15 defines IncAddr AMISTD_2:def 15 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard homogeneous regular J/A-independent AMI-Struct of N
for p being NAT -defined the Instructions of b₂ -valued finite Function
for k being natural number
for b₅ being FinPartState of S holds
( b₅ = IncAddr p,k iff ( dom b₅ = dom p & ( for m being natural number st m in dom p holds
b₅ . m = IncAddr (p /. m),k ) ) );

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard-ins standard homogeneous regular J/A-independent AMI-Struct of N;
let F be NAT -defined the Instructions of S -valued finite Function;
let k be natural number ;
cluster IncAddr F,k -> NAT -defined the Instructions of S -valued ;
coherence
( IncAddr F,k is NAT -defined & IncAddr F,k is the Instructions of S -valued )

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard-ins standard regular J/A-independent AMI-Struct of N;
cluster Relation-like NAT -defined the carrier of S -defined Function-like the Object-Kind of S -compatible empty finite countable set ;
existence
ex b₁ being FinPartState of S st
( b₁ is empty & b₁ is NAT -defined )

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard-ins standard homogeneous regular J/A-independent AMI-Struct of N;
let F be NAT -defined the Instructions of S -valued empty FinPartState of ;
let k be natural number ;
cluster IncAddr F,k -> empty ;
coherence
IncAddr F,k is empty

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard-ins standard homogeneous regular J/A-independent AMI-Struct of N;
let F be NAT -defined the Instructions of S -valued non empty FinPartState of ;
let k be natural number ;
cluster IncAddr F,k -> non empty ;
coherence
not IncAddr F,k is empty

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard-ins standard homogeneous regular J/A-independent AMI-Struct of N;
let F be NAT -defined the Instructions of S -valued initial FinPartState of ;
let k be natural number ;
cluster IncAddr F,k -> initial ;
coherence
IncAddr F,k is initial

proof end;

end;

theorem Th38: :: AMISTD_2:38

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard homogeneous regular J/A-independent AMI-Struct of N
for F being NAT -defined the Instructions of b₂ -valued FinPartState of holds IncAddr F,0 = F

proof end;

theorem :: AMISTD_2:39

for k, m being natural number
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard homogeneous regular J/A-independent AMI-Struct of N
for F being NAT -defined the Instructions of b₄ -valued finite Function holds IncAddr (IncAddr F,k),m = IncAddr F,(k + m)

proof end;

definition

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard-ins standard homogeneous regular J/A-independent AMI-Struct of N;
let p be NAT -defined the Instructions of S -valued finite Function;
let k be Element of NAT ;
func Reloc p,k -> NAT -defined the Instructions of S -valued finite Function equals :: AMISTD_2:def 16
IncAddr (Shift p,k),k;
coherence
IncAddr (Shift p,k),k is NAT -defined the Instructions of S -valued finite Function ;

end;

:: deftheorem defines Reloc AMISTD_2:def 16 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard homogeneous regular J/A-independent AMI-Struct of N
for p being NAT -defined the Instructions of b₂ -valued finite Function
for k being Element of NAT holds Reloc p,k = IncAddr (Shift p,k),k;

definition

canceled;
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins halting standard homogeneous regular J/A-independent AMI-Struct of N;
let I be Instruction of S;
attr I is IC-good means :Def17: :: AMISTD_2:def 18
for k being natural number
for s1 being State of S holds (IC (Exec I,s1)) + k = IC (Exec (IncAddr I,k),(IncrIC s1,k));

end;

:: deftheorem AMISTD_2:def 17 :
canceled;

:: deftheorem Def17 defines IC-good 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 halting standard homogeneous regular J/A-independent AMI-Struct of N
for I being Instruction of S holds
( I is IC-good iff for k being natural number
for s1 being State of S holds (IC (Exec I,s1)) + k = IC (Exec (IncAddr I,k),(IncrIC s1,k)) );

definition

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins halting standard homogeneous regular J/A-independent AMI-Struct of N;
attr S is IC-good means :Def18: :: AMISTD_2:def 19
for I being Instruction of S holds I is IC-good ;

end;

:: deftheorem Def18 defines IC-good 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 halting standard homogeneous regular J/A-independent AMI-Struct of N holds
( S is IC-good iff for I being Instruction of S holds I is IC-good );

definition

let N be with_non-empty_elements set ;
let S be stored-program AMI-Struct of N;
let I be Instruction of S;
attr I is Exec-preserving means :Def19: :: AMISTD_2:def 20
for s1, s2 being State of S st s1,s2 equal_outside NAT holds
Exec I,s1, Exec I,s2 equal_outside NAT ;

end;

:: deftheorem Def19 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 );

definition

let N be with_non-empty_elements set ;
let S be stored-program AMI-Struct of N;
attr S is Exec-preserving means :Def20: :: AMISTD_2:def 21
for I being Instruction of S holds I is Exec-preserving ;

end;

:: deftheorem Def20 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 :: AMISTD_2:40

canceled;

theorem :: AMISTD_2:41

canceled;

theorem :: AMISTD_2:42

canceled;

theorem :: AMISTD_2:43

canceled;

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins halting standard homogeneous without_implicit_jumps regular J/A-independent AMI-Struct of N;
cluster sequential -> IC-good Element of the Instructions of S;
coherence
for b₁ being Instruction of S st b₁ is sequential holds
b₁ is IC-good

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins halting steady-programmed standard homogeneous without_implicit_jumps regular J/A-independent AMI-Struct of N;
cluster halting -> IC-good Element of the Instructions of S;
coherence
for b₁ being Instruction of S st b₁ is halting holds
b₁ is IC-good

proof end;

end;

theorem :: AMISTD_2:44

canceled;

theorem :: AMISTD_2:45

canceled;

registration

let N be non empty with_non-empty_elements set ;
let S be stored-program AMI-Struct of N;
cluster halting -> Exec-preserving Element of the Instructions of S;
coherence
for b₁ being Instruction of S st b₁ is halting holds
b₁ is Exec-preserving

proof end;

end;

theorem Th46: :: AMISTD_2:46

for N being non empty with_non-empty_elements set
for S being stored-program AMI-Struct of N
for I being Instruction of S st I is halting holds
I is Exec-preserving ;

registration

let N be non empty with_non-empty_elements set ;
cluster STC N -> IC-good Exec-preserving ;
coherence
( STC N is IC-good & STC N is Exec-preserving )

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
cluster non empty stored-program IC-Ins-separated definite realistic standard-ins halting steady-programmed standard homogeneous with_explicit_jumps without_implicit_jumps regular J/A-independent Exec-preserving AMI-Struct of N;
existence
ex b₁ being non empty stored-program IC-Ins-separated definite standard-ins standard regular J/A-independent AMI-Struct of N st
( b₁ is homogeneous & b₁ is realistic & b₁ is steady-programmed & b₁ is halting & b₁ is with_explicit_jumps & b₁ is without_implicit_jumps & b₁ is Exec-preserving )

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
cluster non empty stored-program IC-Ins-separated definite realistic standard-ins halting steady-programmed standard homogeneous with_explicit_jumps without_implicit_jumps regular J/A-independent IC-good Exec-preserving AMI-Struct of N;
existence
ex b₁ being non empty stored-program IC-Ins-separated definite realistic standard-ins halting steady-programmed standard homogeneous with_explicit_jumps without_implicit_jumps regular J/A-independent Exec-preserving AMI-Struct of N st b₁ is IC-good

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
cluster non empty stored-program IC-Ins-separated definite standard-ins regular J/A-independent AMI-Struct of N;
existence
ex b₁ being non empty stored-program IC-Ins-separated definite standard-ins AMI-Struct of N st
( b₁ is J/A-independent & b₁ is regular )

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
cluster Trivial-AMI N -> Exec-preserving ;
coherence
Trivial-AMI N is Exec-preserving

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
cluster non empty stored-program IC-Ins-separated definite realistic standard-ins halting steady-programmed with_explicit_jumps without_implicit_jumps regular J/A-independent Exec-preserving AMI-Struct of N;
existence
ex b₁ being non empty stored-program IC-Ins-separated definite standard-ins regular J/A-independent AMI-Struct of N st
( b₁ is halting & b₁ is realistic & b₁ is steady-programmed & b₁ is with_explicit_jumps & b₁ is without_implicit_jumps & b₁ is Exec-preserving )

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins halting standard homogeneous regular J/A-independent IC-good AMI-Struct of N;
cluster -> IC-good Element of the Instructions of S;
coherence
for b₁ being Instruction of S holds b₁ is IC-good by Def18;

end;

registration

let N be non empty with_non-empty_elements set ;
let S be stored-program Exec-preserving AMI-Struct of N;
cluster -> Exec-preserving Element of the Instructions of S;
coherence
for b₁ being Instruction of S holds b₁ is Exec-preserving by Def20;

end;

theorem :: AMISTD_2:47

canceled;

theorem :: AMISTD_2:48

canceled;

theorem :: AMISTD_2:49

canceled;

theorem Th50: :: AMISTD_2:50

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard homogeneous regular J/A-independent AMI-Struct of N
for F being NAT -defined non empty initial FinPartState of
for G being NAT -defined the Instructions of b₂ -valued non empty FinPartState of holds dom (CutLastLoc F) misses dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1))

proof end;

theorem Th51: :: AMISTD_2:51

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting standard AMI-Struct of N
for F being NAT -defined non empty initial unique-halt FinPartState of
for I being Element of NAT st I in dom (CutLastLoc F) holds
(CutLastLoc F) . I <> halt S

proof end;

definition

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard-ins standard homogeneous regular J/A-independent AMI-Struct of N;
let F, G be NAT -defined the Instructions of S -valued non empty FinPartState of ;
func F ';' G -> NAT -defined the Instructions of S -valued FinPartState of equals :: AMISTD_2:def 22
(CutLastLoc F) +* (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1));
coherence
(CutLastLoc F) +* (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1)) is NAT -defined the Instructions of S -valued FinPartState of

proof end;

end;

:: deftheorem defines ';' AMISTD_2:def 22 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard homogeneous regular J/A-independent AMI-Struct of N
for F, G being NAT -defined the Instructions of b₂ -valued non empty FinPartState of holds F ';' G = (CutLastLoc F) +* (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1));

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard-ins standard homogeneous regular J/A-independent AMI-Struct of N;
let F, G be NAT -defined the Instructions of S -valued non empty FinPartState of ;
cluster F ';' G -> NAT -defined the Instructions of S -valued non empty ;
coherence
( not F ';' G is empty & F ';' G is the Instructions of S -valued & F ';' G is NAT -defined ) ;

end;

theorem Th52: :: AMISTD_2:52

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard homogeneous regular J/A-independent AMI-Struct of N
for F being NAT -defined the Instructions of b₂ -valued non empty initial FinPartState of
for G being NAT -defined the Instructions of b₂ -valued non empty FinPartState of holds
( card (F ';' G) = ((card F) + (card G)) - 1 & card (F ';' G) = ((card F) + (card G)) -' 1 )

proof end;

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard-ins standard homogeneous regular J/A-independent AMI-Struct of N;
let F, G be NAT -defined the Instructions of S -valued non empty initial FinPartState of ;
cluster F ';' G -> NAT -defined the Instructions of S -valued initial ;
coherence
F ';' G is initial

proof end;

end;

theorem Th53: :: AMISTD_2:53

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard homogeneous regular J/A-independent AMI-Struct of N
for F, G being NAT -defined the Instructions of b₂ -valued non empty initial FinPartState of holds dom F c= dom (F ';' G)

proof end;

theorem Th54: :: AMISTD_2:54

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard homogeneous regular J/A-independent AMI-Struct of N
for F, G being NAT -defined the Instructions of b₂ -valued non empty initial FinPartState of holds CutLastLoc F c= CutLastLoc (F ';' G)

proof end;

theorem Th55: :: AMISTD_2:55

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard homogeneous regular J/A-independent AMI-Struct of N
for F, G being NAT -defined the Instructions of b₂ -valued non empty initial FinPartState of holds (F ';' G) . (LastLoc F) = (IncAddr G,((card F) -' 1)) . 0

proof end;

theorem :: AMISTD_2:56

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard homogeneous regular J/A-independent AMI-Struct of N
for F, G being NAT -defined the Instructions of b₂ -valued non empty initial FinPartState of
for f being Element of NAT st f < (card F) - 1 holds
(IncAddr F,((card F) -' 1)) . f = (IncAddr (F ';' G),((card F) -' 1)) . f

proof end;

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins halting steady-programmed standard homogeneous without_implicit_jumps regular J/A-independent AMI-Struct of N;
let F be NAT -defined the Instructions of S -valued non empty initial FinPartState of ;
let G be NAT -defined the Instructions of S -valued non empty initial halt-ending FinPartState of ;
cluster F ';' G -> NAT -defined the Instructions of S -valued halt-ending ;
coherence
F ';' G is halt-ending

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins halting steady-programmed standard homogeneous without_implicit_jumps regular J/A-independent AMI-Struct of N;
let F, G be NAT -defined the Instructions of S -valued non empty initial halt-ending unique-halt FinPartState of ;
cluster F ';' G -> NAT -defined the Instructions of S -valued unique-halt ;
coherence
F ';' G is unique-halt

proof end;

end;

definition

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins halting steady-programmed standard homogeneous without_implicit_jumps regular J/A-independent AMI-Struct of N;
let F, G be pre-Macro of S;
:: original: ';'
redefine func F ';' G -> pre-Macro of S;
coherence
F ';' G is pre-Macro of S ;

end;

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins halting steady-programmed standard homogeneous regular J/A-independent IC-good Exec-preserving AMI-Struct of N;
let F, G be NAT -defined the Instructions of S -valued non empty initial closed FinPartState of ;
cluster F ';' G -> NAT -defined the Instructions of S -valued closed ;
coherence
F ';' G is closed

proof end;

end;

theorem Th57: :: AMISTD_2:57

for k being natural number
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins halting steady-programmed standard homogeneous without_implicit_jumps regular J/A-independent AMI-Struct of N holds IncAddr (Stop S),k = Stop S

proof end;

theorem Th58: :: AMISTD_2:58

for N being non empty with_non-empty_elements set
for k being Element of NAT
for S being non empty stored-program IC-Ins-separated definite halting standard AMI-Struct of N holds Shift (Stop S),k = k .--> (halt S)

proof end;

theorem Th59: :: AMISTD_2:59

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins halting steady-programmed standard homogeneous without_implicit_jumps regular J/A-independent AMI-Struct of N
for F being pre-Macro of S holds F ';' (Stop S) = F

proof end;

theorem Th60: :: AMISTD_2:60

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins halting standard homogeneous regular J/A-independent AMI-Struct of N
for F being pre-Macro of S holds (Stop S) ';' F = F

proof end;

theorem :: AMISTD_2:61

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins halting steady-programmed standard homogeneous without_implicit_jumps regular J/A-independent AMI-Struct of N
for F, G, H being pre-Macro of S holds (F ';' G) ';' H = F ';' (G ';' H)

proof end;

theorem :: AMISTD_2:62

for N being non empty with_non-empty_elements set
for S being non empty stored-program standard-ins homogeneous regular AMI-Struct of N
for I being Instruction of S
for x being set st x in dom (JumpPart I) holds
(JumpPart I) . x in (product" (JumpParts (InsCode I))) . x

proof end;

theorem :: AMISTD_2:63

for N being non empty with_non-empty_elements set
for I being Instruction of (Trivial-AMI N) holds JumpPart I = 0 by Lm3;

theorem :: AMISTD_2:64

for N being non empty with_non-empty_elements set
for T being InsType of (Trivial-AMI N) holds JumpParts T = {0 } by Lm4;

begin

Lm7: for a, b, c being set st a c= c & b c= c \ a holds
c = (a \/ (c \ (a \/ b))) \/ b

proof end;

Lm8: for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic AMI-Struct of N holds NAT c= the carrier of S \ {(IC S)}

proof end;

theorem :: AMISTD_2:65

canceled;

theorem :: AMISTD_2:66

canceled;

theorem :: AMISTD_2:67

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic steady-programmed Exec-preserving AMI-Struct of N
for s being State of S
for i being Instruction of S
for p being NAT -defined FinPartState of holds Exec i,(s +* p) = (Exec i,s) +* p

proof end;

definition

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins halting standard homogeneous regular J/A-independent AMI-Struct of N;
let k be Element of NAT ;
let p be FinPartState of S;
func Relocated p,k -> FinPartState of S equals :: AMISTD_2:def 23
(IncrIC (NPP p),k) +* (Reloc (ProgramPart p),k);
coherence
(IncrIC (NPP p),k) +* (Reloc (ProgramPart p),k) is FinPartState of S ;

end;

:: deftheorem defines Relocated AMISTD_2:def 23 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins halting standard homogeneous regular J/A-independent AMI-Struct of N
for k being Element of NAT
for p being FinPartState of S holds Relocated p,k = (IncrIC (NPP p),k) +* (Reloc (ProgramPart p),k);

theorem :: AMISTD_2:68

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins halting standard homogeneous regular J/A-independent AMI-Struct of N
for g being FinPartState of S
for k being Element of NAT holds DataPart (Relocated g,k) = DataPart g

proof end;

theorem Th69: :: AMISTD_2:69

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins halting standard homogeneous regular J/A-independent AMI-Struct of N
for g being FinPartState of S
for k being Element of NAT holds ProgramPart (Relocated g,k) = Reloc (ProgramPart g),k

proof end;

theorem Th70: :: AMISTD_2:70

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins halting standard homogeneous regular J/A-independent AMI-Struct of N
for k being Element of NAT
for p being NAT -defined the Instructions of b₂ -valued finite Function holds dom (Reloc p,k) = { (j + k) where j is Element of NAT : j in dom p }

proof end;

theorem :: AMISTD_2:71

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins halting standard homogeneous regular J/A-independent AMI-Struct of N
for g being FinPartState of S
for il, k being Element of NAT holds
( il in dom g iff il + k in dom (Relocated g,k) )

proof end;

theorem Th72: :: AMISTD_2:72

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins halting standard homogeneous regular J/A-independent AMI-Struct of N
for g being FinPartState of S
for k being Element of NAT holds IC S in dom (Relocated g,k)

proof end;

theorem Th73: :: AMISTD_2:73

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins halting standard homogeneous regular J/A-independent AMI-Struct of N
for g being FinPartState of S
for k being Element of NAT st IC S in dom g holds
IC (Relocated g,k) = (IC g) + k

proof end;

theorem :: AMISTD_2:74

canceled;

theorem Th75: :: AMISTD_2:75

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins halting standard homogeneous regular J/A-independent AMI-Struct of N
for i, j being Element of NAT
for p being NAT -defined the Instructions of b₂ -valued FinPartState of holds Shift (IncAddr p,i),j = IncAddr (Shift p,j),i

proof end;

theorem :: AMISTD_2:76

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins halting standard homogeneous regular J/A-independent AMI-Struct of N
for g being FinPartState of S
for il, k being Element of NAT
for I being Instruction of S st il in dom (ProgramPart g) & I = g . il holds
IncAddr I,k = (Relocated g,k) . (il + k)

proof end;

theorem :: AMISTD_2:77

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins halting standard homogeneous regular J/A-independent AMI-Struct of N
for g being FinPartState of S
for k being Element of NAT st IC S in dom g holds
Start-At ((IC g) + k),S c= Relocated g,k

proof end;

theorem :: AMISTD_2:78

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins halting standard homogeneous regular J/A-independent AMI-Struct of N
for g being FinPartState of S
for k being Element of NAT
for q being data-only FinPartState of S holds Relocated (g +* q),k = (Relocated g,k) +* q

proof end;