begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem Th10:
theorem
begin
definition
canceled;canceled;func SCMPDS-Instr -> set equals
((({ [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
canceled;
theorem Th13:
theorem Th14:
theorem
canceled;
theorem
:: deftheorem Def4 defines SCMPDS-OK SCMPDS_1:def 4 :
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem
theorem
theorem Th23:
theorem Th24:
theorem
:: deftheorem defines IC SCMPDS_1:def 5 :
:: deftheorem defines SCM-Chg SCMPDS_1:def 6 :
theorem
theorem
theorem
:: deftheorem defines SCM-Chg SCMPDS_1:def 7 :
theorem
theorem
theorem
theorem
:: deftheorem defines Address_Add SCMPDS_1:def 8 :
:: deftheorem defines jump_address SCMPDS_1:def 9 :
:: deftheorem Def10 defines address_1 SCMPDS_1:def 10 :
theorem
:: deftheorem Def11 defines const_INT SCMPDS_1:def 11 :
theorem
:: deftheorem Def12 defines P21address SCMPDS_1:def 12 :
:: deftheorem Def13 defines P22const SCMPDS_1:def 13 :
theorem
:: deftheorem Def14 defines P31address SCMPDS_1:def 14 :
:: deftheorem Def15 defines P32const SCMPDS_1:def 15 :
:: deftheorem Def16 defines P33const SCMPDS_1:def 16 :
theorem
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:
ex
f being
FinSequence of
SCM-Data-Loc \/ INT st
(
f = x `2 &
it = f /. 1 );
existence
ex b1 being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b1 = f /. 1 )
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b1 = f /. 1 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b2 = f /. 1 ) holds
b1 = b2
;
func x P42address -> Element of
SCM-Data-Loc means :
Def18:
ex
f being
FinSequence of
SCM-Data-Loc \/ INT st
(
f = x `2 &
it = f /. 2 );
existence
ex b1 being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b1 = f /. 2 )
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b1 = f /. 2 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b2 = f /. 2 ) holds
b1 = b2
;
func x P43const -> Integer means :
Def19:
ex
f being
FinSequence of
SCM-Data-Loc \/ INT st
(
f = x `2 &
it = f /. 3 );
existence
ex b1 being Integer ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b1 = f /. 3 )
uniqueness
for b1, b2 being Integer st ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b1 = f /. 3 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b2 = f /. 3 ) holds
b1 = b2
;
func x P44const -> Integer means :
Def20:
ex
f being
FinSequence of
SCM-Data-Loc \/ INT st
(
f = x `2 &
it = f /. 4 );
existence
ex b1 being Integer ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b1 = f /. 4 )
uniqueness
for b1, b2 being Integer st ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b1 = f /. 4 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b2 = f /. 4 ) holds
b1 = b2
;
end;
:: deftheorem Def17 defines P41address SCMPDS_1:def 17 :
:: deftheorem Def18 defines P42address SCMPDS_1:def 18 :
:: deftheorem Def19 defines P43const SCMPDS_1:def 19 :
:: deftheorem Def20 defines P44const SCMPDS_1:def 20 :
theorem
:: deftheorem defines PopInstrLoc SCMPDS_1:def 21 :
:: deftheorem defines RetSP SCMPDS_1:def 22 :
:: deftheorem defines RetIC SCMPDS_1:def 23 :
definition
let x be
Element of
SCMPDS-Instr ;
let s be
SCMPDS-State;
func SCM-Exec-Res x,
s -> SCMPDS-State equals
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 ZFMISC_1:33;
end;
:: deftheorem defines SCM-Exec-Res SCMPDS_1:def 24 :
for
x being
Element of
SCMPDS-Instr for
s being
SCMPDS-State holds
( ( ex
k1 being
Integer st
x = [0 ,<*k1*>] implies
SCM-Exec-Res x,
s = SCM-Chg s,
(jump_address s,(x const_INT )) ) & ( ex
d1 being
Element of
SCM-Data-Loc ex
k1 being
Integer st
x = [2,<*d1,k1*>] implies
SCM-Exec-Res x,
s = SCM-Chg (SCM-Chg s,(x P21address ),(x P22const )),
(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 ) );
:: deftheorem defines SCMPDS-Exec SCMPDS_1:def 25 :