Module LICMproof

Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
Require Import AST Linking.
Require Import Memory Registers Op RTL.
Require Import LICM.
Require Injectproof.

Definition match_prog : program -> program -> Prop :=
  Injectproof.match_prog gen_injections.

Section PRESERVATION.

  Variables prog tprog: program.
  Hypothesis TRANSF: match_prog prog tprog.

  Lemma transf_program_match:
    forall prog tprog, transf_program prog = OK tprog -> match_prog prog tprog.
  
  Theorem transf_program_correct :
    Smallstep.forward_simulation (semantics prog) (semantics tprog).
End PRESERVATION.