:: by JingChao Chen

::

:: Received June 15, 1999

:: Copyright (c) 1999-2018 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)

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))

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

for s1, s2 being State of SCMPDS st DataPart s1 = DataPart s2 holds

s1 . a = s2 . a

proof end;

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

for iloc being Nat

for a being Int_position holds s . a = (s +* (Start-At (iloc,SCMPDS))) . a

proof end;

theorem :: SCMPDS_3:7

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

end;
let a be Integer;

:: original: .-->

redefine func la .--> a -> FinPartState of SCMPDS;

coherence

la .--> a is FinPartState of SCMPDS

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

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)

for k1, k2 being Nat st IC s1 = IC s2 & k1 <> k2 holds

ICplusConst (s1,k1) <> ICplusConst (s2,k2)

proof end;

registration
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 b_{3} -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))

for q being NAT -defined the InstructionsF of SCMPDS -valued finite non halt-free Function

for p being non empty b

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 b_{3} -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))

for q being NAT -defined the InstructionsF of SCMPDS -valued finite non halt-free Function

for p being non empty b

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 b_{3} -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))

for q being NAT -defined the InstructionsF of SCMPDS -valued finite non halt-free Function

for p being non empty b

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 b_{3} -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)))

for q being NAT -defined the InstructionsF of SCMPDS -valued finite non halt-free Function

for p being non empty b

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 b_{3} -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 )

for q being NAT -defined the InstructionsF of SCMPDS -valued finite non halt-free Function

for p being non empty b

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 b_{3} -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 )

for q being NAT -defined the InstructionsF of SCMPDS -valued finite non halt-free Function

for p being non empty b

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 b_{3} -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 )

for q being NAT -defined the InstructionsF of SCMPDS -valued finite non halt-free Function

for p being non empty b

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;