environ
vocabularies HIDDEN, NUMBERS, SCMFSA_2, AMI_1, AMISTD_2, CARD_1, TARSKI, SCMFSA6A, FUNCT_4, FSM_1, RELAT_1, CIRCUIT2, FUNCT_1, SF_MASTR, SUBSET_1, ARYTM_3, SCMFSA7B, SCMFSA6B, SCMFSA6C, AMI_3, SCMFSA8A, NAT_1, GRAPHSP, XXREAL_0, MSUALG_1, STRUCT_0, ARYTM_1, INT_1, COMPLEX1, PARTFUN1, FINSEQ_1, FINSEQ_2, SCMFSA8B, EXTPRO_1, RELOC, FUNCOP_1, COMPOS_1, AMISTD_1, FRECHET;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, NAT_D, CARD_3, VALUED_1, INT_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCOP_1, FUNCT_4, PBOOLE, FUNCT_7, FINSEQ_1, FINSEQ_2, STRUCT_0, MEMSTR_0, COMPOS_0, COMPOS_1, COMPOS_2, EXTPRO_1, AMISTD_1, AMISTD_2, SCMFSA_2, SCMFSA6A, SF_MASTR, SCMFSA6B, SCMFSA6C, SCMFSA7B, SCMFSA8A, INT_2, SCMFSA_M;
definitions AMISTD_1, TARSKI;
theorems TARSKI, NAT_1, FUNCT_1, FUNCT_4, SCMFSA_2, MEMSTR_0, SCMFSA6A, GRFUNC_1, SCMFSA6B, SCMFSA6C, SCMFSA7B, SCMFSA8A, XBOOLE_1, XREAL_1, ORDINAL1, FUNCOP_1, PARTFUN1, AFINSQ_1, COMPOS_1, EXTPRO_1, PBOOLE, AMISTD_1, COMPOS_0, SCMFSA_M, SCMFSA_X;
schemes NAT_1;
registrations XXREAL_0, XREAL_0, NAT_1, INT_1, SCMFSA_2, SCMFSA6B, SCMFSA6C, ORDINAL1, MEMSTR_0, RELSET_1, SCMFSA10, AMISTD_2, COMPOS_1, EXTPRO_1, FUNCT_4, FUNCOP_1, STRUCT_0, AMI_3, COMPOS_0, SCMFSA_M, SCMFSA6A, AMISTD_1, SCMFSA_X, AFINSQ_1, CARD_3, FUNCT_1, VALUED_1, RELAT_1, CARD_1;
constructors HIDDEN, DOMAIN_1, XXREAL_0, NAT_1, INT_2, SCMFSA6A, SF_MASTR, SCMFSA6B, SCMFSA6C, SCMFSA8A, AMISTD_2, RELSET_1, SCMFSA7B, PRE_POLY, AMISTD_1, PBOOLE, FUNCOP_1, FUNCT_4, MEMSTR_0, SCMFSA_M, FUNCT_7, SCMFSA_X, NAT_D, AMI_3, COMPOS_2;
requirements HIDDEN, NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
equalities FUNCOP_1, EXTPRO_1, SCMFSA6A, MEMSTR_0, SCMFSA_M, COMPOS_1, SCMFSA8A, VALUED_1, AMISTD_1;
expansions EXTPRO_1, SCMFSA_M, MEMSTR_0;
set A = NAT ;
set D = Data-Locations ;
set SA0 = Start-At (0,SCM+FSA);
theorem Th2:
for
P1,
P2 being
Instruction-Sequence of
SCM+FSA for
s1 being
0 -started State of
SCM+FSA for
s2 being
State of
SCM+FSA for
I being
really-closed Program of
SCM+FSA st
I c= P1 holds
for
n being
Nat st
IC s2 = n &
DataPart s1 = DataPart s2 &
Reloc (
I,
n)
c= P2 holds
for
i being
Nat holds
(
(IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) &
IncAddr (
(CurInstr (P1,(Comput (P1,s1,i)))),
n)
= CurInstr (
P2,
(Comput (P2,s2,i))) &
DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )
canceled;
Lm1:
for a being Int-Location
for I, J being MacroInstruction of SCM+FSA holds
( 1 in dom (if=0 (a,I,J)) & 1 in dom (if>0 (a,I,J)) )
Lm2:
for a being Int-Location
for I, J being MacroInstruction of SCM+FSA holds
( (if=0 (a,I,J)) . 0 = a =0_goto ((card J) + 3) & (if=0 (a,I,J)) . 1 = goto 2 & (if>0 (a,I,J)) . 0 = a >0_goto ((card J) + 3) & (if>0 (a,I,J)) . 1 = goto 2 )
Lm3:
for I, J being really-closed MacroInstruction of SCM+FSA holds ((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA) is really-closed
theorem Th11:
for
P being
Instruction-Sequence of
SCM+FSA for
s being
State of
SCM+FSA for
I,
J being
really-closed parahalting MacroInstruction of
SCM+FSA for
a being
read-write Int-Location holds
(
if=0 (
a,
I,
J) is
parahalting & (
s . a = 0 implies
IExec (
(if=0 (a,I,J)),
P,
s)
= (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) & (
s . a <> 0 implies
IExec (
(if=0 (a,I,J)),
P,
s)
= (IExec (J,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) )
theorem Th12:
for
P being
Instruction-Sequence of
SCM+FSA for
s being
State of
SCM+FSA for
I,
J being
really-closed parahalting MacroInstruction of
SCM+FSA for
a being
read-write Int-Location holds
(
IC (IExec ((if=0 (a,I,J)),P,s)) = ((card I) + (card J)) + 3 & (
s . a = 0 implies ( ( for
d being
Int-Location holds
(IExec ((if=0 (a,I,J)),P,s)) . d = (IExec (I,P,s)) . d ) & ( for
f being
FinSeq-Location holds
(IExec ((if=0 (a,I,J)),P,s)) . f = (IExec (I,P,s)) . f ) ) ) & (
s . a <> 0 implies ( ( for
d being
Int-Location holds
(IExec ((if=0 (a,I,J)),P,s)) . d = (IExec (J,P,s)) . d ) & ( for
f being
FinSeq-Location holds
(IExec ((if=0 (a,I,J)),P,s)) . f = (IExec (J,P,s)) . f ) ) ) )
theorem Th17:
for
P being
Instruction-Sequence of
SCM+FSA for
s being
State of
SCM+FSA for
I,
J being
really-closed parahalting MacroInstruction of
SCM+FSA for
a being
read-write Int-Location holds
(
if>0 (
a,
I,
J) is
parahalting & (
s . a > 0 implies
IExec (
(if>0 (a,I,J)),
P,
s)
= (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) & (
s . a <= 0 implies
IExec (
(if>0 (a,I,J)),
P,
s)
= (IExec (J,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) )
theorem Th18:
for
P being
Instruction-Sequence of
SCM+FSA for
s being
State of
SCM+FSA for
I,
J being
really-closed parahalting MacroInstruction of
SCM+FSA for
a being
read-write Int-Location holds
(
IC (IExec ((if>0 (a,I,J)),P,s)) = ((card I) + (card J)) + 3 & (
s . a > 0 implies ( ( for
d being
Int-Location holds
(IExec ((if>0 (a,I,J)),P,s)) . d = (IExec (I,P,s)) . d ) & ( for
f being
FinSeq-Location holds
(IExec ((if>0 (a,I,J)),P,s)) . f = (IExec (I,P,s)) . f ) ) ) & (
s . a <= 0 implies ( ( for
d being
Int-Location holds
(IExec ((if>0 (a,I,J)),P,s)) . d = (IExec (J,P,s)) . d ) & ( for
f being
FinSeq-Location holds
(IExec ((if>0 (a,I,J)),P,s)) . f = (IExec (J,P,s)) . f ) ) ) )
registration
let a,
b be
Int-Location;
let I,
J be
MacroInstruction of
SCM+FSA ;
coherence
( if=0 (a,b,I,J) is halt-ending & if=0 (a,b,I,J) is unique-halt )
;
coherence
( if>0 (a,b,I,J) is halt-ending & if>0 (a,b,I,J) is unique-halt )
;
end;
theorem Th22:
for
P1,
P2 being
Instruction-Sequence of
SCM+FSA for
s1,
s2 being
State of
SCM+FSA for
I being
really-closed Program of
SCM+FSA for
a being
Int-Location st not
I refers a & ( for
b being
Int-Location st
a <> b holds
s1 . b = s2 . b ) & ( for
f being
FinSeq-Location holds
s1 . f = s2 . f ) holds
for
k being
Nat holds
( ( for
b being
Int-Location st
a <> b holds
(Comput ((P1 +* I),(Initialize s1),k)) . b = (Comput ((P2 +* I),(Initialize s2),k)) . b ) & ( for
f being
FinSeq-Location holds
(Comput ((P1 +* I),(Initialize s1),k)) . f = (Comput ((P2 +* I),(Initialize s2),k)) . f ) &
IC (Comput ((P1 +* I),(Initialize s1),k)) = IC (Comput ((P2 +* I),(Initialize s2),k)) &
CurInstr (
(P1 +* I),
(Comput ((P1 +* I),(Initialize s1),k)))
= CurInstr (
(P2 +* I),
(Comput ((P2 +* I),(Initialize s2),k))) )
theorem Th25:
for
P1,
P2 being
Instruction-Sequence of
SCM+FSA for
s1,
s2 being
State of
SCM+FSA for
I being
really-closed Program of
SCM+FSA for
a being
Int-Location st ( for
d being
read-write Int-Location st
a <> d holds
s1 . d = s2 . d ) & ( for
f being
FinSeq-Location holds
s1 . f = s2 . f ) & not
I refers a &
I is_halting_on Initialized s1,
P1 holds
( ( for
d being
Int-Location st
a <> d holds
(IExec (I,P1,s1)) . d = (IExec (I,P2,s2)) . d ) & ( for
f being
FinSeq-Location holds
(IExec (I,P1,s1)) . f = (IExec (I,P2,s2)) . f ) &
IC (IExec (I,P1,s1)) = IC (IExec (I,P2,s2)) )
theorem
for
P being
Instruction-Sequence of
SCM+FSA for
s being
State of
SCM+FSA for
I,
J being
really-closed parahalting MacroInstruction of
SCM+FSA for
a,
b being
read-write Int-Location st not
I refers a & not
J refers a holds
(
IC (IExec ((if=0 (a,b,I,J)),P,s)) = ((card I) + (card J)) + 5 & (
s . a = s . b implies ( ( for
d being
Int-Location st
a <> d holds
(IExec ((if=0 (a,b,I,J)),P,s)) . d = (IExec (I,P,s)) . d ) & ( for
f being
FinSeq-Location holds
(IExec ((if=0 (a,b,I,J)),P,s)) . f = (IExec (I,P,s)) . f ) ) ) & (
s . a <> s . b implies ( ( for
d being
Int-Location st
a <> d holds
(IExec ((if=0 (a,b,I,J)),P,s)) . d = (IExec (J,P,s)) . d ) & ( for
f being
FinSeq-Location holds
(IExec ((if=0 (a,b,I,J)),P,s)) . f = (IExec (J,P,s)) . f ) ) ) )
theorem
for
P being
Instruction-Sequence of
SCM+FSA for
s being
State of
SCM+FSA for
I,
J being
really-closed parahalting MacroInstruction of
SCM+FSA for
a,
b being
read-write Int-Location st not
I refers a & not
J refers a holds
(
IC (IExec ((if>0 (a,b,I,J)),P,s)) = ((card I) + (card J)) + 5 & (
s . a > s . b implies ( ( for
d being
Int-Location st
a <> d holds
(IExec ((if>0 (a,b,I,J)),P,s)) . d = (IExec (I,P,s)) . d ) & ( for
f being
FinSeq-Location holds
(IExec ((if>0 (a,b,I,J)),P,s)) . f = (IExec (I,P,s)) . f ) ) ) & (
s . a <= s . b implies ( ( for
d being
Int-Location st
a <> d holds
(IExec ((if>0 (a,b,I,J)),P,s)) . d = (IExec (J,P,s)) . d ) & ( for
f being
FinSeq-Location holds
(IExec ((if>0 (a,b,I,J)),P,s)) . f = (IExec (J,P,s)) . f ) ) ) )