:: 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

registration

let D be set ;
cluster -> functional FinSequenceSet of D;
coherence
for b₁ being FinSequenceSet of D holds b₁ is functional ;

end;

registration

let i be Element of NAT ;
let D be set ;
cluster i -tuples_on D -> with_common_domain ;
coherence
i -tuples_on D is with_common_domain

proof end;

end;

registration

let i be Element of NAT ;
let D be set ;
cluster i -tuples_on D -> product-like ;
coherence
i -tuples_on D is product-like

proof end;

end;

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;

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

for X, IL, N being set
for S being AMI-Struct of IL,N
for F being FinPartState of S holds F \ X is FinPartState of S by CARD_3:80;

theorem Th12: :: AMISTD_2:12

for X being set
for N being with_non-empty_elements set
for IL being non empty set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N
for F being programmed FinPartState of S holds F \ X is programmed FinPartState of S

proof end;

definition

let IL be non empty set ;
canceled;
canceled;
let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N;
let i1, i2 be Instruction-Location of S;
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 IL be non empty set ;
let N be with_non-empty_elements set ;
let S be stored-program halting AMI-Struct of IL,N;
cluster halting Element of the Instructions of S;
existence
ex b₁ being Instruction of S st b₁ is halting

proof end;

end;

theorem Th13: :: AMISTD_2:13

for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for F being programmed lower FinPartState of S
for G being programmed FinPartState of S st dom F = dom G holds
G is lower

proof end;

theorem Th14: :: AMISTD_2:14

for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for F being programmed lower FinPartState of S
for f being Instruction-Location of S st f in dom F holds
locnum f < card F

proof end;

theorem Th15: :: AMISTD_2:15

for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for F being programmed lower FinPartState of S holds dom F = { (il. S,k) where k is Element of NAT : k < card F }

proof end;

definition

let IL, N be set ;
let S be AMI-Struct of IL,N;
let I be Element of the Instructions of S;
func AddressPart I -> set equals :: AMISTD_2:def 3
I `2 ;
coherence
I `2 is set ;

end;

:: deftheorem defines AddressPart AMISTD_2:def 3 :

for IL, N being set
for S being AMI-Struct of IL,N
for I being Element of the Instructions of S holds AddressPart I = I `2 ;

definition

let IL, N be set ;
let S be standard-ins AMI-Struct of IL,N;
let I be Element of the Instructions of S;
:: original: AddressPart
redefine func AddressPart I -> FinSequence of (union N) \/ the carrier of S;
coherence
AddressPart I is FinSequence of (union N) \/ the carrier of S

proof end;

end;

theorem Th16: :: AMISTD_2:16

for IL being non empty set
for N being set
for S being standard-ins AMI-Struct of IL,N
for I, J being Element of the Instructions of S st InsCode I = InsCode J & AddressPart I = AddressPart J holds
I = J

proof end;

definition

let IL, N be set ;
let S be standard-ins AMI-Struct of IL,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 (AddressPart I) = dom (AddressPart J);

end;

:: deftheorem Def4 defines homogeneous AMISTD_2:def 4 :

for IL, N being set
for S being standard-ins AMI-Struct of IL,N holds
( S is homogeneous iff for I, J being Instruction of S st InsCode I = InsCode J holds
dom (AddressPart I) = dom (AddressPart J) );

theorem Th17: :: AMISTD_2:17

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

proof end;

definition

let IL, N be set ;
let S be standard-ins AMI-Struct of IL,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 IL, N being set
for S being standard-ins AMI-Struct of IL,N
for T being InsType of S holds AddressParts T = { (AddressPart I) where I is Instruction of S : InsCode I = T } ;

registration

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

proof end;

end;

definition

let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard-ins AMI-Struct of IL,N;
let I be Instruction of S;
attr I is with_explicit_jumps means :Def6: :: AMISTD_2:def 6
for f being set st f in JUMP I holds
ex k being set st
( k in dom (AddressPart I) & f = (AddressPart I) . k & (product" (AddressParts (InsCode I))) . k = IL );
attr I is without_implicit_jumps means :Def7: :: AMISTD_2:def 7
for f being set st ex k being set st
( k in dom (AddressPart I) & f = (AddressPart I) . k & (product" (AddressParts (InsCode I))) . k = IL ) holds
f in JUMP I;

end;

:: deftheorem Def6 defines with_explicit_jumps AMISTD_2:def 6 :

for IL being non empty set
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins AMI-Struct of IL,N
for I being Instruction of S holds
( I is with_explicit_jumps iff for f being set st f in JUMP I holds
ex k being set st
( k in dom (AddressPart I) & f = (AddressPart I) . k & (product" (AddressParts (InsCode I))) . k = IL ) );

:: deftheorem Def7 defines without_implicit_jumps AMISTD_2:def 7 :

for IL being non empty set
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins AMI-Struct of IL,N
for I being Instruction of S holds
( I is without_implicit_jumps iff for f being set st ex k being set st
( k in dom (AddressPart I) & f = (AddressPart I) . k & (product" (AddressParts (InsCode I))) . k = IL ) holds
f in JUMP I );

definition

let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard-ins AMI-Struct of IL,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 IL being non empty set
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins AMI-Struct of IL,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 IL being non empty set
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins AMI-Struct of IL,N holds
( S is without_implicit_jumps iff for I being Instruction of S holds I is without_implicit_jumps );

registration

let N be 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 NAT ,N;
coherence
for b₁ being non empty stored-program IC-Ins-separated definite AMI-Struct of NAT ,N st b₁ is standard holds
verum ;

end;

registration

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

proof end;

end;

theorem Th18: :: AMISTD_2:18

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

proof end;

registration

let N be 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 IL, N be set ;
let S be standard-ins AMI-Struct of IL,N;
canceled;
attr S is regular means :Def11: :: AMISTD_2:def 11
for T being InsType of S holds AddressParts T is product-like;

end;

:: deftheorem AMISTD_2:def 10 :

canceled;

:: deftheorem Def11 defines regular AMISTD_2:def 11 :

for IL, N being set
for S being standard-ins AMI-Struct of IL,N holds
( S is regular iff for T being InsType of S holds AddressParts T is product-like );

registration

let IL, N be set ;
cluster standard-ins regular -> standard-ins homogeneous AMI-Struct of IL,N;
coherence
for b₁ being standard-ins AMI-Struct of IL,N st b₁ is regular holds
b₁ is homogeneous

proof end;

end;

theorem Th19: :: AMISTD_2:19

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

proof end;

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

proof end;

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

proof end;

registration

let N be with_non-empty_elements set ;
cluster STC N -> with_explicit_jumps without_implicit_jumps regular ;
coherence
( STC N is with_explicit_jumps & STC N is without_implicit_jumps & STC N is regular )

proof end;

end;

registration

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

proof end;

end;

registration

let IL be non empty set ;
let N be with_non-empty_elements set ;
cluster Trivial-AMI IL,N -> regular ;
coherence
Trivial-AMI IL,N is regular

proof end;

end;

registration

let IL be non empty set ;
let N be with_non-empty_elements set ;
cluster standard-ins regular AMI-Struct of IL,N;
existence
ex b₁ being standard-ins AMI-Struct of IL,N st b₁ is regular

proof end;

end;

registration

let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be standard-ins regular AMI-Struct of IL,N;
let T be InsType of S;
cluster AddressParts T -> product-like ;
coherence
AddressParts T is product-like by Def11;

end;

registration

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

proof end;

end;

registration

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

proof end;

end;

registration

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

proof end;

end;

registration

let IL be non trivial set ;
let N be with_non-empty_elements set ;
cluster non empty stored-program standard-ins regular AMI-Struct of IL,N;
existence
ex b₁ being non empty stored-program standard-ins AMI-Struct of IL,N st b₁ is regular

proof end;

end;

theorem Th20: :: AMISTD_2:20

for N being with_non-empty_elements set
for IL being non trivial set
for S being non empty stored-program standard-ins homogeneous AMI-Struct of IL,N
for I being Instruction of S
for x being set st x in dom (AddressPart I) & (product" (AddressParts (InsCode I))) . x = IL holds
(AddressPart I) . x is Instruction-Location of S

proof end;

registration

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

proof end;

end;

registration

let IL be non trivial set ;
let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard-ins with_explicit_jumps AMI-Struct of IL,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 IL be non trivial set ;
let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard-ins without_implicit_jumps AMI-Struct of IL,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 with_non-empty_elements set
for IL being non trivial set
for S being non empty stored-program IC-Ins-separated definite realistic AMI-Struct of IL,N
for I being Instruction of S st I is halting holds
JUMP I is empty

proof end;

registration

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

end;

registration

let IL be non trivial set ;
let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N;
cluster non trivial programmed Element of sproduct the Object-Kind of S;
existence
ex b₁ being FinPartState of S st
( not b₁ is trivial & b₁ is programmed )

proof end;

end;

registration

let N be with_non-empty_elements set ;
let S be non empty stored-program halting IC-Ins-separated definite standard AMI-Struct of NAT ,N;
cluster non empty trivial programmed -> non empty programmed unique-halt Element of sproduct the Object-Kind of S;
coherence
for b₁ being non empty programmed FinPartState of S st b₁ is trivial holds
b₁ is unique-halt

proof end;

end;

definition

let IL, N be set ;
let S be standard-ins AMI-Struct of IL,N;
let I be Instruction of S;
attr I is ins-loc-free means :Def12: :: AMISTD_2:def 12
for x being set st x in dom (AddressPart I) holds
(product" (AddressParts (InsCode I))) . x <> IL;

end;

:: deftheorem Def12 defines ins-loc-free AMISTD_2:def 12 :

for IL, N being set
for S being standard-ins AMI-Struct of IL,N
for I being Instruction of S holds
( I is ins-loc-free iff for x being set st x in dom (AddressPart I) holds
(product" (AddressParts (InsCode I))) . x <> IL );

theorem :: AMISTD_2:22

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

proof end;

theorem Th23: :: AMISTD_2:23

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

proof end;

registration

let IL be non trivial set ;
let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins without_implicit_jumps AMI-Struct of IL,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 by Th23;

end;

theorem Th24: :: AMISTD_2:24

for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard without_implicit_jumps AMI-Struct of NAT ,N
for I being Instruction of S st I is sequential holds
I is ins-loc-free

proof end;

registration

let N be 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 NAT ,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 by Th24;

end;

definition

let N be with_non-empty_elements set ;
let S be non empty stored-program halting IC-Ins-separated definite standard AMI-Struct of NAT ,N;
func Stop S -> FinPartState of S equals :: AMISTD_2:def 13
(il. S,0 ) .--> (halt S);
coherence
(il. S,0 ) .--> (halt S) is FinPartState of S ;

end;

:: deftheorem defines Stop AMISTD_2:def 13 :

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

Lm5: now

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

end;

registration

let N be with_non-empty_elements set ;
let S be non empty stored-program halting IC-Ins-separated definite standard AMI-Struct of NAT ,N;
cluster Stop S -> non empty trivial programmed lower ;
coherence
( Stop S is lower & not Stop S is empty & Stop S is programmed & Stop S is trivial ) by AMISTD_1:48;

end;

registration

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

end;

registration

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

end;

theorem Th25: :: AMISTD_2:25

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

proof end;

theorem Th26: :: AMISTD_2:26

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

proof end;

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

proof end;

theorem Th27: :: AMISTD_2:27

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

proof end;

registration

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

proof end;

end;

definition

let N be with_non-empty_elements set ;
let S be non empty stored-program halting IC-Ins-separated definite standard AMI-Struct of NAT ,N;
:: original: Stop
redefine func Stop S -> pre-Macro of S;
coherence
Stop S is pre-Macro of S ;

end;

definition

let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,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 & dom (AddressPart it) = dom (AddressPart I) & ( for n being set st n in dom (AddressPart I) holds
( ( (product" (AddressParts (InsCode I))) . n = NAT implies ex f being Instruction-Location of S st
( f = (AddressPart I) . n & (AddressPart it) . n = il. S,(k + (locnum f)) ) ) & ( (product" (AddressParts (InsCode I))) . n <> NAT implies (AddressPart it) . n = (AddressPart I) . n ) ) ) );
existence
ex b₁ being Instruction of S st
( InsCode b₁ = InsCode I & dom (AddressPart b₁) = dom (AddressPart I) & ( for n being set st n in dom (AddressPart I) holds
( ( (product" (AddressParts (InsCode I))) . n = NAT implies ex f being Instruction-Location of S st
( f = (AddressPart I) . n & (AddressPart b₁) . n = il. S,(k + (locnum f)) ) ) & ( (product" (AddressParts (InsCode I))) . n <> NAT implies (AddressPart b₁) . n = (AddressPart I) . n ) ) ) )

proof end;

uniqueness
for b₁, b₂ being Instruction of S st InsCode b₁ = InsCode I & dom (AddressPart b₁) = dom (AddressPart I) & ( for n being set st n in dom (AddressPart I) holds
( ( (product" (AddressParts (InsCode I))) . n = NAT implies ex f being Instruction-Location of S st
( f = (AddressPart I) . n & (AddressPart b₁) . n = il. S,(k + (locnum f)) ) ) & ( (product" (AddressParts (InsCode I))) . n <> NAT implies (AddressPart b₁) . n = (AddressPart I) . n ) ) ) & InsCode b₂ = InsCode I & dom (AddressPart b₂) = dom (AddressPart I) & ( for n being set st n in dom (AddressPart I) holds
( ( (product" (AddressParts (InsCode I))) . n = NAT implies ex f being Instruction-Location of S st
( f = (AddressPart I) . n & (AddressPart b₂) . n = il. S,(k + (locnum f)) ) ) & ( (product" (AddressParts (InsCode I))) . n <> NAT implies (AddressPart b₂) . n = (AddressPart I) . n ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def14 defines IncAddr AMISTD_2:def 14 :

for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,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 & dom (AddressPart b₅) = dom (AddressPart I) & ( for n being set st n in dom (AddressPart I) holds
( ( (product" (AddressParts (InsCode I))) . n = NAT implies ex f being Instruction-Location of S st
( f = (AddressPart I) . n & (AddressPart b₅) . n = il. S,(k + (locnum f)) ) ) & ( (product" (AddressParts (InsCode I))) . n <> NAT implies (AddressPart b₅) . n = (AddressPart I) . n ) ) ) ) );

theorem Th28: :: AMISTD_2:28

for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,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 with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,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 with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite realistic standard-ins standard without_implicit_jumps regular AMI-Struct of NAT ,N holds IncAddr (halt S),k = halt S by Th29;

registration

let N be with_non-empty_elements set ;
let S be non empty stored-program halting IC-Ins-separated definite realistic standard-ins standard without_implicit_jumps regular AMI-Struct of NAT ,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 Th31: :: AMISTD_2:31

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

proof end;

theorem Th32: :: AMISTD_2:32

for x being set
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N
for I, J being Instruction of S st ex k being natural number st IncAddr I,k = IncAddr J,k & (product" (AddressParts (InsCode I))) . x = NAT holds
(product" (AddressParts (InsCode J))) . x = NAT

proof end;

theorem Th33: :: AMISTD_2:33

for x being set
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N
for I, J being Instruction of S st ex k being natural number st IncAddr I,k = IncAddr J,k & (product" (AddressParts (InsCode I))) . x <> NAT holds
(product" (AddressParts (InsCode J))) . x <> NAT

proof end;

theorem Th34: :: AMISTD_2:34

for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,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 with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite realistic standard-ins standard without_implicit_jumps regular AMI-Struct of NAT ,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 with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite realistic standard-ins standard without_implicit_jumps regular AMI-Struct of NAT ,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 with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N
for I being Instruction of S holds IncAddr (IncAddr I,k),m = IncAddr I,(k + m)

proof end;

definition

let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N;
let p be programmed FinPartState of S;
let k be natural number ;
A1: dom p c= NAT by AMI_1:def 40;
func IncAddr p,k -> FinPartState of S means :Def15: :: AMISTD_2:def 15
( dom it = dom p & ( for m being natural number st il. S,m in dom p holds
it . (il. S,m) = IncAddr (pi p,(il. S,m)),k ) );
existence
ex b₁ being FinPartState of S st
( dom b₁ = dom p & ( for m being natural number st il. S,m in dom p holds
b₁ . (il. S,m) = IncAddr (pi p,(il. S,m)),k ) )

proof end;

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

proof end;

end;

:: deftheorem Def15 defines IncAddr AMISTD_2:def 15 :

for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N
for p being programmed FinPartState of S
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 il. S,m in dom p holds
b₅ . (il. S,m) = IncAddr (pi p,(il. S,m)),k ) ) );

registration

let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N;
let F be programmed FinPartState of S;
let k be natural number ;
cluster IncAddr F,k -> programmed ;
coherence
IncAddr F,k is programmed

proof end;

end;

registration

let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N;
let F be empty programmed FinPartState of S;
let k be natural number ;
cluster IncAddr F,k -> empty ;
coherence
IncAddr F,k is empty

proof end;

end;

registration

let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N;
let F be non empty programmed FinPartState of S;
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 with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N;
let F be programmed lower FinPartState of S;
let k be natural number ;
cluster IncAddr F,k -> lower ;
coherence
IncAddr F,k is lower

proof end;

end;

theorem Th38: :: AMISTD_2:38

for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N
for F being programmed FinPartState of S holds IncAddr F,0 = F

proof end;

theorem :: AMISTD_2:39

for k, m being natural number
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N
for F being programmed lower FinPartState of S holds IncAddr (IncAddr F,k),m = IncAddr F,(k + m)

proof end;

definition

let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N;
let p be FinPartState of S;
let k be natural number ;
func Shift p,k -> FinPartState of S means :Def16: :: AMISTD_2:def 16
( dom it = { (il. S,(m + k)) where m is Element of NAT : il. S,m in dom p } & ( for m being Element of NAT st il. S,m in dom p holds
it . (il. S,(m + k)) = p . (il. S,m) ) );
existence
ex b₁ being FinPartState of S st
( dom b₁ = { (il. S,(m + k)) where m is Element of NAT : il. S,m in dom p } & ( for m being Element of NAT st il. S,m in dom p holds
b₁ . (il. S,(m + k)) = p . (il. S,m) ) )

proof end;

uniqueness
for b₁, b₂ being FinPartState of S st dom b₁ = { (il. S,(m + k)) where m is Element of NAT : il. S,m in dom p } & ( for m being Element of NAT st il. S,m in dom p holds
b₁ . (il. S,(m + k)) = p . (il. S,m) ) & dom b₂ = { (il. S,(m + k)) where m is Element of NAT : il. S,m in dom p } & ( for m being Element of NAT st il. S,m in dom p holds
b₂ . (il. S,(m + k)) = p . (il. S,m) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def16 defines Shift AMISTD_2:def 16 :

for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for p being FinPartState of S
for k being natural number
for b₅ being FinPartState of S holds
( b₅ = Shift p,k iff ( dom b₅ = { (il. S,(m + k)) where m is Element of NAT : il. S,m in dom p } & ( for m being Element of NAT st il. S,m in dom p holds
b₅ . (il. S,(m + k)) = p . (il. S,m) ) ) );

registration

let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N;
let F be FinPartState of S;
let k be natural number ;
cluster Shift F,k -> programmed ;
coherence
Shift F,k is programmed

proof end;

end;

registration

let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N;
let F be empty FinPartState of S;
let k be natural number ;
cluster Shift F,k -> empty ;
coherence
Shift F,k is empty

proof end;

end;

registration

let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N;
let F be non empty programmed FinPartState of S;
let k be natural number ;
cluster Shift F,k -> non empty ;
coherence
not Shift F,k is empty

proof end;

end;

theorem Th40: :: AMISTD_2:40

for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for F being programmed FinPartState of S holds Shift F,0 = F

proof end;

theorem Th41: :: AMISTD_2:41

for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for F being FinPartState of S
for k being natural number st k > 0 holds
not il. S,0 in dom (Shift F,k)

proof end;

theorem :: AMISTD_2:42

for m, k being natural number
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for F being FinPartState of S holds Shift (Shift F,m),k = Shift F,(m + k)

proof end;

theorem Th43: :: AMISTD_2:43

for k being natural number
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for F being programmed FinPartState of S holds dom F, dom (Shift F,k) are_equipotent

proof end;

definition

let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N;
let I be Instruction of S;
attr I is IC-good means :Def17: :: AMISTD_2:def 17
for k being natural number
for s1, s2 being State of S st s2 = s1 +* ((IC S) .--> ((IC s1) + k)) holds
(IC (Exec I,s1)) + k = IC (Exec (IncAddr I,k),s2);

end;

:: deftheorem Def17 defines IC-good AMISTD_2:def 17 :

for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N
for I being Instruction of S holds
( I is IC-good iff for k being natural number
for s1, s2 being State of S st s2 = s1 +* ((IC S) .--> ((IC s1) + k)) holds
(IC (Exec I,s1)) + k = IC (Exec (IncAddr I,k),s2) );

definition

let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N;
attr S is IC-good means :Def18: :: AMISTD_2:def 18
for I being Instruction of S holds I is IC-good;

end;

:: deftheorem Def18 defines IC-good AMISTD_2:def 18 :

for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N holds
( S is IC-good iff for I being Instruction of S holds I is IC-good );

definition

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

end;

:: deftheorem Def19 defines Exec-preserving AMISTD_2:def 19 :

for IL being non empty set
for N being with_non-empty_elements set
for S being stored-program AMI-Struct of IL,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 IL holds
Exec I,s1, Exec I,s2 equal_outside IL );

definition

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

end;

:: deftheorem Def20 defines Exec-preserving AMISTD_2:def 20 :

for IL being non empty set
for N being with_non-empty_elements set
for S being stored-program AMI-Struct of IL,N holds
( S is Exec-preserving iff for I being Instruction of S holds I is Exec-preserving );

theorem Th44: :: AMISTD_2:44

for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard without_implicit_jumps regular AMI-Struct of NAT ,N
for I being Instruction of S st I is sequential holds
I is IC-good

proof end;

registration

let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard-ins standard without_implicit_jumps regular AMI-Struct of NAT ,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 by Th44;

end;

theorem Th45: :: AMISTD_2:45

for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins standard without_implicit_jumps regular AMI-Struct of NAT ,N
for I being Instruction of S st I is halting holds
I is IC-good

proof end;

registration

let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins standard without_implicit_jumps regular AMI-Struct of NAT ,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 by Th45;

end;

theorem Th46: :: AMISTD_2:46

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

proof end;

registration

let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be stored-program AMI-Struct of IL,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 by Th46;

end;

registration

let N be 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 with_non-empty_elements set ;
cluster non empty stored-program halting IC-Ins-separated steady-programmed definite realistic programmable standard-ins standard homogeneous with_explicit_jumps without_implicit_jumps regular IC-good Exec-preserving AMI-Struct of NAT ,N;
existence
ex b₁ being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N st
( b₁ is halting & b₁ is realistic & b₁ is steady-programmed & b₁ is programmable & b₁ is with_explicit_jumps & b₁ is without_implicit_jumps & b₁ is IC-good & b₁ is Exec-preserving )

proof end;

end;

registration

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

proof end;

end;

registration

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

proof end;

end;

registration

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

proof end;

end;

registration

let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard-ins standard regular IC-good AMI-Struct of NAT ,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 IL be non trivial set ;
let N be with_non-empty_elements set ;
let S be stored-program Exec-preserving AMI-Struct of IL,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;

definition

let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N;
let F be non empty programmed FinPartState of S;
func CutLastLoc F -> FinPartState of S equals :: AMISTD_2:def 21
F \ ((LastLoc F) .--> (F . (LastLoc F)));
coherence
F \ ((LastLoc F) .--> (F . (LastLoc F))) is FinPartState of S by CARD_3:80;

end;

:: deftheorem defines CutLastLoc AMISTD_2:def 21 :

for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for F being non empty programmed FinPartState of S holds CutLastLoc F = F \ ((LastLoc F) .--> (F . (LastLoc F)));

theorem Th47: :: AMISTD_2:47

for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for F being non empty programmed FinPartState of S holds dom (CutLastLoc F) = (dom F) \ {(LastLoc F)}

proof end;

theorem Th48: :: AMISTD_2:48

for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for F being non empty programmed FinPartState of S holds dom F = (dom (CutLastLoc F)) \/ {(LastLoc F)}

proof end;

registration

let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N;
let F be non empty trivial programmed FinPartState of S;
cluster CutLastLoc F -> empty ;
coherence
CutLastLoc F is empty

proof end;

end;

registration

let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N;
let F be non empty programmed FinPartState of S;
cluster CutLastLoc F -> programmed ;
coherence
CutLastLoc F is programmed by Th12;

end;

registration

let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N;
let F be non empty programmed lower FinPartState of S;
cluster CutLastLoc F -> lower ;
coherence
CutLastLoc F is lower

proof end;

end;

theorem Th49: :: AMISTD_2:49

for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for F being non empty programmed FinPartState of S holds card (CutLastLoc F) = (card F) - 1

proof end;

theorem Th50: :: AMISTD_2:50

for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N
for F being non empty programmed lower FinPartState of S
for G being non empty programmed FinPartState of S 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 with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite standard AMI-Struct of NAT ,N
for F being non empty programmed lower unique-halt FinPartState of S
for I being Instruction-Location of S st I in dom (CutLastLoc F) holds
(CutLastLoc F) . I <> halt S

proof end;

definition

let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N;
let F, G be non empty programmed FinPartState of S;
func F ';' G -> FinPartState of S 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 FinPartState of S ;

end;

:: deftheorem defines ';' AMISTD_2:def 22 :

for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N
for F, G being non empty programmed FinPartState of S holds F ';' G = (CutLastLoc F) +* (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1));

registration

let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N;
let F, G be non empty programmed FinPartState of S;
cluster F ';' G -> non empty programmed ;
coherence
( not F ';' G is empty & F ';' G is programmed ) ;

end;

theorem Th52: :: AMISTD_2:52

for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N
for F being non empty programmed lower FinPartState of S
for G being non empty programmed FinPartState of S holds
( card (F ';' G) = ((card F) + (card G)) - 1 & card (F ';' G) = ((card F) + (card G)) -' 1 )

proof end;

registration

let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N;
let F, G be non empty programmed lower FinPartState of S;
cluster F ';' G -> lower ;
coherence
F ';' G is lower

proof end;

end;

theorem Th53: :: AMISTD_2:53

for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N
for F, G being non empty programmed lower FinPartState of S holds dom F c= dom (F ';' G)

proof end;

theorem Th54: :: AMISTD_2:54

for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N
for F, G being non empty programmed lower FinPartState of S holds CutLastLoc F c= CutLastLoc (F ';' G)

proof end;

theorem Th55: :: AMISTD_2:55

for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N
for F, G being non empty programmed lower FinPartState of S holds (F ';' G) . (LastLoc F) = (IncAddr G,((card F) -' 1)) . (il. S,0 )

proof end;

theorem :: AMISTD_2:56

for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N
for F, G being non empty programmed lower FinPartState of S
for f being Instruction-Location of S st locnum f < (card F) - 1 holds
(IncAddr F,((card F) -' 1)) . f = (IncAddr (F ';' G),((card F) -' 1)) . f

proof end;

registration

let N be with_non-empty_elements set ;
let S be non empty stored-program halting IC-Ins-separated steady-programmed definite realistic standard-ins standard without_implicit_jumps regular AMI-Struct of NAT ,N;
let F be non empty programmed lower FinPartState of S;
let G be non empty programmed lower halt-ending FinPartState of S;
cluster F ';' G -> halt-ending ;
coherence
F ';' G is halt-ending

proof end;

end;

registration

let N be with_non-empty_elements set ;
let S be non empty stored-program halting IC-Ins-separated steady-programmed definite realistic standard-ins standard without_implicit_jumps regular AMI-Struct of NAT ,N;
let F, G be non empty programmed lower halt-ending unique-halt FinPartState of S;
cluster F ';' G -> unique-halt ;
coherence
F ';' G is unique-halt

proof end;

end;

definition

let N be with_non-empty_elements set ;
let S be non empty stored-program halting IC-Ins-separated steady-programmed definite realistic standard-ins standard without_implicit_jumps regular AMI-Struct of NAT ,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 with_non-empty_elements set ;
let S be non empty stored-program halting IC-Ins-separated steady-programmed definite realistic standard-ins standard regular IC-good Exec-preserving AMI-Struct of NAT ,N;
let F, G be non empty programmed closed lower FinPartState of S;
cluster F ';' G -> closed ;
coherence
F ';' G is closed

proof end;

end;

theorem Th57: :: AMISTD_2:57

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

proof end;

theorem Th58: :: AMISTD_2:58

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

proof end;

theorem Th59: :: AMISTD_2:59

for N being with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite realistic standard-ins standard without_implicit_jumps regular AMI-Struct of NAT ,N
for F being pre-Macro of S holds F ';' (Stop S) = F

proof end;

theorem Th60: :: AMISTD_2:60

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

proof end;

theorem :: AMISTD_2:61

for N being with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated steady-programmed definite realistic standard-ins standard without_implicit_jumps regular AMI-Struct of NAT ,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 with_non-empty_elements set
for IL being non empty set
for S being non empty stored-program standard-ins regular AMI-Struct of IL,N
for I being Instruction of S
for x being set st x in dom (AddressPart I) holds
(AddressPart I) . x in (product" (AddressParts (InsCode I))) . x

proof end;

theorem :: AMISTD_2:63

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

theorem :: AMISTD_2:64

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

theorem Th65: :: AMISTD_2:65

for k being natural number
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for l being Instruction-Location of S
for f being FinPartState of S st l in dom f holds
(Shift f,k) . (l + k) = f . l

proof end;

theorem :: AMISTD_2:66

for k being natural number
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for f being FinPartState of S holds dom (Shift f,k) = { (il + k) where il is Instruction-Location of S : il in dom f }

proof end;

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

proof end;

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

proof end;

theorem :: AMISTD_2:67

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

proof end;

definition

let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N;
let k be natural number ;
let p be FinPartState of S;
func Relocated p,k -> FinPartState of S equals :: AMISTD_2:def 23
((Start-At ((IC p) + k)) +* (IncAddr (Shift (ProgramPart p),k),k)) +* (DataPart p);
coherence
((Start-At ((IC p) + k)) +* (IncAddr (Shift (ProgramPart p),k),k)) +* (DataPart p) is FinPartState of S ;

end;

:: deftheorem defines Relocated AMISTD_2:def 23 :

for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N
for k being natural number
for p being FinPartState of S holds Relocated p,k = ((Start-At ((IC p) + k)) +* (IncAddr (Shift (ProgramPart p),k),k)) +* (DataPart p);

Lm3: now

let L, C, I be set ; :: thesis: I misses C \ (L \/ I)
set B = C \ (L \/ I);
thus I misses C \ (L \/ I) :: thesis: verum

proof

assume I meets C \ (L \/ I) ; :: thesis: contradiction
then consider o being set such that
A1: o in I and
A2: o in C \ (L \/ I) by XBOOLE_0:3;
not o in L \/ I by A2, XBOOLE_0:def 5;
hence contradiction by A1, XBOOLE_0:def 3; :: thesis: verum

end;

end;

theorem :: AMISTD_2:68

for k being natural number
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N
for g being FinPartState of S holds DataPart (Relocated g,k) = DataPart g

proof end;

theorem Th48: :: AMISTD_2:69

for k being natural number
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N
for g being FinPartState of S st S is realistic holds
ProgramPart (Relocated g,k) = IncAddr (Shift (ProgramPart g),k),k

proof end;

theorem Th49: :: AMISTD_2:70

for k being natural number
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N
for g being FinPartState of S st S is realistic holds
dom (ProgramPart (Relocated g,k)) = { (il. S,(j + k)) where j is Element of NAT : il. S,j in dom (ProgramPart g) }

proof end;

theorem :: AMISTD_2:71

for k being natural number
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N
for g being FinPartState of S
for il being Instruction-Location of S st S is realistic holds
( il in dom g iff il + k in dom (Relocated g,k) )

proof end;

theorem Th51: :: AMISTD_2:72

for k being natural number
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N
for g being FinPartState of S holds IC S in dom (Relocated g,k)

proof end;

theorem Th52: :: AMISTD_2:73

for k being natural number
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N
for g being FinPartState of S st S is realistic holds
IC (Relocated g,k) = (IC g) + k

proof end;

theorem Th53: :: AMISTD_2:74

for k being natural number
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N
for p being programmed FinPartState of S
for l being Element of NAT st l in dom p holds
(IncAddr p,k) . l = IncAddr (pi p,l),k

proof end;

registration

let N be set ;
let S be AMI-Struct of NAT ,N;
cluster -> natural Instruction-Location of S;
coherence
for b₁ being Instruction-Location of S holds b₁ is natural ;

end;

theorem Th54: :: AMISTD_2:75

for i being natural number
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N
for p being programmed FinPartState of S holds Shift (IncAddr p,i),i = IncAddr (Shift p,i),i

proof end;

theorem :: AMISTD_2:76

for k being natural number
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N
for g being FinPartState of S
for il being Instruction-Location of S st S is realistic holds
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 k being natural number
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N
for g being FinPartState of S st S is realistic holds
Start-At ((IC g) + k) c= Relocated g,k

proof end;

Lm2: for a, b, c being set holds not c in a \ ({c} \/ b)

proof end;

theorem :: AMISTD_2:78

for k being natural number
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N
for g being FinPartState of S
for q being data-only FinPartState of S st IC S in dom g holds
Relocated (g +* q),k = (Relocated g,k) +* q

proof end;