:: SCMPDS_3 semantic presentation

theorem Th1: :: SCMPDS_3:1

for n being natural number holds
( not n <= 13 or n = 0 or n = 1 or n = 2 or n = 3 or n = 4 or n = 5 or n = 6 or n = 7 or n = 8 or n = 9 or n = 10 or n = 11 or n = 12 or n = 13 )

proof end;

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 s1 | SCM-Data-Loc = s2 | SCM-Data-Loc 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 s1 | SCM-Data-Loc = s2 | SCM-Data-Loc holds
s1 . a = s2 . a

proof end;

theorem Th5: :: SCMPDS_3:5

the carrier of SCMPDS = ({(IC SCMPDS )} \/ SCM-Data-Loc ) \/ the Instruction-Locations of SCMPDS by SCMPDS_2:5, SCMPDS_2:def 1;

theorem Th6: :: 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) | SCM-Instr-Loc = s | SCM-Instr-Loc

proof end;

theorem Th9: :: SCMPDS_3:9

for p being FinPartState of SCMPDS holds DataPart p = p | SCM-Data-Loc

proof end;

theorem :: SCMPDS_3:10

for p being FinPartState of SCMPDS holds
( p is data-only iff dom p c= SCM-Data-Loc )

proof end;

theorem :: SCMPDS_3:11

for p being FinPartState of SCMPDS holds dom (DataPart p) c= SCM-Data-Loc

proof end;

theorem :: SCMPDS_3:12

for p being FinPartState of SCMPDS holds dom (ProgramPart p) c= the Instruction-Locations of SCMPDS by RELAT_1:87;

theorem :: SCMPDS_3:13

for i being Instruction of SCMPDS
for s being State of SCMPDS
for p being programmed FinPartState 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;

definition

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

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 autonomic non programmed FinPartState of SCMPDS ;
existence

proof end;

end;

theorem Th17: :: SCMPDS_3:17

for p being autonomic non programmed 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 - 2) + (2 * k1) >= 0 & (m - 2) + (2 * 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 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 autonomic non programmed FinPartState of SCMPDS
for s being State of SCMPDS st p c= s holds
for i being Nat holds IC ((Computation s) . i) in dom (ProgramPart p)

proof end;

theorem Th23: :: SCMPDS_3:23

for p being autonomic non programmed FinPartState of SCMPDS
for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 holds
for i being 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 autonomic non programmed FinPartState of SCMPDS
for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 holds
for i being 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 autonomic non programmed FinPartState of SCMPDS
for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 holds
for i being 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 autonomic non programmed FinPartState of SCMPDS
for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 holds
for i being 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 autonomic non programmed FinPartState of SCMPDS
for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 holds
for i being 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 autonomic non programmed FinPartState of SCMPDS
for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 holds
for i, m being 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 - 2) + (2 * 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 autonomic non programmed FinPartState of SCMPDS
for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 holds
for i, m being 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 - 2) + (2 * 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 autonomic non programmed FinPartState of SCMPDS
for s1, s2 being State of SCMPDS st p c= s1 & p c= s2 holds
for i, m being 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 - 2) + (2 * 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;

definition

let k be Nat;
canceled;
func inspos k -> Instruction-Location of SCMPDS equals :: SCMPDS_3:def 2
il. k;
coherence by AMI_3:def 1, SCMPDS_2:def 1;

end;

:: deftheorem SCMPDS_3:def 1 :

:: deftheorem defines inspos SCMPDS_3:def 2 :

theorem Th31: :: SCMPDS_3:31

for k1, k2 being Nat st k1 <> k2 holds
inspos k1 <> inspos k2 by AMI_3:53;

theorem Th32: :: SCMPDS_3:32

for il being Instruction-Location of SCMPDS ex i being Nat st il = inspos i

proof end;

definition

let loc be Instruction-Location of SCMPDS ;
let k be Nat;
func loc + k -> Instruction-Location of SCMPDS means :Def3: :: SCMPDS_3:def 3
ex m being Nat st
( loc = inspos m & it = inspos (m + k) );
existence

proof end;

uniqueness by Th31;
func loc -' k -> Instruction-Location of SCMPDS means :Def4: :: SCMPDS_3:def 4
ex m being Nat st
( loc = inspos m & it = inspos (m -' k) );
existence

proof end;

uniqueness by Th31;

end;

:: deftheorem Def3 defines + SCMPDS_3:def 3 :

:: deftheorem Def4 defines -' SCMPDS_3:def 4 :

theorem :: SCMPDS_3:33

for l being Instruction-Location of SCMPDS
for m, n being Nat holds (l + m) + n = l + (m + n)

proof end;

theorem Th34: :: SCMPDS_3:34

for loc being Instruction-Location of SCMPDS
for k being Nat holds (loc + k) -' k = loc

proof end;

theorem :: SCMPDS_3:35

for l1, l2 being Instruction-Location of SCMPDS
for k being Nat holds
( Start-At (l1 + k) = Start-At (l2 + k) iff Start-At l1 = Start-At l2 )

proof end;

theorem :: SCMPDS_3:36

for l1, l2 being Instruction-Location of SCMPDS
for k being Nat st Start-At l1 = Start-At l2 holds
Start-At (l1 -' k) = Start-At (l2 -' k)

proof end;

definition

let IT be FinPartState of SCMPDS ;
attr IT is initial means :: SCMPDS_3:def 5
for m, n being Nat st inspos n in dom IT & m < n holds
inspos m in dom IT;

end;

:: deftheorem defines initial SCMPDS_3:def 5 :

definition

func SCMPDS-Stop -> FinPartState of SCMPDS equals :: SCMPDS_3:def 6
(inspos 0) .--> (halt SCMPDS );
correctness ;

end;

:: deftheorem defines SCMPDS-Stop SCMPDS_3:def 6 :

registration

cluster SCMPDS-Stop -> non empty programmed initial ;
coherence

proof end;

end;

registration

cluster non empty programmed initial FinPartState of SCMPDS ;
existence

proof end;

end;

definition

let p be programmed FinPartState of SCMPDS ;
let k be Nat;
func Shift p,k -> programmed FinPartState of SCMPDS means :Def7: :: SCMPDS_3:def 7
( dom it = { (inspos (m + k)) where m is Nat : inspos m in dom p } & ( for m being Nat st inspos m in dom p holds
it . (inspos (m + k)) = p . (inspos m) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines Shift SCMPDS_3:def 7 :

theorem :: SCMPDS_3:37

for l being Instruction-Location of SCMPDS
for k being Nat
for p being programmed FinPartState of SCMPDS st l in dom p holds
(Shift p,k) . (l + k) = p . l

proof end;

theorem :: SCMPDS_3:38

for p being programmed FinPartState of SCMPDS
for k being Nat holds dom (Shift p,k) = { (il + k) where il is Instruction-Location of SCMPDS : il in dom p }

proof end;

theorem :: SCMPDS_3:39

for m, n being Nat
for I being programmed FinPartState of SCMPDS holds Shift (Shift I,m),n = Shift I,(m + n)

proof end;

theorem :: SCMPDS_3:40

for s being programmed FinPartState of SCMPDS
for f being Function of the Instructions of SCMPDS ,the Instructions of SCMPDS
for n being Nat holds Shift (f * s),n = f * (Shift s,n)

proof end;

theorem :: SCMPDS_3:41

for n being Nat
for I, J being programmed FinPartState of SCMPDS holds Shift (I +* J),n = (Shift I,n) +* (Shift J,n)

proof end;