environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, CARD_1, AMI_2, XBOOLE_0, STRUCT_0, ZFMISC_1, RELAT_1, FINSEQ_1, FUNCSDOM, FUNCT_1, AMI_1, PARTFUN1, TARSKI, SCMRING1, RECDEF_2, ALGSTR_0, UNIALG_1, AMISTD_2, VALUED_0, COMPOS_0, XXREAL_0, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XTUPLE_0, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, VALUED_0, ORDINAL1, CARD_1, RECDEF_2, XXREAL_0, NUMBERS, STRUCT_0, ALGSTR_0, VECTSP_1, MCART_1, FINSEQ_1, FINSEQ_4, COMPOS_0, SCM_INST;
definitions TARSKI, FINSEQ_1, COMPOS_0;
theorems ENUMSET1, FINSEQ_1, FINSEQ_4, FUNCT_1, MCART_1, TARSKI, SUBSET_1, XBOOLE_0, XBOOLE_1, NAT_1, FUNCT_7, COMPOS_0, ORDINAL1, XTUPLE_0;
schemes ;
registrations XBOOLE_0, RELAT_1, ORDINAL1, FINSEQ_1, STRUCT_0, CARD_1, GCD_1, FUNCT_1, ALGSTR_0, ALGSTR_1, COMPOS_0, SCM_INST, XXREAL_0, VALUED_0, XTUPLE_0;
constructors HIDDEN, FINSEQ_4, REALSET2, FINSEQ_2, COMPOS_1, SCM_INST, VALUED_0, XTUPLE_0;
requirements HIDDEN, NUMERALS, REAL, SUBSET, BOOLE;
equalities SCM_INST, XTUPLE_0, ORDINAL1;
expansions TARSKI, COMPOS_0;
definition
let S be non
empty 1-sorted ;
func SCM-Instr S -> non
empty set equals
((({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Nat : verum } ) \/ { [7,<*i*>,<*a*>] where i is Nat, a is Element of SCM-Data-Loc : verum } ) \/ { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } ;
coherence
((({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Nat : verum } ) \/ { [7,<*i*>,<*a*>] where i is Nat, a is Element of SCM-Data-Loc : verum } ) \/ { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } is non empty set
;
end;
::
deftheorem defines
SCM-Instr SCMRINGI:def 1 :
for S being non empty 1-sorted holds SCM-Instr S = ((({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Nat : verum } ) \/ { [7,<*i*>,<*a*>] where i is Nat, a is Element of SCM-Data-Loc : verum } ) \/ { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } ;
theorem Th7:
for
S being non
empty 1-sorted for
x being
Element of
SCM-Instr S holds
( (
x in {[0,{},{}]} &
InsCode x = 0 ) or (
x in { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } & (
InsCode x = 1 or
InsCode x = 2 or
InsCode x = 3 or
InsCode x = 4 ) ) or (
x in { [6,<*i*>,{}] where i is Nat : verum } &
InsCode x = 6 ) or (
x in { [7,<*i*>,<*a*>] where i is Nat, a is Element of SCM-Data-Loc : verum } &
InsCode x = 7 ) or (
x in { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } &
InsCode x = 5 ) )
Lm1:
for R being Ring
for i being Element of SCM-Instr R holds InsCode i <= 7
Lm2:
for S being non empty 1-sorted
for i being Element of SCM-Instr S st not not InsCode i = 1 & ... & not InsCode i = 4 holds
JumpPart i = {}
Lm3:
for S being non empty 1-sorted
for i being Element of SCM-Instr S st InsCode i = 5 holds
JumpPart i = {}
Lm4:
for R being Ring
for I being Element of SCM-Instr R st InsCode I = 6 holds
dom (JumpPart I) = Seg 1
Lm5:
for R being Ring
for I being Element of SCM-Instr R st InsCode I = 7 holds
dom (JumpPart I) = Seg 1