:: On the Decomposition of the States of SCM
:: by Yasushi Tanaka
::
:: 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 ;

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
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
coherence
proof end;
end;

registration
coherence
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 b1 -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 b1 -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 b1 -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 b1 -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 b1 -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 b1 -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 b1 -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 b1 -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;