:: 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 )} \/ SCM-Data-Loc ) \/ NAT by AMI_3:4;

theorem :: AMI_5:24

for s being State of SCM
for d being Data-Location
for l being Element of NAT holds
( d in dom s & l 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

for s being State of SCM holds SCM-Data-Loc c= dom s by AMI_3:72, SCMNORM:13;

theorem Th28: :: AMI_5:28

for s being State of SCM holds NAT c= dom s

proof end;

theorem :: AMI_5:29

canceled;

theorem :: AMI_5:30

for s being State of SCM holds dom (s | NAT ) = NAT

proof end;

theorem :: AMI_5:31

not SCM-Data-Loc is finite ;

theorem :: AMI_5:32

not NAT is finite ;

registration

cluster SCM-Data-Loc -> infinite ;
coherence
not SCM-Data-Loc is finite ;

end;

definition

canceled;
let I be Instruction of SCM ;
func @ I -> Element of SCM-Instr equals :: AMI_5:def 2
I;
coherence
I is Element of SCM-Instr ;

end;

:: deftheorem AMI_5:def 1 :

canceled;

:: deftheorem defines @ AMI_5:def 2 :

for I being Instruction of SCM holds @ I = I;

definition

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

end;

:: deftheorem AMI_5:def 3 :

canceled;

:: deftheorem defines @ AMI_5:def 4 :

for loc being Element of SCM-Data-Loc 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, MCART_1:7;

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

for loc being Element of NAT holds (@ (SCM-goto loc)) jump_address = loc

proof end;

theorem :: AMI_5:56

for loc being Element of NAT
for a being Data-Location holds
( (@ (a =0_goto loc)) cjump_address = loc & (@ (a =0_goto loc)) cond_address = a )

proof end;

theorem :: AMI_5:57

for loc being Element of NAT
for a being Data-Location holds
( (@ (a >0_goto loc)) cjump_address = loc & (@ (a >0_goto loc)) cond_address = a )

proof end;

theorem Th58: :: AMI_5:58

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

proof end;

theorem Th59: :: AMI_5:59

for i being Instruction of SCM
for s being State of SCM holds (Exec i,s) | NAT = s | NAT

proof end;

begin

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

for i being Instruction of SCM
for s being State of SCM
for p being NAT -defined FinPartState of holds Exec i,(s +* p) = (Exec i,s) +* p

proof end;

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;

registration

cluster Relation-like non NAT -defined the carrier of SCM -defined Function-like the Object-Kind of SCM -compatible finite V61() autonomic set ;
existence
ex b₁ being FinPartState of SCM st
( b₁ is autonomic & not b₁ is NAT -defined )

proof end;

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 (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i) holds
( IC (Comput (ProgramPart s1),s1,i) = IC (Comput (ProgramPart s2),s2,i) & I = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),(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 (Comput (ProgramPart s1),s1,i)),(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 (Comput (ProgramPart s1),s1,i)),(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 (Comput (ProgramPart s1),s1,i)),(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 (Comput (ProgramPart s1),s1,i)),(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 (Comput (ProgramPart s1),s1,i)),(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 (Comput (ProgramPart s1),s1,i)),(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 (Comput (ProgramPart s1),s1,i)),(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 (Comput (ProgramPart s1),s1,i)),(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;