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

begin

theorem :: SCMPDS_3:1

canceled;

theorem Th2: :: SCMPDS_3:2

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 Th3: :: SCMPDS_3:3

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 Th4: :: SCMPDS_3:4

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

canceled;

theorem :: SCMPDS_3:6

not IC in SCM-Data-Loc

proof end;

theorem :: SCMPDS_3:7

for s1, s2 being State of SCMPDS st s1 | (SCM-Data-Loc \/ {(IC )}) = s2 | (SCM-Data-Loc \/ {(IC )}) holds
for l being Instruction of SCMPDS holds (Exec (l,s1)) | (SCM-Data-Loc \/ {(IC )}) = (Exec (l,s2)) | (SCM-Data-Loc \/ {(IC )})

proof end;

begin

theorem :: SCMPDS_3:8

canceled;

theorem :: SCMPDS_3:9

canceled;

theorem :: SCMPDS_3:10

canceled;

theorem :: SCMPDS_3:11

canceled;

theorem :: SCMPDS_3:12

canceled;

theorem :: SCMPDS_3:13

canceled;

theorem :: SCMPDS_3:14

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

proof end;

theorem :: SCMPDS_3:15

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 func la .--> a -> FinPartState of SCMPDS;
coherence
la .--> a is FinPartState of SCMPDS

proof end;

end;

registration

cluster SCMPDS -> IC-recognized ;
coherence
SCMPDS is IC-recognized

proof end;

end;

theorem :: SCMPDS_3:16

canceled;

theorem :: SCMPDS_3:17

canceled;

theorem Th18: :: SCMPDS_3:18

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

for s1, s2 being State of SCMPDS
for k1, k2 being Element of NAT st IC s1 = IC s2 & k1 <> k2 holds
ICplusConst (s1,k1) <> ICplusConst (s2,k2)

proof end;

theorem Th20: :: SCMPDS_3:20

for s being State of SCMPDS holds succ (IC s) = ICplusConst (s,1)

proof end;

registration

cluster SCMPDS -> CurIns-recognized ;
coherence
SCMPDS is CurIns-recognized

proof end;

end;

theorem :: SCMPDS_3:21

canceled;

theorem :: SCMPDS_3:22

for p being non NAT -defined autonomic FinPartState of
for s being State of SCMPDS st NPP p c= s holds
for P being the Instructions of SCMPDS -valued ManySortedSet of NAT st ProgramPart p c= P holds
for i being Element of NAT holds IC (Comput (P,s,i)) in dom (ProgramPart p) by AMISTD_5:def 4;

theorem :: SCMPDS_3:23

canceled;

Lm1: for a being Int_position
for p being PartState of SCMPDS st a in dom p holds
a in dom (NPP p)

proof end;

theorem :: SCMPDS_3:24

for P1, P2 being the Instructions of SCMPDS -valued ManySortedSet of NAT
for p being non NAT -defined autonomic FinPartState of
for s1, s2 being State of SCMPDS st NPP p c= s1 & NPP p c= s2 & ProgramPart p c= P1 & ProgramPart p 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) & 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:25

for P1, P2 being the Instructions of SCMPDS -valued ManySortedSet of NAT
for p being non NAT -defined autonomic FinPartState of
for s1, s2 being State of SCMPDS st NPP p c= s1 & NPP p c= s2 & ProgramPart p c= P1 & ProgramPart p 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) & 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:26

for P1, P2 being the Instructions of SCMPDS -valued ManySortedSet of NAT
for p being non NAT -defined autonomic FinPartState of
for s1, s2 being State of SCMPDS st NPP p c= s1 & NPP p c= s2 & ProgramPart p c= P1 & ProgramPart p 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) & 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:27

for P1, P2 being the Instructions of SCMPDS -valued ManySortedSet of NAT
for p being non NAT -defined autonomic FinPartState of
for s1, s2 being State of SCMPDS st NPP p c= s1 & NPP p c= s2 & ProgramPart p c= P1 & ProgramPart p 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) & 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:28

for P1, P2 being the Instructions of SCMPDS -valued ManySortedSet of NAT
for p being non NAT -defined autonomic FinPartState of
for s1, s2 being State of SCMPDS st NPP p c= s1 & NPP p c= s2 & ProgramPart p c= P1 & ProgramPart p 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 & 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:29

for P1, P2 being the Instructions of SCMPDS -valued ManySortedSet of NAT
for p being non NAT -defined autonomic FinPartState of
for s1, s2 being State of SCMPDS st NPP p c= s1 & NPP p c= s2 & ProgramPart p c= P1 & ProgramPart p 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 & 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:30

for P1, P2 being the Instructions of SCMPDS -valued ManySortedSet of NAT
for p being non NAT -defined autonomic FinPartState of
for s1, s2 being State of SCMPDS st NPP p c= s1 & NPP p c= s2 & ProgramPart p c= P1 & ProgramPart p 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 & 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;