Loading [MathJax]/jax/input/TeX/config.js
theorem Th7:
for
n being
Nat for
R being non
trivial Ring for
a,
b being
Data-Location of
R for
s1,
s2 being
State of
(SCM R) for
P1,
P2 being
Instruction-Sequence of
(SCM R) for
q being
NAT -defined the
InstructionsF of
(SCM b2) -valued finite non
halt-free Function for
p being non
empty b9 -autonomic FinPartState of
(SCM R) st
p c= s1 &
p c= s2 &
q c= P1 &
q c= P2 &
CurInstr (
P1,
(Comput (P1,s1,n)))
= a := b &
a in dom p holds
(Comput (P1,s1,n)) . b = (Comput (P2,s2,n)) . b
theorem Th8:
for
n being
Nat for
R being non
trivial Ring for
a,
b being
Data-Location of
R for
s1,
s2 being
State of
(SCM R) for
P1,
P2 being
Instruction-Sequence of
(SCM R) for
q being
NAT -defined the
InstructionsF of
(SCM b2) -valued finite non
halt-free Function for
p being non
empty b9 -autonomic FinPartState of
(SCM R) st
p c= s1 &
p c= s2 &
q c= P1 &
q c= P2 &
CurInstr (
P1,
(Comput (P1,s1,n)))
= AddTo (
a,
b) &
a in dom p holds
((Comput (P1,s1,n)) . a) + ((Comput (P1,s1,n)) . b) = ((Comput (P2,s2,n)) . a) + ((Comput (P2,s2,n)) . b)
theorem Th9:
for
n being
Nat for
R being non
trivial Ring for
a,
b being
Data-Location of
R for
s1,
s2 being
State of
(SCM R) for
P1,
P2 being
Instruction-Sequence of
(SCM R) for
q being
NAT -defined the
InstructionsF of
(SCM b2) -valued finite non
halt-free Function for
p being non
empty b9 -autonomic FinPartState of
(SCM R) st
p c= s1 &
p c= s2 &
q c= P1 &
q c= P2 &
CurInstr (
P1,
(Comput (P1,s1,n)))
= SubFrom (
a,
b) &
a in dom p holds
((Comput (P1,s1,n)) . a) - ((Comput (P1,s1,n)) . b) = ((Comput (P2,s2,n)) . a) - ((Comput (P2,s2,n)) . b)
theorem Th10:
for
n being
Nat for
R being non
trivial Ring for
a,
b being
Data-Location of
R for
s1,
s2 being
State of
(SCM R) for
P1,
P2 being
Instruction-Sequence of
(SCM R) for
q being
NAT -defined the
InstructionsF of
(SCM b2) -valued finite non
halt-free Function for
p being non
empty b9 -autonomic FinPartState of
(SCM R) st
p c= s1 &
p c= s2 &
q c= P1 &
q c= P2 &
CurInstr (
P1,
(Comput (P1,s1,n)))
= MultBy (
a,
b) &
a in dom p holds
((Comput (P1,s1,n)) . a) * ((Comput (P1,s1,n)) . b) = ((Comput (P2,s2,n)) . a) * ((Comput (P2,s2,n)) . b)
theorem Th11:
for
n being
Nat for
R being non
trivial Ring for
a being
Data-Location of
R for
loc being
Nat for
s1,
s2 being
State of
(SCM R) for
P1,
P2 being
Instruction-Sequence of
(SCM R) for
q being
NAT -defined the
InstructionsF of
(SCM b2) -valued finite non
halt-free Function for
p being non
empty b9 -autonomic FinPartState of
(SCM R) st
p c= s1 &
p c= s2 &
q c= P1 &
q c= P2 &
CurInstr (
P1,
(Comput (P1,s1,n)))
= a =0_goto loc &
loc <> (IC (Comput (P1,s1,n))) + 1 holds
(
(Comput (P1,s1,n)) . a = 0. R iff
(Comput (P2,s2,n)) . a = 0. R )
theorem Th12:
for
k being
Nat for
R being non
trivial Ring for
s1,
s2 being
State of
(SCM R) for
q being
NAT -defined the
InstructionsF of
(SCM b2) -valued finite non
halt-free Function for
p being non
empty b5 -autonomic FinPartState of
(SCM R) st
p c= s1 &
IncIC (
p,
k)
c= s2 holds
for
P1,
P2 being
Instruction-Sequence of
(SCM R) st
q c= P1 &
Reloc (
q,
k)
c= P2 holds
for
i being
Nat holds
(
(IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) &
IncAddr (
(CurInstr (P1,(Comput (P1,s1,i)))),
k)
= CurInstr (
P2,
(Comput (P2,s2,i))) &
(Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) &
DataPart (Comput (P1,(s1 +* (DataPart s2)),i)) = DataPart (Comput (P2,s2,i)) )