environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, AMI_1, SCMPDS_2, SCMFSA_7, CARD_1, FUNCOP_1, RELAT_1, FUNCT_1, NAT_1, ARYTM_3, XBOOLE_0, TARSKI, VALUED_1, EXTPRO_1, FSM_1, INT_1, FUNCT_4, GRAPHSP, AMI_3, AMI_2, STRUCT_0, COMPLEX1, XXREAL_0, ARYTM_1, TURING_1, AMISTD_2, SCMFSA6B, MSUALG_1, CIRCUIT2, SCMPDS_4, PARTFUN1, ORDINAL4, FINSET_1, COMPOS_1, GOBRD13, MEMSTR_0;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, XTUPLE_0, SUBSET_1, CARD_1, FINSET_1, ORDINAL1, NUMBERS, XCMPLX_0, RELAT_1, FUNCT_1, PARTFUN1, AFINSQ_1, VALUED_1, FUNCT_4, FUNCT_7, INT_1, NAT_1, INT_2, XXREAL_0, STRUCT_0, MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1, AMI_2, SCMPDS_2;
definitions EXTPRO_1;
theorems NAT_1, TARSKI, FUNCT_4, FUNCT_1, INT_1, RELAT_1, SCMPDS_2, AMI_2, FUNCT_2, FUNCT_7, SCMPDS_3, ENUMSET1, ABSVALUE, GRFUNC_1, XBOOLE_0, XREAL_1, FUNCOP_1, VALUED_1, AFINSQ_1, PARTFUN1, COMPOS_1, EXTPRO_1, PBOOLE, STRUCT_0, MEMSTR_0, XTUPLE_0;
schemes NAT_1, CLASSES1;
registrations FUNCT_1, ORDINAL1, XREAL_0, NAT_1, INT_1, SCMPDS_2, FINSET_1, FUNCT_4, PRE_POLY, AFINSQ_1, COMPOS_1, ORDINAL5, EXTPRO_1, FUNCT_7, MEMSTR_0, AMI_3, COMPOS_0, CARD_3, STRUCT_0, RELSET_1, XTUPLE_0;
constructors HIDDEN, INT_2, SCMPDS_1, SCMPDS_3, DOMAIN_1, RELSET_1, PRE_POLY, AMI_3, FUNCT_7;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities TARSKI, COMPOS_1, EXTPRO_1, XBOOLE_0, SCMPDS_2, FUNCOP_1, NAT_1, AFINSQ_1, MEMSTR_0;
expansions ;
Lm1:
Load (halt SCMPDS) is parahalting
Lm2:
Load (halt SCMPDS) is shiftable
registration
let a,
b be
Int_position;
let k1,
k2 be
Integer;
coherence
AddTo (a,k1,b,k2) is shiftable
coherence
SubFrom (a,k1,b,k2) is shiftable
coherence
MultBy (a,k1,b,k2) is shiftable
coherence
Divide (a,k1,b,k2) is shiftable
coherence
(a,k1) := (b,k2) is shiftable
end;
theorem
for
s2 being
State of
SCMPDS for
P1,
P2 being
Instruction-Sequence of
SCMPDS for
s1 being
0 -started State of
SCMPDS for
J being
parahalting shiftable Program of st
stop J c= P1 holds
for
n being
Nat st
Shift (
(stop J),
n)
c= P2 &
IC s2 = n &
DataPart s1 = DataPart s2 holds
for
i being
Nat holds
(
(IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) &
CurInstr (
P1,
(Comput (P1,s1,i)))
= CurInstr (
P2,
(Comput (P2,s2,i))) &
DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )