:: On the Decomposition of the States of SCM
:: by Yasushi Tanaka
::
:: Received November 23, 1993
:: Copyright (c) 1993-2011 Association of Mizar Users

begin

theorem :: AMI_5:1

canceled;

theorem :: AMI_5:2

canceled;

theorem :: AMI_5:3

canceled;

theorem :: AMI_5:4

canceled;

theorem :: AMI_5:5

canceled;

theorem :: AMI_5:6

canceled;

theorem :: AMI_5:7

canceled;

theorem :: AMI_5:8

canceled;

theorem :: AMI_5:9

canceled;

theorem :: AMI_5:10

canceled;

theorem :: AMI_5:11

canceled;

theorem :: AMI_5:12

canceled;

theorem :: AMI_5:13

canceled;

theorem :: AMI_5:14

canceled;

theorem :: AMI_5:15

canceled;

theorem :: AMI_5:16

canceled;

theorem :: AMI_5:17

canceled;

theorem Th18: :: AMI_5:18

for dl being Data-Location ex i being Element of NAT st dl = dl. i

proof end;

theorem :: AMI_5:19

canceled;

theorem Th20: :: AMI_5:20

for dl being Data-Location holds dl <> IC

proof end;

theorem :: AMI_5:21

canceled;

theorem Th22: :: AMI_5:22

for il being Element of NAT
for dl being Data-Location holds il <> dl

proof end;

theorem :: AMI_5:23

canceled;

theorem :: AMI_5:24

for s being State of SCM
for d being Data-Location holds d in dom s

proof end;

theorem :: AMI_5:25

canceled;

theorem :: AMI_5:26

for s1, s2 being State of SCM st IC s1 = IC s2 & ( for a being Data-Location holds s1 . a = s2 . a ) & ( for i being Element of NAT holds s1 . i = s2 . i ) holds
s1 = s2

proof end;

registration

cluster Data-Locations SCM -> infinite ;
coherence
not Data-Locations SCM is finite by AMI_3:72;

end;

Lm1: for b being Element of Data-Locations SCM holds b is Data-Location

proof end;

theorem :: AMI_5:27

canceled;

theorem :: AMI_5:28

canceled;

theorem :: AMI_5:29

canceled;

theorem :: AMI_5:30

canceled;

theorem :: AMI_5:31

canceled;

theorem :: AMI_5:32

canceled;

theorem :: AMI_5:33

canceled;

theorem :: AMI_5:34

canceled;

theorem :: AMI_5:35

canceled;

theorem :: AMI_5:36

for l being Instruction of SCM holds InsCode l <= 8

proof end;

theorem Th37: :: AMI_5:37

InsCode (halt SCM) = 0 by AMI_3:71, RECDEF_2:def 1;

theorem :: AMI_5:38

canceled;

theorem :: AMI_5:39

canceled;

theorem :: AMI_5:40

canceled;

theorem :: AMI_5:41

canceled;

theorem :: AMI_5:42

canceled;

theorem :: AMI_5:43

canceled;

theorem :: AMI_5:44

canceled;

theorem :: AMI_5:45

canceled;

theorem :: AMI_5:46

for ins being Instruction of SCM st InsCode ins = 0 holds
ins = halt SCM

proof end;

theorem :: AMI_5:47

for ins being Instruction of SCM st InsCode ins = 1 holds
ex da, db being Data-Location st ins = da := db

proof end;

theorem :: AMI_5:48

for ins being Instruction of SCM st InsCode ins = 2 holds
ex da, db being Data-Location st ins = AddTo (da,db)

proof end;

theorem :: AMI_5:49

for ins being Instruction of SCM st InsCode ins = 3 holds
ex da, db being Data-Location st ins = SubFrom (da,db)

proof end;

theorem :: AMI_5:50

for ins being Instruction of SCM st InsCode ins = 4 holds
ex da, db being Data-Location st ins = MultBy (da,db)

proof end;

theorem :: AMI_5:51

for ins being Instruction of SCM st InsCode ins = 5 holds
ex da, db being Data-Location st ins = Divide (da,db)

proof end;

theorem :: AMI_5:52

for ins being Instruction of SCM st InsCode ins = 6 holds
ex loc being Element of NAT st ins = SCM-goto loc

proof end;

theorem :: AMI_5:53

for ins being Instruction of SCM st InsCode ins = 7 holds
ex loc being Element of NAT ex da being Data-Location st ins = da =0_goto loc

proof end;

theorem :: AMI_5:54

for ins being Instruction of SCM st InsCode ins = 8 holds
ex loc being Element of NAT ex da being Data-Location st ins = da >0_goto loc

proof end;

begin

theorem :: AMI_5:55

canceled;

theorem :: AMI_5:56

canceled;

theorem :: AMI_5:57

canceled;

theorem :: AMI_5:58

canceled;

theorem :: AMI_5:59

canceled;

theorem :: AMI_5:60

canceled;

theorem :: AMI_5:61

canceled;

theorem :: AMI_5:62

canceled;

theorem :: AMI_5:63

canceled;

theorem :: AMI_5:64

canceled;

theorem :: AMI_5:65

canceled;

theorem :: AMI_5:66

canceled;

theorem :: AMI_5:67

canceled;

theorem :: AMI_5:68

canceled;

theorem :: AMI_5:69

canceled;

theorem :: AMI_5:70

canceled;

theorem :: AMI_5:71

canceled;

theorem :: AMI_5:72

canceled;

theorem :: AMI_5:73

canceled;

theorem :: AMI_5:74

canceled;

theorem :: AMI_5:75

canceled;

theorem :: AMI_5:76

canceled;

theorem :: AMI_5:77

canceled;

theorem :: AMI_5:78

canceled;

theorem :: AMI_5:79

canceled;

theorem :: AMI_5:80

for s being State of SCM
for iloc being Element of NAT
for a being Data-Location holds s . a = (s +* (Start-At (iloc,SCM))) . a

proof end;

begin

registration

cluster SCM -> IC-recognized ;
coherence
SCM is IC-recognized

proof end;

end;

registration

cluster SCM -> CurIns-recognized ;
coherence
SCM is CurIns-recognized

proof end;

end;

theorem :: AMI_5:81

canceled;

theorem :: AMI_5:82

canceled;

theorem :: AMI_5:83

canceled;

theorem :: AMI_5:84

canceled;

theorem :: AMI_5:85

canceled;

theorem :: AMI_5:86

canceled;

theorem :: AMI_5:87

canceled;

Lm2: for da being Data-Location
for p being PartState of SCM st da in dom p holds
da in dom (NPP p)

proof end;

theorem :: AMI_5:88

for p being non NAT -defined autonomic FinPartState of
for s1, s2 being State of SCM st NPP p c= s1 & NPP p c= s2 holds
for P1, P2 being the Instructions of SCM -valued ManySortedSet of NAT st ProgramPart p c= P1 & ProgramPart p c= P2 holds
for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = da := db & da in dom p holds
(Comput (P1,s1,i)) . db = (Comput (P2,s2,i)) . db

proof end;

theorem :: AMI_5:89

for p being non NAT -defined autonomic FinPartState of
for s1, s2 being State of SCM st NPP p c= s1 & NPP p c= s2 holds
for P1, P2 being the Instructions of SCM -valued ManySortedSet of NAT st ProgramPart p c= P1 & ProgramPart p c= P2 holds
for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = AddTo (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) + ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db)

proof end;

theorem :: AMI_5:90

for p being non NAT -defined autonomic FinPartState of
for s1, s2 being State of SCM st NPP p c= s1 & NPP p c= s2 holds
for P1, P2 being the Instructions of SCM -valued ManySortedSet of NAT st ProgramPart p c= P1 & ProgramPart p c= P2 holds
for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = SubFrom (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db)

proof end;

theorem :: AMI_5:91

for p being non NAT -defined autonomic FinPartState of
for s1, s2 being State of SCM st NPP p c= s1 & NPP p c= s2 holds
for P1, P2 being the Instructions of SCM -valued ManySortedSet of NAT st ProgramPart p c= P1 & ProgramPart p c= P2 holds
for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = MultBy (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) * ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db)

proof end;

theorem :: AMI_5:92

for p being non NAT -defined autonomic FinPartState of
for s1, s2 being State of SCM st NPP p c= s1 & NPP p c= s2 holds
for P1, P2 being the Instructions of SCM -valued ManySortedSet of NAT st ProgramPart p c= P1 & ProgramPart p c= P2 holds
for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = Divide (da,db) & da in dom p & da <> db holds
((Comput (P1,s1,i)) . da) div ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) div ((Comput (P2,s2,i)) . db)

proof end;

theorem :: AMI_5:93

for p being non NAT -defined autonomic FinPartState of
for s1, s2 being State of SCM st NPP p c= s1 & NPP p c= s2 holds
for P1, P2 being the Instructions of SCM -valued ManySortedSet of NAT st ProgramPart p c= P1 & ProgramPart p c= P2 holds
for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = Divide (da,db) & db in dom p holds
((Comput (P1,s1,i)) . da) mod ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db)

proof end;

theorem :: AMI_5:94

for p being non NAT -defined autonomic FinPartState of
for s1, s2 being State of SCM st NPP p c= s1 & NPP p c= s2 holds
for P1, P2 being the Instructions of SCM -valued ManySortedSet of NAT st ProgramPart p c= P1 & ProgramPart p c= P2 holds
for i being Element of NAT
for da being Data-Location
for loc being Element of NAT
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = da =0_goto loc & loc <> succ (IC (Comput (P1,s1,i))) holds
( (Comput (P1,s1,i)) . da = 0 iff (Comput (P2,s2,i)) . da = 0 )

proof end;

theorem :: AMI_5:95

for p being non NAT -defined autonomic FinPartState of
for s1, s2 being State of SCM st NPP p c= s1 & NPP p c= s2 holds
for P1, P2 being the Instructions of SCM -valued ManySortedSet of NAT st ProgramPart p c= P1 & ProgramPart p c= P2 holds
for i being Element of NAT
for da being Data-Location
for loc being Element of NAT
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = da >0_goto loc & loc <> succ (IC (Comput (P1,s1,i))) holds
( (Comput (P1,s1,i)) . da > 0 iff (Comput (P2,s2,i)) . da > 0 )

proof end;

theorem :: AMI_5:96

for s1, s2 being State of SCM st IC s1 = IC s2 & ( for a being Data-Location holds s1 . a = s2 . a ) holds
NPP s1 = NPP s2

proof end;