:: by JingChao Chen

::

:: Received June 15, 1999

:: Copyright (c) 1999-2012 Association of Mizar Users

begin

begin

definition

(((({[0,{},{}]} \/ { [14,{},<*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 15, 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 15, 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 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } is set ;

end;

func SCMPDS-Instr -> set equals :: SCMPDS_I:def 1

(((({[0,{},{}]} \/ { [14,{},<*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 15, 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 15, 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 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } ;

coherence (((({[0,{},{}]} \/ { [14,{},<*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 15, 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 15, 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 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } ;

(((({[0,{},{}]} \/ { [14,{},<*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 15, 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 15, 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 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } is set ;

:: deftheorem defines SCMPDS-Instr SCMPDS_I:def 1 :

SCMPDS-Instr = (((({[0,{},{}]} \/ { [14,{},<*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 15, 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 15, 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 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } ;

SCMPDS-Instr = (((({[0,{},{}]} \/ { [14,{},<*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 15, 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 15, 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 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } ;

Lm1: [0,{},{}] in SCMPDS-Instr

proof end;

definition

let d be Element of SCM-Data-Loc ;

let s be Integer;

:: original: <*

redefine func <*d,s*> -> FinSequence of SCM-Data-Loc \/ INT;

coherence

<*d,s*> is FinSequence of SCM-Data-Loc \/ INT

end;
let s be Integer;

:: original: <*

redefine func <*d,s*> -> FinSequence of SCM-Data-Loc \/ INT;

coherence

<*d,s*> is FinSequence of SCM-Data-Loc \/ INT

proof end;

definition

let x be Element of SCMPDS-Instr ;

given mk being Element of SCM-Data-Loc , I being Element of Segm 15 such that A1: x = [I,{},<*mk*>] ;

ex b_{1} being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc st

( f = x `3_3 & b_{1} = f /. 1 )

for b_{1}, b_{2} being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc st

( f = x `3_3 & b_{1} = f /. 1 ) & ex f being FinSequence of SCM-Data-Loc st

( f = x `3_3 & b_{2} = f /. 1 ) holds

b_{1} = b_{2}
;

end;
given mk being Element of SCM-Data-Loc , I being Element of Segm 15 such that A1: x = [I,{},<*mk*>] ;

func x address_1 -> Element of SCM-Data-Loc means :Def2: :: SCMPDS_I:def 2

ex f being FinSequence of SCM-Data-Loc st

( f = x `3_3 & it = f /. 1 );

existence ex f being FinSequence of SCM-Data-Loc st

( f = x `3_3 & it = f /. 1 );

ex b

( f = x `3_3 & b

proof end;

uniqueness for b

( f = x `3_3 & b

( f = x `3_3 & b

b

:: deftheorem Def2 defines address_1 SCMPDS_I:def 2 :

for x being Element of SCMPDS-Instr st ex mk being Element of SCM-Data-Loc ex I being Element of Segm 15 st x = [I,{},<*mk*>] holds

for b_{2} being Element of SCM-Data-Loc holds

( b_{2} = x address_1 iff ex f being FinSequence of SCM-Data-Loc st

( f = x `3_3 & b_{2} = f /. 1 ) );

for x being Element of SCMPDS-Instr st ex mk being Element of SCM-Data-Loc ex I being Element of Segm 15 st x = [I,{},<*mk*>] holds

for b

( b

( f = x `3_3 & b

theorem :: SCMPDS_I:3

for I being Element of Segm 15

for x being Element of SCMPDS-Instr

for mk being Element of SCM-Data-Loc st x = [I,{},<*mk*>] holds

x address_1 = mk

for x being Element of SCMPDS-Instr

for mk being Element of SCM-Data-Loc st x = [I,{},<*mk*>] holds

x address_1 = mk

proof end;

definition

let x be Element of SCMPDS-Instr ;

given r being Integer, I being Element of Segm 15 such that A1: x = [I,{},<*r*>] ;

ex b_{1} being Integer ex f being FinSequence of INT st

( f = x `3_3 & b_{1} = f /. 1 )

for b_{1}, b_{2} being Integer st ex f being FinSequence of INT st

( f = x `3_3 & b_{1} = f /. 1 ) & ex f being FinSequence of INT st

( f = x `3_3 & b_{2} = f /. 1 ) holds

b_{1} = b_{2}
;

end;
given r being Integer, I being Element of Segm 15 such that A1: x = [I,{},<*r*>] ;

func x const_INT -> Integer means :Def3: :: SCMPDS_I:def 3

ex f being FinSequence of INT st

( f = x `3_3 & it = f /. 1 );

existence ex f being FinSequence of INT st

( f = x `3_3 & it = f /. 1 );

ex b

( f = x `3_3 & b

proof end;

uniqueness for b

( f = x `3_3 & b

( f = x `3_3 & b

b

:: deftheorem Def3 defines const_INT SCMPDS_I:def 3 :

for x being Element of SCMPDS-Instr st ex r being Integer ex I being Element of Segm 15 st x = [I,{},<*r*>] holds

for b_{2} being Integer holds

( b_{2} = x const_INT iff ex f being FinSequence of INT st

( f = x `3_3 & b_{2} = f /. 1 ) );

for x being Element of SCMPDS-Instr st ex r being Integer ex I being Element of Segm 15 st x = [I,{},<*r*>] holds

for b

( b

( f = x `3_3 & b

theorem :: SCMPDS_I:4

for I being Element of Segm 15

for x being Element of SCMPDS-Instr

for k being Integer st x = [I,{},<*k*>] holds

x const_INT = k

for x being Element of SCMPDS-Instr

for k being Integer st x = [I,{},<*k*>] holds

x const_INT = k

proof end;

definition

let x be Element of SCMPDS-Instr ;

given mk being Element of SCM-Data-Loc , r being Integer, I being Element of Segm 15 such that A1: x = [I,{},<*mk,r*>] ;

ex b_{1} being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & b_{1} = f /. 1 )

for b_{1}, b_{2} being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & b_{1} = f /. 1 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & b_{2} = f /. 1 ) holds

b_{1} = b_{2}
;

ex b_{1} being Integer ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & b_{1} = f /. 2 )

for b_{1}, b_{2} being Integer st ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & b_{1} = f /. 2 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & b_{2} = f /. 2 ) holds

b_{1} = b_{2}
;

end;
given mk being Element of SCM-Data-Loc , r being Integer, I being Element of Segm 15 such that A1: x = [I,{},<*mk,r*>] ;

func x P21address -> Element of SCM-Data-Loc means :Def4: :: SCMPDS_I:def 4

ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & it = f /. 1 );

existence ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & it = f /. 1 );

ex b

( f = x `3_3 & b

proof end;

uniqueness for b

( f = x `3_3 & b

( f = x `3_3 & b

b

func x P22const -> Integer means :Def5: :: SCMPDS_I:def 5

ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & it = f /. 2 );

existence ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & it = f /. 2 );

ex b

( f = x `3_3 & b

proof end;

uniqueness for b

( f = x `3_3 & b

( f = x `3_3 & b

b

:: deftheorem Def4 defines P21address SCMPDS_I:def 4 :

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 15 st x = [I,{},<*mk,r*>] holds

for b_{2} being Element of SCM-Data-Loc holds

( b_{2} = x P21address iff ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & b_{2} = f /. 1 ) );

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 15 st x = [I,{},<*mk,r*>] holds

for b

( b

( f = x `3_3 & b

:: deftheorem Def5 defines P22const SCMPDS_I:def 5 :

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 15 st x = [I,{},<*mk,r*>] holds

for b_{2} being Integer holds

( b_{2} = x P22const iff ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & b_{2} = f /. 2 ) );

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 15 st x = [I,{},<*mk,r*>] holds

for b

( b

( f = x `3_3 & b

theorem :: SCMPDS_I:5

for I being Element of Segm 15

for x being Element of SCMPDS-Instr

for mk being Element of SCM-Data-Loc

for r being Integer st x = [I,{},<*mk,r*>] holds

( x P21address = mk & x P22const = r )

for x being Element of SCMPDS-Instr

for mk being Element of SCM-Data-Loc

for r being Integer st x = [I,{},<*mk,r*>] holds

( x P21address = mk & x P22const = r )

proof end;

definition

let x be Element of SCMPDS-Instr ;

given m1 being Element of SCM-Data-Loc , k1, k2 being Integer, I being Element of Segm 15 such that A1: x = [I,{},<*m1,k1,k2*>] ;

ex b_{1} being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & b_{1} = f /. 1 )

for b_{1}, b_{2} being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & b_{1} = f /. 1 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & b_{2} = f /. 1 ) holds

b_{1} = b_{2}
;

ex b_{1} being Integer ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & b_{1} = f /. 2 )

for b_{1}, b_{2} being Integer st ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & b_{1} = f /. 2 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & b_{2} = f /. 2 ) holds

b_{1} = b_{2}
;

ex b_{1} being Integer ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & b_{1} = f /. 3 )

for b_{1}, b_{2} being Integer st ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & b_{1} = f /. 3 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & b_{2} = f /. 3 ) holds

b_{1} = b_{2}
;

end;
given m1 being Element of SCM-Data-Loc , k1, k2 being Integer, I being Element of Segm 15 such that A1: x = [I,{},<*m1,k1,k2*>] ;

func x P31address -> Element of SCM-Data-Loc means :Def6: :: SCMPDS_I:def 6

ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & it = f /. 1 );

existence ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & it = f /. 1 );

ex b

( f = x `3_3 & b

proof end;

uniqueness for b

( f = x `3_3 & b

( f = x `3_3 & b

b

func x P32const -> Integer means :Def7: :: SCMPDS_I:def 7

ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & it = f /. 2 );

existence ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & it = f /. 2 );

ex b

( f = x `3_3 & b

proof end;

uniqueness for b

( f = x `3_3 & b

( f = x `3_3 & b

b

func x P33const -> Integer means :Def8: :: SCMPDS_I:def 8

ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & it = f /. 3 );

existence ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & it = f /. 3 );

ex b

( f = x `3_3 & b

proof end;

uniqueness for b

( f = x `3_3 & b

( f = x `3_3 & b

b

:: deftheorem Def6 defines P31address SCMPDS_I:def 6 :

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 15 st x = [I,{},<*m1,k1,k2*>] holds

for b_{2} being Element of SCM-Data-Loc holds

( b_{2} = x P31address iff ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & b_{2} = f /. 1 ) );

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 15 st x = [I,{},<*m1,k1,k2*>] holds

for b

( b

( f = x `3_3 & b

:: deftheorem Def7 defines P32const SCMPDS_I:def 7 :

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 15 st x = [I,{},<*m1,k1,k2*>] holds

for b_{2} being Integer holds

( b_{2} = x P32const iff ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & b_{2} = f /. 2 ) );

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 15 st x = [I,{},<*m1,k1,k2*>] holds

for b

( b

( f = x `3_3 & b

:: deftheorem Def8 defines P33const SCMPDS_I:def 8 :

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 15 st x = [I,{},<*m1,k1,k2*>] holds

for b_{2} being Integer holds

( b_{2} = x P33const iff ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & b_{2} = f /. 3 ) );

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 15 st x = [I,{},<*m1,k1,k2*>] holds

for b

( b

( f = x `3_3 & b

theorem :: SCMPDS_I:6

for I being Element of Segm 15

for x being Element of SCMPDS-Instr

for d1 being Element of SCM-Data-Loc

for k1, k2 being Integer st x = [I,{},<*d1,k1,k2*>] holds

( x P31address = d1 & x P32const = k1 & x P33const = k2 )

for x being Element of SCMPDS-Instr

for d1 being Element of SCM-Data-Loc

for k1, k2 being Integer st x = [I,{},<*d1,k1,k2*>] holds

( x P31address = d1 & x P32const = k1 & x P33const = k2 )

proof end;

definition

let x be Element of SCMPDS-Instr ;

given m1, m2 being Element of SCM-Data-Loc , k1, k2 being Integer, I being Element of Segm 15 such that A1: x = [I,{},<*m1,m2,k1,k2*>] ;

ex b_{1} being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & b_{1} = f /. 1 )

for b_{1}, b_{2} being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & b_{1} = f /. 1 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & b_{2} = f /. 1 ) holds

b_{1} = b_{2}
;

ex b_{1} being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & b_{1} = f /. 2 )

for b_{1}, b_{2} being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & b_{1} = f /. 2 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & b_{2} = f /. 2 ) holds

b_{1} = b_{2}
;

ex b_{1} being Integer ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & b_{1} = f /. 3 )

for b_{1}, b_{2} being Integer st ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & b_{1} = f /. 3 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & b_{2} = f /. 3 ) holds

b_{1} = b_{2}
;

ex b_{1} being Integer ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & b_{1} = f /. 4 )

for b_{1}, b_{2} being Integer st ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & b_{1} = f /. 4 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & b_{2} = f /. 4 ) holds

b_{1} = b_{2}
;

end;
given m1, m2 being Element of SCM-Data-Loc , k1, k2 being Integer, I being Element of Segm 15 such that A1: x = [I,{},<*m1,m2,k1,k2*>] ;

func x P41address -> Element of SCM-Data-Loc means :Def9: :: SCMPDS_I:def 9

ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & it = f /. 1 );

existence ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & it = f /. 1 );

ex b

( f = x `3_3 & b

proof end;

uniqueness for b

( f = x `3_3 & b

( f = x `3_3 & b

b

func x P42address -> Element of SCM-Data-Loc means :Def10: :: SCMPDS_I:def 10

ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & it = f /. 2 );

existence ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & it = f /. 2 );

ex b

( f = x `3_3 & b

proof end;

uniqueness for b

( f = x `3_3 & b

( f = x `3_3 & b

b

func x P43const -> Integer means :Def11: :: SCMPDS_I:def 11

ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & it = f /. 3 );

existence ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & it = f /. 3 );

ex b

( f = x `3_3 & b

proof end;

uniqueness for b

( f = x `3_3 & b

( f = x `3_3 & b

b

func x P44const -> Integer means :Def12: :: SCMPDS_I:def 12

ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & it = f /. 4 );

existence ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & it = f /. 4 );

ex b

( f = x `3_3 & b

proof end;

uniqueness for b

( f = x `3_3 & b

( f = x `3_3 & b

b

:: deftheorem Def9 defines P41address SCMPDS_I:def 9 :

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 15 st x = [I,{},<*m1,m2,k1,k2*>] holds

for b_{2} being Element of SCM-Data-Loc holds

( b_{2} = x P41address iff ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & b_{2} = f /. 1 ) );

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 15 st x = [I,{},<*m1,m2,k1,k2*>] holds

for b

( b

( f = x `3_3 & b

:: deftheorem Def10 defines P42address SCMPDS_I:def 10 :

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 15 st x = [I,{},<*m1,m2,k1,k2*>] holds

for b_{2} being Element of SCM-Data-Loc holds

( b_{2} = x P42address iff ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & b_{2} = f /. 2 ) );

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 15 st x = [I,{},<*m1,m2,k1,k2*>] holds

for b

( b

( f = x `3_3 & b

:: deftheorem Def11 defines P43const SCMPDS_I:def 11 :

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 15 st x = [I,{},<*m1,m2,k1,k2*>] holds

for b_{2} being Integer holds

( b_{2} = x P43const iff ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & b_{2} = f /. 3 ) );

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 15 st x = [I,{},<*m1,m2,k1,k2*>] holds

for b

( b

( f = x `3_3 & b

:: deftheorem Def12 defines P44const SCMPDS_I:def 12 :

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 15 st x = [I,{},<*m1,m2,k1,k2*>] holds

for b_{2} being Integer holds

( b_{2} = x P44const iff ex f being FinSequence of SCM-Data-Loc \/ INT st

( f = x `3_3 & b_{2} = f /. 4 ) );

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 15 st x = [I,{},<*m1,m2,k1,k2*>] holds

for b

( b

( f = x `3_3 & b

theorem :: SCMPDS_I:7

for I being Element of Segm 15

for x being Element of SCMPDS-Instr

for d1, d2 being Element of SCM-Data-Loc

for k1, k2 being Integer st x = [I,{},<*d1,d2,k1,k2*>] holds

( x P41address = d1 & x P42address = d2 & x P43const = k1 & x P44const = k2 )

for x being Element of SCMPDS-Instr

for d1, d2 being Element of SCM-Data-Loc

for k1, k2 being Integer st x = [I,{},<*d1,d2,k1,k2*>] holds

( x P41address = d1 & x P42address = d2 & x P43const = k1 & x P44const = k2 )

proof end;

:: RetSP: Return Stack Pointer

:: RetIC: Return Instruction-Counter

:: RetIC: Return Instruction-Counter

theorem Th8: :: SCMPDS_I:8

for x being Element of SCMPDS-Instr holds

( ( x in {[0,{},{}]} & InsCode x = 0 ) or ( x in { [14,{},<*l*>] where l is Element of INT : verum } & InsCode x = 14 ) or ( x in { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } & InsCode x = 1 ) or ( x in { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } & ( InsCode x = 2 or InsCode x = 3 ) ) or ( x in { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } & ( InsCode x = 4 or InsCode x = 5 or InsCode x = 6 or InsCode x = 7 or InsCode x = 8 ) ) or ( x in { [I,{},<*v1,v2,c1,c2*>] where I is Element of Segm 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } & ( InsCode x = 9 or InsCode x = 10 or InsCode x = 11 or InsCode x = 12 or InsCode x = 13 ) ) )

( ( x in {[0,{},{}]} & InsCode x = 0 ) or ( x in { [14,{},<*l*>] where l is Element of INT : verum } & InsCode x = 14 ) or ( x in { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } & InsCode x = 1 ) or ( x in { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } & ( InsCode x = 2 or InsCode x = 3 ) ) or ( x in { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } & ( InsCode x = 4 or InsCode x = 5 or InsCode x = 6 or InsCode x = 7 or InsCode x = 8 ) ) or ( x in { [I,{},<*v1,v2,c1,c2*>] where I is Element of Segm 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } & ( InsCode x = 9 or InsCode x = 10 or InsCode x = 11 or InsCode x = 12 or InsCode x = 13 ) ) )

proof end;

begin

registration
end;

Lm2: for l being Element of SCMPDS-Instr holds InsCode l <= 14

proof end;

Lm3: for i being Element of SCMPDS-Instr st InsCode i = 0 holds

JumpPart i = {}

proof end;

Lm4: for i being Element of SCMPDS-Instr st InsCode i = 14 holds

JumpPart i = {}

proof end;

Lm5: for i being Element of SCMPDS-Instr st InsCode i = 1 holds

JumpPart i = {}

proof end;

Lm6: for i being Element of SCMPDS-Instr st ( InsCode i = 2 or InsCode i = 3 ) holds

JumpPart i = {}

proof end;

Lm7: for i being Element of SCMPDS-Instr st ( InsCode i = 4 or InsCode i = 5 or InsCode i = 6 or InsCode i = 7 or InsCode i = 8 ) holds

JumpPart i = {}

proof end;

Lm8: for i being Element of SCMPDS-Instr st ( InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or InsCode i = 13 ) holds

JumpPart i = {}

proof end;

registration
end;

registration
end;

registration
end;

:: [1,return sp<-sp+0,count<-(sp)+2]

:: [2,a:=c(constant)]

:: [3,saveIC (a,k)]

:: [4,if(a,k)<>0 goto L ]

:: [5,if(a,k)<=0 goto L ]

:: [6,if(a,k)>=0 goto L ]

:: [7,(a,k):=c(constant) ]

:: [8,(a,k1)+k2]

:: [9, (a1,k1)+(a2,k2)]

:: [10,(a1,k1)-(a2,k2)]

:: [11,(a1,k1)*(a2,k2)]

:: [12,(a1,k1)/(a2,k2)]

:: [13,(a1,k1):=(a2,k2)]