:: 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 Instruction-Location of SCMPDS
for a being Int_position holds s . a = (s +* (Start-At iloc)) . a

proof end;

theorem :: SCMPDS_3:15

for s, t being State of SCMPDS holds s +* (t | SCM-Data-Loc ) is State of SCMPDS

proof end;

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 non NAT -defined autonomic Element of sproduct the Object-Kind of SCMPDS ;
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 SCMPDS 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 Next (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 SCMPDS
for s being State of SCMPDS st p c= s holds
for i being Element of NAT holds IC (Computation s,i) in dom (ProgramPart p)

proof end;

theorem Th23: :: SCMPDS_3:23

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

proof end;

theorem :: SCMPDS_3:24

for p being non NAT -defined autonomic FinPartState of SCMPDS
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 (Computation s1,i) = a,k1 := b,k2 & a in dom p & DataLoc ((Computation s1,i) . a),k1 in dom p holds
(Computation s1,i) . (DataLoc ((Computation s1,i) . b),k2) = (Computation s2,i) . (DataLoc ((Computation s2,i) . b),k2)

proof end;

theorem :: SCMPDS_3:25

for p being non NAT -defined autonomic FinPartState of SCMPDS
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 (Computation s1,i) = AddTo a,k1,b,k2 & a in dom p & DataLoc ((Computation s1,i) . a),k1 in dom p holds
(Computation s1,i) . (DataLoc ((Computation s1,i) . b),k2) = (Computation s2,i) . (DataLoc ((Computation s2,i) . b),k2)

proof end;

theorem :: SCMPDS_3:26

for p being non NAT -defined autonomic FinPartState of SCMPDS
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 (Computation s1,i) = SubFrom a,k1,b,k2 & a in dom p & DataLoc ((Computation s1,i) . a),k1 in dom p holds
(Computation s1,i) . (DataLoc ((Computation s1,i) . b),k2) = (Computation s2,i) . (DataLoc ((Computation s2,i) . b),k2)

proof end;

theorem :: SCMPDS_3:27

for p being non NAT -defined autonomic FinPartState of SCMPDS
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 (Computation s1,i) = MultBy a,k1,b,k2 & a in dom p & DataLoc ((Computation s1,i) . a),k1 in dom p holds
((Computation s1,i) . (DataLoc ((Computation s1,i) . a),k1)) * ((Computation s1,i) . (DataLoc ((Computation s1,i) . b),k2)) = ((Computation s2,i) . (DataLoc ((Computation s2,i) . a),k1)) * ((Computation s2,i) . (DataLoc ((Computation s2,i) . b),k2))

proof end;

theorem :: SCMPDS_3:28

for p being non NAT -defined autonomic FinPartState of SCMPDS
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 (Computation s1,i) = a,k1 <>0_goto k2 & m = IC (Computation s1,i) & m + k2 >= 0 & k2 <> 1 holds
( (Computation s1,i) . (DataLoc ((Computation s1,i) . a),k1) = 0 iff (Computation s2,i) . (DataLoc ((Computation s2,i) . a),k1) = 0 )

proof end;

theorem :: SCMPDS_3:29

for p being non NAT -defined autonomic FinPartState of SCMPDS
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 (Computation s1,i) = a,k1 <=0_goto k2 & m = IC (Computation s1,i) & m + k2 >= 0 & k2 <> 1 holds
( (Computation s1,i) . (DataLoc ((Computation s1,i) . a),k1) > 0 iff (Computation s2,i) . (DataLoc ((Computation s2,i) . a),k1) > 0 )

proof end;

theorem :: SCMPDS_3:30

for p being non NAT -defined autonomic FinPartState of SCMPDS
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 (Computation s1,i) = a,k1 >=0_goto k2 & m = IC (Computation s1,i) & m + k2 >= 0 & k2 <> 1 holds
( (Computation s1,i) . (DataLoc ((Computation s1,i) . a),k1) < 0 iff (Computation s2,i) . (DataLoc ((Computation s2,i) . a),k1) < 0 )

proof end;

begin

definition

let k be Element of NAT ;
canceled;
func inspos k -> Instruction-Location of SCMPDS equals :: SCMPDS_3:def 2
k;
coherence
k is Instruction-Location of SCMPDS by AMI_1:def 4;

end;

:: deftheorem SCMPDS_3:def 1 :

canceled;

:: deftheorem defines inspos SCMPDS_3:def 2 :

for k being Element of NAT holds inspos k = k;