environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, STRUCT_0, AMI_1, AMI_2, FUNCT_7, XBOOLE_0, RELAT_1, TARSKI, CAT_1, FSM_1, FUNCT_1, INT_1, NAT_1, GRAPHSP, FINSEQ_1, CARD_1, ARYTM_3, ARYTM_1, FUNCOP_1, XXREAL_0, GLIB_000, FUNCT_4, AMI_3, RECDEF_2, QUANTAL1, XCMPLX_0, MEMSTR_0, GOBRD13;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, XTUPLE_0, SUBSET_1, ORDINAL1, XCMPLX_0, RELAT_1, FUNCT_1, XXREAL_0, INT_1, FUNCOP_1, CARD_1, FUNCT_4, FUNCT_7, FINSEQ_1, RECDEF_2, NUMBERS, MEASURE6, STRUCT_0, MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1, SCM_INST, AMI_2;
definitions EXTPRO_1, MEMSTR_0;
theorems TARSKI, ZFMISC_1, ENUMSET1, AMI_2, FUNCOP_1, FUNCT_4, CARD_3, INT_1, ORDINAL1, XBOOLE_0, XBOOLE_1, XXREAL_0, NAT_1, RELAT_1, FUNCT_1, PARTFUN1, SCM_INST, XTUPLE_0, SUBSET_1;
schemes ;
registrations XBOOLE_0, SETFAM_1, ORDINAL1, FUNCOP_1, XREAL_0, INT_1, CARD_3, AMI_2, XXREAL_0, FUNCT_1, FINSEQ_1, EXTPRO_1, FUNCT_4, MEMSTR_0, RELAT_1, COMPOS_0, SCM_INST, XTUPLE_0, ORDINAL2, NAT_1, CARD_1, FACIRC_1;
constructors HIDDEN, DOMAIN_1, FINSEQ_4, CAT_2, AMI_2, RELSET_1, EXTPRO_1, FUNCT_7, MEASURE6, XTUPLE_0, FUNCT_4;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities TARSKI, COMPOS_1, EXTPRO_1, FUNCOP_1, AMI_2, CARD_1, NAT_1, STRUCT_0, MEMSTR_0, COMPOS_0, SCM_INST, ORDINAL1;
expansions EXTPRO_1, AMI_2, STRUCT_0, MEMSTR_0;
Lm1: the_Values_of SCM =
the ValuesF of SCM * the Object-Kind of SCM
.=
SCM-VAL * SCM-OK
;
definition
let a,
b be
Data-Location;
correctness
coherence
[1,{},<*a,b*>] is Instruction of SCM;
correctness
coherence
[2,{},<*a,b*>] is Instruction of SCM;
correctness
coherence
[3,{},<*a,b*>] is Instruction of SCM;
correctness
coherence
[4,{},<*a,b*>] is Instruction of SCM;
correctness
coherence
[5,{},<*a,b*>] is Instruction of SCM;
end;
Lm2:
for I being Instruction of SCM st ex s being State of SCM st (Exec (I,s)) . (IC ) = (IC s) + 1 holds
not I is halting
Lm3:
for I being Instruction of SCM st I = [0,{},{}] holds
I is halting
Lm4:
for a, b being Data-Location holds not a := b is halting
Lm5:
for a, b being Data-Location holds not AddTo (a,b) is halting
Lm6:
for a, b being Data-Location holds not SubFrom (a,b) is halting
Lm7:
for a, b being Data-Location holds not MultBy (a,b) is halting
Lm8:
for a, b being Data-Location holds not Divide (a,b) is halting
Lm9:
for loc being Nat holds not SCM-goto loc is halting
Lm10:
for a being Data-Location
for loc being Nat holds not a =0_goto loc is halting
Lm11:
for a being Data-Location
for loc being Nat holds not a >0_goto loc is halting
Lm12:
for I being set holds
( I is Instruction of SCM iff ( I = [0,{},{}] or ex a, b being Data-Location st I = a := b or ex a, b being Data-Location st I = AddTo (a,b) or ex a, b being Data-Location st I = SubFrom (a,b) or ex a, b being Data-Location st I = MultBy (a,b) or ex a, b being Data-Location st I = Divide (a,b) or ex loc being Nat st I = SCM-goto loc or ex a being Data-Location ex loc being Nat st I = a =0_goto loc or ex a being Data-Location ex loc being Nat st I = a >0_goto loc ) )
Lm13:
for W being Instruction of SCM st W is halting holds
W = [0,{},{}]
theorem
for
I being
set holds
(
I is
Instruction of
SCM iff (
I = [0,{},{}] or ex
a,
b being
Data-Location st
I = a := b or ex
a,
b being
Data-Location st
I = AddTo (
a,
b) or ex
a,
b being
Data-Location st
I = SubFrom (
a,
b) or ex
a,
b being
Data-Location st
I = MultBy (
a,
b) or ex
a,
b being
Data-Location st
I = Divide (
a,
b) or ex
loc being
Nat st
I = SCM-goto loc or ex
a being
Data-Location ex
loc being
Nat st
I = a =0_goto loc or ex
a being
Data-Location ex
loc being
Nat st
I = a >0_goto loc ) )
by Lm12;