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


begin

definition
func SCMPDS -> strict AMI-Struct over 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 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 by STRUCT_0:def 1;
end;

registration
cluster SCMPDS -> with_non-empty_values IC-Ins-separated strict ;
coherence
( SCMPDS is with_non-empty_values & SCMPDS is IC-Ins-separated )
proof end;
end;

theorem :: SCMPDS_2:1
canceled;

theorem Th2: :: SCMPDS_2:2
IC = NAT by AMI_2:22, FUNCT_7:def 1;

begin

registration
cluster Int-like for Element of the carrier of SCMPDS;
existence
ex b1 being Object of SCMPDS st b1 is Int-like
proof end;
end;

definition
mode Int_position is Int-like Object of SCMPDS;
canceled;
end;

:: deftheorem SCMPDS_2:def 2 :
canceled;

theorem :: SCMPDS_2:3
canceled;

theorem :: SCMPDS_2:4
canceled;

theorem Th5: :: SCMPDS_2:5
for l being Int_position holds Values l = INT
proof end;

begin

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,(abs (m + n))];
coherence
[1,(abs (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,(abs (m + n))];

theorem Th7: :: SCMPDS_2:7
for k1 being Integer holds [14,{},<*k1*>] in SCMPDS-Instr
proof end;

theorem Th8: :: SCMPDS_2:8
for d1 being Element of SCM-Data-Loc holds [1,{},<*d1*>] in SCMPDS-Instr
proof end;

theorem Th9: :: 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 Th10: :: 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 Th11: :: 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 Th7;
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 by RECDEF_2:def 1;

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

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

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

theorem :: SCMPDS_2:16
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:17
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:18
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:19
for k1, k2 being Integer
for a being Int_position holds InsCode ((a,k1) := k2) = 7 by RECDEF_2:def 1;

theorem :: SCMPDS_2:20
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:21
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:22
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:23
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:24
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:25
for k1, k2 being Integer
for a, b being Int_position holds InsCode ((a,k1) := (b,k2)) = 13 by RECDEF_2:def 1;

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

begin

theorem Th45: :: SCMPDS_2:45
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 Th46: :: 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 ) = 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 Th47: :: 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 ) = 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 Th48: :: 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 ) = 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 Th49: :: 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 ) = 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 Th50: :: 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 ) = 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 Th51: :: 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 ) = 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 Th52: :: 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 ) = 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: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 ) = 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 Th52;

definition
let s be State of SCMPDS;
let c be Integer;
func ICplusConst (s,c) -> Element of NAT means :Def18: :: SCMPDS_2:def 18
 ex m being Element of NAT st
( m = IC s & it = abs (m + c) );
existence
ex b1, m being Element of NAT st
( m = IC s & b1 = abs (m + c) )
proof end;
correctness
uniqueness
for b1, b2 being Element of NAT st ex m being Element of NAT st
( m = IC s & b1 = abs (m + c) ) & ex m being Element of NAT st
( m = IC s & b2 = abs (m + c) ) holds
b1 = b2;
;
end;

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

theorem Th54: :: 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 Th55: :: 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 ) = succ (IC s) ) & (Exec (((a,k1) <>0_goto k2),s)) . b = s . b )
proof end;

theorem Th56: :: 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 ) = succ (IC s) ) & (Exec (((a,k1) <=0_goto k2),s)) . b = s . b )
proof end;

theorem Th57: :: 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 ) = succ (IC s) ) & (Exec (((a,k1) >=0_goto k2),s)) . b = s . b )
proof end;

theorem Th58: :: SCMPDS_2:58
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 Th59: :: 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 ) = 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 :: SCMPDS_2:60
canceled;

theorem Th61: :: 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 Th62: :: 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 Th63: :: SCMPDS_2:63
for I being Instruction of SCMPDS st I = [0,{},{}] holds
I is halting
proof end;

theorem Th64: :: SCMPDS_2:64
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 :: 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
proof 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;
theorem :: SCMPDS_2:80
halt SCMPDS = [0,{},{}] ;

theorem :: SCMPDS_2:81
canceled;

theorem :: SCMPDS_2:82
for i being Element of NAT holds IC <> dl. i
proof end;

theorem :: SCMPDS_2:83
canceled;

theorem :: SCMPDS_2:84
Data-Locations = SCM-Data-Loc by Lm10;

theorem :: SCMPDS_2:85
canceled;

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;