begin
definition
func SCM+FSA-Instr -> non
empty set equals
(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} } is non empty set
;
end;
::
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} } ;
Lm1:
SCM+FSA-Instr c= [:NAT,(NAT *),(proj2 SCM+FSA-Instr):]
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*>]
;
existence
ex b1, 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 & b1 = c )
uniqueness
for b1, b2 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 & b1 = 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 & b2 = c ) holds
b1 = b2
existence
ex b1, 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 & b1 = b )
correctness
uniqueness
for b1, b2 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 & b1 = 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 & b2 = b ) holds
b1 = b2;
existence
ex b1 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 & b1 = f )
correctness
uniqueness
for b1, b2 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 & b1 = 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 & b2 = f ) holds
b1 = b2;
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 ,
J being
Element of
Segm 13
such that A1:
x = [J,{},<*c,f*>]
;
existence
ex b1, c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `3_3 & b1 = c )
uniqueness
for b1, b2 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 & b1 = c ) & ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `3_3 & b2 = c ) holds
b1 = b2
existence
ex b1 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 & b1 = f )
correctness
uniqueness
for b1, b2 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 & b1 = f ) & ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `3_3 & b2 = f ) holds
b1 = b2;
end;
theorem Th7:
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 ) ) )
Lm2:
for i being Element of SCM+FSA-Instr holds InsCode i <= 12
Lm3:
for i being Element of SCM+FSA-Instr st ( InsCode i = 9 or InsCode i = 10 ) holds
JumpPart i = {}
Lm4:
for i being Element of SCM+FSA-Instr st ( InsCode i = 11 or InsCode i = 12 ) holds
JumpPart i = {}
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)