environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, SCMPDS_2, INT_1, FSM_1, AMI_1, COMPLEX1, ARYTM_3, FUNCT_1, AMI_2, STRUCT_0, XBOOLE_0, RELAT_1, TARSKI, CARD_1, AMI_3, GRAPHSP, EXTPRO_1, XXREAL_0, ARYTM_1, FUNCT_4, FUNCOP_1, CIRCUIT2, PARTFUN1, AMISTD_5, FINSET_1, COMPOS_1, GOBRD13, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_4, FINSET_1, INT_1, NAT_1, STRUCT_0, FUNCOP_1, INT_2, XXREAL_0, MEMSTR_0, COMPOS_1, EXTPRO_1, AMI_2, AMISTD_5, SCMPDS_2;
definitions EXTPRO_1, AMISTD_5;
theorems GRFUNC_1, FUNCOP_1, TARSKI, FUNCT_4, FUNCT_1, ZFMISC_1, INT_1, RELAT_1, ABSVALUE, SCMPDS_2, XBOOLE_0, XBOOLE_1, NUMBERS, PBOOLE, PARTFUN1, EXTPRO_1, AMISTD_5, MEMSTR_0, AMI_2;
schemes ;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, XREAL_0, INT_1, CARD_3, AMI_3, SCMPDS_2, FINSET_1, COMPOS_1, EXTPRO_1, FUNCT_4, FUNCOP_1, MEMSTR_0, COMPOS_0, NAT_1;
constructors HIDDEN, DOMAIN_1, INT_2, SCMPDS_1, SCMPDS_2, REAL_1, PRE_POLY, AMI_3, AMISTD_5, FUNCT_7, RELSET_1;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE, ARITHM, REAL;
equalities EXTPRO_1, AMI_2, FUNCOP_1, SCMPDS_2, NAT_1, MEMSTR_0;
expansions ;
theorem
for
P1,
P2 being
Instruction-Sequence of
SCMPDS for
q being
NAT -defined the
InstructionsF of
SCMPDS -valued finite non
halt-free Function for
p being non
empty b3 -autonomic FinPartState of
SCMPDS for
s1,
s2 being
State of
SCMPDS st
p c= s1 &
p c= s2 &
q c= P1 &
q c= P2 holds
for
i being
Nat for
k1,
k2 being
Integer for
a,
b being
Int_position st
CurInstr (
P1,
(Comput (P1,s1,i)))
= (
a,
k1)
:= (
b,
k2) &
a in dom p &
DataLoc (
((Comput (P1,s1,i)) . a),
k1)
in dom p holds
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2))
theorem
for
P1,
P2 being
Instruction-Sequence of
SCMPDS for
q being
NAT -defined the
InstructionsF of
SCMPDS -valued finite non
halt-free Function for
p being non
empty b3 -autonomic FinPartState of
SCMPDS for
s1,
s2 being
State of
SCMPDS st
p c= s1 &
p c= s2 &
q c= P1 &
q c= P2 holds
for
i being
Nat for
k1,
k2 being
Integer for
a,
b being
Int_position st
CurInstr (
P1,
(Comput (P1,s1,i)))
= AddTo (
a,
k1,
b,
k2) &
a in dom p &
DataLoc (
((Comput (P1,s1,i)) . a),
k1)
in dom p holds
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2))
theorem
for
P1,
P2 being
Instruction-Sequence of
SCMPDS for
q being
NAT -defined the
InstructionsF of
SCMPDS -valued finite non
halt-free Function for
p being non
empty b3 -autonomic FinPartState of
SCMPDS for
s1,
s2 being
State of
SCMPDS st
p c= s1 &
p c= s2 &
q c= P1 &
q c= P2 holds
for
i being
Nat for
k1,
k2 being
Integer for
a,
b being
Int_position st
CurInstr (
P1,
(Comput (P1,s1,i)))
= SubFrom (
a,
k1,
b,
k2) &
a in dom p &
DataLoc (
((Comput (P1,s1,i)) . a),
k1)
in dom p holds
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2))
theorem
for
P1,
P2 being
Instruction-Sequence of
SCMPDS for
q being
NAT -defined the
InstructionsF of
SCMPDS -valued finite non
halt-free Function for
p being non
empty b3 -autonomic FinPartState of
SCMPDS for
s1,
s2 being
State of
SCMPDS st
p c= s1 &
p c= s2 &
q c= P1 &
q c= P2 holds
for
i being
Nat for
k1,
k2 being
Integer for
a,
b being
Int_position st
CurInstr (
P1,
(Comput (P1,s1,i)))
= MultBy (
a,
k1,
b,
k2) &
a in dom p &
DataLoc (
((Comput (P1,s1,i)) . a),
k1)
in dom p holds
((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1))) * ((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2))) = ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1))) * ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2)))
theorem
for
P1,
P2 being
Instruction-Sequence of
SCMPDS for
q being
NAT -defined the
InstructionsF of
SCMPDS -valued finite non
halt-free Function for
p being non
empty b3 -autonomic FinPartState of
SCMPDS for
s1,
s2 being
State of
SCMPDS st
p c= s1 &
p c= s2 &
q c= P1 &
q c= P2 holds
for
i,
m being
Nat for
a being
Int_position for
k1,
k2 being
Integer st
CurInstr (
P1,
(Comput (P1,s1,i)))
= (
a,
k1)
<>0_goto k2 &
m = IC (Comput (P1,s1,i)) &
m + k2 >= 0 &
k2 <> 1 holds
(
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = 0 iff
(Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) = 0 )
theorem
for
P1,
P2 being
Instruction-Sequence of
SCMPDS for
q being
NAT -defined the
InstructionsF of
SCMPDS -valued finite non
halt-free Function for
p being non
empty b3 -autonomic FinPartState of
SCMPDS for
s1,
s2 being
State of
SCMPDS st
p c= s1 &
p c= s2 &
q c= P1 &
q c= P2 holds
for
i,
m being
Nat for
a being
Int_position for
k1,
k2 being
Integer st
CurInstr (
P1,
(Comput (P1,s1,i)))
= (
a,
k1)
<=0_goto k2 &
m = IC (Comput (P1,s1,i)) &
m + k2 >= 0 &
k2 <> 1 holds
(
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) > 0 iff
(Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) > 0 )
theorem
for
P1,
P2 being
Instruction-Sequence of
SCMPDS for
q being
NAT -defined the
InstructionsF of
SCMPDS -valued finite non
halt-free Function for
p being non
empty b3 -autonomic FinPartState of
SCMPDS for
s1,
s2 being
State of
SCMPDS st
p c= s1 &
p c= s2 &
q c= P1 &
q c= P2 holds
for
i,
m being
Nat for
a being
Int_position for
k1,
k2 being
Integer st
CurInstr (
P1,
(Comput (P1,s1,i)))
= (
a,
k1)
>=0_goto k2 &
m = IC (Comput (P1,s1,i)) &
m + k2 >= 0 &
k2 <> 1 holds
(
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) < 0 iff
(Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) < 0 )