environ
vocabularies HIDDEN, AMI_1, SCMFSA_2, SCMFSA7B, SCMFSA6A, SF_MASTR, GRAPHSP, AMI_3, SCMFSA6B, AOFA_I00, SCMFSA8C, CARD_1, AMISTD_2, RELAT_1, TARSKI, XXREAL_0, ARYTM_3, FSM_1, XBOOLE_0, FUNCT_4, NUMBERS, SCMFSA6C, CIRCUIT2, FUNCT_1, MSUALG_1, SUBSET_1, NAT_1, STRUCT_0, FINSET_1, EXTPRO_1, SFMASTR1, PARTFUN1, RELOC, FUNCOP_1, COMPOS_1, AMISTD_1, FRECHET;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, FINSET_1, NAT_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_4, FUNCOP_1, PBOOLE, VALUED_1, FUNCT_7, AMI_2, STRUCT_0, MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1, AMISTD_1, AMISTD_2, SCMFSA_1, SCMFSA_2, SCMFSA6A, SCMFSA6B, SF_MASTR, SCMFSA6C, SCMFSA7B, SCMFSA8C, XXREAL_0, SEQ_4, SCMFSA_M;
definitions EXTPRO_1, SCMFSA7B;
theorems TARSKI, NAT_1, RELAT_1, FUNCT_1, GRFUNC_1, FUNCT_4, SCMFSA_2, MEMSTR_0, SCMFSA6A, SCMFSA6B, SF_MASTR, SCMFSA6C, SCMFSA7B, SCMFSA8A, SCMFSA8B, SCMFSA8C, XBOOLE_0, XBOOLE_1, XREAL_1, ORDINAL1, FUNCOP_1, PBOOLE, PARTFUN1, COMPOS_1, EXTPRO_1, AMI_2, COMPOS_0, SCMFSA_M, AMISTD_1, AFINSQ_1;
schemes NAT_1;
registrations ORDINAL1, FINSET_1, XREAL_0, NAT_1, INT_1, SCMFSA_2, SF_MASTR, SCMFSA6B, SCMFSA6C, SCMFSA7B, SCMFSA8A, SCMFSA8C, SCMFSA_9, SCMFSA10, AMISTD_2, COMPOS_1, EXTPRO_1, FUNCT_4, FUNCOP_1, STRUCT_0, MEMSTR_0, AMI_3, COMPOS_0, SCMFSA_M, SCMFSA8B, SCMFSA6A;
constructors HIDDEN, DOMAIN_1, SETWISEO, SEQ_4, PRE_FF, SCM_1, SCMFSA6A, SF_MASTR, SCMFSA6B, SCMFSA6C, SCMFSA8A, SCMFSA8B, SCMFSA8C, RELSET_1, PRE_POLY, AMISTD_2, SCMFSA7B, SCMFSA_1, PBOOLE, AMISTD_1, COMPLEX1, INT_2, NAT_D, XXREAL_1, MEMSTR_0, SCMFSA_M, FUNCT_7, SCMFSA_X;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE, ARITHM, REAL;
equalities EXTPRO_1, SCMFSA_2, FUNCOP_1, SCMFSA6A, MEMSTR_0, SCMFSA_M, SCMFSA8B, SCMFSA8C;
expansions SCMFSA7B, SCMFSA_M;
set D = Data-Locations ;
set SAt = Start-At (0,SCM+FSA);
Lm1:
for p being Instruction-Sequence of SCM+FSA
for I being good really-closed Program of SCM+FSA
for J being really-closed Program of SCM+FSA
for s being State of SCM+FSA st s . (intloc 0) = 1 & I is_halting_on s,p & J is_halting_on IExec (I,p,s),p & Initialize ((intloc 0) .--> 1) c= s & I ";" J c= p holds
( IC (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) = card I & DataPart (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) = DataPart (Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) & Reloc (J,(card I)) c= p & (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) . (intloc 0) = 1 & p halts_on s & LifeSpan (p,s) = ((LifeSpan ((p +* I),s)) + 1) + (LifeSpan (((p +* I) +* J),(Initialized (Result ((p +* I),s))))) & ( J is good implies (Result (p,s)) . (intloc 0) = 1 ) )
theorem Th5:
for
p being
Instruction-Sequence of
SCM+FSA for
s being
State of
SCM+FSA for
Ig being
good really-closed Program of
SCM+FSA for
J being
really-closed Program of
SCM+FSA st
Ig is_halting_on Initialized s,
p &
J is_halting_on IExec (
Ig,
p,
s),
p holds
IExec (
(Ig ";" J),
p,
s)
= (IExec (J,p,(IExec (Ig,p,s)))) +* (Start-At (((IC (IExec (J,p,(IExec (Ig,p,s))))) + (card Ig)),SCM+FSA))
theorem Th6:
for
p being
Instruction-Sequence of
SCM+FSA for
s being
State of
SCM+FSA for
a being
Int-Location for
Ig being
good really-closed Program of
SCM+FSA for
J being
really-closed Program of
SCM+FSA st (
Ig is
parahalting or
Ig is_halting_on Initialized s,
p ) & (
J is
parahalting or
J is_halting_on IExec (
Ig,
p,
s),
p ) holds
(IExec ((Ig ";" J),p,s)) . a = (IExec (J,p,(IExec (Ig,p,s)))) . a
theorem Th7:
for
p being
Instruction-Sequence of
SCM+FSA for
s being
State of
SCM+FSA for
f being
FinSeq-Location for
Ig being
good really-closed Program of
SCM+FSA for
J being
really-closed Program of
SCM+FSA st (
Ig is
parahalting or
Ig is_halting_on Initialized s,
p ) & (
J is
parahalting or
J is_halting_on IExec (
Ig,
p,
s),
p ) holds
(IExec ((Ig ";" J),p,s)) . f = (IExec (J,p,(IExec (Ig,p,s)))) . f
theorem
for
p being
Instruction-Sequence of
SCM+FSA for
s being
State of
SCM+FSA for
Ig being
good really-closed Program of
SCM+FSA for
J being
really-closed Program of
SCM+FSA st (
Ig is
parahalting or
Ig is_halting_on Initialized s,
p ) & (
J is
parahalting or
J is_halting_on IExec (
Ig,
p,
s),
p ) holds
DataPart (IExec ((Ig ";" J),p,s)) = DataPart (IExec (J,p,(IExec (Ig,p,s))))