Home

Module PreservationStack

Load PreservationHeader.

Lemma goal : forall sf (Hin: In sf (State.stack s2)), stackframe_weak_inv prog s2 sf.
Proof.
 destruct sf; intros; try exact I.
 destruct inhpath; destruct k.
  Require Import PreservationStackKconstrotherBase.
  eauto using goal.
  Require Import PreservationStackKconstrotherField.
  destruct kind; eauto using goal.
 Require Import PreservationStackKconstrothercells.
 eauto using goal.
 destruct inhpath; destruct k.
  Require Import PreservationStackKdestrotherBase.
  eauto using goal.
  Require Import PreservationStackKdestrotherField.
  destruct kind; eauto using goal.
 Require Import PreservationStackKdestrcell.
 eauto using goal.
Qed.

End Preservation.