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

theorem Th1: :: AMI_5:1

for dl being Data-Location ex i being Nat st dl = dl. i

proof end;

theorem Th2: :: AMI_5:2

for dl being Data-Location holds dl <> IC by Th1, AMI_3:13;

theorem :: AMI_5:3

for il being Nat
for dl being Data-Location holds il <> dl

proof end;

theorem :: AMI_5:4

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

proof end;

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

proof end;

theorem :: AMI_5:5

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

proof end;

theorem :: AMI_5:6

canceled;

::$CT

theorem :: AMI_5:7

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

proof end;

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

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

theorem :: AMI_5:13

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

proof end;

theorem :: AMI_5:14

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

proof end;

theorem :: AMI_5:15

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

proof end;

theorem :: AMI_5:16

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

proof end;

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:17

for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function
for p being non empty b₁ -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being 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:18

for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function
for p being non empty b₁ -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being 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:19

for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function
for p being non empty b₁ -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being 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:20

for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function
for p being non empty b₁ -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being 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:21

for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function
for p being non empty b₁ -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being 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:22

for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function
for p being non empty b₁ -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being 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:23

for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function
for p being non empty b₁ -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Nat
for da being Data-Location
for loc being Nat
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = da =0_goto loc & loc <> (IC (Comput (P1,s1,i))) + 1 holds
( (Comput (P1,s1,i)) . da = 0 iff (Comput (P2,s2,i)) . da = 0 )

proof end;

theorem :: AMI_5:24

for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function
for p being non empty b₁ -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Nat
for da being Data-Location
for loc being Nat
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = da >0_goto loc & loc <> (IC (Comput (P1,s1,i))) + 1 holds
( (Comput (P1,s1,i)) . da > 0 iff (Comput (P2,s2,i)) . da > 0 )

proof end;

theorem :: AMI_5:25

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

proof end;