:: A Small Computer Model with Push-Down Stack
:: by JingChao Chen
::
:: Received June 15, 1999
:: Copyright (c) 1999 Association of Mizar Users
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 Th9: :: SCMPDS_1:9
theorem Th10: :: SCMPDS_1:10
theorem :: SCMPDS_1:11
definition
canceled;canceled;func SCMPDS-Instr -> Subset of
[:NAT ,(((union {INT }) \/ SCM-Memory ) * ):] equals :: SCMPDS_1:def 3
((({ [0 ,<*l*>] where l is Element of INT : verum } \/ { [1,<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) \/ { [I,<*v,c*>] where I is Element of Segm 14, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ) \/ { [I,<*v,c1,c2*>] where I is Element of Segm 14, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } ) \/ { [I,<*v1,v2,c1,c2*>] where I is Element of Segm 14, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } ;
coherence
((({ [0 ,<*l*>] where l is Element of INT : verum } \/ { [1,<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) \/ { [I,<*v,c*>] where I is Element of Segm 14, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ) \/ { [I,<*v,c1,c2*>] where I is Element of Segm 14, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } ) \/ { [I,<*v1,v2,c1,c2*>] where I is Element of Segm 14, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } is Subset of [:NAT ,(((union {INT }) \/ SCM-Memory ) * ):]
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
theorem Th14: :: SCMPDS_1:14
theorem :: SCMPDS_1:15
canceled;
theorem :: SCMPDS_1:16
:: deftheorem Def4 defines SCMPDS-OK SCMPDS_1:def 4 :
theorem Th17: :: SCMPDS_1:17
theorem Th18: :: SCMPDS_1:18
theorem Th19: :: SCMPDS_1:19
theorem Th20: :: SCMPDS_1:20
theorem :: SCMPDS_1:21
theorem :: SCMPDS_1:22
theorem Th23: :: SCMPDS_1:23
theorem Th24: :: SCMPDS_1:24
theorem :: SCMPDS_1:25
:: deftheorem defines IC SCMPDS_1:def 5 :
:: deftheorem defines SCM-Chg SCMPDS_1:def 6 :
theorem :: SCMPDS_1:26
theorem :: SCMPDS_1:27
theorem :: SCMPDS_1:28
:: deftheorem defines SCM-Chg SCMPDS_1:def 7 :
theorem :: SCMPDS_1:29
theorem :: SCMPDS_1:30
theorem :: SCMPDS_1:31
theorem :: SCMPDS_1:32
:: 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 :: SCMPDS_1:33
:: deftheorem Def11 defines const_INT SCMPDS_1:def 11 :
theorem :: SCMPDS_1:34
:: deftheorem Def12 defines P21address SCMPDS_1:def 12 :
:: deftheorem Def13 defines P22const SCMPDS_1:def 13 :
theorem :: SCMPDS_1:35
:: 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 :: SCMPDS_1:36
definition
let x be
Element of
SCMPDS-Instr ;
given m1,
m2 being
Element of
SCM-Data-Loc ,
k1,
k2 being
Integer,
I being
Element of
Segm 14
such that A1:
x = [I,<*m1,m2,k1,k2*>]
;
func x P41address -> Element of
SCM-Data-Loc means :
Def17:
:: SCMPDS_1:def 17
ex
f being
FinSequence of
SCM-Data-Loc \/ INT st
(
f = x `2 &
it = f /. 1 );
existence
ex b1 being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b1 = f /. 1 )
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b1 = f /. 1 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b2 = f /. 1 ) holds
b1 = b2
;
func x P42address -> Element of
SCM-Data-Loc means :
Def18:
:: SCMPDS_1:def 18
ex
f being
FinSequence of
SCM-Data-Loc \/ INT st
(
f = x `2 &
it = f /. 2 );
existence
ex b1 being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b1 = f /. 2 )
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b1 = f /. 2 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b2 = f /. 2 ) holds
b1 = b2
;
func x P43const -> Integer means :
Def19:
:: SCMPDS_1:def 19
ex
f being
FinSequence of
SCM-Data-Loc \/ INT st
(
f = x `2 &
it = f /. 3 );
existence
ex b1 being Integer ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b1 = f /. 3 )
uniqueness
for b1, b2 being Integer st ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b1 = f /. 3 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b2 = f /. 3 ) holds
b1 = b2
;
func x P44const -> Integer means :
Def20:
:: SCMPDS_1:def 20
ex
f being
FinSequence of
SCM-Data-Loc \/ INT st
(
f = x `2 &
it = f /. 4 );
existence
ex b1 being Integer ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `2 & b1 = f /. 4 )
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 :: SCMPDS_1:37
:: 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 :: 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 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 ) );
definition
func SCMPDS-Exec -> Function of
SCMPDS-Instr ,
Funcs (product SCMPDS-OK ),
(product SCMPDS-OK ) means :: SCMPDS_1:def 25
for
x being
Element of
SCMPDS-Instr for
y being
SCMPDS-State holds
(it . x) . y = SCM-Exec-Res x,
y;
existence
ex b1 being Function of SCMPDS-Instr , Funcs (product SCMPDS-OK ),(product SCMPDS-OK ) st
for x being Element of SCMPDS-Instr
for y being SCMPDS-State holds (b1 . x) . y = SCM-Exec-Res x,y
uniqueness
for b1, b2 being Function of SCMPDS-Instr , Funcs (product SCMPDS-OK ),(product SCMPDS-OK ) st ( for x being Element of SCMPDS-Instr
for y being SCMPDS-State holds (b1 . x) . y = SCM-Exec-Res x,y ) & ( for x being Element of SCMPDS-Instr
for y being SCMPDS-State holds (b2 . x) . y = SCM-Exec-Res x,y ) holds
b1 = b2
end;
:: deftheorem defines SCMPDS-Exec SCMPDS_1:def 25 :