:: Computation and Program Shift in the SCMPDS Computer
:: by JingChao Chen
::
:: Received June 15, 1999
:: Copyright (c) 1999 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

the carrier of SCMPDS = ({(IC SCMPDS )} \/ SCM-Data-Loc ) \/ NAT by AMI_3:4;

theorem :: SCMPDS_3:6

not IC SCMPDS in SCM-Data-Loc

proof end;

theorem Th7: :: SCMPDS_3:7

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

proof end;

theorem :: SCMPDS_3:8

for i being Instruction of SCMPDS
for s being State of SCMPDS holds (Exec i,s) | NAT = s | NAT

proof end;

begin

theorem :: SCMPDS_3:9

canceled;

theorem :: SCMPDS_3:10

canceled;

theorem :: SCMPDS_3:11

canceled;

theorem :: SCMPDS_3:12

canceled;

theorem :: SCMPDS_3:13

for i being Instruction of SCMPDS
for s being State of SCMPDS
for p being preProgram of SCMPDS holds Exec i,(s +* p) = (Exec i,s) +* p

proof end;

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;

theorem Th16: :: SCMPDS_3:16

for p being autonomic FinPartState of SCMPDS st DataPart p <> {} holds
IC SCMPDS in dom p

proof end;

registration

cluster Relation-like non NAT -defined the carrier of SCMPDS -defined Function-like the Object-Kind of SCMPDS -compatible V32() V62() autonomic set ;
existence
ex b₁ being FinPartState of SCMPDS st
( b₁ is autonomic & not b₁ is NAT -defined )

proof end;

end;

theorem Th17: :: SCMPDS_3:17

for p being non NAT -defined autonomic FinPartState of holds IC SCMPDS in dom p

proof end;

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 Th19: :: 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;

theorem :: SCMPDS_3:21

for p being autonomic FinPartState of SCMPDS st IC SCMPDS in dom p holds
IC p in dom p

proof end;

theorem Th22: :: SCMPDS_3:22

for p being non NAT -defined autonomic FinPartState of
for s being State of SCMPDS st p c= s holds
for i being Element of NAT holds IC (Comput (ProgramPart s),s,i) in dom (ProgramPart p)

proof end;

theorem Th23: :: SCMPDS_3:23

for p being non NAT -defined autonomic FinPartState of
for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 holds
for i being Element of NAT holds
( IC (Comput (ProgramPart s1),s1,i) = IC (Comput (ProgramPart s2),s2,i) & CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i) = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),(Comput (ProgramPart s2),s2,i) )

proof end;

theorem :: SCMPDS_3:24

for p being non NAT -defined autonomic FinPartState of
for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 holds
for i being Element of NAT
for k1, k2 being Integer
for a, b being Int_position st CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i) = a,k1 := b,k2 & a in dom p & DataLoc ((Comput (ProgramPart s1),s1,i) . a),k1 in dom p holds
(Comput (ProgramPart s1),s1,i) . (DataLoc ((Comput (ProgramPart s1),s1,i) . b),k2) = (Comput (ProgramPart s2),s2,i) . (DataLoc ((Comput (ProgramPart s2),s2,i) . b),k2)

proof end;

theorem :: SCMPDS_3:25

for p being non NAT -defined autonomic FinPartState of
for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 holds
for i being Element of NAT
for k1, k2 being Integer
for a, b being Int_position st CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i) = AddTo a,k1,b,k2 & a in dom p & DataLoc ((Comput (ProgramPart s1),s1,i) . a),k1 in dom p holds
(Comput (ProgramPart s1),s1,i) . (DataLoc ((Comput (ProgramPart s1),s1,i) . b),k2) = (Comput (ProgramPart s2),s2,i) . (DataLoc ((Comput (ProgramPart s2),s2,i) . b),k2)

proof end;

theorem :: SCMPDS_3:26

for p being non NAT -defined autonomic FinPartState of
for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 holds
for i being Element of NAT
for k1, k2 being Integer
for a, b being Int_position st CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i) = SubFrom a,k1,b,k2 & a in dom p & DataLoc ((Comput (ProgramPart s1),s1,i) . a),k1 in dom p holds
(Comput (ProgramPart s1),s1,i) . (DataLoc ((Comput (ProgramPart s1),s1,i) . b),k2) = (Comput (ProgramPart s2),s2,i) . (DataLoc ((Comput (ProgramPart s2),s2,i) . b),k2)

proof end;

theorem :: SCMPDS_3:27

for p being non NAT -defined autonomic FinPartState of
for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 holds
for i being Element of NAT
for k1, k2 being Integer
for a, b being Int_position st CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i) = MultBy a,k1,b,k2 & a in dom p & DataLoc ((Comput (ProgramPart s1),s1,i) . a),k1 in dom p holds
((Comput (ProgramPart s1),s1,i) . (DataLoc ((Comput (ProgramPart s1),s1,i) . a),k1)) * ((Comput (ProgramPart s1),s1,i) . (DataLoc ((Comput (ProgramPart s1),s1,i) . b),k2)) = ((Comput (ProgramPart s2),s2,i) . (DataLoc ((Comput (ProgramPart s2),s2,i) . a),k1)) * ((Comput (ProgramPart s2),s2,i) . (DataLoc ((Comput (ProgramPart s2),s2,i) . b),k2))

proof end;

theorem :: SCMPDS_3:28

for p being non NAT -defined autonomic FinPartState of
for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 holds
for i, m being Element of NAT
for a being Int_position
for k1, k2 being Integer st CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i) = a,k1 <>0_goto k2 & m = IC (Comput (ProgramPart s1),s1,i) & m + k2 >= 0 & k2 <> 1 holds
( (Comput (ProgramPart s1),s1,i) . (DataLoc ((Comput (ProgramPart s1),s1,i) . a),k1) = 0 iff (Comput (ProgramPart s2),s2,i) . (DataLoc ((Comput (ProgramPart s2),s2,i) . a),k1) = 0 )

proof end;

theorem :: SCMPDS_3:29

for p being non NAT -defined autonomic FinPartState of
for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 holds
for i, m being Element of NAT
for a being Int_position
for k1, k2 being Integer st CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i) = a,k1 <=0_goto k2 & m = IC (Comput (ProgramPart s1),s1,i) & m + k2 >= 0 & k2 <> 1 holds
( (Comput (ProgramPart s1),s1,i) . (DataLoc ((Comput (ProgramPart s1),s1,i) . a),k1) > 0 iff (Comput (ProgramPart s2),s2,i) . (DataLoc ((Comput (ProgramPart s2),s2,i) . a),k1) > 0 )

proof end;

theorem :: SCMPDS_3:30

for p being non NAT -defined autonomic FinPartState of
for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 holds
for i, m being Element of NAT
for a being Int_position
for k1, k2 being Integer st CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i) = a,k1 >=0_goto k2 & m = IC (Comput (ProgramPart s1),s1,i) & m + k2 >= 0 & k2 <> 1 holds
( (Comput (ProgramPart s1),s1,i) . (DataLoc ((Comput (ProgramPart s1),s1,i) . a),k1) < 0 iff (Comput (ProgramPart s2),s2,i) . (DataLoc ((Comput (ProgramPart s2),s2,i) . a),k1) < 0 )

proof end;