:: SCMPDS_1 semantic presentation

definition
let c1, c2, c3, c4 be set ;
func <*c1,c2,c3,c4*> -> set equals :: SCMPDS_1:def 1
<*a1,a2,a3*> ^ <*a4*>;
correctness
coherence
<*c1,c2,c3*> ^ <*c4*> is set ;
;
let c5 be set ;
func <*c1,c2,c3,c4,c5*> -> set equals :: SCMPDS_1:def 2
<*a1,a2,a3*> ^ <*a4,a5*>;
correctness
coherence
<*c1,c2,c3*> ^ <*c4,c5*> is set ;
;
end;

:: deftheorem Def1 defines <* SCMPDS_1:def 1 :
for b1, b2, b3, b4 being set holds <*b1,b2,b3,b4*> = <*b1,b2,b3*> ^ <*b4*>;

:: deftheorem Def2 defines <* SCMPDS_1:def 2 :
for b1, b2, b3, b4, b5 being set holds <*b1,b2,b3,b4,b5*> = <*b1,b2,b3*> ^ <*b4,b5*>;

registration
let c1, c2, c3, c4 be set ;
cluster <*a1,a2,a3,a4*> -> Relation-like Function-like ;
coherence
( <*c1,c2,c3,c4*> is Function-like & <*c1,c2,c3,c4*> is Relation-like ) ;
let c5 be set ;
cluster <*a1,a2,a3,a4,a5*> -> Relation-like Function-like ;
coherence
( <*c1,c2,c3,c4,c5*> is Function-like & <*c1,c2,c3,c4,c5*> is Relation-like ) ;
end;

registration
let c1, c2, c3, c4 be set ;
cluster <*a1,a2,a3,a4*> -> Relation-like Function-like FinSequence-like ;
coherence
<*c1,c2,c3,c4*> is FinSequence-like ;
let c5 be set ;
cluster <*a1,a2,a3,a4,a5*> -> Relation-like Function-like FinSequence-like ;
coherence
<*c1,c2,c3,c4,c5*> is FinSequence-like ;
end;

definition
let c1 be non empty set ;
let c2, c3, c4, c5 be Element of c1;
redefine func <* as <*c2,c3,c4,c5*> -> FinSequence of a1;
coherence
<*c2,c3,c4,c5*> is FinSequence of c1
proof end;
end;

definition
let c1 be non empty set ;
let c2, c3, c4, c5, c6 be Element of c1;
redefine func <* as <*c2,c3,c4,c5,c6*> -> FinSequence of a1;
coherence
<*c2,c3,c4,c5,c6*> is FinSequence of c1
proof end;
end;

theorem Th1: :: SCMPDS_1:1
for b1, b2, b3, b4 being set holds
( <*b1,b2,b3,b4*> = <*b1,b2,b3*> ^ <*b4*> & <*b1,b2,b3,b4*> = <*b1,b2*> ^ <*b3,b4*> & <*b1,b2,b3,b4*> = <*b1*> ^ <*b2,b3,b4*> & <*b1,b2,b3,b4*> = ((<*b1*> ^ <*b2*>) ^ <*b3*>) ^ <*b4*> )
proof end;

theorem Th2: :: SCMPDS_1:2
for b1, b2, b3, b4, b5 being set holds
( <*b1,b2,b3,b4,b5*> = <*b1,b2,b3*> ^ <*b4,b5*> & <*b1,b2,b3,b4,b5*> = <*b1,b2,b3,b4*> ^ <*b5*> & <*b1,b2,b3,b4,b5*> = (((<*b1*> ^ <*b2*>) ^ <*b3*>) ^ <*b4*>) ^ <*b5*> & <*b1,b2,b3,b4,b5*> = <*b1,b2*> ^ <*b3,b4,b5*> & <*b1,b2,b3,b4,b5*> = <*b1*> ^ <*b2,b3,b4,b5*> )
proof end;

theorem Th3: :: SCMPDS_1:3
for b1, b2, b3, b4 being set
for b5 being FinSequence holds
( b5 = <*b1,b2,b3,b4*> iff ( len b5 = 4 & b5 . 1 = b1 & b5 . 2 = b2 & b5 . 3 = b3 & b5 . 4 = b4 ) )
proof end;

theorem Th4: :: SCMPDS_1:4
for b1, b2, b3, b4 being set holds dom <*b1,b2,b3,b4*> = Seg 4
proof end;

theorem Th5: :: SCMPDS_1:5
for b1, b2, b3, b4, b5 being set
for b6 being FinSequence holds
( b6 = <*b1,b2,b3,b4,b5*> iff ( len b6 = 5 & b6 . 1 = b1 & b6 . 2 = b2 & b6 . 3 = b3 & b6 . 4 = b4 & b6 . 5 = b5 ) )
proof end;

theorem Th6: :: SCMPDS_1:6
for b1, b2, b3, b4, b5 being set holds dom <*b1,b2,b3,b4,b5*> = Seg 5
proof end;

theorem Th7: :: SCMPDS_1:7
for b1 being non empty set
for b2, b3, b4, b5 being Element of b1 holds
( <*b2,b3,b4,b5*> /. 1 = b2 & <*b2,b3,b4,b5*> /. 2 = b3 & <*b2,b3,b4,b5*> /. 3 = b4 & <*b2,b3,b4,b5*> /. 4 = b5 )
proof end;

theorem Th8: :: SCMPDS_1:8
for b1 being non empty set
for b2, b3, b4, b5, b6 being Element of b1 holds
( <*b2,b3,b4,b5,b6*> /. 1 = b2 & <*b2,b3,b4,b5,b6*> /. 2 = b3 & <*b2,b3,b4,b5,b6*> /. 3 = b4 & <*b2,b3,b4,b5,b6*> /. 4 = b5 & <*b2,b3,b4,b5,b6*> /. 5 = b6 )
proof end;

theorem Th9: :: SCMPDS_1:9
for b1 being Integer holds b1 in (union {INT }) \/ NAT
proof end;

theorem Th10: :: SCMPDS_1:10
for b1 being Integer holds b1 in SCM-Data-Loc \/ INT
proof end;

theorem Th11: :: SCMPDS_1:11
for b1 being Element of SCM-Data-Loc holds b1 in SCM-Data-Loc \/ INT
proof end;

definition
func SCMPDS-Instr -> Subset of [:(Segm 14),(((union {INT }) \/ NAT ) * ):] equals :: SCMPDS_1:def 3
((({ [0,<*b1*>] where B is Element of INT : verum } \/ { [1,<*b1*>] where B is Element of SCM-Data-Loc : verum } ) \/ { [b1,<*b2,b3*>] where B is Element of Segm 14, B is Element of SCM-Data-Loc , B is Element of INT : b1 in {2,3} } ) \/ { [b1,<*b2,b3,b4*>] where B is Element of Segm 14, B is Element of SCM-Data-Loc , B is Element of INT , B is Element of INT : b1 in {4,5,6,7,8} } ) \/ { [b1,<*b2,b3,b4,b5*>] where B is Element of Segm 14, B is Element of SCM-Data-Loc , B is Element of SCM-Data-Loc , B is Element of INT , B is Element of INT : b1 in {9,10,11,12,13} } ;
coherence
((({ [0,<*b1*>] where B is Element of INT : verum } \/ { [1,<*b1*>] where B is Element of SCM-Data-Loc : verum } ) \/ { [b1,<*b2,b3*>] where B is Element of Segm 14, B is Element of SCM-Data-Loc , B is Element of INT : b1 in {2,3} } ) \/ { [b1,<*b2,b3,b4*>] where B is Element of Segm 14, B is Element of SCM-Data-Loc , B is Element of INT , B is Element of INT : b1 in {4,5,6,7,8} } ) \/ { [b1,<*b2,b3,b4,b5*>] where B is Element of Segm 14, B is Element of SCM-Data-Loc , B is Element of SCM-Data-Loc , B is Element of INT , B is Element of INT : b1 in {9,10,11,12,13} } is Subset of [:(Segm 14),(((union {INT }) \/ NAT ) * ):]
proof end;
end;

:: deftheorem Def3 defines SCMPDS-Instr SCMPDS_1:def 3 :
SCMPDS-Instr = ((({ [0,<*b1*>] where B is Element of INT : verum } \/ { [1,<*b1*>] where B is Element of SCM-Data-Loc : verum } ) \/ { [b1,<*b2,b3*>] where B is Element of Segm 14, B is Element of SCM-Data-Loc , B is Element of INT : b1 in {2,3} } ) \/ { [b1,<*b2,b3,b4*>] where B is Element of Segm 14, B is Element of SCM-Data-Loc , B is Element of INT , B is Element of INT : b1 in {4,5,6,7,8} } ) \/ { [b1,<*b2,b3,b4,b5*>] where B is Element of Segm 14, B is Element of SCM-Data-Loc , B is Element of SCM-Data-Loc , B is Element of INT , B is Element of INT : b1 in {9,10,11,12,13} } ;

theorem Th12: :: SCMPDS_1:12
canceled;

theorem Th13: :: SCMPDS_1:13
[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
for b1 being Nat holds
( b1 = 0 or ex b2 being Nat st b1 = (2 * b2) + 1 or ex b2 being Nat st b1 = (2 * b2) + 2 )
proof end;

theorem Th15: :: SCMPDS_1:15
canceled;

theorem Th16: :: SCMPDS_1:16
for b1 being Nat holds
( ( ex b2 being Nat st b1 = (2 * b2) + 1 implies ( b1 <> 0 & ( for b2 being Nat holds not b1 = (2 * b2) + 2 ) ) ) & ( ex b2 being Nat st b1 = (2 * b2) + 2 implies ( b1 <> 0 & ( for b2 being Nat holds not b1 = (2 * b2) + 1 ) ) ) )
proof end;

definition
func SCMPDS-OK -> Function of NAT ,{INT } \/ {SCMPDS-Instr ,SCM-Instr-Loc } means :Def4: :: SCMPDS_1:def 4
( a1 . 0 = SCM-Instr-Loc & ( for b1 being Nat holds
( a1 . ((2 * b1) + 1) = INT & a1 . ((2 * b1) + 2) = SCMPDS-Instr ) ) );
existence
ex b1 being Function of NAT ,{INT } \/ {SCMPDS-Instr ,SCM-Instr-Loc } st
( b1 . 0 = SCM-Instr-Loc & ( for b2 being Nat holds
( b1 . ((2 * b2) + 1) = INT & b1 . ((2 * b2) + 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 b3 being Nat holds
( b1 . ((2 * b3) + 1) = INT & b1 . ((2 * b3) + 2) = SCMPDS-Instr ) ) & b2 . 0 = SCM-Instr-Loc & ( for b3 being Nat holds
( b2 . ((2 * b3) + 1) = INT & b2 . ((2 * b3) + 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 b2 being Nat holds
( b1 . ((2 * b2) + 1) = INT & b1 . ((2 * b2) + 2) = SCMPDS-Instr ) ) ) );

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

theorem Th17: :: SCMPDS_1:17
( SCM-Instr-Loc <> SCMPDS-Instr & SCMPDS-Instr <> INT )
proof end;

theorem Th18: :: SCMPDS_1:18
for b1 being Nat holds
( SCMPDS-OK . b1 = SCM-Instr-Loc iff b1 = 0 )
proof end;

theorem Th19: :: SCMPDS_1:19
for b1 being Nat holds
( SCMPDS-OK . b1 = INT iff ex b2 being Nat st b1 = (2 * b2) + 1 )
proof end;

theorem Th20: :: SCMPDS_1:20
for b1 being Nat holds
( SCMPDS-OK . b1 = SCMPDS-Instr iff ex b2 being Nat st b1 = (2 * b2) + 2 )
proof end;

theorem Th21: :: SCMPDS_1:21
for b1 being Element of SCM-Data-Loc holds SCMPDS-OK . b1 = INT
proof end;

theorem Th22: :: SCMPDS_1:22
for b1 being Element of SCM-Instr-Loc holds SCMPDS-OK . b1 = SCMPDS-Instr
proof end;

theorem Th23: :: SCMPDS_1:23
pi (product SCMPDS-OK ),0 = SCM-Instr-Loc
proof end;

theorem Th24: :: SCMPDS_1:24
for b1 being Element of SCM-Data-Loc holds pi (product SCMPDS-OK ),b1 = INT
proof end;

theorem Th25: :: SCMPDS_1:25
for b1 being Element of SCM-Instr-Loc holds pi (product SCMPDS-OK ),b1 = SCMPDS-Instr
proof end;

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

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

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

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

theorem Th26: :: SCMPDS_1:26
for b1 being SCMPDS-State
for b2 being Element of SCM-Instr-Loc holds (SCM-Chg b1,b2) . 0 = b2
proof end;

theorem Th27: :: SCMPDS_1:27
for b1 being SCMPDS-State
for b2 being Element of SCM-Instr-Loc
for b3 being Element of SCM-Data-Loc holds (SCM-Chg b1,b2) . b3 = b1 . b3
proof end;

theorem Th28: :: SCMPDS_1:28
for b1 being SCMPDS-State
for b2, b3 being Element of SCM-Instr-Loc holds (SCM-Chg b1,b2) . b3 = b1 . b3
proof end;

definition
let c1 be SCMPDS-State;
let c2 be Element of SCM-Data-Loc ;
let c3 be Integer;
func SCM-Chg c1,c2,c3 -> SCMPDS-State equals :: SCMPDS_1:def 7
a1 +* (a2 .--> a3);
coherence
c1 +* (c2 .--> c3) is SCMPDS-State
proof end;
end;

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

theorem Th29: :: SCMPDS_1:29
for b1 being SCMPDS-State
for b2 being Element of SCM-Data-Loc
for b3 being Integer holds (SCM-Chg b1,b2,b3) . 0 = b1 . 0
proof end;

theorem Th30: :: SCMPDS_1:30
for b1 being SCMPDS-State
for b2 being Element of SCM-Data-Loc
for b3 being Integer holds (SCM-Chg b1,b2,b3) . b2 = b3
proof end;

theorem Th31: :: SCMPDS_1:31
for b1 being SCMPDS-State
for b2 being Element of SCM-Data-Loc
for b3 being Integer
for b4 being Element of SCM-Data-Loc st b4 <> b2 holds
(SCM-Chg b1,b2,b3) . b4 = b1 . b4
proof end;

theorem Th32: :: SCMPDS_1:32
for b1 being SCMPDS-State
for b2 being Element of SCM-Data-Loc
for b3 being Integer
for b4 being Element of SCM-Instr-Loc holds (SCM-Chg b1,b2,b3) . b4 = b1 . b4
proof end;

definition
let c1 be SCMPDS-State;
let c2 be Element of SCM-Data-Loc ;
redefine func . as c1 . c2 -> Integer;
coherence
c1 . c2 is Integer
proof end;
end;

definition
let c1 be SCMPDS-State;
let c2 be Element of SCM-Data-Loc ;
let c3 be Integer;
func Address_Add c1,c2,c3 -> Element of SCM-Data-Loc equals :: SCMPDS_1:def 8
(2 * (abs ((a1 . a2) + a3))) + 1;
coherence
(2 * (abs ((c1 . c2) + c3))) + 1 is Element of SCM-Data-Loc
proof end;
end;

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

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

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

definition
let c1 be Element of SCM-Data-Loc ;
let c2 be Integer;
redefine func <* as <*c1,c2*> -> FinSequence of SCM-Data-Loc \/ INT ;
coherence
<*c1,c2*> is FinSequence of SCM-Data-Loc \/ INT
proof end;
end;

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

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

theorem Th33: :: SCMPDS_1:33
for b1 being Element of Segm 14
for b2 being Element of SCMPDS-Instr
for b3 being Element of SCM-Data-Loc st b2 = [b1,<*b3*>] holds
b2 address_1 = b3
proof end;

definition
let c1 be Element of SCMPDS-Instr ;
given c2 being Integer, c3 being Element of Segm 14 such that E24: c1 = [c3,<*c2*>] ;
func c1 const_INT -> Integer means :Def11: :: SCMPDS_1:def 11
ex b1 being FinSequence of INT st
( b1 = a1 `2 & a2 = b1 /. 1 );
existence
ex b1 being Integerex b2 being FinSequence of INT st
( b2 = c1 `2 & b1 = b2 /. 1 )
proof end;
uniqueness
for b1, b2 being Integer st ex b3 being FinSequence of INT st
( b3 = c1 `2 & b1 = b3 /. 1 ) & ex b3 being FinSequence of INT st
( b3 = c1 `2 & b2 = b3 /. 1 ) holds
b1 = b2 ;
end;

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

theorem Th34: :: SCMPDS_1:34
for b1 being Element of Segm 14
for b2 being Element of SCMPDS-Instr
for b3 being Integer st b2 = [b1,<*b3*>] holds
b2 const_INT = b3
proof end;

definition
let c1 be Element of SCMPDS-Instr ;
given c2 being Element of SCM-Data-Loc , c3 being Integer, c4 being Element of Segm 14 such that E25: c1 = [c4,<*c2,c3*>] ;
func c1 P21address -> Element of SCM-Data-Loc means :Def12: :: SCMPDS_1:def 12
ex b1 being FinSequence of SCM-Data-Loc \/ INT st
( b1 = a1 `2 & a2 = b1 /. 1 );
existence
ex b1 being Element of SCM-Data-Loc ex b2 being FinSequence of SCM-Data-Loc \/ INT st
( b2 = c1 `2 & b1 = b2 /. 1 )
proof end;
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex b3 being FinSequence of SCM-Data-Loc \/ INT st
( b3 = c1 `2 & b1 = b3 /. 1 ) & ex b3 being FinSequence of SCM-Data-Loc \/ INT st
( b3 = c1 `2 & b2 = b3 /. 1 ) holds
b1 = b2 ;
func c1 P22const -> Integer means :Def13: :: SCMPDS_1:def 13
ex b1 being FinSequence of SCM-Data-Loc \/ INT st
( b1 = a1 `2 & a2 = b1 /. 2 );
existence
ex b1 being Integerex b2 being FinSequence of SCM-Data-Loc \/ INT st
( b2 = c1 `2 & b1 = b2 /. 2 )
proof end;
uniqueness
for b1, b2 being Integer st ex b3 being FinSequence of SCM-Data-Loc \/ INT st
( b3 = c1 `2 & b1 = b3 /. 2 ) & ex b3 being FinSequence of SCM-Data-Loc \/ INT st
( b3 = c1 `2 & b2 = b3 /. 2 ) holds
b1 = b2 ;
end;

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

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

theorem Th35: :: SCMPDS_1:35
for b1 being Element of Segm 14
for b2 being Element of SCMPDS-Instr
for b3 being Element of SCM-Data-Loc
for b4 being Integer st b2 = [b1,<*b3,b4*>] holds
( b2 P21address = b3 & b2 P22const = b4 )
proof end;

definition
let c1 be Element of SCMPDS-Instr ;
given c2 being Element of SCM-Data-Loc , c3, c4 being Integer, c5 being Element of Segm 14 such that E27: c1 = [c5,<*c2,c3,c4*>] ;
func c1 P31address -> Element of SCM-Data-Loc means :Def14: :: SCMPDS_1:def 14
ex b1 being FinSequence of SCM-Data-Loc \/ INT st
( b1 = a1 `2 & a2 = b1 /. 1 );
existence
ex b1 being Element of SCM-Data-Loc ex b2 being FinSequence of SCM-Data-Loc \/ INT st
( b2 = c1 `2 & b1 = b2 /. 1 )
proof end;
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex b3 being FinSequence of SCM-Data-Loc \/ INT st
( b3 = c1 `2 & b1 = b3 /. 1 ) & ex b3 being FinSequence of SCM-Data-Loc \/ INT st
( b3 = c1 `2 & b2 = b3 /. 1 ) holds
b1 = b2 ;
func c1 P32const -> Integer means :Def15: :: SCMPDS_1:def 15
ex b1 being FinSequence of SCM-Data-Loc \/ INT st
( b1 = a1 `2 & a2 = b1 /. 2 );
existence
ex b1 being Integerex b2 being FinSequence of SCM-Data-Loc \/ INT st
( b2 = c1 `2 & b1 = b2 /. 2 )
proof end;
uniqueness
for b1, b2 being Integer st ex b3 being FinSequence of SCM-Data-Loc \/ INT st
( b3 = c1 `2 & b1 = b3 /. 2 ) & ex b3 being FinSequence of SCM-Data-Loc \/ INT st
( b3 = c1 `2 & b2 = b3 /. 2 ) holds
b1 = b2 ;
func c1 P33const -> Integer means :Def16: :: SCMPDS_1:def 16
ex b1 being FinSequence of SCM-Data-Loc \/ INT st
( b1 = a1 `2 & a2 = b1 /. 3 );
existence
ex b1 being Integerex b2 being FinSequence of SCM-Data-Loc \/ INT st
( b2 = c1 `2 & b1 = b2 /. 3 )
proof end;
uniqueness
for b1, b2 being Integer st ex b3 being FinSequence of SCM-Data-Loc \/ INT st
( b3 = c1 `2 & b1 = b3 /. 3 ) & ex b3 being FinSequence of SCM-Data-Loc \/ INT st
( b3 = c1 `2 & b2 = b3 /. 3 ) holds
b1 = b2 ;
end;

:: deftheorem Def14 defines P31address SCMPDS_1:def 14 :
for b1 being Element of SCMPDS-Instr st ex b2 being Element of SCM-Data-Loc ex b3, b4 being Integerex b5 being Element of Segm 14 st b1 = [b5,<*b2,b3,b4*>] holds
for b2 being Element of SCM-Data-Loc holds
( b2 = b1 P31address iff ex b3 being FinSequence of SCM-Data-Loc \/ INT st
( b3 = b1 `2 & b2 = b3 /. 1 ) );

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

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

theorem Th36: :: SCMPDS_1:36
for b1 being Element of Segm 14
for b2 being Element of SCMPDS-Instr
for b3 being Element of SCM-Data-Loc
for b4, b5 being Integer st b2 = [b1,<*b3,b4,b5*>] holds
( b2 P31address = b3 & b2 P32const = b4 & b2 P33const = b5 )
proof end;

definition
let c1 be Element of SCMPDS-Instr ;
given c2, c3 being Element of SCM-Data-Loc , c4, c5 being Integer, c6 being Element of Segm 14 such that E30: c1 = [c6,<*c2,c3,c4,c5*>] ;
func c1 P41address -> Element of SCM-Data-Loc means :Def17: :: SCMPDS_1:def 17
ex b1 being FinSequence of SCM-Data-Loc \/ INT st
( b1 = a1 `2 & a2 = b1 /. 1 );
existence
ex b1 being Element of SCM-Data-Loc ex b2 being FinSequence of SCM-Data-Loc \/ INT st
( b2 = c1 `2 & b1 = b2 /. 1 )
proof end;
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex b3 being FinSequence of SCM-Data-Loc \/ INT st
( b3 = c1 `2 & b1 = b3 /. 1 ) & ex b3 being FinSequence of SCM-Data-Loc \/ INT st
( b3 = c1 `2 & b2 = b3 /. 1 ) holds
b1 = b2 ;
func c1 P42address -> Element of SCM-Data-Loc means :Def18: :: SCMPDS_1:def 18
ex b1 being FinSequence of SCM-Data-Loc \/ INT st
( b1 = a1 `2 & a2 = b1 /. 2 );
existence
ex b1 being Element of SCM-Data-Loc ex b2 being FinSequence of SCM-Data-Loc \/ INT st
( b2 = c1 `2 & b1 = b2 /. 2 )
proof end;
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex b3 being FinSequence of SCM-Data-Loc \/ INT st
( b3 = c1 `2 & b1 = b3 /. 2 ) & ex b3 being FinSequence of SCM-Data-Loc \/ INT st
( b3 = c1 `2 & b2 = b3 /. 2 ) holds
b1 = b2 ;
func c1 P43const -> Integer means :Def19: :: SCMPDS_1:def 19
ex b1 being FinSequence of SCM-Data-Loc \/ INT st
( b1 = a1 `2 & a2 = b1 /. 3 );
existence
ex b1 being Integerex b2 being FinSequence of SCM-Data-Loc \/ INT st
( b2 = c1 `2 & b1 = b2 /. 3 )
proof end;
uniqueness
for b1, b2 being Integer st ex b3 being FinSequence of SCM-Data-Loc \/ INT st
( b3 = c1 `2 & b1 = b3 /. 3 ) & ex b3 being FinSequence of SCM-Data-Loc \/ INT st
( b3 = c1 `2 & b2 = b3 /. 3 ) holds
b1 = b2 ;
func c1 P44const -> Integer means :Def20: :: SCMPDS_1:def 20
ex b1 being FinSequence of SCM-Data-Loc \/ INT st
( b1 = a1 `2 & a2 = b1 /. 4 );
existence
ex b1 being Integerex b2 being FinSequence of SCM-Data-Loc \/ INT st
( b2 = c1 `2 & b1 = b2 /. 4 )
proof end;
uniqueness
for b1, b2 being Integer st ex b3 being FinSequence of SCM-Data-Loc \/ INT st
( b3 = c1 `2 & b1 = b3 /. 4 ) & ex b3 being FinSequence of SCM-Data-Loc \/ INT st
( b3 = c1 `2 & b2 = b3 /. 4 ) holds
b1 = b2 ;
end;

:: deftheorem Def17 defines P41address SCMPDS_1:def 17 :
for b1 being Element of SCMPDS-Instr st ex b2, b3 being Element of SCM-Data-Loc ex b4, b5 being Integerex b6 being Element of Segm 14 st b1 = [b6,<*b2,b3,b4,b5*>] holds
for b2 being Element of SCM-Data-Loc holds
( b2 = b1 P41address iff ex b3 being FinSequence of SCM-Data-Loc \/ INT st
( b3 = b1 `2 & b2 = b3 /. 1 ) );

:: deftheorem Def18 defines P42address SCMPDS_1:def 18 :
for b1 being Element of SCMPDS-Instr st ex b2, b3 being Element of SCM-Data-Loc ex b4, b5 being Integerex b6 being Element of Segm 14 st b1 = [b6,<*b2,b3,b4,b5*>] holds
for b2 being Element of SCM-Data-Loc holds
( b2 = b1 P42address iff ex b3 being FinSequence of SCM-Data-Loc \/ INT st
( b3 = b1 `2 & b2 = b3 /. 2 ) );

:: deftheorem Def19 defines P43const SCMPDS_1:def 19 :
for b1 being Element of SCMPDS-Instr st ex b2, b3 being Element of SCM-Data-Loc ex b4, b5 being Integerex b6 being Element of Segm 14 st b1 = [b6,<*b2,b3,b4,b5*>] holds
for b2 being Integer holds
( b2 = b1 P43const iff ex b3 being FinSequence of SCM-Data-Loc \/ INT st
( b3 = b1 `2 & b2 = b3 /. 3 ) );

:: deftheorem Def20 defines P44const SCMPDS_1:def 20 :
for b1 being Element of SCMPDS-Instr st ex b2, b3 being Element of SCM-Data-Loc ex b4, b5 being Integerex b6 being Element of Segm 14 st b1 = [b6,<*b2,b3,b4,b5*>] holds
for b2 being Integer holds
( b2 = b1 P44const iff ex b3 being FinSequence of SCM-Data-Loc \/ INT st
( b3 = b1 `2 & b2 = b3 /. 4 ) );

theorem Th37: :: SCMPDS_1:37
for b1 being Element of Segm 14
for b2 being Element of SCMPDS-Instr
for b3, b4 being Element of SCM-Data-Loc
for b5, b6 being Integer st b2 = [b1,<*b3,b4,b5,b6*>] holds
( b2 P41address = b3 & b2 P42address = b4 & b2 P43const = b5 & b2 P44const = b6 )
proof end;

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

:: deftheorem Def21 defines PopInstrLoc SCMPDS_1:def 21 :
for b1 being SCMPDS-State
for b2 being Element of SCM-Data-Loc holds PopInstrLoc b1,b2 = (2 * ((abs (b1 . b2)) 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 Def22 defines RetSP SCMPDS_1:def 22 :
RetSP = 0;

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

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

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

registration
let c1 be Function of SCMPDS-Instr , Funcs (product SCMPDS-OK ),(product SCMPDS-OK );
let c2 be Element of SCMPDS-Instr ;
cluster a1 . a2 -> Relation-like Function-like ;
coherence
( c1 . c2 is Function-like & c1 . c2 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 b1 being Element of SCMPDS-Instr
for b2 being SCMPDS-State holds (a1 . b1) . b2 = SCM-Exec-Res b1,b2;
existence
ex b1 being Function of SCMPDS-Instr , Funcs (product SCMPDS-OK ),(product SCMPDS-OK ) st
for b2 being Element of SCMPDS-Instr
for b3 being SCMPDS-State holds (b1 . b2) . b3 = SCM-Exec-Res b2,b3
proof end;
uniqueness
for b1, b2 being Function of SCMPDS-Instr , Funcs (product SCMPDS-OK ),(product SCMPDS-OK ) st ( for b3 being Element of SCMPDS-Instr
for b4 being SCMPDS-State holds (b1 . b3) . b4 = SCM-Exec-Res b3,b4 ) & ( for b3 being Element of SCMPDS-Instr
for b4 being SCMPDS-State holds (b2 . b3) . b4 = SCM-Exec-Res b3,b4 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def25 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 b2 being Element of SCMPDS-Instr
for b3 being SCMPDS-State holds (b1 . b2) . b3 = SCM-Exec-Res b2,b3 );