:: SCMPDS_2 semantic presentation

definition
func SCMPDS -> strict AMI-Struct of {INT } equals :: SCMPDS_2:def 1
 AMI-Struct(# NAT ,0,SCM-Instr-Loc ,(Segm 14),SCMPDS-Instr ,SCMPDS-OK ,SCMPDS-Exec #);
correctness
coherence
AMI-Struct(# NAT ,0,SCM-Instr-Loc ,(Segm 14),SCMPDS-Instr ,SCMPDS-OK ,SCMPDS-Exec #) is strict AMI-Struct of {INT };
;
end;

:: deftheorem Def1 defines SCMPDS SCMPDS_2:def 1 :
SCMPDS = AMI-Struct(# NAT ,0,SCM-Instr-Loc ,(Segm 14),SCMPDS-Instr ,SCMPDS-OK ,SCMPDS-Exec #);

registration
cluster SCMPDS -> non empty strict non void ;
coherence
( not SCMPDS is empty & not SCMPDS is void ) by AMI_1:def 3, STRUCT_0:def 1;
end;

theorem Th1: :: SCMPDS_2:1
for b1 being set holds
( ex b2 being Nat st b1 = (2 * b2) + 2 iff b1 in SCM-Instr-Loc )
proof end;

theorem Th2: :: SCMPDS_2:2
SCMPDS is data-oriented
proof end;

theorem Th3: :: SCMPDS_2:3
SCMPDS is definite
proof end;

registration
cluster SCMPDS -> non empty strict non void IC-Ins-separated data-oriented definite ;
coherence
( SCMPDS is IC-Ins-separated & SCMPDS is data-oriented & SCMPDS is definite )
proof end;
end;

theorem Th4: :: SCMPDS_2:4
( the Instruction-Locations of SCMPDS <> INT & the Instructions of SCMPDS <> INT & the Instruction-Locations of SCMPDS <> the Instructions of SCMPDS ) by AMI_2:6, SCMPDS_1:17;

theorem Th5: :: SCMPDS_2:5
NAT = ({0} \/ SCM-Data-Loc ) \/ SCM-Instr-Loc
proof end;

theorem Th6: :: SCMPDS_2:6
IC SCMPDS = 0 ;

theorem Th7: :: SCMPDS_2:7
for b1 being State of SCMPDS
for b2 being SCMPDS-State st b2 = b1 holds
IC b1 = IC b2 by SCMPDS_1:def 5;

definition
mode Int_position -> Object of SCMPDS means :Def2: :: SCMPDS_2:def 2
a1 in SCM-Data-Loc ;
existence
ex b1 being Object of SCMPDS st b1 in SCM-Data-Loc
proof end;
end;

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

theorem Th8: :: SCMPDS_2:8
canceled;

theorem Th9: :: SCMPDS_2:9
for b1 being set st b1 in SCM-Data-Loc holds
b1 is Int_position by Def2;

theorem Th10: :: SCMPDS_2:10
SCM-Data-Loc misses the Instruction-Locations of SCMPDS by AMI_5:33;

theorem Th11: :: SCMPDS_2:11
not the Instruction-Locations of SCMPDS is finite by AMI_3:def 1, AMI_5:32;

theorem Th12: :: SCMPDS_2:12
for b1 being Int_position holds b1 is Data-Location
proof end;

theorem Th13: :: SCMPDS_2:13
for b1 being Int_position holds ObjectKind b1 = INT
proof end;

theorem Th14: :: SCMPDS_2:14
for b1 being set st b1 in SCM-Instr-Loc holds
b1 is Instruction-Location of SCMPDS ;

registration
let c1 be Instruction of SCMPDS ;
cluster InsCode a1 -> natural ;
coherence
InsCode c1 is natural
proof end;
end;

set c1 = { [0,<*b1*>] where B is Element of INT : verum } ;

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

set c3 = { [b1,<*b2,b3*>] where B is Element of Segm 14, B is Element of SCM-Data-Loc , B is Element of INT : b1 in {2,3} } ;

set c4 = { [b1,<*b2,b3,b4*>] where B is Element of Segm 14, B is Element of SCM-Data-Loc , B is Element of INT , B is Element of INT : b1 in {4,5,6,7,8} } ;

set c5 = { [b1,<*b2,b3,b4,b5*>] where B is Element of Segm 14, B is Element of SCM-Data-Loc , B is Element of SCM-Data-Loc , B is Element of INT , B is Element of INT : b1 in {9,10,11,12,13} } ;

Lemma8: for b1 being Instruction of SCMPDS holds
( not b1 in SCMPDS-Instr or b1 in { [0,<*b2*>] where B is Element of INT : verum } or b1 in { [1,<*b2*>] where B is Element of SCM-Data-Loc : verum } or b1 in { [b2,<*b3,b4*>] where B is Element of Segm 14, B is Element of SCM-Data-Loc , B is Element of INT : b2 in {2,3} } or b1 in { [b2,<*b3,b4,b5*>] where B is Element of Segm 14, B is Element of SCM-Data-Loc , B is Element of INT , B is Element of INT : b2 in {4,5,6,7,8} } or b1 in { [b2,<*b3,b4,b5,b6*>] where B is Element of Segm 14, B is Element of SCM-Data-Loc , B is Element of SCM-Data-Loc , B is Element of INT , B is Element of INT : b2 in {9,10,11,12,13} } )
proof end;

theorem Th15: :: SCMPDS_2:15
for b1 being Instruction of SCMPDS holds InsCode b1 <= 13
proof end;

definition
let c6 be State of SCMPDS ;
let c7 be Int_position ;
redefine func . as c1 . c2 -> Integer;
coherence
c6 . c7 is Integer
proof end;
end;

definition
let c6, c7 be Integer;
canceled;
func DataLoc c1,c2 -> Int_position equals :: SCMPDS_2:def 4
(2 * (abs (a1 + a2))) + 1;
coherence
(2 * (abs (c6 + c7))) + 1 is Int_position
proof end;
end;

:: deftheorem Def3 SCMPDS_2:def 3 :
canceled;

:: deftheorem Def4 defines DataLoc SCMPDS_2:def 4 :
for b1, b2 being Integer holds DataLoc b1,b2 = (2 * (abs (b1 + b2))) + 1;

theorem Th16: :: SCMPDS_2:16
for b1 being Integer holds [0,<*b1*>] in SCMPDS-Instr
proof end;

theorem Th17: :: SCMPDS_2:17
for b1 being Element of SCM-Data-Loc holds [1,<*b1*>] in SCMPDS-Instr
proof end;

theorem Th18: :: SCMPDS_2:18
for b1 being set
for b2 being Element of SCM-Data-Loc
for b3 being Integer st b1 in {2,3} holds
[b1,<*b2,b3*>] in SCMPDS-Instr
proof end;

theorem Th19: :: SCMPDS_2:19
for b1 being set
for b2 being Element of SCM-Data-Loc
for b3, b4 being Integer st b1 in {4,5,6,7,8} holds
[b1,<*b2,b3,b4*>] in SCMPDS-Instr
proof end;

theorem Th20: :: SCMPDS_2:20
for b1 being set
for b2, b3 being Element of SCM-Data-Loc
for b4, b5 being Integer st b1 in {9,10,11,12,13} holds
[b1,<*b2,b3,b4,b5*>] in SCMPDS-Instr
proof end;

definition
let c6 be Integer;
func goto c1 -> Instruction of SCMPDS equals :: SCMPDS_2:def 5
[0,<*a1*>];
correctness
coherence
[0,<*c6*>] is Instruction of SCMPDS ;
by Th16;
end;

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

definition
let c6 be Int_position ;
func return c1 -> Instruction of SCMPDS equals :: SCMPDS_2:def 6
[1,<*a1*>];
correctness
coherence
[1,<*c6*>] is Instruction of SCMPDS ;
proof end;
end;

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

definition
let c6 be Int_position ;
let c7 be Integer;
func c1 := c2 -> Instruction of SCMPDS equals :: SCMPDS_2:def 7
[2,<*a1,a2*>];
correctness
coherence
[2,<*c6,c7*>] is Instruction of SCMPDS ;
proof end;
func saveIC c1,c2 -> Instruction of SCMPDS equals :: SCMPDS_2:def 8
[3,<*a1,a2*>];
correctness
coherence
[3,<*c6,c7*>] is Instruction of SCMPDS ;
proof end;
end;

:: deftheorem Def7 defines := SCMPDS_2:def 7 :
for b1 being Int_position
for b2 being Integer holds b1 := b2 = [2,<*b1,b2*>];

:: deftheorem Def8 defines saveIC SCMPDS_2:def 8 :
for b1 being Int_position
for b2 being Integer holds saveIC b1,b2 = [3,<*b1,b2*>];

definition
let c6 be Int_position ;
let c7, c8 be Integer;
func c1,c2 <>0_goto c3 -> Instruction of SCMPDS equals :: SCMPDS_2:def 9
[4,<*a1,a2,a3*>];
correctness
coherence
[4,<*c6,c7,c8*>] is Instruction of SCMPDS ;
proof end;
func c1,c2 <=0_goto c3 -> Instruction of SCMPDS equals :: SCMPDS_2:def 10
[5,<*a1,a2,a3*>];
correctness
coherence
[5,<*c6,c7,c8*>] is Instruction of SCMPDS ;
proof end;
func c1,c2 >=0_goto c3 -> Instruction of SCMPDS equals :: SCMPDS_2:def 11
[6,<*a1,a2,a3*>];
correctness
coherence
[6,<*c6,c7,c8*>] is Instruction of SCMPDS ;
proof end;
func c1,c2 := c3 -> Instruction of SCMPDS equals :: SCMPDS_2:def 12
[7,<*a1,a2,a3*>];
correctness
coherence
[7,<*c6,c7,c8*>] is Instruction of SCMPDS ;
proof end;
func AddTo c1,c2,c3 -> Instruction of SCMPDS equals :: SCMPDS_2:def 13
[8,<*a1,a2,a3*>];
correctness
coherence
[8,<*c6,c7,c8*>] is Instruction of SCMPDS ;
proof end;
end;

:: deftheorem Def9 defines <>0_goto SCMPDS_2:def 9 :
for b1 being Int_position
for b2, b3 being Integer holds b1,b2 <>0_goto b3 = [4,<*b1,b2,b3*>];

:: deftheorem Def10 defines <=0_goto SCMPDS_2:def 10 :
for b1 being Int_position
for b2, b3 being Integer holds b1,b2 <=0_goto b3 = [5,<*b1,b2,b3*>];

:: deftheorem Def11 defines >=0_goto SCMPDS_2:def 11 :
for b1 being Int_position
for b2, b3 being Integer holds b1,b2 >=0_goto b3 = [6,<*b1,b2,b3*>];

:: deftheorem Def12 defines := SCMPDS_2:def 12 :
for b1 being Int_position
for b2, b3 being Integer holds b1,b2 := b3 = [7,<*b1,b2,b3*>];

:: deftheorem Def13 defines AddTo SCMPDS_2:def 13 :
for b1 being Int_position
for b2, b3 being Integer holds AddTo b1,b2,b3 = [8,<*b1,b2,b3*>];

definition
let c6, c7 be Int_position ;
let c8, c9 be Integer;
func AddTo c1,c3,c2,c4 -> Instruction of SCMPDS equals :: SCMPDS_2:def 14
[9,<*a1,a2,a3,a4*>];
correctness
coherence
[9,<*c6,c7,c8,c9*>] is Instruction of SCMPDS ;
proof end;
func SubFrom c1,c3,c2,c4 -> Instruction of SCMPDS equals :: SCMPDS_2:def 15
[10,<*a1,a2,a3,a4*>];
correctness
coherence
[10,<*c6,c7,c8,c9*>] is Instruction of SCMPDS ;
proof end;
func MultBy c1,c3,c2,c4 -> Instruction of SCMPDS equals :: SCMPDS_2:def 16
[11,<*a1,a2,a3,a4*>];
correctness
coherence
[11,<*c6,c7,c8,c9*>] is Instruction of SCMPDS ;
proof end;
func Divide c1,c3,c2,c4 -> Instruction of SCMPDS equals :: SCMPDS_2:def 17
[12,<*a1,a2,a3,a4*>];
correctness
coherence
[12,<*c6,c7,c8,c9*>] is Instruction of SCMPDS ;
proof end;
func c1,c3 := c2,c4 -> Instruction of SCMPDS equals :: SCMPDS_2:def 18
[13,<*a1,a2,a3,a4*>];
correctness
coherence
[13,<*c6,c7,c8,c9*>] is Instruction of SCMPDS ;
proof end;
end;

:: deftheorem Def14 defines AddTo SCMPDS_2:def 14 :
for b1, b2 being Int_position
for b3, b4 being Integer holds AddTo b1,b3,b2,b4 = [9,<*b1,b2,b3,b4*>];

:: deftheorem Def15 defines SubFrom SCMPDS_2:def 15 :
for b1, b2 being Int_position
for b3, b4 being Integer holds SubFrom b1,b3,b2,b4 = [10,<*b1,b2,b3,b4*>];

:: deftheorem Def16 defines MultBy SCMPDS_2:def 16 :
for b1, b2 being Int_position
for b3, b4 being Integer holds MultBy b1,b3,b2,b4 = [11,<*b1,b2,b3,b4*>];

:: deftheorem Def17 defines Divide SCMPDS_2:def 17 :
for b1, b2 being Int_position
for b3, b4 being Integer holds Divide b1,b3,b2,b4 = [12,<*b1,b2,b3,b4*>];

:: deftheorem Def18 defines := SCMPDS_2:def 18 :
for b1, b2 being Int_position
for b3, b4 being Integer holds b1,b3 := b2,b4 = [13,<*b1,b2,b3,b4*>];

theorem Th21: :: SCMPDS_2:21
for b1 being Integer holds InsCode (goto b1) = 0
proof end;

theorem Th22: :: SCMPDS_2:22
for b1 being Int_position holds InsCode (return b1) = 1
proof end;

theorem Th23: :: SCMPDS_2:23
for b1 being Integer
for b2 being Int_position holds InsCode (b2 := b1) = 2
proof end;

theorem Th24: :: SCMPDS_2:24
for b1 being Integer
for b2 being Int_position holds InsCode (saveIC b2,b1) = 3
proof end;

theorem Th25: :: SCMPDS_2:25
for b1, b2 being Integer
for b3 being Int_position holds InsCode (b3,b1 <>0_goto b2) = 4
proof end;

theorem Th26: :: SCMPDS_2:26
for b1, b2 being Integer
for b3 being Int_position holds InsCode (b3,b1 <=0_goto b2) = 5
proof end;

theorem Th27: :: SCMPDS_2:27
for b1, b2 being Integer
for b3 being Int_position holds InsCode (b3,b1 >=0_goto b2) = 6
proof end;

theorem Th28: :: SCMPDS_2:28
for b1, b2 being Integer
for b3 being Int_position holds InsCode (b3,b1 := b2) = 7
proof end;

theorem Th29: :: SCMPDS_2:29
for b1, b2 being Integer
for b3 being Int_position holds InsCode (AddTo b3,b1,b2) = 8
proof end;

theorem Th30: :: SCMPDS_2:30
for b1, b2 being Integer
for b3, b4 being Int_position holds InsCode (AddTo b3,b1,b4,b2) = 9
proof end;

theorem Th31: :: SCMPDS_2:31
for b1, b2 being Integer
for b3, b4 being Int_position holds InsCode (SubFrom b3,b1,b4,b2) = 10
proof end;

theorem Th32: :: SCMPDS_2:32
for b1, b2 being Integer
for b3, b4 being Int_position holds InsCode (MultBy b3,b1,b4,b2) = 11
proof end;

theorem Th33: :: SCMPDS_2:33
for b1, b2 being Integer
for b3, b4 being Int_position holds InsCode (Divide b3,b1,b4,b2) = 12
proof end;

theorem Th34: :: SCMPDS_2:34
for b1, b2 being Integer
for b3, b4 being Int_position holds InsCode (b3,b1 := b4,b2) = 13
proof end;

Lemma14: for b1 being Instruction of SCMPDS st b1 in { [0,<*b2*>] where B is Element of INT : verum } holds
InsCode b1 = 0
proof end;

Lemma15: for b1 being Instruction of SCMPDS st b1 in { [1,<*b2*>] where B is Element of SCM-Data-Loc : verum } holds
InsCode b1 = 1
proof end;

Lemma16: for b1 being Instruction of SCMPDS holds
( not b1 in { [b2,<*b3,b4*>] where B is Element of Segm 14, B is Element of SCM-Data-Loc , B is Element of INT : b2 in {2,3} } or InsCode b1 = 2 or InsCode b1 = 3 )
proof end;

Lemma17: for b1 being Instruction of SCMPDS holds
( not b1 in { [b2,<*b3,b4,b5*>] where B is Element of Segm 14, B is Element of SCM-Data-Loc , B is Element of INT , B is Element of INT : b2 in {4,5,6,7,8} } or InsCode b1 = 4 or InsCode b1 = 5 or InsCode b1 = 6 or InsCode b1 = 7 or InsCode b1 = 8 )
proof end;

Lemma18: for b1 being Instruction of SCMPDS holds
( not b1 in { [b2,<*b3,b4,b5,b6*>] where B is Element of Segm 14, B is Element of SCM-Data-Loc , B is Element of SCM-Data-Loc , B is Element of INT , B is Element of INT : b2 in {9,10,11,12,13} } or InsCode b1 = 9 or InsCode b1 = 10 or InsCode b1 = 11 or InsCode b1 = 12 or InsCode b1 = 13 )
proof end;

theorem Th35: :: SCMPDS_2:35
for b1 being Instruction of SCMPDS st InsCode b1 = 0 holds
ex b2 being Integer st b1 = goto b2
proof end;

theorem Th36: :: SCMPDS_2:36
for b1 being Instruction of SCMPDS st InsCode b1 = 1 holds
ex b2 being Int_position st b1 = return b2
proof end;

theorem Th37: :: SCMPDS_2:37
for b1 being Instruction of SCMPDS st InsCode b1 = 2 holds
ex b2 being Int_position ex b3 being Integer st b1 = b2 := b3
proof end;

theorem Th38: :: SCMPDS_2:38
for b1 being Instruction of SCMPDS st InsCode b1 = 3 holds
ex b2 being Int_position ex b3 being Integer st b1 = saveIC b2,b3
proof end;

Lemma19: for b1 being Instruction of SCMPDS holds
( ( not b1 in { [0,<*b2*>] where B is Element of INT : verum } & not b1 in { [1,<*b2*>] where B is Element of SCM-Data-Loc : verum } & not b1 in { [b2,<*b3,b4*>] where B is Element of Segm 14, B is Element of SCM-Data-Loc , B is Element of INT : b2 in {2,3} } & not b1 in { [b2,<*b3,b4,b5,b6*>] where B is Element of Segm 14, B is Element of SCM-Data-Loc , B is Element of SCM-Data-Loc , B is Element of INT , B is Element of INT : b2 in {9,10,11,12,13} } ) or InsCode b1 = 0 or InsCode b1 = 1 or InsCode b1 = 2 or InsCode b1 = 3 or InsCode b1 = 9 or InsCode b1 = 10 or InsCode b1 = 11 or InsCode b1 = 12 or InsCode b1 = 13 )
proof end;

theorem Th39: :: SCMPDS_2:39
for b1 being Instruction of SCMPDS st InsCode b1 = 4 holds
ex b2 being Int_position ex b3, b4 being Integer st b1 = b2,b3 <>0_goto b4
proof end;

theorem Th40: :: SCMPDS_2:40
for b1 being Instruction of SCMPDS st InsCode b1 = 5 holds
ex b2 being Int_position ex b3, b4 being Integer st b1 = b2,b3 <=0_goto b4
proof end;

theorem Th41: :: SCMPDS_2:41
for b1 being Instruction of SCMPDS st InsCode b1 = 6 holds
ex b2 being Int_position ex b3, b4 being Integer st b1 = b2,b3 >=0_goto b4
proof end;

theorem Th42: :: SCMPDS_2:42
for b1 being Instruction of SCMPDS st InsCode b1 = 7 holds
ex b2 being Int_position ex b3, b4 being Integer st b1 = b2,b3 := b4
proof end;

theorem Th43: :: SCMPDS_2:43
for b1 being Instruction of SCMPDS st InsCode b1 = 8 holds
ex b2 being Int_position ex b3, b4 being Integer st b1 = AddTo b2,b3,b4
proof end;

Lemma20: for b1 being Instruction of SCMPDS holds
( ( not b1 in { [0,<*b2*>] where B is Element of INT : verum } & not b1 in { [1,<*b2*>] where B is Element of SCM-Data-Loc : verum } & not b1 in { [b2,<*b3,b4*>] where B is Element of Segm 14, B is Element of SCM-Data-Loc , B is Element of INT : b2 in {2,3} } & not b1 in { [b2,<*b3,b4,b5*>] where B is Element of Segm 14, B is Element of SCM-Data-Loc , B is Element of INT , B is Element of INT : b2 in {4,5,6,7,8} } ) or InsCode b1 = 0 or InsCode b1 = 1 or InsCode b1 = 2 or InsCode b1 = 3 or InsCode b1 = 4 or InsCode b1 = 5 or InsCode b1 = 6 or InsCode b1 = 7 or InsCode b1 = 8 )
proof end;

theorem Th44: :: SCMPDS_2:44
for b1 being Instruction of SCMPDS st InsCode b1 = 9 holds
ex b2, b3 being Int_position ex b4, b5 being Integer st b1 = AddTo b2,b4,b3,b5
proof end;

theorem Th45: :: SCMPDS_2:45
for b1 being Instruction of SCMPDS st InsCode b1 = 10 holds
ex b2, b3 being Int_position ex b4, b5 being Integer st b1 = SubFrom b2,b4,b3,b5
proof end;

theorem Th46: :: SCMPDS_2:46
for b1 being Instruction of SCMPDS st InsCode b1 = 11 holds
ex b2, b3 being Int_position ex b4, b5 being Integer st b1 = MultBy b2,b4,b3,b5
proof end;

theorem Th47: :: SCMPDS_2:47
for b1 being Instruction of SCMPDS st InsCode b1 = 12 holds
ex b2, b3 being Int_position ex b4, b5 being Integer st b1 = Divide b2,b4,b3,b5
proof end;

theorem Th48: :: SCMPDS_2:48
for b1 being Instruction of SCMPDS st InsCode b1 = 13 holds
ex b2, b3 being Int_position ex b4, b5 being Integer st b1 = b2,b4 := b3,b5
proof end;

theorem Th49: :: SCMPDS_2:49
for b1 being State of SCMPDS
for b2 being Int_position holds b2 in dom b1
proof end;

theorem Th50: :: SCMPDS_2:50
for b1 being State of SCMPDS holds SCM-Data-Loc c= dom b1
proof end;

theorem Th51: :: SCMPDS_2:51
for b1 being State of SCMPDS holds dom (b1 | SCM-Data-Loc ) = SCM-Data-Loc
proof end;

theorem Th52: :: SCMPDS_2:52
for b1 being Int_position holds b1 <> IC SCMPDS
proof end;

theorem Th53: :: SCMPDS_2:53
for b1 being Instruction-Location of SCMPDS
for b2 being Int_position holds b1 <> b2
proof end;

theorem Th54: :: SCMPDS_2:54
for b1, b2 being State of SCMPDS st IC b1 = IC b2 & ( for b3 being Int_position holds b1 . b3 = b2 . b3 ) & ( for b3 being Instruction-Location of SCMPDS holds b1 . b3 = b2 . b3 ) holds
b1 = b2
proof end;

definition
let c6 be Instruction-Location of SCMPDS ;
func Next c1 -> Instruction-Location of SCMPDS means :Def19: :: SCMPDS_2:def 19
ex b1 being Element of SCM-Instr-Loc st
( b1 = a1 & a2 = Next b1 );
existence
ex b1 being Instruction-Location of SCMPDS ex b2 being Element of SCM-Instr-Loc st
( b2 = c6 & b1 = Next b2 )
proof end;
correctness
uniqueness
for b1, b2 being Instruction-Location of SCMPDS st ex b3 being Element of SCM-Instr-Loc st
( b3 = c6 & b1 = Next b3 ) & ex b3 being Element of SCM-Instr-Loc st
( b3 = c6 & b2 = Next b3 ) holds
b1 = b2;
;
end;

:: deftheorem Def19 defines Next SCMPDS_2:def 19 :
for b1, b2 being Instruction-Location of SCMPDS holds
( b2 = Next b1 iff ex b3 being Element of SCM-Instr-Loc st
( b3 = b1 & b2 = Next b3 ) );

theorem Th55: :: SCMPDS_2:55
for b1 being Instruction-Location of SCMPDS
for b2 being Element of SCM-Instr-Loc st b2 = b1 holds
Next b2 = Next b1 by Def19;

theorem Th56: :: SCMPDS_2:56
for b1 being State of SCMPDS
for b2 being Instruction of SCMPDS
for b3 being Element of SCMPDS-Instr st b3 = b2 holds
for b4 being SCMPDS-State st b4 = b1 holds
Exec b2,b1 = SCM-Exec-Res b3,b4 by SCMPDS_1:def 25;

theorem Th57: :: SCMPDS_2:57
for b1 being State of SCMPDS
for b2 being Integer
for b3 being Int_position holds
( (Exec (b3 := b2),b1) . (IC SCMPDS ) = Next (IC b1) & (Exec (b3 := b2),b1) . b3 = b2 & ( for b4 being Int_position st b4 <> b3 holds
(Exec (b3 := b2),b1) . b4 = b1 . b4 ) )
proof end;

theorem Th58: :: SCMPDS_2:58
for b1 being State of SCMPDS
for b2, b3 being Integer
for b4 being Int_position holds
( (Exec (b4,b2 := b3),b1) . (IC SCMPDS ) = Next (IC b1) & (Exec (b4,b2 := b3),b1) . (DataLoc (b1 . b4),b2) = b3 & ( for b5 being Int_position st b5 <> DataLoc (b1 . b4),b2 holds
(Exec (b4,b2 := b3),b1) . b5 = b1 . b5 ) )
proof end;

theorem Th59: :: SCMPDS_2:59
for b1 being State of SCMPDS
for b2, b3 being Integer
for b4, b5 being Int_position holds
( (Exec (b4,b2 := b5,b3),b1) . (IC SCMPDS ) = Next (IC b1) & (Exec (b4,b2 := b5,b3),b1) . (DataLoc (b1 . b4),b2) = b1 . (DataLoc (b1 . b5),b3) & ( for b6 being Int_position st b6 <> DataLoc (b1 . b4),b2 holds
(Exec (b4,b2 := b5,b3),b1) . b6 = b1 . b6 ) )
proof end;

theorem Th60: :: SCMPDS_2:60
for b1 being State of SCMPDS
for b2, b3 being Integer
for b4 being Int_position holds
( (Exec (AddTo b4,b2,b3),b1) . (IC SCMPDS ) = Next (IC b1) & (Exec (AddTo b4,b2,b3),b1) . (DataLoc (b1 . b4),b2) = (b1 . (DataLoc (b1 . b4),b2)) + b3 & ( for b5 being Int_position st b5 <> DataLoc (b1 . b4),b2 holds
(Exec (AddTo b4,b2,b3),b1) . b5 = b1 . b5 ) )
proof end;

theorem Th61: :: SCMPDS_2:61
for b1 being State of SCMPDS
for b2, b3 being Integer
for b4, b5 being Int_position holds
( (Exec (AddTo b4,b2,b5,b3),b1) . (IC SCMPDS ) = Next (IC b1) & (Exec (AddTo b4,b2,b5,b3),b1) . (DataLoc (b1 . b4),b2) = (b1 . (DataLoc (b1 . b4),b2)) + (b1 . (DataLoc (b1 . b5),b3)) & ( for b6 being Int_position st b6 <> DataLoc (b1 . b4),b2 holds
(Exec (AddTo b4,b2,b5,b3),b1) . b6 = b1 . b6 ) )
proof end;

theorem Th62: :: SCMPDS_2:62
for b1 being State of SCMPDS
for b2, b3 being Integer
for b4, b5 being Int_position holds
( (Exec (SubFrom b4,b2,b5,b3),b1) . (IC SCMPDS ) = Next (IC b1) & (Exec (SubFrom b4,b2,b5,b3),b1) . (DataLoc (b1 . b4),b2) = (b1 . (DataLoc (b1 . b4),b2)) - (b1 . (DataLoc (b1 . b5),b3)) & ( for b6 being Int_position st b6 <> DataLoc (b1 . b4),b2 holds
(Exec (SubFrom b4,b2,b5,b3),b1) . b6 = b1 . b6 ) )
proof end;

theorem Th63: :: SCMPDS_2:63
for b1 being State of SCMPDS
for b2, b3 being Integer
for b4, b5 being Int_position holds
( (Exec (MultBy b4,b2,b5,b3),b1) . (IC SCMPDS ) = Next (IC b1) & (Exec (MultBy b4,b2,b5,b3),b1) . (DataLoc (b1 . b4),b2) = (b1 . (DataLoc (b1 . b4),b2)) * (b1 . (DataLoc (b1 . b5),b3)) & ( for b6 being Int_position st b6 <> DataLoc (b1 . b4),b2 holds
(Exec (MultBy b4,b2,b5,b3),b1) . b6 = b1 . b6 ) )
proof end;

theorem Th64: :: SCMPDS_2:64
for b1 being State of SCMPDS
for b2, b3 being Integer
for b4, b5 being Int_position holds
( (Exec (Divide b4,b2,b5,b3),b1) . (IC SCMPDS ) = Next (IC b1) & ( DataLoc (b1 . b4),b2 <> DataLoc (b1 . b5),b3 implies (Exec (Divide b4,b2,b5,b3),b1) . (DataLoc (b1 . b4),b2) = (b1 . (DataLoc (b1 . b4),b2)) div (b1 . (DataLoc (b1 . b5),b3)) ) & (Exec (Divide b4,b2,b5,b3),b1) . (DataLoc (b1 . b5),b3) = (b1 . (DataLoc (b1 . b4),b2)) mod (b1 . (DataLoc (b1 . b5),b3)) & ( for b6 being Int_position st b6 <> DataLoc (b1 . b4),b2 & b6 <> DataLoc (b1 . b5),b3 holds
(Exec (Divide b4,b2,b5,b3),b1) . b6 = b1 . b6 ) )
proof end;

theorem Th65: :: SCMPDS_2:65
for b1 being State of SCMPDS
for b2 being Integer
for b3 being Int_position holds
( (Exec (Divide b3,b2,b3,b2),b1) . (IC SCMPDS ) = Next (IC b1) & (Exec (Divide b3,b2,b3,b2),b1) . (DataLoc (b1 . b3),b2) = (b1 . (DataLoc (b1 . b3),b2)) mod (b1 . (DataLoc (b1 . b3),b2)) & ( for b4 being Int_position st b4 <> DataLoc (b1 . b3),b2 holds
(Exec (Divide b3,b2,b3,b2),b1) . b4 = b1 . b4 ) ) by Th64;

definition
let c6 be State of SCMPDS ;
let c7 be Integer;
func ICplusConst c1,c2 -> Instruction-Location of SCMPDS means :Def20: :: SCMPDS_2:def 20
ex b1 being Nat st
( b1 = IC a1 & a3 = (abs ((b1 - 2) + (2 * a2))) + 2 );
existence
ex b1 being Instruction-Location of SCMPDS ex b2 being Nat st
( b2 = IC c6 & b1 = (abs ((b2 - 2) + (2 * c7))) + 2 )
proof end;
correctness
uniqueness
for b1, b2 being Instruction-Location of SCMPDS st ex b3 being Nat st
( b3 = IC c6 & b1 = (abs ((b3 - 2) + (2 * c7))) + 2 ) & ex b3 being Nat st
( b3 = IC c6 & b2 = (abs ((b3 - 2) + (2 * c7))) + 2 ) holds
b1 = b2;
;
end;

:: deftheorem Def20 defines ICplusConst SCMPDS_2:def 20 :
for b1 being State of SCMPDS
for b2 being Integer
for b3 being Instruction-Location of SCMPDS holds
( b3 = ICplusConst b1,b2 iff ex b4 being Nat st
( b4 = IC b1 & b3 = (abs ((b4 - 2) + (2 * b2))) + 2 ) );

theorem Th66: :: SCMPDS_2:66
for b1 being State of SCMPDS
for b2 being Integer holds
( (Exec (goto b2),b1) . (IC SCMPDS ) = ICplusConst b1,b2 & ( for b3 being Int_position holds (Exec (goto b2),b1) . b3 = b1 . b3 ) )
proof end;

theorem Th67: :: SCMPDS_2:67
for b1 being State of SCMPDS
for b2, b3 being Integer
for b4, b5 being Int_position holds
( ( b1 . (DataLoc (b1 . b4),b2) <> 0 implies (Exec (b4,b2 <>0_goto b3),b1) . (IC SCMPDS ) = ICplusConst b1,b3 ) & ( b1 . (DataLoc (b1 . b4),b2) = 0 implies (Exec (b4,b2 <>0_goto b3),b1) . (IC SCMPDS ) = Next (IC b1) ) & (Exec (b4,b2 <>0_goto b3),b1) . b5 = b1 . b5 )
proof end;

theorem Th68: :: SCMPDS_2:68
for b1 being State of SCMPDS
for b2, b3 being Integer
for b4, b5 being Int_position holds
( ( b1 . (DataLoc (b1 . b4),b2) <= 0 implies (Exec (b4,b2 <=0_goto b3),b1) . (IC SCMPDS ) = ICplusConst b1,b3 ) & ( b1 . (DataLoc (b1 . b4),b2) > 0 implies (Exec (b4,b2 <=0_goto b3),b1) . (IC SCMPDS ) = Next (IC b1) ) & (Exec (b4,b2 <=0_goto b3),b1) . b5 = b1 . b5 )
proof end;

theorem Th69: :: SCMPDS_2:69
for b1 being State of SCMPDS
for b2, b3 being Integer
for b4, b5 being Int_position holds
( ( b1 . (DataLoc (b1 . b4),b2) >= 0 implies (Exec (b4,b2 >=0_goto b3),b1) . (IC SCMPDS ) = ICplusConst b1,b3 ) & ( b1 . (DataLoc (b1 . b4),b2) < 0 implies (Exec (b4,b2 >=0_goto b3),b1) . (IC SCMPDS ) = Next (IC b1) ) & (Exec (b4,b2 >=0_goto b3),b1) . b5 = b1 . b5 )
proof end;

theorem Th70: :: SCMPDS_2:70
for b1 being State of SCMPDS
for b2 being Int_position holds
( (Exec (return b2),b1) . (IC SCMPDS ) = (2 * ((abs (b1 . (DataLoc (b1 . b2),RetIC ))) div 2)) + 4 & (Exec (return b2),b1) . b2 = b1 . (DataLoc (b1 . b2),RetSP ) & ( for b3 being Int_position st b2 <> b3 holds
(Exec (return b2),b1) . b3 = b1 . b3 ) )
proof end;

theorem Th71: :: SCMPDS_2:71
for b1 being State of SCMPDS
for b2 being Integer
for b3 being Int_position holds
( (Exec (saveIC b3,b2),b1) . (IC SCMPDS ) = Next (IC b1) & (Exec (saveIC b3,b2),b1) . (DataLoc (b1 . b3),b2) = IC b1 & ( for b4 being Int_position st DataLoc (b1 . b3),b2 <> b4 holds
(Exec (saveIC b3,b2),b1) . b4 = b1 . b4 ) )
proof end;

theorem Th72: :: SCMPDS_2:72
for b1 being Integer ex b2 being Function of SCM-Data-Loc , INT st
for b3 being Element of SCM-Data-Loc holds b2 . b3 = b1
proof end;

theorem Th73: :: SCMPDS_2:73
for b1 being Integer ex b2 being State of SCMPDS st
for b3 being Int_position holds b2 . b3 = b1
proof end;

theorem Th74: :: SCMPDS_2:74
for b1 being Integer
for b2 being Instruction-Location of SCMPDS ex b3 being State of SCMPDS st
( b3 . 0 = b2 & ( for b4 being Int_position holds b3 . b4 = b1 ) )
proof end;

theorem Th75: :: SCMPDS_2:75
goto 0 is halting
proof end;

theorem Th76: :: SCMPDS_2:76
for b1 being Instruction of SCMPDS st ex b2 being State of SCMPDS st (Exec b1,b2) . (IC SCMPDS ) = Next (IC b2) holds
not b1 is halting
proof end;

theorem Th77: :: SCMPDS_2:77
for b1 being Integer
for b2 being Int_position holds not b2 := b1 is halting
proof end;

theorem Th78: :: SCMPDS_2:78
for b1, b2 being Integer
for b3 being Int_position holds not b3,b1 := b2 is halting
proof end;

theorem Th79: :: SCMPDS_2:79
for b1, b2 being Integer
for b3, b4 being Int_position holds not b3,b1 := b4,b2 is halting
proof end;

theorem Th80: :: SCMPDS_2:80
for b1, b2 being Integer
for b3 being Int_position holds not AddTo b3,b1,b2 is halting
proof end;

theorem Th81: :: SCMPDS_2:81
for b1, b2 being Integer
for b3, b4 being Int_position holds not AddTo b3,b1,b4,b2 is halting
proof end;

theorem Th82: :: SCMPDS_2:82
for b1, b2 being Integer
for b3, b4 being Int_position holds not SubFrom b3,b1,b4,b2 is halting
proof end;

theorem Th83: :: SCMPDS_2:83
for b1, b2 being Integer
for b3, b4 being Int_position holds not MultBy b3,b1,b4,b2 is halting
proof end;

theorem Th84: :: SCMPDS_2:84
for b1, b2 being Integer
for b3, b4 being Int_position holds not Divide b3,b1,b4,b2 is halting
proof end;

theorem Th85: :: SCMPDS_2:85
for b1 being Integer st b1 <> 0 holds
not goto b1 is halting
proof end;

theorem Th86: :: SCMPDS_2:86
for b1, b2 being Integer
for b3 being Int_position holds not b3,b1 <>0_goto b2 is halting
proof end;

theorem Th87: :: SCMPDS_2:87
for b1, b2 being Integer
for b3 being Int_position holds not b3,b1 <=0_goto b2 is halting
proof end;

theorem Th88: :: SCMPDS_2:88
for b1, b2 being Integer
for b3 being Int_position holds not b3,b1 >=0_goto b2 is halting
proof end;

theorem Th89: :: SCMPDS_2:89
for b1 being Int_position holds not return b1 is halting
proof end;

theorem Th90: :: SCMPDS_2:90
for b1 being Integer
for b2 being Int_position holds not saveIC b2,b1 is halting
proof end;

theorem Th91: :: SCMPDS_2:91
for b1 being set holds
( b1 is Instruction of SCMPDS iff ( ex b2 being Integer st b1 = goto b2 or ex b2 being Int_position st b1 = return b2 or ex b2 being Int_position ex b3 being Integer st b1 = saveIC b2,b3 or ex b2 being Int_position ex b3 being Integer st b1 = b2 := b3 or ex b2 being Int_position ex b3, b4 being Integer st b1 = b2,b3 := b4 or ex b2 being Int_position ex b3, b4 being Integer st b1 = b2,b3 <>0_goto b4 or ex b2 being Int_position ex b3, b4 being Integer st b1 = b2,b3 <=0_goto b4 or ex b2 being Int_position ex b3, b4 being Integer st b1 = b2,b3 >=0_goto b4 or ex b2, b3 being Int_position ex b4, b5 being Integer st b1 = AddTo b2,b4,b5 or ex b2, b3 being Int_position ex b4, b5 being Integer st b1 = AddTo b2,b4,b3,b5 or ex b2, b3 being Int_position ex b4, b5 being Integer st b1 = SubFrom b2,b4,b3,b5 or ex b2, b3 being Int_position ex b4, b5 being Integer st b1 = MultBy b2,b4,b3,b5 or ex b2, b3 being Int_position ex b4, b5 being Integer st b1 = Divide b2,b4,b3,b5 or ex b2, b3 being Int_position ex b4, b5 being Integer st b1 = b2,b4 := b3,b5 ) )
proof end;

registration
cluster SCMPDS -> non empty strict non void halting IC-Ins-separated data-oriented definite ;
coherence
SCMPDS is halting
proof end;
end;

theorem Th92: :: SCMPDS_2:92
for b1 being Instruction of SCMPDS st b1 is halting holds
b1 = halt SCMPDS
proof end;

theorem Th93: :: SCMPDS_2:93
halt SCMPDS = goto 0 by Th75, Th92;

theorem Th94: :: SCMPDS_2:94
canceled;

theorem Th95: :: SCMPDS_2:95
canceled;

theorem Th96: :: SCMPDS_2:96
for b1 being State of SCMPDS
for b2 being Instruction of SCMPDS
for b3 being Instruction-Location of SCMPDS holds (Exec b2,b1) . b3 = b1 . b3
proof end;

theorem Th97: :: SCMPDS_2:97
SCMPDS is realistic by AMI_1:def 21, SCMPDS_1:17;

registration
cluster SCMPDS -> non empty strict non void halting IC-Ins-separated data-oriented steady-programmed definite realistic ;
coherence
( SCMPDS is steady-programmed & SCMPDS is realistic )
proof end;
end;

theorem Th98: :: SCMPDS_2:98
for b1 being Nat holds
( IC SCMPDS <> dl. b1 & IC SCMPDS <> il. b1 )
proof end;

theorem Th99: :: SCMPDS_2:99
for b1 being Instruction of SCMPDS st b1 = goto 0 holds
b1 is halting by Th75;