:: by JingChao Chen

::

:: Received June 15, 1999

:: Copyright (c) 1999-2016 Association of Mizar Users

definition

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;

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 AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),SCMPDS-Instr,SCM-OK,SCM-VAL,SCMPDS-Exec #);

coherence

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

;

:: deftheorem defines SCMPDS SCMPDS_2:def 1 :

SCMPDS = AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),SCMPDS-Instr,SCM-OK,SCM-VAL,SCMPDS-Exec #);

SCMPDS = AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),SCMPDS-Instr,SCM-OK,SCM-VAL,SCMPDS-Exec #);

registration

coherence

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

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

::$CT

::$CD

::$CD

::$CT 2

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;

registration
end;

:: deftheorem defines DataLoc SCMPDS_2:def 3 :

for m, n being Integer holds DataLoc (m,n) = [1,|.(m + n).|];

for m, n being Integer holds DataLoc (m,n) = [1,|.(m + n).|];

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

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

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

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
end;

definition
end;

:: deftheorem defines return SCMPDS_2:def 5 :

for a being Int_position holds return a = [1,{},<*a*>];

for a being Int_position holds return a = [1,{},<*a*>];

definition

let a be Int_position;

let k1 be Integer;

correctness

coherence

[2,{},<*a,k1*>] is Instruction of SCMPDS;

coherence

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

end;
let k1 be Integer;

correctness

coherence

[2,{},<*a,k1*>] is Instruction of SCMPDS;

proof end;

correctness coherence

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

proof end;

:: deftheorem defines := SCMPDS_2:def 6 :

for a being Int_position

for k1 being Integer holds a := k1 = [2,{},<*a,k1*>];

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*>];

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;

correctness

coherence

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

coherence

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

coherence

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

coherence

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

coherence

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

end;
let k1, k2 be Integer;

correctness

coherence

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

proof end;

correctness coherence

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

proof end;

correctness coherence

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

proof end;

correctness coherence

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

proof end;

correctness coherence

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

proof 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*>];

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*>];

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*>];

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*>];

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*>];

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;

correctness

coherence

[9,{},<*a,b,k1,k2*>] is Instruction of SCMPDS;

coherence

[10,{},<*a,b,k1,k2*>] is Instruction of SCMPDS;

coherence

[11,{},<*a,b,k1,k2*>] is Instruction of SCMPDS;

coherence

[12,{},<*a,b,k1,k2*>] is Instruction of SCMPDS;

coherence

[13,{},<*a,b,k1,k2*>] is Instruction of SCMPDS;

end;
let k1, k2 be Integer;

correctness

coherence

[9,{},<*a,b,k1,k2*>] is Instruction of SCMPDS;

proof end;

correctness coherence

[10,{},<*a,b,k1,k2*>] is Instruction of SCMPDS;

proof end;

correctness coherence

[11,{},<*a,b,k1,k2*>] is Instruction of SCMPDS;

proof end;

correctness coherence

[12,{},<*a,b,k1,k2*>] is Instruction of SCMPDS;

proof end;

correctness coherence

[13,{},<*a,b,k1,k2*>] is Instruction of SCMPDS;

proof 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*>];

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*>];

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*>];

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*>];

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*>];

for a, b being Int_position

for k1, k2 being Integer holds (a,k1) := (b,k2) = [13,{},<*a,b,k1,k2*>];

theorem :: SCMPDS_2:15

theorem :: SCMPDS_2:16

theorem :: SCMPDS_2:17

theorem :: SCMPDS_2:18

theorem :: SCMPDS_2:19

theorem :: SCMPDS_2:20

theorem :: SCMPDS_2:21

theorem :: SCMPDS_2:22

theorem :: SCMPDS_2:23

theorem :: SCMPDS_2:24

theorem :: SCMPDS_2:25

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

for ins being Instruction of SCMPDS st InsCode ins = 1 holds

ex a being Int_position st ins = return a

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

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)

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

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

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

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

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)

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)

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)

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)

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)

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)

ex a, b being Int_position ex k1, k2 being Integer st ins = (a,k1) := (b,k2)

proof end;

Lm10: Data-Locations = SCM-Data-Loc

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

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 ) )

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 ) )

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 ) )

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 ) )

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 ) )

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 ) )

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 ) )

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 ) )

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;

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;

ex b_{1}, m being Element of NAT st

( m = IC s & b_{1} = |.(m + c).| )

uniqueness

for b_{1}, b_{2} being Element of NAT st ex m being Element of NAT st

( m = IC s & b_{1} = |.(m + c).| ) & ex m being Element of NAT st

( m = IC s & b_{2} = |.(m + c).| ) holds

b_{1} = b_{2};

;

end;
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 m being Element of NAT st

( m = IC s & it = |.(m + c).| );

ex b

( m = IC s & b

proof end;

correctness uniqueness

for b

( m = IC s & b

( m = IC s & b

b

;

:: deftheorem Def17 defines ICplusConst SCMPDS_2:def 18 :

for s being State of SCMPDS

for c being Integer

for b_{3} being Element of NAT holds

( b_{3} = ICplusConst (s,c) iff ex m being Element of NAT st

( m = IC s & b_{3} = |.(m + c).| ) );

for s being State of SCMPDS

for c being Integer

for b

( b

( m = IC s & b

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 ) )

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 )

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 )

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 )

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 ) )

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 ) )

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;

::$CT

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 ) )

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

not I 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) )

( 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;

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

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

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

::$CT

::$CT

::$CT

theorem :: SCMPDS_2:86