:: The SCMPDS Computer and the Basic Semantics of Its Instructions
:: by JingChao Chen
::
:: Received June 15, 1999
:: Copyright (c) 1999-2011 Association of Mizar Users

begin

definition

func SCMPDS -> strict AMI-Struct of {INT} equals :: SCMPDS_2:def 1
AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),SCMPDS-Instr,(In ([0,{},<*0*>],SCMPDS-Instr)),SCMPDS-OK,SCMPDS-Exec #);
correctness
coherence
AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),SCMPDS-Instr,(In ([0,{},<*0*>],SCMPDS-Instr)),SCMPDS-OK,SCMPDS-Exec #) is strict AMI-Struct of {INT};
;

end;

:: deftheorem defines SCMPDS SCMPDS_2:def 1 :
SCMPDS = AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),SCMPDS-Instr,(In ([0,{},<*0*>],SCMPDS-Instr)),SCMPDS-OK,SCMPDS-Exec #);

registration

cluster rng SCMPDS-Instr -> FinSequence-membered ;
coherence
proj2 SCMPDS-Instr is FinSequence-membered

proof end;

end;

Lm1: NAT c= SCM-Memory
by XBOOLE_1:7;

registration

cluster SCMPDS -> non empty stored-program standard-ins strict ;
coherence
( not SCMPDS is empty & SCMPDS is stored-program & SCMPDS is standard-ins )

proof end;

end;

registration

cluster Relation-like NAT -defined Function-like -> the carrier of SCMPDS -defined set ;
coherence
for b₁ being Function st b₁ is NAT -defined holds
b₁ is the carrier of SCMPDS -defined

proof end;

end;

theorem :: SCMPDS_2:1

canceled;

theorem :: SCMPDS_2:2

canceled;

theorem Th3: :: SCMPDS_2:3

SCMPDS is definite

proof end;

registration

cluster SCMPDS -> IC-Ins-separated definite strict ;
coherence
( SCMPDS is IC-Ins-separated & SCMPDS is definite )

proof end;

end;

theorem :: SCMPDS_2:4

( the Instructions of SCMPDS <> INT & NAT <> the Instructions of SCMPDS ) by SCMPDS_1:17;

theorem :: SCMPDS_2:5

canceled;

theorem Th6: :: SCMPDS_2:6

IC = NAT by AMI_2:30, FUNCT_7:def 1;

begin

definition

mode Int_position -> Object of SCMPDS means :Def2: :: SCMPDS_2:def 2
it in SCM-Data-Loc ;
existence
ex b₁ being Object of SCMPDS st b₁ in SCM-Data-Loc

proof end;

end;

:: deftheorem Def2 defines Int_position SCMPDS_2:def 2 :
for b₁ being Object of SCMPDS holds
( b₁ is Int_position iff b₁ in SCM-Data-Loc );

theorem :: SCMPDS_2:7

canceled;

theorem :: SCMPDS_2:8

canceled;

theorem :: SCMPDS_2:9

for x being set st x in SCM-Data-Loc holds
x is Int_position by Def2;

theorem :: SCMPDS_2:10

canceled;

theorem :: SCMPDS_2:11

not NAT is finite ;

theorem :: SCMPDS_2:12

for I being Int_position holds I is Data-Location

proof end;

theorem Th13: :: SCMPDS_2:13

for l being Int_position holds ObjectKind l = INT

proof end;

begin

set S1 = { [0,{},<*k1*>] where k1 is Element of INT : verum } ;

set S2 = { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } ;

set S3 = { [I1,{},<*d2,k2*>] where I1 is Element of Segm 14, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I1 in {2,3} } ;

set S4 = { [I2,{},<*d3,k3,k4*>] where I2 is Element of Segm 14, d3 is Element of SCM-Data-Loc , k3, k4 is Element of INT : I2 in {4,5,6,7,8} } ;

set S5 = { [I3,{},<*d4,d5,k5,k6*>] where I3 is Element of Segm 14, d4, d5 is Element of SCM-Data-Loc , k5, k6 is Element of INT : I3 in {9,10,11,12,13} } ;

Lm2: for I being Instruction of SCMPDS holds
( I in { [0,{},<*k1*>] where k1 is Element of INT : verum } or I in { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } or I in { [I1,{},<*d2,k2*>] where I1 is Element of Segm 14, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I1 in {2,3} } or I in { [I2,{},<*d3,k3,k4*>] where I2 is Element of Segm 14, d3 is Element of SCM-Data-Loc , k3, k4 is Element of INT : I2 in {4,5,6,7,8} } or I in { [I3,{},<*d4,d5,k5,k6*>] where I3 is Element of Segm 14, d4, d5 is Element of SCM-Data-Loc , k5, k6 is Element of INT : I3 in {9,10,11,12,13} } )

proof end;

theorem :: SCMPDS_2:14

canceled;

theorem :: SCMPDS_2:15

for I being Instruction of SCMPDS holds InsCode I <= 13

proof end;

definition

let s be State of SCMPDS;
let d be Int_position ;
:: original: .
redefine func s . d -> Integer;
coherence
s . d is Integer

proof end;

end;

definition

let m, n be Integer;
canceled;
func DataLoc (m,n) -> Int_position equals :: SCMPDS_2:def 4
[1,(abs (m + n))];
coherence
[1,(abs (m + n))] is Int_position

proof end;

end;

:: deftheorem SCMPDS_2:def 3 :
canceled;

:: deftheorem defines DataLoc SCMPDS_2:def 4 :
for m, n being Integer holds DataLoc (m,n) = [1,(abs (m + n))];

theorem Th16: :: SCMPDS_2:16

for k1 being Integer holds [0,{},<*k1*>] in SCMPDS-Instr

proof end;

theorem Th17: :: SCMPDS_2:17

for d1 being Element of SCM-Data-Loc holds [1,{},<*d1*>] in SCMPDS-Instr

proof end;

theorem Th18: :: SCMPDS_2:18

for x being set
for d2 being Element of SCM-Data-Loc
for k2 being Integer st x in {2,3} holds
[x,{},<*d2,k2*>] in SCMPDS-Instr

proof end;

theorem Th19: :: SCMPDS_2:19

for x being set
for d2 being Element of SCM-Data-Loc
for k3, k4 being Integer st x in {4,5,6,7,8} holds
[x,{},<*d2,k3,k4*>] in SCMPDS-Instr

proof end;

theorem Th20: :: SCMPDS_2:20

for x being set
for d4, d5 being Element of SCM-Data-Loc
for k5, k6 being Integer st x in {9,10,11,12,13} holds
[x,{},<*d4,d5,k5,k6*>] in SCMPDS-Instr

proof end;

definition

let k1 be Integer;
func goto k1 -> Instruction of SCMPDS equals :: SCMPDS_2:def 5
[0,{},<*k1*>];
correctness
coherence
[0,{},<*k1*>] is Instruction of SCMPDS;
by Th16;

end;

:: deftheorem defines goto SCMPDS_2:def 5 :
for k1 being Integer holds goto k1 = [0,{},<*k1*>];

definition

let a be Int_position ;
func return a -> Instruction of SCMPDS equals :: SCMPDS_2:def 6
[1,{},<*a*>];
correctness
coherence
[1,{},<*a*>] is Instruction of SCMPDS;

proof end;

end;

:: deftheorem defines return SCMPDS_2:def 6 :
for a being Int_position holds return a = [1,{},<*a*>];

definition

let a be Int_position ;
let k1 be Integer;
func a := k1 -> Instruction of SCMPDS equals :: SCMPDS_2:def 7
[2,{},<*a,k1*>];
correctness
coherence
[2,{},<*a,k1*>] is Instruction of SCMPDS;

proof end;

func saveIC (a,k1) -> Instruction of SCMPDS equals :: SCMPDS_2:def 8
[3,{},<*a,k1*>];
correctness
coherence
[3,{},<*a,k1*>] is Instruction of SCMPDS;

proof end;

end;

:: deftheorem defines := SCMPDS_2:def 7 :
for a being Int_position
for k1 being Integer holds a := k1 = [2,{},<*a,k1*>];

:: deftheorem defines saveIC SCMPDS_2:def 8 :
for a being Int_position
for k1 being Integer holds saveIC (a,k1) = [3,{},<*a,k1*>];

definition

let a be Int_position ;
let k1, k2 be Integer;
func (a,k1) <>0_goto k2 -> Instruction of SCMPDS equals :: SCMPDS_2:def 9
[4,{},<*a,k1,k2*>];
correctness
coherence
[4,{},<*a,k1,k2*>] is Instruction of SCMPDS;

proof end;

func (a,k1) <=0_goto k2 -> Instruction of SCMPDS equals :: SCMPDS_2:def 10
[5,{},<*a,k1,k2*>];
correctness
coherence
[5,{},<*a,k1,k2*>] is Instruction of SCMPDS;

proof end;

func (a,k1) >=0_goto k2 -> Instruction of SCMPDS equals :: SCMPDS_2:def 11
[6,{},<*a,k1,k2*>];
correctness
coherence
[6,{},<*a,k1,k2*>] is Instruction of SCMPDS;

proof end;

func (a,k1) := k2 -> Instruction of SCMPDS equals :: SCMPDS_2:def 12
[7,{},<*a,k1,k2*>];
correctness
coherence
[7,{},<*a,k1,k2*>] is Instruction of SCMPDS;

proof end;

func AddTo (a,k1,k2) -> Instruction of SCMPDS equals :: SCMPDS_2:def 13
[8,{},<*a,k1,k2*>];
correctness
coherence
[8,{},<*a,k1,k2*>] is Instruction of SCMPDS;

proof end;

end;

:: deftheorem defines <>0_goto SCMPDS_2:def 9 :
for a being Int_position
for k1, k2 being Integer holds (a,k1) <>0_goto k2 = [4,{},<*a,k1,k2*>];

:: deftheorem defines <=0_goto SCMPDS_2:def 10 :
for a being Int_position
for k1, k2 being Integer holds (a,k1) <=0_goto k2 = [5,{},<*a,k1,k2*>];

:: deftheorem defines >=0_goto SCMPDS_2:def 11 :
for a being Int_position
for k1, k2 being Integer holds (a,k1) >=0_goto k2 = [6,{},<*a,k1,k2*>];

:: deftheorem defines := SCMPDS_2:def 12 :
for a being Int_position
for k1, k2 being Integer holds (a,k1) := k2 = [7,{},<*a,k1,k2*>];

:: deftheorem defines AddTo SCMPDS_2:def 13 :
for a being Int_position
for k1, k2 being Integer holds AddTo (a,k1,k2) = [8,{},<*a,k1,k2*>];

definition

let a, b be Int_position ;
let k1, k2 be Integer;
func AddTo (a,k1,b,k2) -> Instruction of SCMPDS equals :: SCMPDS_2:def 14
[9,{},<*a,b,k1,k2*>];
correctness
coherence
[9,{},<*a,b,k1,k2*>] is Instruction of SCMPDS;

proof end;

func SubFrom (a,k1,b,k2) -> Instruction of SCMPDS equals :: SCMPDS_2:def 15
[10,{},<*a,b,k1,k2*>];
correctness
coherence
[10,{},<*a,b,k1,k2*>] is Instruction of SCMPDS;

proof end;

func MultBy (a,k1,b,k2) -> Instruction of SCMPDS equals :: SCMPDS_2:def 16
[11,{},<*a,b,k1,k2*>];
correctness
coherence
[11,{},<*a,b,k1,k2*>] is Instruction of SCMPDS;

proof end;

func Divide (a,k1,b,k2) -> Instruction of SCMPDS equals :: SCMPDS_2:def 17
[12,{},<*a,b,k1,k2*>];
correctness
coherence
[12,{},<*a,b,k1,k2*>] is Instruction of SCMPDS;

proof end;

func (a,k1) := (b,k2) -> Instruction of SCMPDS equals :: SCMPDS_2:def 18
[13,{},<*a,b,k1,k2*>];
correctness
coherence
[13,{},<*a,b,k1,k2*>] is Instruction of SCMPDS;

proof end;

end;

:: deftheorem defines AddTo SCMPDS_2:def 14 :
for a, b being Int_position
for k1, k2 being Integer holds AddTo (a,k1,b,k2) = [9,{},<*a,b,k1,k2*>];

:: deftheorem defines SubFrom SCMPDS_2:def 15 :
for a, b being Int_position
for k1, k2 being Integer holds SubFrom (a,k1,b,k2) = [10,{},<*a,b,k1,k2*>];

:: deftheorem defines MultBy SCMPDS_2:def 16 :
for a, b being Int_position
for k1, k2 being Integer holds MultBy (a,k1,b,k2) = [11,{},<*a,b,k1,k2*>];

:: deftheorem defines Divide SCMPDS_2:def 17 :
for a, b being Int_position
for k1, k2 being Integer holds Divide (a,k1,b,k2) = [12,{},<*a,b,k1,k2*>];

:: deftheorem defines := SCMPDS_2:def 18 :
for a, b being Int_position
for k1, k2 being Integer holds (a,k1) := (b,k2) = [13,{},<*a,b,k1,k2*>];

theorem :: SCMPDS_2:21

for k1 being Integer holds InsCode (goto k1) = 0 by RECDEF_2:def 1;

theorem :: SCMPDS_2:22

for a being Int_position holds InsCode (return a) = 1 by RECDEF_2:def 1;

theorem :: SCMPDS_2:23

for k1 being Integer
for a being Int_position holds InsCode (a := k1) = 2 by RECDEF_2:def 1;

theorem :: SCMPDS_2:24

for k1 being Integer
for a being Int_position holds InsCode (saveIC (a,k1)) = 3 by RECDEF_2:def 1;

theorem :: SCMPDS_2:25

for k1, k2 being Integer
for a being Int_position holds InsCode ((a,k1) <>0_goto k2) = 4 by RECDEF_2:def 1;

theorem :: SCMPDS_2:26

for k1, k2 being Integer
for a being Int_position holds InsCode ((a,k1) <=0_goto k2) = 5 by RECDEF_2:def 1;

theorem :: SCMPDS_2:27

for k1, k2 being Integer
for a being Int_position holds InsCode ((a,k1) >=0_goto k2) = 6 by RECDEF_2:def 1;

theorem :: SCMPDS_2:28

for k1, k2 being Integer
for a being Int_position holds InsCode ((a,k1) := k2) = 7 by RECDEF_2:def 1;

theorem :: SCMPDS_2:29

for k1, k2 being Integer
for a being Int_position holds InsCode (AddTo (a,k1,k2)) = 8 by RECDEF_2:def 1;

theorem :: SCMPDS_2:30

for k1, k2 being Integer
for a, b being Int_position holds InsCode (AddTo (a,k1,b,k2)) = 9 by RECDEF_2:def 1;

theorem :: SCMPDS_2:31

for k1, k2 being Integer
for a, b being Int_position holds InsCode (SubFrom (a,k1,b,k2)) = 10 by RECDEF_2:def 1;

theorem :: SCMPDS_2:32

for k1, k2 being Integer
for a, b being Int_position holds InsCode (MultBy (a,k1,b,k2)) = 11 by RECDEF_2:def 1;

theorem :: SCMPDS_2:33

for k1, k2 being Integer
for a, b being Int_position holds InsCode (Divide (a,k1,b,k2)) = 12 by RECDEF_2:def 1;

theorem :: SCMPDS_2:34

for k1, k2 being Integer
for a, b being Int_position holds InsCode ((a,k1) := (b,k2)) = 13 by RECDEF_2:def 1;

Lm3: for I being Instruction of SCMPDS st I in { [0,{},<*k1*>] where k1 is Element of INT : verum } holds
InsCode I = 0

proof end;

Lm4: for I being Instruction of SCMPDS st I in { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } holds
InsCode I = 1

proof end;

Lm5: for I being Instruction of SCMPDS holds
( not I in { [I1,{},<*d1,k1*>] where I1 is Element of Segm 14, d1 is Element of SCM-Data-Loc , k1 is Element of INT : I1 in {2,3} } or InsCode I = 2 or InsCode I = 3 )

proof end;

Lm6: for I being Instruction of SCMPDS holds
( not I in { [I1,{},<*d1,k1,k2*>] where I1 is Element of Segm 14, d1 is Element of SCM-Data-Loc , k1, k2 is Element of INT : I1 in {4,5,6,7,8} } or InsCode I = 4 or InsCode I = 5 or InsCode I = 6 or InsCode I = 7 or InsCode I = 8 )

proof end;

Lm7: for I being Instruction of SCMPDS holds
( not I in { [I1,{},<*d1,d2,k1,k2*>] where I1 is Element of Segm 14, d1, d2 is Element of SCM-Data-Loc , k1, k2 is Element of INT : I1 in {9,10,11,12,13} } or InsCode I = 9 or InsCode I = 10 or InsCode I = 11 or InsCode I = 12 or InsCode I = 13 )

proof end;

theorem :: SCMPDS_2:35

for ins being Instruction of SCMPDS st InsCode ins = 0 holds
ex k1 being Integer st ins = goto k1

proof end;

theorem :: SCMPDS_2:36

for ins being Instruction of SCMPDS st InsCode ins = 1 holds
ex a being Int_position st ins = return a

proof end;

theorem :: SCMPDS_2:37

for ins being Instruction of SCMPDS st InsCode ins = 2 holds
ex a being Int_position ex k1 being Integer st ins = a := k1

proof end;

theorem :: SCMPDS_2:38

for ins being Instruction of SCMPDS st InsCode ins = 3 holds
ex a being Int_position ex k1 being Integer st ins = saveIC (a,k1)

proof end;

Lm8: for I being Instruction of SCMPDS holds
( ( not I in { [0,{},<*k1*>] where k1 is Element of INT : verum } & not I in { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } & not I in { [I1,{},<*d2,k2*>] where I1 is Element of Segm 14, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I1 in {2,3} } & not I in { [I3,{},<*d4,d5,k5,k6*>] where I3 is Element of Segm 14, d4, d5 is Element of SCM-Data-Loc , k5, k6 is Element of INT : I3 in {9,10,11,12,13} } ) or InsCode I = 0 or InsCode I = 1 or InsCode I = 2 or InsCode I = 3 or InsCode I = 9 or InsCode I = 10 or InsCode I = 11 or InsCode I = 12 or InsCode I = 13 )

proof end;

theorem :: SCMPDS_2:39

for ins being Instruction of SCMPDS st InsCode ins = 4 holds
ex a being Int_position ex k1, k2 being Integer st ins = (a,k1) <>0_goto k2

proof end;

theorem :: SCMPDS_2:40

for ins being Instruction of SCMPDS st InsCode ins = 5 holds
ex a being Int_position ex k1, k2 being Integer st ins = (a,k1) <=0_goto k2

proof end;

theorem :: SCMPDS_2:41

for ins being Instruction of SCMPDS st InsCode ins = 6 holds
ex a being Int_position ex k1, k2 being Integer st ins = (a,k1) >=0_goto k2

proof end;

theorem :: SCMPDS_2:42

for ins being Instruction of SCMPDS st InsCode ins = 7 holds
ex a being Int_position ex k1, k2 being Integer st ins = (a,k1) := k2

proof end;

theorem :: SCMPDS_2:43

for ins being Instruction of SCMPDS st InsCode ins = 8 holds
ex a being Int_position ex k1, k2 being Integer st ins = AddTo (a,k1,k2)

proof end;

Lm9: for I being Instruction of SCMPDS holds
( ( not I in { [0,{},<*k1*>] where k1 is Element of INT : verum } & not I in { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } & not I in { [I1,{},<*d2,k2*>] where I1 is Element of Segm 14, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I1 in {2,3} } & not I in { [I2,{},<*d3,k3,k4*>] where I2 is Element of Segm 14, d3 is Element of SCM-Data-Loc , k3, k4 is Element of INT : I2 in {4,5,6,7,8} } ) or InsCode I = 0 or InsCode I = 1 or InsCode I = 2 or InsCode I = 3 or InsCode I = 4 or InsCode I = 5 or InsCode I = 6 or InsCode I = 7 or InsCode I = 8 )

proof end;

theorem :: SCMPDS_2:44

for ins being Instruction of SCMPDS st InsCode ins = 9 holds
ex a, b being Int_position ex k1, k2 being Integer st ins = AddTo (a,k1,b,k2)

proof end;

theorem :: SCMPDS_2:45

for ins being Instruction of SCMPDS st InsCode ins = 10 holds
ex a, b being Int_position ex k1, k2 being Integer st ins = SubFrom (a,k1,b,k2)

proof end;

theorem :: SCMPDS_2:46

for ins being Instruction of SCMPDS st InsCode ins = 11 holds
ex a, b being Int_position ex k1, k2 being Integer st ins = MultBy (a,k1,b,k2)

proof end;

theorem :: SCMPDS_2:47

for ins being Instruction of SCMPDS st InsCode ins = 12 holds
ex a, b being Int_position ex k1, k2 being Integer st ins = Divide (a,k1,b,k2)

proof end;

theorem :: SCMPDS_2:48

for ins being Instruction of SCMPDS st InsCode ins = 13 holds
ex a, b being Int_position ex k1, k2 being Integer st ins = (a,k1) := (b,k2)

proof end;

theorem :: SCMPDS_2:49

for s being State of SCMPDS
for d being Int_position holds d in dom s

proof end;

theorem Th50: :: SCMPDS_2:50

for s being State of SCMPDS holds SCM-Data-Loc c= dom s

proof end;

Lm10: Data-Locations SCMPDS = SCM-Data-Loc

proof end;

theorem :: SCMPDS_2:51

for s being State of SCMPDS holds dom (DataPart s) = SCM-Data-Loc

proof end;

theorem :: SCMPDS_2:52

for dl being Int_position holds dl <> IC

proof end;

theorem :: SCMPDS_2:53

for il being Element of NAT
for dl being Int_position holds il <> dl

proof end;

theorem :: SCMPDS_2:54

for s1, s2 being State of SCMPDS st IC s1 = IC s2 & ( for a being Int_position holds s1 . a = s2 . a ) & ( for i being Element of NAT holds s1 . i = s2 . i ) holds
s1 = s2

proof end;

begin

theorem :: SCMPDS_2:55

canceled;

theorem :: SCMPDS_2:56

canceled;

theorem Th57: :: SCMPDS_2:57

for s being State of SCMPDS
for k1 being Integer
for a being Int_position holds
( (Exec ((a := k1),s)) . (IC ) = succ (IC s) & (Exec ((a := k1),s)) . a = k1 & ( for b being Int_position st b <> a holds
(Exec ((a := k1),s)) . b = s . b ) )

proof end;

theorem Th58: :: SCMPDS_2:58

for s being State of SCMPDS
for k1, k2 being Integer
for a being Int_position holds
( (Exec (((a,k1) := k2),s)) . (IC ) = succ (IC s) & (Exec (((a,k1) := k2),s)) . (DataLoc ((s . a),k1)) = k2 & ( for b being Int_position st b <> DataLoc ((s . a),k1) holds
(Exec (((a,k1) := k2),s)) . b = s . b ) )

proof end;

theorem Th59: :: SCMPDS_2:59

for s being State of SCMPDS
for k1, k2 being Integer
for a, b being Int_position holds
( (Exec (((a,k1) := (b,k2)),s)) . (IC ) = succ (IC s) & (Exec (((a,k1) := (b,k2)),s)) . (DataLoc ((s . a),k1)) = s . (DataLoc ((s . b),k2)) & ( for c being Int_position st c <> DataLoc ((s . a),k1) holds
(Exec (((a,k1) := (b,k2)),s)) . c = s . c ) )

proof end;

theorem Th60: :: SCMPDS_2:60

for s being State of SCMPDS
for k1, k2 being Integer
for a being Int_position holds
( (Exec ((AddTo (a,k1,k2)),s)) . (IC ) = succ (IC s) & (Exec ((AddTo (a,k1,k2)),s)) . (DataLoc ((s . a),k1)) = (s . (DataLoc ((s . a),k1))) + k2 & ( for b being Int_position st b <> DataLoc ((s . a),k1) holds
(Exec ((AddTo (a,k1,k2)),s)) . b = s . b ) )

proof end;

theorem Th61: :: SCMPDS_2:61

for s being State of SCMPDS
for k1, k2 being Integer
for a, b being Int_position holds
( (Exec ((AddTo (a,k1,b,k2)),s)) . (IC ) = succ (IC s) & (Exec ((AddTo (a,k1,b,k2)),s)) . (DataLoc ((s . a),k1)) = (s . (DataLoc ((s . a),k1))) + (s . (DataLoc ((s . b),k2))) & ( for c being Int_position st c <> DataLoc ((s . a),k1) holds
(Exec ((AddTo (a,k1,b,k2)),s)) . c = s . c ) )

proof end;

theorem Th62: :: SCMPDS_2:62

for s being State of SCMPDS
for k1, k2 being Integer
for a, b being Int_position holds
( (Exec ((SubFrom (a,k1,b,k2)),s)) . (IC ) = succ (IC s) & (Exec ((SubFrom (a,k1,b,k2)),s)) . (DataLoc ((s . a),k1)) = (s . (DataLoc ((s . a),k1))) - (s . (DataLoc ((s . b),k2))) & ( for c being Int_position st c <> DataLoc ((s . a),k1) holds
(Exec ((SubFrom (a,k1,b,k2)),s)) . c = s . c ) )

proof end;

theorem Th63: :: SCMPDS_2:63

for s being State of SCMPDS
for k1, k2 being Integer
for a, b being Int_position holds
( (Exec ((MultBy (a,k1,b,k2)),s)) . (IC ) = succ (IC s) & (Exec ((MultBy (a,k1,b,k2)),s)) . (DataLoc ((s . a),k1)) = (s . (DataLoc ((s . a),k1))) * (s . (DataLoc ((s . b),k2))) & ( for c being Int_position st c <> DataLoc ((s . a),k1) holds
(Exec ((MultBy (a,k1,b,k2)),s)) . c = s . c ) )

proof end;

theorem Th64: :: SCMPDS_2:64

for s being State of SCMPDS
for k1, k2 being Integer
for a, b being Int_position holds
( (Exec ((Divide (a,k1,b,k2)),s)) . (IC ) = succ (IC s) & ( DataLoc ((s . a),k1) <> DataLoc ((s . b),k2) implies (Exec ((Divide (a,k1,b,k2)),s)) . (DataLoc ((s . a),k1)) = (s . (DataLoc ((s . a),k1))) div (s . (DataLoc ((s . b),k2))) ) & (Exec ((Divide (a,k1,b,k2)),s)) . (DataLoc ((s . b),k2)) = (s . (DataLoc ((s . a),k1))) mod (s . (DataLoc ((s . b),k2))) & ( for c being Int_position st c <> DataLoc ((s . a),k1) & c <> DataLoc ((s . b),k2) holds
(Exec ((Divide (a,k1,b,k2)),s)) . c = s . c ) )

proof end;

theorem :: SCMPDS_2:65

for s being State of SCMPDS
for k1 being Integer
for a being Int_position holds
( (Exec ((Divide (a,k1,a,k1)),s)) . (IC ) = succ (IC s) & (Exec ((Divide (a,k1,a,k1)),s)) . (DataLoc ((s . a),k1)) = (s . (DataLoc ((s . a),k1))) mod (s . (DataLoc ((s . a),k1))) & ( for c being Int_position st c <> DataLoc ((s . a),k1) holds
(Exec ((Divide (a,k1,a,k1)),s)) . c = s . c ) ) by Th64;

definition

canceled;
let s be State of SCMPDS;
let c be Integer;
func ICplusConst (s,c) -> Element of NAT means :Def20: :: SCMPDS_2:def 20
ex m being Element of NAT st
( m = IC s & it = abs (m + c) );
existence
ex b₁, m being Element of NAT st
( m = IC s & b₁ = abs (m + c) )

proof end;

correctness
uniqueness
for b₁, b₂ being Element of NAT st ex m being Element of NAT st
( m = IC s & b₁ = abs (m + c) ) & ex m being Element of NAT st
( m = IC s & b₂ = abs (m + c) ) holds
b₁ = b₂;
;

end;

:: deftheorem SCMPDS_2:def 19 :
canceled;

:: deftheorem Def20 defines ICplusConst SCMPDS_2:def 20 :
for s being State of SCMPDS
for c being Integer
for b₃ being Element of NAT holds
( b₃ = ICplusConst (s,c) iff ex m being Element of NAT st
( m = IC s & b₃ = abs (m + c) ) );

theorem Th66: :: SCMPDS_2:66

for s being State of SCMPDS
for k1 being Integer holds
( (Exec ((goto k1),s)) . (IC ) = ICplusConst (s,k1) & ( for a being Int_position holds (Exec ((goto k1),s)) . a = s . a ) )

proof end;

theorem Th67: :: SCMPDS_2:67

for s being State of SCMPDS
for k1, k2 being Integer
for a, b being Int_position holds
( ( s . (DataLoc ((s . a),k1)) <> 0 implies (Exec (((a,k1) <>0_goto k2),s)) . (IC ) = ICplusConst (s,k2) ) & ( s . (DataLoc ((s . a),k1)) = 0 implies (Exec (((a,k1) <>0_goto k2),s)) . (IC ) = succ (IC s) ) & (Exec (((a,k1) <>0_goto k2),s)) . b = s . b )

proof end;

theorem Th68: :: SCMPDS_2:68

for s being State of SCMPDS
for k1, k2 being Integer
for a, b being Int_position holds
( ( s . (DataLoc ((s . a),k1)) <= 0 implies (Exec (((a,k1) <=0_goto k2),s)) . (IC ) = ICplusConst (s,k2) ) & ( s . (DataLoc ((s . a),k1)) > 0 implies (Exec (((a,k1) <=0_goto k2),s)) . (IC ) = succ (IC s) ) & (Exec (((a,k1) <=0_goto k2),s)) . b = s . b )

proof end;

theorem Th69: :: SCMPDS_2:69

for s being State of SCMPDS
for k1, k2 being Integer
for a, b being Int_position holds
( ( s . (DataLoc ((s . a),k1)) >= 0 implies (Exec (((a,k1) >=0_goto k2),s)) . (IC ) = ICplusConst (s,k2) ) & ( s . (DataLoc ((s . a),k1)) < 0 implies (Exec (((a,k1) >=0_goto k2),s)) . (IC ) = succ (IC s) ) & (Exec (((a,k1) >=0_goto k2),s)) . b = s . b )

proof end;

theorem Th70: :: SCMPDS_2:70

for s being State of SCMPDS
for a being Int_position holds
( (Exec ((return a),s)) . (IC ) = (abs (s . (DataLoc ((s . a),RetIC)))) + 2 & (Exec ((return a),s)) . a = s . (DataLoc ((s . a),RetSP)) & ( for b being Int_position st a <> b holds
(Exec ((return a),s)) . b = s . b ) )

proof end;

theorem Th71: :: SCMPDS_2:71

for s being State of SCMPDS
for k1 being Integer
for a being Int_position holds
( (Exec ((saveIC (a,k1)),s)) . (IC ) = succ (IC s) & (Exec ((saveIC (a,k1)),s)) . (DataLoc ((s . a),k1)) = IC s & ( for b being Int_position st DataLoc ((s . a),k1) <> b holds
(Exec ((saveIC (a,k1)),s)) . b = s . b ) )

proof end;

theorem Th72: :: SCMPDS_2:72

for k being Integer ex f being Function of SCM-Data-Loc,INT st
for x being Element of SCM-Data-Loc holds f . x = k

proof end;

theorem Th73: :: SCMPDS_2:73

for k being Integer ex s being State of SCMPDS st
for d being Int_position holds s . d = k

proof end;

theorem Th74: :: SCMPDS_2:74

for k being Integer
for loc being Element of NAT ex s being State of SCMPDS st
( s . NAT = loc & ( for d being Int_position holds s . d = k ) )

proof end;

theorem Th75: :: SCMPDS_2:75

goto 0 is halting

proof end;

theorem Th76: :: SCMPDS_2:76

for I being Instruction of SCMPDS st ex s being State of SCMPDS st (Exec (I,s)) . (IC ) = succ (IC s) holds
not I is halting

proof end;

theorem Th77: :: SCMPDS_2:77

for k1 being Integer
for a being Int_position holds not a := k1 is halting

proof end;

theorem Th78: :: SCMPDS_2:78

for k1, k2 being Integer
for a being Int_position holds not (a,k1) := k2 is halting

proof end;

theorem Th79: :: SCMPDS_2:79

for k1, k2 being Integer
for a, b being Int_position holds not (a,k1) := (b,k2) is halting

proof end;

theorem Th80: :: SCMPDS_2:80

for k1, k2 being Integer
for a being Int_position holds not AddTo (a,k1,k2) is halting

proof end;

theorem Th81: :: SCMPDS_2:81

for k1, k2 being Integer
for a, b being Int_position holds not AddTo (a,k1,b,k2) is halting

proof end;

theorem Th82: :: SCMPDS_2:82

for k1, k2 being Integer
for a, b being Int_position holds not SubFrom (a,k1,b,k2) is halting

proof end;

theorem Th83: :: SCMPDS_2:83

for k1, k2 being Integer
for a, b being Int_position holds not MultBy (a,k1,b,k2) is halting

proof end;

theorem Th84: :: SCMPDS_2:84

for k1, k2 being Integer
for a, b being Int_position holds not Divide (a,k1,b,k2) is halting

proof end;

theorem Th85: :: SCMPDS_2:85

for k1 being Integer st k1 <> 0 holds
not goto k1 is halting

proof end;

theorem Th86: :: SCMPDS_2:86

for k1, k2 being Integer
for a being Int_position holds not (a,k1) <>0_goto k2 is halting

proof end;

theorem Th87: :: SCMPDS_2:87

for k1, k2 being Integer
for a being Int_position holds not (a,k1) <=0_goto k2 is halting

proof end;

theorem Th88: :: SCMPDS_2:88

for k1, k2 being Integer
for a being Int_position holds not (a,k1) >=0_goto k2 is halting

proof end;

theorem Th89: :: SCMPDS_2:89

for a being Int_position holds not return a is halting

proof end;

theorem Th90: :: SCMPDS_2:90

for k1 being Integer
for a being Int_position holds not saveIC (a,k1) is halting

proof end;

theorem Th91: :: SCMPDS_2:91

for I being set holds
( not I is Instruction of SCMPDS or ex k1 being Integer st I = goto k1 or ex a being Int_position st I = return a or ex a being Int_position ex k1 being Integer st I = saveIC (a,k1) or ex a being Int_position ex k1 being Integer st I = a := k1 or ex a being Int_position ex k1, k2 being Integer st I = (a,k1) := k2 or ex a being Int_position ex k1, k2 being Integer st I = (a,k1) <>0_goto k2 or ex a being Int_position ex k1, k2 being Integer st I = (a,k1) <=0_goto k2 or ex a being Int_position ex k1, k2 being Integer st I = (a,k1) >=0_goto k2 or ex a, b being Int_position ex k1, k2 being Integer st I = AddTo (a,k1,k2) or ex a, b being Int_position ex k1, k2 being Integer st I = AddTo (a,k1,b,k2) or ex a, b being Int_position ex k1, k2 being Integer st I = SubFrom (a,k1,b,k2) or ex a, b being Int_position ex k1, k2 being Integer st I = MultBy (a,k1,b,k2) or ex a, b being Int_position ex k1, k2 being Integer st I = Divide (a,k1,b,k2) or ex a, b being Int_position ex k1, k2 being Integer st I = (a,k1) := (b,k2) )

proof end;

Lm11: for W being Instruction of SCMPDS st W is halting holds
W = goto 0

proof end;

registration

cluster SCMPDS -> strict halting ;
coherence
SCMPDS is halting

proof end;

end;

theorem Th92: :: SCMPDS_2:92

for I being Instruction of SCMPDS st I is halting holds
I = halt SCMPDS

proof end;

theorem :: SCMPDS_2:93

halt SCMPDS = goto 0 by Th75, Th92;

registration

cluster SCMPDS -> realistic strict ;
coherence
SCMPDS is realistic

proof end;

end;

theorem :: SCMPDS_2:94

canceled;

theorem :: SCMPDS_2:95

canceled;

theorem :: SCMPDS_2:96

canceled;

theorem :: SCMPDS_2:97

canceled;

theorem :: SCMPDS_2:98

for i being Element of NAT holds
( IC <> dl. i & IC <> i )

proof end;

theorem :: SCMPDS_2:99

for I being Instruction of SCMPDS st I = goto 0 holds
I is halting by Th75;

theorem :: SCMPDS_2:100

Data-Locations SCMPDS = SCM-Data-Loc by Lm10;