environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, FINSEQ_1, AMI_1, SCMFSA_2, RELAT_1, SCMFSA_7, ARYTM_3, ARYTM_1, TARSKI, FUNCT_1, XXREAL_0, PARTFUN1, CAT_1, NAT_1, CARD_1, FUNCOP_1, SCMFSA6A, ORDINAL4, AMI_3, FUNCT_4, INT_1, GRAPHSP, FSM_1, CIRCUIT2, EXTPRO_1, SCMFSA6B, SF_MASTR, MSUALG_1, XBOOLE_0, PRE_POLY, AMISTD_2, SCMFSA7B, AFINSQ_1, SCMFSA6C, COMPOS_1, AMISTD_1, TURING_1, RELOC, VALUED_1, SCMPDS_4;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, COMPLEX1, NAT_1, INT_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSEQ_1, FINSEQ_2, FUNCT_4, DOMAIN_1, VALUED_1, AFINSQ_1, STRUCT_0, MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1, FUNCT_7, SCMFSA_2, AMISTD_1, AMISTD_2, FUNCOP_1, XXREAL_0, ENUMSET1, NAT_D, PBOOLE, AFINSQ_2, AMISTD_4, SCMFSA_7, COMPOS_2, SCMFSA6A, SF_MASTR, SCMFSA6B, INT_2, PRE_POLY, SCMFSA_M;
definitions TARSKI, SCMFSA6B, AMISTD_1;
theorems SCMFSA_7, NAT_1, GRFUNC_1, FUNCT_1, FUNCT_4, FUNCT_7, ENUMSET1, SCMFSA_2, FUNCOP_1, INT_1, RELAT_1, TARSKI, SF_MASTR, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, AFINSQ_1, COMPOS_1, AFINSQ_2, CARD_1, EXTPRO_1, PARTFUN1, MEMSTR_0, SCMFSA_M, ORDINAL1, AMISTD_1, COMPOS_0, VALUED_1;
schemes NAT_1, AFINSQ_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, FUNCOP_1, XXREAL_0, XREAL_0, NAT_1, INT_1, SCMFSA_2, SCMFSA6B, ORDINAL1, CARD_1, AFINSQ_1, COMPOS_1, AFINSQ_2, EXTPRO_1, FUNCT_4, STRUCT_0, MEMSTR_0, SCMFSA10, AMI_3, COMPOS_0, SCMFSA_M, SCMFSA6A, COMPOS_2, SCMFSA6C, SCMFSA_4;
constructors HIDDEN, ENUMSET1, XXREAL_0, REAL_1, SCMFSA_7, SCMFSA6A, SF_MASTR, SCMFSA6B, NAT_D, RELSET_1, PRE_POLY, DOMAIN_1, AFINSQ_2, PARTFUN3, PBOOLE, AMISTD_1, AMISTD_2, AMI_3, MEMSTR_0, SCMFSA_M, FUNCT_7, COMPOS_2;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities FUNCOP_1, SCMFSA6A, SCMFSA6B, COMPOS_1, SCMFSA_7, EXTPRO_1, MEMSTR_0, SCMFSA_M, CARD_1, ORDINAL1, COMPOS_2;
expansions TARSKI, AMISTD_1;
set A = NAT ;
Lm1:
for s being State of SCM+FSA st IC s = 0 holds
for P being Instruction-Sequence of SCM+FSA
for a being Int-Location
for k being Integer st a := k c= P holds
P halts_on s
Lm2:
for p1, p2, p3, p4 being XFinSequence holds ((p1 ^ p2) ^ p3) ^ p4 = p1 ^ ((p2 ^ p3) ^ p4)
Lm3:
for c0 being Element of NAT
for s being b1 -started State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for a being Int-Location
for k being Integer st ( for c being Element of NAT st c < len (aSeq (a,k)) holds
(aSeq (a,k)) . c = P . (c0 + c) ) holds
for i being Element of NAT st i <= len (aSeq (a,k)) holds
IC (Comput (P,s,i)) = c0 + i
Lm4:
for s being 0 -started State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for a being Int-Location
for k being Integer st aSeq (a,k) c= P holds
for i being Element of NAT st i <= len (aSeq (a,k)) holds
IC (Comput (P,s,i)) = i
Lm5:
for s being 0 -started State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for f being FinSeq-Location
for p being FinSequence of INT st f := p c= P holds
P halts_on s
definition
let i be
Instruction of
SCM+FSA;
let a be
Int-Location;
pred i refers a means
not for
b being
Int-Location for
l being
Nat for
f being
FinSeq-Location holds
(
b := a <> i &
AddTo (
b,
a)
<> i &
SubFrom (
b,
a)
<> i &
MultBy (
b,
a)
<> i &
Divide (
b,
a)
<> i &
Divide (
a,
b)
<> i &
a =0_goto l <> i &
a >0_goto l <> i &
b := (
f,
a)
<> i & (
f,
b)
:= a <> i & (
f,
a)
:= b <> i &
f :=<0,...,0> a <> i );
end;
::
deftheorem defines
refers SCMFSA7B:def 1 :
for i being Instruction of SCM+FSA
for a being Int-Location holds
( i refers a iff not for b being Int-Location
for l being Nat
for f being FinSeq-Location holds
( b := a <> i & AddTo (b,a) <> i & SubFrom (b,a) <> i & MultBy (b,a) <> i & Divide (b,a) <> i & Divide (a,b) <> i & a =0_goto l <> i & a >0_goto l <> i & b := (f,a) <> i & (f,b) := a <> i & (f,a) := b <> i & f :=<0,...,0> a <> i ) );
canceled;