(*
 * Vericert: Verified high-level synthesis.
 * Copyright (C) 2020-2022 Yann Herklotz <yann@yannherklotz.com>
 *
 * This program is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 *
 * This program is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with this program.  If not, see <https://www.gnu.org/licenses/>.
 *)

Require Import compcert.backend.Registers.
Require Import compcert.common.AST.
Require Import compcert.common.Events.
Require Import compcert.common.Globalenvs.
Require Import compcert.common.Memory.
Require Import compcert.common.Smallstep.
Require Import compcert.common.Values.
Require Import compcert.lib.Coqlib.
Require Import compcert.lib.Integers.
Require Import compcert.lib.Maps.
Require Import compcert.verilog.Op.

Require Import vericert.common.Vericertlib.
Require Import vericert.hls.Gible.
Require Import vericert.hls.Predicate.

GibleSeq

Module SeqBB <: BlockType.

  Definition t := list instr.

  Definition foldl {A: Type}: (A -> instr -> A) -> t -> A -> A := @fold_left A instr.

  Definition length : t -> nat := @length instr.

Instruction list step

The step_instr_list definition describes the execution of a list of instructions in one big step, inductively traversing the list of instructions and applying the step_instr.

This is simply using the high-level function step_list, which is a general function that can execute lists of things, given their execution rule.

  Definition step {A B: Type} (ge: Genv.t A B) := step_list (step_instr ge).

End SeqBB.

Module GibleSeq := Gible(SeqBB).
Export GibleSeq.

Fixpoint replace_section {A: Type} (f: A -> instr -> (A * SeqBB.t)) (s: A) (b: SeqBB.t): A * SeqBB.t :=
  match b with
  | i :: b' =>
      let (s', b'') := replace_section f s b' in
      let (s'', i') := f s' i in
      (s'', i' ++ b'')
  | nil => (s, nil)
  end.

Lemma forbidden_term_trans :
  forall A B ge sp i c b i' c',
    ~ @SeqBB.step A B ge sp (Iterm i c) b (Iterm i' c').forall (A B : Type) (ge : Genv.t A B) (sp : val)
  (i : instr_state) (c : cf_instr) (b : list instr)
  (i' : instr_state) (c' : cf_instr),
~ SeqBB.step ge sp (Iterm i c) b (Iterm i' c')
Proof.forall (A B : Type) (ge : Genv.t A B) (sp : val)
  (i : instr_state) (c : cf_instr) (b : list instr)
  (i' : instr_state) (c' : cf_instr),
~ SeqBB.step ge sp (Iterm i c) b (Iterm i' c') induction b; unfold not; intros; inv H. Qed.

Lemma step_instr_false :
  forall A B ge sp i c a i0,
    ~ @step_instr A B ge sp (Iterm i c) a (Iexec i0).forall (A B : Type) (ge : Genv.t A B) (sp : val)
  (i : instr_state) (c : cf_instr) (a : instr)
  (i0 : instr_state),
~ step_instr ge sp (Iterm i c) a (Iexec i0)
Proof.forall (A B : Type) (ge : Genv.t A B) (sp : val)
  (i : instr_state) (c : cf_instr) (a : instr)
  (i0 : instr_state),
~ step_instr ge sp (Iterm i c) a (Iexec i0) destruct a; unfold not; intros; inv H. Qed.

Lemma step_list_false :
  forall A B ge sp a i0 s,
    ~ step_list (@step_instr A B ge) sp s a (Iexec i0).forall (A B : Type) (ge : Genv.t A B) (sp : val)
  (a : list instr) (i0 : instr_state) (s : istate),
~ step_list (step_instr ge) sp s a (Iexec i0)
Proof.forall (A B : Type) (ge : Genv.t A B) (sp : val)
  (a : list instr) (i0 : instr_state) (s : istate),
~ step_list (step_instr ge) sp s a (Iexec i0) destruct a; unfold not; intros; inv H. Qed.

Lemma step_list2_false :
  forall A B ge l0 sp i c i0',
    ~ step_list2 (@step_instr A B ge) sp (Iterm i c) l0 (Iexec i0').forall (A B : Type) (ge : Genv.t A B)
  (l0 : list instr) (sp : val) (i : instr_state)
  (c : cf_instr) (i0' : instr_state),
~
step_list2 (step_instr ge) sp (Iterm i c) l0
  (Iexec i0')
Proof.forall (A B : Type) (ge : Genv.t A B)
  (l0 : list instr) (sp : val) (i : instr_state)
  (c : cf_instr) (i0' : instr_state),
~
step_list2 (step_instr ge) sp (Iterm i c) l0
  (Iexec i0')
  induction l0; unfold not; intros.A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
c: cf_instr
i0': instr_state
H: step_list2 (step_instr ge) sp (Iterm i c) nil
  (Iexec i0')
False
A, B: Type
ge: Genv.t A B
a: instr
l0: list instr
IHl0: forall (sp : val) (i : instr_state)
  (c : cf_instr) (i0' : instr_state),
~
step_list2 (step_instr ge) sp 
  (Iterm i c) l0 (Iexec i0')
sp: val
i: instr_state
c: cf_instr
i0': instr_state
H: step_list2 (step_instr ge) sp 
  (Iterm i c) (a :: l0) (Iexec i0')
False
  inv H.A, B: Type
ge: Genv.t A B
a: instr
l0: list instr
IHl0: forall (sp : val) (i : instr_state)
  (c : cf_instr) (i0' : instr_state),
~
step_list2 (step_instr ge) sp 
  (Iterm i c) l0 (Iexec i0')
sp: val
i: instr_state
c: cf_instr
i0': instr_state
H: step_list2 (step_instr ge) sp 
  (Iterm i c) (a :: l0) (Iexec i0')
False inv H.A, B: Type
ge: Genv.t A B
a: instr
l0: list instr
IHl0: forall (sp : val) (i : instr_state)
  (c : cf_instr) (i0' : instr_state),
~
step_list2 (step_instr ge) sp 
  (Iterm i c) l0 (Iexec i0')
sp: val
i: instr_state
c: cf_instr
i0': instr_state
i1: istate
H4: step_instr ge sp (Iterm i c) a i1
H6: step_list2 (step_instr ge) sp i1 l0 (Iexec i0')
False destruct i1.A, B: Type
ge: Genv.t A B
a: instr
l0: list instr
IHl0: forall (sp : val) (i : instr_state)
  (c : cf_instr) (i0' : instr_state),
~
step_list2 (step_instr ge) sp 
  (Iterm i c) l0 (Iexec i0')
sp: val
i: instr_state
c: cf_instr
i0', i0: instr_state
H4: step_instr ge sp (Iterm i c) a (Iexec i0)
H6: step_list2 (step_instr ge) sp 
  (Iexec i0) l0 (Iexec i0')
False
A, B: Type
ge: Genv.t A B
a: instr
l0: list instr
IHl0: forall (sp : val) (i : instr_state)
  (c : cf_instr) (i0' : instr_state),
~
step_list2 (step_instr ge) sp 
  (Iterm i c) l0 (Iexec i0')
sp: val
i: instr_state
c: cf_instr
i0', i0: instr_state
c0: cf_instr
H4: step_instr ge sp (Iterm i c) a (Iterm i0 c0)
H6: step_list2 (step_instr ge) sp 
  (Iterm i0 c0) l0 (Iexec i0')
False eapply step_instr_false in H4.A, B: Type
ge: Genv.t A B
a: instr
l0: list instr
IHl0: forall (sp : val) (i : instr_state)
  (c : cf_instr) (i0' : instr_state),
~
step_list2 (step_instr ge) sp 
  (Iterm i c) l0 (Iexec i0')
sp: val
i: instr_state
c: cf_instr
i0', i0: instr_state
H4: False
H6: step_list2 (step_instr ge) sp 
  (Iexec i0) l0 (Iexec i0')
False
A, B: Type
ge: Genv.t A B
a: instr
l0: list instr
IHl0: forall (sp : val) (i : instr_state)
  (c : cf_instr) (i0' : instr_state),
~
step_list2 (step_instr ge) sp 
  (Iterm i c) l0 (Iexec i0')
sp: val
i: instr_state
c: cf_instr
i0', i0: instr_state
c0: cf_instr
H4: step_instr ge sp (Iterm i c) a (Iterm i0 c0)
H6: step_list2 (step_instr ge) sp 
  (Iterm i0 c0) l0 (Iexec i0')
False auto.A, B: Type
ge: Genv.t A B
a: instr
l0: list instr
IHl0: forall (sp : val) (i : instr_state)
  (c : cf_instr) (i0' : instr_state),
~
step_list2 (step_instr ge) sp 
  (Iterm i c) l0 (Iexec i0')
sp: val
i: instr_state
c: cf_instr
i0', i0: instr_state
c0: cf_instr
H4: step_instr ge sp (Iterm i c) a (Iterm i0 c0)
H6: step_list2 (step_instr ge) sp 
  (Iterm i0 c0) l0 (Iexec i0')
False
  eapply IHl0; eauto.
Qed.

Lemma append' :
  forall A B l0 cf i0 i1 l1 sp ge i0',
    step_list2 (@step_instr A B ge) sp (Iexec i0) l0 (Iexec i0') ->
    @SeqBB.step A B ge sp (Iexec i0') l1 (Iterm i1 cf) ->
    @SeqBB.step A B ge sp (Iexec i0) (l0 ++ l1) (Iterm i1 cf).forall (A B : Type) (l0 : list instr) (cf : cf_instr)
  (i0 i1 : instr_state) (l1 : list instr) (sp : val)
  (ge : Genv.t A B) (i0' : instr_state),
step_list2 (step_instr ge) sp (Iexec i0) l0
  (Iexec i0') ->
SeqBB.step ge sp (Iexec i0') l1 (Iterm i1 cf) ->
SeqBB.step ge sp (Iexec i0) (l0 ++ l1) (Iterm i1 cf)
Proof.forall (A B : Type) (l0 : list instr) (cf : cf_instr)
  (i0 i1 : instr_state) (l1 : list instr) (sp : val)
  (ge : Genv.t A B) (i0' : instr_state),
step_list2 (step_instr ge) sp (Iexec i0) l0
  (Iexec i0') ->
SeqBB.step ge sp (Iexec i0') l1 (Iterm i1 cf) ->
SeqBB.step ge sp (Iexec i0) (l0 ++ l1) (Iterm i1 cf)
  induction l0; crush.A, B: Type
cf: cf_instr
i0, i1: instr_state
l1: list instr
sp: val
ge: Genv.t A B
i0': instr_state
H: step_list2 (step_instr ge) sp (Iexec i0) nil
  (Iexec i0')
H0: SeqBB.step ge sp (Iexec i0') l1 (Iterm i1 cf)
SeqBB.step ge sp (Iexec i0) l1 (Iterm i1 cf)
A, B: Type
a: instr
l0: list instr
IHl0: forall (cf : cf_instr) (i0 i1 : instr_state)
  (l1 : list instr) (sp : val)
  (ge : Genv.t A B) (i0' : instr_state),
step_list2 (step_instr ge) sp 
  (Iexec i0) l0 (Iexec i0') ->
SeqBB.step ge sp (Iexec i0') l1 (Iterm i1 cf) ->
SeqBB.step ge sp (Iexec i0) 
  (l0 ++ l1) (Iterm i1 cf)
cf: cf_instr
i0, i1: instr_state
l1: list instr
sp: val
ge: Genv.t A B
i0': instr_state
H: step_list2 (step_instr ge) sp 
  (Iexec i0) (a :: l0) (Iexec i0')
H0: SeqBB.step ge sp (Iexec i0') l1 (Iterm i1 cf)
SeqBB.step ge sp (Iexec i0) (a :: l0 ++ l1)
  (Iterm i1 cf) inv H.A, B: Type
cf: cf_instr
i1: instr_state
l1: list instr
sp: val
ge: Genv.t A B
i0': instr_state
H0: SeqBB.step ge sp (Iexec i0') l1 (Iterm i1 cf)
SeqBB.step ge sp (Iexec i0') l1 (Iterm i1 cf)
A, B: Type
a: instr
l0: list instr
IHl0: forall (cf : cf_instr) (i0 i1 : instr_state)
  (l1 : list instr) (sp : val)
  (ge : Genv.t A B) (i0' : instr_state),
step_list2 (step_instr ge) sp 
  (Iexec i0) l0 (Iexec i0') ->
SeqBB.step ge sp (Iexec i0') l1 (Iterm i1 cf) ->
SeqBB.step ge sp (Iexec i0) 
  (l0 ++ l1) (Iterm i1 cf)
cf: cf_instr
i0, i1: instr_state
l1: list instr
sp: val
ge: Genv.t A B
i0': instr_state
H: step_list2 (step_instr ge) sp 
  (Iexec i0) (a :: l0) (Iexec i0')
H0: SeqBB.step ge sp (Iexec i0') l1 (Iterm i1 cf)
SeqBB.step ge sp (Iexec i0) (a :: l0 ++ l1)
  (Iterm i1 cf) eauto.A, B: Type
a: instr
l0: list instr
IHl0: forall (cf : cf_instr) (i0 i1 : instr_state)
  (l1 : list instr) (sp : val)
  (ge : Genv.t A B) (i0' : instr_state),
step_list2 (step_instr ge) sp 
  (Iexec i0) l0 (Iexec i0') ->
SeqBB.step ge sp (Iexec i0') l1 (Iterm i1 cf) ->
SeqBB.step ge sp (Iexec i0) 
  (l0 ++ l1) (Iterm i1 cf)
cf: cf_instr
i0, i1: instr_state
l1: list instr
sp: val
ge: Genv.t A B
i0': instr_state
H: step_list2 (step_instr ge) sp 
  (Iexec i0) (a :: l0) (Iexec i0')
H0: SeqBB.step ge sp (Iexec i0') l1 (Iterm i1 cf)
SeqBB.step ge sp (Iexec i0) (a :: l0 ++ l1)
  (Iterm i1 cf) inv H.A, B: Type
a: instr
l0: list instr
IHl0: forall (cf : cf_instr) (i0 i1 : instr_state)
  (l1 : list instr) (sp : val)
  (ge : Genv.t A B) (i0' : instr_state),
step_list2 (step_instr ge) sp 
  (Iexec i0) l0 (Iexec i0') ->
SeqBB.step ge sp (Iexec i0') l1 (Iterm i1 cf) ->
SeqBB.step ge sp (Iexec i0) 
  (l0 ++ l1) (Iterm i1 cf)
cf: cf_instr
i0, i1: instr_state
l1: list instr
sp: val
ge: Genv.t A B
i0': instr_state
H0: SeqBB.step ge sp (Iexec i0') l1 (Iterm i1 cf)
i3: istate
H5: step_instr ge sp (Iexec i0) a i3
H7: step_list2 (step_instr ge) sp i3 l0 (Iexec i0')
SeqBB.step ge sp (Iexec i0) (a :: l0 ++ l1)
  (Iterm i1 cf) destruct i3.A, B: Type
a: instr
l0: list instr
IHl0: forall (cf : cf_instr) (i0 i1 : instr_state)
  (l1 : list instr) (sp : val)
  (ge : Genv.t A B) (i0' : instr_state),
step_list2 (step_instr ge) sp 
  (Iexec i0) l0 (Iexec i0') ->
SeqBB.step ge sp (Iexec i0') l1 (Iterm i1 cf) ->
SeqBB.step ge sp (Iexec i0) 
  (l0 ++ l1) (Iterm i1 cf)
cf: cf_instr
i0, i1: instr_state
l1: list instr
sp: val
ge: Genv.t A B
i0': instr_state
H0: SeqBB.step ge sp (Iexec i0') l1 (Iterm i1 cf)
i: instr_state
H5: step_instr ge sp (Iexec i0) a (Iexec i)
H7: step_list2 (step_instr ge) sp 
  (Iexec i) l0 (Iexec i0')
SeqBB.step ge sp (Iexec i0) (a :: l0 ++ l1)
  (Iterm i1 cf)
A, B: Type
a: instr
l0: list instr
IHl0: forall (cf : cf_instr) (i0 i1 : instr_state)
  (l1 : list instr) (sp : val)
  (ge : Genv.t A B) (i0' : instr_state),
step_list2 (step_instr ge) sp 
  (Iexec i0) l0 (Iexec i0') ->
SeqBB.step ge sp (Iexec i0') l1 (Iterm i1 cf) ->
SeqBB.step ge sp (Iexec i0) 
  (l0 ++ l1) (Iterm i1 cf)
cf: cf_instr
i0, i1: instr_state
l1: list instr
sp: val
ge: Genv.t A B
i0': instr_state
H0: SeqBB.step ge sp (Iexec i0') l1 (Iterm i1 cf)
i: instr_state
c: cf_instr
H5: step_instr ge sp (Iexec i0) a (Iterm i c)
H7: step_list2 (step_instr ge) sp 
  (Iterm i c) l0 (Iexec i0')
SeqBB.step ge sp (Iexec i0) 
  (a :: l0 ++ l1) (Iterm i1 cf)
  econstructor; eauto.A, B: Type
a: instr
l0: list instr
IHl0: forall (cf : cf_instr) (i0 i1 : instr_state)
  (l1 : list instr) (sp : val)
  (ge : Genv.t A B) (i0' : instr_state),
step_list2 (step_instr ge) sp 
  (Iexec i0) l0 (Iexec i0') ->
SeqBB.step ge sp (Iexec i0') l1 (Iterm i1 cf) ->
SeqBB.step ge sp (Iexec i0) 
  (l0 ++ l1) (Iterm i1 cf)
cf: cf_instr
i0, i1: instr_state
l1: list instr
sp: val
ge: Genv.t A B
i0': instr_state
H0: SeqBB.step ge sp (Iexec i0') l1 (Iterm i1 cf)
i: instr_state
H5: step_instr ge sp (Iexec i0) a (Iexec i)
H7: step_list2 (step_instr ge) sp 
  (Iexec i) l0 (Iexec i0')
step_list (step_instr ge) sp (Iexec i) (l0 ++ l1)
  (Iterm i1 cf)
A, B: Type
a: instr
l0: list instr
IHl0: forall (cf : cf_instr) (i0 i1 : instr_state)
  (l1 : list instr) (sp : val)
  (ge : Genv.t A B) (i0' : instr_state),
step_list2 (step_instr ge) sp 
  (Iexec i0) l0 (Iexec i0') ->
SeqBB.step ge sp (Iexec i0') l1 (Iterm i1 cf) ->
SeqBB.step ge sp (Iexec i0) 
  (l0 ++ l1) (Iterm i1 cf)
cf: cf_instr
i0, i1: instr_state
l1: list instr
sp: val
ge: Genv.t A B
i0': instr_state
H0: SeqBB.step ge sp (Iexec i0') l1 (Iterm i1 cf)
i: instr_state
c: cf_instr
H5: step_instr ge sp (Iexec i0) a (Iterm i c)
H7: step_list2 (step_instr ge) sp 
  (Iterm i c) l0 (Iexec i0')
SeqBB.step ge sp (Iexec i0) 
  (a :: l0 ++ l1) (Iterm i1 cf) eapply IHl0; eauto.A, B: Type
a: instr
l0: list instr
IHl0: forall (cf : cf_instr) (i0 i1 : instr_state)
  (l1 : list instr) (sp : val)
  (ge : Genv.t A B) (i0' : instr_state),
step_list2 (step_instr ge) sp 
  (Iexec i0) l0 (Iexec i0') ->
SeqBB.step ge sp (Iexec i0') l1 (Iterm i1 cf) ->
SeqBB.step ge sp (Iexec i0) 
  (l0 ++ l1) (Iterm i1 cf)
cf: cf_instr
i0, i1: instr_state
l1: list instr
sp: val
ge: Genv.t A B
i0': instr_state
H0: SeqBB.step ge sp (Iexec i0') l1 (Iterm i1 cf)
i: instr_state
c: cf_instr
H5: step_instr ge sp (Iexec i0) a (Iterm i c)
H7: step_list2 (step_instr ge) sp 
  (Iterm i c) l0 (Iexec i0')
SeqBB.step ge sp (Iexec i0) (a :: l0 ++ l1)
  (Iterm i1 cf)
  eapply step_list2_false in H7.A, B: Type
a: instr
l0: list instr
IHl0: forall (cf : cf_instr) (i0 i1 : instr_state)
  (l1 : list instr) (sp : val)
  (ge : Genv.t A B) (i0' : instr_state),
step_list2 (step_instr ge) sp 
  (Iexec i0) l0 (Iexec i0') ->
SeqBB.step ge sp (Iexec i0') l1 (Iterm i1 cf) ->
SeqBB.step ge sp (Iexec i0) 
  (l0 ++ l1) (Iterm i1 cf)
cf: cf_instr
i0, i1: instr_state
l1: list instr
sp: val
ge: Genv.t A B
i0': instr_state
H0: SeqBB.step ge sp (Iexec i0') l1 (Iterm i1 cf)
i: instr_state
c: cf_instr
H5: step_instr ge sp (Iexec i0) a (Iterm i c)
H7: False
SeqBB.step ge sp (Iexec i0) (a :: l0 ++ l1)
  (Iterm i1 cf) exfalso; auto.
Qed.

Lemma append :
  forall A B cf i0 i1 l0 l1 sp ge,
      (exists i0', step_list2 (@step_instr A B ge) sp (Iexec i0) l0 (Iexec i0') /\
                    @SeqBB.step A B ge sp (Iexec i0') l1 (Iterm i1 cf)) ->
    @SeqBB.step A B ge sp (Iexec i0) (l0 ++ l1) (Iterm i1 cf).forall (A B : Type) (cf : cf_instr)
  (i0 i1 : instr_state) (l0 l1 : list instr)
  (sp : val) (ge : Genv.t A B),
(exists i0' : instr_state,
   step_list2 (step_instr ge) sp (Iexec i0) l0
     (Iexec i0') /\
   SeqBB.step ge sp (Iexec i0') l1 (Iterm i1 cf)) ->
SeqBB.step ge sp (Iexec i0) (l0 ++ l1) (Iterm i1 cf)
Proof.forall (A B : Type) (cf : cf_instr)
  (i0 i1 : instr_state) (l0 l1 : list instr)
  (sp : val) (ge : Genv.t A B),
(exists i0' : instr_state,
   step_list2 (step_instr ge) sp (Iexec i0) l0
     (Iexec i0') /\
   SeqBB.step ge sp (Iexec i0') l1 (Iterm i1 cf)) ->
SeqBB.step ge sp (Iexec i0) (l0 ++ l1) (Iterm i1 cf) intros.A, B: Type
cf: cf_instr
i0, i1: instr_state
l0, l1: list instr
sp: val
ge: Genv.t A B
H: exists i0' : instr_state,
  step_list2 (step_instr ge) sp (Iexec i0) l0
    (Iexec i0') /\
  SeqBB.step ge sp (Iexec i0') l1 (Iterm i1 cf)
SeqBB.step ge sp (Iexec i0) (l0 ++ l1) (Iterm i1 cf) simplify.A, B: Type
cf: cf_instr
i0, i1: instr_state
l0, l1: list instr
sp: val
ge: Genv.t A B
x: instr_state
H: step_list2 (step_instr ge) sp (Iexec i0) l0
  (Iexec x)
H1: SeqBB.step ge sp (Iexec x) l1 (Iterm i1 cf)
SeqBB.step ge sp (Iexec i0) (l0 ++ l1) (Iterm i1 cf) eapply append'; eauto. Qed.

Lemma append2 :
  forall A B l0 cf i0 i1 l1 sp ge,
    @SeqBB.step A B ge sp (Iexec i0) l0 (Iterm i1 cf) ->
    @SeqBB.step A B ge sp (Iexec i0) (l0 ++ l1) (Iterm i1 cf).forall (A B : Type) (l0 : list instr) (cf : cf_instr)
  (i0 i1 : instr_state) (l1 : list instr) (sp : val)
  (ge : Genv.t A B),
SeqBB.step ge sp (Iexec i0) l0 (Iterm i1 cf) ->
SeqBB.step ge sp (Iexec i0) (l0 ++ l1) (Iterm i1 cf)
Proof.forall (A B : Type) (l0 : list instr) (cf : cf_instr)
  (i0 i1 : instr_state) (l1 : list instr) (sp : val)
  (ge : Genv.t A B),
SeqBB.step ge sp (Iexec i0) l0 (Iterm i1 cf) ->
SeqBB.step ge sp (Iexec i0) (l0 ++ l1) (Iterm i1 cf)
  induction l0; crush.A, B: Type
cf: cf_instr
i0, i1: instr_state
l1: list instr
sp: val
ge: Genv.t A B
H: SeqBB.step ge sp (Iexec i0) nil (Iterm i1 cf)
SeqBB.step ge sp (Iexec i0) l1 (Iterm i1 cf)
A, B: Type
a: instr
l0: list instr
IHl0: forall (cf : cf_instr) (i0 i1 : instr_state)
  (l1 : list instr) (sp : val)
  (ge : Genv.t A B),
SeqBB.step ge sp (Iexec i0) l0 (Iterm i1 cf) ->
SeqBB.step ge sp (Iexec i0) 
  (l0 ++ l1) (Iterm i1 cf)
cf: cf_instr
i0, i1: instr_state
l1: list instr
sp: val
ge: Genv.t A B
H: SeqBB.step ge sp (Iexec i0) 
  (a :: l0) (Iterm i1 cf)
SeqBB.step ge sp (Iexec i0) (a :: l0 ++ l1)
  (Iterm i1 cf)
  inv H.A, B: Type
a: instr
l0: list instr
IHl0: forall (cf : cf_instr) (i0 i1 : instr_state)
  (l1 : list instr) (sp : val)
  (ge : Genv.t A B),
SeqBB.step ge sp (Iexec i0) l0 (Iterm i1 cf) ->
SeqBB.step ge sp (Iexec i0) 
  (l0 ++ l1) (Iterm i1 cf)
cf: cf_instr
i0, i1: instr_state
l1: list instr
sp: val
ge: Genv.t A B
H: SeqBB.step ge sp (Iexec i0) 
  (a :: l0) (Iterm i1 cf)
SeqBB.step ge sp (Iexec i0) (a :: l0 ++ l1)
  (Iterm i1 cf)
  inv H.A, B: Type
a: instr
l0: list instr
IHl0: forall (cf : cf_instr) (i0 i1 : instr_state)
  (l1 : list instr) (sp : val)
  (ge : Genv.t A B),
SeqBB.step ge sp (Iexec i0) l0 (Iterm i1 cf) ->
SeqBB.step ge sp (Iexec i0) 
  (l0 ++ l1) (Iterm i1 cf)
cf: cf_instr
i0, i1: instr_state
l1: list instr
sp: val
ge: Genv.t A B
state': instr_state
H5: step_instr ge sp (Iexec i0) a (Iexec state')
H7: step_list (step_instr ge) sp 
  (Iexec state') l0 (Iterm i1 cf)
SeqBB.step ge sp (Iexec i0) (a :: l0 ++ l1)
  (Iterm i1 cf)
A, B: Type
a: instr
l0: list instr
IHl0: forall (cf : cf_instr) (i0 i1 : instr_state)
  (l1 : list instr) (sp : val)
  (ge : Genv.t A B),
SeqBB.step ge sp (Iexec i0) l0 (Iterm i1 cf) ->
SeqBB.step ge sp (Iexec i0) 
  (l0 ++ l1) (Iterm i1 cf)
cf: cf_instr
i0, i1: instr_state
l1: list instr
sp: val
ge: Genv.t A B
H3: step_instr ge sp (Iexec i0) a (Iterm i1 cf)
SeqBB.step ge sp (Iexec i0) 
  (a :: l0 ++ l1) (Iterm i1 cf) econstructor; eauto.A, B: Type
a: instr
l0: list instr
IHl0: forall (cf : cf_instr) (i0 i1 : instr_state)
  (l1 : list instr) (sp : val)
  (ge : Genv.t A B),
SeqBB.step ge sp (Iexec i0) l0 (Iterm i1 cf) ->
SeqBB.step ge sp (Iexec i0) 
  (l0 ++ l1) (Iterm i1 cf)
cf: cf_instr
i0, i1: instr_state
l1: list instr
sp: val
ge: Genv.t A B
state': instr_state
H5: step_instr ge sp (Iexec i0) a (Iexec state')
H7: step_list (step_instr ge) sp 
  (Iexec state') l0 (Iterm i1 cf)
step_list (step_instr ge) sp (Iexec state') (l0 ++ l1)
  (Iterm i1 cf)
A, B: Type
a: instr
l0: list instr
IHl0: forall (cf : cf_instr) (i0 i1 : instr_state)
  (l1 : list instr) (sp : val)
  (ge : Genv.t A B),
SeqBB.step ge sp (Iexec i0) l0 (Iterm i1 cf) ->
SeqBB.step ge sp (Iexec i0) 
  (l0 ++ l1) (Iterm i1 cf)
cf: cf_instr
i0, i1: instr_state
l1: list instr
sp: val
ge: Genv.t A B
H3: step_instr ge sp (Iexec i0) a (Iterm i1 cf)
SeqBB.step ge sp (Iexec i0) 
  (a :: l0 ++ l1) (Iterm i1 cf) eapply IHl0; eauto.A, B: Type
a: instr
l0: list instr
IHl0: forall (cf : cf_instr) (i0 i1 : instr_state)
  (l1 : list instr) (sp : val)
  (ge : Genv.t A B),
SeqBB.step ge sp (Iexec i0) l0 (Iterm i1 cf) ->
SeqBB.step ge sp (Iexec i0) 
  (l0 ++ l1) (Iterm i1 cf)
cf: cf_instr
i0, i1: instr_state
l1: list instr
sp: val
ge: Genv.t A B
H3: step_instr ge sp (Iexec i0) a (Iterm i1 cf)
SeqBB.step ge sp (Iexec i0) (a :: l0 ++ l1)
  (Iterm i1 cf)
  constructor; auto.
Qed.

#[local] Notation "'mki'" := (mk_instr_state) (at level 1).

Lemma exec_rbexit_truthy :
  forall A B bb ge sp rs pr m rs' pr' m' cf,
    @SeqBB.step A B ge sp (Iexec (mki rs pr m)) bb (Iterm (mki rs' pr' m') cf) ->
    exists p b1 b2,
      truthy pr' p
      /\ bb = b1 ++ (RBexit p cf) :: b2
      /\ step_list2 (Gible.step_instr ge) sp (Iexec (mki rs pr m)) b1 (Iexec (mki rs' pr' m')).forall (A B : Type) (bb : list instr)
  (ge : Genv.t A B) (sp : val) (rs : regset)
  (pr : predset) (m : mem) (rs' : regset)
  (pr' : predset) (m' : mem) (cf : cf_instr),
SeqBB.step ge sp (Iexec (mki rs pr m)) bb
  (Iterm (mki rs' pr' m') cf) ->
exists
  (p : option Gible.pred_op) (b1 b2 : list instr),
  truthy pr' p /\
  bb = b1 ++ RBexit p cf :: b2 /\
  step_list2 (step_instr ge) sp (Iexec (mki rs pr m))
    b1 (Iexec (mki rs' pr' m'))
Proof.forall (A B : Type) (bb : list instr)
  (ge : Genv.t A B) (sp : val) (rs : regset)
  (pr : predset) (m : mem) (rs' : regset)
  (pr' : predset) (m' : mem) (cf : cf_instr),
SeqBB.step ge sp (Iexec (mki rs pr m)) bb
  (Iterm (mki rs' pr' m') cf) ->
exists
  (p : option Gible.pred_op) (b1 b2 : list instr),
  truthy pr' p /\
  bb = b1 ++ RBexit p cf :: b2 /\
  step_list2 (step_instr ge) sp (Iexec (mki rs pr m))
    b1 (Iexec (mki rs' pr' m'))
  induction bb; crush.A, B: Type
ge: Genv.t A B
sp: val
rs: regset
pr: predset
m: mem
rs': regset
pr': predset
m': mem
cf: cf_instr
H: SeqBB.step ge sp (Iexec (mki rs pr m)) nil
  (Iterm (mki rs' pr' m') cf)
exists
  (p : option Gible.pred_op) (b1 b2 : list instr),
  truthy pr' p /\
  nil = b1 ++ RBexit p cf :: b2 /\
  step_list2 (step_instr ge) sp (Iexec (mki rs pr m))
    b1 (Iexec (mki rs' pr' m'))
A, B: Type
a: instr
bb: list instr
IHbb: forall (ge : Genv.t A B) 
  (sp : val) (rs : regset) 
  (pr : predset) (m : mem) 
  (rs' : regset) (pr' : predset) 
  (m' : mem) (cf : cf_instr),
SeqBB.step ge sp (Iexec (mki rs pr m)) bb
  (Iterm (mki rs' pr' m') cf) ->
exists
  (p : option Gible.pred_op) 
(b1 b2 : list instr),
  truthy pr' p /\
  bb = b1 ++ RBexit p cf :: b2 /\
  step_list2 (step_instr ge) sp
    (Iexec (mki rs pr m)) b1
    (Iexec (mki rs' pr' m'))
ge: Genv.t A B
sp: val
rs: regset
pr: predset
m: mem
rs': regset
pr': predset
m': mem
cf: cf_instr
H: SeqBB.step ge sp (Iexec (mki rs pr m)) 
  (a :: bb) (Iterm (mki rs' pr' m') cf)
exists
  (p : option Gible.pred_op) (b1 b2 : list instr),
  truthy pr' p /\
  a :: bb = b1 ++ RBexit p cf :: b2 /\
  step_list2 (step_instr ge) sp (Iexec (mki rs pr m))
    b1 (Iexec (mki rs' pr' m'))
  inv H.A, B: Type
a: instr
bb: list instr
IHbb: forall (ge : Genv.t A B) 
  (sp : val) (rs : regset) 
  (pr : predset) (m : mem) 
  (rs' : regset) (pr' : predset) 
  (m' : mem) (cf : cf_instr),
SeqBB.step ge sp (Iexec (mki rs pr m)) bb
  (Iterm (mki rs' pr' m') cf) ->
exists
  (p : option Gible.pred_op) 
(b1 b2 : list instr),
  truthy pr' p /\
  bb = b1 ++ RBexit p cf :: b2 /\
  step_list2 (step_instr ge) sp
    (Iexec (mki rs pr m)) b1
    (Iexec (mki rs' pr' m'))
ge: Genv.t A B
sp: val
rs: regset
pr: predset
m: mem
rs': regset
pr': predset
m': mem
cf: cf_instr
H: SeqBB.step ge sp (Iexec (mki rs pr m)) 
  (a :: bb) (Iterm (mki rs' pr' m') cf)
exists
  (p : option Gible.pred_op) (b1 b2 : list instr),
  truthy pr' p /\
  a :: bb = b1 ++ RBexit p cf :: b2 /\
  step_list2 (step_instr ge) sp (Iexec (mki rs pr m))
    b1 (Iexec (mki rs' pr' m')) inv H.A, B: Type
a: instr
bb: list instr
IHbb: forall (ge : Genv.t A B) 
  (sp : val) (rs : regset) 
  (pr : predset) (m : mem) 
  (rs' : regset) (pr' : predset) 
  (m' : mem) (cf : cf_instr),
SeqBB.step ge sp (Iexec (mki rs pr m)) bb
  (Iterm (mki rs' pr' m') cf) ->
exists
  (p : option Gible.pred_op) 
(b1 b2 : list instr),
  truthy pr' p /\
  bb = b1 ++ RBexit p cf :: b2 /\
  step_list2 (step_instr ge) sp
    (Iexec (mki rs pr m)) b1
    (Iexec (mki rs' pr' m'))
ge: Genv.t A B
sp: val
rs: regset
pr: predset
m: mem
rs': regset
pr': predset
m': mem
cf: cf_instr
state': instr_state
H5: step_instr ge sp (Iexec (mki rs pr m)) a
  (Iexec state')
H7: step_list (step_instr ge) sp 
  (Iexec state') bb (Iterm (mki rs' pr' m') cf)
exists
  (p : option Gible.pred_op) (b1 b2 : list instr),
  truthy pr' p /\
  a :: bb = b1 ++ RBexit p cf :: b2 /\
  step_list2 (step_instr ge) sp (Iexec (mki rs pr m))
    b1 (Iexec (mki rs' pr' m'))
A, B: Type
a: instr
bb: list instr
IHbb: forall (ge : Genv.t A B) 
  (sp : val) (rs : regset) 
  (pr : predset) (m : mem) 
  (rs' : regset) (pr' : predset) 
  (m' : mem) (cf : cf_instr),
SeqBB.step ge sp (Iexec (mki rs pr m)) bb
  (Iterm (mki rs' pr' m') cf) ->
exists
  (p : option Gible.pred_op) 
(b1 b2 : list instr),
  truthy pr' p /\
  bb = b1 ++ RBexit p cf :: b2 /\
  step_list2 (step_instr ge) sp
    (Iexec (mki rs pr m)) b1
    (Iexec (mki rs' pr' m'))
ge: Genv.t A B
sp: val
rs: regset
pr: predset
m: mem
rs': regset
pr': predset
m': mem
cf: cf_instr
H3: step_instr ge sp (Iexec (mki rs pr m)) a
  (Iterm (mki rs' pr' m') cf)
exists
  (p : option Gible.pred_op) 
(b1 b2 : list instr),
  truthy pr' p /\
  a :: bb = b1 ++ RBexit p cf :: b2 /\
  step_list2 (step_instr ge) sp 
    (Iexec (mki rs pr m)) b1 
    (Iexec (mki rs' pr' m'))
  -A, B: Type
a: instr
bb: list instr
IHbb: forall (ge : Genv.t A B) 
  (sp : val) (rs : regset) 
  (pr : predset) (m : mem) 
  (rs' : regset) (pr' : predset) 
  (m' : mem) (cf : cf_instr),
SeqBB.step ge sp (Iexec (mki rs pr m)) bb
  (Iterm (mki rs' pr' m') cf) ->
exists
  (p : option Gible.pred_op) 
(b1 b2 : list instr),
  truthy pr' p /\
  bb = b1 ++ RBexit p cf :: b2 /\
  step_list2 (step_instr ge) sp
    (Iexec (mki rs pr m)) b1
    (Iexec (mki rs' pr' m'))
ge: Genv.t A B
sp: val
rs: regset
pr: predset
m: mem
rs': regset
pr': predset
m': mem
cf: cf_instr
state': instr_state
H5: step_instr ge sp (Iexec (mki rs pr m)) a
  (Iexec state')
H7: step_list (step_instr ge) sp 
  (Iexec state') bb (Iterm (mki rs' pr' m') cf)
exists
  (p : option Gible.pred_op) (b1 b2 : list instr),
  truthy pr' p /\
  a :: bb = b1 ++ RBexit p cf :: b2 /\
  step_list2 (step_instr ge) sp (Iexec (mki rs pr m))
    b1 (Iexec (mki rs' pr' m')) destruct state'.A, B: Type
a: instr
bb: list instr
IHbb: forall (ge : Genv.t A B) 
  (sp : val) (rs : regset) 
  (pr : predset) (m : mem) 
  (rs' : regset) (pr' : predset) 
  (m' : mem) (cf : cf_instr),
SeqBB.step ge sp (Iexec (mki rs pr m)) bb
  (Iterm (mki rs' pr' m') cf) ->
exists
  (p : option Gible.pred_op) 
(b1 b2 : list instr),
  truthy pr' p /\
  bb = b1 ++ RBexit p cf :: b2 /\
  step_list2 (step_instr ge) sp
    (Iexec (mki rs pr m)) b1
    (Iexec (mki rs' pr' m'))
ge: Genv.t A B
sp: val
rs: regset
pr: predset
m: mem
rs': regset
pr': predset
m': mem
cf: cf_instr
is_rs: regset
is_ps: predset
is_mem: mem
H5: step_instr ge sp (Iexec (mki rs pr m)) a
  (Iexec (mki is_rs is_ps is_mem))
H7: step_list (step_instr ge) sp
  (Iexec (mki is_rs is_ps is_mem)) bb
  (Iterm (mki rs' pr' m') cf)
exists
  (p : option Gible.pred_op) (b1 b2 : list instr),
  truthy pr' p /\
  a :: bb = b1 ++ RBexit p cf :: b2 /\
  step_list2 (step_instr ge) sp (Iexec (mki rs pr m))
    b1 (Iexec (mki rs' pr' m')) exploit IHbb; eauto; simplify.A, B: Type
a: instr
cf: cf_instr
x: option Gible.pred_op
x0, x1: list instr
IHbb: forall (ge : Genv.t A B) 
  (sp : val) (rs : regset) 
  (pr : predset) (m : mem) 
  (rs' : regset) (pr' : predset) 
  (m' : mem) (cf0 : cf_instr),
SeqBB.step ge sp (Iexec (mki rs pr m))
  (x0 ++ RBexit x cf :: x1)
  (Iterm (mki rs' pr' m') cf0) ->
exists
  (p : option Gible.pred_op) 
(b1 b2 : list instr),
  truthy pr' p /\
  x0 ++ RBexit x cf :: x1 =
  b1 ++ RBexit p cf0 :: b2 /\
  step_list2 (step_instr ge) sp
    (Iexec (mki rs pr m)) b1
    (Iexec (mki rs' pr' m'))
ge: Genv.t A B
sp: val
rs: regset
pr: predset
m: mem
rs': regset
pr': predset
m': mem
is_rs: regset
is_ps: predset
is_mem: mem
H5: step_instr ge sp (Iexec (mki rs pr m)) a
  (Iexec (mki is_rs is_ps is_mem))
H7: step_list (step_instr ge) sp
  (Iexec (mki is_rs is_ps is_mem))
  (x0 ++ RBexit x cf :: x1)
  (Iterm (mki rs' pr' m') cf)
H: truthy pr' x
H2: step_list2 (step_instr ge) sp
  (Iexec (mki is_rs is_ps is_mem)) x0
  (Iexec (mki rs' pr' m'))
exists
  (p : option Gible.pred_op) (b1 b2 : list instr),
  truthy pr' p /\
  a :: x0 ++ RBexit x cf :: x1 =
  b1 ++ RBexit p cf :: b2 /\
  step_list2 (step_instr ge) sp (Iexec (mki rs pr m))
    b1 (Iexec (mki rs' pr' m'))
    exists x.A, B: Type
a: instr
cf: cf_instr
x: option Gible.pred_op
x0, x1: list instr
IHbb: forall (ge : Genv.t A B) 
  (sp : val) (rs : regset) 
  (pr : predset) (m : mem) 
  (rs' : regset) (pr' : predset) 
  (m' : mem) (cf0 : cf_instr),
SeqBB.step ge sp (Iexec (mki rs pr m))
  (x0 ++ RBexit x cf :: x1)
  (Iterm (mki rs' pr' m') cf0) ->
exists
  (p : option Gible.pred_op) 
(b1 b2 : list instr),
  truthy pr' p /\
  x0 ++ RBexit x cf :: x1 =
  b1 ++ RBexit p cf0 :: b2 /\
  step_list2 (step_instr ge) sp
    (Iexec (mki rs pr m)) b1
    (Iexec (mki rs' pr' m'))
ge: Genv.t A B
sp: val
rs: regset
pr: predset
m: mem
rs': regset
pr': predset
m': mem
is_rs: regset
is_ps: predset
is_mem: mem
H5: step_instr ge sp (Iexec (mki rs pr m)) a
  (Iexec (mki is_rs is_ps is_mem))
H7: step_list (step_instr ge) sp
  (Iexec (mki is_rs is_ps is_mem))
  (x0 ++ RBexit x cf :: x1)
  (Iterm (mki rs' pr' m') cf)
H: truthy pr' x
H2: step_list2 (step_instr ge) sp
  (Iexec (mki is_rs is_ps is_mem)) x0
  (Iexec (mki rs' pr' m'))
exists b1 b2 : list instr,
  truthy pr' x /\
  a :: x0 ++ RBexit x cf :: x1 =
  b1 ++ RBexit x cf :: b2 /\
  step_list2 (step_instr ge) sp (Iexec (mki rs pr m))
    b1 (Iexec (mki rs' pr' m')) exists (a :: x0).A, B: Type
a: instr
cf: cf_instr
x: option Gible.pred_op
x0, x1: list instr
IHbb: forall (ge : Genv.t A B) 
  (sp : val) (rs : regset) 
  (pr : predset) (m : mem) 
  (rs' : regset) (pr' : predset) 
  (m' : mem) (cf0 : cf_instr),
SeqBB.step ge sp (Iexec (mki rs pr m))
  (x0 ++ RBexit x cf :: x1)
  (Iterm (mki rs' pr' m') cf0) ->
exists
  (p : option Gible.pred_op) 
(b1 b2 : list instr),
  truthy pr' p /\
  x0 ++ RBexit x cf :: x1 =
  b1 ++ RBexit p cf0 :: b2 /\
  step_list2 (step_instr ge) sp
    (Iexec (mki rs pr m)) b1
    (Iexec (mki rs' pr' m'))
ge: Genv.t A B
sp: val
rs: regset
pr: predset
m: mem
rs': regset
pr': predset
m': mem
is_rs: regset
is_ps: predset
is_mem: mem
H5: step_instr ge sp (Iexec (mki rs pr m)) a
  (Iexec (mki is_rs is_ps is_mem))
H7: step_list (step_instr ge) sp
  (Iexec (mki is_rs is_ps is_mem))
  (x0 ++ RBexit x cf :: x1)
  (Iterm (mki rs' pr' m') cf)
H: truthy pr' x
H2: step_list2 (step_instr ge) sp
  (Iexec (mki is_rs is_ps is_mem)) x0
  (Iexec (mki rs' pr' m'))
exists b2 : list instr,
  truthy pr' x /\
  a :: x0 ++ RBexit x cf :: x1 =
  (a :: x0) ++ RBexit x cf :: b2 /\
  step_list2 (step_instr ge) sp (Iexec (mki rs pr m))
    (a :: x0) (Iexec (mki rs' pr' m')) exists x1.A, B: Type
a: instr
cf: cf_instr
x: option Gible.pred_op
x0, x1: list instr
IHbb: forall (ge : Genv.t A B) 
  (sp : val) (rs : regset) 
  (pr : predset) (m : mem) 
  (rs' : regset) (pr' : predset) 
  (m' : mem) (cf0 : cf_instr),
SeqBB.step ge sp (Iexec (mki rs pr m))
  (x0 ++ RBexit x cf :: x1)
  (Iterm (mki rs' pr' m') cf0) ->
exists
  (p : option Gible.pred_op) 
(b1 b2 : list instr),
  truthy pr' p /\
  x0 ++ RBexit x cf :: x1 =
  b1 ++ RBexit p cf0 :: b2 /\
  step_list2 (step_instr ge) sp
    (Iexec (mki rs pr m)) b1
    (Iexec (mki rs' pr' m'))
ge: Genv.t A B
sp: val
rs: regset
pr: predset
m: mem
rs': regset
pr': predset
m': mem
is_rs: regset
is_ps: predset
is_mem: mem
H5: step_instr ge sp (Iexec (mki rs pr m)) a
  (Iexec (mki is_rs is_ps is_mem))
H7: step_list (step_instr ge) sp
  (Iexec (mki is_rs is_ps is_mem))
  (x0 ++ RBexit x cf :: x1)
  (Iterm (mki rs' pr' m') cf)
H: truthy pr' x
H2: step_list2 (step_instr ge) sp
  (Iexec (mki is_rs is_ps is_mem)) x0
  (Iexec (mki rs' pr' m'))
truthy pr' x /\
a :: x0 ++ RBexit x cf :: x1 =
(a :: x0) ++ RBexit x cf :: x1 /\
step_list2 (step_instr ge) sp (Iexec (mki rs pr m))
  (a :: x0) (Iexec (mki rs' pr' m')) simplify; auto.A, B: Type
a: instr
cf: cf_instr
x: option Gible.pred_op
x0, x1: list instr
IHbb: forall (ge : Genv.t A B) 
  (sp : val) (rs : regset) 
  (pr : predset) (m : mem) 
  (rs' : regset) (pr' : predset) 
  (m' : mem) (cf0 : cf_instr),
SeqBB.step ge sp (Iexec (mki rs pr m))
  (x0 ++ RBexit x cf :: x1)
  (Iterm (mki rs' pr' m') cf0) ->
exists
  (p : option Gible.pred_op) 
(b1 b2 : list instr),
  truthy pr' p /\
  x0 ++ RBexit x cf :: x1 =
  b1 ++ RBexit p cf0 :: b2 /\
  step_list2 (step_instr ge) sp
    (Iexec (mki rs pr m)) b1
    (Iexec (mki rs' pr' m'))
ge: Genv.t A B
sp: val
rs: regset
pr: predset
m: mem
rs': regset
pr': predset
m': mem
is_rs: regset
is_ps: predset
is_mem: mem
H5: step_instr ge sp (Iexec (mki rs pr m)) a
  (Iexec (mki is_rs is_ps is_mem))
H7: step_list (step_instr ge) sp
  (Iexec (mki is_rs is_ps is_mem))
  (x0 ++ RBexit x cf :: x1)
  (Iterm (mki rs' pr' m') cf)
H: truthy pr' x
H2: step_list2 (step_instr ge) sp
  (Iexec (mki is_rs is_ps is_mem)) x0
  (Iexec (mki rs' pr' m'))
step_list2 (step_instr ge) sp (Iexec (mki rs pr m))
  (a :: x0) (Iexec (mki rs' pr' m'))
    econstructor; eauto.
  -A, B: Type
a: instr
bb: list instr
IHbb: forall (ge : Genv.t A B) 
  (sp : val) (rs : regset) 
  (pr : predset) (m : mem) 
  (rs' : regset) (pr' : predset) 
  (m' : mem) (cf : cf_instr),
SeqBB.step ge sp (Iexec (mki rs pr m)) bb
  (Iterm (mki rs' pr' m') cf) ->
exists
  (p : option Gible.pred_op) 
(b1 b2 : list instr),
  truthy pr' p /\
  bb = b1 ++ RBexit p cf :: b2 /\
  step_list2 (step_instr ge) sp
    (Iexec (mki rs pr m)) b1
    (Iexec (mki rs' pr' m'))
ge: Genv.t A B
sp: val
rs: regset
pr: predset
m: mem
rs': regset
pr': predset
m': mem
cf: cf_instr
H3: step_instr ge sp (Iexec (mki rs pr m)) a
  (Iterm (mki rs' pr' m') cf)
exists
  (p : option Gible.pred_op) (b1 b2 : list instr),
  truthy pr' p /\
  a :: bb = b1 ++ RBexit p cf :: b2 /\
  step_list2 (step_instr ge) sp (Iexec (mki rs pr m))
    b1 (Iexec (mki rs' pr' m'))  inv H3.A, B: Type
bb: list instr
IHbb: forall (ge : Genv.t A B) 
  (sp : val) (rs : regset) 
  (pr : predset) (m : mem) 
  (rs' : regset) (pr' : predset) 
  (m' : mem) (cf : cf_instr),
SeqBB.step ge sp (Iexec (mki rs pr m)) bb
  (Iterm (mki rs' pr' m') cf) ->
exists
  (p : option Gible.pred_op) 
(b1 b2 : list instr),
  truthy pr' p /\
  bb = b1 ++ RBexit p cf :: b2 /\
  step_list2 (step_instr ge) sp
    (Iexec (mki rs pr m)) b1
    (Iexec (mki rs' pr' m'))
ge: Genv.t A B
sp: val
rs': regset
pr': predset
m': mem
cf: cf_instr
p: option Gible.pred_op
H4: truthy (is_ps (mki rs' pr' m')) p
exists
  (p0 : option Gible.pred_op) (b1 b2 : list instr),
  truthy pr' p0 /\
  RBexit p cf :: bb = b1 ++ RBexit p0 cf :: b2 /\
  step_list2 (step_instr ge) sp
    (Iexec (mki rs' pr' m')) b1
    (Iexec (mki rs' pr' m'))
     exists p.A, B: Type
bb: list instr
IHbb: forall (ge : Genv.t A B) 
  (sp : val) (rs : regset) 
  (pr : predset) (m : mem) 
  (rs' : regset) (pr' : predset) 
  (m' : mem) (cf : cf_instr),
SeqBB.step ge sp (Iexec (mki rs pr m)) bb
  (Iterm (mki rs' pr' m') cf) ->
exists
  (p : option Gible.pred_op) 
(b1 b2 : list instr),
  truthy pr' p /\
  bb = b1 ++ RBexit p cf :: b2 /\
  step_list2 (step_instr ge) sp
    (Iexec (mki rs pr m)) b1
    (Iexec (mki rs' pr' m'))
ge: Genv.t A B
sp: val
rs': regset
pr': predset
m': mem
cf: cf_instr
p: option Gible.pred_op
H4: truthy (is_ps (mki rs' pr' m')) p
exists b1 b2 : list instr,
  truthy pr' p /\
  RBexit p cf :: bb = b1 ++ RBexit p cf :: b2 /\
  step_list2 (step_instr ge) sp
    (Iexec (mki rs' pr' m')) b1
    (Iexec (mki rs' pr' m')) exists (@nil instr).A, B: Type
bb: list instr
IHbb: forall (ge : Genv.t A B) 
  (sp : val) (rs : regset) 
  (pr : predset) (m : mem) 
  (rs' : regset) (pr' : predset) 
  (m' : mem) (cf : cf_instr),
SeqBB.step ge sp (Iexec (mki rs pr m)) bb
  (Iterm (mki rs' pr' m') cf) ->
exists
  (p : option Gible.pred_op) 
(b1 b2 : list instr),
  truthy pr' p /\
  bb = b1 ++ RBexit p cf :: b2 /\
  step_list2 (step_instr ge) sp
    (Iexec (mki rs pr m)) b1
    (Iexec (mki rs' pr' m'))
ge: Genv.t A B
sp: val
rs': regset
pr': predset
m': mem
cf: cf_instr
p: option Gible.pred_op
H4: truthy (is_ps (mki rs' pr' m')) p
exists b2 : list instr,
  truthy pr' p /\
  RBexit p cf :: bb = nil ++ RBexit p cf :: b2 /\
  step_list2 (step_instr ge) sp
    (Iexec (mki rs' pr' m')) nil
    (Iexec (mki rs' pr' m')) exists bb.A, B: Type
bb: list instr
IHbb: forall (ge : Genv.t A B) 
  (sp : val) (rs : regset) 
  (pr : predset) (m : mem) 
  (rs' : regset) (pr' : predset) 
  (m' : mem) (cf : cf_instr),
SeqBB.step ge sp (Iexec (mki rs pr m)) bb
  (Iterm (mki rs' pr' m') cf) ->
exists
  (p : option Gible.pred_op) 
(b1 b2 : list instr),
  truthy pr' p /\
  bb = b1 ++ RBexit p cf :: b2 /\
  step_list2 (step_instr ge) sp
    (Iexec (mki rs pr m)) b1
    (Iexec (mki rs' pr' m'))
ge: Genv.t A B
sp: val
rs': regset
pr': predset
m': mem
cf: cf_instr
p: option Gible.pred_op
H4: truthy (is_ps (mki rs' pr' m')) p
truthy pr' p /\
RBexit p cf :: bb = nil ++ RBexit p cf :: bb /\
step_list2 (step_instr ge) sp (Iexec (mki rs' pr' m'))
  nil (Iexec (mki rs' pr' m')) crush.A, B: Type
bb: list instr
IHbb: forall (ge : Genv.t A B) 
  (sp : val) (rs : regset) 
  (pr : predset) (m : mem) 
  (rs' : regset) (pr' : predset) 
  (m' : mem) (cf : cf_instr),
SeqBB.step ge sp (Iexec (mki rs pr m)) bb
  (Iterm (mki rs' pr' m') cf) ->
exists
  (p : option Gible.pred_op) 
(b1 b2 : list instr),
  truthy pr' p /\
  bb = b1 ++ RBexit p cf :: b2 /\
  step_list2 (step_instr ge) sp
    (Iexec (mki rs pr m)) b1
    (Iexec (mki rs' pr' m'))
ge: Genv.t A B
sp: val
rs': regset
pr': predset
m': mem
cf: cf_instr
p: option Gible.pred_op
H4: truthy pr' p
step_list2 (step_instr ge) sp (Iexec (mki rs' pr' m'))
  nil (Iexec (mki rs' pr' m'))
     constructor.
Qed.

#[local] Open Scope positive.

Lemma max_pred_instr_lt :
  forall y a,
    y <= max_pred_instr y a.forall (y : positive) (a : instr),
y <= max_pred_instr y a
Proof.forall (y : positive) (a : instr),
y <= max_pred_instr y a
  unfold max_pred_instr; intros.y: positive
a: instr
y <=
match a with
| RBsetpred (Some p') _ _ p =>
    Pos.max y (Pos.max p (max_predicate p'))
| RBsetpred None _ _ p => Pos.max y p
| RBop (Some p) _ _ _ | RBload (Some p) _ _ _ _ |
  RBstore (Some p) _ _ _ _ | RBexit (Some p) _ =>
    Pos.max y (max_predicate p)
| _ => y
end
  destruct a; try destruct o; lia.
Qed.

Lemma max_pred_instr_fold_lt :
  forall b y,
    y <= fold_left max_pred_instr b y.forall (b : list instr) (y : positive),
y <= fold_left max_pred_instr b y
Proof.forall (b : list instr) (y : positive),
y <= fold_left max_pred_instr b y
  induction b; crush.a: instr
b: list instr
IHb: forall y : positive, y <= fold_left max_pred_instr b y
y: positive
y <= fold_left max_pred_instr b (max_pred_instr y a)
  transitivity (max_pred_instr y a); auto.a: instr
b: list instr
IHb: forall y : positive, y <= fold_left max_pred_instr b y
y: positive
y <= max_pred_instr y a
  apply max_pred_instr_lt.
Qed.

Lemma max_pred_block_lt :
  forall y a b,
    y <= max_pred_block y a b.forall (y : positive) (a : node) (b : SeqBB.t),
y <= max_pred_block y a b
Proof.forall (y : positive) (a : node) (b : SeqBB.t),
y <= max_pred_block y a b
  unfold max_pred_block, SeqBB.foldl; intros.y: positive
a: node
b: SeqBB.t
y <= fold_left max_pred_instr b y
  apply max_pred_instr_fold_lt.
Qed.

Lemma max_fold_left_initial :
  forall l y,
    y <= fold_left (fun (a : positive) (p0 : positive * SeqBB.t) => max_pred_block a (fst p0) (snd p0)) l y.forall (l : list (positive * SeqBB.t)) (y : positive),
y <=
fold_left
  (fun (a : positive) (p0 : positive * SeqBB.t) =>
   max_pred_block a (fst p0) (snd p0)) l y
Proof.forall (l : list (positive * SeqBB.t)) (y : positive),
y <=
fold_left
  (fun (a : positive) (p0 : positive * SeqBB.t) =>
   max_pred_block a (fst p0) (snd p0)) l y
  induction l; crush.a: (positive * SeqBB.t)%type
l: list (positive * SeqBB.t)
IHl: forall y : positive,
y <=
fold_left
(fun (a : positive) (p0 : positive * SeqBB.t) =>
max_pred_block a (fst p0) (snd p0)) l y
y: positive
y <=
fold_left
  (fun (a : positive) (p0 : positive * SeqBB.t) =>
   max_pred_block a (fst p0) (snd p0)) l
  (max_pred_block y (fst a) (snd a))
  transitivity (max_pred_block y (fst a) (snd a)); eauto.a: (positive * SeqBB.t)%type
l: list (positive * SeqBB.t)
IHl: forall y : positive,
y <=
fold_left
(fun (a : positive) (p0 : positive * SeqBB.t) =>
max_pred_block a (fst p0) (snd p0)) l y
y: positive
y <= max_pred_block y (fst a) (snd a)
  apply max_pred_block_lt.
Qed.

Lemma max_pred_in_max :
  forall y p i,
    In p (pred_uses i) ->
    p <= max_pred_instr y i.forall (y : positive) (p : predicate) (i : instr),
In p (pred_uses i) -> p <= max_pred_instr y i
Proof.forall (y : positive) (p : predicate) (i : instr),
In p (pred_uses i) -> p <= max_pred_instr y i
  intros.y: positive
p: predicate
i: instr
H: In p (pred_uses i)
p <= max_pred_instr y i unfold max_pred_instr.y: positive
p: predicate
i: instr
H: In p (pred_uses i)
p <=
match i with
| RBsetpred (Some p') _ _ p =>
    Pos.max y (Pos.max p (max_predicate p'))
| RBsetpred None _ _ p => Pos.max y p
| RBop (Some p) _ _ _ | RBload (Some p) _ _ _ _ |
  RBstore (Some p) _ _ _ _ | RBexit (Some p) _ =>
    Pos.max y (max_predicate p)
| _ => y
end destruct i; try destruct o; cbn in *; try easy.y: positive
p: predicate
p0: Gible.pred_op
o0: operation
l: list reg
r: reg
H: In p (predicate_use p0)
p <= Pos.max y (max_predicate p0)
y: positive
p: predicate
p0: Gible.pred_op
m: memory_chunk
a: addressing
l: list reg
r: reg
H: In p (predicate_use p0)
p <= Pos.max y (max_predicate p0)
y: positive
p: predicate
p0: Gible.pred_op
m: memory_chunk
a: addressing
l: list reg
r: reg
H: In p (predicate_use p0)
p <= Pos.max y (max_predicate p0)
y: positive
p: predicate
p1: Gible.pred_op
c: condition
l: list reg
p0: Gible.predicate
H: p0 = p \/ In p (predicate_use p1)
p <= Pos.max y (Pos.max p0 (max_predicate p1))
y: positive
p: predicate
c: condition
l: list reg
p0: Gible.predicate
H: p0 = p \/ False
p <= Pos.max y p0
y: positive
p: predicate
p0: Gible.pred_op
c: cf_instr
H: In p (predicate_use p0)
p <= Pos.max y (max_predicate p0)
  -y: positive
p: predicate
p0: Gible.pred_op
o0: operation
l: list reg
r: reg
H: In p (predicate_use p0)
p <= Pos.max y (max_predicate p0) eapply predicate_lt in H; lia.
  -y: positive
p: predicate
p0: Gible.pred_op
m: memory_chunk
a: addressing
l: list reg
r: reg
H: In p (predicate_use p0)
p <= Pos.max y (max_predicate p0) eapply predicate_lt in H; lia.
  -y: positive
p: predicate
p0: Gible.pred_op
m: memory_chunk
a: addressing
l: list reg
r: reg
H: In p (predicate_use p0)
p <= Pos.max y (max_predicate p0) eapply predicate_lt in H; lia.
  -y: positive
p: predicate
p1: Gible.pred_op
c: condition
l: list reg
p0: Gible.predicate
H: p0 = p \/ In p (predicate_use p1)
p <= Pos.max y (Pos.max p0 (max_predicate p1)) inv H; try lia.y: positive
p: predicate
p1: Gible.pred_op
c: condition
l: list reg
p0: Gible.predicate
H0: In p (predicate_use p1)
p <= Pos.max y (Pos.max p0 (max_predicate p1)) eapply predicate_lt in H0; lia.
  -y: positive
p: predicate
c: condition
l: list reg
p0: Gible.predicate
H: p0 = p \/ False
p <= Pos.max y p0 inv H; try lia.
  -y: positive
p: predicate
p0: Gible.pred_op
c: cf_instr
H: In p (predicate_use p0)
p <= Pos.max y (max_predicate p0) eapply predicate_lt in H; lia.
Qed.

Lemma fold_left_in_max :
  forall bb p y i,
    In i bb ->
    In p (pred_uses i) ->
    p <= fold_left max_pred_instr bb y.forall (bb : list instr) (p : predicate)
  (y : positive) (i : instr),
In i bb ->
In p (pred_uses i) ->
p <= fold_left max_pred_instr bb y
Proof.forall (bb : list instr) (p : predicate)
  (y : positive) (i : instr),
In i bb ->
In p (pred_uses i) ->
p <= fold_left max_pred_instr bb y
  induction bb; crush.a: instr
bb: list instr
IHbb: forall (p : predicate) (y : positive)
  (i : instr),
In i bb ->
In p (pred_uses i) ->
p <= fold_left max_pred_instr bb y
p: predicate
y: positive
i: instr
H: a = i \/ In i bb
H0: In p (pred_uses i)
p <= fold_left max_pred_instr bb (max_pred_instr y a) inv H; eauto.bb: list instr
IHbb: forall (p : predicate) (y : positive)
  (i : instr),
In i bb ->
In p (pred_uses i) ->
p <= fold_left max_pred_instr bb y
p: predicate
y: positive
i: instr
H0: In p (pred_uses i)
p <= fold_left max_pred_instr bb (max_pred_instr y i)
  transitivity (max_pred_instr y i); [|eapply max_pred_instr_fold_lt].bb: list instr
IHbb: forall (p : predicate) (y : positive)
  (i : instr),
In i bb ->
In p (pred_uses i) ->
p <= fold_left max_pred_instr bb y
p: predicate
y: positive
i: instr
H0: In p (pred_uses i)
p <= max_pred_instr y i
  apply max_pred_in_max; auto.
Qed.

Lemma max_pred_function_use' :
  forall l pc bb p i y,
    In (pc, bb) l ->
    In i bb ->
    In p (pred_uses i) ->
    p <= fold_left (fun (a : positive) (p0 : positive * SeqBB.t) => max_pred_block a (fst p0) (snd p0)) l y.forall (l : list (positive * list instr))
  (pc : positive) (bb : list instr) (p : predicate)
  (i : instr) (y : positive),
In (pc, bb) l ->
In i bb ->
In p (pred_uses i) ->
p <=
fold_left
  (fun (a : positive) (p0 : positive * SeqBB.t) =>
   max_pred_block a (fst p0) (snd p0)) l y
Proof.forall (l : list (positive * list instr))
  (pc : positive) (bb : list instr) (p : predicate)
  (i : instr) (y : positive),
In (pc, bb) l ->
In i bb ->
In p (pred_uses i) ->
p <=
fold_left
  (fun (a : positive) (p0 : positive * SeqBB.t) =>
   max_pred_block a (fst p0) (snd p0)) l y
  induction l; crush.a: (positive * list instr)%type
l: list (positive * list instr)
IHl: forall (pc : positive) (bb : list instr) (p : predicate) (i : instr)
(y : positive),
In (pc, bb) l ->
In i bb ->
In p (pred_uses i) ->
p <=
fold_left
(fun (a : positive) (p0 : positive * SeqBB.t) =>
max_pred_block a (fst p0) (snd p0)) l y
pc: positive
bb: list instr
p: predicate
i: instr
y: positive
H: a = (pc, bb) \/ In (pc, bb) l
H0: In i bb
H1: In p (pred_uses i)
p <=
fold_left
  (fun (a : positive) (p0 : positive * SeqBB.t) =>
   max_pred_block a (fst p0) (snd p0)) l
  (max_pred_block y (fst a) (snd a)) inv H; eauto.l: list (positive * list instr)
IHl: forall (pc : positive) (bb : list instr) (p : predicate) (i : instr)
(y : positive),
In (pc, bb) l ->
In i bb ->
In p (pred_uses i) ->
p <=
fold_left
(fun (a : positive) (p0 : positive * SeqBB.t) =>
max_pred_block a (fst p0) (snd p0)) l y
pc: positive
bb: list instr
p: predicate
i: instr
y: positive
H0: In i bb
H1: In p (pred_uses i)
p <=
fold_left
  (fun (a : positive) (p0 : positive * SeqBB.t) =>
   max_pred_block a (fst p0) (snd p0)) l
  (max_pred_block y (fst (pc, bb)) (snd (pc, bb)))
  transitivity (max_pred_block y (fst (pc, bb)) (snd (pc, bb))); eauto;
    [|eapply max_fold_left_initial].l: list (positive * list instr)
IHl: forall (pc : positive) (bb : list instr) (p : predicate) (i : instr)
(y : positive),
In (pc, bb) l ->
In i bb ->
In p (pred_uses i) ->
p <=
fold_left
(fun (a : positive) (p0 : positive * SeqBB.t) =>
max_pred_block a (fst p0) (snd p0)) l y
pc: positive
bb: list instr
p: predicate
i: instr
y: positive
H0: In i bb
H1: In p (pred_uses i)
p <= max_pred_block y (fst (pc, bb)) (snd (pc, bb))
  cbn.l: list (positive * list instr)
IHl: forall (pc : positive) (bb : list instr) (p : predicate) (i : instr)
(y : positive),
In (pc, bb) l ->
In i bb ->
In p (pred_uses i) ->
p <=
fold_left
(fun (a : positive) (p0 : positive * SeqBB.t) =>
max_pred_block a (fst p0) (snd p0)) l y
pc: positive
bb: list instr
p: predicate
i: instr
y: positive
H0: In i bb
H1: In p (pred_uses i)
p <= SeqBB.foldl max_pred_instr bb y unfold SeqBB.foldl.l: list (positive * list instr)
IHl: forall (pc : positive) (bb : list instr) (p : predicate) (i : instr)
(y : positive),
In (pc, bb) l ->
In i bb ->
In p (pred_uses i) ->
p <=
fold_left
(fun (a : positive) (p0 : positive * SeqBB.t) =>
max_pred_block a (fst p0) (snd p0)) l y
pc: positive
bb: list instr
p: predicate
i: instr
y: positive
H0: In i bb
H1: In p (pred_uses i)
p <= fold_left max_pred_instr bb y
  eapply fold_left_in_max; eauto.
Qed.

Lemma max_pred_function_use :
  forall f pc bb i p,
    f.(fn_code) ! pc = Some bb ->
    In i bb ->
    In p (pred_uses i) ->
    p <= max_pred_function f.forall (f : function) (pc : positive) (bb : SeqBB.t)
  (i : instr) (p : predicate),
(fn_code f) ! pc = Some bb ->
In i bb ->
In p (pred_uses i) -> p <= max_pred_function f
Proof.forall (f : function) (pc : positive) (bb : SeqBB.t)
  (i : instr) (p : predicate),
(fn_code f) ! pc = Some bb ->
In i bb ->
In p (pred_uses i) -> p <= max_pred_function f
  unfold max_pred_function; intros.f: function
pc: positive
bb: SeqBB.t
i: instr
p: predicate
H: (fn_code f) ! pc = Some bb
H0: In i bb
H1: In p (pred_uses i)
p <= PTree.fold max_pred_block (fn_code f) 1
  rewrite PTree.fold_spec.f: function
pc: positive
bb: SeqBB.t
i: instr
p: predicate
H: (fn_code f) ! pc = Some bb
H0: In i bb
H1: In p (pred_uses i)
p <=
fold_left
  (fun (a : positive) (p : positive * SeqBB.t) =>
   max_pred_block a (fst p) (snd p))
  (PTree.elements (fn_code f)) 1
  eapply max_pred_function_use'; eauto.f: function
pc: positive
bb: SeqBB.t
i: instr
p: predicate
H: (fn_code f) ! pc = Some bb
H0: In i bb
H1: In p (pred_uses i)
In (?pc, bb) (PTree.elements (fn_code f))
  eapply PTree.elements_correct; eauto.
Qed.

Ltac truthy_falsy :=
  match goal with
  | H: instr_falsy ?ps (RBop ?p _ _ _), H2: truthy ?ps ?p |- _ =>
      solve [inv H2; inv H; crush]
  | H: instr_falsy ?ps (RBload ?p _ _ _ _), H2: truthy ?ps ?p |- _ =>
      solve [inv H2; inv H; crush]
  | H: instr_falsy ?ps (RBstore ?p _ _ _ _), H2: truthy ?ps ?p |- _ =>
      solve [inv H2; inv H; crush]
  | H: instr_falsy ?ps (RBexit ?p _), H2: truthy ?ps ?p |- _ =>
      solve [inv H2; inv H; crush]
  | H: instr_falsy ?ps (RBsetpred ?p _ _ _), H2: truthy ?ps ?p |- _ =>
      solve [inv H2; inv H; crush]
  end.

Lemma exec_determ :
  forall A B ge sp s1 a s2 s2',
    @step_instr A B ge sp s1 a s2 ->
    step_instr ge sp s1 a s2' ->
    s2 = s2'.forall (A B : Type) (ge : Genv.t A B) (sp : val)
  (s1 : istate) (a : instr) (s2 s2' : istate),
step_instr ge sp s1 a s2 ->
step_instr ge sp s1 a s2' -> s2 = s2'
Proof.forall (A B : Type) (ge : Genv.t A B) (sp : val)
  (s1 : istate) (a : instr) (s2 s2' : istate),
step_instr ge sp s1 a s2 ->
step_instr ge sp s1 a s2' -> s2 = s2'
  inversion 1; subst; crush.A, B: Type
ge: Genv.t A B
sp: val
s2': istate
ist: instr_state
H: step_instr ge sp (Iexec ist) RBnop (Iexec ist)
H0: step_instr ge sp (Iexec ist) RBnop s2'
Iexec ist = s2'
A, B: Type
ge: Genv.t A B
sp: val
s2': istate
rs: Regmap.t val
m: mem
pr: predset
op: operation
res: reg
args: list positive
p: option Gible.pred_op
v: val
H: step_instr ge sp (Iexec (mki rs pr m))
  (RBop p op args res)
  (Iexec (mki rs # res <- v pr m))
H0: eval_operation ge sp op rs ## args m = Some v
H1: truthy pr p
H2: step_instr ge sp (Iexec (mki rs pr m))
  (RBop p op args res) s2'
Iexec (mki rs # res <- v pr m) = s2'
A, B: Type
ge: Genv.t A B
sp: val
s2': istate
rs: Regmap.t val
m: mem
pr: predset
addr: addressing
args: list positive
chunk: memory_chunk
dst: reg
p: option Gible.pred_op
v: val
H: step_instr ge sp (Iexec (mki rs pr m))
  (RBload p chunk addr args dst)
  (Iexec (mki rs # dst <- v pr m))
a0: val
H0: eval_addressing ge sp addr rs ## args = Some a0
H1: Mem.loadv chunk m a0 = Some v
H2: truthy pr p
H3: step_instr ge sp (Iexec (mki rs pr m))
  (RBload p chunk addr args dst) s2'
Iexec (mki rs # dst <- v pr m) = s2'
A, B: Type
ge: Genv.t A B
sp: val
s2': istate
rs: Regmap.t val
m: mem
pr: predset
addr: addressing
args: list positive
chunk: memory_chunk
src: positive
p: option Gible.pred_op
m': mem
H: step_instr ge sp (Iexec (mki rs pr m))
  (RBstore p chunk addr args src)
  (Iexec (mki rs pr m'))
a0: val
H0: eval_addressing ge sp addr rs ## args = Some a0
H1: Mem.storev chunk m a0 rs !! src = Some m'
H2: truthy pr p
H3: step_instr ge sp (Iexec (mki rs pr m))
  (RBstore p chunk addr args src) s2'
Iexec (mki rs pr m') = s2'
A, B: Type
ge: Genv.t A B
sp: val
s2': istate
rs: Regmap.t val
pr: predset
m: mem
p: Gible.predicate
c: condition
args: list positive
p': option Gible.pred_op
b: bool
H: step_instr ge sp (Iexec (mki rs pr m))
  (RBsetpred p' c args p)
  (Iexec (mki rs pr # p <- b m))
H0: eval_condition c rs ## args m = Some b
H1: truthy pr p'
H2: step_instr ge sp (Iexec (mki rs pr m))
  (RBsetpred p' c args p) s2'
Iexec (mki rs pr # p <- b m) = s2'
A, B: Type
ge: Genv.t A B
sp: val
s2': istate
i: instr_state
p: option Gible.pred_op
c: cf_instr
H: step_instr ge sp (Iexec i) 
  (RBexit p c) (Iterm i c)
H0: truthy (is_ps i) p
H1: step_instr ge sp (Iexec i) (RBexit p c) s2'
Iterm i c = s2'
A, B: Type
ge: Genv.t A B
sp: val
a: instr
s2': istate
st: instr_state
H: step_instr ge sp (Iexec st) a (Iexec st)
H0: instr_falsy (is_ps st) a
H1: step_instr ge sp (Iexec st) a s2'
Iexec st = s2'
  -A, B: Type
ge: Genv.t A B
sp: val
s2': istate
ist: instr_state
H: step_instr ge sp (Iexec ist) RBnop (Iexec ist)
H0: step_instr ge sp (Iexec ist) RBnop s2'
Iexec ist = s2' inv H0; auto.
  -A, B: Type
ge: Genv.t A B
sp: val
s2': istate
rs: Regmap.t val
m: mem
pr: predset
op: operation
res: reg
args: list positive
p: option Gible.pred_op
v: val
H: step_instr ge sp (Iexec (mki rs pr m))
  (RBop p op args res)
  (Iexec (mki rs # res <- v pr m))
H0: eval_operation ge sp op rs ## args m = Some v
H1: truthy pr p
H2: step_instr ge sp (Iexec (mki rs pr m))
  (RBop p op args res) s2'
Iexec (mki rs # res <- v pr m) = s2' inv H2; crush; truthy_falsy.
  -A, B: Type
ge: Genv.t A B
sp: val
s2': istate
rs: Regmap.t val
m: mem
pr: predset
addr: addressing
args: list positive
chunk: memory_chunk
dst: reg
p: option Gible.pred_op
v: val
H: step_instr ge sp (Iexec (mki rs pr m))
  (RBload p chunk addr args dst)
  (Iexec (mki rs # dst <- v pr m))
a0: val
H0: eval_addressing ge sp addr rs ## args = Some a0
H1: Mem.loadv chunk m a0 = Some v
H2: truthy pr p
H3: step_instr ge sp (Iexec (mki rs pr m))
  (RBload p chunk addr args dst) s2'
Iexec (mki rs # dst <- v pr m) = s2' inv H3; crush.A, B: Type
ge: Genv.t A B
sp: val
rs: Regmap.t val
m: mem
pr: predset
addr: addressing
args: list positive
chunk: memory_chunk
dst: reg
p: option Gible.pred_op
v: val
H: step_instr ge sp (Iexec (mki rs pr m))
  (RBload p chunk addr args dst)
  (Iexec (mki rs # dst <- v pr m))
a0: val
H0: eval_addressing ge sp addr rs ## args = Some a0
H1: Mem.loadv chunk m a0 = Some v
H2: truthy pr p
H6: instr_falsy pr (RBload p chunk addr args dst)
Iexec (mki rs # dst <- v pr m) = Iexec (mki rs pr m) truthy_falsy.
  -A, B: Type
ge: Genv.t A B
sp: val
s2': istate
rs: Regmap.t val
m: mem
pr: predset
addr: addressing
args: list positive
chunk: memory_chunk
src: positive
p: option Gible.pred_op
m': mem
H: step_instr ge sp (Iexec (mki rs pr m))
  (RBstore p chunk addr args src)
  (Iexec (mki rs pr m'))
a0: val
H0: eval_addressing ge sp addr rs ## args = Some a0
H1: Mem.storev chunk m a0 rs !! src = Some m'
H2: truthy pr p
H3: step_instr ge sp (Iexec (mki rs pr m))
  (RBstore p chunk addr args src) s2'
Iexec (mki rs pr m') = s2' inv H3; crush.A, B: Type
ge: Genv.t A B
sp: val
rs: Regmap.t val
m: mem
pr: predset
addr: addressing
args: list positive
chunk: memory_chunk
src: positive
p: option Gible.pred_op
m': mem
H: step_instr ge sp (Iexec (mki rs pr m))
  (RBstore p chunk addr args src)
  (Iexec (mki rs pr m'))
a0: val
H0: eval_addressing ge sp addr rs ## args = Some a0
H1: Mem.storev chunk m a0 rs !! src = Some m'
H2: truthy pr p
H6: instr_falsy pr (RBstore p chunk addr args src)
Iexec (mki rs pr m') = Iexec (mki rs pr m) truthy_falsy.
  -A, B: Type
ge: Genv.t A B
sp: val
s2': istate
rs: Regmap.t val
pr: predset
m: mem
p: Gible.predicate
c: condition
args: list positive
p': option Gible.pred_op
b: bool
H: step_instr ge sp (Iexec (mki rs pr m))
  (RBsetpred p' c args p)
  (Iexec (mki rs pr # p <- b m))
H0: eval_condition c rs ## args m = Some b
H1: truthy pr p'
H2: step_instr ge sp (Iexec (mki rs pr m))
  (RBsetpred p' c args p) s2'
Iexec (mki rs pr # p <- b m) = s2' inv H2; crush.A, B: Type
ge: Genv.t A B
sp: val
rs: Regmap.t val
pr: predset
m: mem
p: Gible.predicate
c: condition
args: list positive
p': option Gible.pred_op
b: bool
H: step_instr ge sp (Iexec (mki rs pr m))
  (RBsetpred p' c args p)
  (Iexec (mki rs pr # p <- b m))
H0: eval_condition c rs ## args m = Some b
H1: truthy pr p'
H5: instr_falsy pr (RBsetpred p' c args p)
Iexec (mki rs pr # p <- b m) = Iexec (mki rs pr m) truthy_falsy.
  -A, B: Type
ge: Genv.t A B
sp: val
s2': istate
i: instr_state
p: option Gible.pred_op
c: cf_instr
H: step_instr ge sp (Iexec i) 
  (RBexit p c) (Iterm i c)
H0: truthy (is_ps i) p
H1: step_instr ge sp (Iexec i) (RBexit p c) s2'
Iterm i c = s2' inv H1; crush.A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
p: option Gible.pred_op
c: cf_instr
H: step_instr ge sp (Iexec i) 
  (RBexit p c) (Iterm i c)
H0: truthy (is_ps i) p
H4: instr_falsy (is_ps i) (RBexit p c)
Iterm i c = Iexec i truthy_falsy.
  -A, B: Type
ge: Genv.t A B
sp: val
a: instr
s2': istate
st: instr_state
H: step_instr ge sp (Iexec st) a (Iexec st)
H0: instr_falsy (is_ps st) a
H1: step_instr ge sp (Iexec st) a s2'
Iexec st = s2' destruct st; simplify.A, B: Type
ge: Genv.t A B
sp: val
a: instr
s2': istate
is_rs: regset
is_ps: predset
is_mem: mem
H: step_instr ge sp (Iexec (mki is_rs is_ps is_mem))
  a (Iexec (mki is_rs is_ps is_mem))
H0: instr_falsy is_ps a
H1: step_instr ge sp (Iexec (mki is_rs is_ps is_mem))
  a s2'
Iexec (mki is_rs is_ps is_mem) = s2' inv H1; crush; truthy_falsy.
Qed.

Lemma append3 :
  forall A B l0 l1 sp ge s1 s2 s3,
    step_list2 (step_instr ge) sp s1 l0 (Iexec s2) ->
    @SeqBB.step A B ge sp s1 (l0 ++ l1) s3 ->
    @SeqBB.step A B ge sp (Iexec s2) l1 s3.forall (A B : Type) (l0 l1 : list instr) (sp : val)
  (ge : Genv.t A B) (s1 : istate) (s2 : instr_state)
  (s3 : istate),
step_list2 (step_instr ge) sp s1 l0 (Iexec s2) ->
SeqBB.step ge sp s1 (l0 ++ l1) s3 ->
SeqBB.step ge sp (Iexec s2) l1 s3
Proof.forall (A B : Type) (l0 l1 : list instr) (sp : val)
  (ge : Genv.t A B) (s1 : istate) (s2 : instr_state)
  (s3 : istate),
step_list2 (step_instr ge) sp s1 l0 (Iexec s2) ->
SeqBB.step ge sp s1 (l0 ++ l1) s3 ->
SeqBB.step ge sp (Iexec s2) l1 s3
  induction l0; crush.A, B: Type
l1: list instr
sp: val
ge: Genv.t A B
s1: istate
s2: instr_state
s3: istate
H: step_list2 (step_instr ge) sp s1 nil (Iexec s2)
H0: SeqBB.step ge sp s1 l1 s3
SeqBB.step ge sp (Iexec s2) l1 s3
A, B: Type
a: instr
l0: list instr
IHl0: forall (l1 : list instr) 
  (sp : val) (ge : Genv.t A B) 
  (s1 : istate) (s2 : instr_state)
  (s3 : istate),
step_list2 (step_instr ge) sp s1 l0 (Iexec s2) ->
SeqBB.step ge sp s1 (l0 ++ l1) s3 ->
SeqBB.step ge sp (Iexec s2) l1 s3
l1: list instr
sp: val
ge: Genv.t A B
s1: istate
s2: instr_state
s3: istate
H: step_list2 (step_instr ge) sp s1 
  (a :: l0) (Iexec s2)
H0: SeqBB.step ge sp s1 (a :: l0 ++ l1) s3
SeqBB.step ge sp (Iexec s2) l1 s3 inv H.A, B: Type
l1: list instr
sp: val
ge: Genv.t A B
s2: instr_state
s3: istate
H0: SeqBB.step ge sp (Iexec s2) l1 s3
SeqBB.step ge sp (Iexec s2) l1 s3
A, B: Type
a: instr
l0: list instr
IHl0: forall (l1 : list instr) 
  (sp : val) (ge : Genv.t A B) 
  (s1 : istate) (s2 : instr_state)
  (s3 : istate),
step_list2 (step_instr ge) sp s1 l0 (Iexec s2) ->
SeqBB.step ge sp s1 (l0 ++ l1) s3 ->
SeqBB.step ge sp (Iexec s2) l1 s3
l1: list instr
sp: val
ge: Genv.t A B
s1: istate
s2: instr_state
s3: istate
H: step_list2 (step_instr ge) sp s1 
  (a :: l0) (Iexec s2)
H0: SeqBB.step ge sp s1 (a :: l0 ++ l1) s3
SeqBB.step ge sp (Iexec s2) l1 s3 auto.A, B: Type
a: instr
l0: list instr
IHl0: forall (l1 : list instr) 
  (sp : val) (ge : Genv.t A B) 
  (s1 : istate) (s2 : instr_state)
  (s3 : istate),
step_list2 (step_instr ge) sp s1 l0 (Iexec s2) ->
SeqBB.step ge sp s1 (l0 ++ l1) s3 ->
SeqBB.step ge sp (Iexec s2) l1 s3
l1: list instr
sp: val
ge: Genv.t A B
s1: istate
s2: instr_state
s3: istate
H: step_list2 (step_instr ge) sp s1 
  (a :: l0) (Iexec s2)
H0: SeqBB.step ge sp s1 (a :: l0 ++ l1) s3
SeqBB.step ge sp (Iexec s2) l1 s3
  inv H0.A, B: Type
a: instr
l0: list instr
IHl0: forall (l1 : list instr) 
  (sp : val) (ge : Genv.t A B) 
  (s1 : istate) (s2 : instr_state)
  (s3 : istate),
step_list2 (step_instr ge) sp s1 l0 (Iexec s2) ->
SeqBB.step ge sp s1 (l0 ++ l1) s3 ->
SeqBB.step ge sp (Iexec s2) l1 s3
l1: list instr
sp: val
ge: Genv.t A B
s2, state0: instr_state
H: step_list2 (step_instr ge) sp 
  (Iexec state0) (a :: l0) 
  (Iexec s2)
state', state'': instr_state
cf: cf_instr
H5: step_instr ge sp (Iexec state0) a (Iexec state')
H7: step_list (step_instr ge) sp 
  (Iexec state') (l0 ++ l1) 
  (Iterm state'' cf)
SeqBB.step ge sp (Iexec s2) l1 (Iterm state'' cf)
A, B: Type
a: instr
l0: list instr
IHl0: forall (l1 : list instr) 
  (sp : val) (ge : Genv.t A B) 
  (s1 : istate) (s2 : instr_state)
  (s3 : istate),
step_list2 (step_instr ge) sp s1 l0 (Iexec s2) ->
SeqBB.step ge sp s1 (l0 ++ l1) s3 ->
SeqBB.step ge sp (Iexec s2) l1 s3
l1: list instr
sp: val
ge: Genv.t A B
s2, state0: instr_state
H: step_list2 (step_instr ge) sp 
  (Iexec state0) (a :: l0) 
  (Iexec s2)
state': instr_state
cf: cf_instr
H6: step_instr ge sp (Iexec state0) a
  (Iterm state' cf)
SeqBB.step ge sp (Iexec s2) l1 (Iterm state' cf) inv H.A, B: Type
a: instr
l0: list instr
IHl0: forall (l1 : list instr) 
  (sp : val) (ge : Genv.t A B) 
  (s1 : istate) (s2 : instr_state)
  (s3 : istate),
step_list2 (step_instr ge) sp s1 l0 (Iexec s2) ->
SeqBB.step ge sp s1 (l0 ++ l1) s3 ->
SeqBB.step ge sp (Iexec s2) l1 s3
l1: list instr
sp: val
ge: Genv.t A B
s2, state0, state', state'': instr_state
cf: cf_instr
H5: step_instr ge sp (Iexec state0) a (Iexec state')
H7: step_list (step_instr ge) sp 
  (Iexec state') (l0 ++ l1) 
  (Iterm state'' cf)
i1: istate
H4: step_instr ge sp (Iexec state0) a i1
H8: step_list2 (step_instr ge) sp i1 l0 (Iexec s2)
SeqBB.step ge sp (Iexec s2) l1 (Iterm state'' cf)
A, B: Type
a: instr
l0: list instr
IHl0: forall (l1 : list instr) 
  (sp : val) (ge : Genv.t A B) 
  (s1 : istate) (s2 : instr_state)
  (s3 : istate),
step_list2 (step_instr ge) sp s1 l0 (Iexec s2) ->
SeqBB.step ge sp s1 (l0 ++ l1) s3 ->
SeqBB.step ge sp (Iexec s2) l1 s3
l1: list instr
sp: val
ge: Genv.t A B
s2, state0: instr_state
H: step_list2 (step_instr ge) sp 
  (Iexec state0) (a :: l0) 
  (Iexec s2)
state': instr_state
cf: cf_instr
H6: step_instr ge sp (Iexec state0) a
  (Iterm state' cf)
SeqBB.step ge sp (Iexec s2) l1 (Iterm state' cf) assert (i1 = (Iexec state')) by (eapply exec_determ; eauto).A, B: Type
a: instr
l0: list instr
IHl0: forall (l1 : list instr) 
  (sp : val) (ge : Genv.t A B) 
  (s1 : istate) (s2 : instr_state)
  (s3 : istate),
step_list2 (step_instr ge) sp s1 l0 (Iexec s2) ->
SeqBB.step ge sp s1 (l0 ++ l1) s3 ->
SeqBB.step ge sp (Iexec s2) l1 s3
l1: list instr
sp: val
ge: Genv.t A B
s2, state0, state', state'': instr_state
cf: cf_instr
H5: step_instr ge sp (Iexec state0) a (Iexec state')
H7: step_list (step_instr ge) sp 
  (Iexec state') (l0 ++ l1) 
  (Iterm state'' cf)
i1: istate
H4: step_instr ge sp (Iexec state0) a i1
H8: step_list2 (step_instr ge) sp i1 l0 (Iexec s2)
H: i1 = Iexec state'
SeqBB.step ge sp (Iexec s2) l1 (Iterm state'' cf)
A, B: Type
a: instr
l0: list instr
IHl0: forall (l1 : list instr) 
  (sp : val) (ge : Genv.t A B) 
  (s1 : istate) (s2 : instr_state)
  (s3 : istate),
step_list2 (step_instr ge) sp s1 l0 (Iexec s2) ->
SeqBB.step ge sp s1 (l0 ++ l1) s3 ->
SeqBB.step ge sp (Iexec s2) l1 s3
l1: list instr
sp: val
ge: Genv.t A B
s2, state0: instr_state
H: step_list2 (step_instr ge) sp 
  (Iexec state0) (a :: l0) 
  (Iexec s2)
state': instr_state
cf: cf_instr
H6: step_instr ge sp (Iexec state0) a
  (Iterm state' cf)
SeqBB.step ge sp (Iexec s2) l1 (Iterm state' cf) subst.A, B: Type
a: instr
l0: list instr
IHl0: forall (l1 : list instr) 
  (sp : val) (ge : Genv.t A B) 
  (s1 : istate) (s2 : instr_state)
  (s3 : istate),
step_list2 (step_instr ge) sp s1 l0 (Iexec s2) ->
SeqBB.step ge sp s1 (l0 ++ l1) s3 ->
SeqBB.step ge sp (Iexec s2) l1 s3
l1: list instr
sp: val
ge: Genv.t A B
s2, state0, state', state'': instr_state
cf: cf_instr
H5: step_instr ge sp (Iexec state0) a (Iexec state')
H7: step_list (step_instr ge) sp 
  (Iexec state') (l0 ++ l1) 
  (Iterm state'' cf)
H8: step_list2 (step_instr ge) sp 
  (Iexec state') l0 (Iexec s2)
H4: step_instr ge sp (Iexec state0) a (Iexec state')
SeqBB.step ge sp (Iexec s2) l1 (Iterm state'' cf)
A, B: Type
a: instr
l0: list instr
IHl0: forall (l1 : list instr) 
  (sp : val) (ge : Genv.t A B) 
  (s1 : istate) (s2 : instr_state)
  (s3 : istate),
step_list2 (step_instr ge) sp s1 l0 (Iexec s2) ->
SeqBB.step ge sp s1 (l0 ++ l1) s3 ->
SeqBB.step ge sp (Iexec s2) l1 s3
l1: list instr
sp: val
ge: Genv.t A B
s2, state0: instr_state
H: step_list2 (step_instr ge) sp 
  (Iexec state0) (a :: l0) 
  (Iexec s2)
state': instr_state
cf: cf_instr
H6: step_instr ge sp (Iexec state0) a
  (Iterm state' cf)
SeqBB.step ge sp (Iexec s2) l1 (Iterm state' cf) eauto.A, B: Type
a: instr
l0: list instr
IHl0: forall (l1 : list instr) 
  (sp : val) (ge : Genv.t A B) 
  (s1 : istate) (s2 : instr_state)
  (s3 : istate),
step_list2 (step_instr ge) sp s1 l0 (Iexec s2) ->
SeqBB.step ge sp s1 (l0 ++ l1) s3 ->
SeqBB.step ge sp (Iexec s2) l1 s3
l1: list instr
sp: val
ge: Genv.t A B
s2, state0: instr_state
H: step_list2 (step_instr ge) sp 
  (Iexec state0) (a :: l0) 
  (Iexec s2)
state': instr_state
cf: cf_instr
H6: step_instr ge sp (Iexec state0) a
  (Iterm state' cf)
SeqBB.step ge sp (Iexec s2) l1 (Iterm state' cf)
  inv H.A, B: Type
a: instr
l0: list instr
IHl0: forall (l1 : list instr) 
  (sp : val) (ge : Genv.t A B) 
  (s1 : istate) (s2 : instr_state)
  (s3 : istate),
step_list2 (step_instr ge) sp s1 l0 (Iexec s2) ->
SeqBB.step ge sp s1 (l0 ++ l1) s3 ->
SeqBB.step ge sp (Iexec s2) l1 s3
l1: list instr
sp: val
ge: Genv.t A B
s2, state0, state': instr_state
cf: cf_instr
H6: step_instr ge sp (Iexec state0) a
  (Iterm state' cf)
i1: istate
H4: step_instr ge sp (Iexec state0) a i1
H7: step_list2 (step_instr ge) sp i1 l0 (Iexec s2)
SeqBB.step ge sp (Iexec s2) l1 (Iterm state' cf) assert (i1 = (Iterm state' cf)) by (eapply exec_determ; eauto).A, B: Type
a: instr
l0: list instr
IHl0: forall (l1 : list instr) 
  (sp : val) (ge : Genv.t A B) 
  (s1 : istate) (s2 : instr_state)
  (s3 : istate),
step_list2 (step_instr ge) sp s1 l0 (Iexec s2) ->
SeqBB.step ge sp s1 (l0 ++ l1) s3 ->
SeqBB.step ge sp (Iexec s2) l1 s3
l1: list instr
sp: val
ge: Genv.t A B
s2, state0, state': instr_state
cf: cf_instr
H6: step_instr ge sp (Iexec state0) a
  (Iterm state' cf)
i1: istate
H4: step_instr ge sp (Iexec state0) a i1
H7: step_list2 (step_instr ge) sp i1 l0 (Iexec s2)
H: i1 = Iterm state' cf
SeqBB.step ge sp (Iexec s2) l1 (Iterm state' cf) subst.A, B: Type
a: instr
l0: list instr
IHl0: forall (l1 : list instr) 
  (sp : val) (ge : Genv.t A B) 
  (s1 : istate) (s2 : instr_state)
  (s3 : istate),
step_list2 (step_instr ge) sp s1 l0 (Iexec s2) ->
SeqBB.step ge sp s1 (l0 ++ l1) s3 ->
SeqBB.step ge sp (Iexec s2) l1 s3
l1: list instr
sp: val
ge: Genv.t A B
s2, state0, state': instr_state
cf: cf_instr
H6: step_instr ge sp (Iexec state0) a
  (Iterm state' cf)
H7: step_list2 (step_instr ge) sp 
  (Iterm state' cf) l0 (Iexec s2)
H4: step_instr ge sp (Iexec state0) a
  (Iterm state' cf)
SeqBB.step ge sp (Iexec s2) l1 (Iterm state' cf)
  exfalso; eapply step_list2_false; eauto.
Qed.

Lemma step_cf_in :
  forall A B (ge: Genv.t A B) sp bb i1 i2 cf,
    SeqBB.step ge sp (Iexec i1) bb (Iterm i2 cf) ->
    exists p, In (RBexit p cf) bb.forall (A B : Type) (ge : Genv.t A B) (sp : val)
  (bb : list instr) (i1 i2 : instr_state)
  (cf : cf_instr),
SeqBB.step ge sp (Iexec i1) bb (Iterm i2 cf) ->
exists p : option Gible.pred_op, In (RBexit p cf) bb
Proof.forall (A B : Type) (ge : Genv.t A B) (sp : val)
  (bb : list instr) (i1 i2 : instr_state)
  (cf : cf_instr),
SeqBB.step ge sp (Iexec i1) bb (Iterm i2 cf) ->
exists p : option Gible.pred_op, In (RBexit p cf) bb
  induction bb; crush; inv H; eauto.A, B: Type
ge: Genv.t A B
sp: val
a: instr
bb: list instr
IHbb: forall (i1 i2 : instr_state) (cf : cf_instr),
SeqBB.step ge sp (Iexec i1) bb (Iterm i2 cf) ->
exists p : option Gible.pred_op,
  In (RBexit p cf) bb
i1, i2: instr_state
cf: cf_instr
state': instr_state
H5: step_instr ge sp (Iexec i1) a (Iexec state')
H7: step_list (step_instr ge) sp 
  (Iexec state') bb (Iterm i2 cf)
exists p : option Gible.pred_op,
  a = RBexit p cf \/ In (RBexit p cf) bb
A, B: Type
ge: Genv.t A B
sp: val
a: instr
bb: list instr
IHbb: forall (i1 i2 : instr_state) (cf : cf_instr),
SeqBB.step ge sp (Iexec i1) bb (Iterm i2 cf) ->
exists p : option Gible.pred_op,
  In (RBexit p cf) bb
i1, i2: instr_state
cf: cf_instr
H3: step_instr ge sp (Iexec i1) a (Iterm i2 cf)
exists p : option Gible.pred_op,
  a = RBexit p cf \/ In (RBexit p cf) bb
  exploit IHbb; eauto; simplify; eauto.A, B: Type
ge: Genv.t A B
sp: val
a: instr
bb: list instr
IHbb: forall (i1 i2 : instr_state) (cf : cf_instr),
SeqBB.step ge sp (Iexec i1) bb (Iterm i2 cf) ->
exists p : option Gible.pred_op,
  In (RBexit p cf) bb
i1, i2: instr_state
cf: cf_instr
H3: step_instr ge sp (Iexec i1) a (Iterm i2 cf)
exists p : option Gible.pred_op,
  a = RBexit p cf \/ In (RBexit p cf) bb
  inv H3; eauto.
Qed.

Lemma SeqBB_foldl_In :
  forall bb l pc,
    In pc l ->
    In pc (fold_left (fun (ns : list node) (i : instr) => match i with
                                                       | RBexit _ cf0 => successors_instr cf0 ++ ns
                                                       | _ => ns
                                                       end) bb l).forall (bb : list instr) (l : list node) (pc : node),
In pc l ->
In pc
  (fold_left
     (fun (ns : list node) (i : instr) =>
      match i with
      | RBexit _ cf0 => successors_instr cf0 ++ ns
      | _ => ns
      end) bb l)
Proof.forall (bb : list instr) (l : list node) (pc : node),
In pc l ->
In pc
  (fold_left
     (fun (ns : list node) (i : instr) =>
      match i with
      | RBexit _ cf0 => successors_instr cf0 ++ ns
      | _ => ns
      end) bb l)
  induction bb; crush.a: instr
bb: list instr
IHbb: forall (l : list node) (pc : node),
In pc l ->
In pc
  (fold_left
     (fun (ns : list node) (i : instr) =>
      match i with
      | RBexit _ cf0 =>
          successors_instr cf0 ++ ns
      | _ => ns
      end) bb l)
l: list node
pc: node
H: In pc l
In pc
  (fold_left
     (fun (ns : list node) (i : instr) =>
      match i with
      | RBexit _ cf0 => successors_instr cf0 ++ ns
      | _ => ns
      end) bb
     match a with
     | RBexit _ cf0 => successors_instr cf0 ++ l
     | _ => l
     end) eapply IHbb; eauto.a: instr
bb: list instr
IHbb: forall (l : list node) (pc : node),
In pc l ->
In pc
  (fold_left
     (fun (ns : list node) (i : instr) =>
      match i with
      | RBexit _ cf0 =>
          successors_instr cf0 ++ ns
      | _ => ns
      end) bb l)
l: list node
pc: node
H: In pc l
In pc
  match a with
  | RBexit _ cf0 => successors_instr cf0 ++ l
  | _ => l
  end
  destruct a; auto.o: option Gible.pred_op
c: cf_instr
bb: list instr
IHbb: forall (l : list node) (pc : node),
In pc l ->
In pc
  (fold_left
     (fun (ns : list node) (i : instr) =>
      match i with
      | RBexit _ cf0 =>
          successors_instr cf0 ++ ns
      | _ => ns
      end) bb l)
l: list node
pc: node
H: In pc l
In pc (successors_instr c ++ l)
  apply in_or_app; auto.
Qed.

Lemma in_cf_all_successors' :
  forall bb pc cf p l,
    In pc (successors_instr cf) ->
    In (RBexit p cf) bb ->
    In pc (fold_left (fun (ns : list node) (i : instr) => match i with
                                                       | RBexit _ cf0 => successors_instr cf0 ++ ns
                                                       | _ => ns
                                                       end) bb l).forall (bb : list instr) (pc : node) (cf : cf_instr)
  (p : option Gible.pred_op) (l : list node),
In pc (successors_instr cf) ->
In (RBexit p cf) bb ->
In pc
  (fold_left
     (fun (ns : list node) (i : instr) =>
      match i with
      | RBexit _ cf0 => successors_instr cf0 ++ ns
      | _ => ns
      end) bb l)
Proof.forall (bb : list instr) (pc : node) (cf : cf_instr)
  (p : option Gible.pred_op) (l : list node),
In pc (successors_instr cf) ->
In (RBexit p cf) bb ->
In pc
  (fold_left
     (fun (ns : list node) (i : instr) =>
      match i with
      | RBexit _ cf0 => successors_instr cf0 ++ ns
      | _ => ns
      end) bb l)
  induction bb; crush.a: instr
bb: list instr
IHbb: forall (pc : node) (cf : cf_instr)
  (p : option Gible.pred_op) 
  (l : list node),
In pc (successors_instr cf) ->
In (RBexit p cf) bb ->
In pc
  (fold_left
     (fun (ns : list node) (i : instr) =>
      match i with
      | RBexit _ cf0 =>
          successors_instr cf0 ++ ns
      | _ => ns
      end) bb l)
pc: node
cf: cf_instr
p: option Gible.pred_op
l: list node
H: In pc (successors_instr cf)
H0: a = RBexit p cf \/ In (RBexit p cf) bb
In pc
  (fold_left
     (fun (ns : list node) (i : instr) =>
      match i with
      | RBexit _ cf0 => successors_instr cf0 ++ ns
      | _ => ns
      end) bb
     match a with
     | RBexit _ cf0 => successors_instr cf0 ++ l
     | _ => l
     end)
  inv H0.bb: list instr
IHbb: forall (pc : node) (cf : cf_instr)
  (p : option Gible.pred_op) 
  (l : list node),
In pc (successors_instr cf) ->
In (RBexit p cf) bb ->
In pc
  (fold_left
     (fun (ns : list node) (i : instr) =>
      match i with
      | RBexit _ cf0 =>
          successors_instr cf0 ++ ns
      | _ => ns
      end) bb l)
pc: node
cf: cf_instr
p: option Gible.pred_op
l: list node
H: In pc (successors_instr cf)
In pc
  (fold_left
     (fun (ns : list node) (i : instr) =>
      match i with
      | RBexit _ cf0 => successors_instr cf0 ++ ns
      | _ => ns
      end) bb (successors_instr cf ++ l))
a: instr
bb: list instr
IHbb: forall (pc : node) (cf : cf_instr)
  (p : option Gible.pred_op) 
  (l : list node),
In pc (successors_instr cf) ->
In (RBexit p cf) bb ->
In pc
  (fold_left
     (fun (ns : list node) (i : instr) =>
      match i with
      | RBexit _ cf0 =>
          successors_instr cf0 ++ ns
      | _ => ns
      end) bb l)
pc: node
cf: cf_instr
p: option Gible.pred_op
l: list node
H: In pc (successors_instr cf)
H1: In (RBexit p cf) bb
In pc
  (fold_left
     (fun (ns : list node) (i : instr) =>
      match i with
      | RBexit _ cf0 => successors_instr cf0 ++ ns
      | _ => ns
      end) bb
     match a with
     | RBexit _ cf0 => successors_instr cf0 ++ l
     | _ => l
     end) simplify.bb: list instr
IHbb: forall (pc : node) (cf : cf_instr)
  (p : option Gible.pred_op) 
  (l : list node),
In pc (successors_instr cf) ->
In (RBexit p cf) bb ->
In pc
  (fold_left
     (fun (ns : list node) (i : instr) =>
      match i with
      | RBexit _ cf0 =>
          successors_instr cf0 ++ ns
      | _ => ns
      end) bb l)
pc: node
cf: cf_instr
p: option Gible.pred_op
l: list node
H: In pc (successors_instr cf)
In pc
  (fold_left
     (fun (ns : list node) (i : instr) =>
      match i with
      | RBexit _ cf0 => successors_instr cf0 ++ ns
      | _ => ns
      end) bb (successors_instr cf ++ l))
a: instr
bb: list instr
IHbb: forall (pc : node) (cf : cf_instr)
  (p : option Gible.pred_op) 
  (l : list node),
In pc (successors_instr cf) ->
In (RBexit p cf) bb ->
In pc
  (fold_left
     (fun (ns : list node) (i : instr) =>
      match i with
      | RBexit _ cf0 =>
          successors_instr cf0 ++ ns
      | _ => ns
      end) bb l)
pc: node
cf: cf_instr
p: option Gible.pred_op
l: list node
H: In pc (successors_instr cf)
H1: In (RBexit p cf) bb
In pc
  (fold_left
     (fun (ns : list node) (i : instr) =>
      match i with
      | RBexit _ cf0 => successors_instr cf0 ++ ns
      | _ => ns
      end) bb
     match a with
     | RBexit _ cf0 => successors_instr cf0 ++ l
     | _ => l
     end)
  eapply SeqBB_foldl_In.bb: list instr
IHbb: forall (pc : node) (cf : cf_instr)
  (p : option Gible.pred_op) 
  (l : list node),
In pc (successors_instr cf) ->
In (RBexit p cf) bb ->
In pc
  (fold_left
     (fun (ns : list node) (i : instr) =>
      match i with
      | RBexit _ cf0 =>
          successors_instr cf0 ++ ns
      | _ => ns
      end) bb l)
pc: node
cf: cf_instr
p: option Gible.pred_op
l: list node
H: In pc (successors_instr cf)
In pc (successors_instr cf ++ l)
a: instr
bb: list instr
IHbb: forall (pc : node) (cf : cf_instr)
  (p : option Gible.pred_op) 
  (l : list node),
In pc (successors_instr cf) ->
In (RBexit p cf) bb ->
In pc
  (fold_left
     (fun (ns : list node) (i : instr) =>
      match i with
      | RBexit _ cf0 =>
          successors_instr cf0 ++ ns
      | _ => ns
      end) bb l)
pc: node
cf: cf_instr
p: option Gible.pred_op
l: list node
H: In pc (successors_instr cf)
H1: In (RBexit p cf) bb
In pc
  (fold_left
     (fun (ns : list node) (i : instr) =>
      match i with
      | RBexit _ cf0 => successors_instr cf0 ++ ns
      | _ => ns
      end) bb
     match a with
     | RBexit _ cf0 => successors_instr cf0 ++ l
     | _ => l
     end)
  apply in_or_app; auto.a: instr
bb: list instr
IHbb: forall (pc : node) (cf : cf_instr)
  (p : option Gible.pred_op) 
  (l : list node),
In pc (successors_instr cf) ->
In (RBexit p cf) bb ->
In pc
  (fold_left
     (fun (ns : list node) (i : instr) =>
      match i with
      | RBexit _ cf0 =>
          successors_instr cf0 ++ ns
      | _ => ns
      end) bb l)
pc: node
cf: cf_instr
p: option Gible.pred_op
l: list node
H: In pc (successors_instr cf)
H1: In (RBexit p cf) bb
In pc
  (fold_left
     (fun (ns : list node) (i : instr) =>
      match i with
      | RBexit _ cf0 => successors_instr cf0 ++ ns
      | _ => ns
      end) bb
     match a with
     | RBexit _ cf0 => successors_instr cf0 ++ l
     | _ => l
     end)
  eapply IHbb; eauto.
Qed.

Lemma in_cf_all_successors :
  forall bb pc cf p,
    In pc (successors_instr cf) ->
    In (RBexit p cf) bb ->
    In pc (all_successors bb).forall (bb : list instr) (pc : node) (cf : cf_instr)
  (p : option Gible.pred_op),
In pc (successors_instr cf) ->
In (RBexit p cf) bb -> In pc (all_successors bb)
Proof.forall (bb : list instr) (pc : node) (cf : cf_instr)
  (p : option Gible.pred_op),
In pc (successors_instr cf) ->
In (RBexit p cf) bb -> In pc (all_successors bb)
  unfold all_successors, SeqBB.foldl; intros.bb: list instr
pc: node
cf: cf_instr
p: option Gible.pred_op
H: In pc (successors_instr cf)
H0: In (RBexit p cf) bb
In pc
  (fold_left
     (fun (ns : list node) (i : instr) =>
      match i with
      | RBexit _ cf => successors_instr cf ++ ns
      | _ => ns
      end) bb nil)
  eapply in_cf_all_successors'; eauto.
Qed.

Lemma eq_stepBB :
  forall A B (ge: Genv.t A B) sp l i1 i2 i2',
    SeqBB.step ge sp i1 l i2 ->
    SeqBB.step ge sp i1 l i2' ->
    i2 = i2'.forall (A B : Type) (ge : Genv.t A B) (sp : val)
  (l : list instr) (i1 i2 i2' : istate),
SeqBB.step ge sp i1 l i2 ->
SeqBB.step ge sp i1 l i2' -> i2 = i2'
Proof.forall (A B : Type) (ge : Genv.t A B) (sp : val)
  (l : list instr) (i1 i2 i2' : istate),
SeqBB.step ge sp i1 l i2 ->
SeqBB.step ge sp i1 l i2' -> i2 = i2'
  induction l; crush.A, B: Type
ge: Genv.t A B
sp: val
i1, i2, i2': istate
H: SeqBB.step ge sp i1 nil i2
H0: SeqBB.step ge sp i1 nil i2'
i2 = i2'
A, B: Type
ge: Genv.t A B
sp: val
a: instr
l: list instr
IHl: forall i1 i2 i2' : istate,
SeqBB.step ge sp i1 l i2 -> SeqBB.step ge sp i1 l i2' -> i2 = i2'
i1, i2, i2': istate
H: SeqBB.step ge sp i1 (a :: l) i2
H0: SeqBB.step ge sp i1 (a :: l) i2'
i2 = i2'  inv H.A, B: Type
ge: Genv.t A B
sp: val
a: instr
l: list instr
IHl: forall i1 i2 i2' : istate,
SeqBB.step ge sp i1 l i2 -> SeqBB.step ge sp i1 l i2' -> i2 = i2'
i1, i2, i2': istate
H: SeqBB.step ge sp i1 (a :: l) i2
H0: SeqBB.step ge sp i1 (a :: l) i2'
i2 = i2'
  inv H; inv H0.A, B: Type
ge: Genv.t A B
sp: val
a: instr
l: list instr
IHl: forall i1 i2 i2' : istate,
SeqBB.step ge sp i1 l i2 -> SeqBB.step ge sp i1 l i2' -> i2 = i2'
state0, state', state'': instr_state
cf: cf_instr
H5: step_instr ge sp (Iexec state0) a (Iexec state')
H7: step_list (step_instr ge) sp 
  (Iexec state') l (Iterm state'' cf)
state'0, state''0: instr_state
cf0: cf_instr
H4: step_instr ge sp (Iexec state0) a (Iexec state'0)
H8: step_list (step_instr ge) sp 
  (Iexec state'0) l (Iterm state''0 cf0)
Iterm state'' cf = Iterm state''0 cf0
A, B: Type
ge: Genv.t A B
sp: val
a: instr
l: list instr
IHl: forall i1 i2 i2' : istate,
SeqBB.step ge sp i1 l i2 ->
SeqBB.step ge sp i1 l i2' -> i2 = i2'
state0, state', state'': instr_state
cf: cf_instr
H5: step_instr ge sp (Iexec state0) a (Iexec state')
H7: step_list (step_instr ge) sp 
  (Iexec state') l (Iterm state'' cf)
state'0: instr_state
cf0: cf_instr
H6: step_instr ge sp (Iexec state0) a
  (Iterm state'0 cf0)
Iterm state'' cf = Iterm state'0 cf0
A, B: Type
ge: Genv.t A B
sp: val
a: instr
l: list instr
IHl: forall i1 i2 i2' : istate,
SeqBB.step ge sp i1 l i2 ->
SeqBB.step ge sp i1 l i2' -> i2 = i2'
state0, state': instr_state
cf: cf_instr
H6: step_instr ge sp (Iexec state0) a
  (Iterm state' cf)
state'0, state'': instr_state
cf0: cf_instr
H4: step_instr ge sp (Iexec state0) a (Iexec state'0)
H7: step_list (step_instr ge) sp 
  (Iexec state'0) l (Iterm state'' cf0)
Iterm state' cf = Iterm state'' cf0
A, B: Type
ge: Genv.t A B
sp: val
a: instr
l: list instr
IHl: forall i1 i2 i2' : istate,
SeqBB.step ge sp i1 l i2 ->
SeqBB.step ge sp i1 l i2' -> i2 = i2'
state0, state': instr_state
cf: cf_instr
H6: step_instr ge sp (Iexec state0) a
  (Iterm state' cf)
state'0: instr_state
cf0: cf_instr
H5: step_instr ge sp (Iexec state0) a
  (Iterm state'0 cf0)
Iterm state' cf = Iterm state'0 cf0
  assert (Iexec state' = Iexec state'0).A, B: Type
ge: Genv.t A B
sp: val
a: instr
l: list instr
IHl: forall i1 i2 i2' : istate,
SeqBB.step ge sp i1 l i2 ->
SeqBB.step ge sp i1 l i2' -> i2 = i2'
state0, state', state'': instr_state
cf: cf_instr
H5: step_instr ge sp (Iexec state0) a (Iexec state')
H7: step_list (step_instr ge) sp 
  (Iexec state') l (Iterm state'' cf)
state'0, state''0: instr_state
cf0: cf_instr
H4: step_instr ge sp (Iexec state0) a (Iexec state'0)
H8: step_list (step_instr ge) sp 
  (Iexec state'0) l (Iterm state''0 cf0)
Iexec state' = Iexec state'0
A, B: Type
ge: Genv.t A B
sp: val
a: instr
l: list instr
IHl: forall i1 i2 i2' : istate,
SeqBB.step ge sp i1 l i2 ->
SeqBB.step ge sp i1 l i2' -> i2 = i2'
state0, state', state'': instr_state
cf: cf_instr
H5: step_instr ge sp (Iexec state0) a (Iexec state')
H7: step_list (step_instr ge) sp 
  (Iexec state') l (Iterm state'' cf)
state'0, state''0: instr_state
cf0: cf_instr
H4: step_instr ge sp (Iexec state0) a (Iexec state'0)
H8: step_list (step_instr ge) sp 
  (Iexec state'0) l (Iterm state''0 cf0)
H: Iexec state' = Iexec state'0
Iterm state'' cf = Iterm state''0 cf0
A, B: Type
ge: Genv.t A B
sp: val
a: instr
l: list instr
IHl: forall i1 i2 i2' : istate,
SeqBB.step ge sp i1 l i2 ->
SeqBB.step ge sp i1 l i2' -> i2 = i2'
state0, state', state'': instr_state
cf: cf_instr
H5: step_instr ge sp (Iexec state0) a (Iexec state')
H7: step_list (step_instr ge) sp 
  (Iexec state') l (Iterm state'' cf)
state'0: instr_state
cf0: cf_instr
H6: step_instr ge sp (Iexec state0) a
  (Iterm state'0 cf0)
Iterm state'' cf = Iterm state'0 cf0
A, B: Type
ge: Genv.t A B
sp: val
a: instr
l: list instr
IHl: forall i1 i2 i2' : istate,
SeqBB.step ge sp i1 l i2 ->
SeqBB.step ge sp i1 l i2' -> i2 = i2'
state0, state': instr_state
cf: cf_instr
H6: step_instr ge sp (Iexec state0) a
  (Iterm state' cf)
state'0, state'': instr_state
cf0: cf_instr
H4: step_instr ge sp (Iexec state0) a (Iexec state'0)
H7: step_list (step_instr ge) sp 
  (Iexec state'0) l (Iterm state'' cf0)
Iterm state' cf = Iterm state'' cf0
A, B: Type
ge: Genv.t A B
sp: val
a: instr
l: list instr
IHl: forall i1 i2 i2' : istate,
SeqBB.step ge sp i1 l i2 ->
SeqBB.step ge sp i1 l i2' -> i2 = i2'
state0, state': instr_state
cf: cf_instr
H6: step_instr ge sp (Iexec state0) a
  (Iterm state' cf)
state'0: instr_state
cf0: cf_instr
H5: step_instr ge sp (Iexec state0) a
  (Iterm state'0 cf0)
Iterm state' cf = Iterm state'0 cf0
  {A, B: Type
ge: Genv.t A B
sp: val
a: instr
l: list instr
IHl: forall i1 i2 i2' : istate,
SeqBB.step ge sp i1 l i2 ->
SeqBB.step ge sp i1 l i2' -> i2 = i2'
state0, state', state'': instr_state
cf: cf_instr
H5: step_instr ge sp (Iexec state0) a (Iexec state')
H7: step_list (step_instr ge) sp 
  (Iexec state') l (Iterm state'' cf)
state'0, state''0: instr_state
cf0: cf_instr
H4: step_instr ge sp (Iexec state0) a (Iexec state'0)
H8: step_list (step_instr ge) sp 
  (Iexec state'0) l (Iterm state''0 cf0)
Iexec state' = Iexec state'0 eapply exec_determ; eauto. }A, B: Type
ge: Genv.t A B
sp: val
a: instr
l: list instr
IHl: forall i1 i2 i2' : istate,
SeqBB.step ge sp i1 l i2 ->
SeqBB.step ge sp i1 l i2' -> i2 = i2'
state0, state', state'': instr_state
cf: cf_instr
H5: step_instr ge sp (Iexec state0) a (Iexec state')
H7: step_list (step_instr ge) sp 
  (Iexec state') l (Iterm state'' cf)
state'0, state''0: instr_state
cf0: cf_instr
H4: step_instr ge sp (Iexec state0) a (Iexec state'0)
H8: step_list (step_instr ge) sp 
  (Iexec state'0) l (Iterm state''0 cf0)
H: Iexec state' = Iexec state'0
Iterm state'' cf = Iterm state''0 cf0
A, B: Type
ge: Genv.t A B
sp: val
a: instr
l: list instr
IHl: forall i1 i2 i2' : istate,
SeqBB.step ge sp i1 l i2 ->
SeqBB.step ge sp i1 l i2' -> i2 = i2'
state0, state', state'': instr_state
cf: cf_instr
H5: step_instr ge sp (Iexec state0) a (Iexec state')
H7: step_list (step_instr ge) sp 
  (Iexec state') l (Iterm state'' cf)
state'0: instr_state
cf0: cf_instr
H6: step_instr ge sp (Iexec state0) a
  (Iterm state'0 cf0)
Iterm state'' cf = Iterm state'0 cf0
A, B: Type
ge: Genv.t A B
sp: val
a: instr
l: list instr
IHl: forall i1 i2 i2' : istate,
SeqBB.step ge sp i1 l i2 ->
SeqBB.step ge sp i1 l i2' -> i2 = i2'
state0, state': instr_state
cf: cf_instr
H6: step_instr ge sp (Iexec state0) a
  (Iterm state' cf)
state'0, state'': instr_state
cf0: cf_instr
H4: step_instr ge sp (Iexec state0) a (Iexec state'0)
H7: step_list (step_instr ge) sp 
  (Iexec state'0) l (Iterm state'' cf0)
Iterm state' cf = Iterm state'' cf0
A, B: Type
ge: Genv.t A B
sp: val
a: instr
l: list instr
IHl: forall i1 i2 i2' : istate,
SeqBB.step ge sp i1 l i2 ->
SeqBB.step ge sp i1 l i2' -> i2 = i2'
state0, state': instr_state
cf: cf_instr
H6: step_instr ge sp (Iexec state0) a
  (Iterm state' cf)
state'0: instr_state
cf0: cf_instr
H5: step_instr ge sp (Iexec state0) a
  (Iterm state'0 cf0)
Iterm state' cf = Iterm state'0 cf0
  inv H.A, B: Type
ge: Genv.t A B
sp: val
a: instr
l: list instr
IHl: forall i1 i2 i2' : istate,
SeqBB.step ge sp i1 l i2 ->
SeqBB.step ge sp i1 l i2' -> i2 = i2'
state0, state'': instr_state
cf: cf_instr
state'0: instr_state
H7: step_list (step_instr ge) sp 
  (Iexec state'0) l (Iterm state'' cf)
H5: step_instr ge sp (Iexec state0) a (Iexec state'0)
state''0: instr_state
cf0: cf_instr
H4: step_instr ge sp (Iexec state0) a (Iexec state'0)
H8: step_list (step_instr ge) sp 
  (Iexec state'0) l (Iterm state''0 cf0)
Iterm state'' cf = Iterm state''0 cf0
A, B: Type
ge: Genv.t A B
sp: val
a: instr
l: list instr
IHl: forall i1 i2 i2' : istate,
SeqBB.step ge sp i1 l i2 ->
SeqBB.step ge sp i1 l i2' -> i2 = i2'
state0, state', state'': instr_state
cf: cf_instr
H5: step_instr ge sp (Iexec state0) a (Iexec state')
H7: step_list (step_instr ge) sp 
  (Iexec state') l (Iterm state'' cf)
state'0: instr_state
cf0: cf_instr
H6: step_instr ge sp (Iexec state0) a
  (Iterm state'0 cf0)
Iterm state'' cf = Iterm state'0 cf0
A, B: Type
ge: Genv.t A B
sp: val
a: instr
l: list instr
IHl: forall i1 i2 i2' : istate,
SeqBB.step ge sp i1 l i2 ->
SeqBB.step ge sp i1 l i2' -> i2 = i2'
state0, state': instr_state
cf: cf_instr
H6: step_instr ge sp (Iexec state0) a
  (Iterm state' cf)
state'0, state'': instr_state
cf0: cf_instr
H4: step_instr ge sp (Iexec state0) a (Iexec state'0)
H7: step_list (step_instr ge) sp 
  (Iexec state'0) l (Iterm state'' cf0)
Iterm state' cf = Iterm state'' cf0
A, B: Type
ge: Genv.t A B
sp: val
a: instr
l: list instr
IHl: forall i1 i2 i2' : istate,
SeqBB.step ge sp i1 l i2 ->
SeqBB.step ge sp i1 l i2' -> i2 = i2'
state0, state': instr_state
cf: cf_instr
H6: step_instr ge sp (Iexec state0) a
  (Iterm state' cf)
state'0: instr_state
cf0: cf_instr
H5: step_instr ge sp (Iexec state0) a
  (Iterm state'0 cf0)
Iterm state' cf = Iterm state'0 cf0 eauto.A, B: Type
ge: Genv.t A B
sp: val
a: instr
l: list instr
IHl: forall i1 i2 i2' : istate,
SeqBB.step ge sp i1 l i2 ->
SeqBB.step ge sp i1 l i2' -> i2 = i2'
state0, state', state'': instr_state
cf: cf_instr
H5: step_instr ge sp (Iexec state0) a (Iexec state')
H7: step_list (step_instr ge) sp 
  (Iexec state') l (Iterm state'' cf)
state'0: instr_state
cf0: cf_instr
H6: step_instr ge sp (Iexec state0) a
  (Iterm state'0 cf0)
Iterm state'' cf = Iterm state'0 cf0
A, B: Type
ge: Genv.t A B
sp: val
a: instr
l: list instr
IHl: forall i1 i2 i2' : istate,
SeqBB.step ge sp i1 l i2 ->
SeqBB.step ge sp i1 l i2' -> i2 = i2'
state0, state': instr_state
cf: cf_instr
H6: step_instr ge sp (Iexec state0) a
  (Iterm state' cf)
state'0, state'': instr_state
cf0: cf_instr
H4: step_instr ge sp (Iexec state0) a (Iexec state'0)
H7: step_list (step_instr ge) sp 
  (Iexec state'0) l (Iterm state'' cf0)
Iterm state' cf = Iterm state'' cf0
A, B: Type
ge: Genv.t A B
sp: val
a: instr
l: list instr
IHl: forall i1 i2 i2' : istate,
SeqBB.step ge sp i1 l i2 ->
SeqBB.step ge sp i1 l i2' -> i2 = i2'
state0, state': instr_state
cf: cf_instr
H6: step_instr ge sp (Iexec state0) a
  (Iterm state' cf)
state'0: instr_state
cf0: cf_instr
H5: step_instr ge sp (Iexec state0) a
  (Iterm state'0 cf0)
Iterm state' cf = Iterm state'0 cf0
  assert (Iexec state' = Iterm state'0 cf0).A, B: Type
ge: Genv.t A B
sp: val
a: instr
l: list instr
IHl: forall i1 i2 i2' : istate,
SeqBB.step ge sp i1 l i2 ->
SeqBB.step ge sp i1 l i2' -> i2 = i2'
state0, state', state'': instr_state
cf: cf_instr
H5: step_instr ge sp (Iexec state0) a (Iexec state')
H7: step_list (step_instr ge) sp 
  (Iexec state') l (Iterm state'' cf)
state'0: instr_state
cf0: cf_instr
H6: step_instr ge sp (Iexec state0) a
  (Iterm state'0 cf0)
Iexec state' = Iterm state'0 cf0
A, B: Type
ge: Genv.t A B
sp: val
a: instr
l: list instr
IHl: forall i1 i2 i2' : istate,
SeqBB.step ge sp i1 l i2 ->
SeqBB.step ge sp i1 l i2' -> i2 = i2'
state0, state', state'': instr_state
cf: cf_instr
H5: step_instr ge sp (Iexec state0) a (Iexec state')
H7: step_list (step_instr ge) sp 
  (Iexec state') l (Iterm state'' cf)
state'0: instr_state
cf0: cf_instr
H6: step_instr ge sp (Iexec state0) a
  (Iterm state'0 cf0)
H: Iexec state' = Iterm state'0 cf0
Iterm state'' cf = Iterm state'0 cf0
A, B: Type
ge: Genv.t A B
sp: val
a: instr
l: list instr
IHl: forall i1 i2 i2' : istate,
SeqBB.step ge sp i1 l i2 ->
SeqBB.step ge sp i1 l i2' -> i2 = i2'
state0, state': instr_state
cf: cf_instr
H6: step_instr ge sp (Iexec state0) a
  (Iterm state' cf)
state'0, state'': instr_state
cf0: cf_instr
H4: step_instr ge sp (Iexec state0) a (Iexec state'0)
H7: step_list (step_instr ge) sp 
  (Iexec state'0) l (Iterm state'' cf0)
Iterm state' cf = Iterm state'' cf0
A, B: Type
ge: Genv.t A B
sp: val
a: instr
l: list instr
IHl: forall i1 i2 i2' : istate,
SeqBB.step ge sp i1 l i2 ->
SeqBB.step ge sp i1 l i2' -> i2 = i2'
state0, state': instr_state
cf: cf_instr
H6: step_instr ge sp (Iexec state0) a
  (Iterm state' cf)
state'0: instr_state
cf0: cf_instr
H5: step_instr ge sp (Iexec state0) a
  (Iterm state'0 cf0)
Iterm state' cf = Iterm state'0 cf0
  {A, B: Type
ge: Genv.t A B
sp: val
a: instr
l: list instr
IHl: forall i1 i2 i2' : istate,
SeqBB.step ge sp i1 l i2 ->
SeqBB.step ge sp i1 l i2' -> i2 = i2'
state0, state', state'': instr_state
cf: cf_instr
H5: step_instr ge sp (Iexec state0) a (Iexec state')
H7: step_list (step_instr ge) sp 
  (Iexec state') l (Iterm state'' cf)
state'0: instr_state
cf0: cf_instr
H6: step_instr ge sp (Iexec state0) a
  (Iterm state'0 cf0)
Iexec state' = Iterm state'0 cf0 eapply exec_determ; eauto. }A, B: Type
ge: Genv.t A B
sp: val
a: instr
l: list instr
IHl: forall i1 i2 i2' : istate,
SeqBB.step ge sp i1 l i2 ->
SeqBB.step ge sp i1 l i2' -> i2 = i2'
state0, state', state'': instr_state
cf: cf_instr
H5: step_instr ge sp (Iexec state0) a (Iexec state')
H7: step_list (step_instr ge) sp 
  (Iexec state') l (Iterm state'' cf)
state'0: instr_state
cf0: cf_instr
H6: step_instr ge sp (Iexec state0) a
  (Iterm state'0 cf0)
H: Iexec state' = Iterm state'0 cf0
Iterm state'' cf = Iterm state'0 cf0
A, B: Type
ge: Genv.t A B
sp: val
a: instr
l: list instr
IHl: forall i1 i2 i2' : istate,
SeqBB.step ge sp i1 l i2 ->
SeqBB.step ge sp i1 l i2' -> i2 = i2'
state0, state': instr_state
cf: cf_instr
H6: step_instr ge sp (Iexec state0) a
  (Iterm state' cf)
state'0, state'': instr_state
cf0: cf_instr
H4: step_instr ge sp (Iexec state0) a (Iexec state'0)
H7: step_list (step_instr ge) sp 
  (Iexec state'0) l (Iterm state'' cf0)
Iterm state' cf = Iterm state'' cf0
A, B: Type
ge: Genv.t A B
sp: val
a: instr
l: list instr
IHl: forall i1 i2 i2' : istate,
SeqBB.step ge sp i1 l i2 ->
SeqBB.step ge sp i1 l i2' -> i2 = i2'
state0, state': instr_state
cf: cf_instr
H6: step_instr ge sp (Iexec state0) a
  (Iterm state' cf)
state'0: instr_state
cf0: cf_instr
H5: step_instr ge sp (Iexec state0) a
  (Iterm state'0 cf0)
Iterm state' cf = Iterm state'0 cf0
  discriminate.A, B: Type
ge: Genv.t A B
sp: val
a: instr
l: list instr
IHl: forall i1 i2 i2' : istate,
SeqBB.step ge sp i1 l i2 ->
SeqBB.step ge sp i1 l i2' -> i2 = i2'
state0, state': instr_state
cf: cf_instr
H6: step_instr ge sp (Iexec state0) a
  (Iterm state' cf)
state'0, state'': instr_state
cf0: cf_instr
H4: step_instr ge sp (Iexec state0) a (Iexec state'0)
H7: step_list (step_instr ge) sp 
  (Iexec state'0) l (Iterm state'' cf0)
Iterm state' cf = Iterm state'' cf0
A, B: Type
ge: Genv.t A B
sp: val
a: instr
l: list instr
IHl: forall i1 i2 i2' : istate,
SeqBB.step ge sp i1 l i2 ->
SeqBB.step ge sp i1 l i2' -> i2 = i2'
state0, state': instr_state
cf: cf_instr
H6: step_instr ge sp (Iexec state0) a
  (Iterm state' cf)
state'0: instr_state
cf0: cf_instr
H5: step_instr ge sp (Iexec state0) a
  (Iterm state'0 cf0)
Iterm state' cf = Iterm state'0 cf0
  assert (Iterm state' cf = Iexec state'0).A, B: Type
ge: Genv.t A B
sp: val
a: instr
l: list instr
IHl: forall i1 i2 i2' : istate,
SeqBB.step ge sp i1 l i2 ->
SeqBB.step ge sp i1 l i2' -> i2 = i2'
state0, state': instr_state
cf: cf_instr
H6: step_instr ge sp (Iexec state0) a
  (Iterm state' cf)
state'0, state'': instr_state
cf0: cf_instr
H4: step_instr ge sp (Iexec state0) a (Iexec state'0)
H7: step_list (step_instr ge) sp 
  (Iexec state'0) l (Iterm state'' cf0)
Iterm state' cf = Iexec state'0
A, B: Type
ge: Genv.t A B
sp: val
a: instr
l: list instr
IHl: forall i1 i2 i2' : istate,
SeqBB.step ge sp i1 l i2 ->
SeqBB.step ge sp i1 l i2' -> i2 = i2'
state0, state': instr_state
cf: cf_instr
H6: step_instr ge sp (Iexec state0) a
  (Iterm state' cf)
state'0, state'': instr_state
cf0: cf_instr
H4: step_instr ge sp (Iexec state0) a (Iexec state'0)
H7: step_list (step_instr ge) sp 
  (Iexec state'0) l (Iterm state'' cf0)
H: Iterm state' cf = Iexec state'0
Iterm state' cf = Iterm state'' cf0
A, B: Type
ge: Genv.t A B
sp: val
a: instr
l: list instr
IHl: forall i1 i2 i2' : istate,
SeqBB.step ge sp i1 l i2 ->
SeqBB.step ge sp i1 l i2' -> i2 = i2'
state0, state': instr_state
cf: cf_instr
H6: step_instr ge sp (Iexec state0) a
  (Iterm state' cf)
state'0: instr_state
cf0: cf_instr
H5: step_instr ge sp (Iexec state0) a
  (Iterm state'0 cf0)
Iterm state' cf = Iterm state'0 cf0
  {A, B: Type
ge: Genv.t A B
sp: val
a: instr
l: list instr
IHl: forall i1 i2 i2' : istate,
SeqBB.step ge sp i1 l i2 ->
SeqBB.step ge sp i1 l i2' -> i2 = i2'
state0, state': instr_state
cf: cf_instr
H6: step_instr ge sp (Iexec state0) a
  (Iterm state' cf)
state'0, state'': instr_state
cf0: cf_instr
H4: step_instr ge sp (Iexec state0) a (Iexec state'0)
H7: step_list (step_instr ge) sp 
  (Iexec state'0) l (Iterm state'' cf0)
Iterm state' cf = Iexec state'0 eapply exec_determ; eauto. }A, B: Type
ge: Genv.t A B
sp: val
a: instr
l: list instr
IHl: forall i1 i2 i2' : istate,
SeqBB.step ge sp i1 l i2 ->
SeqBB.step ge sp i1 l i2' -> i2 = i2'
state0, state': instr_state
cf: cf_instr
H6: step_instr ge sp (Iexec state0) a
  (Iterm state' cf)
state'0, state'': instr_state
cf0: cf_instr
H4: step_instr ge sp (Iexec state0) a (Iexec state'0)
H7: step_list (step_instr ge) sp 
  (Iexec state'0) l (Iterm state'' cf0)
H: Iterm state' cf = Iexec state'0
Iterm state' cf = Iterm state'' cf0
A, B: Type
ge: Genv.t A B
sp: val
a: instr
l: list instr
IHl: forall i1 i2 i2' : istate,
SeqBB.step ge sp i1 l i2 ->
SeqBB.step ge sp i1 l i2' -> i2 = i2'
state0, state': instr_state
cf: cf_instr
H6: step_instr ge sp (Iexec state0) a
  (Iterm state' cf)
state'0: instr_state
cf0: cf_instr
H5: step_instr ge sp (Iexec state0) a
  (Iterm state'0 cf0)
Iterm state' cf = Iterm state'0 cf0
  discriminate.A, B: Type
ge: Genv.t A B
sp: val
a: instr
l: list instr
IHl: forall i1 i2 i2' : istate,
SeqBB.step ge sp i1 l i2 ->
SeqBB.step ge sp i1 l i2' -> i2 = i2'
state0, state': instr_state
cf: cf_instr
H6: step_instr ge sp (Iexec state0) a
  (Iterm state' cf)
state'0: instr_state
cf0: cf_instr
H5: step_instr ge sp (Iexec state0) a
  (Iterm state'0 cf0)
Iterm state' cf = Iterm state'0 cf0
  eapply exec_determ; eauto.
Qed.

Lemma step_options :
  forall A B (ge: Genv.t A B) a b i1 i2 cf sp,
    SeqBB.step ge sp (Iexec i1) (a ++ b) (Iterm i2 cf) ->
    (SeqBB.step ge sp (Iexec i1) a (Iterm i2 cf) \/
       exists i1', step_list2 (step_instr ge) sp (Iexec i1) a (Iexec i1')
              /\ SeqBB.step ge sp (Iexec i1') b (Iterm i2 cf)).forall (A B : Type) (ge : Genv.t A B)
  (a b : list instr) (i1 i2 : instr_state)
  (cf : cf_instr) (sp : val),
SeqBB.step ge sp (Iexec i1) (a ++ b) (Iterm i2 cf) ->
SeqBB.step ge sp (Iexec i1) a (Iterm i2 cf) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp (Iexec i1) a
     (Iexec i1') /\
   SeqBB.step ge sp (Iexec i1') b (Iterm i2 cf))
Proof.forall (A B : Type) (ge : Genv.t A B)
  (a b : list instr) (i1 i2 : instr_state)
  (cf : cf_instr) (sp : val),
SeqBB.step ge sp (Iexec i1) (a ++ b) (Iterm i2 cf) ->
SeqBB.step ge sp (Iexec i1) a (Iterm i2 cf) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp (Iexec i1) a
     (Iexec i1') /\
   SeqBB.step ge sp (Iexec i1') b (Iterm i2 cf))
  induction a; crush.A, B: Type
ge: Genv.t A B
b: list instr
i1, i2: instr_state
cf: cf_instr
sp: val
H: SeqBB.step ge sp (Iexec i1) b (Iterm i2 cf)
SeqBB.step ge sp (Iexec i1) nil (Iterm i2 cf) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp (Iexec i1) nil
     (Iexec i1') /\
   SeqBB.step ge sp (Iexec i1') b (Iterm i2 cf))
A, B: Type
ge: Genv.t A B
a: instr
a0: list instr
IHa: forall (b : list instr) (i1 i2 : instr_state) (cf : cf_instr) (sp : val),
SeqBB.step ge sp (Iexec i1) (a0 ++ b) (Iterm i2 cf) ->
SeqBB.step ge sp (Iexec i1) a0 (Iterm i2 cf) \/
(exists i1' : instr_state,
step_list2 (step_instr ge) sp (Iexec i1) a0 (Iexec i1') /\
SeqBB.step ge sp (Iexec i1') b (Iterm i2 cf))
b: list instr
i1, i2: instr_state
cf: cf_instr
sp: val
H: SeqBB.step ge sp (Iexec i1) (a :: a0 ++ b)
  (Iterm i2 cf)
SeqBB.step ge sp (Iexec i1) (a :: a0) (Iterm i2 cf) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp (Iexec i1) (a :: a0)
     (Iexec i1') /\
   SeqBB.step ge sp (Iexec i1') b (Iterm i2 cf)) right; eexists; split; [constructor|auto].A, B: Type
ge: Genv.t A B
a: instr
a0: list instr
IHa: forall (b : list instr) (i1 i2 : instr_state) (cf : cf_instr) (sp : val),
SeqBB.step ge sp (Iexec i1) (a0 ++ b) (Iterm i2 cf) ->
SeqBB.step ge sp (Iexec i1) a0 (Iterm i2 cf) \/
(exists i1' : instr_state,
step_list2 (step_instr ge) sp (Iexec i1) a0 (Iexec i1') /\
SeqBB.step ge sp (Iexec i1') b (Iterm i2 cf))
b: list instr
i1, i2: instr_state
cf: cf_instr
sp: val
H: SeqBB.step ge sp (Iexec i1) (a :: a0 ++ b)
  (Iterm i2 cf)
SeqBB.step ge sp (Iexec i1) (a :: a0) (Iterm i2 cf) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp (Iexec i1) (a :: a0)
     (Iexec i1') /\
   SeqBB.step ge sp (Iexec i1') b (Iterm i2 cf))
  inv H.A, B: Type
ge: Genv.t A B
a: instr
a0: list instr
IHa: forall (b : list instr) (i1 i2 : instr_state) (cf : cf_instr) (sp : val),
SeqBB.step ge sp (Iexec i1) (a0 ++ b) (Iterm i2 cf) ->
SeqBB.step ge sp (Iexec i1) a0 (Iterm i2 cf) \/
(exists i1' : instr_state,
step_list2 (step_instr ge) sp (Iexec i1) a0 (Iexec i1') /\
SeqBB.step ge sp (Iexec i1') b (Iterm i2 cf))
b: list instr
i1, i2: instr_state
cf: cf_instr
sp: val
state': instr_state
H5: step_instr ge sp (Iexec i1) a (Iexec state')
H7: step_list (step_instr ge) sp 
  (Iexec state') (a0 ++ b) 
  (Iterm i2 cf)
SeqBB.step ge sp (Iexec i1) (a :: a0) (Iterm i2 cf) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp (Iexec i1) (a :: a0)
     (Iexec i1') /\
   SeqBB.step ge sp (Iexec i1') b (Iterm i2 cf))
A, B: Type
ge: Genv.t A B
a: instr
a0: list instr
IHa: forall (b : list instr) 
  (i1 i2 : instr_state) 
  (cf : cf_instr) (sp : val),
SeqBB.step ge sp (Iexec i1) 
  (a0 ++ b) (Iterm i2 cf) ->
SeqBB.step ge sp (Iexec i1) a0 (Iterm i2 cf) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp 
     (Iexec i1) a0 (Iexec i1') /\
   SeqBB.step ge sp (Iexec i1') b (Iterm i2 cf))
b: list instr
i1, i2: instr_state
cf: cf_instr
sp: val
H3: step_instr ge sp (Iexec i1) a (Iterm i2 cf)
SeqBB.step ge sp (Iexec i1) (a :: a0) (Iterm i2 cf) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp 
     (Iexec i1) (a :: a0) 
     (Iexec i1') /\
   SeqBB.step ge sp (Iexec i1') b (Iterm i2 cf)) exploit IHa; eauto; intros.A, B: Type
ge: Genv.t A B
a: instr
a0: list instr
IHa: forall (b : list instr) 
  (i1 i2 : instr_state) 
  (cf : cf_instr) (sp : val),
SeqBB.step ge sp (Iexec i1) 
  (a0 ++ b) (Iterm i2 cf) ->
SeqBB.step ge sp (Iexec i1) a0 (Iterm i2 cf) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp 
     (Iexec i1) a0 (Iexec i1') /\
   SeqBB.step ge sp (Iexec i1') b (Iterm i2 cf))
b: list instr
i1, i2: instr_state
cf: cf_instr
sp: val
state': instr_state
H5: step_instr ge sp (Iexec i1) a (Iexec state')
H7: step_list (step_instr ge) sp 
  (Iexec state') (a0 ++ b) 
  (Iterm i2 cf)
H: SeqBB.step ge sp (Iexec state') a0 (Iterm i2 cf) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp 
     (Iexec state') a0 (Iexec i1') /\
   SeqBB.step ge sp (Iexec i1') b (Iterm i2 cf))
SeqBB.step ge sp (Iexec i1) (a :: a0) (Iterm i2 cf) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp 
     (Iexec i1) (a :: a0) 
     (Iexec i1') /\
   SeqBB.step ge sp (Iexec i1') b (Iterm i2 cf))
A, B: Type
ge: Genv.t A B
a: instr
a0: list instr
IHa: forall (b : list instr) 
  (i1 i2 : instr_state) 
  (cf : cf_instr) (sp : val),
SeqBB.step ge sp (Iexec i1) 
  (a0 ++ b) (Iterm i2 cf) ->
SeqBB.step ge sp (Iexec i1) a0 (Iterm i2 cf) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp 
     (Iexec i1) a0 (Iexec i1') /\
   SeqBB.step ge sp (Iexec i1') b (Iterm i2 cf))
b: list instr
i1, i2: instr_state
cf: cf_instr
sp: val
H3: step_instr ge sp (Iexec i1) a (Iterm i2 cf)
SeqBB.step ge sp (Iexec i1) (a :: a0) (Iterm i2 cf) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp 
     (Iexec i1) (a :: a0) 
     (Iexec i1') /\
   SeqBB.step ge sp (Iexec i1') b (Iterm i2 cf)) inv H.A, B: Type
ge: Genv.t A B
a: instr
a0: list instr
IHa: forall (b : list instr) 
  (i1 i2 : instr_state) 
  (cf : cf_instr) (sp : val),
SeqBB.step ge sp (Iexec i1) 
  (a0 ++ b) (Iterm i2 cf) ->
SeqBB.step ge sp (Iexec i1) a0 (Iterm i2 cf) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp 
     (Iexec i1) a0 (Iexec i1') /\
   SeqBB.step ge sp (Iexec i1') b (Iterm i2 cf))
b: list instr
i1, i2: instr_state
cf: cf_instr
sp: val
state': instr_state
H5: step_instr ge sp (Iexec i1) a (Iexec state')
H7: step_list (step_instr ge) sp 
  (Iexec state') (a0 ++ b) 
  (Iterm i2 cf)
H0: SeqBB.step ge sp (Iexec state') a0 (Iterm i2 cf)
SeqBB.step ge sp (Iexec i1) (a :: a0) (Iterm i2 cf) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp 
     (Iexec i1) (a :: a0) 
     (Iexec i1') /\
   SeqBB.step ge sp (Iexec i1') b (Iterm i2 cf))
A, B: Type
ge: Genv.t A B
a: instr
a0: list instr
IHa: forall (b : list instr) 
  (i1 i2 : instr_state) 
  (cf : cf_instr) (sp : val),
SeqBB.step ge sp (Iexec i1) 
  (a0 ++ b) (Iterm i2 cf) ->
SeqBB.step ge sp (Iexec i1) a0 (Iterm i2 cf) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp 
     (Iexec i1) a0 (Iexec i1') /\
   SeqBB.step ge sp (Iexec i1') b (Iterm i2 cf))
b: list instr
i1, i2: instr_state
cf: cf_instr
sp: val
state': instr_state
H5: step_instr ge sp (Iexec i1) a (Iexec state')
H7: step_list (step_instr ge) sp 
  (Iexec state') (a0 ++ b) 
  (Iterm i2 cf)
H0: exists i1' : instr_state,
  step_list2 (step_instr ge) sp 
    (Iexec state') a0 (Iexec i1') /\
  SeqBB.step ge sp (Iexec i1') b (Iterm i2 cf)
SeqBB.step ge sp (Iexec i1) (a :: a0) (Iterm i2 cf) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp 
     (Iexec i1) (a :: a0) 
     (Iexec i1') /\
   SeqBB.step ge sp (Iexec i1') b (Iterm i2 cf))
A, B: Type
ge: Genv.t A B
a: instr
a0: list instr
IHa: forall (b : list instr) 
  (i1 i2 : instr_state) 
  (cf : cf_instr) (sp : val),
SeqBB.step ge sp (Iexec i1) 
  (a0 ++ b) (Iterm i2 cf) ->
SeqBB.step ge sp (Iexec i1) a0 (Iterm i2 cf) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp 
     (Iexec i1) a0 (Iexec i1') /\
   SeqBB.step ge sp (Iexec i1') b (Iterm i2 cf))
b: list instr
i1, i2: instr_state
cf: cf_instr
sp: val
H3: step_instr ge sp (Iexec i1) a (Iterm i2 cf)
SeqBB.step ge sp (Iexec i1) (a :: a0) (Iterm i2 cf) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp 
     (Iexec i1) (a :: a0) 
     (Iexec i1') /\
   SeqBB.step ge sp (Iexec i1') b (Iterm i2 cf))
  left; econstructor; eauto.A, B: Type
ge: Genv.t A B
a: instr
a0: list instr
IHa: forall (b : list instr) 
  (i1 i2 : instr_state) 
  (cf : cf_instr) (sp : val),
SeqBB.step ge sp (Iexec i1) 
  (a0 ++ b) (Iterm i2 cf) ->
SeqBB.step ge sp (Iexec i1) a0 (Iterm i2 cf) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp 
     (Iexec i1) a0 (Iexec i1') /\
   SeqBB.step ge sp (Iexec i1') b (Iterm i2 cf))
b: list instr
i1, i2: instr_state
cf: cf_instr
sp: val
state': instr_state
H5: step_instr ge sp (Iexec i1) a (Iexec state')
H7: step_list (step_instr ge) sp 
  (Iexec state') (a0 ++ b) 
  (Iterm i2 cf)
H0: exists i1' : instr_state,
  step_list2 (step_instr ge) sp 
    (Iexec state') a0 (Iexec i1') /\
  SeqBB.step ge sp (Iexec i1') b (Iterm i2 cf)
SeqBB.step ge sp (Iexec i1) (a :: a0) (Iterm i2 cf) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp 
     (Iexec i1) (a :: a0) 
     (Iexec i1') /\
   SeqBB.step ge sp (Iexec i1') b (Iterm i2 cf))
A, B: Type
ge: Genv.t A B
a: instr
a0: list instr
IHa: forall (b : list instr) 
  (i1 i2 : instr_state) 
  (cf : cf_instr) (sp : val),
SeqBB.step ge sp (Iexec i1) 
  (a0 ++ b) (Iterm i2 cf) ->
SeqBB.step ge sp (Iexec i1) a0 (Iterm i2 cf) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp 
     (Iexec i1) a0 (Iexec i1') /\
   SeqBB.step ge sp (Iexec i1') b (Iterm i2 cf))
b: list instr
i1, i2: instr_state
cf: cf_instr
sp: val
H3: step_instr ge sp (Iexec i1) a (Iterm i2 cf)
SeqBB.step ge sp (Iexec i1) (a :: a0) (Iterm i2 cf) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp 
     (Iexec i1) (a :: a0) 
     (Iexec i1') /\
   SeqBB.step ge sp (Iexec i1') b (Iterm i2 cf))
  simplify.A, B: Type
ge: Genv.t A B
a: instr
a0: list instr
IHa: forall (b : list instr) 
  (i1 i2 : instr_state) 
  (cf : cf_instr) (sp : val),
SeqBB.step ge sp (Iexec i1) 
  (a0 ++ b) (Iterm i2 cf) ->
SeqBB.step ge sp (Iexec i1) a0 (Iterm i2 cf) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp 
     (Iexec i1) a0 (Iexec i1') /\
   SeqBB.step ge sp (Iexec i1') b (Iterm i2 cf))
b: list instr
i1, i2: instr_state
cf: cf_instr
sp: val
state': instr_state
H5: step_instr ge sp (Iexec i1) a (Iexec state')
H7: step_list (step_instr ge) sp 
  (Iexec state') (a0 ++ b) 
  (Iterm i2 cf)
x: instr_state
H0: step_list2 (step_instr ge) sp 
  (Iexec state') a0 (Iexec x)
H1: SeqBB.step ge sp (Iexec x) b (Iterm i2 cf)
SeqBB.step ge sp (Iexec i1) (a :: a0) (Iterm i2 cf) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp 
     (Iexec i1) (a :: a0) 
     (Iexec i1') /\
   SeqBB.step ge sp (Iexec i1') b (Iterm i2 cf))
A, B: Type
ge: Genv.t A B
a: instr
a0: list instr
IHa: forall (b : list instr) 
  (i1 i2 : instr_state) 
  (cf : cf_instr) (sp : val),
SeqBB.step ge sp (Iexec i1) 
  (a0 ++ b) (Iterm i2 cf) ->
SeqBB.step ge sp (Iexec i1) a0 (Iterm i2 cf) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp 
     (Iexec i1) a0 (Iexec i1') /\
   SeqBB.step ge sp (Iexec i1') b (Iterm i2 cf))
b: list instr
i1, i2: instr_state
cf: cf_instr
sp: val
H3: step_instr ge sp (Iexec i1) a (Iterm i2 cf)
SeqBB.step ge sp (Iexec i1) (a :: a0) (Iterm i2 cf) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp 
     (Iexec i1) (a :: a0) 
     (Iexec i1') /\
   SeqBB.step ge sp (Iexec i1') b (Iterm i2 cf))
  right.A, B: Type
ge: Genv.t A B
a: instr
a0: list instr
IHa: forall (b : list instr) 
  (i1 i2 : instr_state) 
  (cf : cf_instr) (sp : val),
SeqBB.step ge sp (Iexec i1) 
  (a0 ++ b) (Iterm i2 cf) ->
SeqBB.step ge sp (Iexec i1) a0 (Iterm i2 cf) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp 
     (Iexec i1) a0 (Iexec i1') /\
   SeqBB.step ge sp (Iexec i1') b (Iterm i2 cf))
b: list instr
i1, i2: instr_state
cf: cf_instr
sp: val
state': instr_state
H5: step_instr ge sp (Iexec i1) a (Iexec state')
H7: step_list (step_instr ge) sp 
  (Iexec state') (a0 ++ b) 
  (Iterm i2 cf)
x: instr_state
H0: step_list2 (step_instr ge) sp 
  (Iexec state') a0 (Iexec x)
H1: SeqBB.step ge sp (Iexec x) b (Iterm i2 cf)
exists i1' : instr_state,
  step_list2 (step_instr ge) sp 
    (Iexec i1) (a :: a0) 
    (Iexec i1') /\
  SeqBB.step ge sp (Iexec i1') b (Iterm i2 cf)
A, B: Type
ge: Genv.t A B
a: instr
a0: list instr
IHa: forall (b : list instr) 
  (i1 i2 : instr_state) 
  (cf : cf_instr) (sp : val),
SeqBB.step ge sp (Iexec i1) 
  (a0 ++ b) (Iterm i2 cf) ->
SeqBB.step ge sp (Iexec i1) a0 (Iterm i2 cf) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp 
     (Iexec i1) a0 (Iexec i1') /\
   SeqBB.step ge sp (Iexec i1') b (Iterm i2 cf))
b: list instr
i1, i2: instr_state
cf: cf_instr
sp: val
H3: step_instr ge sp (Iexec i1) a (Iterm i2 cf)
SeqBB.step ge sp (Iexec i1) (a :: a0) (Iterm i2 cf) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp 
     (Iexec i1) (a :: a0) 
     (Iexec i1') /\
   SeqBB.step ge sp (Iexec i1') b (Iterm i2 cf)) eexists; split; eauto.A, B: Type
ge: Genv.t A B
a: instr
a0: list instr
IHa: forall (b : list instr) 
  (i1 i2 : instr_state) 
  (cf : cf_instr) (sp : val),
SeqBB.step ge sp (Iexec i1) 
  (a0 ++ b) (Iterm i2 cf) ->
SeqBB.step ge sp (Iexec i1) a0 (Iterm i2 cf) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp 
     (Iexec i1) a0 (Iexec i1') /\
   SeqBB.step ge sp (Iexec i1') b (Iterm i2 cf))
b: list instr
i1, i2: instr_state
cf: cf_instr
sp: val
state': instr_state
H5: step_instr ge sp (Iexec i1) a (Iexec state')
H7: step_list (step_instr ge) sp 
  (Iexec state') (a0 ++ b) 
  (Iterm i2 cf)
x: instr_state
H0: step_list2 (step_instr ge) sp 
  (Iexec state') a0 (Iexec x)
H1: SeqBB.step ge sp (Iexec x) b (Iterm i2 cf)
step_list2 (step_instr ge) sp 
  (Iexec i1) (a :: a0) (Iexec x)
A, B: Type
ge: Genv.t A B
a: instr
a0: list instr
IHa: forall (b : list instr) 
  (i1 i2 : instr_state) 
  (cf : cf_instr) (sp : val),
SeqBB.step ge sp (Iexec i1) 
  (a0 ++ b) (Iterm i2 cf) ->
SeqBB.step ge sp (Iexec i1) a0 (Iterm i2 cf) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp 
     (Iexec i1) a0 (Iexec i1') /\
   SeqBB.step ge sp (Iexec i1') b (Iterm i2 cf))
b: list instr
i1, i2: instr_state
cf: cf_instr
sp: val
H3: step_instr ge sp (Iexec i1) a (Iterm i2 cf)
SeqBB.step ge sp (Iexec i1) (a :: a0) (Iterm i2 cf) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp 
     (Iexec i1) (a :: a0) 
     (Iexec i1') /\
   SeqBB.step ge sp (Iexec i1') b (Iterm i2 cf)) econstructor; eauto.A, B: Type
ge: Genv.t A B
a: instr
a0: list instr
IHa: forall (b : list instr) 
  (i1 i2 : instr_state) 
  (cf : cf_instr) (sp : val),
SeqBB.step ge sp (Iexec i1) 
  (a0 ++ b) (Iterm i2 cf) ->
SeqBB.step ge sp (Iexec i1) a0 (Iterm i2 cf) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp 
     (Iexec i1) a0 (Iexec i1') /\
   SeqBB.step ge sp (Iexec i1') b (Iterm i2 cf))
b: list instr
i1, i2: instr_state
cf: cf_instr
sp: val
H3: step_instr ge sp (Iexec i1) a (Iterm i2 cf)
SeqBB.step ge sp (Iexec i1) (a :: a0) (Iterm i2 cf) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp 
     (Iexec i1) (a :: a0) 
     (Iexec i1') /\
   SeqBB.step ge sp (Iexec i1') b (Iterm i2 cf))
  left.A, B: Type
ge: Genv.t A B
a: instr
a0: list instr
IHa: forall (b : list instr) 
  (i1 i2 : instr_state) 
  (cf : cf_instr) (sp : val),
SeqBB.step ge sp (Iexec i1) 
  (a0 ++ b) (Iterm i2 cf) ->
SeqBB.step ge sp (Iexec i1) a0 (Iterm i2 cf) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp 
     (Iexec i1) a0 (Iexec i1') /\
   SeqBB.step ge sp (Iexec i1') b (Iterm i2 cf))
b: list instr
i1, i2: instr_state
cf: cf_instr
sp: val
H3: step_instr ge sp (Iexec i1) a (Iterm i2 cf)
SeqBB.step ge sp (Iexec i1) (a :: a0) (Iterm i2 cf) constructor; eauto.
Qed.

Lemma step_options2' :
  forall A B (ge: Genv.t A B) a b i1 i2 sp,
    step_list2 (step_instr ge) sp (Iexec i1) (a ++ b) (Iexec i2) ->
    (step_list2 (step_instr ge) sp (Iexec i1) a (Iexec i2) \/
       exists i1', step_list2 (step_instr ge) sp (Iexec i1) a (Iexec i1')
              /\ step_list2 (step_instr ge) sp (Iexec i1') b (Iexec i2)).forall (A B : Type) (ge : Genv.t A B)
  (a b : list instr) (i1 i2 : instr_state) (sp : val),
step_list2 (step_instr ge) sp (Iexec i1) (a ++ b)
  (Iexec i2) ->
step_list2 (step_instr ge) sp (Iexec i1) a (Iexec i2) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp (Iexec i1) a
     (Iexec i1') /\
   step_list2 (step_instr ge) sp (Iexec i1') b
     (Iexec i2))
Proof.forall (A B : Type) (ge : Genv.t A B)
  (a b : list instr) (i1 i2 : instr_state) (sp : val),
step_list2 (step_instr ge) sp (Iexec i1) (a ++ b)
  (Iexec i2) ->
step_list2 (step_instr ge) sp (Iexec i1) a (Iexec i2) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp (Iexec i1) a
     (Iexec i1') /\
   step_list2 (step_instr ge) sp (Iexec i1') b
     (Iexec i2))
  induction a; crush.A, B: Type
ge: Genv.t A B
b: list instr
i1, i2: instr_state
sp: val
H: step_list2 (step_instr ge) sp (Iexec i1) b
  (Iexec i2)
step_list2 (step_instr ge) sp (Iexec i1) nil
  (Iexec i2) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp (Iexec i1) nil
     (Iexec i1') /\
   step_list2 (step_instr ge) sp (Iexec i1') b
     (Iexec i2))
A, B: Type
ge: Genv.t A B
a: instr
a0: list instr
IHa: forall (b : list instr) (i1 i2 : instr_state) (sp : val),
step_list2 (step_instr ge) sp (Iexec i1) (a0 ++ b) (Iexec i2) ->
step_list2 (step_instr ge) sp (Iexec i1) a0 (Iexec i2) \/
(exists i1' : instr_state,
step_list2 (step_instr ge) sp (Iexec i1) a0 (Iexec i1') /\
step_list2 (step_instr ge) sp (Iexec i1') b (Iexec i2))
b: list instr
i1, i2: instr_state
sp: val
H: step_list2 (step_instr ge) sp (Iexec i1)
  (a :: a0 ++ b) (Iexec i2)
step_list2 (step_instr ge) sp (Iexec i1) (a :: a0)
  (Iexec i2) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp (Iexec i1) (a :: a0)
     (Iexec i1') /\
   step_list2 (step_instr ge) sp (Iexec i1') b
     (Iexec i2)) right; eexists; split; [constructor|auto].A, B: Type
ge: Genv.t A B
a: instr
a0: list instr
IHa: forall (b : list instr) (i1 i2 : instr_state) (sp : val),
step_list2 (step_instr ge) sp (Iexec i1) (a0 ++ b) (Iexec i2) ->
step_list2 (step_instr ge) sp (Iexec i1) a0 (Iexec i2) \/
(exists i1' : instr_state,
step_list2 (step_instr ge) sp (Iexec i1) a0 (Iexec i1') /\
step_list2 (step_instr ge) sp (Iexec i1') b (Iexec i2))
b: list instr
i1, i2: instr_state
sp: val
H: step_list2 (step_instr ge) sp (Iexec i1)
  (a :: a0 ++ b) (Iexec i2)
step_list2 (step_instr ge) sp (Iexec i1) (a :: a0)
  (Iexec i2) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp (Iexec i1) (a :: a0)
     (Iexec i1') /\
   step_list2 (step_instr ge) sp (Iexec i1') b
     (Iexec i2))
  inv H.A, B: Type
ge: Genv.t A B
a: instr
a0: list instr
IHa: forall (b : list instr) (i1 i2 : instr_state) (sp : val),
step_list2 (step_instr ge) sp (Iexec i1) (a0 ++ b) (Iexec i2) ->
step_list2 (step_instr ge) sp (Iexec i1) a0 (Iexec i2) \/
(exists i1' : instr_state,
step_list2 (step_instr ge) sp (Iexec i1) a0 (Iexec i1') /\
step_list2 (step_instr ge) sp (Iexec i1') b (Iexec i2))
b: list instr
i1, i2: instr_state
sp: val
i3: istate
H4: step_instr ge sp (Iexec i1) a i3
H6: step_list2 (step_instr ge) sp i3 (a0 ++ b)
  (Iexec i2)
step_list2 (step_instr ge) sp (Iexec i1) (a :: a0)
  (Iexec i2) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp (Iexec i1) (a :: a0)
     (Iexec i1') /\
   step_list2 (step_instr ge) sp (Iexec i1') b
     (Iexec i2)) destruct i3; [|exfalso; eapply step_list2_false; eauto].A, B: Type
ge: Genv.t A B
a: instr
a0: list instr
IHa: forall (b : list instr) (i1 i2 : instr_state) (sp : val),
step_list2 (step_instr ge) sp (Iexec i1) (a0 ++ b) (Iexec i2) ->
step_list2 (step_instr ge) sp (Iexec i1) a0 (Iexec i2) \/
(exists i1' : instr_state,
step_list2 (step_instr ge) sp (Iexec i1) a0 (Iexec i1') /\
step_list2 (step_instr ge) sp (Iexec i1') b (Iexec i2))
b: list instr
i1, i2: instr_state
sp: val
i: instr_state
H4: step_instr ge sp (Iexec i1) a (Iexec i)
H6: step_list2 (step_instr ge) sp (Iexec i) (a0 ++ b)
  (Iexec i2)
step_list2 (step_instr ge) sp (Iexec i1) (a :: a0)
  (Iexec i2) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp (Iexec i1) (a :: a0)
     (Iexec i1') /\
   step_list2 (step_instr ge) sp (Iexec i1') b
     (Iexec i2)) exploit IHa; eauto; intros.A, B: Type
ge: Genv.t A B
a: instr
a0: list instr
IHa: forall (b : list instr) (i1 i2 : instr_state) (sp : val),
step_list2 (step_instr ge) sp (Iexec i1) (a0 ++ b) (Iexec i2) ->
step_list2 (step_instr ge) sp (Iexec i1) a0 (Iexec i2) \/
(exists i1' : instr_state,
step_list2 (step_instr ge) sp (Iexec i1) a0 (Iexec i1') /\
step_list2 (step_instr ge) sp (Iexec i1') b (Iexec i2))
b: list instr
i1, i2: instr_state
sp: val
i: instr_state
H4: step_instr ge sp (Iexec i1) a (Iexec i)
H6: step_list2 (step_instr ge) sp (Iexec i) (a0 ++ b)
  (Iexec i2)
H: step_list2 (step_instr ge) sp (Iexec i) a0
  (Iexec i2) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp (Iexec i) a0
     (Iexec i1') /\
   step_list2 (step_instr ge) sp (Iexec i1') b
     (Iexec i2))
step_list2 (step_instr ge) sp (Iexec i1) (a :: a0)
  (Iexec i2) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp (Iexec i1) (a :: a0)
     (Iexec i1') /\
   step_list2 (step_instr ge) sp (Iexec i1') b
     (Iexec i2)) inv H.A, B: Type
ge: Genv.t A B
a: instr
a0: list instr
IHa: forall (b : list instr) (i1 i2 : instr_state) (sp : val),
step_list2 (step_instr ge) sp (Iexec i1) (a0 ++ b) (Iexec i2) ->
step_list2 (step_instr ge) sp (Iexec i1) a0 (Iexec i2) \/
(exists i1' : instr_state,
step_list2 (step_instr ge) sp (Iexec i1) a0 (Iexec i1') /\
step_list2 (step_instr ge) sp (Iexec i1') b (Iexec i2))
b: list instr
i1, i2: instr_state
sp: val
i: instr_state
H4: step_instr ge sp (Iexec i1) a (Iexec i)
H6: step_list2 (step_instr ge) sp (Iexec i) (a0 ++ b)
  (Iexec i2)
H0: step_list2 (step_instr ge) sp (Iexec i) a0
  (Iexec i2)
step_list2 (step_instr ge) sp (Iexec i1) (a :: a0)
  (Iexec i2) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp (Iexec i1) (a :: a0)
     (Iexec i1') /\
   step_list2 (step_instr ge) sp (Iexec i1') b
     (Iexec i2))
A, B: Type
ge: Genv.t A B
a: instr
a0: list instr
IHa: forall (b : list instr) (i1 i2 : instr_state) (sp : val),
step_list2 (step_instr ge) sp (Iexec i1) (a0 ++ b) (Iexec i2) ->
step_list2 (step_instr ge) sp (Iexec i1) a0 (Iexec i2) \/
(exists i1' : instr_state,
step_list2 (step_instr ge) sp (Iexec i1) a0 (Iexec i1') /\
step_list2 (step_instr ge) sp (Iexec i1') b (Iexec i2))
b: list instr
i1, i2: instr_state
sp: val
i: instr_state
H4: step_instr ge sp (Iexec i1) a (Iexec i)
H6: step_list2 (step_instr ge) sp (Iexec i) (a0 ++ b)
  (Iexec i2)
H0: exists i1' : instr_state,
  step_list2 (step_instr ge) sp (Iexec i) a0
    (Iexec i1') /\
  step_list2 (step_instr ge) sp (Iexec i1') b
    (Iexec i2)
step_list2 (step_instr ge) sp (Iexec i1) (a :: a0)
  (Iexec i2) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp (Iexec i1) (a :: a0)
     (Iexec i1') /\
   step_list2 (step_instr ge) sp (Iexec i1') b
     (Iexec i2))
  left; econstructor; eauto.A, B: Type
ge: Genv.t A B
a: instr
a0: list instr
IHa: forall (b : list instr) (i1 i2 : instr_state) (sp : val),
step_list2 (step_instr ge) sp (Iexec i1) (a0 ++ b) (Iexec i2) ->
step_list2 (step_instr ge) sp (Iexec i1) a0 (Iexec i2) \/
(exists i1' : instr_state,
step_list2 (step_instr ge) sp (Iexec i1) a0 (Iexec i1') /\
step_list2 (step_instr ge) sp (Iexec i1') b (Iexec i2))
b: list instr
i1, i2: instr_state
sp: val
i: instr_state
H4: step_instr ge sp (Iexec i1) a (Iexec i)
H6: step_list2 (step_instr ge) sp (Iexec i) (a0 ++ b)
  (Iexec i2)
H0: exists i1' : instr_state,
  step_list2 (step_instr ge) sp (Iexec i) a0
    (Iexec i1') /\
  step_list2 (step_instr ge) sp (Iexec i1') b
    (Iexec i2)
step_list2 (step_instr ge) sp (Iexec i1) (a :: a0)
  (Iexec i2) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp (Iexec i1) (a :: a0)
     (Iexec i1') /\
   step_list2 (step_instr ge) sp (Iexec i1') b
     (Iexec i2))
  simplify.A, B: Type
ge: Genv.t A B
a: instr
a0: list instr
IHa: forall (b : list instr) (i1 i2 : instr_state) (sp : val),
step_list2 (step_instr ge) sp (Iexec i1) (a0 ++ b) (Iexec i2) ->
step_list2 (step_instr ge) sp (Iexec i1) a0 (Iexec i2) \/
(exists i1' : instr_state,
step_list2 (step_instr ge) sp (Iexec i1) a0 (Iexec i1') /\
step_list2 (step_instr ge) sp (Iexec i1') b (Iexec i2))
b: list instr
i1, i2: instr_state
sp: val
i: instr_state
H4: step_instr ge sp (Iexec i1) a (Iexec i)
H6: step_list2 (step_instr ge) sp (Iexec i) (a0 ++ b)
  (Iexec i2)
x: instr_state
H0: step_list2 (step_instr ge) sp (Iexec i) a0
  (Iexec x)
H1: step_list2 (step_instr ge) sp (Iexec x) b
  (Iexec i2)
step_list2 (step_instr ge) sp (Iexec i1) (a :: a0)
  (Iexec i2) \/
(exists i1' : instr_state,
   step_list2 (step_instr ge) sp (Iexec i1) (a :: a0)
     (Iexec i1') /\
   step_list2 (step_instr ge) sp (Iexec i1') b
     (Iexec i2))
  right.A, B: Type
ge: Genv.t A B
a: instr
a0: list instr
IHa: forall (b : list instr) (i1 i2 : instr_state) (sp : val),
step_list2 (step_instr ge) sp (Iexec i1) (a0 ++ b) (Iexec i2) ->
step_list2 (step_instr ge) sp (Iexec i1) a0 (Iexec i2) \/
(exists i1' : instr_state,
step_list2 (step_instr ge) sp (Iexec i1) a0 (Iexec i1') /\
step_list2 (step_instr ge) sp (Iexec i1') b (Iexec i2))
b: list instr
i1, i2: instr_state
sp: val
i: instr_state
H4: step_instr ge sp (Iexec i1) a (Iexec i)
H6: step_list2 (step_instr ge) sp (Iexec i) (a0 ++ b)
  (Iexec i2)
x: instr_state
H0: step_list2 (step_instr ge) sp (Iexec i) a0
  (Iexec x)
H1: step_list2 (step_instr ge) sp (Iexec x) b
  (Iexec i2)
exists i1' : instr_state,
  step_list2 (step_instr ge) sp (Iexec i1) (a :: a0)
    (Iexec i1') /\
  step_list2 (step_instr ge) sp (Iexec i1') b
    (Iexec i2) eexists; split; eauto.A, B: Type
ge: Genv.t A B
a: instr
a0: list instr
IHa: forall (b : list instr) (i1 i2 : instr_state) (sp : val),
step_list2 (step_instr ge) sp (Iexec i1) (a0 ++ b) (Iexec i2) ->
step_list2 (step_instr ge) sp (Iexec i1) a0 (Iexec i2) \/
(exists i1' : instr_state,
step_list2 (step_instr ge) sp (Iexec i1) a0 (Iexec i1') /\
step_list2 (step_instr ge) sp (Iexec i1') b (Iexec i2))
b: list instr
i1, i2: instr_state
sp: val
i: instr_state
H4: step_instr ge sp (Iexec i1) a (Iexec i)
H6: step_list2 (step_instr ge) sp (Iexec i) (a0 ++ b)
  (Iexec i2)
x: instr_state
H0: step_list2 (step_instr ge) sp (Iexec i) a0
  (Iexec x)
H1: step_list2 (step_instr ge) sp (Iexec x) b
  (Iexec i2)
step_list2 (step_instr ge) sp (Iexec i1) (a :: a0)
  (Iexec x) econstructor; eauto.
Qed.

Lemma step_options2 :
  forall A B (ge: Genv.t A B) a b i1 i2 sp,
    step_list2 (step_instr ge) sp (Iexec i1) (a ++ b) (Iexec i2) ->
    exists i', step_list2 (step_instr ge) sp (Iexec i1) a (Iexec i')
          /\ step_list2 (step_instr ge) sp (Iexec i') b (Iexec i2).forall (A B : Type) (ge : Genv.t A B)
  (a b : list instr) (i1 i2 : instr_state) (sp : val),
step_list2 (step_instr ge) sp (Iexec i1) (a ++ b)
  (Iexec i2) ->
exists i' : instr_state,
  step_list2 (step_instr ge) sp (Iexec i1) a
    (Iexec i') /\
  step_list2 (step_instr ge) sp (Iexec i') b
    (Iexec i2)
Proof.forall (A B : Type) (ge : Genv.t A B)
  (a b : list instr) (i1 i2 : instr_state) (sp : val),
step_list2 (step_instr ge) sp (Iexec i1) (a ++ b)
  (Iexec i2) ->
exists i' : instr_state,
  step_list2 (step_instr ge) sp (Iexec i1) a
    (Iexec i') /\
  step_list2 (step_instr ge) sp (Iexec i') b
    (Iexec i2)
  induction a; crush.A, B: Type
ge: Genv.t A B
b: list instr
i1, i2: instr_state
sp: val
H: step_list2 (step_instr ge) sp (Iexec i1) b
  (Iexec i2)
exists i' : instr_state,
  step_list2 (step_instr ge) sp (Iexec i1) nil
    (Iexec i') /\
  step_list2 (step_instr ge) sp (Iexec i') b
    (Iexec i2)
A, B: Type
ge: Genv.t A B
a: instr
a0: list instr
IHa: forall (b : list instr) (i1 i2 : instr_state) (sp : val),
step_list2 (step_instr ge) sp (Iexec i1) (a0 ++ b) (Iexec i2) ->
exists i' : instr_state,
step_list2 (step_instr ge) sp (Iexec i1) a0 (Iexec i') /\
step_list2 (step_instr ge) sp (Iexec i') b (Iexec i2)
b: list instr
i1, i2: instr_state
sp: val
H: step_list2 (step_instr ge) sp (Iexec i1)
  (a :: a0 ++ b) (Iexec i2)
exists i' : instr_state,
  step_list2 (step_instr ge) sp (Iexec i1) (a :: a0)
    (Iexec i') /\
  step_list2 (step_instr ge) sp (Iexec i') b
    (Iexec i2) eexists; split; eauto.A, B: Type
ge: Genv.t A B
b: list instr
i1, i2: instr_state
sp: val
H: step_list2 (step_instr ge) sp (Iexec i1) b
  (Iexec i2)
step_list2 (step_instr ge) sp (Iexec i1) nil
  (Iexec i1)
A, B: Type
ge: Genv.t A B
a: instr
a0: list instr
IHa: forall (b : list instr) (i1 i2 : instr_state) (sp : val),
step_list2 (step_instr ge) sp (Iexec i1) (a0 ++ b) (Iexec i2) ->
exists i' : instr_state,
step_list2 (step_instr ge) sp (Iexec i1) a0 (Iexec i') /\
step_list2 (step_instr ge) sp (Iexec i') b (Iexec i2)
b: list instr
i1, i2: instr_state
sp: val
H: step_list2 (step_instr ge) sp (Iexec i1)
  (a :: a0 ++ b) (Iexec i2)
exists i' : instr_state,
  step_list2 (step_instr ge) sp (Iexec i1) (a :: a0)
    (Iexec i') /\
  step_list2 (step_instr ge) sp (Iexec i') b
    (Iexec i2)
  constructor.A, B: Type
ge: Genv.t A B
a: instr
a0: list instr
IHa: forall (b : list instr) (i1 i2 : instr_state) (sp : val),
step_list2 (step_instr ge) sp (Iexec i1) (a0 ++ b) (Iexec i2) ->
exists i' : instr_state,
step_list2 (step_instr ge) sp (Iexec i1) a0 (Iexec i') /\
step_list2 (step_instr ge) sp (Iexec i') b (Iexec i2)
b: list instr
i1, i2: instr_state
sp: val
H: step_list2 (step_instr ge) sp (Iexec i1)
  (a :: a0 ++ b) (Iexec i2)
exists i' : instr_state,
  step_list2 (step_instr ge) sp (Iexec i1) (a :: a0)
    (Iexec i') /\
  step_list2 (step_instr ge) sp (Iexec i') b
    (Iexec i2)
  inv H.A, B: Type
ge: Genv.t A B
a: instr
a0: list instr
IHa: forall (b : list instr) (i1 i2 : instr_state) (sp : val),
step_list2 (step_instr ge) sp (Iexec i1) (a0 ++ b) (Iexec i2) ->
exists i' : instr_state,
step_list2 (step_instr ge) sp (Iexec i1) a0 (Iexec i') /\
step_list2 (step_instr ge) sp (Iexec i') b (Iexec i2)
b: list instr
i1, i2: instr_state
sp: val
i3: istate
H4: step_instr ge sp (Iexec i1) a i3
H6: step_list2 (step_instr ge) sp i3 (a0 ++ b)
  (Iexec i2)
exists i' : instr_state,
  step_list2 (step_instr ge) sp (Iexec i1) (a :: a0)
    (Iexec i') /\
  step_list2 (step_instr ge) sp (Iexec i') b
    (Iexec i2) destruct i3; [|exfalso; eapply step_list2_false; eauto].A, B: Type
ge: Genv.t A B
a: instr
a0: list instr
IHa: forall (b : list instr) (i1 i2 : instr_state) (sp : val),
step_list2 (step_instr ge) sp (Iexec i1) (a0 ++ b) (Iexec i2) ->
exists i' : instr_state,
step_list2 (step_instr ge) sp (Iexec i1) a0 (Iexec i') /\
step_list2 (step_instr ge) sp (Iexec i') b (Iexec i2)
b: list instr
i1, i2: instr_state
sp: val
i: instr_state
H4: step_instr ge sp (Iexec i1) a (Iexec i)
H6: step_list2 (step_instr ge) sp (Iexec i) (a0 ++ b)
  (Iexec i2)
exists i' : instr_state,
  step_list2 (step_instr ge) sp (Iexec i1) (a :: a0)
    (Iexec i') /\
  step_list2 (step_instr ge) sp (Iexec i') b
    (Iexec i2)
  exploit IHa; eauto; simplify.A, B: Type
ge: Genv.t A B
a: instr
a0: list instr
IHa: forall (b : list instr) (i1 i2 : instr_state) (sp : val),
step_list2 (step_instr ge) sp (Iexec i1) (a0 ++ b) (Iexec i2) ->
exists i' : instr_state,
step_list2 (step_instr ge) sp (Iexec i1) a0 (Iexec i') /\
step_list2 (step_instr ge) sp (Iexec i') b (Iexec i2)
b: list instr
i1, i2: instr_state
sp: val
i: instr_state
H4: step_instr ge sp (Iexec i1) a (Iexec i)
H6: step_list2 (step_instr ge) sp (Iexec i) (a0 ++ b)
  (Iexec i2)
x: instr_state
H: step_list2 (step_instr ge) sp (Iexec i) a0
  (Iexec x)
H1: step_list2 (step_instr ge) sp (Iexec x) b
  (Iexec i2)
exists i' : instr_state,
  step_list2 (step_instr ge) sp (Iexec i1) (a :: a0)
    (Iexec i') /\
  step_list2 (step_instr ge) sp (Iexec i') b
    (Iexec i2)
  eexists; split; eauto.A, B: Type
ge: Genv.t A B
a: instr
a0: list instr
IHa: forall (b : list instr) (i1 i2 : instr_state) (sp : val),
step_list2 (step_instr ge) sp (Iexec i1) (a0 ++ b) (Iexec i2) ->
exists i' : instr_state,
step_list2 (step_instr ge) sp (Iexec i1) a0 (Iexec i') /\
step_list2 (step_instr ge) sp (Iexec i') b (Iexec i2)
b: list instr
i1, i2: instr_state
sp: val
i: instr_state
H4: step_instr ge sp (Iexec i1) a (Iexec i)
H6: step_list2 (step_instr ge) sp (Iexec i) (a0 ++ b)
  (Iexec i2)
x: instr_state
H: step_list2 (step_instr ge) sp (Iexec i) a0
  (Iexec x)
H1: step_list2 (step_instr ge) sp (Iexec x) b
  (Iexec i2)
step_list2 (step_instr ge) sp (Iexec i1) (a :: a0)
  (Iexec x) econstructor; eauto.
Qed.

Lemma step_instr_unchanged_state :
  forall A (ge: Genv.t A unit) sp r st st' cf,
    step_instr ge sp (Iexec st) r (Iterm st' cf) -> st = st'.forall (A : Type) (ge : Genv.t A unit) (sp : val)
  (r : instr) (st st' : instr_state) (cf : cf_instr),
step_instr ge sp (Iexec st) r (Iterm st' cf) ->
st = st'
Proof.forall (A : Type) (ge : Genv.t A unit) (sp : val)
  (r : instr) (st st' : instr_state) (cf : cf_instr),
step_instr ge sp (Iexec st) r (Iterm st' cf) ->
st = st' intros.A: Type
ge: Genv.t A unit
sp: val
r: instr
st, st': instr_state
cf: cf_instr
H: step_instr ge sp (Iexec st) r (Iterm st' cf)
st = st' inv H; auto. Qed.

Lemma step_exists:
  forall A (ge: Genv.t A unit) sp instrs i i' ti cf,
    SeqBB.step ge sp (Iexec i) instrs (Iterm i' cf) ->
    state_equiv i ti ->
    exists ti',
      SeqBB.step ge sp (Iexec ti) instrs (Iterm ti' cf)
      /\ state_equiv i' ti'.forall (A : Type) (ge : Genv.t A unit) (sp : val)
  (instrs : list instr) (i i' ti : instr_state)
  (cf : cf_instr),
SeqBB.step ge sp (Iexec i) instrs (Iterm i' cf) ->
state_equiv i ti ->
exists ti' : instr_state,
  SeqBB.step ge sp (Iexec ti) instrs (Iterm ti' cf) /\
  state_equiv i' ti'
Proof.forall (A : Type) (ge : Genv.t A unit) (sp : val)
  (instrs : list instr) (i i' ti : instr_state)
  (cf : cf_instr),
SeqBB.step ge sp (Iexec i) instrs (Iterm i' cf) ->
state_equiv i ti ->
exists ti' : instr_state,
  SeqBB.step ge sp (Iexec ti) instrs (Iterm ti' cf) /\
  state_equiv i' ti'
  induction instrs.A: Type
ge: Genv.t A unit
sp: val
forall (i i' ti : instr_state) (cf : cf_instr),
SeqBB.step ge sp (Iexec i) nil (Iterm i' cf) ->
state_equiv i ti ->
exists ti' : instr_state,
  SeqBB.step ge sp (Iexec ti) nil (Iterm ti' cf) /\
  state_equiv i' ti'
A: Type
ge: Genv.t A unit
sp: val
a: instr
instrs: list instr
IHinstrs: forall (i i' ti : instr_state)
  (cf : cf_instr),
SeqBB.step ge sp (Iexec i) instrs
  (Iterm i' cf) ->
state_equiv i ti ->
exists ti' : instr_state,
  SeqBB.step ge sp (Iexec ti) instrs
    (Iterm ti' cf) /\ state_equiv i' ti'
forall (i i' ti : instr_state) (cf : cf_instr),
SeqBB.step ge sp (Iexec i) (a :: instrs) (Iterm i' cf) ->
state_equiv i ti ->
exists ti' : instr_state,
  SeqBB.step ge sp (Iexec ti) (a :: instrs)
    (Iterm ti' cf) /\ state_equiv i' ti'
  -A: Type
ge: Genv.t A unit
sp: val
forall (i i' ti : instr_state) (cf : cf_instr),
SeqBB.step ge sp (Iexec i) nil (Iterm i' cf) ->
state_equiv i ti ->
exists ti' : instr_state,
  SeqBB.step ge sp (Iexec ti) nil (Iterm ti' cf) /\
  state_equiv i' ti' intros.A: Type
ge: Genv.t A unit
sp: val
i, i', ti: instr_state
cf: cf_instr
H: SeqBB.step ge sp (Iexec i) nil (Iterm i' cf)
H0: state_equiv i ti
exists ti' : instr_state,
  SeqBB.step ge sp (Iexec ti) nil (Iterm ti' cf) /\
  state_equiv i' ti' inv H.
  -A: Type
ge: Genv.t A unit
sp: val
a: instr
instrs: list instr
IHinstrs: forall (i i' ti : instr_state)
  (cf : cf_instr),
SeqBB.step ge sp (Iexec i) instrs
  (Iterm i' cf) ->
state_equiv i ti ->
exists ti' : instr_state,
  SeqBB.step ge sp (Iexec ti) instrs
    (Iterm ti' cf) /\ state_equiv i' ti'
forall (i i' ti : instr_state) (cf : cf_instr),
SeqBB.step ge sp (Iexec i) (a :: instrs) (Iterm i' cf) ->
state_equiv i ti ->
exists ti' : instr_state,
  SeqBB.step ge sp (Iexec ti) 
    (a :: instrs) (Iterm ti' cf) /\ 
  state_equiv i' ti' intros.A: Type
ge: Genv.t A unit
sp: val
a: instr
instrs: list instr
IHinstrs: forall (i i' ti : instr_state)
  (cf : cf_instr),
SeqBB.step ge sp (Iexec i) instrs
  (Iterm i' cf) ->
state_equiv i ti ->
exists ti' : instr_state,
  SeqBB.step ge sp (Iexec ti) instrs
    (Iterm ti' cf) /\ state_equiv i' ti'
i, i', ti: instr_state
cf: cf_instr
H: SeqBB.step ge sp (Iexec i) 
  (a :: instrs) (Iterm i' cf)
H0: state_equiv i ti
exists ti' : instr_state,
  SeqBB.step ge sp (Iexec ti) 
    (a :: instrs) (Iterm ti' cf) /\ 
  state_equiv i' ti' inv H.A: Type
ge: Genv.t A unit
sp: val
a: instr
instrs: list instr
IHinstrs: forall (i i' ti : instr_state)
  (cf : cf_instr),
SeqBB.step ge sp (Iexec i) instrs
  (Iterm i' cf) ->
state_equiv i ti ->
exists ti' : instr_state,
  SeqBB.step ge sp (Iexec ti) instrs
    (Iterm ti' cf) /\ state_equiv i' ti'
i, i', ti: instr_state
cf: cf_instr
H0: state_equiv i ti
state': instr_state
H6: step_instr ge sp (Iexec i) a (Iexec state')
H8: step_list (step_instr ge) sp 
  (Iexec state') instrs 
  (Iterm i' cf)
exists ti' : instr_state,
  SeqBB.step ge sp (Iexec ti) 
    (a :: instrs) (Iterm ti' cf) /\ 
  state_equiv i' ti'
A: Type
ge: Genv.t A unit
sp: val
a: instr
instrs: list instr
IHinstrs: forall (i i' ti : instr_state)
  (cf : cf_instr),
SeqBB.step ge sp (Iexec i) instrs
  (Iterm i' cf) ->
state_equiv i ti ->
exists ti' : instr_state,
  SeqBB.step ge sp (Iexec ti) instrs
    (Iterm ti' cf) /\ state_equiv i' ti'
i, i', ti: instr_state
cf: cf_instr
H0: state_equiv i ti
H4: step_instr ge sp (Iexec i) a (Iterm i' cf)
exists ti' : instr_state,
  SeqBB.step ge sp (Iexec ti) 
    (a :: instrs) (Iterm ti' cf) /\ 
  state_equiv i' ti'
    +A: Type
ge: Genv.t A unit
sp: val
a: instr
instrs: list instr
IHinstrs: forall (i i' ti : instr_state)
  (cf : cf_instr),
SeqBB.step ge sp (Iexec i) instrs
  (Iterm i' cf) ->
state_equiv i ti ->
exists ti' : instr_state,
  SeqBB.step ge sp (Iexec ti) instrs
    (Iterm ti' cf) /\ state_equiv i' ti'
i, i', ti: instr_state
cf: cf_instr
H0: state_equiv i ti
state': instr_state
H6: step_instr ge sp (Iexec i) a (Iexec state')
H8: step_list (step_instr ge) sp 
  (Iexec state') instrs 
  (Iterm i' cf)
exists ti' : instr_state,
  SeqBB.step ge sp (Iexec ti) 
    (a :: instrs) (Iterm ti' cf) /\ 
  state_equiv i' ti' exploit (@step_exists A); eauto; simplify.A: Type
ge: Genv.t A unit
sp: val
a: instr
instrs: list instr
IHinstrs: forall (i i' ti : instr_state)
  (cf : cf_instr),
SeqBB.step ge sp (Iexec i) instrs
  (Iterm i' cf) ->
state_equiv i ti ->
exists ti' : instr_state,
  SeqBB.step ge sp (Iexec ti) instrs
    (Iterm ti' cf) /\ state_equiv i' ti'
i, i', ti: instr_state
cf: cf_instr
H0: state_equiv i ti
state': instr_state
H6: step_instr ge sp (Iexec i) a (Iexec state')
H8: step_list (step_instr ge) sp 
  (Iexec state') instrs 
  (Iterm i' cf)
x: instr_state
H: step_instr ge sp (Iexec ti) a (Iexec x)
H2: state_equiv state' x
exists ti' : instr_state,
  SeqBB.step ge sp (Iexec ti) 
    (a :: instrs) (Iterm ti' cf) /\ 
  state_equiv i' ti'
      exploit IHinstrs; eauto; simplify.A: Type
ge: Genv.t A unit
sp: val
a: instr
instrs: list instr
IHinstrs: forall (i i' ti : instr_state)
  (cf : cf_instr),
SeqBB.step ge sp (Iexec i) instrs
  (Iterm i' cf) ->
state_equiv i ti ->
exists ti' : instr_state,
  SeqBB.step ge sp (Iexec ti) instrs
    (Iterm ti' cf) /\ state_equiv i' ti'
i, i', ti: instr_state
cf: cf_instr
H0: state_equiv i ti
state': instr_state
H6: step_instr ge sp (Iexec i) a (Iexec state')
H8: step_list (step_instr ge) sp 
  (Iexec state') instrs 
  (Iterm i' cf)
x: instr_state
H: step_instr ge sp (Iexec ti) a (Iexec x)
H2: state_equiv state' x
x0: instr_state
H1: SeqBB.step ge sp (Iexec x) instrs (Iterm x0 cf)
H4: state_equiv i' x0
exists ti' : instr_state,
  SeqBB.step ge sp (Iexec ti) 
    (a :: instrs) (Iterm ti' cf) /\ 
  state_equiv i' ti'
      eexists; split.A: Type
ge: Genv.t A unit
sp: val
a: instr
instrs: list instr
IHinstrs: forall (i i' ti : instr_state)
  (cf : cf_instr),
SeqBB.step ge sp (Iexec i) instrs
  (Iterm i' cf) ->
state_equiv i ti ->
exists ti' : instr_state,
  SeqBB.step ge sp (Iexec ti) instrs
    (Iterm ti' cf) /\ state_equiv i' ti'
i, i', ti: instr_state
cf: cf_instr
H0: state_equiv i ti
state': instr_state
H6: step_instr ge sp (Iexec i) a (Iexec state')
H8: step_list (step_instr ge) sp 
  (Iexec state') instrs 
  (Iterm i' cf)
x: instr_state
H: step_instr ge sp (Iexec ti) a (Iexec x)
H2: state_equiv state' x
x0: instr_state
H1: SeqBB.step ge sp (Iexec x) instrs (Iterm x0 cf)
H4: state_equiv i' x0
SeqBB.step ge sp (Iexec ti) 
  (a :: instrs) (Iterm ?ti' cf)
A: Type
ge: Genv.t A unit
sp: val
a: instr
instrs: list instr
IHinstrs: forall (i i' ti : instr_state)
  (cf : cf_instr),
SeqBB.step ge sp (Iexec i) instrs
  (Iterm i' cf) ->
state_equiv i ti ->
exists ti' : instr_state,
  SeqBB.step ge sp (Iexec ti) instrs
    (Iterm ti' cf) /\ state_equiv i' ti'
i, i', ti: instr_state
cf: cf_instr
H0: state_equiv i ti
state': instr_state
H6: step_instr ge sp (Iexec i) a (Iexec state')
H8: step_list (step_instr ge) sp 
  (Iexec state') instrs 
  (Iterm i' cf)
x: instr_state
H: step_instr ge sp (Iexec ti) a (Iexec x)
H2: state_equiv state' x
x0: instr_state
H1: SeqBB.step ge sp (Iexec x) instrs (Iterm x0 cf)
H4: state_equiv i' x0
state_equiv i' ?ti' econstructor; eauto.A: Type
ge: Genv.t A unit
sp: val
a: instr
instrs: list instr
IHinstrs: forall (i i' ti : instr_state)
  (cf : cf_instr),
SeqBB.step ge sp (Iexec i) instrs
  (Iterm i' cf) ->
state_equiv i ti ->
exists ti' : instr_state,
  SeqBB.step ge sp (Iexec ti) instrs
    (Iterm ti' cf) /\ state_equiv i' ti'
i, i', ti: instr_state
cf: cf_instr
H0: state_equiv i ti
state': instr_state
H6: step_instr ge sp (Iexec i) a (Iexec state')
H8: step_list (step_instr ge) sp 
  (Iexec state') instrs 
  (Iterm i' cf)
x: instr_state
H: step_instr ge sp (Iexec ti) a (Iexec x)
H2: state_equiv state' x
x0: instr_state
H1: SeqBB.step ge sp (Iexec x) instrs (Iterm x0 cf)
H4: state_equiv i' x0
state_equiv i' x0 auto.
    +A: Type
ge: Genv.t A unit
sp: val
a: instr
instrs: list instr
IHinstrs: forall (i i' ti : instr_state)
  (cf : cf_instr),
SeqBB.step ge sp (Iexec i) instrs
  (Iterm i' cf) ->
state_equiv i ti ->
exists ti' : instr_state,
  SeqBB.step ge sp (Iexec ti) instrs
    (Iterm ti' cf) /\ state_equiv i' ti'
i, i', ti: instr_state
cf: cf_instr
H0: state_equiv i ti
H4: step_instr ge sp (Iexec i) a (Iterm i' cf)
exists ti' : instr_state,
  SeqBB.step ge sp (Iexec ti) 
    (a :: instrs) (Iterm ti' cf) /\ 
  state_equiv i' ti' inversion H4; subst.A: Type
ge: Genv.t A unit
sp: val
instrs: list instr
IHinstrs: forall (i i' ti : instr_state)
  (cf : cf_instr),
SeqBB.step ge sp (Iexec i) instrs
  (Iterm i' cf) ->
state_equiv i ti ->
exists ti' : instr_state,
  SeqBB.step ge sp (Iexec ti) instrs
    (Iterm ti' cf) /\ state_equiv i' ti'
i', ti: instr_state
cf: cf_instr
H0: state_equiv i' ti
p: option Gible.pred_op
H4: step_instr ge sp (Iexec i') 
  (RBexit p cf) (Iterm i' cf)
H5: truthy (is_ps i') p
exists ti' : instr_state,
  SeqBB.step ge sp (Iexec ti) 
    (RBexit p cf :: instrs) 
    (Iterm ti' cf) /\ state_equiv i' ti' eexists.A: Type
ge: Genv.t A unit
sp: val
instrs: list instr
IHinstrs: forall (i i' ti : instr_state)
  (cf : cf_instr),
SeqBB.step ge sp (Iexec i) instrs
  (Iterm i' cf) ->
state_equiv i ti ->
exists ti' : instr_state,
  SeqBB.step ge sp (Iexec ti) instrs
    (Iterm ti' cf) /\ state_equiv i' ti'
i', ti: instr_state
cf: cf_instr
H0: state_equiv i' ti
p: option Gible.pred_op
H4: step_instr ge sp (Iexec i') 
  (RBexit p cf) (Iterm i' cf)
H5: truthy (is_ps i') p
SeqBB.step ge sp (Iexec ti) 
  (RBexit p cf :: instrs) 
  (Iterm ?ti' cf) /\ state_equiv i' ?ti' constructor.A: Type
ge: Genv.t A unit
sp: val
instrs: list instr
IHinstrs: forall (i i' ti : instr_state)
  (cf : cf_instr),
SeqBB.step ge sp (Iexec i) instrs
  (Iterm i' cf) ->
state_equiv i ti ->
exists ti' : instr_state,
  SeqBB.step ge sp (Iexec ti) instrs
    (Iterm ti' cf) /\ state_equiv i' ti'
i', ti: instr_state
cf: cf_instr
H0: state_equiv i' ti
p: option Gible.pred_op
H4: step_instr ge sp (Iexec i') 
  (RBexit p cf) (Iterm i' cf)
H5: truthy (is_ps i') p
SeqBB.step ge sp (Iexec ti) 
  (RBexit p cf :: instrs) 
  (Iterm ?ti' cf)
A: Type
ge: Genv.t A unit
sp: val
instrs: list instr
IHinstrs: forall (i i' ti : instr_state)
  (cf : cf_instr),
SeqBB.step ge sp (Iexec i) instrs
  (Iterm i' cf) ->
state_equiv i ti ->
exists ti' : instr_state,
  SeqBB.step ge sp (Iexec ti) instrs
    (Iterm ti' cf) /\ state_equiv i' ti'
i', ti: instr_state
cf: cf_instr
H0: state_equiv i' ti
p: option Gible.pred_op
H4: step_instr ge sp (Iexec i') 
  (RBexit p cf) (Iterm i' cf)
H5: truthy (is_ps i') p
state_equiv i' ?ti'
      constructor.A: Type
ge: Genv.t A unit
sp: val
instrs: list instr
IHinstrs: forall (i i' ti : instr_state)
  (cf : cf_instr),
SeqBB.step ge sp (Iexec i) instrs
  (Iterm i' cf) ->
state_equiv i ti ->
exists ti' : instr_state,
  SeqBB.step ge sp (Iexec ti) instrs
    (Iterm ti' cf) /\ state_equiv i' ti'
i', ti: instr_state
cf: cf_instr
H0: state_equiv i' ti
p: option Gible.pred_op
H4: step_instr ge sp (Iexec i') 
  (RBexit p cf) (Iterm i' cf)
H5: truthy (is_ps i') p
step_instr ge sp (Iexec ti) 
  (RBexit p cf) (Iterm ?ti' cf)
A: Type
ge: Genv.t A unit
sp: val
instrs: list instr
IHinstrs: forall (i i' ti : instr_state)
  (cf : cf_instr),
SeqBB.step ge sp (Iexec i) instrs
  (Iterm i' cf) ->
state_equiv i ti ->
exists ti' : instr_state,
  SeqBB.step ge sp (Iexec ti) instrs
    (Iterm ti' cf) /\ state_equiv i' ti'
i', ti: instr_state
cf: cf_instr
H0: state_equiv i' ti
p: option Gible.pred_op
H4: step_instr ge sp (Iexec i') 
  (RBexit p cf) (Iterm i' cf)
H5: truthy (is_ps i') p
state_equiv i' ?ti' eapply step_exists_Iterm; eauto.A: Type
ge: Genv.t A unit
sp: val
instrs: list instr
IHinstrs: forall (i i' ti : instr_state)
  (cf : cf_instr),
SeqBB.step ge sp (Iexec i) instrs
  (Iterm i' cf) ->
state_equiv i ti ->
exists ti' : instr_state,
  SeqBB.step ge sp (Iexec ti) instrs
    (Iterm ti' cf) /\ state_equiv i' ti'
i', ti: instr_state
cf: cf_instr
H0: state_equiv i' ti
p: option Gible.pred_op
H4: step_instr ge sp (Iexec i') 
  (RBexit p cf) (Iterm i' cf)
H5: truthy (is_ps i') p
state_equiv i' ti auto.
Qed.