Home

Module PreservationStack2Header

Load PreservationHeader.

Lemma stack2_2 : forall (sf2 sf1 : StackFrame.t A nativeop)
    (l1 l2 : list (StackFrame.t A nativeop)),
    State.stack s1 = l1 ++ sf1 :: sf2 :: l2 ->
    is_code_frame sf1 ->
    stackframe_constructor_inv prog s1 sf2
.
Proof.
 intros.
 destruct (stack2 Hs1 (sf1 := sf1) (l1 := l1) (l2 := sf2 :: l2) H).
 eauto.
Qed.

Set Printing Depth 1048576.