:: Computation and Program Shift in the SCMPDS Computer
:: by JingChao Chen
::
:: Copyright (c) 1999-2021 Association of Mizar Users

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

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

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

theorem :: SCMPDS_3:4
proof end;

theorem :: SCMPDS_3:5
canceled;

::\$CT
theorem :: SCMPDS_3:6
for s being State of SCMPDS
for iloc being Nat
for a being Int_position holds s . a = (s +* (Start-At (iloc,SCMPDS))) . a
proof end;

theorem :: SCMPDS_3:7
for s, t being State of SCMPDS holds s +* () is State of SCMPDS ;

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

registration
coherence
proof end;
end;

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

theorem :: SCMPDS_3:9
for s1, s2 being State of SCMPDS
for k1, k2 being Nat st IC s1 = IC s2 & k1 <> k2 holds
ICplusConst (s1,k1) <> ICplusConst (s2,k2)
proof end;

theorem Th9: :: SCMPDS_3:10
for s being State of SCMPDS holds (IC s) + 1 = ICplusConst (s,1)
proof end;

registration
coherence
proof end;
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 & p c= s2 & q c= P1 & q c= P2 holds
for i being Nat
for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) := (b,k2) & a in dom p & 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))
proof end;

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 & p c= s2 & q c= P1 & q c= P2 holds
for i being Nat
for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = AddTo (a,k1,b,k2) & a in dom p & 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))
proof end;

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 & p c= s2 & q c= P1 & q c= P2 holds
for i being Nat
for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = SubFrom (a,k1,b,k2) & a in dom p & 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))
proof end;

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 & p c= s2 & q c= P1 & q c= P2 holds
for i being Nat
for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = MultBy (a,k1,b,k2) & a in dom p & 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)))
proof end;

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 & p c= s2 & q c= P1 & q c= P2 holds
for i, m being Nat
for a being Int_position
for k1, k2 being Integer st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) <>0_goto k2 & m = IC (Comput (P1,s1,i)) & m + k2 >= 0 & 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 )
proof end;

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 & p c= s2 & q c= P1 & q c= P2 holds
for i, m being Nat
for a being Int_position
for k1, k2 being Integer st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) <=0_goto k2 & m = IC (Comput (P1,s1,i)) & m + k2 >= 0 & 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 )
proof end;

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 & p c= s2 & q c= P1 & q c= P2 holds
for i, m being Nat
for a being Int_position
for k1, k2 being Integer st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) >=0_goto k2 & m = IC (Comput (P1,s1,i)) & m + k2 >= 0 & 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 )
proof end;