# Changeset 1971 for src/ASM/Interpret.ma

Ignore:
Timestamp:
May 20, 2012, 10:34:31 PM (9 years ago)
Message:
1. Interpret.ma: we need to prove \sigma (execute_preinstruction s) = execute_preinstruction (\sigma s)

Thus execute_preinstruction cannot be defined using Russell.
Changed, but the proof of the properties still uses Russell
(with a trick...)

1. AssemblyProofSplit?: the preinstruction case of the main theorem moved to a main lemma which is also proved using the Russell trick. This seems very promising ATM.
File:
1 edited

Unmodified