Load IncludeHeader.

POPL 2012 submission: Lemma 1 and 2 (invariant preservation)

Require Import PreservationAux.

Variable A : ATOM.t.
Variable nativeop : Type.

Variable prog : Program.t A nativeop.

Theorem init : forall s1, initial_state prog s1 ->
invariant prog s1.

Proof.

Variable cppsem : cppsemparam.
Variable sem : semparam A nativeop.

Theorem goal : forall
( hierarchy_wf : Well_formed_hierarchy.prop (Program.hierarchy prog) )
(s1 : State.t A nativeop)
(Hs1 : invariant prog s1 )
( t : trace (evtr sem) )
( s2 : State.t A nativeop )
( step : step prog cppsem s1 t s2 )
,
invariant prog s2.

Proof.

Module Preservation