environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, AMI_2, XBOOLE_0, TARSKI, CARD_1, FINSEQ_1, ZFMISC_1, RELAT_1, AMI_1, XXREAL_0, FUNCT_1, PARTFUN1, SCMFSA_1, RECDEF_2, UNIALG_1, AMISTD_2, VALUED_0, COMPOS_0;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, XFAMILY, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, MCART_1, RELAT_1, FUNCT_1, PARTFUN1, VALUED_0, FINSEQ_1, XXREAL_0, RECDEF_2, COMPOS_0, SCM_INST;
definitions TARSKI, XBOOLE_0, FINSEQ_1, COMPOS_0;
theorems TARSKI, FINSEQ_1, FINSEQ_4, MCART_1, XBOOLE_0, XBOOLE_1, NUMBERS, NAT_1, COMPOS_0, SCM_INST, XTUPLE_0;
schemes ;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, XREAL_0, FINSEQ_1, GR_CY_1, RELAT_1, COMPOS_0, SCM_INST, VALUED_0, XTUPLE_0, CARD_1;
constructors HIDDEN, AMI_3, VALUED_0, XTUPLE_0, NUMBERS, XFAMILY;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET;
equalities COMPOS_0, XTUPLE_0, ORDINAL1;
expansions TARSKI, COMPOS_0;
definition
func SCM+FSA-Instr -> non
empty set equals
(SCM-Instr \/ { [J,{},<*c,f,b*>] where J is Element of Segm 13, b, c 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, b, c 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, b, c 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 )
by A1;
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 )
by A1;
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 )
by A1;
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 )
by A1;
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 )
by A1;
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 & not not
InsCode x = 0 & ... & not
InsCode x = 8 ) or (
x in { [J,{},<*c,f,b*>] where J is Element of Segm 13, b, c 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)