theorem
for
N being
with_zero set for
S being non
empty with_non-empty_values IC-Ins-separated halting IC-recognized CurIns-recognized AMI-Struct over
N for
q being
NAT -defined the
InstructionsF of
b2 -valued finite non
halt-free Function for
p being non
empty b3 -autonomic FinPartState of
S for
s1,
s2 being
State of
S st
p c= s1 &
p c= s2 holds
for
P1,
P2 being
Instruction-Sequence of
S st
q c= P1 &
q c= P2 holds
for
i being
Nat holds
(
IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) &
CurInstr (
P1,
(Comput (P1,s1,i)))
= CurInstr (
P2,
(Comput (P2,s2,i))) )