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

definition
let x1, x2, x3, x4 be set ;
func <*x1,x2,x3,x4*> -> set equals :: SCMPDS_1:def 1
<*x1,x2,x3*> ^ <*x4*>;
correctness
coherence
<*x1,x2,x3*> ^ <*x4*> is set ;
;
let x5 be set ;
func <*x1,x2,x3,x4,x5*> -> set equals :: SCMPDS_1:def 2
<*x1,x2,x3*> ^ <*x4,x5*>;
correctness
coherence
<*x1,x2,x3*> ^ <*x4,x5*> is set ;
;
end;

:: deftheorem defines <* SCMPDS_1:def 1 :
for x1, x2, x3, x4 being set holds <*x1,x2,x3,x4*> = <*x1,x2,x3*> ^ <*x4*>;

:: deftheorem defines <* SCMPDS_1:def 2 :
for x1, x2, x3, x4, x5 being set holds <*x1,x2,x3,x4,x5*> = <*x1,x2,x3*> ^ <*x4,x5*>;

registration
let x1, x2, x3, x4 be set ;
cluster <*x1,x2,x3,x4*> -> Relation-like Function-like ;
coherence
( <*x1,x2,x3,x4*> is Function-like & <*x1,x2,x3,x4*> is Relation-like ) ;
let x5 be set ;
cluster <*x1,x2,x3,x4,x5*> -> Relation-like Function-like ;
coherence
( <*x1,x2,x3,x4,x5*> is Function-like & <*x1,x2,x3,x4,x5*> is Relation-like ) ;
end;

registration
let x1, x2, x3, x4 be set ;
cluster <*x1,x2,x3,x4*> -> Relation-like Function-like FinSequence-like ;
coherence
<*x1,x2,x3,x4*> is FinSequence-like ;
let x5 be set ;
cluster <*x1,x2,x3,x4,x5*> -> Relation-like Function-like FinSequence-like ;
coherence
<*x1,x2,x3,x4,x5*> is FinSequence-like ;
end;

definition
let D be non empty set ;
let x1, x2, x3, x4 be Element of D;
:: original: <*
redefine func <*x1,x2,x3,x4*> -> FinSequence of D;
coherence
<*x1,x2,x3,x4*> is FinSequence of D
proof end;
end;

definition
let D be non empty set ;
let x1, x2, x3, x4, x5 be Element of D;
:: original: <*
redefine func <*x1,x2,x3,x4,x5*> -> FinSequence of D;
coherence
<*x1,x2,x3,x4,x5*> is FinSequence of D
proof end;
end;

theorem Th1: :: SCMPDS_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2, x3, x4 being set holds
( <*x1,x2,x3,x4*> = <*x1,x2,x3*> ^ <*x4*> & <*x1,x2,x3,x4*> = <*x1,x2*> ^ <*x3,x4*> & <*x1,x2,x3,x4*> = <*x1*> ^ <*x2,x3,x4*> & <*x1,x2,x3,x4*> = ((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*> )
proof end;

theorem Th2: :: SCMPDS_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2, x3, x4, x5 being set holds
( <*x1,x2,x3,x4,x5*> = <*x1,x2,x3*> ^ <*x4,x5*> & <*x1,x2,x3,x4,x5*> = <*x1,x2,x3,x4*> ^ <*x5*> & <*x1,x2,x3,x4,x5*> = (((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*> & <*x1,x2,x3,x4,x5*> = <*x1,x2*> ^ <*x3,x4,x5*> & <*x1,x2,x3,x4,x5*> = <*x1*> ^ <*x2,x3,x4,x5*> )
proof end;

theorem Th3: :: SCMPDS_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2, x3, x4 being set
for p being FinSequence holds
( p = <*x1,x2,x3,x4*> iff ( len p = 4 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 ) )
proof end;

theorem Th4: :: SCMPDS_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2, x3, x4 being set holds dom <*x1,x2,x3,x4*> = Seg 4
proof end;

theorem Th5: :: SCMPDS_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2, x3, x4, x5 being set
for p being FinSequence holds
( p = <*x1,x2,x3,x4,x5*> iff ( len p = 5 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 ) )
proof end;

theorem Th6: :: SCMPDS_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2, x3, x4, x5 being set holds dom <*x1,x2,x3,x4,x5*> = Seg 5
proof end;

theorem Th7: :: SCMPDS_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for ND being non empty set
for y1, y2, y3, y4 being Element of ND holds
( <*y1,y2,y3,y4*> /. 1 = y1 & <*y1,y2,y3,y4*> /. 2 = y2 & <*y1,y2,y3,y4*> /. 3 = y3 & <*y1,y2,y3,y4*> /. 4 = y4 )
proof end;

theorem :: SCMPDS_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for ND being non empty set
for y1, y2, y3, y4, y5 being Element of ND holds
( <*y1,y2,y3,y4,y5*> /. 1 = y1 & <*y1,y2,y3,y4,y5*> /. 2 = y2 & <*y1,y2,y3,y4,y5*> /. 3 = y3 & <*y1,y2,y3,y4,y5*> /. 4 = y4 & <*y1,y2,y3,y4,y5*> /. 5 = y5 )
proof end;

theorem Th9: :: SCMPDS_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Integer holds k in (union {INT }) \/ NAT
proof end;

theorem Th10: :: SCMPDS_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Integer holds k in SCM-Data-Loc \/ INT
proof end;

theorem Th11: :: SCMPDS_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for d being Element of SCM-Data-Loc holds d in SCM-Data-Loc \/ INT
proof end;

definition
func SCMPDS-Instr -> Subset of [:(Segm 14),(((union {INT }) \/ NAT ) * ):] equals :: SCMPDS_1:def 3
((({ [0,<*l*>] where l is Element of INT : verum } \/ { [1,<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) \/ { [I,<*v,c*>] where I is Element of Segm 14, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ) \/ { [I,<*v,c1,c2*>] where I is Element of Segm 14, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } ) \/ { [I,<*v1,v2,c1,c2*>] where I is Element of Segm 14, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } ;
coherence
((({ [0,<*l*>] where l is Element of INT : verum } \/ { [1,<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) \/ { [I,<*v,c*>] where I is Element of Segm 14, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ) \/ { [I,<*v,c1,c2*>] where I is Element of Segm 14, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } ) \/ { [I,<*v1,v2,c1,c2*>] where I is Element of Segm 14, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } is Subset of [:(Segm 14),(((union {INT }) \/ NAT ) * ):]
proof end;
end;

:: deftheorem defines SCMPDS-Instr SCMPDS_1:def 3 :
SCMPDS-Instr = ((({ [0,<*l*>] where l is Element of INT : verum } \/ { [1,<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) \/ { [I,<*v,c*>] where I is Element of Segm 14, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ) \/ { [I,<*v,c1,c2*>] where I is Element of Segm 14, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } ) \/ { [I,<*v1,v2,c1,c2*>] where I is Element of Segm 14, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } ;

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

theorem Th13: :: SCMPDS_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
[0,<*0*>] in SCMPDS-Instr
proof end;

registration
cluster SCMPDS-Instr -> non empty ;
coherence
not SCMPDS-Instr is empty by Th13;
end;

theorem Th14: :: SCMPDS_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat holds
( k = 0 or ex j being Nat st k = (2 * j) + 1 or ex j being Nat st k = (2 * j) + 2 )
proof end;

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

theorem Th16: :: SCMPDS_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat holds
( ( ex j being Nat st k = (2 * j) + 1 implies ( k <> 0 & ( for j being Nat holds not k = (2 * j) + 2 ) ) ) & ( ex j being Nat st k = (2 * j) + 2 implies ( k <> 0 & ( for j being Nat holds not k = (2 * j) + 1 ) ) ) )
proof end;

definition
func SCMPDS-OK -> Function of NAT ,{INT } \/ {SCMPDS-Instr ,SCM-Instr-Loc } means :Def4: :: SCMPDS_1:def 4
( it . 0 = SCM-Instr-Loc & ( for k being Nat holds
( it . ((2 * k) + 1) = INT & it . ((2 * k) + 2) = SCMPDS-Instr ) ) );
existence
ex b1 being Function of NAT ,{INT } \/ {SCMPDS-Instr ,SCM-Instr-Loc } st
( b1 . 0 = SCM-Instr-Loc & ( for k being Nat holds
( b1 . ((2 * k) + 1) = INT & b1 . ((2 * k) + 2) = SCMPDS-Instr ) ) )
proof end;
uniqueness
for b1, b2 being Function of NAT ,{INT } \/ {SCMPDS-Instr ,SCM-Instr-Loc } st b1 . 0 = SCM-Instr-Loc & ( for k being Nat holds
( b1 . ((2 * k) + 1) = INT & b1 . ((2 * k) + 2) = SCMPDS-Instr ) ) & b2 . 0 = SCM-Instr-Loc & ( for k being Nat holds
( b2 . ((2 * k) + 1) = INT & b2 . ((2 * k) + 2) = SCMPDS-Instr ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines SCMPDS-OK SCMPDS_1:def 4 :
for b1 being Function of NAT ,{INT } \/ {SCMPDS-Instr ,SCM-Instr-Loc } holds
( b1 = SCMPDS-OK iff ( b1 . 0 = SCM-Instr-Loc & ( for k being Nat holds
( b1 . ((2 * k) + 1) = INT & b1 . ((2 * k) + 2) = SCMPDS-Instr ) ) ) );

definition
mode SCMPDS-State is Element of product SCMPDS-OK ;
end;

theorem Th17: :: SCMPDS_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( SCM-Instr-Loc <> SCMPDS-Instr & SCMPDS-Instr <> INT )
proof end;

theorem Th18: :: SCMPDS_1:18  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
( SCMPDS-OK . i = SCM-Instr-Loc iff i = 0 )
proof end;

theorem Th19: :: SCMPDS_1:19  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
( SCMPDS-OK . i = INT iff ex k being Nat st i = (2 * k) + 1 )
proof end;

theorem Th20: :: SCMPDS_1:20  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
( SCMPDS-OK . i = SCMPDS-Instr iff ex k being Nat st i = (2 * k) + 2 )
proof end;

theorem Th21: :: SCMPDS_1:21  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 SCMPDS-OK . d1 = INT
proof end;

theorem Th22: :: SCMPDS_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i1 being Element of SCM-Instr-Loc holds SCMPDS-OK . i1 = SCMPDS-Instr
proof end;

theorem Th23: :: SCMPDS_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
pi (product SCMPDS-OK ),0 = SCM-Instr-Loc
proof end;

theorem Th24: :: SCMPDS_1:24  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 pi (product SCMPDS-OK ),d1 = INT
proof end;

theorem :: SCMPDS_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i1 being Element of SCM-Instr-Loc holds pi (product SCMPDS-OK ),i1 = SCMPDS-Instr
proof end;

definition
let s be SCMPDS-State;
func IC s -> Element of SCM-Instr-Loc equals :: SCMPDS_1:def 5
s . 0;
coherence
s . 0 is Element of SCM-Instr-Loc by Th23, CARD_3:def 6;
end;

:: deftheorem defines IC SCMPDS_1:def 5 :
for s being SCMPDS-State holds IC s = s . 0;

definition
let s be SCMPDS-State;
let u be Element of SCM-Instr-Loc ;
func SCM-Chg s,u -> SCMPDS-State equals :: SCMPDS_1:def 6
s +* (0 .--> u);
coherence
s +* (0 .--> u) is SCMPDS-State
proof end;
end;

:: deftheorem defines SCM-Chg SCMPDS_1:def 6 :
for s being SCMPDS-State
for u being Element of SCM-Instr-Loc holds SCM-Chg s,u = s +* (0 .--> u);

theorem :: SCMPDS_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being SCMPDS-State
for u being Element of SCM-Instr-Loc holds (SCM-Chg s,u) . 0 = u
proof end;

theorem :: SCMPDS_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being SCMPDS-State
for u being Element of SCM-Instr-Loc
for mk being Element of SCM-Data-Loc holds (SCM-Chg s,u) . mk = s . mk
proof end;

theorem :: SCMPDS_1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being SCMPDS-State
for u, v being Element of SCM-Instr-Loc holds (SCM-Chg s,u) . v = s . v
proof end;

definition
let s be SCMPDS-State;
let t be Element of SCM-Data-Loc ;
let u be Integer;
func SCM-Chg s,t,u -> SCMPDS-State equals :: SCMPDS_1:def 7
s +* (t .--> u);
coherence
s +* (t .--> u) is SCMPDS-State
proof end;
end;

:: deftheorem defines SCM-Chg SCMPDS_1:def 7 :
for s being SCMPDS-State
for t being Element of SCM-Data-Loc
for u being Integer holds SCM-Chg s,t,u = s +* (t .--> u);

theorem :: SCMPDS_1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being SCMPDS-State
for t being Element of SCM-Data-Loc
for u being Integer holds (SCM-Chg s,t,u) . 0 = s . 0
proof end;

theorem :: SCMPDS_1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being SCMPDS-State
for t being Element of SCM-Data-Loc
for u being Integer holds (SCM-Chg s,t,u) . t = u
proof end;

theorem :: SCMPDS_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being SCMPDS-State
for t being Element of SCM-Data-Loc
for u being Integer
for mk being Element of SCM-Data-Loc st mk <> t holds
(SCM-Chg s,t,u) . mk = s . mk
proof end;

theorem :: SCMPDS_1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being SCMPDS-State
for t being Element of SCM-Data-Loc
for u being Integer
for v being Element of SCM-Instr-Loc holds (SCM-Chg s,t,u) . v = s . v
proof end;

definition
let s be SCMPDS-State;
let a be Element of SCM-Data-Loc ;
:: original: .
redefine func s . a -> Integer;
coherence
s . a is Integer
proof end;
end;

definition
let s be SCMPDS-State;
let a be Element of SCM-Data-Loc ;
let n be Integer;
func Address_Add s,a,n -> Element of SCM-Data-Loc equals :: SCMPDS_1:def 8
(2 * (abs ((s . a) + n))) + 1;
coherence
(2 * (abs ((s . a) + n))) + 1 is Element of SCM-Data-Loc
proof end;
end;

:: deftheorem defines Address_Add SCMPDS_1:def 8 :
for s being SCMPDS-State
for a being Element of SCM-Data-Loc
for n being Integer holds Address_Add s,a,n = (2 * (abs ((s . a) + n))) + 1;

definition
let s be SCMPDS-State;
let n be Integer;
func jump_address s,n -> Element of SCM-Instr-Loc equals :: SCMPDS_1:def 9
(abs (((IC s) - 2) + (2 * n))) + 2;
coherence
(abs (((IC s) - 2) + (2 * n))) + 2 is Element of SCM-Instr-Loc
proof end;
end;

:: deftheorem defines jump_address SCMPDS_1:def 9 :
for s being SCMPDS-State
for n being Integer holds jump_address s,n = (abs (((IC s) - 2) + (2 * n))) + 2;

definition
let d be Element of SCM-Data-Loc ;
let s be Integer;
:: original: <*
redefine func <*d,s*> -> FinSequence of SCM-Data-Loc \/ INT ;
coherence
<*d,s*> is FinSequence of SCM-Data-Loc \/ INT
proof end;
end;

definition
let x be Element of SCMPDS-Instr ;
given mk being Element of SCM-Data-Loc , I being Element of Segm 14 such that A1: x = [I,<*mk*>] ;
func x address_1 -> Element of SCM-Data-Loc means :Def10: :: SCMPDS_1:def 10
 ex f being FinSequence of SCM-Data-Loc st
( f = x `2 & it = f /. 1 );
existence
ex b1 being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc st
( f = x `2 & b1 = f /. 1 )
proof end;
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc st
( f = x `2 & b1 = f /. 1 ) & ex f being FinSequence of SCM-Data-Loc st
( f = x `2 & b2 = f /. 1 ) holds
b1 = b2 ;
end;

:: deftheorem Def10 defines address_1 SCMPDS_1:def 10 :
for x being Element of SCMPDS-Instr st ex mk being Element of SCM-Data-Loc ex I being Element of Segm 14 st x = [I,<*mk*>] holds
for b2 being Element of SCM-Data-Loc holds
( b2 = x address_1 iff ex f being FinSequence of SCM-Data-Loc st
( f = x `2 & b2 = f /. 1 ) );

theorem :: SCMPDS_1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being Element of Segm 14
for x being Element of SCMPDS-Instr
for mk being Element of SCM-Data-Loc st x = [I,<*mk*>] holds
x address_1 = mk
proof end;

definition
let x be Element of SCMPDS-Instr ;
given r being Integer, I being Element of Segm 14 such that A1: x = [I,<*r*>] ;
func x const_INT -> Integer means :Def11: :: SCMPDS_1:def 11
 ex f being FinSequence of INT st
( f = x `2 & it = f /. 1 );
existence
ex b1 being Integer ex f being FinSequence of INT st
( f = x `2 & b1 = f /. 1 )
proof end;
uniqueness
for b1, b2 being Integer st ex f being FinSequence of INT st
( f = x `2 & b1 = f /. 1 ) & ex f being FinSequence of INT st
( f = x `2 & b2 = f /. 1 ) holds
b1 = b2 ;
end;

:: deftheorem Def11 defines const_INT SCMPDS_1:def 11 :
for x being Element of SCMPDS-Instr st ex r being Integer ex I being Element of Segm 14 st x = [I,<*r*>] holds
for b2 being Integer holds
( b2 = x const_INT iff ex f being FinSequence of INT st
( f = x `2 & b2 = f /. 1 ) );

theorem :: SCMPDS_1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being Element of Segm 14
for x being Element of SCMPDS-Instr
for k being Integer st x = [I,<*k*>] holds
x const_INT = k
proof end;

definition
let x be Element of SCMPDS-Instr ;
given mk being Element of SCM-Data-Loc , r being Integer, I being Element of Segm 14 such that A1: x = [I,<*mk,r*>] ;
func x P21address -> Element of SCM-Data-Loc means :Def12: :: SCMPDS_1:def 12
 ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & it = f /. 1 );
existence
ex b1 being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b1 = f /. 1 )
proof end;
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b1 = f /. 1 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b2 = f /. 1 ) holds
b1 = b2 ;
func x P22const -> Integer means :Def13: :: SCMPDS_1:def 13
 ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & it = f /. 2 );
existence
ex b1 being Integer ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b1 = f /. 2 )
proof end;
uniqueness
for b1, b2 being Integer st ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b1 = f /. 2 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b2 = f /. 2 ) holds
b1 = b2 ;
end;

:: deftheorem Def12 defines P21address SCMPDS_1:def 12 :
for x being Element of SCMPDS-Instr st ex mk being Element of SCM-Data-Loc ex r being Integer ex I being Element of Segm 14 st x = [I,<*mk,r*>] holds
for b2 being Element of SCM-Data-Loc holds
( b2 = x P21address iff ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b2 = f /. 1 ) );

:: deftheorem Def13 defines P22const SCMPDS_1:def 13 :
for x being Element of SCMPDS-Instr st ex mk being Element of SCM-Data-Loc ex r being Integer ex I being Element of Segm 14 st x = [I,<*mk,r*>] holds
for b2 being Integer holds
( b2 = x P22const iff ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b2 = f /. 2 ) );

theorem :: SCMPDS_1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being Element of Segm 14
for x being Element of SCMPDS-Instr
for mk being Element of SCM-Data-Loc
for r being Integer st x = [I,<*mk,r*>] holds
( x P21address = mk & x P22const = r )
proof end;

definition
let x be Element of SCMPDS-Instr ;
given m1 being Element of SCM-Data-Loc , k1, k2 being Integer, I being Element of Segm 14 such that A1: x = [I,<*m1,k1,k2*>] ;
func x P31address -> Element of SCM-Data-Loc means :Def14: :: SCMPDS_1:def 14
 ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & it = f /. 1 );
existence
ex b1 being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b1 = f /. 1 )
proof end;
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b1 = f /. 1 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b2 = f /. 1 ) holds
b1 = b2 ;
func x P32const -> Integer means :Def15: :: SCMPDS_1:def 15
 ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & it = f /. 2 );
existence
ex b1 being Integer ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b1 = f /. 2 )
proof end;
uniqueness
for b1, b2 being Integer st ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b1 = f /. 2 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b2 = f /. 2 ) holds
b1 = b2 ;
func x P33const -> Integer means :Def16: :: SCMPDS_1:def 16
 ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & it = f /. 3 );
existence
ex b1 being Integer ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b1 = f /. 3 )
proof end;
uniqueness
for b1, b2 being Integer st ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b1 = f /. 3 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b2 = f /. 3 ) holds
b1 = b2 ;
end;

:: deftheorem Def14 defines P31address SCMPDS_1:def 14 :
for x being Element of SCMPDS-Instr st ex m1 being Element of SCM-Data-Loc ex k1, k2 being Integer ex I being Element of Segm 14 st x = [I,<*m1,k1,k2*>] holds
for b2 being Element of SCM-Data-Loc holds
( b2 = x P31address iff ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b2 = f /. 1 ) );

:: deftheorem Def15 defines P32const SCMPDS_1:def 15 :
for x being Element of SCMPDS-Instr st ex m1 being Element of SCM-Data-Loc ex k1, k2 being Integer ex I being Element of Segm 14 st x = [I,<*m1,k1,k2*>] holds
for b2 being Integer holds
( b2 = x P32const iff ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b2 = f /. 2 ) );

:: deftheorem Def16 defines P33const SCMPDS_1:def 16 :
for x being Element of SCMPDS-Instr st ex m1 being Element of SCM-Data-Loc ex k1, k2 being Integer ex I being Element of Segm 14 st x = [I,<*m1,k1,k2*>] holds
for b2 being Integer holds
( b2 = x P33const iff ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b2 = f /. 3 ) );

theorem :: SCMPDS_1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being Element of Segm 14
for x being Element of SCMPDS-Instr
for d1 being Element of SCM-Data-Loc
for k1, k2 being Integer st x = [I,<*d1,k1,k2*>] holds
( x P31address = d1 & x P32const = k1 & x P33const = k2 )
proof end;

definition
let x be Element of SCMPDS-Instr ;
given m1, m2 being Element of SCM-Data-Loc , k1, k2 being Integer, I being Element of Segm 14 such that A1: x = [I,<*m1,m2,k1,k2*>] ;
func x P41address -> Element of SCM-Data-Loc means :Def17: :: SCMPDS_1:def 17
 ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & it = f /. 1 );
existence
ex b1 being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b1 = f /. 1 )
proof end;
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b1 = f /. 1 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b2 = f /. 1 ) holds
b1 = b2 ;
func x P42address -> Element of SCM-Data-Loc means :Def18: :: SCMPDS_1:def 18
 ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & it = f /. 2 );
existence
ex b1 being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b1 = f /. 2 )
proof end;
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b1 = f /. 2 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b2 = f /. 2 ) holds
b1 = b2 ;
func x P43const -> Integer means :Def19: :: SCMPDS_1:def 19
 ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & it = f /. 3 );
existence
ex b1 being Integer ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b1 = f /. 3 )
proof end;
uniqueness
for b1, b2 being Integer st ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b1 = f /. 3 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b2 = f /. 3 ) holds
b1 = b2 ;
func x P44const -> Integer means :Def20: :: SCMPDS_1:def 20
 ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & it = f /. 4 );
existence
ex b1 being Integer ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b1 = f /. 4 )
proof end;
uniqueness
for b1, b2 being Integer st ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b1 = f /. 4 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b2 = f /. 4 ) holds
b1 = b2 ;
end;

:: deftheorem Def17 defines P41address SCMPDS_1:def 17 :
for x being Element of SCMPDS-Instr st ex m1, m2 being Element of SCM-Data-Loc ex k1, k2 being Integer ex I being Element of Segm 14 st x = [I,<*m1,m2,k1,k2*>] holds
for b2 being Element of SCM-Data-Loc holds
( b2 = x P41address iff ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b2 = f /. 1 ) );

:: deftheorem Def18 defines P42address SCMPDS_1:def 18 :
for x being Element of SCMPDS-Instr st ex m1, m2 being Element of SCM-Data-Loc ex k1, k2 being Integer ex I being Element of Segm 14 st x = [I,<*m1,m2,k1,k2*>] holds
for b2 being Element of SCM-Data-Loc holds
( b2 = x P42address iff ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b2 = f /. 2 ) );

:: deftheorem Def19 defines P43const SCMPDS_1:def 19 :
for x being Element of SCMPDS-Instr st ex m1, m2 being Element of SCM-Data-Loc ex k1, k2 being Integer ex I being Element of Segm 14 st x = [I,<*m1,m2,k1,k2*>] holds
for b2 being Integer holds
( b2 = x P43const iff ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b2 = f /. 3 ) );

:: deftheorem Def20 defines P44const SCMPDS_1:def 20 :
for x being Element of SCMPDS-Instr st ex m1, m2 being Element of SCM-Data-Loc ex k1, k2 being Integer ex I being Element of Segm 14 st x = [I,<*m1,m2,k1,k2*>] holds
for b2 being Integer holds
( b2 = x P44const iff ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b2 = f /. 4 ) );

theorem :: SCMPDS_1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being Element of Segm 14
for x being Element of SCMPDS-Instr
for d1, d2 being Element of SCM-Data-Loc
for k1, k2 being Integer st x = [I,<*d1,d2,k1,k2*>] holds
( x P41address = d1 & x P42address = d2 & x P43const = k1 & x P44const = k2 )
proof end;

definition
let s be SCMPDS-State;
let a be Element of SCM-Data-Loc ;
func PopInstrLoc s,a -> Element of SCM-Instr-Loc equals :: SCMPDS_1:def 21
(2 * ((abs (s . a)) div 2)) + 4;
coherence
(2 * ((abs (s . a)) div 2)) + 4 is Element of SCM-Instr-Loc
proof end;
end;

:: deftheorem defines PopInstrLoc SCMPDS_1:def 21 :
for s being SCMPDS-State
for a being Element of SCM-Data-Loc holds PopInstrLoc s,a = (2 * ((abs (s . a)) div 2)) + 4;

definition
func RetSP -> Nat equals :: SCMPDS_1:def 22
0;
coherence
0 is Nat ;
func RetIC -> Nat equals :: SCMPDS_1:def 23
1;
coherence
1 is Nat ;
end;

:: deftheorem defines RetSP SCMPDS_1:def 22 :
RetSP = 0;

:: deftheorem defines RetIC SCMPDS_1:def 23 :
RetIC = 1;

definition
let x be Element of SCMPDS-Instr ;
let s be SCMPDS-State;
func SCM-Exec-Res x,s -> SCMPDS-State equals :: SCMPDS_1:def 24
 SCM-Chg s,(jump_address s,(x const_INT )) if ex k1 being Integer st x = [0,<*k1*>]
SCM-Chg (SCM-Chg s,(x P21address ),(x P22const )),(Next (IC s)) if ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [2,<*d1,k1*>]
SCM-Chg (SCM-Chg s,(Address_Add s,(x P21address ),(x P22const )),(IC s)),(Next (IC s)) if ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [3,<*d1,k1*>]
SCM-Chg (SCM-Chg s,(x address_1 ),(s . (Address_Add s,(x address_1 ),RetSP ))),(PopInstrLoc s,(Address_Add s,(x address_1 ),RetIC )) if ex d1 being Element of SCM-Data-Loc st x = [1,<*d1*>]
SCM-Chg s,(IFEQ (s . (Address_Add s,(x P31address ),(x P32const ))),0,(Next (IC s)),(jump_address s,(x P33const ))) if ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [4,<*d1,k1,k2*>]
SCM-Chg s,(IFGT (s . (Address_Add s,(x P31address ),(x P32const ))),0,(Next (IC s)),(jump_address s,(x P33const ))) if ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [5,<*d1,k1,k2*>]
SCM-Chg s,(IFGT 0,(s . (Address_Add s,(x P31address ),(x P32const ))),(Next (IC s)),(jump_address s,(x P33const ))) if ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [6,<*d1,k1,k2*>]
SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),(x P33const )),(Next (IC s)) if ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [7,<*d1,k1,k2*>]
SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),((s . (Address_Add s,(x P31address ),(x P32const ))) + (x P33const ))),(Next (IC s)) if ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [8,<*d1,k1,k2*>]
SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) + (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) if ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [9,<*d1,d2,k1,k2*>]
SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) - (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) if ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [10,<*d1,d2,k1,k2*>]
SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) * (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) if ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [11,<*d1,d2,k1,k2*>]
SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),(s . (Address_Add s,(x P42address ),(x P44const )))),(Next (IC s)) if ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [13,<*d1,d2,k1,k2*>]
SCM-Chg (SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) div (s . (Address_Add s,(x P42address ),(x P44const ))))),(Address_Add s,(x P42address ),(x P44const )),((s . (Address_Add s,(x P41address ),(x P43const ))) mod (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) if ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [12,<*d1,d2,k1,k2*>]
otherwise s;
coherence
( ( ex k1 being Integer st x = [0,<*k1*>] implies SCM-Chg s,(jump_address s,(x const_INT )) is SCMPDS-State ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [2,<*d1,k1*>] implies SCM-Chg (SCM-Chg s,(x P21address ),(x P22const )),(Next (IC s)) is SCMPDS-State ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [3,<*d1,k1*>] implies SCM-Chg (SCM-Chg s,(Address_Add s,(x P21address ),(x P22const )),(IC s)),(Next (IC s)) is SCMPDS-State ) & ( ex d1 being Element of SCM-Data-Loc st x = [1,<*d1*>] implies SCM-Chg (SCM-Chg s,(x address_1 ),(s . (Address_Add s,(x address_1 ),RetSP ))),(PopInstrLoc s,(Address_Add s,(x address_1 ),RetIC )) is SCMPDS-State ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [4,<*d1,k1,k2*>] implies SCM-Chg s,(IFEQ (s . (Address_Add s,(x P31address ),(x P32const ))),0,(Next (IC s)),(jump_address s,(x P33const ))) is SCMPDS-State ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [5,<*d1,k1,k2*>] implies SCM-Chg s,(IFGT (s . (Address_Add s,(x P31address ),(x P32const ))),0,(Next (IC s)),(jump_address s,(x P33const ))) is SCMPDS-State ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [6,<*d1,k1,k2*>] implies SCM-Chg s,(IFGT 0,(s . (Address_Add s,(x P31address ),(x P32const ))),(Next (IC s)),(jump_address s,(x P33const ))) is SCMPDS-State ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [7,<*d1,k1,k2*>] implies SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),(x P33const )),(Next (IC s)) is SCMPDS-State ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [8,<*d1,k1,k2*>] implies SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),((s . (Address_Add s,(x P31address ),(x P32const ))) + (x P33const ))),(Next (IC s)) is SCMPDS-State ) & ( ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [9,<*d1,d2,k1,k2*>] implies SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) + (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) is SCMPDS-State ) & ( ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [10,<*d1,d2,k1,k2*>] implies SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) - (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) is SCMPDS-State ) & ( ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [11,<*d1,d2,k1,k2*>] implies SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) * (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) is SCMPDS-State ) & ( ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [13,<*d1,d2,k1,k2*>] implies SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),(s . (Address_Add s,(x P42address ),(x P44const )))),(Next (IC s)) is SCMPDS-State ) & ( ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [12,<*d1,d2,k1,k2*>] implies SCM-Chg (SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) div (s . (Address_Add s,(x P42address ),(x P44const ))))),(Address_Add s,(x P42address ),(x P44const )),((s . (Address_Add s,(x P41address ),(x P43const ))) mod (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) is SCMPDS-State ) & ( ( for k1 being Integer holds not x = [0,<*k1*>] ) & ( for d1 being Element of SCM-Data-Loc
for k1 being Integer holds not x = [2,<*d1,k1*>] ) & ( for d1 being Element of SCM-Data-Loc
for k1 being Integer holds not x = [3,<*d1,k1*>] ) & ( for d1 being Element of SCM-Data-Loc holds not x = [1,<*d1*>] ) & ( for d1 being Element of SCM-Data-Loc
for k1, k2 being Integer holds not x = [4,<*d1,k1,k2*>] ) & ( for d1 being Element of SCM-Data-Loc
for k1, k2 being Integer holds not x = [5,<*d1,k1,k2*>] ) & ( for d1 being Element of SCM-Data-Loc
for k1, k2 being Integer holds not x = [6,<*d1,k1,k2*>] ) & ( for d1 being Element of SCM-Data-Loc
for k1, k2 being Integer holds not x = [7,<*d1,k1,k2*>] ) & ( for d1 being Element of SCM-Data-Loc
for k1, k2 being Integer holds not x = [8,<*d1,k1,k2*>] ) & ( for d1, d2 being Element of SCM-Data-Loc
for k1, k2 being Integer holds not x = [9,<*d1,d2,k1,k2*>] ) & ( for d1, d2 being Element of SCM-Data-Loc
for k1, k2 being Integer holds not x = [10,<*d1,d2,k1,k2*>] ) & ( for d1, d2 being Element of SCM-Data-Loc
for k1, k2 being Integer holds not x = [11,<*d1,d2,k1,k2*>] ) & ( for d1, d2 being Element of SCM-Data-Loc
for k1, k2 being Integer holds not x = [13,<*d1,d2,k1,k2*>] ) & ( for d1, d2 being Element of SCM-Data-Loc
for k1, k2 being Integer holds not x = [12,<*d1,d2,k1,k2*>] ) implies s is SCMPDS-State ) ) ;
consistency
for b1 being SCMPDS-State holds
( ( ex k1 being Integer st x = [0,<*k1*>] & ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [2,<*d1,k1*>] implies ( b1 = SCM-Chg s,(jump_address s,(x const_INT )) iff b1 = SCM-Chg (SCM-Chg s,(x P21address ),(x P22const )),(Next (IC s)) ) ) & ( ex k1 being Integer st x = [0,<*k1*>] & ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [3,<*d1,k1*>] implies ( b1 = SCM-Chg s,(jump_address s,(x const_INT )) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P21address ),(x P22const )),(IC s)),(Next (IC s)) ) ) & ( ex k1 being Integer st x = [0,<*k1*>] & ex d1 being Element of SCM-Data-Loc st x = [1,<*d1*>] implies ( b1 = SCM-Chg s,(jump_address s,(x const_INT )) iff b1 = SCM-Chg (SCM-Chg s,(x address_1 ),(s . (Address_Add s,(x address_1 ),RetSP ))),(PopInstrLoc s,(Address_Add s,(x address_1 ),RetIC )) ) ) & ( ex k1 being Integer st x = [0,<*k1*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [4,<*d1,k1,k2*>] implies ( b1 = SCM-Chg s,(jump_address s,(x const_INT )) iff b1 = SCM-Chg s,(IFEQ (s . (Address_Add s,(x P31address ),(x P32const ))),0,(Next (IC s)),(jump_address s,(x P33const ))) ) ) & ( ex k1 being Integer st x = [0,<*k1*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [5,<*d1,k1,k2*>] implies ( b1 = SCM-Chg s,(jump_address s,(x const_INT )) iff b1 = SCM-Chg s,(IFGT (s . (Address_Add s,(x P31address ),(x P32const ))),0,(Next (IC s)),(jump_address s,(x P33const ))) ) ) & ( ex k1 being Integer st x = [0,<*k1*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [6,<*d1,k1,k2*>] implies ( b1 = SCM-Chg s,(jump_address s,(x const_INT )) iff b1 = SCM-Chg s,(IFGT 0,(s . (Address_Add s,(x P31address ),(x P32const ))),(Next (IC s)),(jump_address s,(x P33const ))) ) ) & ( ex k1 being Integer st x = [0,<*k1*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [7,<*d1,k1,k2*>] implies ( b1 = SCM-Chg s,(jump_address s,(x const_INT )) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),(x P33const )),(Next (IC s)) ) ) & ( ex k1 being Integer st x = [0,<*k1*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [8,<*d1,k1,k2*>] implies ( b1 = SCM-Chg s,(jump_address s,(x const_INT )) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),((s . (Address_Add s,(x P31address ),(x P32const ))) + (x P33const ))),(Next (IC s)) ) ) & ( ex k1 being Integer st x = [0,<*k1*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [9,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg s,(jump_address s,(x const_INT )) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) + (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) ) & ( ex k1 being Integer st x = [0,<*k1*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [10,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg s,(jump_address s,(x const_INT )) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) - (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) ) & ( ex k1 being Integer st x = [0,<*k1*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [11,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg s,(jump_address s,(x const_INT )) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) * (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) ) & ( ex k1 being Integer st x = [0,<*k1*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [13,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg s,(jump_address s,(x const_INT )) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),(s . (Address_Add s,(x P42address ),(x P44const )))),(Next (IC s)) ) ) & ( ex k1 being Integer st x = [0,<*k1*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [12,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg s,(jump_address s,(x const_INT )) iff b1 = SCM-Chg (SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) div (s . (Address_Add s,(x P42address ),(x P44const ))))),(Address_Add s,(x P42address ),(x P44const )),((s . (Address_Add s,(x P41address ),(x P43const ))) mod (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [2,<*d1,k1*>] & ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [3,<*d1,k1*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x P21address ),(x P22const )),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P21address ),(x P22const )),(IC s)),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [2,<*d1,k1*>] & ex d1 being Element of SCM-Data-Loc st x = [1,<*d1*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x P21address ),(x P22const )),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(x address_1 ),(s . (Address_Add s,(x address_1 ),RetSP ))),(PopInstrLoc s,(Address_Add s,(x address_1 ),RetIC )) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [2,<*d1,k1*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [4,<*d1,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x P21address ),(x P22const )),(Next (IC s)) iff b1 = SCM-Chg s,(IFEQ (s . (Address_Add s,(x P31address ),(x P32const ))),0,(Next (IC s)),(jump_address s,(x P33const ))) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [2,<*d1,k1*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [5,<*d1,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x P21address ),(x P22const )),(Next (IC s)) iff b1 = SCM-Chg s,(IFGT (s . (Address_Add s,(x P31address ),(x P32const ))),0,(Next (IC s)),(jump_address s,(x P33const ))) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [2,<*d1,k1*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [6,<*d1,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x P21address ),(x P22const )),(Next (IC s)) iff b1 = SCM-Chg s,(IFGT 0,(s . (Address_Add s,(x P31address ),(x P32const ))),(Next (IC s)),(jump_address s,(x P33const ))) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [2,<*d1,k1*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [7,<*d1,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x P21address ),(x P22const )),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),(x P33const )),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [2,<*d1,k1*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [8,<*d1,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x P21address ),(x P22const )),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),((s . (Address_Add s,(x P31address ),(x P32const ))) + (x P33const ))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [2,<*d1,k1*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [9,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x P21address ),(x P22const )),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) + (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [2,<*d1,k1*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [10,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x P21address ),(x P22const )),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) - (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [2,<*d1,k1*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [11,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x P21address ),(x P22const )),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) * (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [2,<*d1,k1*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [13,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x P21address ),(x P22const )),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),(s . (Address_Add s,(x P42address ),(x P44const )))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [2,<*d1,k1*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [12,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x P21address ),(x P22const )),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) div (s . (Address_Add s,(x P42address ),(x P44const ))))),(Address_Add s,(x P42address ),(x P44const )),((s . (Address_Add s,(x P41address ),(x P43const ))) mod (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [3,<*d1,k1*>] & ex d1 being Element of SCM-Data-Loc st x = [1,<*d1*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P21address ),(x P22const )),(IC s)),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(x address_1 ),(s . (Address_Add s,(x address_1 ),RetSP ))),(PopInstrLoc s,(Address_Add s,(x address_1 ),RetIC )) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [3,<*d1,k1*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [4,<*d1,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P21address ),(x P22const )),(IC s)),(Next (IC s)) iff b1 = SCM-Chg s,(IFEQ (s . (Address_Add s,(x P31address ),(x P32const ))),0,(Next (IC s)),(jump_address s,(x P33const ))) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [3,<*d1,k1*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [5,<*d1,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P21address ),(x P22const )),(IC s)),(Next (IC s)) iff b1 = SCM-Chg s,(IFGT (s . (Address_Add s,(x P31address ),(x P32const ))),0,(Next (IC s)),(jump_address s,(x P33const ))) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [3,<*d1,k1*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [6,<*d1,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P21address ),(x P22const )),(IC s)),(Next (IC s)) iff b1 = SCM-Chg s,(IFGT 0,(s . (Address_Add s,(x P31address ),(x P32const ))),(Next (IC s)),(jump_address s,(x P33const ))) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [3,<*d1,k1*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [7,<*d1,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P21address ),(x P22const )),(IC s)),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),(x P33const )),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [3,<*d1,k1*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [8,<*d1,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P21address ),(x P22const )),(IC s)),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),((s . (Address_Add s,(x P31address ),(x P32const ))) + (x P33const ))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [3,<*d1,k1*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [9,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P21address ),(x P22const )),(IC s)),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) + (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [3,<*d1,k1*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [10,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P21address ),(x P22const )),(IC s)),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) - (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [3,<*d1,k1*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [11,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P21address ),(x P22const )),(IC s)),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) * (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [3,<*d1,k1*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [13,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P21address ),(x P22const )),(IC s)),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),(s . (Address_Add s,(x P42address ),(x P44const )))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [3,<*d1,k1*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [12,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P21address ),(x P22const )),(IC s)),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) div (s . (Address_Add s,(x P42address ),(x P44const ))))),(Address_Add s,(x P42address ),(x P44const )),((s . (Address_Add s,(x P41address ),(x P43const ))) mod (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc st x = [1,<*d1*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [4,<*d1,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),(s . (Address_Add s,(x address_1 ),RetSP ))),(PopInstrLoc s,(Address_Add s,(x address_1 ),RetIC )) iff b1 = SCM-Chg s,(IFEQ (s . (Address_Add s,(x P31address ),(x P32const ))),0,(Next (IC s)),(jump_address s,(x P33const ))) ) ) & ( ex d1 being Element of SCM-Data-Loc st x = [1,<*d1*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [5,<*d1,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),(s . (Address_Add s,(x address_1 ),RetSP ))),(PopInstrLoc s,(Address_Add s,(x address_1 ),RetIC )) iff b1 = SCM-Chg s,(IFGT (s . (Address_Add s,(x P31address ),(x P32const ))),0,(Next (IC s)),(jump_address s,(x P33const ))) ) ) & ( ex d1 being Element of SCM-Data-Loc st x = [1,<*d1*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [6,<*d1,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),(s . (Address_Add s,(x address_1 ),RetSP ))),(PopInstrLoc s,(Address_Add s,(x address_1 ),RetIC )) iff b1 = SCM-Chg s,(IFGT 0,(s . (Address_Add s,(x P31address ),(x P32const ))),(Next (IC s)),(jump_address s,(x P33const ))) ) ) & ( ex d1 being Element of SCM-Data-Loc st x = [1,<*d1*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [7,<*d1,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),(s . (Address_Add s,(x address_1 ),RetSP ))),(PopInstrLoc s,(Address_Add s,(x address_1 ),RetIC )) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),(x P33const )),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc st x = [1,<*d1*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [8,<*d1,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),(s . (Address_Add s,(x address_1 ),RetSP ))),(PopInstrLoc s,(Address_Add s,(x address_1 ),RetIC )) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),((s . (Address_Add s,(x P31address ),(x P32const ))) + (x P33const ))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc st x = [1,<*d1*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [9,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),(s . (Address_Add s,(x address_1 ),RetSP ))),(PopInstrLoc s,(Address_Add s,(x address_1 ),RetIC )) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) + (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc st x = [1,<*d1*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [10,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),(s . (Address_Add s,(x address_1 ),RetSP ))),(PopInstrLoc s,(Address_Add s,(x address_1 ),RetIC )) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) - (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc st x = [1,<*d1*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [11,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),(s . (Address_Add s,(x address_1 ),RetSP ))),(PopInstrLoc s,(Address_Add s,(x address_1 ),RetIC )) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) * (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc st x = [1,<*d1*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [13,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),(s . (Address_Add s,(x address_1 ),RetSP ))),(PopInstrLoc s,(Address_Add s,(x address_1 ),RetIC )) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),(s . (Address_Add s,(x P42address ),(x P44const )))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc st x = [1,<*d1*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [12,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),(s . (Address_Add s,(x address_1 ),RetSP ))),(PopInstrLoc s,(Address_Add s,(x address_1 ),RetIC )) iff b1 = SCM-Chg (SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) div (s . (Address_Add s,(x P42address ),(x P44const ))))),(Address_Add s,(x P42address ),(x P44const )),((s . (Address_Add s,(x P41address ),(x P43const ))) mod (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [4,<*d1,k1,k2*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [5,<*d1,k1,k2*>] implies ( b1 = SCM-Chg s,(IFEQ (s . (Address_Add s,(x P31address ),(x P32const ))),0,(Next (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg s,(IFGT (s . (Address_Add s,(x P31address ),(x P32const ))),0,(Next (IC s)),(jump_address s,(x P33const ))) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [4,<*d1,k1,k2*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [6,<*d1,k1,k2*>] implies ( b1 = SCM-Chg s,(IFEQ (s . (Address_Add s,(x P31address ),(x P32const ))),0,(Next (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg s,(IFGT 0,(s . (Address_Add s,(x P31address ),(x P32const ))),(Next (IC s)),(jump_address s,(x P33const ))) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [4,<*d1,k1,k2*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [7,<*d1,k1,k2*>] implies ( b1 = SCM-Chg s,(IFEQ (s . (Address_Add s,(x P31address ),(x P32const ))),0,(Next (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),(x P33const )),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [4,<*d1,k1,k2*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [8,<*d1,k1,k2*>] implies ( b1 = SCM-Chg s,(IFEQ (s . (Address_Add s,(x P31address ),(x P32const ))),0,(Next (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),((s . (Address_Add s,(x P31address ),(x P32const ))) + (x P33const ))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [4,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [9,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg s,(IFEQ (s . (Address_Add s,(x P31address ),(x P32const ))),0,(Next (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) + (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [4,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [10,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg s,(IFEQ (s . (Address_Add s,(x P31address ),(x P32const ))),0,(Next (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) - (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [4,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [11,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg s,(IFEQ (s . (Address_Add s,(x P31address ),(x P32const ))),0,(Next (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) * (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [4,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [13,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg s,(IFEQ (s . (Address_Add s,(x P31address ),(x P32const ))),0,(Next (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),(s . (Address_Add s,(x P42address ),(x P44const )))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [4,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [12,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg s,(IFEQ (s . (Address_Add s,(x P31address ),(x P32const ))),0,(Next (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg (SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) div (s . (Address_Add s,(x P42address ),(x P44const ))))),(Address_Add s,(x P42address ),(x P44const )),((s . (Address_Add s,(x P41address ),(x P43const ))) mod (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [5,<*d1,k1,k2*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [6,<*d1,k1,k2*>] implies ( b1 = SCM-Chg s,(IFGT (s . (Address_Add s,(x P31address ),(x P32const ))),0,(Next (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg s,(IFGT 0,(s . (Address_Add s,(x P31address ),(x P32const ))),(Next (IC s)),(jump_address s,(x P33const ))) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [5,<*d1,k1,k2*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [7,<*d1,k1,k2*>] implies ( b1 = SCM-Chg s,(IFGT (s . (Address_Add s,(x P31address ),(x P32const ))),0,(Next (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),(x P33const )),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [5,<*d1,k1,k2*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [8,<*d1,k1,k2*>] implies ( b1 = SCM-Chg s,(IFGT (s . (Address_Add s,(x P31address ),(x P32const ))),0,(Next (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),((s . (Address_Add s,(x P31address ),(x P32const ))) + (x P33const ))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [5,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [9,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg s,(IFGT (s . (Address_Add s,(x P31address ),(x P32const ))),0,(Next (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) + (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [5,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [10,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg s,(IFGT (s . (Address_Add s,(x P31address ),(x P32const ))),0,(Next (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) - (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [5,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [11,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg s,(IFGT (s . (Address_Add s,(x P31address ),(x P32const ))),0,(Next (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) * (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [5,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [13,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg s,(IFGT (s . (Address_Add s,(x P31address ),(x P32const ))),0,(Next (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),(s . (Address_Add s,(x P42address ),(x P44const )))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [5,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [12,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg s,(IFGT (s . (Address_Add s,(x P31address ),(x P32const ))),0,(Next (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg (SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) div (s . (Address_Add s,(x P42address ),(x P44const ))))),(Address_Add s,(x P42address ),(x P44const )),((s . (Address_Add s,(x P41address ),(x P43const ))) mod (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [6,<*d1,k1,k2*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [7,<*d1,k1,k2*>] implies ( b1 = SCM-Chg s,(IFGT 0,(s . (Address_Add s,(x P31address ),(x P32const ))),(Next (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),(x P33const )),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [6,<*d1,k1,k2*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [8,<*d1,k1,k2*>] implies ( b1 = SCM-Chg s,(IFGT 0,(s . (Address_Add s,(x P31address ),(x P32const ))),(Next (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),((s . (Address_Add s,(x P31address ),(x P32const ))) + (x P33const ))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [6,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [9,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg s,(IFGT 0,(s . (Address_Add s,(x P31address ),(x P32const ))),(Next (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) + (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [6,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [10,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg s,(IFGT 0,(s . (Address_Add s,(x P31address ),(x P32const ))),(Next (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) - (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [6,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [11,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg s,(IFGT 0,(s . (Address_Add s,(x P31address ),(x P32const ))),(Next (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) * (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [6,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [13,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg s,(IFGT 0,(s . (Address_Add s,(x P31address ),(x P32const ))),(Next (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),(s . (Address_Add s,(x P42address ),(x P44const )))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [6,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [12,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg s,(IFGT 0,(s . (Address_Add s,(x P31address ),(x P32const ))),(Next (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg (SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) div (s . (Address_Add s,(x P42address ),(x P44const ))))),(Address_Add s,(x P42address ),(x P44const )),((s . (Address_Add s,(x P41address ),(x P43const ))) mod (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [7,<*d1,k1,k2*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [8,<*d1,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),(x P33const )),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),((s . (Address_Add s,(x P31address ),(x P32const ))) + (x P33const ))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [7,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [9,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),(x P33const )),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) + (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [7,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [10,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),(x P33const )),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) - (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [7,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [11,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),(x P33const )),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) * (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [7,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [13,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),(x P33const )),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),(s . (Address_Add s,(x P42address ),(x P44const )))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [7,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [12,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),(x P33const )),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) div (s . (Address_Add s,(x P42address ),(x P44const ))))),(Address_Add s,(x P42address ),(x P44const )),((s . (Address_Add s,(x P41address ),(x P43const ))) mod (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [8,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [9,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),((s . (Address_Add s,(x P31address ),(x P32const ))) + (x P33const ))),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) + (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [8,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [10,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),((s . (Address_Add s,(x P31address ),(x P32const ))) + (x P33const ))),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) - (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [8,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [11,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),((s . (Address_Add s,(x P31address ),(x P32const ))) + (x P33const ))),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) * (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [8,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [13,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),((s . (Address_Add s,(x P31address ),(x P32const ))) + (x P33const ))),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),(s . (Address_Add s,(x P42address ),(x P44const )))),(Next (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [8,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [12,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),((s . (Address_Add s,(x P31address ),(x P32const ))) + (x P33const ))),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) div (s . (Address_Add s,(x P42address ),(x P44const ))))),(Address_Add s,(x P42address ),(x P44const )),((s . (Address_Add s,(x P41address ),(x P43const ))) mod (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) ) & ( ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [9,<*d1,d2,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [10,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) + (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) - (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) ) & ( ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [9,<*d1,d2,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [11,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) + (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) * (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) ) & ( ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [9,<*d1,d2,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [13,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) + (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),(s . (Address_Add s,(x P42address ),(x P44const )))),(Next (IC s)) ) ) & ( ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [9,<*d1,d2,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [12,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) + (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) div (s . (Address_Add s,(x P42address ),(x P44const ))))),(Address_Add s,(x P42address ),(x P44const )),((s . (Address_Add s,(x P41address ),(x P43const ))) mod (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) ) & ( ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [10,<*d1,d2,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [11,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) - (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) * (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) ) & ( ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [10,<*d1,d2,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [13,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) - (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),(s . (Address_Add s,(x P42address ),(x P44const )))),(Next (IC s)) ) ) & ( ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [10,<*d1,d2,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [12,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) - (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) div (s . (Address_Add s,(x P42address ),(x P44const ))))),(Address_Add s,(x P42address ),(x P44const )),((s . (Address_Add s,(x P41address ),(x P43const ))) mod (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) ) & ( ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [11,<*d1,d2,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [13,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) * (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),(s . (Address_Add s,(x P42address ),(x P44const )))),(Next (IC s)) ) ) & ( ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [11,<*d1,d2,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [12,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) * (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) div (s . (Address_Add s,(x P42address ),(x P44const ))))),(Address_Add s,(x P42address ),(x P44const )),((s . (Address_Add s,(x P41address ),(x P43const ))) mod (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) ) & ( ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [13,<*d1,d2,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [12,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),(s . (Address_Add s,(x P42address ),(x P44const )))),(Next (IC s)) iff b1 = SCM-Chg (SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) div (s . (Address_Add s,(x P42address ),(x P44const ))))),(Address_Add s,(x P42address ),(x P44const )),((s . (Address_Add s,(x P41address ),(x P43const ))) mod (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) ) ) by ZFMISC_1:33;
end;

:: deftheorem defines SCM-Exec-Res SCMPDS_1:def 24 :
for x being Element of SCMPDS-Instr
for s being SCMPDS-State holds
( ( ex k1 being Integer st x = [0,<*k1*>] implies SCM-Exec-Res x,s = SCM-Chg s,(jump_address s,(x const_INT )) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [2,<*d1,k1*>] implies SCM-Exec-Res x,s = SCM-Chg (SCM-Chg s,(x P21address ),(x P22const )),(Next (IC s)) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [3,<*d1,k1*>] implies SCM-Exec-Res x,s = SCM-Chg (SCM-Chg s,(Address_Add s,(x P21address ),(x P22const )),(IC s)),(Next (IC s)) ) & ( ex d1 being Element of SCM-Data-Loc st x = [1,<*d1*>] implies SCM-Exec-Res x,s = SCM-Chg (SCM-Chg s,(x address_1 ),(s . (Address_Add s,(x address_1 ),RetSP ))),(PopInstrLoc s,(Address_Add s,(x address_1 ),RetIC )) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [4,<*d1,k1,k2*>] implies SCM-Exec-Res x,s = SCM-Chg s,(IFEQ (s . (Address_Add s,(x P31address ),(x P32const ))),0,(Next (IC s)),(jump_address s,(x P33const ))) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [5,<*d1,k1,k2*>] implies SCM-Exec-Res x,s = SCM-Chg s,(IFGT (s . (Address_Add s,(x P31address ),(x P32const ))),0,(Next (IC s)),(jump_address s,(x P33const ))) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [6,<*d1,k1,k2*>] implies SCM-Exec-Res x,s = SCM-Chg s,(IFGT 0,(s . (Address_Add s,(x P31address ),(x P32const ))),(Next (IC s)),(jump_address s,(x P33const ))) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [7,<*d1,k1,k2*>] implies SCM-Exec-Res x,s = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),(x P33const )),(Next (IC s)) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [8,<*d1,k1,k2*>] implies SCM-Exec-Res x,s = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),((s . (Address_Add s,(x P31address ),(x P32const ))) + (x P33const ))),(Next (IC s)) ) & ( ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [9,<*d1,d2,k1,k2*>] implies SCM-Exec-Res x,s = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) + (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) & ( ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [10,<*d1,d2,k1,k2*>] implies SCM-Exec-Res x,s = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) - (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) & ( ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [11,<*d1,d2,k1,k2*>] implies SCM-Exec-Res x,s = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) * (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) & ( ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [13,<*d1,d2,k1,k2*>] implies SCM-Exec-Res x,s = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),(s . (Address_Add s,(x P42address ),(x P44const )))),(Next (IC s)) ) & ( ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [12,<*d1,d2,k1,k2*>] implies SCM-Exec-Res x,s = SCM-Chg (SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) div (s . (Address_Add s,(x P42address ),(x P44const ))))),(Address_Add s,(x P42address ),(x P44const )),((s . (Address_Add s,(x P41address ),(x P43const ))) mod (s . (Address_Add s,(x P42address ),(x P44const ))))),(Next (IC s)) ) & ( ( for k1 being Integer holds not x = [0,<*k1*>] ) & ( for d1 being Element of SCM-Data-Loc
for k1 being Integer holds not x = [2,<*d1,k1*>] ) & ( for d1 being Element of SCM-Data-Loc
for k1 being Integer holds not x = [3,<*d1,k1*>] ) & ( for d1 being Element of SCM-Data-Loc holds not x = [1,<*d1*>] ) & ( for d1 being Element of SCM-Data-Loc
for k1, k2 being Integer holds not x = [4,<*d1,k1,k2*>] ) & ( for d1 being Element of SCM-Data-Loc
for k1, k2 being Integer holds not x = [5,<*d1,k1,k2*>] ) & ( for d1 being Element of SCM-Data-Loc
for k1, k2 being Integer holds not x = [6,<*d1,k1,k2*>] ) & ( for d1 being Element of SCM-Data-Loc
for k1, k2 being Integer holds not x = [7,<*d1,k1,k2*>] ) & ( for d1 being Element of SCM-Data-Loc
for k1, k2 being Integer holds not x = [8,<*d1,k1,k2*>] ) & ( for d1, d2 being Element of SCM-Data-Loc
for k1, k2 being Integer holds not x = [9,<*d1,d2,k1,k2*>] ) & ( for d1, d2 being Element of SCM-Data-Loc
for k1, k2 being Integer holds not x = [10,<*d1,d2,k1,k2*>] ) & ( for d1, d2 being Element of SCM-Data-Loc
for k1, k2 being Integer holds not x = [11,<*d1,d2,k1,k2*>] ) & ( for d1, d2 being Element of SCM-Data-Loc
for k1, k2 being Integer holds not x = [13,<*d1,d2,k1,k2*>] ) & ( for d1, d2 being Element of SCM-Data-Loc
for k1, k2 being Integer holds not x = [12,<*d1,d2,k1,k2*>] ) implies SCM-Exec-Res x,s = s ) );

registration
let f be Function of SCMPDS-Instr , Funcs (product SCMPDS-OK ),(product SCMPDS-OK );
let x be Element of SCMPDS-Instr ;
cluster f . x -> Relation-like Function-like ;
coherence
( f . x is Function-like & f . x is Relation-like ) ;
end;

definition
func SCMPDS-Exec -> Function of SCMPDS-Instr , Funcs (product SCMPDS-OK ),(product SCMPDS-OK ) means :: SCMPDS_1:def 25
for x being Element of SCMPDS-Instr
for y being SCMPDS-State holds (it . x) . y = SCM-Exec-Res x,y;
existence
ex b1 being Function of SCMPDS-Instr , Funcs (product SCMPDS-OK ),(product SCMPDS-OK ) st
for x being Element of SCMPDS-Instr
for y being SCMPDS-State holds (b1 . x) . y = SCM-Exec-Res x,y
proof end;
uniqueness
for b1, b2 being Function of SCMPDS-Instr , Funcs (product SCMPDS-OK ),(product SCMPDS-OK ) st ( for x being Element of SCMPDS-Instr
for y being SCMPDS-State holds (b1 . x) . y = SCM-Exec-Res x,y ) & ( for x being Element of SCMPDS-Instr
for y being SCMPDS-State holds (b2 . x) . y = SCM-Exec-Res x,y ) holds
b1 = b2
proof end;
end;

:: deftheorem defines SCMPDS-Exec SCMPDS_1:def 25 :
for b1 being Function of SCMPDS-Instr , Funcs (product SCMPDS-OK ),(product SCMPDS-OK ) holds
( b1 = SCMPDS-Exec iff for x being Element of SCMPDS-Instr
for y being SCMPDS-State holds (b1 . x) . y = SCM-Exec-Res x,y );