:: A Mathematical Model of CPU
:: by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received October 14, 1992
:: Copyright (c) 1992-2011 Association of Mizar Users

begin

definition

canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
let N be with_non-empty_elements set ;
let IT be non empty AMI-Struct of N;
attr IT is steady-programmed means :Def13: :: AMI_1:def 13
for s being State of IT
for i being Instruction of IT
for l being Element of NAT holds (Exec (i,s)) . l = s . l;

end;

:: deftheorem AMI_1:def 1 :
canceled;

:: deftheorem AMI_1:def 2 :
canceled;

:: deftheorem AMI_1:def 3 :
canceled;

:: deftheorem AMI_1:def 4 :
canceled;

:: deftheorem AMI_1:def 5 :
canceled;

:: deftheorem AMI_1:def 6 :
canceled;

:: deftheorem AMI_1:def 7 :
canceled;

:: deftheorem AMI_1:def 8 :
canceled;

:: deftheorem AMI_1:def 9 :
canceled;

:: deftheorem AMI_1:def 10 :
canceled;

:: deftheorem AMI_1:def 11 :
canceled;

:: deftheorem AMI_1:def 12 :
canceled;

:: deftheorem Def13 defines steady-programmed AMI_1:def 13 :
for N being with_non-empty_elements set
for IT being non empty AMI-Struct of N holds
( IT is steady-programmed iff for s being State of IT
for i being Instruction of IT
for l being Element of NAT holds (Exec (i,s)) . l = s . l );

registration

let N be with_non-empty_elements set ;
cluster Trivial-AMI N -> steady-programmed ;
coherence
Trivial-AMI N is steady-programmed

proof end;

end;

registration

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

proof end;

end;

begin

Lm1: for N being with_non-empty_elements set
for S being non empty stored-program steady-programmed AMI-Struct of N
for i being Instruction of S
for s being State of S holds ProgramPart (Exec (i,s)) = ProgramPart s

proof end;

Lm2: for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite steady-programmed AMI-Struct of N
for P being the Instructions of b₂ -valued ManySortedSet of NAT
for s being State of S
for n being Nat holds ProgramPart s = ProgramPart (Comput (P,s,n))

proof end;

theorem :: AMI_1:1

canceled;

theorem :: AMI_1:2

canceled;

theorem :: AMI_1:3

canceled;

theorem :: AMI_1:4

canceled;

theorem :: AMI_1:5

canceled;

theorem :: AMI_1:6

canceled;

theorem :: AMI_1:7

canceled;

theorem :: AMI_1:8

canceled;

theorem :: AMI_1:9

canceled;

theorem :: AMI_1:10

canceled;

theorem :: AMI_1:11

canceled;

theorem :: AMI_1:12

canceled;

theorem :: AMI_1:13

canceled;

theorem :: AMI_1:14

canceled;

theorem :: AMI_1:15

canceled;

theorem :: AMI_1:16

canceled;

theorem :: AMI_1:17

canceled;

theorem :: AMI_1:18

canceled;

theorem :: AMI_1:19

canceled;

theorem :: AMI_1:20

canceled;

theorem :: AMI_1:21

canceled;

theorem :: AMI_1:22

canceled;

theorem :: AMI_1:23

canceled;

theorem :: AMI_1:24

canceled;

theorem :: AMI_1:25

canceled;

theorem :: AMI_1:26

canceled;

theorem :: AMI_1:27

canceled;

theorem :: AMI_1:28

canceled;

theorem :: AMI_1:29

canceled;

theorem :: AMI_1:30

canceled;

theorem :: AMI_1:31

canceled;

theorem :: AMI_1:32

canceled;

theorem :: AMI_1:33

canceled;

theorem :: AMI_1:34

canceled;

theorem :: AMI_1:35

canceled;

theorem :: AMI_1:36

canceled;

theorem :: AMI_1:37

canceled;

theorem :: AMI_1:38

canceled;

theorem :: AMI_1:39

canceled;

theorem :: AMI_1:40

canceled;

theorem :: AMI_1:41

canceled;

theorem :: AMI_1:42

canceled;

theorem :: AMI_1:43

canceled;

theorem :: AMI_1:44

canceled;

theorem :: AMI_1:45

canceled;

theorem :: AMI_1:46

canceled;

theorem :: AMI_1:47

canceled;

theorem :: AMI_1:48

canceled;

theorem :: AMI_1:49

canceled;

theorem :: AMI_1:50

canceled;

theorem :: AMI_1:51

canceled;

theorem :: AMI_1:52

canceled;

theorem :: AMI_1:53

canceled;

theorem Th54: :: AMI_1:54

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite steady-programmed AMI-Struct of N
for P being the Instructions of b₂ -valued ManySortedSet of NAT
for s being State of S
for i, k being Element of NAT holds s . i = (Comput (P,s,k)) . i

proof end;

registration

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

proof end;

end;

theorem :: AMI_1:55

canceled;

theorem :: AMI_1:56

canceled;

theorem :: AMI_1:57

canceled;

theorem :: AMI_1:58

canceled;

theorem :: AMI_1:59

canceled;

theorem :: AMI_1:60

canceled;

theorem :: AMI_1:61

canceled;

theorem :: AMI_1:62

canceled;

theorem :: AMI_1:63

canceled;

theorem :: AMI_1:64

canceled;

theorem :: AMI_1:65

canceled;

theorem :: AMI_1:66

canceled;

theorem :: AMI_1:67

canceled;

theorem :: AMI_1:68

canceled;

theorem :: AMI_1:69

canceled;

theorem :: AMI_1:70

canceled;

theorem :: AMI_1:71

canceled;

theorem :: AMI_1:72

canceled;

theorem :: AMI_1:73

canceled;

theorem :: AMI_1:74

canceled;

theorem :: AMI_1:75

canceled;

theorem :: AMI_1:76

canceled;

theorem :: AMI_1:77

canceled;

theorem :: AMI_1:78

canceled;

theorem :: AMI_1:79

canceled;

theorem :: AMI_1:80

canceled;

theorem Th81: :: AMI_1:81

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite steady-programmed AMI-Struct of N
for p being NAT -defined PartState of
for P being the Instructions of b₂ -valued ManySortedSet of NAT
for s being State of S st p c= s holds
for k being Element of NAT holds p c= Comput (P,s,k)

proof end;

theorem :: AMI_1:82

canceled;

theorem :: AMI_1:83

canceled;

theorem :: AMI_1:84

canceled;

theorem :: AMI_1:85

canceled;

theorem :: AMI_1:86

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite steady-programmed AMI-Struct of N
for s being State of S
for P being the Instructions of b₂ -valued ManySortedSet of NAT
for p being NAT -defined PartState of
for k being Element of NAT holds
( p c= s iff p c= Comput (P,s,k) )

proof end;

theorem :: AMI_1:87

canceled;

theorem :: AMI_1:88

canceled;

theorem :: AMI_1:89

canceled;

theorem :: AMI_1:90

canceled;

theorem :: AMI_1:91

canceled;

theorem :: AMI_1:92

canceled;

theorem :: AMI_1:93

canceled;

theorem :: AMI_1:94

canceled;

theorem :: AMI_1:95

canceled;

theorem :: AMI_1:96

canceled;

theorem :: AMI_1:97

canceled;

theorem :: AMI_1:98

canceled;

theorem :: AMI_1:99

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite steady-programmed AMI-Struct of N
for p being PartState of S
for P being the Instructions of b₂ -valued ManySortedSet of NAT
for s being State of S st p c= s holds
for i being Element of NAT holds ProgramPart p c= Comput (P,s,i)

proof end;

theorem :: AMI_1:100

canceled;

theorem :: AMI_1:101

canceled;

theorem :: AMI_1:102

canceled;

theorem :: AMI_1:103

canceled;

theorem :: AMI_1:104

canceled;

theorem :: AMI_1:105

canceled;

theorem :: AMI_1:106

canceled;

theorem :: AMI_1:107

canceled;

theorem :: AMI_1:108

canceled;

theorem :: AMI_1:109

canceled;

theorem :: AMI_1:110

canceled;

theorem :: AMI_1:111

canceled;

theorem :: AMI_1:112

canceled;

theorem :: AMI_1:113

canceled;

theorem :: AMI_1:114

canceled;

theorem :: AMI_1:115

canceled;

theorem :: AMI_1:116

canceled;

theorem :: AMI_1:117

for N being with_non-empty_elements set
for S being non empty stored-program steady-programmed AMI-Struct of N
for i being Instruction of S
for s being State of S holds ProgramPart (Exec (i,s)) = ProgramPart s by Lm1;

theorem :: AMI_1:118

canceled;

theorem :: AMI_1:119

canceled;

theorem :: AMI_1:120

canceled;

theorem :: AMI_1:121

canceled;

theorem :: AMI_1:122

canceled;

theorem :: AMI_1:123

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite steady-programmed AMI-Struct of N
for P being the Instructions of b₂ -valued ManySortedSet of NAT
for s being State of S
for n being Nat holds ProgramPart s = ProgramPart (Comput (P,s,n)) by Lm2;

theorem :: AMI_1:124

for i being Element of NAT
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite steady-programmed AMI-Struct of N
for p being NAT -defined the Instructions of b₃ -valued Function
for s1, s2 being State of S st p c= s1 & p c= s2 holds
(Comput ((ProgramPart s1),s1,i)) | (dom p) = (Comput ((ProgramPart s2),s2,i)) | (dom p)

proof end;

set III = {[1,0,0],[0,0,0]};

registration

let N be with_non-empty_elements set ;
cluster STC N -> steady-programmed ;
coherence
STC N is steady-programmed

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 standard steady-programmed 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 halting & b₁ is realistic & b₁ is steady-programmed & b₁ is standard-ins )

proof end;

end;

begin

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

proof end;

Lm4: 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 )}

proof end;

theorem :: AMI_1:125

canceled;

theorem :: AMI_1:126

canceled;

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 steady-programmed 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 )

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 steady-programmed 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 steady-programmed & 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 steady-programmed 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 steady-programmed AMI-Struct of N st b₁ is IC-relocable

proof end;

end;

theorem :: AMI_1:127

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic Exec-preserving steady-programmed 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;

set S1 = { [0,{},<*k1*>] where k1 is Element of INT : verum } ;

set S2 = { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } ;

set S3 = { [I1,{},<*d2,k2*>] where I1 is Element of Segm 14, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I1 in {2,3} } ;

set S4 = { [I2,{},<*d3,k3,k4*>] where I2 is Element of Segm 14, d3 is Element of SCM-Data-Loc , k3, k4 is Element of INT : I2 in {4,5,6,7,8} } ;

set S5 = { [I3,{},<*d4,d5,k5,k6*>] where I3 is Element of Segm 14, d4, d5 is Element of SCM-Data-Loc , k5, k6 is Element of INT : I3 in {9,10,11,12,13} } ;

Lm2: for I being Instruction of SCMPDS holds
( I in { [0,{},<*k1*>] where k1 is Element of INT : verum } or I in { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } or I in { [I1,{},<*d2,k2*>] where I1 is Element of Segm 14, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I1 in {2,3} } or I in { [I2,{},<*d3,k3,k4*>] where I2 is Element of Segm 14, d3 is Element of SCM-Data-Loc , k3, k4 is Element of INT : I2 in {4,5,6,7,8} } or I in { [I3,{},<*d4,d5,k5,k6*>] where I3 is Element of Segm 14, d4, d5 is Element of SCM-Data-Loc , k5, k6 is Element of INT : I3 in {9,10,11,12,13} } )

proof end;

theorem Th96: :: AMI_1:128

for s being State of SCMPDS
for i being Instruction of SCMPDS
for l being Element of NAT holds (Exec (i,s)) . l = s . l

proof end;

registration

cluster SCMPDS -> steady-programmed ;
coherence
SCMPDS is steady-programmed

proof end;

end;