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


begin

theorem Th1: :: AMI_5:1
for dl being Data-Location ex i being Element of NAT st dl = dl. i
proofend;

theorem Th2: :: AMI_5:2
for dl being Data-Location holds dl <> IC
proofend;

theorem :: AMI_5:3
for il being Element of NAT
for dl being Data-Location holds il <> dl
proofend;

theorem :: AMI_5:4
for s being State of SCM
for d being Data-Location holds d in dom s
proofend;

registration
cluster NonZero SCM ->  infinite ;
coherence
 not Data-Locations is finite by AMI_3:27;
end;

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

theorem :: AMI_5:5
for l being Instruction of SCM holds InsCode l <= 8
proofend;

theorem :: AMI_5:6
canceled;

theorem :: AMI_5:7
for ins being Instruction of SCM st InsCode ins = 0 holds
ins = halt SCM
proofend;

theorem :: AMI_5:8
for ins being Instruction of SCM st InsCode ins = 1 holds
ex da, db being Data-Location st ins = da := db
proofend;

theorem :: AMI_5:9
for ins being Instruction of SCM st InsCode ins = 2 holds
ex da, db being Data-Location st ins = AddTo (da,db)
proofend;

theorem :: AMI_5:10
for ins being Instruction of SCM st InsCode ins = 3 holds
ex da, db being Data-Location st ins = SubFrom (da,db)
proofend;

theorem :: AMI_5:11
for ins being Instruction of SCM st InsCode ins = 4 holds
ex da, db being Data-Location st ins = MultBy (da,db)
proofend;

theorem :: AMI_5:12
for ins being Instruction of SCM st InsCode ins = 5 holds
ex da, db being Data-Location st ins = Divide (da,db)
proofend;

theorem :: AMI_5:13
for ins being Instruction of SCM st InsCode ins = 6 holds
ex loc being Element of NAT st ins = SCM-goto loc
proofend;

theorem :: AMI_5:14
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
proofend;

theorem :: AMI_5:15
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
proofend;

begin

theorem :: AMI_5:16
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
proofend;

begin

registration
cluster SCM  ->  IC-recognized ;
coherence
 SCM is IC-recognized
proofend;
end;

registration
cluster SCM  ->  CurIns-recognized ;
coherence
 SCM is CurIns-recognized
proofend;
end;

theorem :: AMI_5:17
for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 &amp; p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 &amp; q 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))) &amp; I = da := db &amp; da in dom p holds
(Comput (P1,s1,i)) . db = (Comput (P2,s2,i)) . db
proofend;

theorem :: AMI_5:18
for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 &amp; p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 &amp; q 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))) &amp; I = AddTo (da,db) &amp; 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)
proofend;

theorem :: AMI_5:19
for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 &amp; p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 &amp; q 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))) &amp; I = SubFrom (da,db) &amp; 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)
proofend;

theorem :: AMI_5:20
for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 &amp; p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 &amp; q 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))) &amp; I = MultBy (da,db) &amp; 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)
proofend;

theorem :: AMI_5:21
for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 &amp; p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 &amp; q 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))) &amp; I = Divide (da,db) &amp; da in dom p &amp; 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)
proofend;

theorem :: AMI_5:22
for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 &amp; p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 &amp; q 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))) &amp; I = Divide (da,db) &amp; 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)
proofend;

theorem :: AMI_5:23
for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 &amp; p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 &amp; q 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))) &amp; I = da =0_goto loc &amp; loc <> succ (IC (Comput (P1,s1,i))) holds
( (Comput (P1,s1,i)) . da = 0 iff (Comput (P2,s2,i)) . da = 0 )
proofend;

theorem :: AMI_5:24
for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 &amp; p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 &amp; q 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))) &amp; I = da >0_goto loc &amp; loc <> succ (IC (Comput (P1,s1,i))) holds
( (Comput (P1,s1,i)) . da > 0 iff (Comput (P2,s2,i)) . da > 0 )
proofend;

theorem :: AMI_5:25
for s1, s2 being State of SCM st IC s1 = IC s2 &amp; ( for a being Data-Location holds s1 . a = s2 . a ) holds
s1 = s2
proofend;