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

begin

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

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

end;

:: deftheorem AMISTD_2:def 1 :
canceled;

:: deftheorem AMISTD_2:def 2 :
canceled;

:: deftheorem AMISTD_2:def 3 :
canceled;

:: deftheorem AMISTD_2:def 4 :
canceled;

:: deftheorem AMISTD_2:def 5 :
canceled;

:: deftheorem Def6 defines with_explicit_jumps AMISTD_2:def 6 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins AMI-Struct of N
for I being Instruction of S holds
( I is with_explicit_jumps iff JUMP I = rng (JumpPart I) );

:: deftheorem AMISTD_2:def 7 :
canceled;

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 ;
canceled;

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 AMISTD_2:def 9 :
canceled;

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;

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;

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

proof end;

Lm2: 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 regular J/A-independent with_explicit_jumps ;
coherence
( STC N is with_explicit_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 homogeneous regular J/A-independent halting standard with_explicit_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 standard & b₁ is regular & b₁ is J/A-independent & b₁ is homogeneous & b₁ is halting & b₁ is realistic & b₁ is with_explicit_jumps )

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 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 ;
coherence
Trivial-AMI N is with_explicit_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;

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

theorem :: AMISTD_2:20

canceled;

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 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 AMI-Struct of N;
let I be halting Instruction of S;
cluster JUMP I -> empty ;
coherence
JUMP I is empty by Th21;

end;

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 with_explicit_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 with_explicit_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;

registration

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

end;

begin

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 homogeneous regular J/A-independent halting with_explicit_jumps 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 COMPOS_1:92;

end;

theorem :: AMISTD_2:23

canceled;

theorem :: AMISTD_2:24

canceled;

theorem :: AMISTD_2:25

canceled;

theorem :: AMISTD_2:26

canceled;

theorem :: AMISTD_2:27

canceled;

theorem :: AMISTD_2:28

canceled;

theorem :: AMISTD_2:29

canceled;

theorem :: AMISTD_2:30

canceled;

theorem :: AMISTD_2:31

canceled;

theorem :: AMISTD_2:32

canceled;

theorem :: AMISTD_2:33

canceled;

theorem :: AMISTD_2:34

canceled;

theorem :: AMISTD_2:35

canceled;

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 homogeneous regular J/A-independent halting standard with_explicit_jumps AMI-Struct of N
for I being Instruction of S st I is sequential holds
IncAddr (I,k) is sequential by COMPOS_1:92;

definition

canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
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 homogeneous regular J/A-independent halting AMI-Struct of N;
let I be Instruction of S;
attr I is IC-relocable means :Def18: :: AMISTD_2:def 18
for j, k being natural number
for s being State of S holds (IC (Exec ((IncAddr (I,j)),s))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s,k))));

end;

:: deftheorem AMISTD_2:def 10 :
canceled;

:: deftheorem AMISTD_2:def 11 :
canceled;

:: deftheorem AMISTD_2:def 12 :
canceled;

:: deftheorem AMISTD_2:def 13 :
canceled;

:: deftheorem AMISTD_2:def 14 :
canceled;

:: deftheorem AMISTD_2:def 15 :
canceled;

:: deftheorem AMISTD_2:def 16 :
canceled;

:: deftheorem AMISTD_2:def 17 :
canceled;

:: deftheorem Def18 defines IC-relocable AMISTD_2:def 18 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent halting AMI-Struct of N
for I being Instruction of S holds
( I is IC-relocable iff for j, k being natural number
for s being State of S holds (IC (Exec ((IncAddr (I,j)),s))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s,k)))) );

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 homogeneous regular J/A-independent halting AMI-Struct of N;
attr S is IC-relocable means :Def19: :: AMISTD_2:def 19
for I being Instruction of S holds I is IC-relocable ;

end;

:: deftheorem Def19 defines IC-relocable AMISTD_2:def 19 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent halting AMI-Struct of N holds
( S is IC-relocable iff for I being Instruction of S holds I is IC-relocable );

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 :Def20: :: AMISTD_2:def 20
for s1, s2 being State of S st NPP s1 = NPP s2 holds
NPP (Exec (I,s1)) = NPP (Exec (I,s2));

end;

:: deftheorem Def20 defines Exec-preserving AMISTD_2:def 20 :
for N being with_non-empty_elements set
for S being stored-program AMI-Struct of N
for I being Instruction of S holds
( I is Exec-preserving iff for s1, s2 being State of S st NPP s1 = NPP s2 holds
NPP (Exec (I,s1)) = NPP (Exec (I,s2)) );

definition

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

end;

:: deftheorem Def21 defines Exec-preserving AMISTD_2:def 21 :
for N being with_non-empty_elements set
for S being stored-program AMI-Struct of N holds
( S is Exec-preserving iff for I being Instruction of S holds I is Exec-preserving );

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 homogeneous regular J/A-independent halting with_explicit_jumps AMI-Struct of N;
cluster sequential -> IC-relocable Element of the Instructions of S;
coherence
for b₁ being Instruction of S st b₁ is sequential holds
b₁ is IC-relocable

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 homogeneous regular J/A-independent halting with_explicit_jumps AMI-Struct of N;
cluster halting -> IC-relocable Element of the Instructions of S;
coherence
for b₁ being Instruction of S st b₁ is halting holds
b₁ is IC-relocable

proof end;

end;

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

canceled;

theorem :: AMISTD_2:38

canceled;

theorem :: AMISTD_2:39

canceled;

theorem :: AMISTD_2:40

canceled;

theorem :: AMISTD_2:41

canceled;

theorem :: AMISTD_2:42

canceled;

theorem :: AMISTD_2:43

canceled;

theorem :: AMISTD_2:44

canceled;

theorem :: AMISTD_2:45

canceled;

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-relocable Exec-preserving ;
coherence
( STC N is IC-relocable & 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 homogeneous regular J/A-independent halting standard with_explicit_jumps Exec-preserving AMI-Struct of N;
existence
ex b₁ being non empty stored-program IC-Ins-separated definite standard-ins regular J/A-independent standard AMI-Struct of N st
( b₁ is homogeneous & b₁ is realistic & b₁ is halting & b₁ is with_explicit_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 homogeneous regular J/A-independent halting standard with_explicit_jumps IC-relocable Exec-preserving AMI-Struct of N;
existence
ex b₁ being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent halting standard with_explicit_jumps Exec-preserving AMI-Struct of N st b₁ is IC-relocable

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 ;
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent halting IC-relocable AMI-Struct of N;
cluster -> IC-relocable Element of the Instructions of S;
coherence
for b₁ being Instruction of S holds b₁ is IC-relocable by Def19;

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 Def21;

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 homogeneous regular J/A-independent halting with_explicit_jumps AMI-Struct of N;
cluster with_explicit_jumps IC-relocable Element of the Instructions of S;
existence
ex b₁ being Instruction of S st b₁ is IC-relocable

proof end;

end;

theorem Th47: :: AMISTD_2:47

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

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 homogeneous regular J/A-independent halting standard with_explicit_jumps IC-relocable 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 -> closed ;
coherence
F ';' G is closed

proof end;

end;

theorem :: AMISTD_2:48

canceled;

theorem :: AMISTD_2:49

canceled;

theorem :: AMISTD_2:50

canceled;

theorem :: AMISTD_2:51

canceled;

theorem :: AMISTD_2:52

canceled;

theorem :: AMISTD_2:53

canceled;

theorem :: AMISTD_2:54

canceled;

theorem :: AMISTD_2:55

canceled;

theorem :: AMISTD_2:56

canceled;

theorem :: AMISTD_2:57

canceled;

theorem :: AMISTD_2:58

canceled;

theorem :: AMISTD_2:59

canceled;

theorem :: AMISTD_2:60

canceled;

theorem :: AMISTD_2:61

canceled;

theorem :: AMISTD_2:62

canceled;

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 Lm1;

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 Lm2;

theorem :: AMISTD_2:65

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic Exec-preserving AMI-Struct of N
for s1, s2 being State of S st s1 | ((Data-Locations S) \/ {(IC )}) = s2 | ((Data-Locations S) \/ {(IC )}) holds
for l being Instruction of S holds (Exec (l,s1)) | ((Data-Locations S) \/ {(IC )}) = (Exec (l,s2)) | ((Data-Locations S) \/ {(IC )})

proof end;

theorem :: AMISTD_2:66

for N being non empty with_non-empty_elements set
for n being Element of NAT
for S being non empty stored-program IC-Ins-separated definite realistic Exec-preserving AMI-Struct of N
for s1, s2 being State of S
for I being Program of N
for P1, P2 being the Instructions of b₃ -valued ManySortedSet of NAT st I c= P1 & I c= P2 & NPP s1 = NPP s2 & ( for m being Element of NAT st m < n holds
IC (Comput (P2,s2,m)) in dom I ) holds
for m being Element of NAT st m <= n holds
NPP (Comput (P1,s1,m)) = NPP (Comput (P2,s2,m))

proof end;

theorem ThX: :: 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 halting Exec-preserving AMI-Struct of N
for s1, s2 being State of S st NPP s1 = NPP s2 holds
for P being the Instructions of b₂ -valued ManySortedSet of NAT holds NPP (Following (P,s1)) = NPP (Following (P,s2))

proof end;

theorem ThY: :: 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 halting Exec-preserving AMI-Struct of N
for s1, s2 being State of S st NPP s1 = NPP s2 holds
for P being the Instructions of b₂ -valued ManySortedSet of NAT
for k being Nat holds NPP (Comput (P,s1,k)) = NPP (Comput (P,s2,k))

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 halting Exec-preserving AMI-Struct of N
for s1, s2 being State of S st NPP s1 = NPP s2 holds
for P being the Instructions of b₂ -valued ManySortedSet of NAT st P halts_on s1 holds
P halts_on s2

proof end;

theorem :: 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 halting Exec-preserving AMI-Struct of N
for P being the Instructions of b₂ -valued ManySortedSet of NAT
for s being State of S st NPP s = NPP (Following (P,s)) holds
for n being Element of NAT holds NPP (Comput (P,s,n)) = NPP s

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 halting Exec-preserving AMI-Struct of N
for s1, s2 being State of S st NPP s1 = NPP s2 holds
for P being the Instructions of b₂ -valued ManySortedSet of NAT st P halts_on s1 holds
NPP (Result (P,s1)) = NPP (Result (P,s2))

proof end;