environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, CARD_1, XBOOLE_0, STRUCT_0, FUNCSDOM, AMI_3, AMI_1, AMI_2, FUNCT_7, TARSKI, RELAT_1, FSM_1, FUNCT_1, CAT_1, FINSEQ_1, GRAPHSP, FUNCT_2, CARD_3, ARYTM_3, ARYTM_1, SUPINF_2, FUNCOP_1, SCMRING1, GLIB_000, FUNCT_4, RECDEF_2, GOBRD13, MEMSTR_0, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, DOMAIN_1, RELAT_1, FUNCT_1, ORDINAL1, CARD_1, FUNCT_2, RECDEF_2, XCMPLX_0, STRUCT_0, ALGSTR_0, VECTSP_1, CARD_3, FINSEQ_1, NUMBERS, FUNCOP_1, FUNCT_4, FUNCT_7, MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1, AMI_2, AMI_3, SCMRINGI, SCMRING1;
definitions EXTPRO_1, MEMSTR_0;
theorems AMI_2, AMI_3, CARD_3, FUNCOP_1, ENUMSET1, FUNCT_4, SCMRING1, TARSKI, ZFMISC_1, XBOOLE_0, XBOOLE_1, NAT_1, FUNCT_1, PARTFUN1, RELAT_1, SCMRINGI, SUBSET_1, ORDINAL1;
schemes ;
registrations ORDINAL1, RELSET_1, FUNCOP_1, FINSEQ_1, CARD_3, STRUCT_0, AMI_3, SCMRING1, AMI_2, FUNCT_1, EXTPRO_1, SCMRINGI, SCM_INST, XTUPLE_0, NAT_1, XCMPLX_0, ORDINAL2;
constructors HIDDEN, FINSEQ_4, REALSET1, AMI_3, SCMRING1, PRE_POLY, FUNCT_7, RELSET_1;
requirements HIDDEN, NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
equalities XBOOLE_0, STRUCT_0, FUNCOP_1, SCMRING1, COMPOS_1, EXTPRO_1, NAT_1, AMI_2, MEMSTR_0, COMPOS_0, SCMRINGI;
expansions EXTPRO_1, AMI_2, MEMSTR_0;
Lm2:
for R being Ring holds the carrier of (SCM R) \ {NAT} = SCM-Data-Loc
definition
let R be
Ring;
let a,
b be
Data-Location of
R;
coherence
[1,{},<*a,b*>] is Instruction of (SCM R)
coherence
[2,{},<*a,b*>] is Instruction of (SCM R)
coherence
[3,{},<*a,b*>] is Instruction of (SCM R)
coherence
[4,{},<*a,b*>] is Instruction of (SCM R)
end;
theorem Th7:
for
R being
Ring for
I being
set holds
(
I is
Instruction of
(SCM R) iff (
I = [0,{},{}] or ex
a,
b being
Data-Location of
R st
I = a := b or ex
a,
b being
Data-Location of
R st
I = AddTo (
a,
b) or ex
a,
b being
Data-Location of
R st
I = SubFrom (
a,
b) or ex
a,
b being
Data-Location of
R st
I = MultBy (
a,
b) or ex
i1 being
Nat st
I = goto (
i1,
R) or ex
a being
Data-Location of
R ex
i1 being
Nat st
I = a =0_goto i1 or ex
a being
Data-Location of
R ex
r being
Element of
R st
I = a := r ) )
Lm3:
for R being Ring
for a, b being Data-Location of R holds not a := b is halting
Lm4:
for R being Ring
for a, b being Data-Location of R holds not AddTo (a,b) is halting
Lm5:
for R being Ring
for a, b being Data-Location of R holds not SubFrom (a,b) is halting
Lm6:
for R being Ring
for a, b being Data-Location of R holds not MultBy (a,b) is halting
Lm7:
for R being Ring
for i1 being Nat holds not goto (i1,R) is halting
Lm8:
for R being Ring
for a being Data-Location of R
for i1 being Nat holds not a =0_goto i1 is halting
Lm9:
for R being Ring
for r being Element of R
for a being Data-Location of R holds not a := r is halting
Lm10:
for R being Ring
for W being Instruction of (SCM R) st W is halting holds
W = [0,{},{}]