Abstract definition of Hoare triples
Rules for the combinators
Definition of a specification language for Register machines; rules for lifts
Verification step tactics
Hoare rules for standard machine
generating Legacy Lemmas for Realise/Terminates