:: On the Decomposition of the States of SCM
:: by Yasushi Tanaka
::
:: Received November 23, 1993
:: Copyright (c) 1993 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 SCM

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

the carrier of SCM = ({(IC SCM)} \/ (Data-Locations SCM)) \/ NAT by AMI_3:4, AMI_3:72;

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;

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;

registration

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

end;

definition

canceled;
canceled;
canceled;
let loc be Element of Data-Locations SCM;
func loc @ -> Data-Location equals :: AMI_5:def 4
loc;
coherence
loc is Data-Location

proof end;

end;

:: deftheorem AMI_5:def 1 :
canceled;

:: deftheorem AMI_5:def 2 :
canceled;

:: deftheorem AMI_5:def 3 :
canceled;

:: deftheorem defines @ AMI_5:def 4 :
for loc being Element of Data-Locations SCM holds loc @ = loc;

theorem :: AMI_5:33

canceled;

theorem :: AMI_5:34

canceled;

theorem :: AMI_5:35

canceled;

theorem Th36: :: 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 Th46: :: AMI_5:46

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

proof end;

theorem Th47: :: 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 Th48: :: 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 Th49: :: 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 Th50: :: 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 Th51: :: 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 Th52: :: 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 Th53: :: 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 Th54: :: 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;

theorem :: AMI_5:55

canceled;

theorem :: AMI_5:56

canceled;

theorem :: AMI_5:57

canceled;

theorem :: AMI_5:58

for s1, s2 being State of SCM st s1 | ((Data-Locations SCM) \/ {(IC SCM)}) = s2 | ((Data-Locations SCM) \/ {(IC SCM)}) holds
for l being Instruction of SCM holds (Exec (l,s1)) | ((Data-Locations SCM) \/ {(IC SCM)}) = (Exec (l,s2)) | ((Data-Locations SCM) \/ {(IC SCM)})

proof end;

begin

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

theorem :: AMI_5:81

canceled;

theorem :: AMI_5:82

canceled;

theorem Th83: :: AMI_5:83

for p being autonomic FinPartState of SCM st DataPart p <> {} holds
IC SCM in dom p

proof end;

theorem Th84: :: AMI_5:84

for p being non NAT -defined autonomic FinPartState of holds IC SCM in dom p

proof end;

theorem :: AMI_5:85

for p being autonomic FinPartState of SCM st IC SCM in dom p holds
IC p in dom p

proof end;

theorem Th86: :: AMI_5:86

for p being non NAT -defined autonomic FinPartState of
for s being State of SCM st p c= s holds
for i being Element of NAT holds IC (Comput ((ProgramPart s),s,i)) in dom (ProgramPart p)

proof end;

theorem Th87: :: AMI_5:87

for p being non NAT -defined autonomic FinPartState of
for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for i being Element of NAT
for I being Instruction of SCM st I = CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,i))) holds
( IC (Comput ((ProgramPart s1),s1,i)) = IC (Comput ((ProgramPart s2),s2,i)) & I = CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),s2,i))) )

proof end;

theorem :: AMI_5:88

for p being non NAT -defined autonomic FinPartState of
for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,i))) & I = da := db & da in dom p holds
(Comput ((ProgramPart s1),s1,i)) . db = (Comput ((ProgramPart s2),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 p c= s1 & p c= s2 holds
for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,i))) & I = AddTo (da,db) & da in dom p holds
((Comput ((ProgramPart s1),s1,i)) . da) + ((Comput ((ProgramPart s1),s1,i)) . db) = ((Comput ((ProgramPart s2),s2,i)) . da) + ((Comput ((ProgramPart s2),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 p c= s1 & p c= s2 holds
for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,i))) & I = SubFrom (da,db) & da in dom p holds
((Comput ((ProgramPart s1),s1,i)) . da) - ((Comput ((ProgramPart s1),s1,i)) . db) = ((Comput ((ProgramPart s2),s2,i)) . da) - ((Comput ((ProgramPart s2),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 p c= s1 & p c= s2 holds
for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,i))) & I = MultBy (da,db) & da in dom p holds
((Comput ((ProgramPart s1),s1,i)) . da) * ((Comput ((ProgramPart s1),s1,i)) . db) = ((Comput ((ProgramPart s2),s2,i)) . da) * ((Comput ((ProgramPart s2),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 p c= s1 & p c= s2 holds
for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,i))) & I = Divide (da,db) & da in dom p & da <> db holds
((Comput ((ProgramPart s1),s1,i)) . da) div ((Comput ((ProgramPart s1),s1,i)) . db) = ((Comput ((ProgramPart s2),s2,i)) . da) div ((Comput ((ProgramPart s2),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 p c= s1 & p c= s2 holds
for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,i))) & I = Divide (da,db) & db in dom p holds
((Comput ((ProgramPart s1),s1,i)) . da) mod ((Comput ((ProgramPart s1),s1,i)) . db) = ((Comput ((ProgramPart s2),s2,i)) . da) mod ((Comput ((ProgramPart s2),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 p c= s1 & p c= s2 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 ((ProgramPart s1),(Comput ((ProgramPart s1),s1,i))) & I = da =0_goto loc & loc <> succ (IC (Comput ((ProgramPart s1),s1,i))) holds
( (Comput ((ProgramPart s1),s1,i)) . da = 0 iff (Comput ((ProgramPart s2),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 p c= s1 & p c= s2 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 ((ProgramPart s1),(Comput ((ProgramPart s1),s1,i))) & I = da >0_goto loc & loc <> succ (IC (Comput ((ProgramPart s1),s1,i))) holds
( (Comput ((ProgramPart s1),s1,i)) . da > 0 iff (Comput ((ProgramPart s2),s2,i)) . da > 0 )

proof end;