:: SCMPDS_2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set holds
( ex k being Nat st x = (2 * k) + 2 iff x in SCM-Instr-Loc )
proof end;

theorem Th2: :: SCMPDS_2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
SCMPDS is data-oriented
proof end;

theorem Th3: :: SCMPDS_2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 :: SCMPDS_2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
NAT = ({0} \/ SCM-Data-Loc ) \/ SCM-Instr-Loc
proof end;

theorem :: SCMPDS_2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
IC SCMPDS = 0 ;

theorem Th7: :: SCMPDS_2:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCMPDS
for S being SCMPDS-State st S = s holds
IC s = IC S by SCMPDS_1:def 5;

definition
mode Int_position -> Object of SCMPDS means :Def2: :: SCMPDS_2:def 2
it 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 :: SCMPDS_2:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: SCMPDS_2:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set st x in SCM-Data-Loc holds
x is Int_position by Def2;

theorem :: SCMPDS_2:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
SCM-Data-Loc misses the Instruction-Locations of SCMPDS by AMI_5:33;

theorem :: SCMPDS_2:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
not the Instruction-Locations of SCMPDS is finite by AMI_3:def 1, AMI_5:32;

theorem :: SCMPDS_2:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being Int_position holds I is Data-Location
proof end;

theorem Th13: :: SCMPDS_2:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for l being Int_position holds ObjectKind l = INT
proof end;

theorem :: SCMPDS_2:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set st x in SCM-Instr-Loc holds
x is Instruction-Location of SCMPDS ;

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

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

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

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

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

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

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

theorem :: SCMPDS_2:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being Instruction of SCMPDS holds InsCode I <= 13
proof end;

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

definition
let m, n be Integer;
canceled;
func DataLoc m,n -> Int_position equals :: SCMPDS_2:def 4
(2 * (abs (m + n))) + 1;
coherence
(2 * (abs (m + n))) + 1 is Int_position
proof end;
end;

:: deftheorem SCMPDS_2:def 3 :
canceled;

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

theorem Th16: :: SCMPDS_2:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k1 being Integer holds [0,<*k1*>] in SCMPDS-Instr
proof end;

theorem Th17: :: SCMPDS_2:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for d1 being Element of SCM-Data-Loc holds [1,<*d1*>] in SCMPDS-Instr
proof end;

theorem Th18: :: SCMPDS_2:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for d2 being Element of SCM-Data-Loc
for k2 being Integer st x in {2,3} holds
[x,<*d2,k2*>] in SCMPDS-Instr
proof end;

theorem Th19: :: SCMPDS_2:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for d3 being Element of SCM-Data-Loc
for k3, k4 being Integer st x in {4,5,6,7,8} holds
[x,<*d3,k3,k4*>] in SCMPDS-Instr
proof end;

theorem Th20: :: SCMPDS_2:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for d4, d5 being Element of SCM-Data-Loc
for k5, k6 being Integer st x in {9,10,11,12,13} holds
[x,<*d4,d5,k5,k6*>] in SCMPDS-Instr
proof end;

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

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

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

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

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

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

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

definition
let a be Int_position ;
let k1, k2 be Integer;
func a,k1 <>0_goto k2 -> Instruction of SCMPDS equals :: SCMPDS_2:def 9
[4,<*a,k1,k2*>];
correctness
coherence
[4,<*a,k1,k2*>] is Instruction of SCMPDS ;
proof end;
func a,k1 <=0_goto k2 -> Instruction of SCMPDS equals :: SCMPDS_2:def 10
[5,<*a,k1,k2*>];
correctness
coherence
[5,<*a,k1,k2*>] is Instruction of SCMPDS ;
proof end;
func a,k1 >=0_goto k2 -> Instruction of SCMPDS equals :: SCMPDS_2:def 11
[6,<*a,k1,k2*>];
correctness
coherence
[6,<*a,k1,k2*>] is Instruction of SCMPDS ;
proof end;
func a,k1 := k2 -> Instruction of SCMPDS equals :: SCMPDS_2:def 12
[7,<*a,k1,k2*>];
correctness
coherence
[7,<*a,k1,k2*>] is Instruction of SCMPDS ;
proof end;
func AddTo a,k1,k2 -> Instruction of SCMPDS equals :: SCMPDS_2:def 13
[8,<*a,k1,k2*>];
correctness
coherence
[8,<*a,k1,k2*>] is Instruction of SCMPDS ;
proof end;
end;

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

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

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

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

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

definition
let a, b be Int_position ;
let k1, k2 be Integer;
func AddTo a,k1,b,k2 -> Instruction of SCMPDS equals :: SCMPDS_2:def 14
[9,<*a,b,k1,k2*>];
correctness
coherence
[9,<*a,b,k1,k2*>] is Instruction of SCMPDS ;
proof end;
func SubFrom a,k1,b,k2 -> Instruction of SCMPDS equals :: SCMPDS_2:def 15
[10,<*a,b,k1,k2*>];
correctness
coherence
[10,<*a,b,k1,k2*>] is Instruction of SCMPDS ;
proof end;
func MultBy a,k1,b,k2 -> Instruction of SCMPDS equals :: SCMPDS_2:def 16
[11,<*a,b,k1,k2*>];
correctness
coherence
[11,<*a,b,k1,k2*>] is Instruction of SCMPDS ;
proof end;
func Divide a,k1,b,k2 -> Instruction of SCMPDS equals :: SCMPDS_2:def 17
[12,<*a,b,k1,k2*>];
correctness
coherence
[12,<*a,b,k1,k2*>] is Instruction of SCMPDS ;
proof end;
func a,k1 := b,k2 -> Instruction of SCMPDS equals :: SCMPDS_2:def 18
[13,<*a,b,k1,k2*>];
correctness
coherence
[13,<*a,b,k1,k2*>] is Instruction of SCMPDS ;
proof end;
end;

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

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

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

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

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

theorem :: SCMPDS_2:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k1 being Integer holds InsCode (goto k1) = 0
proof end;

theorem :: SCMPDS_2:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Int_position holds InsCode (return a) = 1
proof end;

theorem :: SCMPDS_2:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k1 being Integer
for a being Int_position holds InsCode (a := k1) = 2
proof end;

theorem :: SCMPDS_2:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k1 being Integer
for a being Int_position holds InsCode (saveIC a,k1) = 3
proof end;

theorem :: SCMPDS_2:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k1, k2 being Integer
for a being Int_position holds InsCode (a,k1 <>0_goto k2) = 4
proof end;

theorem :: SCMPDS_2:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k1, k2 being Integer
for a being Int_position holds InsCode (a,k1 <=0_goto k2) = 5
proof end;

theorem :: SCMPDS_2:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k1, k2 being Integer
for a being Int_position holds InsCode (a,k1 >=0_goto k2) = 6
proof end;

theorem :: SCMPDS_2:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k1, k2 being Integer
for a being Int_position holds InsCode (a,k1 := k2) = 7
proof end;

theorem :: SCMPDS_2:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k1, k2 being Integer
for a being Int_position holds InsCode (AddTo a,k1,k2) = 8
proof end;

theorem :: SCMPDS_2:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k1, k2 being Integer
for a, b being Int_position holds InsCode (AddTo a,k1,b,k2) = 9
proof end;

theorem :: SCMPDS_2:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k1, k2 being Integer
for a, b being Int_position holds InsCode (SubFrom a,k1,b,k2) = 10
proof end;

theorem :: SCMPDS_2:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k1, k2 being Integer
for a, b being Int_position holds InsCode (MultBy a,k1,b,k2) = 11
proof end;

theorem :: SCMPDS_2:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k1, k2 being Integer
for a, b being Int_position holds InsCode (Divide a,k1,b,k2) = 12
proof end;

theorem :: SCMPDS_2:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k1, k2 being Integer
for a, b being Int_position holds InsCode (a,k1 := b,k2) = 13
proof end;

Lm2: for I being Instruction of SCMPDS st I in { [0,<*k1*>] where k1 is Element of INT : verum } holds
InsCode I = 0
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 14, d1 is Element of SCM-Data-Loc , k1 is Element of INT : I1 in {2,3} } or InsCode I = 2 or InsCode I = 3 )
proof end;

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

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

theorem :: SCMPDS_2:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for ins being Instruction of SCMPDS st InsCode ins = 0 holds
ex k1 being Integer st ins = goto k1
proof end;

theorem :: SCMPDS_2:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for ins being Instruction of SCMPDS st InsCode ins = 1 holds
ex a being Int_position st ins = return a
proof end;

theorem :: SCMPDS_2:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for ins being Instruction of SCMPDS st InsCode ins = 2 holds
ex a being Int_position ex k1 being Integer st ins = a := k1
proof end;

theorem :: SCMPDS_2:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

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

theorem :: SCMPDS_2:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for ins being Instruction of SCMPDS st InsCode ins = 4 holds
ex a being Int_position ex k1, k2 being Integer st ins = a,k1 <>0_goto k2
proof end;

theorem :: SCMPDS_2:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for ins being Instruction of SCMPDS st InsCode ins = 5 holds
ex a being Int_position ex k1, k2 being Integer st ins = a,k1 <=0_goto k2
proof end;

theorem :: SCMPDS_2:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for ins being Instruction of SCMPDS st InsCode ins = 6 holds
ex a being Int_position ex k1, k2 being Integer st ins = a,k1 >=0_goto k2
proof end;

theorem :: SCMPDS_2:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for ins being Instruction of SCMPDS st InsCode ins = 7 holds
ex a being Int_position ex k1, k2 being Integer st ins = a,k1 := k2
proof end;

theorem :: SCMPDS_2:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

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

theorem :: SCMPDS_2:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for ins being Instruction of SCMPDS st InsCode ins = 9 holds
ex a, b being Int_position ex k1, k2 being Integer st ins = AddTo a,k1,b,k2
proof end;

theorem :: SCMPDS_2:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for ins being Instruction of SCMPDS st InsCode ins = 10 holds
ex a, b being Int_position ex k1, k2 being Integer st ins = SubFrom a,k1,b,k2
proof end;

theorem :: SCMPDS_2:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for ins being Instruction of SCMPDS st InsCode ins = 11 holds
ex a, b being Int_position ex k1, k2 being Integer st ins = MultBy a,k1,b,k2
proof end;

theorem :: SCMPDS_2:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for ins being Instruction of SCMPDS st InsCode ins = 12 holds
ex a, b being Int_position ex k1, k2 being Integer st ins = Divide a,k1,b,k2
proof end;

theorem :: SCMPDS_2:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for ins being Instruction of SCMPDS st InsCode ins = 13 holds
ex a, b being Int_position ex k1, k2 being Integer st ins = a,k1 := b,k2
proof end;

theorem :: SCMPDS_2:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCMPDS
for d being Int_position holds d in dom s
proof end;

theorem Th50: :: SCMPDS_2:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCMPDS holds SCM-Data-Loc c= dom s
proof end;

theorem :: SCMPDS_2:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCMPDS holds dom (s | SCM-Data-Loc ) = SCM-Data-Loc
proof end;

theorem :: SCMPDS_2:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for dl being Int_position holds dl <> IC SCMPDS
proof end;

theorem :: SCMPDS_2:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for il being Instruction-Location of SCMPDS
for dl being Int_position holds il <> dl
proof end;

theorem :: SCMPDS_2:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s1, s2 being State of SCMPDS st IC s1 = IC s2 & ( for a being Int_position holds s1 . a = s2 . a ) & ( for i being Instruction-Location of SCMPDS holds s1 . i = s2 . i ) holds
s1 = s2
proof end;

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

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

theorem Th55: :: SCMPDS_2:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for loc being Instruction-Location of SCMPDS
for mj being Element of SCM-Instr-Loc st mj = loc holds
Next mj = Next loc by Def19;

theorem Th56: :: SCMPDS_2:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCMPDS
for I being Instruction of SCMPDS
for i being Element of SCMPDS-Instr st i = I holds
for S being SCMPDS-State st S = s holds
Exec I,s = SCM-Exec-Res i,S by SCMPDS_1:def 25;

theorem Th57: :: SCMPDS_2:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCMPDS
for k1 being Integer
for a being Int_position holds
( (Exec (a := k1),s) . (IC SCMPDS ) = Next (IC s) & (Exec (a := k1),s) . a = k1 & ( for b being Int_position st b <> a holds
(Exec (a := k1),s) . b = s . b ) )
proof end;

theorem Th58: :: SCMPDS_2:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCMPDS
for k1, k2 being Integer
for a being Int_position holds
( (Exec (a,k1 := k2),s) . (IC SCMPDS ) = Next (IC s) & (Exec (a,k1 := k2),s) . (DataLoc (s . a),k1) = k2 & ( for b being Int_position st b <> DataLoc (s . a),k1 holds
(Exec (a,k1 := k2),s) . b = s . b ) )
proof end;

theorem Th59: :: SCMPDS_2:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 SCMPDS ) = Next (IC s) & (Exec (a,k1 := b,k2),s) . (DataLoc (s . a),k1) = s . (DataLoc (s . b),k2) & ( for c being Int_position st c <> DataLoc (s . a),k1 holds
(Exec (a,k1 := b,k2),s) . c = s . c ) )
proof end;

theorem Th60: :: SCMPDS_2:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCMPDS
for k1, k2 being Integer
for a being Int_position holds
( (Exec (AddTo a,k1,k2),s) . (IC SCMPDS ) = Next (IC s) & (Exec (AddTo a,k1,k2),s) . (DataLoc (s . a),k1) = (s . (DataLoc (s . a),k1)) + k2 & ( for b being Int_position st b <> DataLoc (s . a),k1 holds
(Exec (AddTo a,k1,k2),s) . b = s . b ) )
proof end;

theorem Th61: :: SCMPDS_2:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 SCMPDS ) = Next (IC s) & (Exec (AddTo a,k1,b,k2),s) . (DataLoc (s . a),k1) = (s . (DataLoc (s . a),k1)) + (s . (DataLoc (s . b),k2)) & ( for c being Int_position st c <> DataLoc (s . a),k1 holds
(Exec (AddTo a,k1,b,k2),s) . c = s . c ) )
proof end;

theorem Th62: :: SCMPDS_2:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 SCMPDS ) = Next (IC s) & (Exec (SubFrom a,k1,b,k2),s) . (DataLoc (s . a),k1) = (s . (DataLoc (s . a),k1)) - (s . (DataLoc (s . b),k2)) & ( for c being Int_position st c <> DataLoc (s . a),k1 holds
(Exec (SubFrom a,k1,b,k2),s) . c = s . c ) )
proof end;

theorem Th63: :: SCMPDS_2:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 SCMPDS ) = Next (IC s) & (Exec (MultBy a,k1,b,k2),s) . (DataLoc (s . a),k1) = (s . (DataLoc (s . a),k1)) * (s . (DataLoc (s . b),k2)) & ( for c being Int_position st c <> DataLoc (s . a),k1 holds
(Exec (MultBy a,k1,b,k2),s) . c = s . c ) )
proof end;

theorem Th64: :: SCMPDS_2:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 SCMPDS ) = Next (IC s) & ( DataLoc (s . a),k1 <> DataLoc (s . b),k2 implies (Exec (Divide a,k1,b,k2),s) . (DataLoc (s . a),k1) = (s . (DataLoc (s . a),k1)) div (s . (DataLoc (s . b),k2)) ) & (Exec (Divide a,k1,b,k2),s) . (DataLoc (s . b),k2) = (s . (DataLoc (s . a),k1)) mod (s . (DataLoc (s . b),k2)) & ( for c being Int_position st c <> DataLoc (s . a),k1 & c <> DataLoc (s . b),k2 holds
(Exec (Divide a,k1,b,k2),s) . c = s . c ) )
proof end;

theorem :: SCMPDS_2:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCMPDS
for k1 being Integer
for a being Int_position holds
( (Exec (Divide a,k1,a,k1),s) . (IC SCMPDS ) = Next (IC s) & (Exec (Divide a,k1,a,k1),s) . (DataLoc (s . a),k1) = (s . (DataLoc (s . a),k1)) mod (s . (DataLoc (s . a),k1)) & ( for c being Int_position st c <> DataLoc (s . a),k1 holds
(Exec (Divide a,k1,a,k1),s) . c = s . c ) ) by Th64;

definition
let s be State of SCMPDS ;
let c be Integer;
func ICplusConst s,c -> Instruction-Location of SCMPDS means :Def20: :: SCMPDS_2:def 20
 ex m being Nat st
( m = IC s & it = (abs ((m - 2) + (2 * c))) + 2 );
existence
ex b1 being Instruction-Location of SCMPDS ex m being Nat st
( m = IC s & b1 = (abs ((m - 2) + (2 * c))) + 2 )
proof end;
correctness
uniqueness
for b1, b2 being Instruction-Location of SCMPDS st ex m being Nat st
( m = IC s & b1 = (abs ((m - 2) + (2 * c))) + 2 ) & ex m being Nat st
( m = IC s & b2 = (abs ((m - 2) + (2 * c))) + 2 ) holds
b1 = b2;
;
end;

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

theorem Th66: :: SCMPDS_2:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCMPDS
for k1 being Integer holds
( (Exec (goto k1),s) . (IC SCMPDS ) = ICplusConst s,k1 & ( for a being Int_position holds (Exec (goto k1),s) . a = s . a ) )
proof end;

theorem Th67: :: SCMPDS_2:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 SCMPDS ) = ICplusConst s,k2 ) & ( s . (DataLoc (s . a),k1) = 0 implies (Exec (a,k1 <>0_goto k2),s) . (IC SCMPDS ) = Next (IC s) ) & (Exec (a,k1 <>0_goto k2),s) . b = s . b )
proof end;

theorem Th68: :: SCMPDS_2:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 SCMPDS ) = ICplusConst s,k2 ) & ( s . (DataLoc (s . a),k1) > 0 implies (Exec (a,k1 <=0_goto k2),s) . (IC SCMPDS ) = Next (IC s) ) & (Exec (a,k1 <=0_goto k2),s) . b = s . b )
proof end;

theorem Th69: :: SCMPDS_2:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 SCMPDS ) = ICplusConst s,k2 ) & ( s . (DataLoc (s . a),k1) < 0 implies (Exec (a,k1 >=0_goto k2),s) . (IC SCMPDS ) = Next (IC s) ) & (Exec (a,k1 >=0_goto k2),s) . b = s . b )
proof end;

theorem Th70: :: SCMPDS_2:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCMPDS
for a being Int_position holds
( (Exec (return a),s) . (IC SCMPDS ) = (2 * ((abs (s . (DataLoc (s . a),RetIC ))) div 2)) + 4 & (Exec (return a),s) . a = s . (DataLoc (s . a),RetSP ) & ( for b being Int_position st a <> b holds
(Exec (return a),s) . b = s . b ) )
proof end;

theorem Th71: :: SCMPDS_2:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCMPDS
for k1 being Integer
for a being Int_position holds
( (Exec (saveIC a,k1),s) . (IC SCMPDS ) = Next (IC s) & (Exec (saveIC a,k1),s) . (DataLoc (s . a),k1) = IC s & ( for b being Int_position st DataLoc (s . a),k1 <> b holds
(Exec (saveIC a,k1),s) . b = s . b ) )
proof end;

theorem Th72: :: SCMPDS_2:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Integer ex f being Function of SCM-Data-Loc , INT st
for x being Element of SCM-Data-Loc holds f . x = k
proof end;

theorem Th73: :: SCMPDS_2:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Integer ex s being State of SCMPDS st
for d being Int_position holds s . d = k
proof end;

theorem Th74: :: SCMPDS_2:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Integer
for loc being Instruction-Location of SCMPDS ex s being State of SCMPDS st
( s . 0 = loc & ( for d being Int_position holds s . d = k ) )
proof end;

theorem Th75: :: SCMPDS_2:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
goto 0 is halting
proof end;

theorem Th76: :: SCMPDS_2:76  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being Instruction of SCMPDS st ex s being State of SCMPDS st (Exec I,s) . (IC SCMPDS ) = Next (IC s) holds
not I is halting
proof end;

theorem Th77: :: SCMPDS_2:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k1 being Integer
for a being Int_position holds not a := k1 is halting
proof end;

theorem Th78: :: SCMPDS_2:78  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k1, k2 being Integer
for a being Int_position holds not a,k1 := k2 is halting
proof end;

theorem Th79: :: SCMPDS_2:79  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k1, k2 being Integer
for a, b being Int_position holds not a,k1 := b,k2 is halting
proof end;

theorem Th80: :: SCMPDS_2:80  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k1, k2 being Integer
for a being Int_position holds not AddTo a,k1,k2 is halting
proof end;

theorem Th81: :: SCMPDS_2:81  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k1, k2 being Integer
for a, b being Int_position holds not AddTo a,k1,b,k2 is halting
proof end;

theorem Th82: :: SCMPDS_2:82  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k1, k2 being Integer
for a, b being Int_position holds not SubFrom a,k1,b,k2 is halting
proof end;

theorem Th83: :: SCMPDS_2:83  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k1, k2 being Integer
for a, b being Int_position holds not MultBy a,k1,b,k2 is halting
proof end;

theorem Th84: :: SCMPDS_2:84  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k1, k2 being Integer
for a, b being Int_position holds not Divide a,k1,b,k2 is halting
proof end;

theorem Th85: :: SCMPDS_2:85  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k1 being Integer st k1 <> 0 holds
not goto k1 is halting
proof end;

theorem Th86: :: SCMPDS_2:86  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k1, k2 being Integer
for a being Int_position holds not a,k1 <>0_goto k2 is halting
proof end;

theorem Th87: :: SCMPDS_2:87  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k1, k2 being Integer
for a being Int_position holds not a,k1 <=0_goto k2 is halting
proof end;

theorem Th88: :: SCMPDS_2:88  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k1, k2 being Integer
for a being Int_position holds not a,k1 >=0_goto k2 is halting
proof end;

theorem Th89: :: SCMPDS_2:89  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Int_position holds not return a is halting
proof end;

theorem Th90: :: SCMPDS_2:90  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k1 being Integer
for a being Int_position holds not saveIC a,k1 is halting
proof end;

theorem Th91: :: SCMPDS_2:91  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set holds
( I is Instruction of SCMPDS iff ( 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;

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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being Instruction of SCMPDS st I is halting holds
I = halt SCMPDS
proof end;

theorem :: SCMPDS_2:93  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
halt SCMPDS = goto 0 by Th75, Th92;

theorem :: SCMPDS_2:94  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: SCMPDS_2:95  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th96: :: SCMPDS_2:96  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCMPDS
for i being Instruction of SCMPDS
for l being Instruction-Location of SCMPDS holds (Exec i,s) . l = s . l
proof end;

theorem :: SCMPDS_2:97  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 :: SCMPDS_2:98  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat holds
( IC SCMPDS <> dl. i & IC SCMPDS <> il. i )
proof end;

theorem :: SCMPDS_2:99  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being Instruction of SCMPDS st I = goto 0 holds
I is halting by Th75;