:: by Andrzej Trybulec , Yatsuka Nakamura and Piotr Rudnicki

::

:: Received February 3, 1996

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

begin

definition
end;

registration
end;

definition

(SCM-Instr \/ { [J,{},<*c,f,b*>] where J is Element of Segm 13, c, b is Element of SCM-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10} } ) \/ { [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12} } is non empty set ;

end;

func SCM+FSA-Instr -> non empty set equals :: SCMFSA_I:def 2

(SCM-Instr \/ { [J,{},<*c,f,b*>] where J is Element of Segm 13, c, b is Element of SCM-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10} } ) \/ { [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12} } ;

coherence (SCM-Instr \/ { [J,{},<*c,f,b*>] where J is Element of Segm 13, c, b is Element of SCM-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10} } ) \/ { [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12} } ;

(SCM-Instr \/ { [J,{},<*c,f,b*>] where J is Element of Segm 13, c, b is Element of SCM-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10} } ) \/ { [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12} } is non empty set ;

:: deftheorem defines SCM+FSA-Instr SCMFSA_I:def 2 :

SCM+FSA-Instr = (SCM-Instr \/ { [J,{},<*c,f,b*>] where J is Element of Segm 13, c, b is Element of SCM-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10} } ) \/ { [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12} } ;

SCM+FSA-Instr = (SCM-Instr \/ { [J,{},<*c,f,b*>] where J is Element of Segm 13, c, b is Element of SCM-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10} } ) \/ { [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12} } ;

Lm1: SCM+FSA-Instr c= [:NAT,(NAT *),(proj2 SCM+FSA-Instr):]

proof end;

registration
end;

theorem Th4: :: SCMFSA_I:4

for x being set

for c, b being Element of SCM-Data-Loc

for f being Element of SCM+FSA-Data*-Loc st x in {9,10} holds

[x,{},<*c,f,b*>] in SCM+FSA-Instr

for c, b being Element of SCM-Data-Loc

for f being Element of SCM+FSA-Data*-Loc st x in {9,10} holds

[x,{},<*c,f,b*>] in SCM+FSA-Instr

proof end;

theorem Th5: :: SCMFSA_I:5

for x being set

for c being Element of SCM-Data-Loc

for f being Element of SCM+FSA-Data*-Loc st x in {11,12} holds

[x,{},<*c,f*>] in SCM+FSA-Instr

for c being Element of SCM-Data-Loc

for f being Element of SCM+FSA-Data*-Loc st x in {11,12} holds

[x,{},<*c,f*>] in SCM+FSA-Instr

proof end;

definition

let x be Element of SCM+FSA-Instr ;

given c being Element of SCM-Data-Loc , f being Element of SCM+FSA-Data*-Loc , b being Element of SCM-Data-Loc , J being Element of Segm 13 such that A1: x = [J,{},<*c,f,b*>] ;

ex b_{1}, c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st

( <*c,f,b*> = x `3_3 & b_{1} = c )

for b_{1}, b_{2} being Element of SCM-Data-Loc st ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st

( <*c,f,b*> = x `3_3 & b_{1} = c ) & ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st

( <*c,f,b*> = x `3_3 & b_{2} = c ) holds

b_{1} = b_{2}

ex b_{1}, c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st

( <*c,f,b*> = x `3_3 & b_{1} = b )

uniqueness

for b_{1}, b_{2} being Element of SCM-Data-Loc st ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st

( <*c,f,b*> = x `3_3 & b_{1} = b ) & ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st

( <*c,f,b*> = x `3_3 & b_{2} = b ) holds

b_{1} = b_{2};

ex b_{1} being Element of SCM+FSA-Data*-Loc ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st

( <*c,f,b*> = x `3_3 & b_{1} = f )

uniqueness

for b_{1}, b_{2} being Element of SCM+FSA-Data*-Loc st ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st

( <*c,f,b*> = x `3_3 & b_{1} = f ) & ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st

( <*c,f,b*> = x `3_3 & b_{2} = f ) holds

b_{1} = b_{2};

end;
given c being Element of SCM-Data-Loc , f being Element of SCM+FSA-Data*-Loc , b being Element of SCM-Data-Loc , J being Element of Segm 13 such that A1: x = [J,{},<*c,f,b*>] ;

func x int_addr1 -> Element of SCM-Data-Loc means :: SCMFSA_I:def 3

ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st

( <*c,f,b*> = x `3_3 & it = c );

existence ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st

( <*c,f,b*> = x `3_3 & it = c );

ex b

( <*c,f,b*> = x `3_3 & b

proof end;

uniqueness for b

( <*c,f,b*> = x `3_3 & b

( <*c,f,b*> = x `3_3 & b

b

proof end;

func x int_addr2 -> Element of SCM-Data-Loc means :: SCMFSA_I:def 4

ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st

( <*c,f,b*> = x `3_3 & it = b );

existence ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st

( <*c,f,b*> = x `3_3 & it = b );

ex b

( <*c,f,b*> = x `3_3 & b

proof end;

correctness uniqueness

for b

( <*c,f,b*> = x `3_3 & b

( <*c,f,b*> = x `3_3 & b

b

proof end;

func x coll_addr1 -> Element of SCM+FSA-Data*-Loc means :: SCMFSA_I:def 5

ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st

( <*c,f,b*> = x `3_3 & it = f );

existence ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st

( <*c,f,b*> = x `3_3 & it = f );

ex b

( <*c,f,b*> = x `3_3 & b

proof end;

correctness uniqueness

for b

( <*c,f,b*> = x `3_3 & b

( <*c,f,b*> = x `3_3 & b

b

proof end;

:: deftheorem defines int_addr1 SCMFSA_I:def 3 :

for x being Element of SCM+FSA-Instr st ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc ex J being Element of Segm 13 st x = [J,{},<*c,f,b*>] holds

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

( b_{2} = x int_addr1 iff ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st

( <*c,f,b*> = x `3_3 & b_{2} = c ) );

for x being Element of SCM+FSA-Instr st ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc ex J being Element of Segm 13 st x = [J,{},<*c,f,b*>] holds

for b

( b

( <*c,f,b*> = x `3_3 & b

:: deftheorem defines int_addr2 SCMFSA_I:def 4 :

for x being Element of SCM+FSA-Instr st ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc ex J being Element of Segm 13 st x = [J,{},<*c,f,b*>] holds

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

( b_{2} = x int_addr2 iff ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st

( <*c,f,b*> = x `3_3 & b_{2} = b ) );

for x being Element of SCM+FSA-Instr st ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc ex J being Element of Segm 13 st x = [J,{},<*c,f,b*>] holds

for b

( b

( <*c,f,b*> = x `3_3 & b

:: deftheorem defines coll_addr1 SCMFSA_I:def 5 :

for x being Element of SCM+FSA-Instr st ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc ex J being Element of Segm 13 st x = [J,{},<*c,f,b*>] holds

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

( b_{2} = x coll_addr1 iff ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st

( <*c,f,b*> = x `3_3 & b_{2} = f ) );

for x being Element of SCM+FSA-Instr st ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc ex J being Element of Segm 13 st x = [J,{},<*c,f,b*>] holds

for b

( b

( <*c,f,b*> = x `3_3 & b

definition

let x be Element of SCM+FSA-Instr ;

given c being Element of SCM-Data-Loc such that A1: x = [13,{},<*c*>] ;

ex b_{1}, c being Element of SCM-Data-Loc st

( <*c*> = x `3_3 & b_{1} = c )

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

( <*c*> = x `3_3 & b_{1} = c ) & ex c being Element of SCM-Data-Loc st

( <*c*> = x `3_3 & b_{2} = c ) holds

b_{1} = b_{2}

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

func x int_addr -> Element of SCM-Data-Loc means :: SCMFSA_I:def 6

ex c being Element of SCM-Data-Loc st

( <*c*> = x `3_3 & it = c );

existence ex c being Element of SCM-Data-Loc st

( <*c*> = x `3_3 & it = c );

ex b

( <*c*> = x `3_3 & b

proof end;

uniqueness for b

( <*c*> = x `3_3 & b

( <*c*> = x `3_3 & b

b

proof end;

:: deftheorem defines int_addr SCMFSA_I:def 6 :

for x being Element of SCM+FSA-Instr st ex c being Element of SCM-Data-Loc st x = [13,{},<*c*>] holds

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

( b_{2} = x int_addr iff ex c being Element of SCM-Data-Loc st

( <*c*> = x `3_3 & b_{2} = c ) );

for x being Element of SCM+FSA-Instr st ex c being Element of SCM-Data-Loc st x = [13,{},<*c*>] holds

for b

( b

( <*c*> = x `3_3 & b

definition

let x be Element of SCM+FSA-Instr ;

given c being Element of SCM-Data-Loc , f being Element of SCM+FSA-Data*-Loc , J being Element of Segm 13 such that A1: x = [J,{},<*c,f*>] ;

ex b_{1}, c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st

( <*c,f*> = x `3_3 & b_{1} = c )

for b_{1}, b_{2} being Element of SCM-Data-Loc st ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st

( <*c,f*> = x `3_3 & b_{1} = c ) & ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st

( <*c,f*> = x `3_3 & b_{2} = c ) holds

b_{1} = b_{2}

ex b_{1} being Element of SCM+FSA-Data*-Loc ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st

( <*c,f*> = x `3_3 & b_{1} = f )

uniqueness

for b_{1}, b_{2} being Element of SCM+FSA-Data*-Loc st ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st

( <*c,f*> = x `3_3 & b_{1} = f ) & ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st

( <*c,f*> = x `3_3 & b_{2} = f ) holds

b_{1} = b_{2};

end;
given c being Element of SCM-Data-Loc , f being Element of SCM+FSA-Data*-Loc , J being Element of Segm 13 such that A1: x = [J,{},<*c,f*>] ;

func x int_addr3 -> Element of SCM-Data-Loc means :: SCMFSA_I:def 7

ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st

( <*c,f*> = x `3_3 & it = c );

existence ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st

( <*c,f*> = x `3_3 & it = c );

ex b

( <*c,f*> = x `3_3 & b

proof end;

uniqueness for b

( <*c,f*> = x `3_3 & b

( <*c,f*> = x `3_3 & b

b

proof end;

func x coll_addr2 -> Element of SCM+FSA-Data*-Loc means :: SCMFSA_I:def 8

ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st

( <*c,f*> = x `3_3 & it = f );

existence ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st

( <*c,f*> = x `3_3 & it = f );

ex b

( <*c,f*> = x `3_3 & b

proof end;

correctness uniqueness

for b

( <*c,f*> = x `3_3 & b

( <*c,f*> = x `3_3 & b

b

proof end;

:: deftheorem defines int_addr3 SCMFSA_I:def 7 :

for x being Element of SCM+FSA-Instr st ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex J being Element of Segm 13 st x = [J,{},<*c,f*>] holds

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

( b_{2} = x int_addr3 iff ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st

( <*c,f*> = x `3_3 & b_{2} = c ) );

for x being Element of SCM+FSA-Instr st ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex J being Element of Segm 13 st x = [J,{},<*c,f*>] holds

for b

( b

( <*c,f*> = x `3_3 & b

:: deftheorem defines coll_addr2 SCMFSA_I:def 8 :

for x being Element of SCM+FSA-Instr st ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex J being Element of Segm 13 st x = [J,{},<*c,f*>] holds

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

( b_{2} = x coll_addr2 iff ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st

( <*c,f*> = x `3_3 & b_{2} = f ) );

for x being Element of SCM+FSA-Instr st ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex J being Element of Segm 13 st x = [J,{},<*c,f*>] holds

for b

( b

( <*c,f*> = x `3_3 & b

theorem Th7: :: SCMFSA_I:7

for x being Element of SCM+FSA-Instr holds

( ( x in SCM-Instr & ( InsCode x = 0 or InsCode x = 1 or InsCode x = 2 or InsCode x = 3 or InsCode x = 4 or InsCode x = 5 or InsCode x = 6 or InsCode x = 7 or InsCode x = 8 ) ) or ( x in { [J,{},<*c,f,b*>] where J is Element of Segm 13, c, b is Element of SCM-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10} } & ( InsCode x = 9 or InsCode x = 10 ) ) or ( x in { [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12} } & ( InsCode x = 11 or InsCode x = 12 ) ) )

( ( x in SCM-Instr & ( InsCode x = 0 or InsCode x = 1 or InsCode x = 2 or InsCode x = 3 or InsCode x = 4 or InsCode x = 5 or InsCode x = 6 or InsCode x = 7 or InsCode x = 8 ) ) or ( x in { [J,{},<*c,f,b*>] where J is Element of Segm 13, c, b is Element of SCM-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10} } & ( InsCode x = 9 or InsCode x = 10 ) ) or ( x in { [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12} } & ( InsCode x = 11 or InsCode x = 12 ) ) )

proof end;

Lm2: for i being Element of SCM+FSA-Instr holds InsCode i <= 12

proof end;

Lm3: for i being Element of SCM+FSA-Instr st ( InsCode i = 9 or InsCode i = 10 ) holds

JumpPart i = {}

proof end;

Lm4: for i being Element of SCM+FSA-Instr st ( InsCode i = 11 or InsCode i = 12 ) holds

JumpPart i = {}

proof end;

registration
end;

Lm5: for i being Element of SCM+FSA-Instr

for ii being Element of SCM-Instr st i = ii holds

JumpParts (InsCode i) = JumpParts (InsCode ii)

proof end;

registration
end;