:: Computation and Program Shift in the SCMPDS Computer
:: by JingChao Chen
::
:: Received June 15, 1999
:: Copyright (c) 1999-2012 Association of Mizar Users


begin

theorem :: SCMPDS_3:1
for k1 being Integer
for s1, s2 being State of SCMPDS st IC s1 = IC s2 holds
ICplusConst (s1,k1) = ICplusConst (s2,k1)
proofend;

theorem :: SCMPDS_3:2
for k1 being Integer
for a being Int_position
for s1, s2 being State of SCMPDS st DataPart s1 = DataPart s2 holds
s1 . (DataLoc ((s1 . a),k1)) = s2 . (DataLoc ((s2 . a),k1))
proofend;

theorem :: SCMPDS_3:3
for a being Int_position
for s1, s2 being State of SCMPDS st DataPart s1 = DataPart s2 holds
s1 . a = s2 . a
proofend;

theorem :: SCMPDS_3:4
not IC in SCM-Data-Loc
proofend;

begin

theorem :: SCMPDS_3:5
canceled;

theorem :: SCMPDS_3:6
for s being State of SCMPDS
for iloc being Element of NAT
for a being Int_position holds s . a = (s +* (Start-At (iloc,SCMPDS))) . a
proofend;

theorem :: SCMPDS_3:7
for s, t being State of SCMPDS holds s +* (t | SCM-Data-Loc) is State of SCMPDS ;

begin

definition
let la be Int_position;
let a be Integer;
:: original:.-->
redefine funcla .--> a ->  FinPartState of SCMPDS;
coherence
 la .--> a is FinPartState of SCMPDS
proofend;
end;

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

theorem Th8: :: SCMPDS_3:8
for s1, s2 being State of SCMPDS
for k1, k2, m being Integer st IC s1 = IC s2 &amp; k1 <> k2 &amp; m = IC s1 &amp; m + k1 >= 0 &amp; m + k2 >= 0 holds
ICplusConst (s1,k1) <> ICplusConst (s2,k2)
proofend;

theorem :: SCMPDS_3:9
for s1, s2 being State of SCMPDS
for k1, k2 being Element of NAT st IC s1 = IC s2 &amp; k1 <> k2 holds
ICplusConst (s1,k1) <> ICplusConst (s2,k2)
proofend;

theorem Th10: :: SCMPDS_3:10
for s being State of SCMPDS holds succ (IC s) = ICplusConst (s,1)
proofend;

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

theorem :: SCMPDS_3:11
for P1, P2 being Instruction-Sequence of SCMPDS
for q being NAT -defined the InstructionsF of SCMPDS -valued finite non halt-free Function
for p being non empty b3 -autonomic FinPartState of SCMPDS
for s1, s2 being State of SCMPDS st p c= s1 &amp; p c= s2 &amp; q c= P1 &amp; q c= P2 holds
for i being Element of NAT
for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) := (b,k2) &amp; a in dom p &amp; DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2))
proofend;

theorem :: SCMPDS_3:12
for P1, P2 being Instruction-Sequence of SCMPDS
for q being NAT -defined the InstructionsF of SCMPDS -valued finite non halt-free Function
for p being non empty b3 -autonomic FinPartState of SCMPDS
for s1, s2 being State of SCMPDS st p c= s1 &amp; p c= s2 &amp; q c= P1 &amp; q c= P2 holds
for i being Element of NAT
for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = AddTo (a,k1,b,k2) &amp; a in dom p &amp; DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2))
proofend;

theorem :: SCMPDS_3:13
for P1, P2 being Instruction-Sequence of SCMPDS
for q being NAT -defined the InstructionsF of SCMPDS -valued finite non halt-free Function
for p being non empty b3 -autonomic FinPartState of SCMPDS
for s1, s2 being State of SCMPDS st p c= s1 &amp; p c= s2 &amp; q c= P1 &amp; q c= P2 holds
for i being Element of NAT
for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = SubFrom (a,k1,b,k2) &amp; a in dom p &amp; DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2))
proofend;

theorem :: SCMPDS_3:14
for P1, P2 being Instruction-Sequence of SCMPDS
for q being NAT -defined the InstructionsF of SCMPDS -valued finite non halt-free Function
for p being non empty b3 -autonomic FinPartState of SCMPDS
for s1, s2 being State of SCMPDS st p c= s1 &amp; p c= s2 &amp; q c= P1 &amp; q c= P2 holds
for i being Element of NAT
for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = MultBy (a,k1,b,k2) &amp; a in dom p &amp; DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1))) * ((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2))) = ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1))) * ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2)))
proofend;

theorem :: SCMPDS_3:15
for P1, P2 being Instruction-Sequence of SCMPDS
for q being NAT -defined the InstructionsF of SCMPDS -valued finite non halt-free Function
for p being non empty b3 -autonomic FinPartState of SCMPDS
for s1, s2 being State of SCMPDS st p c= s1 &amp; p c= s2 &amp; q c= P1 &amp; q c= P2 holds
for i, m being Element of NAT
for a being Int_position
for k1, k2 being Integer st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) <>0_goto k2 &amp; m = IC (Comput (P1,s1,i)) &amp; m + k2 >= 0 &amp; k2 <> 1 holds
( (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = 0 iff (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) = 0 )
proofend;

theorem :: SCMPDS_3:16
for P1, P2 being Instruction-Sequence of SCMPDS
for q being NAT -defined the InstructionsF of SCMPDS -valued finite non halt-free Function
for p being non empty b3 -autonomic FinPartState of SCMPDS
for s1, s2 being State of SCMPDS st p c= s1 &amp; p c= s2 &amp; q c= P1 &amp; q c= P2 holds
for i, m being Element of NAT
for a being Int_position
for k1, k2 being Integer st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) <=0_goto k2 &amp; m = IC (Comput (P1,s1,i)) &amp; m + k2 >= 0 &amp; k2 <> 1 holds
( (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) > 0 iff (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) > 0 )
proofend;

theorem :: SCMPDS_3:17
for P1, P2 being Instruction-Sequence of SCMPDS
for q being NAT -defined the InstructionsF of SCMPDS -valued finite non halt-free Function
for p being non empty b3 -autonomic FinPartState of SCMPDS
for s1, s2 being State of SCMPDS st p c= s1 &amp; p c= s2 &amp; q c= P1 &amp; q c= P2 holds
for i, m being Element of NAT
for a being Int_position
for k1, k2 being Integer st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) >=0_goto k2 &amp; m = IC (Comput (P1,s1,i)) &amp; m + k2 >= 0 &amp; k2 <> 1 holds
( (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) < 0 iff (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) < 0 )
proofend;