environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, SCMFSA_2, AMI_1, RELAT_1, AMI_3, FSM_1, STRUCT_0, FUNCT_4, FUNCOP_1, XBOOLE_0, TARSKI, FUNCT_1, XXREAL_0, ARYTM_3, GRAPHSP, EXTPRO_1, COMPLEX1, PARTFUN1, FINSEQ_1, FINSEQ_2, CARD_1, INT_1, CIRCUIT2, ARYTM_1, AMISTD_5, FINSET_1, COMPOS_1, GOBRD13, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, FINSET_1, ORDINAL1, NUMBERS, XCMPLX_0, INT_2, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_4, INT_1, NAT_1, STRUCT_0, FUNCOP_1, FINSEQ_1, FINSEQ_2, MEMSTR_0, COMPOS_1, EXTPRO_1, FUNCT_7, SCMFSA_2, XXREAL_0, AMISTD_5;
definitions EXTPRO_1, AMISTD_5;
theorems GRFUNC_1, FUNCOP_1, TARSKI, FUNCT_4, FUNCT_1, ZFMISC_1, INT_1, RELAT_1, SCMFSA_2, ABSVALUE, FINSEQ_2, XBOOLE_0, XBOOLE_1, PBOOLE, PARTFUN1, EXTPRO_1, AMISTD_5, MEMSTR_0, AMI_2;
schemes ;
registrations XBOOLE_0, RELAT_1, FUNCT_1, XREAL_0, INT_1, FINSEQ_1, STRUCT_0, AMI_3, SCMFSA_2, FINSET_1, ORDINAL1, COMPOS_1, EXTPRO_1, CARD_1, MEMSTR_0, FUNCT_4, FUNCOP_1;
constructors HIDDEN, DOMAIN_1, INT_2, AMI_3, SCMFSA_2, RELSET_1, PRE_POLY, SCMFSA_1, AMISTD_5, FUNCT_7;
requirements HIDDEN, NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
equalities EXTPRO_1, FUNCOP_1, SCMFSA_2, MEMSTR_0, SCM_INST;
expansions ;
theorem
for
q being
NAT -defined the
InstructionsF of
SCM+FSA -valued finite non
halt-free Function for
p being non
empty b1 -autonomic FinPartState of
SCM+FSA for
s1,
s2 being
State of
SCM+FSA st
p c= s1 &
p c= s2 holds
for
P1,
P2 being
Instruction-Sequence of
SCM+FSA st
q c= P1 &
q c= P2 holds
for
i being
Nat for
da,
db being
Int-Location st
CurInstr (
P1,
(Comput (P1,s1,i)))
= da := db &
da in dom p holds
(Comput (P1,s1,i)) . db = (Comput (P2,s2,i)) . db
theorem
for
q being
NAT -defined the
InstructionsF of
SCM+FSA -valued finite non
halt-free Function for
p being non
empty b1 -autonomic FinPartState of
SCM+FSA for
s1,
s2 being
State of
SCM+FSA st
p c= s1 &
p c= s2 holds
for
P1,
P2 being
Instruction-Sequence of
SCM+FSA st
q c= P1 &
q c= P2 holds
for
i being
Nat for
da,
db being
Int-Location st
CurInstr (
P1,
(Comput (P1,s1,i)))
= AddTo (
da,
db) &
da in dom p holds
((Comput (P1,s1,i)) . da) + ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db)
theorem
for
q being
NAT -defined the
InstructionsF of
SCM+FSA -valued finite non
halt-free Function for
p being non
empty b1 -autonomic FinPartState of
SCM+FSA for
s1,
s2 being
State of
SCM+FSA st
p c= s1 &
p c= s2 holds
for
P1,
P2 being
Instruction-Sequence of
SCM+FSA st
q c= P1 &
q c= P2 holds
for
i being
Nat for
da,
db being
Int-Location st
CurInstr (
P1,
(Comput (P1,s1,i)))
= SubFrom (
da,
db) &
da in dom p holds
((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db)
theorem
for
q being
NAT -defined the
InstructionsF of
SCM+FSA -valued finite non
halt-free Function for
p being non
empty b1 -autonomic FinPartState of
SCM+FSA for
s1,
s2 being
State of
SCM+FSA st
p c= s1 &
p c= s2 holds
for
P1,
P2 being
Instruction-Sequence of
SCM+FSA st
q c= P1 &
q c= P2 holds
for
i being
Nat for
da,
db being
Int-Location st
CurInstr (
P1,
(Comput (P1,s1,i)))
= MultBy (
da,
db) &
da in dom p holds
((Comput (P1,s1,i)) . da) * ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db)
theorem
for
q being
NAT -defined the
InstructionsF of
SCM+FSA -valued finite non
halt-free Function for
p being non
empty b1 -autonomic FinPartState of
SCM+FSA for
s1,
s2 being
State of
SCM+FSA st
p c= s1 &
p c= s2 holds
for
P1,
P2 being
Instruction-Sequence of
SCM+FSA st
q c= P1 &
q c= P2 holds
for
i being
Nat for
da,
db being
Int-Location st
CurInstr (
P1,
(Comput (P1,s1,i)))
= Divide (
da,
db) &
da in dom p &
da <> db holds
((Comput (P1,s1,i)) . da) div ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) div ((Comput (P2,s2,i)) . db)
theorem
for
q being
NAT -defined the
InstructionsF of
SCM+FSA -valued finite non
halt-free Function for
p being non
empty b1 -autonomic FinPartState of
SCM+FSA for
s1,
s2 being
State of
SCM+FSA st
p c= s1 &
p c= s2 holds
for
P1,
P2 being
Instruction-Sequence of
SCM+FSA st
q c= P1 &
q c= P2 holds
for
i being
Nat for
da,
db being
Int-Location st
CurInstr (
P1,
(Comput (P1,s1,i)))
= Divide (
da,
db) &
db in dom p holds
((Comput (P1,s1,i)) . da) mod ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db)
theorem
for
q being
NAT -defined the
InstructionsF of
SCM+FSA -valued finite non
halt-free Function for
p being non
empty b1 -autonomic FinPartState of
SCM+FSA for
s1,
s2 being
State of
SCM+FSA st
p c= s1 &
p c= s2 holds
for
P1,
P2 being
Instruction-Sequence of
SCM+FSA st
q c= P1 &
q c= P2 holds
for
i being
Nat for
da being
Int-Location for
loc being
Nat st
CurInstr (
P1,
(Comput (P1,s1,i)))
= da =0_goto loc &
loc <> (IC (Comput (P1,s1,i))) + 1 holds
(
(Comput (P1,s1,i)) . da = 0 iff
(Comput (P2,s2,i)) . da = 0 )
theorem
for
q being
NAT -defined the
InstructionsF of
SCM+FSA -valued finite non
halt-free Function for
p being non
empty b1 -autonomic FinPartState of
SCM+FSA for
s1,
s2 being
State of
SCM+FSA st
p c= s1 &
p c= s2 holds
for
P1,
P2 being
Instruction-Sequence of
SCM+FSA st
q c= P1 &
q c= P2 holds
for
i being
Nat for
da being
Int-Location for
loc being
Nat st
CurInstr (
P1,
(Comput (P1,s1,i)))
= da >0_goto loc &
loc <> (IC (Comput (P1,s1,i))) + 1 holds
(
(Comput (P1,s1,i)) . da > 0 iff
(Comput (P2,s2,i)) . da > 0 )
theorem
for
q being
NAT -defined the
InstructionsF of
SCM+FSA -valued finite non
halt-free Function for
p being non
empty b1 -autonomic FinPartState of
SCM+FSA for
s1,
s2 being
State of
SCM+FSA st
p c= s1 &
p c= s2 holds
for
P1,
P2 being
Instruction-Sequence of
SCM+FSA st
q c= P1 &
q c= P2 holds
for
i being
Nat for
da,
db being
Int-Location for
f being
FinSeq-Location st
CurInstr (
P1,
(Comput (P1,s1,i)))
= da := (
f,
db) &
da in dom p holds
for
k1,
k2 being
Element of
NAT st
k1 = |.((Comput (P1,s1,i)) . db).| &
k2 = |.((Comput (P2,s2,i)) . db).| holds
((Comput (P1,s1,i)) . f) /. k1 = ((Comput (P2,s2,i)) . f) /. k2
theorem
for
q being
NAT -defined the
InstructionsF of
SCM+FSA -valued finite non
halt-free Function for
p being non
empty b1 -autonomic FinPartState of
SCM+FSA for
s1,
s2 being
State of
SCM+FSA st
p c= s1 &
p c= s2 holds
for
P1,
P2 being
Instruction-Sequence of
SCM+FSA st
q c= P1 &
q c= P2 holds
for
i being
Nat for
da,
db being
Int-Location for
f being
FinSeq-Location st
CurInstr (
P1,
(Comput (P1,s1,i)))
= (
f,
db)
:= da &
f in dom p holds
for
k1,
k2 being
Nat st
k1 = |.((Comput (P1,s1,i)) . db).| &
k2 = |.((Comput (P2,s2,i)) . db).| holds
((Comput (P1,s1,i)) . f) +* (
k1,
((Comput (P1,s1,i)) . da))
= ((Comput (P2,s2,i)) . f) +* (
k2,
((Comput (P2,s2,i)) . da))
theorem
for
q being
NAT -defined the
InstructionsF of
SCM+FSA -valued finite non
halt-free Function for
p being non
empty b1 -autonomic FinPartState of
SCM+FSA for
s1,
s2 being
State of
SCM+FSA st
p c= s1 &
p c= s2 holds
for
P1,
P2 being
Instruction-Sequence of
SCM+FSA st
q c= P1 &
q c= P2 holds
for
i being
Nat for
da being
Int-Location for
f being
FinSeq-Location st
CurInstr (
P1,
(Comput (P1,s1,i)))
= f :=<0,...,0> da &
f in dom p holds
for
k1,
k2 being
Nat st
k1 = |.((Comput (P1,s1,i)) . da).| &
k2 = |.((Comput (P2,s2,i)) . da).| holds
k1 |-> 0 = k2 |-> 0