environ
vocabularies HIDDEN, AMI_1, SCMFSA_2, FSM_1, CARD_1, SCMFSA6B, FUNCT_1, RELAT_1, ARYTM_3, FUNCT_4, SCMFSA6A, TARSKI, XBOOLE_0, CIRCUIT2, NUMBERS, GRAPHSP, AMI_3, XXREAL_0, SF_MASTR, FUNCOP_1, STRUCT_0, ARYTM_1, INT_1, COMPLEX1, PARTFUN1, FINSEQ_1, FINSEQ_2, AOFA_I00, EXTPRO_1, SCMFSA6C, COMPOS_1, NAT_1, AMISTD_1, FRECHET, TURING_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ENUMSET1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, INT_1, COMPLEX1, RELAT_1, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_2, FUNCOP_1, FUNCT_4, PBOOLE, STRUCT_0, MEMSTR_0, COMPOS_0, COMPOS_1, COMPOS_2, EXTPRO_1, AMISTD_1, FUNCT_7, SCMFSA_M, SCMFSA_2, SCMFSA10, SCMFSA6A, SF_MASTR, SCMFSA6B, XXREAL_0;
definitions EXTPRO_1, SCMFSA6B, AMISTD_1;
theorems RELAT_1, FUNCT_4, FUNCT_1, ZFMISC_1, FUNCOP_1, TARSKI, NAT_1, SCMFSA_2, ENUMSET1, GRFUNC_1, SCMFSA6A, SF_MASTR, SCMFSA6B, XBOOLE_0, XBOOLE_1, PARTFUN1, COMPOS_1, EXTPRO_1, AMISTD_2, PBOOLE, STRUCT_0, MEMSTR_0, AMISTD_1, AMI_2, SCMFSA_M, AFINSQ_1;
schemes ;
registrations FUNCT_1, FUNCOP_1, XREAL_0, INT_1, SCMFSA_2, SF_MASTR, SCMFSA6B, ORDINAL1, RELSET_1, COMPOS_1, STRUCT_0, EXTPRO_1, FUNCT_4, MEMSTR_0, AMI_3, COMPOS_0, SCMFSA_M, SCMFSA6A, SCMFSA10, CARD_1, AMISTD_2;
constructors HIDDEN, DOMAIN_1, SETWISEO, XXREAL_0, INT_2, SCMFSA6A, SF_MASTR, SCMFSA6B, RELSET_1, PRE_POLY, AMISTD_1, AMISTD_2, PBOOLE, FUNCT_4, MEMSTR_0, SCMFSA_1, SCMFSA_M, FUNCT_7, SCMFSA10, COMPOS_2;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
equalities FUNCOP_1, EXTPRO_1, SCMFSA6B, SCMFSA6A, MEMSTR_0, SCMFSA_2, SCMFSA_M, COMPOS_2;
expansions EXTPRO_1, SCMFSA_M;
set SA0 = Start-At (0,SCM+FSA);
canceled;
Lm1:
Macro (halt SCM+FSA) is keeping_0
Lm2:
now for I being keeping_0 parahalting Program of SCM+FSA
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA holds DataPart (Initialized (IExec (I,P,s))) = DataPart (IExec (I,P,s))
set IF =
Data-Locations ;
let I be
keeping_0 parahalting Program of
SCM+FSA;
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA holds DataPart (Initialized (IExec (I,P,s))) = DataPart (IExec (I,P,s))let s be
State of
SCM+FSA;
for P being Instruction-Sequence of SCM+FSA holds DataPart (Initialized (IExec (I,P,s))) = DataPart (IExec (I,P,s))let P be
Instruction-Sequence of
SCM+FSA;
DataPart (Initialized (IExec (I,P,s))) = DataPart (IExec (I,P,s))set IE =
IExec (
I,
P,
s);
now ( dom (DataPart (Initialized (IExec (I,P,s)))) = (dom (IExec (I,P,s))) /\ (Data-Locations ) & ( for x being object st x in dom (DataPart (Initialized (IExec (I,P,s)))) holds
(DataPart (Initialized (IExec (I,P,s)))) . x = (IExec (I,P,s)) . x ) )
A1:
dom (Initialized (IExec (I,P,s))) = the
carrier of
SCM+FSA
by PARTFUN1:def 2;
A2:
the
carrier of
SCM+FSA = {(IC )} \/ (Data-Locations )
by STRUCT_0:4;
A3:
dom (IExec (I,P,s)) = the
carrier of
SCM+FSA
by PARTFUN1:def 2;
hence
dom (DataPart (Initialized (IExec (I,P,s)))) = (dom (IExec (I,P,s))) /\ (Data-Locations )
by A1, RELAT_1:61;
for x being object st x in dom (DataPart (Initialized (IExec (I,P,s)))) holds
(DataPart (Initialized (IExec (I,P,s)))) . b2 = (IExec (I,P,s)) . b2then A4:
dom (DataPart (Initialized (IExec (I,P,s)))) = Data-Locations
by A3, A2, XBOOLE_1:21;
let x be
object ;
( x in dom (DataPart (Initialized (IExec (I,P,s)))) implies (DataPart (Initialized (IExec (I,P,s)))) . b1 = (IExec (I,P,s)) . b1 )assume A5:
x in dom (DataPart (Initialized (IExec (I,P,s))))
;
(DataPart (Initialized (IExec (I,P,s)))) . b1 = (IExec (I,P,s)) . b1
per cases
( x in Int-Locations or x in FinSeq-Locations )
by A5, A4, SCMFSA_2:100, XBOOLE_0:def 3;
suppose
x in Int-Locations
;
(DataPart (Initialized (IExec (I,P,s)))) . b1 = (IExec (I,P,s)) . b1
then reconsider x9 =
x as
Int-Location by AMI_2:def 16;
per cases
( x9 is read-write or x9 is read-only )
;
suppose
x9 is
read-only
;
(DataPart (Initialized (IExec (I,P,s)))) . b1 = (IExec (I,P,s)) . b1
then A7:
x9 = intloc 0
;
thus (DataPart (Initialized (IExec (I,P,s)))) . x =
(Initialized (IExec (I,P,s))) . x9
by A5, A4, FUNCT_1:49
.=
1
by A7, SCMFSA_M:9
.=
(IExec (I,P,s)) . x
by A7, SCMFSA6B:11
;
verum
end;
end;
end;
end;
end;
hence
DataPart (Initialized (IExec (I,P,s))) = DataPart (IExec (I,P,s))
by FUNCT_1:46;
verum
end;