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 :
for b1 being Function of SCM-Memory ,({INT } \/ {SCMPDS-Instr ,NAT }) holds
( b1 = SCMPDS-OK iff for k being Element of SCM-Memory holds
( ( k = NAT implies b1 . k = NAT ) & ( k in SCM-Data-Loc implies b1 . k = INT ) & ( k in NAT implies b1 . k = SCMPDS-Instr ) ) );
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem
theorem
theorem Th23:
theorem Th24:
theorem
:: deftheorem defines IC SCMPDS_1:def 5 :
for s being SCMPDS-State holds IC s = s . NAT ;
:: deftheorem defines SCM-Chg SCMPDS_1:def 6 :
for s being SCMPDS-State
for u being Nat holds SCM-Chg s,u = s +* (NAT .--> u);
theorem
theorem
theorem
:: deftheorem defines SCM-Chg SCMPDS_1:def 7 :
for s being SCMPDS-State
for t being Element of SCM-Data-Loc
for u being Integer holds SCM-Chg s,t,u = s +* (t .--> u);
theorem
theorem
theorem
theorem
:: deftheorem defines Address_Add SCMPDS_1:def 8 :
for s being SCMPDS-State
for a being Element of SCM-Data-Loc
for n being Integer holds Address_Add s,a,n = [1,(abs ((s . a) + n))];
:: deftheorem defines jump_address SCMPDS_1:def 9 :
for s being SCMPDS-State
for n being Integer holds jump_address s,n = abs ((IC s) + n);
:: deftheorem Def10 defines address_1 SCMPDS_1:def 10 :
for x being Element of SCMPDS-Instr st ex mk being Element of SCM-Data-Loc ex I being Element of Segm 14 st x = [I,{} ,<*mk*>] holds
for b2 being Element of SCM-Data-Loc holds
( b2 = x address_1 iff ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & b2 = f /. 1 ) );
theorem
:: deftheorem Def11 defines const_INT SCMPDS_1:def 11 :
for x being Element of SCMPDS-Instr st ex r being Integer ex I being Element of Segm 14 st x = [I,{} ,<*r*>] holds
for b2 being Integer holds
( b2 = x const_INT iff ex f being FinSequence of INT st
( f = x `3_3 & b2 = f /. 1 ) );
theorem
:: deftheorem Def12 defines P21address SCMPDS_1:def 12 :
for x being Element of SCMPDS-Instr st ex mk being Element of SCM-Data-Loc ex r being Integer ex I being Element of Segm 14 st x = [I,{} ,<*mk,r*>] holds
for b2 being Element of SCM-Data-Loc holds
( b2 = x P21address iff ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 1 ) );
:: deftheorem Def13 defines P22const SCMPDS_1:def 13 :
for x being Element of SCMPDS-Instr st ex mk being Element of SCM-Data-Loc ex r being Integer ex I being Element of Segm 14 st x = [I,{} ,<*mk,r*>] holds
for b2 being Integer holds
( b2 = x P22const iff ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 2 ) );
theorem
definition
let x be
Element of
SCMPDS-Instr ;
given m1 being
Element of
SCM-Data-Loc ,
k1,
k2 being
Integer,
I being
Element of
Segm 14
such that A1:
x = [I,{} ,<*m1,k1,k2*>]
;
func x P31address -> Element of
SCM-Data-Loc means :
Def14:
ex
f being
FinSequence of
SCM-Data-Loc \/ INT st
(
f = x `3_3 &
it = f /. 1 );
existence
ex b1 being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 1 )
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 1 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 1 ) holds
b1 = b2
;
func x P32const -> Integer means :
Def15:
ex
f being
FinSequence of
SCM-Data-Loc \/ INT st
(
f = x `3_3 &
it = f /. 2 );
existence
ex b1 being Integer ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 2 )
uniqueness
for b1, b2 being Integer st ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 2 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 2 ) holds
b1 = b2
;
func x P33const -> Integer means :
Def16:
ex
f being
FinSequence of
SCM-Data-Loc \/ INT st
(
f = x `3_3 &
it = f /. 3 );
existence
ex b1 being Integer ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 3 )
uniqueness
for b1, b2 being Integer st ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 3 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 3 ) holds
b1 = b2
;
end;
:: deftheorem Def14 defines P31address SCMPDS_1:def 14 :
for x being Element of SCMPDS-Instr st ex m1 being Element of SCM-Data-Loc ex k1, k2 being Integer ex I being Element of Segm 14 st x = [I,{} ,<*m1,k1,k2*>] holds
for b2 being Element of SCM-Data-Loc holds
( b2 = x P31address iff ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 1 ) );
:: deftheorem Def15 defines P32const SCMPDS_1:def 15 :
for x being Element of SCMPDS-Instr st ex m1 being Element of SCM-Data-Loc ex k1, k2 being Integer ex I being Element of Segm 14 st x = [I,{} ,<*m1,k1,k2*>] holds
for b2 being Integer holds
( b2 = x P32const iff ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 2 ) );
:: deftheorem Def16 defines P33const SCMPDS_1:def 16 :
for x being Element of SCMPDS-Instr st ex m1 being Element of SCM-Data-Loc ex k1, k2 being Integer ex I being Element of Segm 14 st x = [I,{} ,<*m1,k1,k2*>] holds
for b2 being Integer holds
( b2 = x P33const iff ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 3 ) );
theorem
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 `3_3 &
it = f /. 1 );
existence
ex b1 being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 1 )
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 1 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 1 ) holds
b1 = b2
;
func x P42address -> Element of
SCM-Data-Loc means :
Def18:
ex
f being
FinSequence of
SCM-Data-Loc \/ INT st
(
f = x `3_3 &
it = f /. 2 );
existence
ex b1 being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 2 )
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 2 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 2 ) holds
b1 = b2
;
func x P43const -> Integer means :
Def19:
ex
f being
FinSequence of
SCM-Data-Loc \/ INT st
(
f = x `3_3 &
it = f /. 3 );
existence
ex b1 being Integer ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 3 )
uniqueness
for b1, b2 being Integer st ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 3 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 3 ) holds
b1 = b2
;
func x P44const -> Integer means :
Def20:
ex
f being
FinSequence of
SCM-Data-Loc \/ INT st
(
f = x `3_3 &
it = f /. 4 );
existence
ex b1 being Integer ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 4 )
uniqueness
for b1, b2 being Integer st ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 4 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 4 ) holds
b1 = b2
;
end;
:: deftheorem Def17 defines P41address SCMPDS_1:def 17 :
for x being Element of SCMPDS-Instr st ex m1, m2 being Element of SCM-Data-Loc ex k1, k2 being Integer ex I being Element of Segm 14 st x = [I,{} ,<*m1,m2,k1,k2*>] holds
for b2 being Element of SCM-Data-Loc holds
( b2 = x P41address iff ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 1 ) );
:: deftheorem Def18 defines P42address SCMPDS_1:def 18 :
for x being Element of SCMPDS-Instr st ex m1, m2 being Element of SCM-Data-Loc ex k1, k2 being Integer ex I being Element of Segm 14 st x = [I,{} ,<*m1,m2,k1,k2*>] holds
for b2 being Element of SCM-Data-Loc holds
( b2 = x P42address iff ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 2 ) );
:: deftheorem Def19 defines P43const SCMPDS_1:def 19 :
for x being Element of SCMPDS-Instr st ex m1, m2 being Element of SCM-Data-Loc ex k1, k2 being Integer ex I being Element of Segm 14 st x = [I,{} ,<*m1,m2,k1,k2*>] holds
for b2 being Integer holds
( b2 = x P43const iff ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 3 ) );
:: deftheorem Def20 defines P44const SCMPDS_1:def 20 :
for x being Element of SCMPDS-Instr st ex m1, m2 being Element of SCM-Data-Loc ex k1, k2 being Integer ex I being Element of Segm 14 st x = [I,{} ,<*m1,m2,k1,k2*>] holds
for b2 being Integer holds
( b2 = x P44const iff ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 4 ) );
theorem
:: deftheorem defines PopInstrLoc SCMPDS_1:def 21 :
for s being SCMPDS-State
for a being Element of SCM-Data-Loc holds PopInstrLoc s,a = (abs (s . a)) + 2;
:: deftheorem defines RetSP SCMPDS_1:def 22 :
RetSP = 0 ;
:: deftheorem defines RetIC SCMPDS_1:def 23 :
RetIC = 1;
definition
let x be
Element of
SCMPDS-Instr ;
let s be
SCMPDS-State;
func SCM-Exec-Res x,
s -> SCMPDS-State equals
SCM-Chg s,
(jump_address s,(x const_INT )) if ex
k1 being
Integer st
x = [0 ,{} ,<*k1*>] SCM-Chg (SCM-Chg s,(x P21address ),(x P22const )),
(succ (IC s)) if ex
d1 being
Element of
SCM-Data-Loc ex
k1 being
Integer st
x = [2,{} ,<*d1,k1*>] SCM-Chg (SCM-Chg s,(Address_Add s,(x P21address ),(x P22const )),(IC s)),
(succ (IC s)) if ex
d1 being
Element of
SCM-Data-Loc ex
k1 being
Integer st
x = [3,{} ,<*d1,k1*>] SCM-Chg (SCM-Chg s,(x address_1 ),(s . (Address_Add s,(x address_1 ),RetSP ))),
(PopInstrLoc s,(Address_Add s,(x address_1 ),RetIC )) if ex
d1 being
Element of
SCM-Data-Loc st
x = [1,{} ,<*d1*>] SCM-Chg s,
(IFEQ (s . (Address_Add s,(x P31address ),(x P32const ))),0 ,(succ (IC s)),(jump_address s,(x P33const ))) if ex
d1 being
Element of
SCM-Data-Loc ex
k1,
k2 being
Integer st
x = [4,{} ,<*d1,k1,k2*>] SCM-Chg s,
(IFGT (s . (Address_Add s,(x P31address ),(x P32const ))),0 ,(succ (IC s)),(jump_address s,(x P33const ))) if ex
d1 being
Element of
SCM-Data-Loc ex
k1,
k2 being
Integer st
x = [5,{} ,<*d1,k1,k2*>] SCM-Chg s,
(IFGT 0 ,(s . (Address_Add s,(x P31address ),(x P32const ))),(succ (IC s)),(jump_address s,(x P33const ))) if ex
d1 being
Element of
SCM-Data-Loc ex
k1,
k2 being
Integer st
x = [6,{} ,<*d1,k1,k2*>] SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),(x P33const )),
(succ (IC s)) if ex
d1 being
Element of
SCM-Data-Loc ex
k1,
k2 being
Integer st
x = [7,{} ,<*d1,k1,k2*>] SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),((s . (Address_Add s,(x P31address ),(x P32const ))) + (x P33const ))),
(succ (IC s)) if ex
d1 being
Element of
SCM-Data-Loc ex
k1,
k2 being
Integer st
x = [8,{} ,<*d1,k1,k2*>] SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) + (s . (Address_Add s,(x P42address ),(x P44const ))))),
(succ (IC s)) if ex
d1,
d2 being
Element of
SCM-Data-Loc ex
k1,
k2 being
Integer st
x = [9,{} ,<*d1,d2,k1,k2*>] SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) - (s . (Address_Add s,(x P42address ),(x P44const ))))),
(succ (IC s)) if ex
d1,
d2 being
Element of
SCM-Data-Loc ex
k1,
k2 being
Integer st
x = [10,{} ,<*d1,d2,k1,k2*>] SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) * (s . (Address_Add s,(x P42address ),(x P44const ))))),
(succ (IC s)) if ex
d1,
d2 being
Element of
SCM-Data-Loc ex
k1,
k2 being
Integer st
x = [11,{} ,<*d1,d2,k1,k2*>] SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),(s . (Address_Add s,(x P42address ),(x P44const )))),
(succ (IC s)) if ex
d1,
d2 being
Element of
SCM-Data-Loc ex
k1,
k2 being
Integer st
x = [13,{} ,<*d1,d2,k1,k2*>] SCM-Chg (SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) div (s . (Address_Add s,(x P42address ),(x P44const ))))),(Address_Add s,(x P42address ),(x P44const )),((s . (Address_Add s,(x P41address ),(x P43const ))) mod (s . (Address_Add s,(x P42address ),(x P44const ))))),
(succ (IC s)) if ex
d1,
d2 being
Element of
SCM-Data-Loc ex
k1,
k2 being
Integer st
x = [12,{} ,<*d1,d2,k1,k2*>] otherwise s;
coherence
( ( ex k1 being Integer st x = [0 ,{} ,<*k1*>] implies SCM-Chg s,(jump_address s,(x const_INT )) is SCMPDS-State ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [2,{} ,<*d1,k1*>] implies SCM-Chg (SCM-Chg s,(x P21address ),(x P22const )),(succ (IC s)) is SCMPDS-State ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [3,{} ,<*d1,k1*>] implies SCM-Chg (SCM-Chg s,(Address_Add s,(x P21address ),(x P22const )),(IC s)),(succ (IC s)) is SCMPDS-State ) & ( ex d1 being Element of SCM-Data-Loc st x = [1,{} ,<*d1*>] implies SCM-Chg (SCM-Chg s,(x address_1 ),(s . (Address_Add s,(x address_1 ),RetSP ))),(PopInstrLoc s,(Address_Add s,(x address_1 ),RetIC )) is SCMPDS-State ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [4,{} ,<*d1,k1,k2*>] implies SCM-Chg s,(IFEQ (s . (Address_Add s,(x P31address ),(x P32const ))),0 ,(succ (IC s)),(jump_address s,(x P33const ))) is SCMPDS-State ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [5,{} ,<*d1,k1,k2*>] implies SCM-Chg s,(IFGT (s . (Address_Add s,(x P31address ),(x P32const ))),0 ,(succ (IC s)),(jump_address s,(x P33const ))) is SCMPDS-State ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [6,{} ,<*d1,k1,k2*>] implies SCM-Chg s,(IFGT 0 ,(s . (Address_Add s,(x P31address ),(x P32const ))),(succ (IC s)),(jump_address s,(x P33const ))) is SCMPDS-State ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [7,{} ,<*d1,k1,k2*>] implies SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),(x P33const )),(succ (IC s)) is SCMPDS-State ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [8,{} ,<*d1,k1,k2*>] implies SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),((s . (Address_Add s,(x P31address ),(x P32const ))) + (x P33const ))),(succ (IC s)) is SCMPDS-State ) & ( ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [9,{} ,<*d1,d2,k1,k2*>] implies SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) + (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) is SCMPDS-State ) & ( ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [10,{} ,<*d1,d2,k1,k2*>] implies SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) - (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) is SCMPDS-State ) & ( ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [11,{} ,<*d1,d2,k1,k2*>] implies SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) * (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) is SCMPDS-State ) & ( ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [13,{} ,<*d1,d2,k1,k2*>] implies SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),(s . (Address_Add s,(x P42address ),(x P44const )))),(succ (IC s)) is SCMPDS-State ) & ( ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [12,{} ,<*d1,d2,k1,k2*>] implies SCM-Chg (SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) div (s . (Address_Add s,(x P42address ),(x P44const ))))),(Address_Add s,(x P42address ),(x P44const )),((s . (Address_Add s,(x P41address ),(x P43const ))) mod (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) is SCMPDS-State ) & ( ( for k1 being Integer holds not x = [0 ,{} ,<*k1*>] ) & ( for d1 being Element of SCM-Data-Loc
for k1 being Integer holds not x = [2,{} ,<*d1,k1*>] ) & ( for d1 being Element of SCM-Data-Loc
for k1 being Integer holds not x = [3,{} ,<*d1,k1*>] ) & ( for d1 being Element of SCM-Data-Loc holds not x = [1,{} ,<*d1*>] ) & ( for d1 being Element of SCM-Data-Loc
for k1, k2 being Integer holds not x = [4,{} ,<*d1,k1,k2*>] ) & ( for d1 being Element of SCM-Data-Loc
for k1, k2 being Integer holds not x = [5,{} ,<*d1,k1,k2*>] ) & ( for d1 being Element of SCM-Data-Loc
for k1, k2 being Integer holds not x = [6,{} ,<*d1,k1,k2*>] ) & ( for d1 being Element of SCM-Data-Loc
for k1, k2 being Integer holds not x = [7,{} ,<*d1,k1,k2*>] ) & ( for d1 being Element of SCM-Data-Loc
for k1, k2 being Integer holds not x = [8,{} ,<*d1,k1,k2*>] ) & ( for d1, d2 being Element of SCM-Data-Loc
for k1, k2 being Integer holds not x = [9,{} ,<*d1,d2,k1,k2*>] ) & ( for d1, d2 being Element of SCM-Data-Loc
for k1, k2 being Integer holds not x = [10,{} ,<*d1,d2,k1,k2*>] ) & ( for d1, d2 being Element of SCM-Data-Loc
for k1, k2 being Integer holds not x = [11,{} ,<*d1,d2,k1,k2*>] ) & ( for d1, d2 being Element of SCM-Data-Loc
for k1, k2 being Integer holds not x = [13,{} ,<*d1,d2,k1,k2*>] ) & ( for d1, d2 being Element of SCM-Data-Loc
for k1, k2 being Integer holds not x = [12,{} ,<*d1,d2,k1,k2*>] ) implies s is SCMPDS-State ) )
;
consistency
for b1 being SCMPDS-State holds
( ( ex k1 being Integer st x = [0 ,{} ,<*k1*>] & ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [2,{} ,<*d1,k1*>] implies ( b1 = SCM-Chg s,(jump_address s,(x const_INT )) iff b1 = SCM-Chg (SCM-Chg s,(x P21address ),(x P22const )),(succ (IC s)) ) ) & ( ex k1 being Integer st x = [0 ,{} ,<*k1*>] & ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [3,{} ,<*d1,k1*>] implies ( b1 = SCM-Chg s,(jump_address s,(x const_INT )) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P21address ),(x P22const )),(IC s)),(succ (IC s)) ) ) & ( ex k1 being Integer st x = [0 ,{} ,<*k1*>] & ex d1 being Element of SCM-Data-Loc st x = [1,{} ,<*d1*>] implies ( b1 = SCM-Chg s,(jump_address s,(x const_INT )) iff b1 = SCM-Chg (SCM-Chg s,(x address_1 ),(s . (Address_Add s,(x address_1 ),RetSP ))),(PopInstrLoc s,(Address_Add s,(x address_1 ),RetIC )) ) ) & ( ex k1 being Integer st x = [0 ,{} ,<*k1*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [4,{} ,<*d1,k1,k2*>] implies ( b1 = SCM-Chg s,(jump_address s,(x const_INT )) iff b1 = SCM-Chg s,(IFEQ (s . (Address_Add s,(x P31address ),(x P32const ))),0 ,(succ (IC s)),(jump_address s,(x P33const ))) ) ) & ( ex k1 being Integer st x = [0 ,{} ,<*k1*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [5,{} ,<*d1,k1,k2*>] implies ( b1 = SCM-Chg s,(jump_address s,(x const_INT )) iff b1 = SCM-Chg s,(IFGT (s . (Address_Add s,(x P31address ),(x P32const ))),0 ,(succ (IC s)),(jump_address s,(x P33const ))) ) ) & ( ex k1 being Integer st x = [0 ,{} ,<*k1*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [6,{} ,<*d1,k1,k2*>] implies ( b1 = SCM-Chg s,(jump_address s,(x const_INT )) iff b1 = SCM-Chg s,(IFGT 0 ,(s . (Address_Add s,(x P31address ),(x P32const ))),(succ (IC s)),(jump_address s,(x P33const ))) ) ) & ( ex k1 being Integer st x = [0 ,{} ,<*k1*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [7,{} ,<*d1,k1,k2*>] implies ( b1 = SCM-Chg s,(jump_address s,(x const_INT )) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),(x P33const )),(succ (IC s)) ) ) & ( ex k1 being Integer st x = [0 ,{} ,<*k1*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [8,{} ,<*d1,k1,k2*>] implies ( b1 = SCM-Chg s,(jump_address s,(x const_INT )) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),((s . (Address_Add s,(x P31address ),(x P32const ))) + (x P33const ))),(succ (IC s)) ) ) & ( ex k1 being Integer st x = [0 ,{} ,<*k1*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [9,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg s,(jump_address s,(x const_INT )) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) + (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) ) & ( ex k1 being Integer st x = [0 ,{} ,<*k1*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [10,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg s,(jump_address s,(x const_INT )) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) - (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) ) & ( ex k1 being Integer st x = [0 ,{} ,<*k1*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [11,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg s,(jump_address s,(x const_INT )) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) * (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) ) & ( ex k1 being Integer st x = [0 ,{} ,<*k1*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [13,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg s,(jump_address s,(x const_INT )) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),(s . (Address_Add s,(x P42address ),(x P44const )))),(succ (IC s)) ) ) & ( ex k1 being Integer st x = [0 ,{} ,<*k1*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [12,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg s,(jump_address s,(x const_INT )) iff b1 = SCM-Chg (SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) div (s . (Address_Add s,(x P42address ),(x P44const ))))),(Address_Add s,(x P42address ),(x P44const )),((s . (Address_Add s,(x P41address ),(x P43const ))) mod (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [2,{} ,<*d1,k1*>] & ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [3,{} ,<*d1,k1*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x P21address ),(x P22const )),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P21address ),(x P22const )),(IC s)),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [2,{} ,<*d1,k1*>] & ex d1 being Element of SCM-Data-Loc st x = [1,{} ,<*d1*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x P21address ),(x P22const )),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(x address_1 ),(s . (Address_Add s,(x address_1 ),RetSP ))),(PopInstrLoc s,(Address_Add s,(x address_1 ),RetIC )) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [2,{} ,<*d1,k1*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [4,{} ,<*d1,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x P21address ),(x P22const )),(succ (IC s)) iff b1 = SCM-Chg s,(IFEQ (s . (Address_Add s,(x P31address ),(x P32const ))),0 ,(succ (IC s)),(jump_address s,(x P33const ))) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [2,{} ,<*d1,k1*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [5,{} ,<*d1,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x P21address ),(x P22const )),(succ (IC s)) iff b1 = SCM-Chg s,(IFGT (s . (Address_Add s,(x P31address ),(x P32const ))),0 ,(succ (IC s)),(jump_address s,(x P33const ))) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [2,{} ,<*d1,k1*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [6,{} ,<*d1,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x P21address ),(x P22const )),(succ (IC s)) iff b1 = SCM-Chg s,(IFGT 0 ,(s . (Address_Add s,(x P31address ),(x P32const ))),(succ (IC s)),(jump_address s,(x P33const ))) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [2,{} ,<*d1,k1*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [7,{} ,<*d1,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x P21address ),(x P22const )),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),(x P33const )),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [2,{} ,<*d1,k1*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [8,{} ,<*d1,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x P21address ),(x P22const )),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),((s . (Address_Add s,(x P31address ),(x P32const ))) + (x P33const ))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [2,{} ,<*d1,k1*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [9,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x P21address ),(x P22const )),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) + (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [2,{} ,<*d1,k1*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [10,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x P21address ),(x P22const )),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) - (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [2,{} ,<*d1,k1*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [11,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x P21address ),(x P22const )),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) * (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [2,{} ,<*d1,k1*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [13,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x P21address ),(x P22const )),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),(s . (Address_Add s,(x P42address ),(x P44const )))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [2,{} ,<*d1,k1*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [12,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x P21address ),(x P22const )),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) div (s . (Address_Add s,(x P42address ),(x P44const ))))),(Address_Add s,(x P42address ),(x P44const )),((s . (Address_Add s,(x P41address ),(x P43const ))) mod (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [3,{} ,<*d1,k1*>] & ex d1 being Element of SCM-Data-Loc st x = [1,{} ,<*d1*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P21address ),(x P22const )),(IC s)),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(x address_1 ),(s . (Address_Add s,(x address_1 ),RetSP ))),(PopInstrLoc s,(Address_Add s,(x address_1 ),RetIC )) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [3,{} ,<*d1,k1*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [4,{} ,<*d1,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P21address ),(x P22const )),(IC s)),(succ (IC s)) iff b1 = SCM-Chg s,(IFEQ (s . (Address_Add s,(x P31address ),(x P32const ))),0 ,(succ (IC s)),(jump_address s,(x P33const ))) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [3,{} ,<*d1,k1*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [5,{} ,<*d1,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P21address ),(x P22const )),(IC s)),(succ (IC s)) iff b1 = SCM-Chg s,(IFGT (s . (Address_Add s,(x P31address ),(x P32const ))),0 ,(succ (IC s)),(jump_address s,(x P33const ))) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [3,{} ,<*d1,k1*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [6,{} ,<*d1,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P21address ),(x P22const )),(IC s)),(succ (IC s)) iff b1 = SCM-Chg s,(IFGT 0 ,(s . (Address_Add s,(x P31address ),(x P32const ))),(succ (IC s)),(jump_address s,(x P33const ))) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [3,{} ,<*d1,k1*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [7,{} ,<*d1,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P21address ),(x P22const )),(IC s)),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),(x P33const )),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [3,{} ,<*d1,k1*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [8,{} ,<*d1,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P21address ),(x P22const )),(IC s)),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),((s . (Address_Add s,(x P31address ),(x P32const ))) + (x P33const ))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [3,{} ,<*d1,k1*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [9,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P21address ),(x P22const )),(IC s)),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) + (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [3,{} ,<*d1,k1*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [10,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P21address ),(x P22const )),(IC s)),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) - (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [3,{} ,<*d1,k1*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [11,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P21address ),(x P22const )),(IC s)),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) * (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [3,{} ,<*d1,k1*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [13,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P21address ),(x P22const )),(IC s)),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),(s . (Address_Add s,(x P42address ),(x P44const )))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [3,{} ,<*d1,k1*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [12,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P21address ),(x P22const )),(IC s)),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) div (s . (Address_Add s,(x P42address ),(x P44const ))))),(Address_Add s,(x P42address ),(x P44const )),((s . (Address_Add s,(x P41address ),(x P43const ))) mod (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc st x = [1,{} ,<*d1*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [4,{} ,<*d1,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),(s . (Address_Add s,(x address_1 ),RetSP ))),(PopInstrLoc s,(Address_Add s,(x address_1 ),RetIC )) iff b1 = SCM-Chg s,(IFEQ (s . (Address_Add s,(x P31address ),(x P32const ))),0 ,(succ (IC s)),(jump_address s,(x P33const ))) ) ) & ( ex d1 being Element of SCM-Data-Loc st x = [1,{} ,<*d1*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [5,{} ,<*d1,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),(s . (Address_Add s,(x address_1 ),RetSP ))),(PopInstrLoc s,(Address_Add s,(x address_1 ),RetIC )) iff b1 = SCM-Chg s,(IFGT (s . (Address_Add s,(x P31address ),(x P32const ))),0 ,(succ (IC s)),(jump_address s,(x P33const ))) ) ) & ( ex d1 being Element of SCM-Data-Loc st x = [1,{} ,<*d1*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [6,{} ,<*d1,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),(s . (Address_Add s,(x address_1 ),RetSP ))),(PopInstrLoc s,(Address_Add s,(x address_1 ),RetIC )) iff b1 = SCM-Chg s,(IFGT 0 ,(s . (Address_Add s,(x P31address ),(x P32const ))),(succ (IC s)),(jump_address s,(x P33const ))) ) ) & ( ex d1 being Element of SCM-Data-Loc st x = [1,{} ,<*d1*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [7,{} ,<*d1,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),(s . (Address_Add s,(x address_1 ),RetSP ))),(PopInstrLoc s,(Address_Add s,(x address_1 ),RetIC )) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),(x P33const )),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc st x = [1,{} ,<*d1*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [8,{} ,<*d1,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),(s . (Address_Add s,(x address_1 ),RetSP ))),(PopInstrLoc s,(Address_Add s,(x address_1 ),RetIC )) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),((s . (Address_Add s,(x P31address ),(x P32const ))) + (x P33const ))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc st x = [1,{} ,<*d1*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [9,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),(s . (Address_Add s,(x address_1 ),RetSP ))),(PopInstrLoc s,(Address_Add s,(x address_1 ),RetIC )) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) + (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc st x = [1,{} ,<*d1*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [10,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),(s . (Address_Add s,(x address_1 ),RetSP ))),(PopInstrLoc s,(Address_Add s,(x address_1 ),RetIC )) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) - (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc st x = [1,{} ,<*d1*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [11,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),(s . (Address_Add s,(x address_1 ),RetSP ))),(PopInstrLoc s,(Address_Add s,(x address_1 ),RetIC )) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) * (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc st x = [1,{} ,<*d1*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [13,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),(s . (Address_Add s,(x address_1 ),RetSP ))),(PopInstrLoc s,(Address_Add s,(x address_1 ),RetIC )) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),(s . (Address_Add s,(x P42address ),(x P44const )))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc st x = [1,{} ,<*d1*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [12,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),(s . (Address_Add s,(x address_1 ),RetSP ))),(PopInstrLoc s,(Address_Add s,(x address_1 ),RetIC )) iff b1 = SCM-Chg (SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) div (s . (Address_Add s,(x P42address ),(x P44const ))))),(Address_Add s,(x P42address ),(x P44const )),((s . (Address_Add s,(x P41address ),(x P43const ))) mod (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [4,{} ,<*d1,k1,k2*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [5,{} ,<*d1,k1,k2*>] implies ( b1 = SCM-Chg s,(IFEQ (s . (Address_Add s,(x P31address ),(x P32const ))),0 ,(succ (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg s,(IFGT (s . (Address_Add s,(x P31address ),(x P32const ))),0 ,(succ (IC s)),(jump_address s,(x P33const ))) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [4,{} ,<*d1,k1,k2*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [6,{} ,<*d1,k1,k2*>] implies ( b1 = SCM-Chg s,(IFEQ (s . (Address_Add s,(x P31address ),(x P32const ))),0 ,(succ (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg s,(IFGT 0 ,(s . (Address_Add s,(x P31address ),(x P32const ))),(succ (IC s)),(jump_address s,(x P33const ))) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [4,{} ,<*d1,k1,k2*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [7,{} ,<*d1,k1,k2*>] implies ( b1 = SCM-Chg s,(IFEQ (s . (Address_Add s,(x P31address ),(x P32const ))),0 ,(succ (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),(x P33const )),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [4,{} ,<*d1,k1,k2*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [8,{} ,<*d1,k1,k2*>] implies ( b1 = SCM-Chg s,(IFEQ (s . (Address_Add s,(x P31address ),(x P32const ))),0 ,(succ (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),((s . (Address_Add s,(x P31address ),(x P32const ))) + (x P33const ))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [4,{} ,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [9,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg s,(IFEQ (s . (Address_Add s,(x P31address ),(x P32const ))),0 ,(succ (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) + (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [4,{} ,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [10,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg s,(IFEQ (s . (Address_Add s,(x P31address ),(x P32const ))),0 ,(succ (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) - (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [4,{} ,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [11,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg s,(IFEQ (s . (Address_Add s,(x P31address ),(x P32const ))),0 ,(succ (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) * (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [4,{} ,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [13,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg s,(IFEQ (s . (Address_Add s,(x P31address ),(x P32const ))),0 ,(succ (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),(s . (Address_Add s,(x P42address ),(x P44const )))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [4,{} ,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [12,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg s,(IFEQ (s . (Address_Add s,(x P31address ),(x P32const ))),0 ,(succ (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg (SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) div (s . (Address_Add s,(x P42address ),(x P44const ))))),(Address_Add s,(x P42address ),(x P44const )),((s . (Address_Add s,(x P41address ),(x P43const ))) mod (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [5,{} ,<*d1,k1,k2*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [6,{} ,<*d1,k1,k2*>] implies ( b1 = SCM-Chg s,(IFGT (s . (Address_Add s,(x P31address ),(x P32const ))),0 ,(succ (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg s,(IFGT 0 ,(s . (Address_Add s,(x P31address ),(x P32const ))),(succ (IC s)),(jump_address s,(x P33const ))) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [5,{} ,<*d1,k1,k2*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [7,{} ,<*d1,k1,k2*>] implies ( b1 = SCM-Chg s,(IFGT (s . (Address_Add s,(x P31address ),(x P32const ))),0 ,(succ (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),(x P33const )),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [5,{} ,<*d1,k1,k2*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [8,{} ,<*d1,k1,k2*>] implies ( b1 = SCM-Chg s,(IFGT (s . (Address_Add s,(x P31address ),(x P32const ))),0 ,(succ (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),((s . (Address_Add s,(x P31address ),(x P32const ))) + (x P33const ))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [5,{} ,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [9,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg s,(IFGT (s . (Address_Add s,(x P31address ),(x P32const ))),0 ,(succ (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) + (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [5,{} ,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [10,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg s,(IFGT (s . (Address_Add s,(x P31address ),(x P32const ))),0 ,(succ (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) - (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [5,{} ,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [11,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg s,(IFGT (s . (Address_Add s,(x P31address ),(x P32const ))),0 ,(succ (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) * (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [5,{} ,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [13,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg s,(IFGT (s . (Address_Add s,(x P31address ),(x P32const ))),0 ,(succ (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),(s . (Address_Add s,(x P42address ),(x P44const )))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [5,{} ,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [12,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg s,(IFGT (s . (Address_Add s,(x P31address ),(x P32const ))),0 ,(succ (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg (SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) div (s . (Address_Add s,(x P42address ),(x P44const ))))),(Address_Add s,(x P42address ),(x P44const )),((s . (Address_Add s,(x P41address ),(x P43const ))) mod (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [6,{} ,<*d1,k1,k2*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [7,{} ,<*d1,k1,k2*>] implies ( b1 = SCM-Chg s,(IFGT 0 ,(s . (Address_Add s,(x P31address ),(x P32const ))),(succ (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),(x P33const )),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [6,{} ,<*d1,k1,k2*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [8,{} ,<*d1,k1,k2*>] implies ( b1 = SCM-Chg s,(IFGT 0 ,(s . (Address_Add s,(x P31address ),(x P32const ))),(succ (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),((s . (Address_Add s,(x P31address ),(x P32const ))) + (x P33const ))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [6,{} ,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [9,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg s,(IFGT 0 ,(s . (Address_Add s,(x P31address ),(x P32const ))),(succ (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) + (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [6,{} ,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [10,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg s,(IFGT 0 ,(s . (Address_Add s,(x P31address ),(x P32const ))),(succ (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) - (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [6,{} ,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [11,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg s,(IFGT 0 ,(s . (Address_Add s,(x P31address ),(x P32const ))),(succ (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) * (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [6,{} ,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [13,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg s,(IFGT 0 ,(s . (Address_Add s,(x P31address ),(x P32const ))),(succ (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),(s . (Address_Add s,(x P42address ),(x P44const )))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [6,{} ,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [12,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg s,(IFGT 0 ,(s . (Address_Add s,(x P31address ),(x P32const ))),(succ (IC s)),(jump_address s,(x P33const ))) iff b1 = SCM-Chg (SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) div (s . (Address_Add s,(x P42address ),(x P44const ))))),(Address_Add s,(x P42address ),(x P44const )),((s . (Address_Add s,(x P41address ),(x P43const ))) mod (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [7,{} ,<*d1,k1,k2*>] & ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [8,{} ,<*d1,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),(x P33const )),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),((s . (Address_Add s,(x P31address ),(x P32const ))) + (x P33const ))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [7,{} ,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [9,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),(x P33const )),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) + (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [7,{} ,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [10,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),(x P33const )),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) - (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [7,{} ,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [11,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),(x P33const )),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) * (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [7,{} ,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [13,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),(x P33const )),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),(s . (Address_Add s,(x P42address ),(x P44const )))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [7,{} ,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [12,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),(x P33const )),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) div (s . (Address_Add s,(x P42address ),(x P44const ))))),(Address_Add s,(x P42address ),(x P44const )),((s . (Address_Add s,(x P41address ),(x P43const ))) mod (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [8,{} ,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [9,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),((s . (Address_Add s,(x P31address ),(x P32const ))) + (x P33const ))),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) + (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [8,{} ,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [10,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),((s . (Address_Add s,(x P31address ),(x P32const ))) + (x P33const ))),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) - (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [8,{} ,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [11,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),((s . (Address_Add s,(x P31address ),(x P32const ))) + (x P33const ))),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) * (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [8,{} ,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [13,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),((s . (Address_Add s,(x P31address ),(x P32const ))) + (x P33const ))),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),(s . (Address_Add s,(x P42address ),(x P44const )))),(succ (IC s)) ) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [8,{} ,<*d1,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [12,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),((s . (Address_Add s,(x P31address ),(x P32const ))) + (x P33const ))),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) div (s . (Address_Add s,(x P42address ),(x P44const ))))),(Address_Add s,(x P42address ),(x P44const )),((s . (Address_Add s,(x P41address ),(x P43const ))) mod (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) ) & ( ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [9,{} ,<*d1,d2,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [10,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) + (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) - (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) ) & ( ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [9,{} ,<*d1,d2,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [11,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) + (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) * (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) ) & ( ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [9,{} ,<*d1,d2,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [13,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) + (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),(s . (Address_Add s,(x P42address ),(x P44const )))),(succ (IC s)) ) ) & ( ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [9,{} ,<*d1,d2,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [12,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) + (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) div (s . (Address_Add s,(x P42address ),(x P44const ))))),(Address_Add s,(x P42address ),(x P44const )),((s . (Address_Add s,(x P41address ),(x P43const ))) mod (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) ) & ( ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [10,{} ,<*d1,d2,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [11,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) - (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) * (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) ) & ( ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [10,{} ,<*d1,d2,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [13,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) - (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),(s . (Address_Add s,(x P42address ),(x P44const )))),(succ (IC s)) ) ) & ( ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [10,{} ,<*d1,d2,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [12,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) - (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) div (s . (Address_Add s,(x P42address ),(x P44const ))))),(Address_Add s,(x P42address ),(x P44const )),((s . (Address_Add s,(x P41address ),(x P43const ))) mod (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) ) & ( ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [11,{} ,<*d1,d2,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [13,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) * (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),(s . (Address_Add s,(x P42address ),(x P44const )))),(succ (IC s)) ) ) & ( ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [11,{} ,<*d1,d2,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [12,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) * (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) div (s . (Address_Add s,(x P42address ),(x P44const ))))),(Address_Add s,(x P42address ),(x P44const )),((s . (Address_Add s,(x P41address ),(x P43const ))) mod (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) ) & ( ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [13,{} ,<*d1,d2,k1,k2*>] & ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [12,{} ,<*d1,d2,k1,k2*>] implies ( b1 = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),(s . (Address_Add s,(x P42address ),(x P44const )))),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) div (s . (Address_Add s,(x P42address ),(x P44const ))))),(Address_Add s,(x P42address ),(x P44const )),((s . (Address_Add s,(x P41address ),(x P43const ))) mod (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) ) )
by MCART_1:28;
end;
:: deftheorem defines SCM-Exec-Res SCMPDS_1:def 24 :
for x being Element of SCMPDS-Instr
for s being SCMPDS-State holds
( ( ex k1 being Integer st x = [0 ,{} ,<*k1*>] implies SCM-Exec-Res x,s = SCM-Chg s,(jump_address s,(x const_INT )) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [2,{} ,<*d1,k1*>] implies SCM-Exec-Res x,s = SCM-Chg (SCM-Chg s,(x P21address ),(x P22const )),(succ (IC s)) ) & ( ex d1 being Element of SCM-Data-Loc ex k1 being Integer st x = [3,{} ,<*d1,k1*>] implies SCM-Exec-Res x,s = SCM-Chg (SCM-Chg s,(Address_Add s,(x P21address ),(x P22const )),(IC s)),(succ (IC s)) ) & ( ex d1 being Element of SCM-Data-Loc st x = [1,{} ,<*d1*>] implies SCM-Exec-Res x,s = SCM-Chg (SCM-Chg s,(x address_1 ),(s . (Address_Add s,(x address_1 ),RetSP ))),(PopInstrLoc s,(Address_Add s,(x address_1 ),RetIC )) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [4,{} ,<*d1,k1,k2*>] implies SCM-Exec-Res x,s = SCM-Chg s,(IFEQ (s . (Address_Add s,(x P31address ),(x P32const ))),0 ,(succ (IC s)),(jump_address s,(x P33const ))) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [5,{} ,<*d1,k1,k2*>] implies SCM-Exec-Res x,s = SCM-Chg s,(IFGT (s . (Address_Add s,(x P31address ),(x P32const ))),0 ,(succ (IC s)),(jump_address s,(x P33const ))) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [6,{} ,<*d1,k1,k2*>] implies SCM-Exec-Res x,s = SCM-Chg s,(IFGT 0 ,(s . (Address_Add s,(x P31address ),(x P32const ))),(succ (IC s)),(jump_address s,(x P33const ))) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [7,{} ,<*d1,k1,k2*>] implies SCM-Exec-Res x,s = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),(x P33const )),(succ (IC s)) ) & ( ex d1 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [8,{} ,<*d1,k1,k2*>] implies SCM-Exec-Res x,s = SCM-Chg (SCM-Chg s,(Address_Add s,(x P31address ),(x P32const )),((s . (Address_Add s,(x P31address ),(x P32const ))) + (x P33const ))),(succ (IC s)) ) & ( ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [9,{} ,<*d1,d2,k1,k2*>] implies SCM-Exec-Res x,s = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) + (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) & ( ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [10,{} ,<*d1,d2,k1,k2*>] implies SCM-Exec-Res x,s = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) - (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) & ( ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [11,{} ,<*d1,d2,k1,k2*>] implies SCM-Exec-Res x,s = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) * (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) & ( ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [13,{} ,<*d1,d2,k1,k2*>] implies SCM-Exec-Res x,s = SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),(s . (Address_Add s,(x P42address ),(x P44const )))),(succ (IC s)) ) & ( ex d1, d2 being Element of SCM-Data-Loc ex k1, k2 being Integer st x = [12,{} ,<*d1,d2,k1,k2*>] implies SCM-Exec-Res x,s = SCM-Chg (SCM-Chg (SCM-Chg s,(Address_Add s,(x P41address ),(x P43const )),((s . (Address_Add s,(x P41address ),(x P43const ))) div (s . (Address_Add s,(x P42address ),(x P44const ))))),(Address_Add s,(x P42address ),(x P44const )),((s . (Address_Add s,(x P41address ),(x P43const ))) mod (s . (Address_Add s,(x P42address ),(x P44const ))))),(succ (IC s)) ) & ( ( for k1 being Integer holds not x = [0 ,{} ,<*k1*>] ) & ( for d1 being Element of SCM-Data-Loc
for k1 being Integer holds not x = [2,{} ,<*d1,k1*>] ) & ( for d1 being Element of SCM-Data-Loc
for k1 being Integer holds not x = [3,{} ,<*d1,k1*>] ) & ( for d1 being Element of SCM-Data-Loc holds not x = [1,{} ,<*d1*>] ) & ( for d1 being Element of SCM-Data-Loc
for k1, k2 being Integer holds not x = [4,{} ,<*d1,k1,k2*>] ) & ( for d1 being Element of SCM-Data-Loc
for k1, k2 being Integer holds not x = [5,{} ,<*d1,k1,k2*>] ) & ( for d1 being Element of SCM-Data-Loc
for k1, k2 being Integer holds not x = [6,{} ,<*d1,k1,k2*>] ) & ( for d1 being Element of SCM-Data-Loc
for k1, k2 being Integer holds not x = [7,{} ,<*d1,k1,k2*>] ) & ( for d1 being Element of SCM-Data-Loc
for k1, k2 being Integer holds not x = [8,{} ,<*d1,k1,k2*>] ) & ( for d1, d2 being Element of SCM-Data-Loc
for k1, k2 being Integer holds not x = [9,{} ,<*d1,d2,k1,k2*>] ) & ( for d1, d2 being Element of SCM-Data-Loc
for k1, k2 being Integer holds not x = [10,{} ,<*d1,d2,k1,k2*>] ) & ( for d1, d2 being Element of SCM-Data-Loc
for k1, k2 being Integer holds not x = [11,{} ,<*d1,d2,k1,k2*>] ) & ( for d1, d2 being Element of SCM-Data-Loc
for k1, k2 being Integer holds not x = [13,{} ,<*d1,d2,k1,k2*>] ) & ( for d1, d2 being Element of SCM-Data-Loc
for k1, k2 being Integer holds not x = [12,{} ,<*d1,d2,k1,k2*>] ) implies SCM-Exec-Res x,s = s ) );
:: deftheorem defines SCMPDS-Exec SCMPDS_1:def 25 :
for b1 being Action of SCMPDS-Instr ,(product SCMPDS-OK ) holds
( b1 = SCMPDS-Exec iff for x being Element of SCMPDS-Instr
for y being SCMPDS-State holds (b1 . x) . y = SCM-Exec-Res x,y );