:: A Small Computer Model with Push-Down Stack
:: by JingChao Chen
::
:: Received June 15, 1999
:: Copyright (c) 1999-2011 Association of Mizar Users


begin

theorem :: SCMPDS_1:1
canceled;

theorem :: SCMPDS_1:2
canceled;

theorem :: SCMPDS_1:3
canceled;

theorem :: SCMPDS_1:4
canceled;

theorem :: SCMPDS_1:5
canceled;

theorem :: SCMPDS_1:6
canceled;

theorem :: SCMPDS_1:7
canceled;

theorem :: SCMPDS_1:8
canceled;

theorem :: SCMPDS_1:9
for k being Integer holds k in (union {INT}) \/ SCM-Memory
proof end;

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

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

begin

definition
canceled;
canceled;
func SCMPDS-Instr -> set 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 set ;
end;

:: deftheorem SCMPDS_1:def 1 :
canceled;

:: deftheorem SCMPDS_1:def 2 :
canceled;

:: 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
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 k being Element of SCM-Memory holds
( k = NAT or k in SCM-Data-Loc or k in NAT )
proof end;

theorem :: SCMPDS_1:15
canceled;

theorem :: SCMPDS_1:16
for k being Element of NAT holds
( ( ex j being Element of NAT st k = (2 * j) + 1 implies ( k <> 0 & ( for j being Element of NAT holds not k = (2 * j) + 2 ) ) ) & ( ex j being Element of NAT st k = (2 * j) + 2 implies ( k <> 0 & ( for j being Element of NAT holds not k = (2 * j) + 1 ) ) ) )
proof end;

Lm1: now
let k be Element of SCM-Memory ; :: thesis: ( k = NAT or k in SCM-Data-Loc or k in NAT )
( k in {NAT} \/ SCM-Data-Loc or k in NAT ) by XBOOLE_0:def 3;
then ( k in {NAT} or k in SCM-Data-Loc or k in NAT ) by XBOOLE_0:def 3;
hence ( k = NAT or k in SCM-Data-Loc or k in NAT ) by TARSKI:def 1; :: thesis: verum
end;

definition
func SCMPDS-OK -> Function of SCM-Memory,({INT} \/ {SCMPDS-Instr,NAT}) means :Def4: :: SCMPDS_1:def 4
 for k being Element of SCM-Memory holds
( ( k = NAT implies it . k = NAT ) & ( k in SCM-Data-Loc implies it . k = INT ) & ( k in NAT implies it . k = SCMPDS-Instr ) );
existence
ex b1 being Function of SCM-Memory,({INT} \/ {SCMPDS-Instr,NAT}) st
for k being Element of SCM-Memory holds
( ( k = NAT implies b1 . k = NAT ) & ( k in SCM-Data-Loc implies b1 . k = INT ) & ( k in NAT implies b1 . k = SCMPDS-Instr ) )
proof end;
uniqueness
for b1, b2 being Function of SCM-Memory,({INT} \/ {SCMPDS-Instr,NAT}) st ( for k being Element of SCM-Memory holds
( ( k = NAT implies b1 . k = NAT ) & ( k in SCM-Data-Loc implies b1 . k = INT ) & ( k in NAT implies b1 . k = SCMPDS-Instr ) ) ) & ( for k being Element of SCM-Memory holds
( ( k = NAT implies b2 . k = NAT ) & ( k in SCM-Data-Loc implies b2 . k = INT ) & ( k in NAT implies b2 . k = SCMPDS-Instr ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines SCMPDS-OK SCMPDS_1:def 4 :
for b1 being Function of SCM-Memory,({INT} \/ {SCMPDS-Instr,NAT}) holds
( b1 = SCMPDS-OK iff for k being Element of SCM-Memory holds
( ( k = NAT implies b1 . k = NAT ) & ( k in SCM-Data-Loc implies b1 . k = INT ) & ( k in NAT implies b1 . k = SCMPDS-Instr ) ) );

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

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

theorem Th18: :: SCMPDS_1:18
for i being Element of SCM-Memory holds
( SCMPDS-OK . i = NAT iff i = NAT )
proof end;

theorem Th19: :: SCMPDS_1:19
for i being Element of SCM-Memory holds
( SCMPDS-OK . i = INT iff i in SCM-Data-Loc )
proof end;

theorem Th20: :: SCMPDS_1:20
for i being Element of SCM-Memory holds
( SCMPDS-OK . i = SCMPDS-Instr iff i in NAT )
proof end;

theorem :: SCMPDS_1:21
for d1 being Element of SCM-Data-Loc holds SCMPDS-OK . d1 = INT by Th19;

Lm2: NAT c= SCM-Memory
by XBOOLE_1:7;

theorem :: SCMPDS_1:22
for i1 being Element of NAT holds SCMPDS-OK . i1 = SCMPDS-Instr
proof end;

registration
cluster SCMPDS-OK -> non-empty ;
coherence
SCMPDS-OK is non-empty ;
end;

theorem Th23: :: SCMPDS_1:23
pi ((product SCMPDS-OK),NAT) = NAT
proof end;

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

theorem :: SCMPDS_1:25
for i1 being Element of NAT holds pi ((product SCMPDS-OK),i1) = SCMPDS-Instr
proof end;

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

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

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

:: deftheorem defines SCM-Chg SCMPDS_1:def 6 :
for s being SCMPDS-State
for u being Nat holds SCM-Chg (s,u) = s +* (NAT .--> u);

theorem :: SCMPDS_1:26
for s being SCMPDS-State
for u being Nat holds (SCM-Chg (s,u)) . NAT = u
proof end;

theorem :: SCMPDS_1:27
for s being SCMPDS-State
for u being Nat
for mk being Element of SCM-Data-Loc holds (SCM-Chg (s,u)) . mk = s . mk
proof end;

theorem :: SCMPDS_1:28
for s being SCMPDS-State
for u, v being Nat 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
for s being SCMPDS-State
for t being Element of SCM-Data-Loc
for u being Integer holds (SCM-Chg (s,t,u)) . NAT = s . NAT
proof end;

theorem :: SCMPDS_1:30
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
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
for s being SCMPDS-State
for t being Element of SCM-Data-Loc
for u being Integer
for v being Element of NAT 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
[1,(abs ((s . a) + n))];
coherence
[1,(abs ((s . a) + n))] is Element of SCM-Data-Loc by AMI_2:33;
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) = [1,(abs ((s . a) + n))];

definition
let s be SCMPDS-State;
let n be Integer;
func jump_address (s,n) -> Element of NAT equals :: SCMPDS_1:def 9
 abs ((IC s) + n);
coherence
abs ((IC s) + n) is Element of NAT ;
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) + n);

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 `3_3 & it = f /. 1 );
existence
ex b1 being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & 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 `3_3 & b1 = f /. 1 ) & ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & 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 `3_3 & b2 = f /. 1 ) );

theorem :: SCMPDS_1:33
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 `3_3 & it = f /. 1 );
existence
ex b1 being Integer ex f being FinSequence of INT st
( f = x `3_3 & b1 = f /. 1 )
proof end;
uniqueness
for b1, b2 being Integer st ex f being FinSequence of INT st
( f = x `3_3 & b1 = f /. 1 ) & ex f being FinSequence of INT st
( f = x `3_3 & 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 `3_3 & b2 = f /. 1 ) );

theorem :: SCMPDS_1:34
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 `3_3 & it = f /. 1 );
existence
ex b1 being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & 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 `3_3 & b1 = f /. 1 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & 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 `3_3 & it = f /. 2 );
existence
ex b1 being Integer ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 2 )
proof end;
uniqueness
for b1, b2 being Integer st ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 2 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & 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 `3_3 & 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 `3_3 & b2 = f /. 2 ) );

theorem :: SCMPDS_1:35
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 `3_3 & it = f /. 1 );
existence
ex b1 being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & 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 `3_3 & b1 = f /. 1 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & 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 `3_3 & it = f /. 2 );
existence
ex b1 being Integer ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 2 )
proof end;
uniqueness
for b1, b2 being Integer st ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 2 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & 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 `3_3 & it = f /. 3 );
existence
ex b1 being Integer ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 3 )
proof end;
uniqueness
for b1, b2 being Integer st ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 3 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & 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 `3_3 & 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 `3_3 & 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 `3_3 & b2 = f /. 3 ) );

theorem :: SCMPDS_1:36
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 `3_3 & it = f /. 1 );
existence
ex b1 being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & 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 `3_3 & b1 = f /. 1 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & 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 `3_3 & it = f /. 2 );
existence
ex b1 being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & 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 `3_3 & b1 = f /. 2 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & 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 `3_3 & it = f /. 3 );
existence
ex b1 being Integer ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 3 )
proof end;
uniqueness
for b1, b2 being Integer st ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 3 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & 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 `3_3 & it = f /. 4 );
existence
ex b1 being Integer ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 4 )
proof end;
uniqueness
for b1, b2 being Integer st ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 4 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & 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 `3_3 & 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 `3_3 & 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 `3_3 & 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 `3_3 & b2 = f /. 4 ) );

theorem :: SCMPDS_1:37
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 NAT equals :: SCMPDS_1:def 21
(abs (s . a)) + 2;
coherence
(abs (s . a)) + 2 is Element of NAT ;
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) = (abs (s . a)) + 2;

definition
func RetSP -> Element of NAT equals :: SCMPDS_1:def 22
 0 ;
coherence
0 is Element of NAT ;
func RetIC -> Element of NAT equals :: SCMPDS_1:def 23
1;
coherence
1 is Element of 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))),(succ (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))),(succ (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,(succ (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,(succ (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)))),(succ (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))),(succ (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)))),(succ (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))))))),(succ (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))))))),(succ (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))))))),(succ (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)))))),(succ (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))))))),(succ (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))),(succ (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))),(succ (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,(succ (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,(succ (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)))),(succ (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))),(succ (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)))),(succ (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))))))),(succ (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))))))),(succ (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))))))),(succ (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)))))),(succ (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))))))),(succ (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))),(succ (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))),(succ (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,(succ (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,(succ (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)))),(succ (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))),(succ (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)))),(succ (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))))))),(succ (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))))))),(succ (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))))))),(succ (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)))))),(succ (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))))))),(succ (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))),(succ (IC s))) iff b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P21address),(x P22const))),(IC s))),(succ (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))),(succ (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))),(succ (IC s))) iff b1 = SCM-Chg (s,(IFEQ ((s . (Address_Add (s,(x P31address),(x P32const)))),0,(succ (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))),(succ (IC s))) iff b1 = SCM-Chg (s,(IFGT ((s . (Address_Add (s,(x P31address),(x P32const)))),0,(succ (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))),(succ (IC s))) iff b1 = SCM-Chg (s,(IFGT (0,(s . (Address_Add (s,(x P31address),(x P32const)))),(succ (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))),(succ (IC s))) iff b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P31address),(x P32const))),(x P33const))),(succ (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))),(succ (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)))),(succ (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))),(succ (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))))))),(succ (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))),(succ (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))))))),(succ (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))),(succ (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))))))),(succ (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))),(succ (IC s))) iff b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P41address),(x P43const))),(s . (Address_Add (s,(x P42address),(x P44const)))))),(succ (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))),(succ (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))))))),(succ (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))),(succ (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))),(succ (IC s))) iff b1 = SCM-Chg (s,(IFEQ ((s . (Address_Add (s,(x P31address),(x P32const)))),0,(succ (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))),(succ (IC s))) iff b1 = SCM-Chg (s,(IFGT ((s . (Address_Add (s,(x P31address),(x P32const)))),0,(succ (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))),(succ (IC s))) iff b1 = SCM-Chg (s,(IFGT (0,(s . (Address_Add (s,(x P31address),(x P32const)))),(succ (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))),(succ (IC s))) iff b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P31address),(x P32const))),(x P33const))),(succ (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))),(succ (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)))),(succ (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))),(succ (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))))))),(succ (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))),(succ (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))))))),(succ (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))),(succ (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))))))),(succ (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))),(succ (IC s))) iff b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P41address),(x P43const))),(s . (Address_Add (s,(x P42address),(x P44const)))))),(succ (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))),(succ (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))))))),(succ (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,(succ (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,(succ (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)))),(succ (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))),(succ (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)))),(succ (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))))))),(succ (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))))))),(succ (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))))))),(succ (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)))))),(succ (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))))))),(succ (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,(succ (IC s)),(jump_address (s,(x P33const)))))) iff b1 = SCM-Chg (s,(IFGT ((s . (Address_Add (s,(x P31address),(x P32const)))),0,(succ (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,(succ (IC s)),(jump_address (s,(x P33const)))))) iff b1 = SCM-Chg (s,(IFGT (0,(s . (Address_Add (s,(x P31address),(x P32const)))),(succ (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,(succ (IC s)),(jump_address (s,(x P33const)))))) iff b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P31address),(x P32const))),(x P33const))),(succ (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,(succ (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)))),(succ (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,(succ (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))))))),(succ (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,(succ (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))))))),(succ (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,(succ (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))))))),(succ (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,(succ (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)))))),(succ (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,(succ (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))))))),(succ (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,(succ (IC s)),(jump_address (s,(x P33const)))))) iff b1 = SCM-Chg (s,(IFGT (0,(s . (Address_Add (s,(x P31address),(x P32const)))),(succ (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,(succ (IC s)),(jump_address (s,(x P33const)))))) iff b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P31address),(x P32const))),(x P33const))),(succ (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,(succ (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)))),(succ (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,(succ (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))))))),(succ (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,(succ (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))))))),(succ (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,(succ (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))))))),(succ (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,(succ (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)))))),(succ (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,(succ (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))))))),(succ (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)))),(succ (IC s)),(jump_address (s,(x P33const)))))) iff b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P31address),(x P32const))),(x P33const))),(succ (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)))),(succ (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)))),(succ (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)))),(succ (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))))))),(succ (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)))),(succ (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))))))),(succ (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)))),(succ (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))))))),(succ (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)))),(succ (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)))))),(succ (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)))),(succ (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))))))),(succ (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))),(succ (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)))),(succ (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))),(succ (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))))))),(succ (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))),(succ (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))))))),(succ (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))),(succ (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))))))),(succ (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))),(succ (IC s))) iff b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P41address),(x P43const))),(s . (Address_Add (s,(x P42address),(x P44const)))))),(succ (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))),(succ (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))))))),(succ (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)))),(succ (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))))))),(succ (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)))),(succ (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))))))),(succ (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)))),(succ (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))))))),(succ (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)))),(succ (IC s))) iff b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P41address),(x P43const))),(s . (Address_Add (s,(x P42address),(x P44const)))))),(succ (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)))),(succ (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))))))),(succ (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))))))),(succ (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))))))),(succ (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))))))),(succ (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))))))),(succ (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))))))),(succ (IC s))) iff b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P41address),(x P43const))),(s . (Address_Add (s,(x P42address),(x P44const)))))),(succ (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))))))),(succ (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))))))),(succ (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))))))),(succ (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))))))),(succ (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))))))),(succ (IC s))) iff b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P41address),(x P43const))),(s . (Address_Add (s,(x P42address),(x P44const)))))),(succ (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))))))),(succ (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))))))),(succ (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))))))),(succ (IC s))) iff b1 = SCM-Chg ((SCM-Chg (s,(Address_Add (s,(x P41address),(x P43const))),(s . (Address_Add (s,(x P42address),(x P44const)))))),(succ (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))))))),(succ (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))))))),(succ (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)))))),(succ (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))))))),(succ (IC s))) ) ) ) by MCART_1:28;
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))),(succ (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))),(succ (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,(succ (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,(succ (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)))),(succ (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))),(succ (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)))),(succ (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))))))),(succ (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))))))),(succ (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))))))),(succ (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)))))),(succ (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))))))),(succ (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 Action of SCMPDS-Instr,(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 -> Action of SCMPDS-Instr,(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 Action of SCMPDS-Instr,(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 Action of SCMPDS-Instr,(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 Action of SCMPDS-Instr,(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) );