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

definition

func SCMPDS -> strict AMI-Struct over Segm 2 equals :: SCMPDS_2:def 1
AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),SCMPDS-Instr,SCM-OK,SCM-VAL,SCMPDS-Exec #);

correctness
coherence
AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),SCMPDS-Instr,SCM-OK,SCM-VAL,SCMPDS-Exec #) is strict AMI-Struct over Segm 2;
;

end;

:: deftheorem defines SCMPDS SCMPDS_2:def 1 :
SCMPDS = AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),SCMPDS-Instr,SCM-OK,SCM-VAL,SCMPDS-Exec #);

registration

cluster SCMPDS -> non empty strict ;

coherence
not SCMPDS is empty ;

end;

registration

cluster SCMPDS -> with_non-empty_values IC-Ins-separated strict ;

coherence
( SCMPDS is with_non-empty_values & SCMPDS is IC-Ins-separated ) by AMI_2:22, SUBSET_1:def 8, AMI_2:6;

end;

theorem :: SCMPDS_2:1

canceled;

::$CT

theorem Th1: :: SCMPDS_2:2

IC = NAT by AMI_2:22, SUBSET_1:def 8;

registration

cluster Int-like for Element of the carrier of SCMPDS;

existence
ex b₁ being Object of SCMPDS st b₁ is Int-like

proof end;

end;

definition

mode Int_position is Int-like Object of SCMPDS;

end;

:: deftheorem SCMPDS_2:def 2 :
canceled;

::$CD

theorem :: SCMPDS_2:3

canceled;

::$CD

theorem :: SCMPDS_2:4

canceled;

::$CT 2

theorem Th2: :: SCMPDS_2:5

for l being Int_position holds Values l = INT

proof end;

set S1 = { [14,{},<*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 15, 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 15, 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 15, d4, d5 is Element of SCM-Data-Loc , k5, k6 is Element of INT : I3 in {9,10,11,12,13} } ;

Lm1: for I being Instruction of SCMPDS holds
( I in {[0,{},{}]} or I in { [14,{},<*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 15, 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 15, 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 15, 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:6

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

proof end;

registration

let s be State of SCMPDS;
let d be Int_position;

cluster s . d -> integer ;

coherence
s . d is integer

proof end;

end;

definition

let m, n be Integer;

func DataLoc (m,n) -> Int_position equals :: SCMPDS_2:def 3
[1,|.(m + n).|];

coherence
[1,|.(m + n).|] is Int_position

proof end;

end;

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

theorem Th4: :: SCMPDS_2:7

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

proof end;

theorem Th5: :: SCMPDS_2:8

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

proof end;

theorem Th6: :: SCMPDS_2:9

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 Th7: :: SCMPDS_2:10

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 Th8: :: SCMPDS_2:11

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 4
[14,{},<*k1*>];

correctness
coherence
[14,{},<*k1*>] is Instruction of SCMPDS;
by Th4;

end;

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

definition

let a be Int_position;

func return a -> Instruction of SCMPDS equals :: SCMPDS_2:def 5
[1,{},<*a*>];

correctness
coherence
[1,{},<*a*>] is Instruction of SCMPDS;

proof end;

end;

:: deftheorem defines return SCMPDS_2:def 5 :
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 6
[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 7
[3,{},<*a,k1*>];

correctness
coherence
[3,{},<*a,k1*>] is Instruction of SCMPDS;

proof end;

end;

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

:: deftheorem defines saveIC SCMPDS_2:def 7 :
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 8
[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 9
[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 10
[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 11
[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 12
[8,{},<*a,k1,k2*>];

correctness
coherence
[8,{},<*a,k1,k2*>] is Instruction of SCMPDS;

proof end;

end;

:: deftheorem defines <>0_goto SCMPDS_2:def 8 :
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 9 :
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 10 :
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 11 :
for a being Int_position
for k1, k2 being Integer holds (a,k1) := k2 = [7,{},<*a,k1,k2*>];

:: deftheorem defines AddTo SCMPDS_2:def 12 :
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 13
[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 14
[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 15
[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 16
[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 17
[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 13 :
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 14 :
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 15 :
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 16 :
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 17 :
for a, b being Int_position
for k1, k2 being Integer holds (a,k1) := (b,k2) = [13,{},<*a,b,k1,k2*>];

theorem :: SCMPDS_2:12

for k1 being Integer holds InsCode (goto k1) = 14 ;

theorem :: SCMPDS_2:13

for a being Int_position holds InsCode (return a) = 1 ;

theorem :: SCMPDS_2:14

for k1 being Integer
for a being Int_position holds InsCode (a := k1) = 2 ;

theorem :: SCMPDS_2:15

for k1 being Integer
for a being Int_position holds InsCode (saveIC (a,k1)) = 3 ;

theorem :: SCMPDS_2:16

for k1, k2 being Integer
for a being Int_position holds InsCode ((a,k1) <>0_goto k2) = 4 ;

theorem :: SCMPDS_2:17

for k1, k2 being Integer
for a being Int_position holds InsCode ((a,k1) <=0_goto k2) = 5 ;

theorem :: SCMPDS_2:18

for k1, k2 being Integer
for a being Int_position holds InsCode ((a,k1) >=0_goto k2) = 6 ;

theorem :: SCMPDS_2:19

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

theorem :: SCMPDS_2:20

for k1, k2 being Integer
for a being Int_position holds InsCode (AddTo (a,k1,k2)) = 8 ;

theorem :: SCMPDS_2:21

for k1, k2 being Integer
for a, b being Int_position holds InsCode (AddTo (a,k1,b,k2)) = 9 ;

theorem :: SCMPDS_2:22

for k1, k2 being Integer
for a, b being Int_position holds InsCode (SubFrom (a,k1,b,k2)) = 10 ;

theorem :: SCMPDS_2:23

for k1, k2 being Integer
for a, b being Int_position holds InsCode (MultBy (a,k1,b,k2)) = 11 ;

theorem :: SCMPDS_2:24

for k1, k2 being Integer
for a, b being Int_position holds InsCode (Divide (a,k1,b,k2)) = 12 ;

theorem :: SCMPDS_2:25

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

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

proof end;

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

Lm4: for I being Instruction of SCMPDS holds
( not I in { [I1,{},<*d1,k1*>] where I1 is Element of Segm 15, 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;

Lm5: for I being Instruction of SCMPDS holds
( not I in { [I1,{},<*d1,k1,k2*>] where I1 is Element of Segm 15, 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;

Lm6: for I being Instruction of SCMPDS holds
( not I in { [I1,{},<*d1,d2,k1,k2*>] where I1 is Element of Segm 15, 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;

Lm7: for I being Instruction of SCMPDS st I in {[0,{},{}]} holds
InsCode I = 0

proof end;

theorem :: SCMPDS_2:26

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

proof end;

theorem :: SCMPDS_2:27

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

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

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,{},{}]} & not I in { [14,{},<*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 15, 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 15, 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 = 14 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 )
by Lm2, Lm3, Lm4, Lm6, Lm7;

theorem :: SCMPDS_2:30

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

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

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

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

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,{},{}]} & not I in { [14,{},<*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 15, 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 15, 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 = 14 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:35

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

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

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

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

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

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

proof end;

theorem Th38: :: SCMPDS_2:41

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

proof end;

Lm10: Data-Locations = SCM-Data-Loc

proof end;

theorem :: SCMPDS_2:42

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

proof end;

theorem :: SCMPDS_2:43

for dl being Int_position holds dl <> IC

proof end;

theorem :: SCMPDS_2:44

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

proof end;

theorem Th42: :: SCMPDS_2:45

for s being State of SCMPDS
for k1 being Integer
for a being Int_position holds
( (Exec ((a := k1),s)) . (IC ) = (IC s) + 1 & (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 Th43: :: SCMPDS_2:46

for s being State of SCMPDS
for k1, k2 being Integer
for a being Int_position holds
( (Exec (((a,k1) := k2),s)) . (IC ) = (IC s) + 1 & (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 Th44: :: SCMPDS_2:47

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 ) = (IC s) + 1 & (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 Th45: :: SCMPDS_2:48

for s being State of SCMPDS
for k1, k2 being Integer
for a being Int_position holds
( (Exec ((AddTo (a,k1,k2)),s)) . (IC ) = (IC s) + 1 & (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 Th46: :: SCMPDS_2:49

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 ) = (IC s) + 1 & (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 Th47: :: SCMPDS_2:50

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 ) = (IC s) + 1 & (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 Th48: :: SCMPDS_2:51

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 ) = (IC s) + 1 & (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 Th49: :: SCMPDS_2:52

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 ) = (IC s) + 1 & ( 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:53

for s being State of SCMPDS
for k1 being Integer
for a being Int_position holds
( (Exec ((Divide (a,k1,a,k1)),s)) . (IC ) = (IC s) + 1 & (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 Th49;

definition

let s be State of SCMPDS;
let c be Integer;

func ICplusConst (s,c) -> Element of NAT means :Def17: :: SCMPDS_2:def 18
ex m being Element of NAT st
( m = IC s & it = |.(m + c).| );

existence
ex b₁, m being Element of NAT st
( m = IC s & b₁ = |.(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₁ = |.(m + c).| ) & ex m being Element of NAT st
( m = IC s & b₂ = |.(m + c).| ) holds
b₁ = b₂;
;

end;

:: deftheorem Def17 defines ICplusConst SCMPDS_2:def 18 :
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₃ = |.(m + c).| ) );

theorem Th51: :: SCMPDS_2:54

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 Th52: :: SCMPDS_2:55

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 ) = (IC s) + 1 ) & (Exec (((a,k1) <>0_goto k2),s)) . b = s . b )

proof end;

theorem Th53: :: SCMPDS_2:56

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 ) = (IC s) + 1 ) & (Exec (((a,k1) <=0_goto k2),s)) . b = s . b )

proof end;

theorem Th54: :: SCMPDS_2:57

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 ) = (IC s) + 1 ) & (Exec (((a,k1) >=0_goto k2),s)) . b = s . b )

proof end;

theorem Th55: :: SCMPDS_2:58

for s being State of SCMPDS
for a being Int_position holds
( (Exec ((return a),s)) . (IC ) = |.(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 Th56: :: SCMPDS_2:59

for s being State of SCMPDS
for k1 being Integer
for a being Int_position holds
( (Exec ((saveIC (a,k1)),s)) . (IC ) = (IC s) + 1 & (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 :: SCMPDS_2:60

canceled;

::$CT

theorem Th57: :: SCMPDS_2:61

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

proof end;

theorem Th58: :: SCMPDS_2:62

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;

Lm11: for s being State of SCMPDS
for I being Instruction of SCMPDS st InsCode I = 0 holds
Exec (I,s) = s

proof end;

theorem Th59: :: SCMPDS_2:63

for I being Instruction of SCMPDS st I = [0,{},{}] holds
I is halting

proof end;

theorem Th60: :: SCMPDS_2:64

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

proof end;

theorem :: SCMPDS_2:65

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

proof end;

theorem :: SCMPDS_2:66

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

proof end;

theorem :: SCMPDS_2:67

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

proof end;

theorem :: SCMPDS_2:68

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

proof end;

theorem :: SCMPDS_2:69

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

proof end;

theorem :: SCMPDS_2:70

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

proof end;

theorem :: SCMPDS_2:71

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

proof end;

theorem :: SCMPDS_2:72

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

proof end;

theorem :: SCMPDS_2:73

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

proof end;

theorem :: SCMPDS_2:74

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

proof end;

theorem :: SCMPDS_2:75

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

proof end;

theorem :: SCMPDS_2:76

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

proof end;

theorem :: SCMPDS_2:77

for a being Int_position holds not return a is halting

proof end;

theorem :: SCMPDS_2:78

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

proof end;

theorem :: SCMPDS_2:79

for I being set holds
( not I is Instruction of SCMPDS or I = [0,{},{}] 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;

:: Poniewaz zostal dodany prawdziwy halt,
:: tego lematu nie mozna udowodnic.
::Lm11: for W being Instruction of SCMPDS st W is halting holds W = goto 0
::proof
:: set I = goto 0;
:: let W be Instruction of SCMPDS such that
::A1: W is halting;
:: assume
::A2: I <> W;
:: per cases by Th91;
:: suppose
:: ex k1 st W=goto k1;
:: hence thesis by A1,A2,Th85;
:: end;
:: suppose
:: ex a st W = return a;
:: hence thesis by A1,Th89;
:: end;
:: suppose
:: ex a,k1 st W = saveIC(a,k1);
:: hence thesis by A1,Th90;
:: end;
:: suppose
:: ex a,k1 st W = a:=k1;
:: hence thesis by A1,Th77;
:: end;
:: suppose
:: ex a,k1,k2 st W=(a,k1):=k2;
:: hence thesis by A1,Th78;
:: end;
:: suppose
:: ex a,k1,k2 st W = (a,k1)<>0_goto k2;
:: hence thesis by A1,Th86;
:: end;
:: suppose
:: ex a,k1,k2 st W = (a,k1)<=0_goto k2;
:: hence thesis by A1,Th87;
:: end;
:: suppose
:: ex a,k1,k2 st W = (a,k1)>=0_goto k2;
:: hence thesis by A1,Th88;
:: end;
:: suppose
:: ex a,b,k1,k2 st W = AddTo(a,k1,k2);
:: hence thesis by A1,Th80;
:: end;
:: suppose
:: ex a,b,k1,k2 st W = AddTo(a,k1,b,k2);
:: hence thesis by A1,Th81;
:: end;
:: suppose
:: ex a,b,k1,k2 st W = SubFrom(a,k1,b,k2);
:: hence thesis by A1,Th82;
:: end;
:: suppose
:: ex a,b,k1,k2 st W = MultBy(a,k1,b,k2);
:: hence thesis by A1,Th83;
:: end;
:: suppose
:: ex a,b,k1,k2 st W = Divide(a,k1,b,k2);
:: hence thesis by A1,Th84;
:: end;
:: suppose
:: ex a,b,k1,k2 st W = (a,k1):=(b,k2);
:: hence thesis by A1,Th79;
:: end;
::end;

registration

cluster SCMPDS -> strict halting ;

coherence
SCMPDS is halting by Th59;

end;

::Dopoki sa przeskoki, to jednoznacznosc instrukcji, ktora jest halting
:: i tak sie nie uda udowodnic.
::theorem Th92:
:: for I being Instruction of SCMPDS st I is halting holds I = halt
:: SCMPDS
::proof
:: let I be Instruction of SCMPDS;
:: assume I is halting;
:: then I = goto 0 by Lm11;
:: hence thesis by Lm11;
::end;

theorem :: SCMPDS_2:80

halt SCMPDS = [0,{},{}] ;

::Dopoki sa przeskoki, to jednoznacznosc instrukcji, ktora jest halting
:: i tak sie nie uda udowodnic.
::theorem Th92:
:: for I being Instruction of SCMPDS st I is halting holds I = halt
:: SCMPDS
::proof
:: let I be Instruction of SCMPDS;
:: assume I is halting;
:: then I = goto 0 by Lm11;
:: hence thesis by Lm11;
::end;

theorem :: SCMPDS_2:81

canceled;

::$CT

theorem :: SCMPDS_2:82

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

proof end;

theorem :: SCMPDS_2:83

canceled;

::$CT

theorem :: SCMPDS_2:84

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

::$CT

theorem :: SCMPDS_2:85

canceled;

::$CT

theorem :: SCMPDS_2:86

for s being State of SCMPDS
for I being Instruction of SCMPDS st InsCode I = 0 holds
Exec (I,s) = s by Lm11;