Require Import Coq.Logic.Decidable.
Require Import Coq.Structures.Equalities.
Require Import Coq.Numbers.Cyclic.Int63.Int63.
Require Import Coq.Sorting.Sorted.
Require Import Coq.Classes.RelationClasses.

Require Import TVSMT.Coqlib.
Require Import TVSMT.Maps.
Require Import TVSMT.Errors.
Require Import TVSMT.Sat.
Require Import TVSMT.Common.
Require Import TVSMT.Predicate.
Require Import TVSMT.Hashtree.
Import TVSMT.Predicate.PredicateNotation.

Require SMTCoq.SMTCoq.
Import SMTCoq.SMT_terms.
Import SMTCoq.SMT_terms.Atom.
Import SMTCoq.SMT_terms.Form.
Import SMTCoq.Trace.

#[local] Open Scope error_monad_scope.
#[local] Open Scope predicate.

#[export] Hint Unfold is_true : smtpred.

Local Notation predicate := (@pred positive).

Parameter pred_verit_unsat :
  PArray.array Atom.atom ->
  PArray.array Form.form ->
  PArray.array Int63.int ->
  (PArray.array Form.form
   * PArray.array Atom.atom
   * PArray.array Int63.int
   * option (PArray.array Int63.int)
   * Checker_Ext.certif)
.

Notation latom := Int63.int (only parsing).
Notation _llit := Int63.int (only parsing).
Notation lfargs := (list _llit) (only parsing).

Inductive lform : Type :=
| LFatom (_:latom)
| LFtrue
| LFfalse
| LFnot2 (_:Int63.int) (_:_llit)
| LFand (_:lfargs)
| LFor  (_:lfargs)
| LFimp (_:lfargs)
| LFxor (_:_llit) (_:_llit)
| LFiff (_:_llit) (_:_llit)
| LFite (_:_llit) (_:_llit) (_:_llit)
(* Bit-blasting predicate (theory of bit vectors):
        bbT a [l1;...;ln] means [l1;...;ln] is the bitwise representation of a
      (in little endian)
      WARNING: this is a slight infringement of stratification
 *)
| LFbbT (_:latom) (_:list _llit)
(* TODO: replace [list _lit] with [fargs] *)
.

Fixpoint of_list' {A} (i: Z) (a: PArray.array A) (l: list A) :=
  match l with
  | nil => a
  | el :: b =>
      of_list' (i+1) (PArray.set a (Int63.of_Z i) el) b
  end.

Definition of_list {A} (d: A) (l: list A) :=
  of_list' 0 (PArray.make (Int63.of_Z (Zlength l)) d) l.

Definition lform_to_form (f: lform): form :=
  match f with
  | LFatom a => Fatom a
  | LFtrue => Ftrue
  | LFfalse => Ffalse
  | LFnot2 i l => Fnot2 i l
  | LFand args => Fand (of_list (Int63.of_Z 0) args)
  | LFor args => For (of_list (Int63.of_Z 0) args)
  | LFimp args => Fimp (of_list (Int63.of_Z 0) args)
  | LFxor l1 l2 => Fxor l1 l2
  | LFiff l1 l2 => Fiff l1 l2
  | LFite l1 l2 l3 => Fite l1 l2 l3
  | LFbbT a b => FbbT a b
  end.

Definition form_to_lform (f: form): lform :=
  match f with
  | Fatom a => LFatom a
  | Ftrue => LFtrue
  | Ffalse => LFfalse
  | Fnot2 i l => LFnot2 i l
  | Fand args => LFand (Misc.to_list args)
  | For args => LFor (Misc.to_list args)
  | Fimp args => LFimp (Misc.to_list args)
  | Fxor l1 l2 => LFxor l1 l2
  | Fiff l1 l2 => LFiff l1 l2
  | Fite l1 l2 l3 => LFite l1 l2 l3
  | FbbT a b => LFbbT a b
  end.

Definition int_dec: forall a b: Int63.int, {a = b} + {a <> b}.
Proof.
  intros.
  destruct (Int63.eqb a b) eqn:?; [left|right].
  now apply Int63.eqb_correct.
  unfold not; intros. apply Int63.eqb_complete in H.
  now rewrite H in Heqb0.
Defined.

Definition form_eq_dec :
  forall d1 d2: lform, {d1 = d2} + {d1 <> d2}.
Proof.
  intros.
  pose proof int_dec.
  pose proof (list_eq_dec H).
  decide equality.
Defined.

Definition atom_eq_dec :
  forall d1 d2: atom, {d1 = d2} + {d1 <> d2}.
Proof.
  intros. destruct (eqb d1 d2) eqn:?. apply eqb_spec in Heqb. auto.
  right. unfold not; intros. apply Typ.not_is_true_eq_false in Heqb.
  apply Heqb. unfold is_true. apply eqb_spec. trivial.
Defined.

Module AtomDec <: MiniDecidableType.
  Definition t := atom.
  Definition eq_dec := atom_eq_dec.
End AtomDec.
Module AtomHash := Make_UDT(AtomDec).
Module Import AH := HashTree(AtomHash).
Module Import AH_Prop := HashTreeProperties(AtomHash).

Module FormDec <: MiniDecidableType.
  Definition t := lform.
  Definition eq_dec := form_eq_dec.
End FormDec.
Module FormHash := Make_UDT(FormDec).
Module Import FH := HashTree(FormHash).
Module Import FH_Prop := HashTreeProperties(FormHash).

Definition pred_list: Type := (predicate * list (positive * predicate)).

Definition to_equiv (p: list (positive * predicate)) :=
  map (fun x => equiv (Pbase (fst x)) (snd x)) p.

Definition eval_pred_list (p: pred_list) (a: PTree.t bool): option bool :=
  eval_hash_pred
    (Pand (fst p)
          (fold_left Pand (to_equiv (snd p)) Ptrue)) a.

Fixpoint unnest_predicate (fresh: positive) (p: predicate)
  : (pred_list * positive) :=
  match p with
  | Ptrue => (Ptrue, nil, fresh)
  | Pfalse => (Pfalse, nil, fresh)
  | Pundef => (Pundef, nil, fresh)
  | Pbase p' => (Pbase p', nil, fresh)
  | Pand p1 p2 =>
    let '(p1', p1l, fresh1) := unnest_predicate fresh p1 in
    let '(p2', p2l, fresh2) := unnest_predicate fresh1 p2 in
    let nvar := Pbase fresh2 in
    (nvar, (fresh2, (Pand p1' p2')) :: p2l ++ p1l, Pos.succ fresh2)
  | Por p1 p2 =>
    let '(p1', p1l, fresh1) := unnest_predicate fresh p1 in
    let '(p2', p2l, fresh2) := unnest_predicate fresh1 p2 in
    let nvar := Pbase fresh2 in
    (nvar, (fresh2, (Por p1' p2')) :: p2l ++ p1l, Pos.succ fresh2)
  | Pimp p1 p2 =>
    let '(p1', p1l, fresh1) := unnest_predicate fresh p1 in
    let '(p2', p2l, fresh2) := unnest_predicate fresh1 p2 in
    let nvar := Pbase fresh2 in
    (nvar, (fresh2, (Pimp p1' p2')) :: p2l ++ p1l, Pos.succ fresh2)
  | Pnot p1 =>
    let '(p1', p1l, fresh1) := unnest_predicate fresh p1 in
    let nvar := Pbase fresh1 in
    (nvar, (fresh1, Pnot p1') :: p1l, Pos.succ fresh1)
  end.

Notation form_t := (PArray.array SMT_terms.Form.form).
Notation atom_t := (PArray.array SMT_terms.Atom.atom).
Notation root_t := (PArray.array Int63.int) (only parsing).

Fixpoint all_preds (tree: PTree.t unit) (p: predicate): PTree.t unit :=
  match p with
  | Ptrue | Pfalse | Pundef => tree
  | Pbase p' => PTree.set p' tt tree
  | Pand p1 p2 | Por p1 p2 | Pimp p1 p2 => all_preds (all_preds tree p1) p2
  | Pnot p1 => all_preds tree p1
  end.

Definition of_P (a: positive) := Int63.of_Z (Zpos a - 2).
Definition to_P (a: Int63.int) := Z.to_pos (Int63.to_Z a + 2).

Definition P_of_P (a: positive) := Int63.of_Z ((Zpos a - 2) * 2).
Definition N_of_P (a: positive) := Int63.of_Z ((Zpos a - 2) * 2 + 1).

Definition of_map {A} (l: PMap.t A): PArray.array A :=
  PTree.fold (fun st i a => PArray.set st (of_P i) a)
             (snd l)
             (PArray.make (Int63.of_pos (max_key (snd l))) (fst l)).

Definition of_tree {A} (d: A) (l: PTree.t A): option (PArray.array A) :=
  let max := ((max_key l) + 1)%positive in
  if Z.pos max <? Int63.wB then
    Some (PTree.fold (fun st i a => PArray.set st (of_P i) a)
                     l (PArray.make (of_P max) d))
  else None.

Lemma max_key_empty :
  forall A (m: PTree.t A),
    PTree.bempty m = true ->
    max_key m = 1%positive.
Proof.
  intros.
  rewrite PTree.bempty_correct in H.
  unfold max_key.
  rewrite PTree.elements_extensional with (n:= PTree.Leaf); auto.
  intros. rewrite PTree.gleaf; auto.
Qed.

Lemma max_key_list_in : forall l,
    ((fold_right Pos.max 1%positive l) = 1%positive /\ l = nil)
    \/ (In (fold_right Pos.max 1%positive l) l /\ l <> nil).
Proof.
  induction l ; intros.
  - auto.
  - inv IHl.
    + inv H. right. simpl.
      split; [lia | congruence].
    + inv H. right. simpl.
      split; [| congruence].
      edestruct Pos.max_spec with (n:= a) (m:= (fold_right Pos.max 1%positive l)).
      * inv H. rewrite H3. right. auto.
      * inv H. rewrite H3. left.  auto.
Qed.

Lemma max_key_list_not_nil : forall A l (m: PTree.t A),
    (l <> nil) ->
    (forall k v, m ! k = Some v -> In k l) ->
    (forall k, In k l -> exists v, m ! k = Some v) ->
    exists x, m ! (fold_right Pos.max 1%positive l) = Some x.
Proof.
  intros A l.
  generalize (max_key_list_in l).
  intros [HCASE | HCASE]; intros.
  - inv HCASE. congruence.
  - inv HCASE.
    eapply H1; eauto.
Qed.

Lemma PTree_bempty_false_exists : forall A (m: PTree.t A),
    PTree.bempty m = false ->
    exists x v, m ! x = Some v.
Proof.
  induction m ; intros.
  - simpl in *. congruence.
  - simpl in *.
    destruct o.
    + exists xH. simpl. eauto.
    + apply andb_false_iff in H.
      inv H.
      * exploit IHm1; eauto. intros [x [v HSOME]].
        exists (xO x). eauto.
      * exploit IHm2; eauto. intros [x [v HSOME]].
        exists (xI x). eauto.
Qed.

Lemma max_key_in :
  forall A (m: PTree.t A),
    PTree.bempty m = false ->
    exists x, m ! (max_key m) = Some x.
Proof.
  unfold max_key.
  intros * BEMPTY.
  eapply max_key_list_not_nil with (l := (map fst (PTree.elements m))).
  - intro. apply map_eq_nil in H.
    generalize (PTree_bempty_false_exists _ m BEMPTY); eauto.
    intros [x [v HGET]].
    eapply PTree.elements_correct in HGET.
    rewrite H in *. inv HGET.
  - intros.
    eapply PTree.elements_correct in H.
    apply in_map_iff. exists (k,v). auto.
  - intros.
    apply in_map_iff in H. destruct H as [[kk v] [Hfst Helt]]. subst.
    simpl. eapply PTree.elements_complete in Helt.
    eauto.
Qed.

Lemma max_key_ext1 :
  forall A (m: PTree.t A) m',
    (forall x, m ! x = m' ! x) ->
    PTree.bempty m = false ->
    (max_key m <= max_key m')%positive.
Proof.
  intros * ALL BEMPTY.
  pose proof (max_key_in _ m BEMPTY) as X. inversion X as [x IN]; clear X.
  pose proof IN as Y. rewrite ALL in Y.
  assert (BEMPTY2: PTree.bempty m' = false).
  { apply not_true_iff_false; unfold not; intros BEMPTY2.
    apply not_true_iff_false in BEMPTY. apply BEMPTY.
    apply PTree.bempty_correct; intros.
    rewrite ALL. eapply PTree.bempty_correct in BEMPTY2; eauto.
  }
  pose proof (max_key_in _ m' BEMPTY2) as XX. inversion XX as [y IN2]; clear XX.
  eapply max_key_correct; eauto.
Qed.

Lemma max_key_ext2 :
  forall A (m: PTree.t A) m',
    (forall x, m ! x = m' ! x) ->
    PTree.bempty m' = false ->
    (max_key m' <= max_key m)%positive.
Proof.
  intros * ALL BEMPTY.
  pose proof (max_key_in _ m' BEMPTY) as X. inversion X as [x IN]; clear X.
  pose proof IN as Y. rewrite <- ALL in Y.
  assert (BEMPTY2: PTree.bempty m = false).
  { apply not_true_iff_false; unfold not; intros BEMPTY2.
    apply not_true_iff_false in BEMPTY. apply BEMPTY.
    apply PTree.bempty_correct; intros.
    rewrite <- ALL. eapply PTree.bempty_correct in BEMPTY2; eauto.
  }
  pose proof (max_key_in _ m BEMPTY2) as XX. inversion XX as [y IN2]; clear XX.
  eapply max_key_correct; eauto.
Qed.

Lemma max_key_ext :
  forall A (m: PTree.t A) m',
    (forall x, m ! x = m' ! x) ->
    max_key m' = max_key m.
Proof.
  unfold max_key; intros; erewrite PTree.elements_extensional; eauto.
Qed.

Lemma max_key_map_le :
  forall A B (m: PTree.t A) (m': PTree.t B),
    (forall x, m ! x <> None <-> m' ! x <> None) ->
    PTree.bempty m = false ->
    (max_key m <= max_key m')%positive.
Proof.
  intros * ALL BEMPTY.
  assert (BEMPTY2: PTree.bempty m' = false).
  { apply not_true_iff_false; unfold not; intros BEMPTY2.
    apply not_true_iff_false in BEMPTY. apply BEMPTY.
    apply PTree.bempty_correct; intros.
    case_eq (m ! x); intros; auto.
    specialize (ALL x). rewrite H in *.
    rewrite PTree.bempty_correct in BEMPTY2.
    specialize (BEMPTY2 x).
    intuition congruence.
  }
  pose proof (max_key_in _ m BEMPTY) as X. inversion X as [x INx]; clear X.
  assert (Y : exists y, m' ! (max_key m) = Some y).
  { case_eq (m' ! (max_key m)); intros; eauto.
    specialize (ALL (max_key m)). intuition congruence.
  }
  inversion Y as [y INy].
  try solve [eapply max_key_correct; eauto].
Qed.

Lemma ptree_map_same_keys: forall A B (f: positive -> A -> B) m,
  forall x, m ! x <> None <-> (PTree.map f m) ! x <> None.
Proof.
  split; intros.
  - intro. elim H.
    rewrite PTree.gmap in H0.
    case_eq (m ! x); intros; auto.
    rewrite H1 in H0; auto.
    simpl in H0. congruence.
  - intro. elim H.
    rewrite PTree.gmap.
    rewrite H0. auto.
Qed.

Lemma max_key_map :
  forall A B (m: PTree.t A) (f: positive -> A -> B),
    max_key m = max_key (PTree.map f m).
Proof.
  intros *. destruct (PTree.bempty m) eqn:Heqb.
  - assert (BEMPTY2: PTree.bempty (PTree.map f m) = true).
    { apply PTree.bempty_correct; intros.
      eapply PTree.bempty_correct in Heqb; eauto.
      rewrite PTree.gmap; eauto.
      rewrite Heqb. auto.
    }
    rewrite ! max_key_empty; auto.
  - assert (BEMPTY2: PTree.bempty (PTree.map f m) = false).
    { apply not_true_iff_false; intro BEMPTY2.
      apply not_true_iff_false in Heqb. apply Heqb.
      apply PTree.bempty_correct; intros.
      eapply PTree.bempty_correct with (x:= x) in BEMPTY2; eauto.
      rewrite PTree.gmap in BEMPTY2; eauto.
      unfold option_map in *. destruct_match; easy.
    }
    eapply Pos.le_antisym; eauto.
    + eapply max_key_map_le; eauto.
      eapply ptree_map_same_keys; eauto.
    + eapply max_key_map_le; eauto.
      split.
      * intros. eapply ptree_map_same_keys; eauto.
      * intros. eapply ptree_map_same_keys in H; eauto.
Qed.

Lemma gt_1_map_iff :
  forall A B (m: PTree.t A) (f: positive -> A -> B),
    gt_1 m <-> gt_1 (PTree.map f m).
Proof.
  unfold gt_1 in *; simplify.
  split.
  - simplify.
    rewrite PTree.gmap in *. unfold option_map in *.
    destruct (m ! x) eqn:?. eapply H. eauto. easy.
  - simplify.
    eapply H; eauto.
    rewrite PTree.gmap. unfold option_map in *.
    rewrite H0. easy.
Qed.

(* From Coq.micromega Require Import RingMicromega QMicromega EnvRing Tauto ZifyComparison ZifyBool ZifyInt63. *)
(* Ltac Zify.zify_post_hook ::= Z.div_mod_to_equations. *)

Lemma bounded_lt :
  forall a b n, a < b -> 0 <= a < n -> 0 <= b < n -> a mod n < b mod n.
Proof.
  intros; rewrite !Z.mod_small; lia. Qed.

Lemma max_key_set_le : forall A (m: PTree.t A) k v,
    (max_key m <= max_key (PTree.set k v m))%positive.
Proof.
  intros.
  case_eq (Pos.leb (max_key m) (max_key (PTree.set k v m)))%positive; intros.
  - apply Pos.leb_le; auto.
  - apply Pos.leb_gt in H; auto.
    apply Pos.lt_gt in H.
    exploit max_not_present; eauto.
    intros.
    assert (k <= max_key (PTree.set k v m))%positive.
    { eapply max_key_correct; eauto.
      rewrite PTree.gss; auto.
    }
    case_eq (PTree.bempty m); intros.
    + exploit max_key_empty; eauto.
      intros. rewrite H3 in *.
      lia.
    + exploit (max_key_in _ m); eauto.
      intros [vmk HSome].
      rewrite PTree.gso in H0.
      * congruence.
      * intro; subst.
        rewrite PTree.gss in H0.
        congruence.
Qed.

Lemma PArray_length_fold_set : forall A B a f (t: PTree.t A) (g: A -> B),
  PArray.length (PTree.fold (fun st i a => PArray.set st (f i) (g a)) t a)
  = PArray.length a.
Proof.
  intros.
  eapply PTree_Properties.fold_rec; eauto.
  intros.
  rewrite PArray.length_set.
  auto.
Qed.

Lemma of_pos_rec_inj: forall p1 p2
    (PVALID: 0 <= Z.pos p1 < wB)
    (KVALID: 0 <= Z.pos p2 < wB),
    (φ (of_pos_rec size p1) = φ (of_pos_rec size p2))%int63 ->
    p1 = p2.
Proof.
  unfold wB. intros.
  rewrite ! of_pos_rec_spec in H; auto.
  rewrite ! Z.mod_small in H; try lia.
Qed.

Lemma of_P_inj : forall k p
    (PVALID: 0 <= Z.pos p - 2 < wB)
    (KVALID: 0 <= Z.pos k - 2 < wB),
  of_P k = of_P p -> k = p.
Proof.
  unfold of_P, of_Z, wB, of_pos; intros.
  do 2 destruct_match; try lia.
  - generalize (of_pos_rec_spec size (Nat.le_refl _) p0).
    rewrite Z.mod_small; auto. intros.
    rewrite <- H in H0.
    rewrite to_Z_0 in H0.
    lia.
  - generalize (of_pos_rec_spec size (Nat.le_refl _) p0).
    rewrite Z.mod_small; auto. intros.
    rewrite H in H0.
    rewrite to_Z_0 in H0.
    lia.
  - generalize (of_pos_rec_spec size (Nat.le_refl _) p0).
    generalize (of_pos_rec_spec size (Nat.le_refl _) p1).
    rewrite !Z.mod_small; auto. intros.
    assert (p0 = p1).
    { eapply of_pos_rec_inj; eauto.
      congruence.
    }
    lia.
Qed.

Definition tree_a_wf (t: PTree.t atom) :=
  1 < Zpos (max_key t) < wB
  /\ gt_1 t
  /\ t ! 2 = Some (Acop CO_xH)
  /\ t ! 3 = Some (Auop UO_Zpos (of_P 2))
  /\ t ! 4 = Some (Auop UO_Zopp (of_P 3))
.

Definition tree_f_wf (t: PTree.t lform) :=
  1 < Zpos (max_key t)
  /\ (Zpos (max_key t) - 2) * 2 + 1 < wB
  /\ gt_1 t
  /\ t ! 2 = Some (LFtrue)
  /\ t ! 3 = Some (LFfalse)
.

(* Abstracting over the type of elements of the tree *)
Definition tree_key_wf A (t: PTree.t A) :=
  1 < Zpos (max_key t)
  /\ ((Zpos (max_key t) - 2) * 2 + 1 < wB
      \/ Zpos (max_key t) < wB)
  /\ gt_1 t.

Lemma of_tree_of_P :
  forall A d t p (v: A) a
         (TAWF: tree_key_wf _ t),
    gt_1 t ->
    t ! p = Some v ->
    of_tree d t = Some a ->
    PArray.get a (of_P p) = v.
Proof.
  unfold of_tree.
  intros. destruct_match; try discriminate. inv H1.
  assert
    (X: 0 <= Z.pos (max_key t) - 1 <=
        to_Z (PArray.length (PTree.fold (fun st i a => PArray.set st (of_P i) a) t
                                        (PArray.make (of_P (max_key t + 1)) d)))).
  { erewrite PArray_length_fold_set; eauto.
    rewrite PArray.length_make.
    unfold PArray.max_length.
    unfold wB, size in Heqb.
    inv TAWF.
    destruct_match; try lia.
    - unfold of_P. rewrite of_Z_spec.
      rewrite Z.mod_small; try lia.
    - rewrite Misc.max_int_wB.
      unfold wB in *. lia.
  }
  unfold gt_1 in *.
  generalize dependent H.
  generalize dependent Heqb.
  generalize dependent v.
  generalize dependent p.
  generalize dependent X.
  apply PTree_Properties.fold_rec; eauto. intros.
  - rewrite <- H in H1.
    eapply H0; auto.
    + erewrite max_key_ext; eauto.
    + erewrite max_key_ext; eauto.
    + intros. rewrite H in H3; eauto.
  - intros.
    now rewrite PTree.gempty in H0.
  - intros.
    destruct (peq k p); subst.
    + rewrite PTree.gss in H2. inv H2.
      rewrite PArray.get_set_same; auto.
      apply Int63.ltb_spec.
      rewrite PArray.length_set in X.
      destruct X as [XX X].
      eapply Z.lt_le_trans; eauto.
      * unfold of_P. rewrite of_Z_spec.
        assert (p <= max_key (PTree.set p v0 m))%positive.
        { eapply max_key_correct; eauto.
          rewrite PTree.gss; auto.
        }
        rewrite Z.mod_small; try lia.
        inv TAWF. inv H5. unfold gt_1 in *.
        specialize (H7 _ _ H0).
        apply max_key_correct with (hi:= p) in H0; eauto.
        apply Pos2Z.pos_le_pos in H0. lia.
    + rewrite PTree.gso in H2; auto.
      rewrite PArray.get_set_other.
      * apply H1; auto.
        -- rewrite PArray.length_set in X.
           destruct X as [XX X].
           split; [lia |].
           eapply Z.le_trans; eauto.
           assert (max_key m <= max_key (PTree.set k v m))%positive
             by (eapply max_key_set_le; eauto).
           lia.
        -- rewrite PArray.length_set in X.
           assert (max_key m <= max_key (PTree.set k v m))%positive
             by (eapply max_key_set_le; eauto).
           rewrite Z.ltb_lt in *.
           lia.
        -- intros. eapply H3; eauto.
           erewrite PTree.gso; eauto.
           congruence.
      * intro; subst.
        eapply of_P_inj in H4; eauto.
        apply Z.ltb_lt in Heqb.
        rewrite PArray.length_set in X.
        -- assert (1 < p)%positive.
           { eapply H3; eauto.
             rewrite PTree.gso; eauto.
           }
           assert (p <= max_key (PTree.set k v m))%positive.
           { eapply max_key_correct; eauto.
             rewrite PTree.gso; eauto.
           }
           lia.
        -- assert (1 < k)%positive.
           { eapply H3; eauto.
             rewrite PTree.gss; auto.
           }
           assert (k <= max_key (PTree.set k v m))%positive.
           { eapply max_key_correct; eauto.
             rewrite PTree.gss; auto.
           }
           apply Z.ltb_lt in Heqb; auto.
           rewrite PArray.length_set in X.
           lia.
Qed.

Definition to_smt_i ah p :=
  match p with
  | Pbase p => match AH.find_tree (Aapp (of_P p) nil) ah with
               | Some pi =>
                   if (1 <? Zpos pi) && (Zpos pi <? wB) && (0 <=? Z.pos p - 2) && (Z.pos p - 2 <? wB)
                   then Some (of_P pi)
                   else None
               | _ => None
               end
  | Ptrue => Some (Int63.of_Z 1)
  | Pfalse => Some (Int63.of_Z 2)
  | _ => None
  end.

Fixpoint get_index_acc {A} (dec: A -> A -> bool) (l : list A)
         (a : A) (acc : nat) {struct l} : option nat :=
  match l with
  | nil => None
  | x :: m => if dec x a then Some acc else get_index_acc dec m a (acc + 1)%nat
  end.

Definition get_index {A} dec (l : list A) (a : A) := get_index_acc dec l a 0.

Definition form_eqb (f1 f2: form) :=
  match f1, f2 with
  | Fatom i1, Fatom i2 => Int63.eqb i1 i2
  | Ftrue, Ftrue => true
  | Ffalse, Ffalse => true
  | Fnot2 a1 b1, Fnot2 a2 b2
  | Fiff a1 b1, Fiff a2 b2
  | Fxor a1 b1, Fxor a2 b2 => Int63.eqb a1 a2 && Int63.eqb b1 b2
  | Fand args1, Fand args2
  | For args1, For args2
  | Fimp args1, Fimp args2 => list_beq Int63.eqb (Misc.to_list args1) (Misc.to_list args2)
  | Fite a1 b1 c1, Fite a2 b2 c2 => Int63.eqb a1 a2 && Int63.eqb b1 b2 && Int63.eqb c1 c2
  | _, _ => false
  end.

Definition get_fi (lf: list form) (fresh: Z) (f: form): Z * Z * list form :=
  match get_index form_eqb lf f with Some i => (Z.of_nat i, fresh, lf) | _ => (fresh, Z.succ fresh, lf ++ f::nil) end.

Definition get_ai (lf: list atom) (fresh: Z) (f: atom): Z * Z * list atom :=
  match get_index Atom.eqb lf f with Some i => (Z.of_nat i, fresh, lf) | _ => (fresh, Z.succ fresh, lf ++ f::nil) end.

Definition to_smt_and hf ha p p1 p2 :=
  let (a1, ha1) := AH.hash_value 1%positive (Abop BO_Zlt p1 p2) ha in
  let (a2, ha2) := AH.hash_value 1%positive (Abop (BO_eq Typ.TZ) p p1) ha1 in
  let (a3, ha3) := AH.hash_value 1%positive (Abop (BO_eq Typ.TZ) p p2) ha2 in
  let (i1, hf1) := FH.hash_value 1%positive (LFatom (of_P a1)) hf in
  let (i2, hf2) := FH.hash_value 1%positive (LFatom (of_P a2)) hf1 in
  let (i3, hf3) := FH.hash_value 1%positive (LFatom (of_P a3)) hf2 in
  let (i4, hf4) := FH.hash_value 1%positive (LFite (P_of_P i1) (P_of_P i2) (P_of_P i3)) hf3 in
  (hf4, ha3, i4).

Definition to_smt_or hf ha p p1 p2 :=
  let '(a1, ha1) := AH.hash_value 1%positive (Abop BO_Zlt p1 p2) ha in
  let '(a2, ha2) := AH.hash_value 1%positive (Abop (BO_eq Typ.TZ) p p2) ha1 in
  let '(a3, ha3) := AH.hash_value 1%positive (Abop (BO_eq Typ.TZ) p p1) ha2 in
  let '(i1, hf1) := FH.hash_value 1%positive (LFatom (of_P a1)) hf in
  let '(i2, hf2) := FH.hash_value 1%positive (LFatom (of_P a2)) hf1 in
  let '(i3, hf3) := FH.hash_value 1%positive (LFatom (of_P a3)) hf2 in
  let '(i4, hf4) := FH.hash_value 1%positive (LFite (P_of_P i1) (P_of_P i2) (P_of_P i3)) hf3 in
  (hf4, ha3, i4).

Definition to_smt_imp hf ha p p1 p2 :=
  let '(a1, ha1) := AH.hash_value 1%positive (Abop BO_Zminus (of_P 3) p1) ha in
  let '(a2, ha2) := AH.hash_value 1%positive (Abop BO_Zplus (of_P a1) p2) ha1 in
  let '(a3, ha3) := AH.hash_value 1%positive (Abop BO_Zlt (of_P 3) (of_P a2)) ha2 in
  let '(a4, ha4) := AH.hash_value 1%positive (Abop (BO_eq Typ.TZ) p (of_P 3)) ha3 in
  let '(a5, ha5) := AH.hash_value 1%positive (Abop (BO_eq Typ.TZ) p (of_P a2)) ha4 in
  let '(i1, hf1) := FH.hash_value 1%positive (LFatom (of_P a3)) hf in
  let '(i2, hf2) := FH.hash_value 1%positive (LFatom (of_P a4)) hf1 in
  let '(i3, hf3) := FH.hash_value 1%positive (LFatom (of_P a5)) hf2 in
  let '(i4, hf4) := FH.hash_value 1%positive (LFite (P_of_P i1) (P_of_P i2) (P_of_P i3)) hf3 in
  (hf4, ha5, i4).

Definition to_smt_not hf ha p p1 :=
  let '(a1, ha1) := AH.hash_value 1%positive (Auop UO_Zopp p1) ha in
  let '(a2, ha2) := AH.hash_value 1%positive (Abop (BO_eq Typ.TZ) p (of_P a1)) ha1 in
  let '(i1, hf1) := FH.hash_value 1%positive (LFatom (of_P a2)) hf in
  (hf1, ha2, i1).

Definition to_smt_l (el: positive * predicate) (state: option (list Int63.int * FH.hash_tree * AH.hash_tree)) :=
  match state with
  | Some (r, f, a) =>
      let to_smt_i := to_smt_i a in
      match el with
      | (p, Pand p1 p2) =>
          match to_smt_i (Pbase p), to_smt_i p1, to_smt_i p2 with
          | Some p', Some p1', Some p2' =>
              let '(f', a', r') := to_smt_and f a p' p1' p2' in
              Some (r++(P_of_P r'::nil), f', a')
          | _, _, _ => None
          end
      | (p, Por p1 p2) =>
          match to_smt_i (Pbase p), to_smt_i p1, to_smt_i p2 with
          | Some p', Some p1', Some p2' =>
              let '(f', a', r') := to_smt_or f a p' p1' p2' in
              Some (r++(P_of_P r'::nil), f', a')
          | _, _, _ => None
          end
      | (p, Pimp p1 p2) =>
          match to_smt_i (Pbase p), to_smt_i p1, to_smt_i p2 with
          | Some p', Some p1', Some p2' =>
              let '(f', a', r') := to_smt_imp f a p' p1' p2' in
              Some (r++(P_of_P r'::nil), f', a')
          | _, _, _ => None
          end
      | (p, Pnot p1) =>
          match to_smt_i (Pbase p), to_smt_i p1 with
          | Some p', Some p1' =>
              let '(f', a', r') := to_smt_not f a p' p1' in
              Some (r++(P_of_P r'::nil), f', a')
          | _, _ => None
          end
      | _ => None
      end
  | _ => None
  end.

Definition declare_atoms_with_bounds
           (a: Z * list Int63.int * FH.hash_tree * AH.hash_tree) :=
  let '(num, cr, cf, ca) := a in
  let (happ, ca_inter) := AH.hash_value 1%positive (Aapp (Int63.of_Z num) nil) ca in
  let '((hlt1, hlt2), ca') :=
    AH.hash_value2 1%positive
                   (Abop BO_Zle (of_P 4) (of_P happ),
                     Abop BO_Zge (of_P 3) (of_P happ)) ca_inter in
  let '((halt1, halt2), cf_inter) :=
    FH.hash_value2 1%positive (LFatom (of_P hlt1), LFatom (of_P hlt2)) cf in
  let (hlfand, cf') :=
    FH.hash_value 1%positive (LFand (P_of_P halt1 :: P_of_P halt2 :: nil)) cf_inter in
  (num + 1, cr ++ (P_of_P hlfand :: nil), cf', ca').

Definition check_tree_f_wf (f: PTree.t lform) :=
  let max := Z.pos (max_key f) in
  (1 <? max)
  && ((max - 2) * 2 + 1 <? wB)
  && match f ! 1 with None => true | _ => false end
  && match f ! 2 with Some LFtrue => true | _ => false end
  && match f ! 3 with Some LFfalse => true | _ => false end.

Definition check_tree_a_wf (a: PTree.t atom) :=
  let max := Z.pos (max_key a) in
  (1 <? max)
  && (max <? wB)
  && match a ! 1 with None => true | _ => false end
  && match a ! 2 with Some (Acop CO_xH) => true | _ => false end
  && match a ! 3 with Some (Auop UO_Zpos v) => (v =? 0)%int63 | _ => false end
  && match a ! 4 with Some (Auop UO_Zopp v) => (v =? 1)%int63 | _ => false end.

Definition to_smt (max: positive) (p: pred_list): option (root_t * form_t * atom_t) :=
  let (p', pl) := p in
  let '(_, init_forms) := FH.hash_value2 1%positive (LFtrue, LFfalse) FH.empty in
  let (hpone, ia_inter1) := AH.hash_value 1%positive (Acop CO_xH) AH.empty in
  let (hzone, ia_inter2) := AH.hash_value 1%positive (Auop UO_Zpos (of_P hpone)) ia_inter1 in
  let (hzmone, init_atoms) := AH.hash_value 1%positive (Auop UO_Zopp (of_P hzone)) ia_inter2 in
  let '(v, r_defs, form_defs, atom_defs) :=
    fold_right (fun _ => declare_atoms_with_bounds)
               (0, nil, init_forms, init_atoms)
               (repeat tt (Pos.to_nat max - 1))
  in
  match
    fold_right to_smt_l (Some (r_defs, form_defs, atom_defs)) pl,
    to_smt_i atom_defs p'
  with
  | Some (r, f, a), Some p'' =>
      let '(a1, fin_a) := AH.hash_value 1%positive (Abop (BO_eq Typ.TZ) p'' (Int63.of_Z 1)) a in
      let '(f1, fin_f) := FH.hash_value 1%positive (LFatom (of_P a1)) f in
      let fin_r := r ++ (N_of_P f1)::nil in
      match
        of_tree Ftrue (PTree.map (fun _ => lform_to_form) fin_f),
        of_tree (Acop CO_xH) fin_a
      with
      | Some fin_f', Some fin_a' =>
          if check_form fin_f'
             && check_atom fin_a'
             && check_tree_f_wf fin_f
             && check_tree_a_wf fin_a
             && (v <? wB)
             && (Zlength fin_r <? wB)
          then Some (of_list (Int63.of_Z 0) fin_r, fin_f', fin_a')
          else None
      | _, _ => None
      end
  | _, _ => None
  end.

Fixpoint check_list {A} (comp: A -> A -> bool) (a b: list A) :=
  match b, a with
  | _, nil => true
  | x::xs, y::ys => comp x y && check_list comp ys xs
  | _, _ => false
  end.

Definition check_array {A} (comp: A -> A -> bool) a b :=
  check_list comp (Misc.to_list a) (Misc.to_list b).

Definition single_form_not_bv f :=
  match f with
  | Fatom _ | Ftrue | Ffalse | Fnot2 _ _ | Fand _
  | For _ | Fxor _ _ | Fiff _ _ | Fite _ _ _ => true
  | FbbT _ _ | Fimp _ => false
  end.

Definition check_atoms_in_form (l: Int63.int) (f: form) :=
  match f with
  | Fatom a => Int63.ltb a l
  | _ => true
  end.

Definition check_local_form la f :=
  Form.check_form f
  && Misc.aforallbi (fun i f' => single_form_not_bv f'
                                 && check_atoms_in_form la f') f.

Definition bool_typ_compdec := SMT_classes.Typ_compdec bool SMT_classes_instances.bool_compdec.
Definition Z_typ_compdec := SMT_classes.Typ_compdec Z SMT_classes_instances.Z_compdec.

Definition t_i_empty := PArray.make (Int63.of_Z 0) Z_typ_compdec.

Definition Ztrue := 1.
Definition Zfalse := -1.
Definition Zundef := 0.

Definition Zand (a b: Z) :=
  if a <? b then a else b.

Definition Zor (a b: Z) :=
  if a <? b then b else a.

Definition Zimp (a b: Z) :=
  if 1 <? (1 - a + b) then 1 else (1 - a + b).

Definition Znot (a: Z) := - a.

Definition Zval (v: option bool): Z :=
  match v with
  | Some true => 1
  | Some false => -1
  | None => 0
  end.

Definition t_func_mk: Z -> tval t_i_empty := fun b => Tval t_i_empty (nil, Typ.TZ) b.

(* Definition asgn_transl' (max: positive) (a: PTree.t bool) := *)
(*   Misc.foldi (fun i na => PArray.set na i (t_func_mk (Zval (a!(to_P i))))) *)
(*              (Int63.of_Z 0) (of_P max) *)
(*              (PArray.make (of_P max) (t_func_mk 0)). *)

Inductive asgn_transl_spec (a: PTree.t bool) (res: PArray.array (tval t_i_empty)) :=
| asgn_transl_rule :
  (forall i, 0 <= Z.pos i - 2 < wB -> PArray.get res (of_P i) = t_func_mk (Zval (a!i))) ->
  PArray.default res = t_func_mk 0 /\ (forall i, exists n, PArray.get res i = t_func_mk n) ->
  asgn_transl_spec a res.

Definition asgn_transl (a: PTree.t bool) :=
  let max := max_key a in
  PTree.fold (fun na i el =>
                PArray.set na (of_P i) (t_func_mk (Zval (Some el)))
             ) a (PArray.make (of_P (max + 1)) (t_func_mk 0)).

Lemma PArray_set_out_of_bound: forall A (a: PArray.array A) k d i,
    (k <? PArray.length a = false)%int63 ->
    PArray.get (PArray.set a k d) i = PArray.get a i.
Proof.
  intros.
  unfold PArray.set in *.
  destruct a. simpl PArray.length in *.
  destruct_match.
  - auto.
  - rewrite Misc.ltb_negb_geb in H.
    rewrite negb_false_iff in H.
    congruence.
Qed.

Lemma PArray_default_fold_set : forall A B (m: PTree.t A) f (g: A -> B) array,
    PArray.default (PTree.fold (fun st i a => PArray.set st (f i) (g a)) m array) =
    PArray.default array.
Proof.
  intros.
  eapply PTree_Properties.fold_rec; eauto.
  intros. rewrite PArray.default_set; auto.
Qed.

Lemma asgn_transl_OOB: forall a k,
    (k <? PArray.length (asgn_transl a) = false)%int63 ->
    PArray.get (asgn_transl a) k = t_func_mk 0.
Proof.
  unfold asgn_transl.
  intros.
  rewrite PArray.get_outofbound; auto.
  rewrite PArray_default_fold_set; auto.
Qed.

Lemma exists_asgn:
  forall a,
  forall (MAX: Z.pos (max_key a) - 2 < wB - 1),
    (forall k x, a ! k = Some x -> (0 <= Z.pos k - 2 < wB)%int63) ->
    exists res, asgn_transl_spec a res.
Proof.
  intros. exists (asgn_transl a).
  constructor.
  intros i.
  case_eq (of_P i <? PArray.length (asgn_transl a))%int63.
  - unfold asgn_transl in *.
    revert H.
    eapply PTree_Properties.fold_rec; eauto.
    + intros. rewrite <- H.
      eapply H0; eauto.
      intros. eapply H1; eauto.
      rewrite <- H. eauto.
    + intros. simpl. unfold Zval. rewrite PTree.gempty.
      destruct_match; auto.
    + unfold Zval. intros.
      rewrite PArray.length_set in H3.
      destruct (peq i k).
      * subst.
        rewrite PTree.gss.
        rewrite PArray.get_set_same; auto.
      * rewrite PTree.gso; auto.
        rewrite PArray.get_set_other; auto.
        -- eapply H1; eauto.
           intros. eapply H2; eauto.
           rewrite PTree.gso; eauto.
           congruence.
        -- intro. eapply of_P_inj in H5; eauto.
           exploit (H2 k); eauto.
           rewrite PTree.gss; eauto.
  - intros.
    rewrite PArray.get_outofbound; auto.
    unfold asgn_transl.
    rewrite PArray_default_fold_set.
    rewrite PArray.default_make.
    case_eq (a ! i); auto. intros b Haib.
    unfold asgn_transl in H0.
    rewrite PArray_length_fold_set in H0.
    rewrite PArray.length_make in H0.
    assert (0 <= Z.pos (max_key a) - 2 < wB).
    { case_eq (PTree.bempty a); intros.
      - rewrite PTree.bempty_correct in H2.
        specialize (H2 i).
        congruence.
      - eapply max_key_in in H2.
        destruct H2 as [x Hmax].
        eapply H in Hmax; eauto.
    }
    assert (i <= max_key a)%positive by (eapply max_key_correct; eauto).
    case_eq (of_P (max_key a + 1) ≤? PArray.max_length)%int63; intros.
    + rewrite H4 in H0.
      rewrite Misc.ltb_negb_geb in H0.
      rewrite negb_false_iff in H0.
      unfold PArray.max_length in *.
      unfold of_P in *.
      rewrite ! leb_spec in *.
      rewrite ! of_Z_spec in *.
      rewrite Misc.max_int_wB in *.
      rewrite ! Z.mod_small in *; try lia.
    + rewrite H4 in *.
      rewrite Misc.leb_negb_gtb in H4.
      rewrite negb_false_iff in H4.
      unfold PArray.max_length in *.
      rewrite ! ltb_spec in *.
      rewrite Misc.max_int_wB in *.
      unfold of_P in *.
      rewrite of_Z_spec in *.
      rewrite Z.mod_small in *; try lia.
  - unfold asgn_transl; intros.
    eapply PTree_Properties.fold_rec; eauto; split; intros.
    + auto.
    + econstructor. rewrite PArray.get_make. auto.
    + rewrite PArray.default_set. tauto.
    + inv H2.
      * destruct (int_dec (of_P k) i); subst.
      ** destruct (of_P k <? PArray.length a0)%int63 eqn:?.
      *** econstructor. rewrite PArray.get_set_same; eauto.
      *** econstructor. rewrite PArray.get_outofbound. rewrite PArray.default_set. eassumption.
          rewrite PArray.length_set. auto.
      ** destruct (i <? PArray.length a0)%int63 eqn:?.
      *** specialize (H4 i). inv H4. econstructor. rewrite PArray.get_set_other; eassumption.
      *** econstructor. rewrite PArray.get_outofbound. rewrite PArray.default_set. eassumption.
          rewrite PArray.length_set. auto.
Qed.

Definition empty_tfunc :=
  PArray.make 0 (t_func_mk 0).

Definition check_root_index (f: PArray.array form) (r: PArray.array Int63.int) :=
  forallb (fun x => to_Z (State.Lit.blit x) <? to_Z (PArray.length f)) (Misc.to_list r).

Definition check_wt_extra a :=
  Misc.aforallbi (fun i a' =>
    match a' with
    | Anop _ _ => false
    | Aapp _ (_::_) => false
    | _ => true
    end) a.

Fixpoint pred_in c p :=
  match p with
  | Ptrue | Pfalse | Pundef => false
  | Pbase c2 => (c =? c2)%positive
  | Pand p1 p2 | Por p1 p2 | Pimp p1 p2 => pred_in c p1 || pred_in c p2
  | Pnot p' => pred_in c p'
  end.

Definition check_smt (p: predicate): bool :=
  let a_preds1 :=
    (max_hash_pred p + 1)%positive
  in
  let '(p', a_preds) := unnest_predicate a_preds1 p in
  match to_smt a_preds p' with
  | Some (d, forms, atoms) =>
      let '(nf, na, roots, used_roots, cert) := pred_verit_unsat atoms forms d in
      check_array form_eqb forms nf
      && check_array Atom.eqb atoms na
      && check_local_form (PArray.length atoms) forms
      && Atom.check_atom na
      && Atom.wt _ empty_tfunc na
      && check_wt_extra na
      && (check_root_index forms d && negb (pred_in 1 p) && (Z.pos a_preds <? wB))
      && Checker_Ext.checker_ext na nf d used_roots cert
  | None => false
  end.

Definition mutate1_p (p: predicate): predicate :=
  match p with
  | Pand p1 p2 => Pand p2 p1
  | Por p1 p2 => Por p2 p1
  | Pimp (Pand p1 p2) b => Pimp (Pand p2 p1) b
  | Pimp (Por p1 p2) b => Pimp (Por p2 p1) b
  | Pimp b (Pand p1 p2) => Pimp b (Pand p2 p1)
  | Pimp b (Por p1 p2) => Pimp b (Por p2 p1)
  | Pnot (Pand p1 p2) => Pnot (Pand p2 p1)
  | Pnot (Por p1 p2) => Pnot (Por p2 p1)
  | p => p
  end.

Fixpoint has_Pbase (p: predicate) :=
  match p with
  | Ptrue | Pfalse | Pundef => false
  | Pbase _ => true
  | Pand a b | Por a b | Pimp a b => has_Pbase a || has_Pbase b
  | Pnot a => has_Pbase a
  end.

Definition check_smt_total (p: predicate): bool :=
  if check_smt p then true
  else if check_smt (mutate1_p p) then true
       else false.

  (** We need a higher level specification for this function so that everything is easier to prove. *)

  Definition upd_asgn :=
    fold_left
      (fun a' el =>
         match eval_hash_pred (snd el) a' with
         | Some p_b => PTree.set (fst el) p_b a'
         | _ => a'
         end).

  Inductive upd_asgn_spec: list (positive * predicate) -> PTree.t bool -> PTree.t bool -> Prop :=
  | upd_asgn_intros x :
    upd_asgn_spec nil x x
  | upd_asgn_cons_Some x xs t1 t2 b:
    eval_hash_pred (snd x) t1 = Some b ->
    upd_asgn_spec xs (PTree.set (fst x) b t1) t2 ->
    upd_asgn_spec (x :: xs) t1 t2
  | upd_asgn_cons_None x xs t1 t2:
    eval_hash_pred (snd x) t1 = None ->
    upd_asgn_spec xs t1 t2 ->
    upd_asgn_spec (x :: xs) t1 t2.

  (* #[local] Open Scope positive. *)
  (* Compute PTree.get 3 (upd_asgn ((3, Pbase 2)::(2, Pbase 1)::nil) (PTree.set 1 false (PTree.empty _))). *)

  (* Lemma upd_asgn_cons : *)
  (*   forall p form r a, *)
  (*     (forall pb, pred_In pb form -> ~ In pb (map fst r)) -> *)
  (*     (upd_asgn ((p, form)::r) a) ! p = eval_hash_pred form a. *)
  (* Proof. *)

  (* Lemma upd_asgn_cons_form : *)
  (*   forall p form r a, *)
  (*     eval_hash_pred (Pbase p) (upd_asgn ((p, form)::r) a) = eval_hash_pred form a. *)
  (* Proof. *)

  (* Lemma wt_correct' : *)
  (*   v_type Typ.type (Typ.interp t_i_empty) (PArray.get (Atom.t_interp t_i_empty a' atoms) i) *)

  Ltac ldestruct_match :=
    match goal with
    | [ H: context[match ?x with | _ => _ end] |- _ ] => destruct x eqn:?
    end.

  Lemma wt_correct' :
    forall a' a (atoms: atom_t)
      (ATOMSNONOP: forall i x l, PArray.get atoms i <> Anop x l)
      (ATOMSAPP: forall i n l, PArray.get atoms i = Aapp n l -> l = nil)
      (GETA1: forall i, exists n, PArray.get a' i = t_func_mk n)
      (GETA2: forall i, exists n, PArray.get a i = t_func_mk n),
      forall i,
        v_type Typ.type (Typ.interp t_i_empty)
          (PArray.get (Atom.t_interp t_i_empty a atoms) i) =
            v_type Typ.type (Typ.interp t_i_empty) (PArray.get (Atom.t_interp t_i_empty a' atoms) i).
  Proof.
    intros. generalize dependent i.
    pose proof (Atom.length_t_interp t_i_empty a atoms) as Y1.
    pose proof (Atom.length_t_interp t_i_empty a' atoms) as Y2.
    generalize dependent Y2.
    generalize dependent Y1.
    apply Misc.foldi_ind2 with
      (P := (fun x b b' =>
        PArray.length b = PArray.length atoms ->
        PArray.length b' = PArray.length atoms ->
        (forall i,
          v_type Typ.type (Typ.interp t_i_empty) (PArray.get b i)
            = v_type Typ.type (Typ.interp t_i_empty) (PArray.get b' i)))).
    + apply Misc.leb_0.
    + intros. rewrite PArray.get_make in *. crush.
    + intros.
      rewrite PArray.length_set in *.
      pose proof H0 as LT1. apply Int63.ltb_spec in LT1.
      pose proof H as LE2. apply Int63.leb_spec in LE2.
      destruct (int_dec i i0); subst.
      rewrite !PArray.get_set_same by (apply Int63.ltb_spec; try (rewrite H3); try rewrite H2; lia); auto.
      specialize (H1 H2 H3). assert (EQ1:=H2). assert (EQ2:=H3). clear H2. clear H3.
      destruct (PArray.get atoms i0) eqn:ATOMS; subst; simplify.
      - unfold interp_cop; repeat destruct_match; subst; auto.
      - assert (HEQ := H1 i). unfold interp_uop; destruct_match; unfold apply_unop;
          repeat destruct_match; auto;
          setoid_rewrite Heqb0 in HEQ; simplify;
          setoid_rewrite Heqb in HEQ; simplify; subst; rewrite Heqc in Heqc0; discriminate.
      - assert (HEQ1 := H1 i). assert (HEQ2 := H1 i1).
        unfold interp_bop. destruct_match;
        unfold apply_binop; repeat destruct_match; auto;
           try (setoid_rewrite Heqb4 in HEQ2; setoid_rewrite Heqb2 in HEQ2;
             setoid_rewrite Heqb3 in HEQ1; setoid_rewrite Heqb1 in HEQ1;
             simplify; subst; try rewrite Heqc0 in *; try rewrite Heqc1 in *;
             try rewrite Heqc2 in *; try rewrite Heqc3 in *; discriminate).
      - assert (HEQ1 := H1 i). assert (HEQ2 := H1 i1). assert (HEQ3 := H1 i2).
        unfold interp_top. destruct_match; subst. unfold apply_terop.
        repeat destruct_match; auto;
        setoid_rewrite Heqb4 in HEQ3; setoid_rewrite Heqb2 in HEQ1; setoid_rewrite Heqb3 in HEQ2;
          setoid_rewrite Heqb1 in HEQ3; setoid_rewrite Heqb in HEQ1; setoid_rewrite Heqb0 in HEQ2;
          simplify; subst; try rewrite Heqc4 in *; try rewrite Heqc3 in *; try rewrite Heqc2 in *;
          try rewrite Heqc1 in *; try rewrite Heqc0 in *; try rewrite Heqc in *; discriminate.
      - exfalso. eapply ATOMSNONOP; eassumption.
      - assert (HEQ1 := H1 i). specialize (GETA1 i). specialize (GETA2 i).
        inv GETA1. inv GETA2.
        repeat destruct_match. assert (l = nil) by (eapply ATOMSAPP; eassumption); subst.
        cbn [map]. unfold t_func_mk in *. unfold Tval in *. inv H2. simpl.
        inv H3. auto.
      - rewrite !PArray.get_set_other
          by (auto; apply Int63.ltb_spec; try (rewrite H3); try rewrite H2; lia);
          eauto.
  Qed.

  Lemma wt_correct2 :
    forall atoms a a'
      (ATOMSNONOP: forall i x l, PArray.get atoms i <> Anop x l)
      (ATOMSAPP: forall i n l, PArray.get atoms i = Aapp n l -> l = nil)
      (GETA1: forall i, exists n, PArray.get a' i = t_func_mk n)
      (GETA2: forall i, exists n, PArray.get a i = t_func_mk n),
      is_true (wt t_i_empty a atoms) ->
      is_true (wt t_i_empty a' atoms).
  Proof.
    unfold is_true, wt; intros.
    apply Misc.aforallbi_spec; intros i LTB.
    eapply Misc.aforallbi_spec in H; [|eassumption].
    unfold check_aux in *.
    destruct (PArray.get atoms i) eqn:?; unfold get_type' in *.
    - erewrite wt_correct'; eassumption.
    - destruct_match. simplify.
      setoid_rewrite wt_correct' with (a':=a); eauto.
      rewrite H0. rewrite H1. auto.
    - repeat destruct_match; simplify.
      setoid_rewrite wt_correct' with (a':=a); eauto.
      rewrite H1. rewrite H. rewrite H2. auto.
    - repeat destruct_match; simplify.
      setoid_rewrite wt_correct' with (a':=a); eauto.
      rewrite H1. rewrite H0. rewrite H2. rewrite H3. auto.
    - exfalso; eapply ATOMSNONOP; eauto.
    - repeat destruct_match; crush. eapply ATOMSAPP in Heqa0; subst. simplify.
      assert (GETB1:=GETA1). assert (GETB2:=GETA2).
      specialize (GETA1 i0). specialize (GETA2 i0). inv GETA1. inv GETA2.
      rewrite H in Heqf. rewrite H2 in Heqf0. unfold t_func_mk, Tval in *.
      simplify. erewrite wt_correct'; eauto.
  Qed.

  Lemma wf_empty_tfunc :
    forall i,
      exists n, PArray.get empty_tfunc i = t_func_mk n.
  Proof. unfold empty_tfunc. intros. eexists. rewrite PArray.get_make. eauto. Qed.

  Lemma to_P_of_P :
      forall p, 1 < Z.pos p < wB -> to_P (of_P p) = p.
  Proof.
    unfold to_P, of_P; intros * LT.
    rewrite of_Z_spec. rewrite !Z.mod_small by lia.
    assert (forall x, x - 2 + 2 = x) by lia.
    rewrite H; auto.
  Qed.

Lemma not_int63_lt_0 : forall i, 0 <= Int63.to_Z i.
Proof.
  intro i.
  assert (~ Int63.to_Z i < 0).
  { unfold not; intros. rewrite <- Int63.to_Z_0 in H.
    apply Int63.ltb_spec in H. now apply Misc.ltb_0 in H. }
  lia.
Qed.

  Lemma of_P_to_P :
      forall p, of_P (to_P p) = p.
  Proof.
    unfold to_P, of_P; intros. rewrite Z2Pos.id.
    assert (forall x, x + 2 - 2 = x) by lia. rewrite H.
    now rewrite of_to_Z.
    pose proof (not_int63_lt_0 p). lia.
  Qed.

  Lemma wf_asgn_spec :
    forall a a',
      asgn_transl_spec a a' ->
      forall i, exists n, PArray.get a' i = t_func_mk n.
  Proof. inversion 1; intros. inv H1. eauto. Qed.

  Lemma wt_correct :
    forall atoms a a'
      (ATOMSNONOP: forall i x l, PArray.get atoms i <> Anop x l)
      (ATOMSAPP: forall i n l, PArray.get atoms i = Aapp n l -> l = nil),
      is_true (wt _ empty_tfunc atoms) ->
      asgn_transl_spec a a' ->
      is_true (wt _ a' atoms).
  Proof.
    intros.
    pose proof (wf_asgn_spec _ _ H0).
    pose proof wf_empty_tfunc.
    eapply wt_correct2; eauto.
  Qed.

Section SMT_PROOF.

  Fixpoint Zeval (a: PTree.t bool) (p: predicate) :=
    match p with
    | Ptrue => 1
    | Pfalse => -1
    | Pundef => 0
    | Pbase p' => Zval (a ! p')
    | Pnot p' => Znot (Zeval a p')
    | Pand p1 p2 => Zand (Zeval a p1) (Zeval a p2)
    | Por p1 p2 => Zor (Zeval a p1) (Zeval a p2)
    | Pimp p1 p2 => Zimp (Zeval a p1) (Zeval a p2)
    end.

  Lemma Zeval_correct :
    forall a p,
      Zeval a p = Zval (eval_hash_pred p a).
  Proof.
    induction p; crush;
      repeat (destruct_match; simplify);
      try (rewrite IHp1; rewrite IHp2);
      auto; rewrite IHp; auto; discriminate.
  Qed.

End SMT_PROOF.

Lemma check_local_form_spec :
  forall l f,
    is_true (check_local_form l f) ->
    (forall i a b, PArray.get f i <> FbbT a b)
    /\ (forall i a, PArray.get f i <> Fimp a)
    /\ (forall i a, PArray.get f i = Fatom a -> is_true (Int63.ltb a l))
    /\ is_true (check_form f).
Proof.
  unfold check_local_form, is_true; simplify; auto.
  - unfold not; intros.
    destruct (Int63.ltb i (PArray.length f)) eqn:Heqb.
    + eapply Misc.aforallbi_spec in H1; try eassumption. now rewrite H in H1.
    + unfold check_form in H0. simplify. unfold is_Ffalse, is_Ftrue in *.
      repeat (destruct_match; try discriminate).
      rewrite PArray.get_outofbound in H; auto. now rewrite Heqf1 in H.
  - unfold not; intros.
    destruct (Int63.ltb i (PArray.length f)) eqn:Heqb.
    + eapply Misc.aforallbi_spec in H1; try eassumption. now rewrite H in H1.
    + unfold check_form in H0. simplify. unfold is_Ffalse, is_Ftrue in *.
      repeat (destruct_match; try discriminate).
      rewrite PArray.get_outofbound in H; auto. now rewrite Heqf1 in H.
  - intros.
    destruct (Int63.ltb i (PArray.length f)) eqn:Heqb.
    + eapply Misc.aforallbi_spec in H1; try eassumption. simplify.
      unfold check_atoms_in_form in H3. now rewrite H in H3.
    + unfold check_form in H0. simplify. unfold is_Ffalse, is_Ftrue in *.
      repeat (destruct_match; try discriminate).
      rewrite PArray.get_outofbound in H by auto. now rewrite Heqf1 in H.
Qed.

Lemma to_list_corr' :
  forall A a,
    (fun f b =>
       (forall i, (Int63.to_Z i < Int63.to_Z f) ->
                  PArray.get a i = nth (Z.to_nat (Int63.to_Z i)) (rev b) (PArray.default a))
       /\ Int63.to_Z f = Zlength b)
      (PArray.length a)
      (Misc.foldi (fun i (l : list A) => PArray.get a i :: l)
                  (Int63.of_Z 0)
                  (PArray.length a) nil).
Proof.
  intros. apply Misc.foldi_ind; intros.
  apply Int63.leb_spec. simplify; auto.
  pose proof (not_int63_lt_0 (PArray.length a)).
  rewrite Int63.to_Z_0. auto.
  split; intros. simpl in H. rewrite Int63.to_Z_0 in H.
  rewrite <- Int63.to_Z_0 in H. apply Int63.ltb_spec in H.
  now apply Misc.ltb_0 in H. auto.
  split; [|erewrite Misc.to_Z_add_1 by eassumption;
           rewrite Zlength_cons; lia].
  cbn [rev]. intros. erewrite Misc.to_Z_add_1 in H2 by eassumption.
  assert (Int63.to_Z i0 < Int63.to_Z i \/ Int63.to_Z i0 = Int63.to_Z i) by lia.
  inv H3. rewrite app_nth1; auto. apply H1; lia. apply Nat2Z.inj_lt.
  rewrite rev_length.
  rewrite <- Zlength_correct.
  rewrite Z_to_nat_max.
  apply Int63.leb_spec in H.
  apply Int63.ltb_spec in H0.
  pose proof (not_int63_lt_0 i0). lia.
  apply Int63.leb_spec in H.
  apply Int63.ltb_spec in H0. simpl in H.
  rewrite app_nth2; rewrite rev_length.
  replace (Datatypes.length a0) with (Z.to_nat (Z.of_nat (Datatypes.length a0)))
    by (now apply Nat2Z.id).
  rewrite <- Zlength_correct.
  rewrite <- Z2Nat.inj_sub. rewrite Zeq_minus by lia.
  simpl. apply Int63.to_Z_inj in H4.
  now subst.
  rewrite Zlength_correct. lia.
  zify. rewrite <- Zlength_correct. lia.
Qed.

Lemma to_list_corr :
  forall A (a: PArray.array A) i,
    Int63.to_Z i < Int63.to_Z (PArray.length a) ->
    PArray.get a i = nth (Z.to_nat (Int63.to_Z i)) (Misc.to_list a) (PArray.default a).
Proof.
  intros; pose proof (to_list_corr' A a).
  inv H0; auto.
Qed.

Lemma check_list_correct :
  forall A comp (a: list A) b i da db
         (CHK : is_true (check_list comp a b))
         (LT : (i < (length a))%nat),
    is_true (comp (nth i b db) (nth i a da)).
Proof.
  unfold is_true; induction a; try solve[crush].
  intros.
  simpl in CHK. destruct_match; try discriminate.
  apply andb_prop in CHK. inv CHK.
  simplify. destruct i. auto.
  apply IHa; auto. lia.
Qed.

Lemma Zlength_aux_concat: forall A (l1 l2: list A) (acc: Z),
    Zlength_aux acc _ (l1 ++ l2) = Zlength_aux (Zlength_aux acc _ l1) _ l2.
Proof.
  induction l1 ; intros; eauto.
  simpl.
  rewrite IHl1; eauto.
Qed.

Lemma length_to_list :
  forall A (a: PArray.array A),
    Int63.to_Z (PArray.length a) = Zlength (Misc.to_list a).
Proof.
  intros. unfold Misc.to_list.
  eapply Misc.foldi_ind; eauto.
  - apply Misc.leb_0.
  - intros. unfold Zlength in *. simpl.
    rewrite Zlength_aux_concat.
    rewrite <- H1. simpl.
    erewrite Misc.to_Z_add_1; eauto.
Qed.

Lemma check_list_length :
  forall A comp (l1: list A) l2,
    is_true (check_list comp l1 l2) ->
    Zlength l1 <= Zlength l2.
Proof.
  induction l1; crush. rewrite Zlength_nil. rewrite Zlength_correct. lia.
  destruct l2; crush. rewrite !Zlength_cons.
  unfold is_true in H. simplify. eapply IHl1 in H1. lia.
Qed.

Lemma check_array_length :
  forall A comp (a: PArray.array A) b,
    is_true (check_array comp a b) ->
    Int63.to_Z (PArray.length a) <= Int63.to_Z (PArray.length b).
Proof.
  intros. unfold check_array in *.
  eapply check_list_length in H. rewrite !length_to_list; auto.
Qed.

Lemma check_array_correct :
  forall A comp (a: PArray.array A) b,
    is_true (check_array comp a b) ->
    forall i,
      Int63.to_Z i < Int63.to_Z (PArray.length a) ->
      is_true (comp (PArray.get b i) (PArray.get a i)).
Proof.
  unfold check_array, is_true; intros * CHK i LT.
  pose proof (not_int63_lt_0 i).
  repeat rewrite to_list_corr.
  apply check_list_correct; auto. zify. rewrite <- Zlength_correct.
  rewrite <- length_to_list. lia.
  lia. apply check_array_length in CHK. lia.
Qed.

Section PROOF.

  Context (t_i: PArray.array SMT_classes.typ_compdec).
  Context (t_func: PArray.array (tval t_i)).

  Definition bo_dec:
    forall (a b: option bool),
      {a = b} + {a <> b}.
  Proof. pose proof bool_dec. decide equality. Qed.

  Lemma of_list'_length : forall A,
      forall (b: list A) acc array,
      PArray.length (of_list' acc array b) = PArray.length array.
  Proof.
    induction b; intros.
    - reflexivity.
    - simpl of_list'.
      erewrite IHb; eauto.
      rewrite PArray.length_set. auto.
  Qed.

  Lemma of_list_Zlength : forall A (d: A) b,
    Zlength b < wB ->
    PArray.length (of_list d b) = of_Z (Z.of_nat (length b)).
  Proof.
    unfold of_list.
    intros. rewrite of_list'_length; eauto.
    rewrite PArray.length_make.
    unfold PArray.max_length.
    destruct_match.
    - rewrite Zlength_correct. auto.
    - rewrite Misc.leb_negb_gtb in Heqb0.
      rewrite negb_false_iff in Heqb0.
      eapply ltb_spec in Heqb0.
      rewrite of_Z_spec in Heqb0.
      rewrite Z.mod_small in Heqb0; try lia.
      + rewrite Misc.max_int_wB in Heqb0. lia.
      + split; auto. rewrite Zlength_correct. lia.
  Qed.

  Opaque PArray.set.

  Lemma Zlength_aux_pos : forall A (b: list A) acc,
      acc >= 0 ->
      Zlength_aux acc A b >= 0.
  Proof.
    induction b; intros.
    - auto.
    - simpl. eapply IHb; eauto.
      lia.
  Qed.

  Lemma Zlength_pos : forall A (b: list A),
      Zlength b >= 0.
  Proof.
    unfold Zlength.
    intros. eapply Zlength_aux_pos; eauto.
    lia.
  Qed.

  Lemma of_list'_idx_preserve : forall A (b: list A) idx array,
    forall i,
      (0 <= idx)%Z ->
      (i <? of_Z idx = true)%int63 ->
      (0 <= idx + (Zlength b) < wB)%Z ->
      (PArray.get (of_list' idx array b) i) = PArray.get array i.
  Proof.
    induction b; intros.
    - auto.
    - simpl of_list'.
      rewrite Zlength_cons in *.
      erewrite IHb; eauto.
      + rewrite PArray.get_set_other; eauto.
        intro ; subst. eelim Misc.not_ltb_refl; eauto.
      + lia.
      + rewrite ltb_spec in *. rewrite of_Z_spec in *.
        assert (Zlength b >= 0) by (eapply Zlength_pos; eauto).
        rewrite ! Z.mod_small in *; try lia.
      + lia.
  Qed.

  Opaque PArray.set.

  Lemma to_list_of_list'3 :
    forall A (l: list A) arr x y,
      y + Zlength l < wB ->
      to_Z x < y ->
      to_Z x < to_Z (PArray.length arr) ->
      PArray.get (of_list' y arr l) x = PArray.get arr x.
  Proof.
    induction l; crush.
    erewrite IHl. rewrite PArray.get_set_other; auto.
    - unfold not; intros. assert (forall x y, x = y -> to_Z x = to_Z y) by (intros; now subst).
      apply H3 in H2. rewrite of_Z_spec in H2. rewrite Z.mod_small in H2; subst. lia.
      pose proof (not_int63_lt_0 x). split. lia. rewrite Zlength_cons in H.
      pose proof (Zlength_pos _ l). lia.
    - rewrite Zlength_cons in H. lia.
    - lia.
    - rewrite PArray.length_set. auto.
  Qed.

  Lemma to_list_of_list'2 :
    forall A l (d: A) x0 v a
        (PARRR: to_Z x0 < to_Z (PArray.length a))
        (XXXXX: v + Zlength l < wB),
      PArray.default a = d ->
      to_Z (PArray.length a) <= Zlength l + v ->
      v <= to_Z x0 ->
      PArray.get (of_list' v a l) x0 = nth ((Z.to_nat (to_Z x0 - v))) l d.
  Proof.
    induction l; intros.
    - simpl. assert ((x0 <? 0)%int63 = false).
      { destruct ((x0 <? 0)%int63) eqn:?; auto. pose proof (not_int63_lt_0 x0). apply Int63.ltb_spec in Heqb.
        replace (to_Z 0) with 0 in Heqb by auto. lia.
      } rewrite Zlength_nil in H0. pose proof (not_int63_lt_0 (PArray.length a)).
        rewrite PArray.get_outofbound. rewrite H. destruct_match; auto.
        apply not_true_is_false. unfold not; intros. apply Int63.ltb_spec in H4. lia.
    - simpl. destruct_match.
     assert (forall x y, x = y -> Z.of_nat x = Z.of_nat y) by (intros; subst; auto).
     apply H2 in Heqn. rewrite Z_to_nat_max in Heqn.
     rewrite Zlength_cons in H0. unfold Z.succ in H0.
     { replace (Z.max (to_Z x0 - v) 0) with (to_Z x0 - v) in Heqn by lia.
       assert (to_Z x0 = v) by lia. subst.
       rewrite of_to_Z. erewrite to_list_of_list'3; try lia.
       rewrite PArray.get_set_same; auto.
       apply Int63.ltb_spec. auto.
       rewrite Zlength_cons in XXXXX. lia.
       rewrite PArray.length_set; auto.
     }
     rewrite IHl with (d:=d).
     assert (Z.to_nat (to_Z x0 - (v + 1)) = n).
     { assert (forall a b, a = b -> (a - 1)%nat = (b - 1)%nat) by lia.
      apply H2 in Heqn.
      assert ((S n - 1)%nat = n) by lia. rewrite H3 in Heqn. rewrite <- Heqn.
      lia.
     } rewrite H2. auto.
     rewrite PArray.length_set. lia. rewrite Zlength_cons in XXXXX. lia.
     rewrite PArray.default_set. auto.
     rewrite PArray.length_set. rewrite Zlength_cons in H0. lia.
     lia.
   Qed.
   Transparent PArray.set.

  Lemma to_list_of_list' :
    forall A l (d: A) x0,
      Zlength l < wB ->
      to_Z x0 < Zlength l ->
      PArray.get (of_list d l) x0 = nth (Z.to_nat (Int63.to_Z x0)) l d.
  Proof.
    unfold of_list. intros.
    replace (to_Z x0) with (to_Z x0 - 0) by lia.
    pose proof (Zlength_pos _ l).
    apply to_list_of_list'2.
    rewrite PArray.length_make.
    assert ((of_Z (Zlength l) <=? PArray.max_length)%int63 = true).
    apply Int63.leb_spec. rewrite of_Z_spec. rewrite Z.mod_small by lia.
    unfold PArray.max_length. rewrite Misc.max_int_wB. lia. rewrite H2.
    rewrite of_Z_spec. rewrite Z.mod_small by lia. auto.
    lia.
    rewrite PArray.default_make; auto.
    rewrite PArray.length_make.
    assert ((of_Z (Zlength l) <=? PArray.max_length)%int63 = true).
    apply Int63.leb_spec. rewrite of_Z_spec. rewrite Z.mod_small by lia.
    unfold PArray.max_length. rewrite Misc.max_int_wB. lia. rewrite H2.
    rewrite of_Z_spec. rewrite Z.mod_small by lia. auto. lia.
    pose proof (not_int63_lt_0 x0). lia.
  Qed.

  Lemma to_list_of_list2 : (* lemmes nth of_list' *)
    forall A (d: A) (b: list A) x,
      Zlength b < wB ->
      In x (Misc.to_list (of_list d b)) ->
      In x b.
  Proof.
    intros. apply Misc.In_to_list in H0. simplify.
    rewrite to_list_of_list'. apply nth_In.
    apply Int63.ltb_spec in H0. rewrite of_list_Zlength in H0 by auto.
    rewrite of_Z_spec in H0. rewrite Z.mod_small in H0.
    assert (Z.of_nat (Z.to_nat φ (x0)%int63) < Z.of_nat (Datatypes.length b)).
    { rewrite Z_to_nat_max.
      pose proof (not_int63_lt_0 x0).
      lia.
    }
    lia.
    simplify. lia.
    rewrite <- Zlength_correct; auto.
    auto.
    apply Int63.ltb_spec in H0. rewrite of_list_Zlength in H0; auto.
    rewrite <- Zlength_correct in H0. rewrite Int63.of_Z_spec in H0.
    rewrite Z.mod_small in H0; auto.
    pose proof (Zlength_pos _ b). lia.
  Qed.

  Lemma of_pos_rec_unfold_xO : forall n p,
    of_pos_rec (S n) (xO p) = (of_pos_rec n p << 1)%int63.
  Proof.
    intros. reflexivity.
  Qed.

  Lemma is_even_of_pos :
    forall p a,
      (Z.pos a - 2) * 2 = Z.pos p ->
      is_even (of_pos p) = true.
  Proof.
    destruct p.
    - lia.
    - intros.
      unfold of_pos, size.
      rewrite of_pos_rec_unfold_xO.
      eapply is_even_lsl_1.
    - lia.
  Qed.

  Lemma is_pos_P_of_P:
    forall a,
      0 <= (Zpos a - 2) * 2 < wB ->
      State.Lit.is_pos (P_of_P a) = true.
  Proof.
    unfold State.Lit.is_pos, P_of_P.
    intros.
    unfold of_Z. case_eq ((Z.pos a - 2) * 2); intros; try lia.
    - apply Bva_checker.is_even_0.
    - eapply is_even_of_pos; eauto.
  Qed.

  Lemma of_pos_rec_unfold_xI : forall n p,
    of_pos_rec (S n) (xI p) = (of_pos_rec n p << 1 lor 1)%int63.
  Proof.
    intros. reflexivity.
  Qed.

  Lemma is_even_of_pos_false :
    forall p a,
      (Z.pos a - 2) * 2 + 1 = Z.pos p ->
      is_even (of_pos p) = false.
  Proof.
    destruct p.
    - intros. unfold of_pos, size.
      rewrite of_pos_rec_unfold_xI.
      rewrite Misc.is_even_or.
      rewrite andb_false_r; auto.
    - lia.
    - intros. auto.
  Qed.

  Lemma is_neg_N_of_P:
    forall a,
      0 <= (Zpos a - 2) * 2 + 1 < wB ->
      State.Lit.is_pos (N_of_P a) = false.
  Proof.
    unfold State.Lit.is_pos, N_of_P.
    intros.
    unfold of_Z. case_eq ((Z.pos a - 2) * 2 + 1); intros; try lia.
    eapply is_even_of_pos_false; eauto.
  Qed.

  Lemma blit_N_of_P:
    forall a,
      1 < Z.pos a ->
      (Z.pos a - 2) * 2 + 1 < wB ->
      State.Lit.blit (N_of_P a) = of_P a.
  Proof.
    unfold State.Lit.blit, of_P, N_of_P; intros.
    apply to_Z_inj.
    rewrite lsr_spec.
    replace (to_Z (1)%int63) with 1 by crush.
    replace (2 ^ 1) with 2 by lia.
    rewrite !of_Z_spec.
    rewrite !Z.mod_small by lia.
    rewrite Z.div_add_l by lia.
    assert (X: 1 / 2 = 0) by auto.
    rewrite X. rewrite Z.add_0_r. auto.
  Qed.

  Lemma blit_P_of_P:
    forall a,
      1 < Z.pos a ->
      (Z.pos a - 2) * 2 < wB ->
      State.Lit.blit (P_of_P a) = of_P a.
  Proof.
    unfold State.Lit.blit, of_P, P_of_P; intros.
    apply to_Z_inj.
    rewrite lsr_spec.
    replace (to_Z (1)%int63) with 1 by crush.
    replace (2 ^ 1) with 2 by lia.
    rewrite !of_Z_spec.
    rewrite !Z.mod_small by lia.
    rewrite Z_div_mult by lia. auto.
  Qed.

  Lemma in_tree_lt_array :
    forall d tree f x y,
      tree_key_wf _ tree ->
      of_tree d (PTree.map (fun _ : positive => lform_to_form) tree) = Some f ->
      tree ! x = Some y ->
      is_true (of_P x <? PArray.length f)%int63.
  Proof.
    intros.
    unfold of_tree in *.
    destruct_match; try congruence.
    inv H0. rewrite PArray_length_fold_set.
    rewrite PArray.length_make.
    unfold PArray.max_length in *.
    erewrite <- max_key_map in *; eauto.
    destruct_match.
    + pose proof (max_key_correct _ _ _ _ H1).
      unfold of_P, is_true, tree_key_wf, gt_1 in *.
      rewrite ltb_spec.
      rewrite Z.ltb_lt in *.
      rewrite ! of_Z_spec.
      inv H. inv H3. specialize (H4 x y H1).
      rewrite ! Z.mod_small; try lia.
    + pose proof (max_key_correct _ _ _ _ H1).
      unfold of_P, is_true, tree_key_wf, gt_1 in *.
      rewrite ltb_spec.
      rewrite ! of_Z_spec.
      rewrite Z.ltb_lt in *.
      rewrite Misc.max_int_wB.
      rewrite ! Z.mod_small; try lia.
      inv H. inv H3. specialize (H4 x y H1). lia.
  Qed.

  Lemma of_tree_default :
    forall A (d: A) f y,
      of_tree d f = Some y ->
      PArray.default y = d.
  Proof.
    intros. unfold of_tree in *. destruct_match; try discriminate; simplify.
    rewrite PArray_default_fold_set; auto.
  Qed.

  Lemma hash_value_in :
    forall max f ht h ht',
      hash_value max f ht = (h, ht') ->
      ht' ! h = Some f.
  Proof.
    unfold hash_value. intros.
    destruct_match.
    - inv H. eapply find_tree_correct; eauto.
    - inv H. rewrite PTree.gss. auto.
  Qed.

  Lemma AHhash_value_in :
    forall max f ht h ht',
      AH.hash_value max f ht = (h, ht') ->
      ht' ! h = Some f.
  Proof.
    unfold AH.hash_value; intros.
    destruct_match.
    - inv H. eapply AH.find_tree_correct; eauto.
    - inv H. rewrite PTree.gss. auto.
  Qed.

  Lemma pos_of_tree_max_key :
    forall A (d: A) h11 h6 x h,
      tree_a_wf h11 ->
      (max_key h6 <= max_key h11)%positive ->
      h11 ! h = h6 ! h ->
      AH.find_tree x h6 = Some h ->
      1 < Z.pos h < wB.
  Proof.
    intros. eapply AH.find_tree_Some in H2.
    pose proof H2. rewrite <- H1 in H3.
    eapply max_key_correct in H2.
    unfold tree_a_wf in *. inversion H as [RANGE [PROP [SOME1 [SOME2 SOME3]]]].
    apply PROP in H3. lia.
  Qed.

  Definition match_one {A} (f: PTree.t A) lf :=
    forall y z, lf ! y = Some z -> f ! y = Some z.

  Definition match_all {A} (f: PTree.t A) lf :=
    Forall (match_one f) lf.

Lemma match_one_refl :
  forall A x, @match_one A x x.
Proof. unfold match_one; auto. Qed.

Instance match_one_Reflexive {A} : Reflexive (@match_one A).
Proof. unfold Reflexive. auto using match_one_refl. Qed.

Lemma match_one_trans :
  forall A x y z, @match_one A x y -> match_one y z -> match_one x z.
Proof. unfold match_one; auto. Qed.

Instance match_one_Transitive {A} : Transitive (@match_one A).
Proof. unfold Transitive. eauto using match_one_trans. Qed.

  Lemma tree_a_wf_lt :
    forall h x y,
      tree_a_wf h ->
      h ! x = Some y ->
      0 <= Z.pos x - 2 < wB.
  Proof.
    unfold tree_a_wf; intros. pose proof H0 as X. apply max_key_correct in H0.
    unfold gt_1 in *. inv H. inv H2. apply H in X.
    all: lia.
  Qed.

  Section PROOF_MORE.

    Context (f: form_t) (a: atom_t) (f_t: PTree.t lform) (a_t: PTree.t atom).

    Context (CHKF: is_true (check_form f)).
    Context (CHKA: is_true (check_atom a)).
    Context (WFF: tree_f_wf f_t).
    Context (WFA: tree_a_wf a_t).

    Context (GENF: of_tree Ftrue (PTree.map (fun _ => lform_to_form) f_t) = Some f).
    Context (GENA: of_tree (Acop CO_xH) a_t = Some a).

    Context (la: PTree.t bool).
    Context (la_arr: PArray.array (tval t_i_empty)).

    Context (MATCH_LA: forall i : positive, 0 <= Z.pos i - 2 < wB ->
      PArray.get la_arr (of_P i) = t_func_mk (Zval la ! i)).

    Lemma match_one_hash_value :
      forall max x h h' y y',
        hash_value max y h = (y', h') ->
        match_one x h' ->
        match_one x h.
    Proof.
      unfold match_one.
      intros.
      eapply H0; eauto.
      eapply hash_constant; eauto.
    Qed.

    Lemma AHmatch_one_hash_value :
      forall max x h h' y y',
        AH.hash_value max y h = (y', h') ->
        match_one x h' ->
        match_one x h.
    Proof.
      unfold match_one.
      intros.
      eapply H0; eauto.
      eapply AH.hash_constant; eauto.
    Qed.

    Lemma gt_1_map :
      gt_1 (PTree.map (fun _ : positive => lform_to_form) f_t).
    Proof.
      inversion WFF; unfold gt_1 in *; simplify.
      rewrite PTree.gmap in H1. unfold option_map in *.
      destruct (f_t ! x) eqn:?. eapply H0. eauto. easy.
    Qed.

    Lemma gt_1_a :
      gt_1 a_t.
    Proof. inversion WFA; crush. Qed.

    Lemma in_tree_bounded :
      forall t p y,
        t ! p = Some y ->
        match_one f_t t ->
        0 <= (Z.pos p - 2) * 2 + 1 < wB.
    Proof.
      intros. unfold match_one in *. apply H0 in H.
      pose proof H. apply max_key_correct in H.
      unfold tree_f_wf in WFF. inversion WFF as [X1 [X2 [X3 X4]]].
      unfold gt_1 in X3.
      apply X3 in H1.
      lia.
    Qed.

    Lemma in_tree_bounded2 :
      forall t p y,
        t ! p = Some y ->
        match_one f_t t ->
        0 <= (Z.pos p - 2) * 2 < wB.
    Proof.
      intros. unfold match_one in *. apply H0 in H.
      pose proof H. apply max_key_correct in H.
      unfold tree_f_wf in WFF. inversion WFF as [X1 [X2 [X3 X4]]].
      unfold gt_1 in X3.
      apply X3 in H1.
      lia.
    Qed.

    Lemma in_tree_bounded3 :
      forall t p y,
        t ! p = Some y ->
        match_one f_t t ->
        0 <= Z.pos p - 2 < wB.
    Proof.
      intros. unfold match_one in *. apply H0 in H.
      pose proof H. apply max_key_correct in H.
      unfold tree_f_wf in WFF. inversion WFF as [X1 [X2 [X3 X4]]].
      unfold gt_1 in X3.
      apply X3 in H1.
      lia.
    Qed.

    Lemma in_tree_bounded4 :
      forall t p y,
        t ! p = Some y ->
        match_one a_t t ->
        0 <= Z.pos p - 2 < wB.
    Proof.
      intros. unfold match_one in *. apply H0 in H.
      pose proof H. apply max_key_correct in H.
      unfold tree_a_wf in WFA. inversion WFA as [X1 [X2 [X3 X4]]].
      unfold gt_1 in X2.
      apply X2 in H1.
      lia.
    Qed.

    Lemma tree_f_wf_tree_key_wf: forall f_t,
      tree_f_wf f_t ->
      tree_key_wf _ f_t.
    Proof.
      clear. intros.
      inversion H as [X1 [X2 [X3 [X4 X5]]]].
      unfold tree_key_wf.
      repeat split; try lia.
      auto.
    Qed.

    Lemma tree_a_wf_tree_key_wf: forall f_t,
      tree_a_wf f_t ->
      tree_key_wf _ f_t.
    Proof.
      clear. intros.
      inversion H as [X1 [X2 [X3 [X4 X5]]]].
      unfold tree_key_wf.
      repeat split; try lia.
      auto.
    Qed.

    Lemma tree_key_wf_map : forall A B f_t (f: positive -> A -> B),
      tree_key_wf _ f_t ->
      tree_key_wf _ (PTree.map f f_t).
    Proof.
      clear. intros.
      inversion H as [X1 [X2 X3]].
      unfold tree_key_wf.
      repeat split; try (erewrite <- max_key_map; eauto).
      rewrite <- gt_1_map_iff; eauto.
    Qed.

    #[local] Hint Resolve gt_1_map : to_smt.
    #[local] Hint Resolve gt_1_a : to_smt.
    #[local] Hint Resolve in_tree_bounded : to_smt.
    #[local] Hint Resolve in_tree_bounded2 : to_smt.
    #[local] Hint Resolve in_tree_bounded3 : to_smt.
    #[local] Hint Resolve in_tree_bounded4 : to_smt.

    Lemma of_tree_of_P_2 :
      forall t p v,
        t ! p = Some v ->
        match_one f_t t ->
        PArray.get f (of_P p) = (lform_to_form v).
    Proof.
      unfold match_one; intros.
      eapply of_tree_of_P; eauto with to_smt.
      - eapply tree_key_wf_map; eauto.
        eapply tree_f_wf_tree_key_wf; eauto.
      - rewrite PTree.gmap. apply H0 in H. rewrite H. auto.
    Qed.

    Lemma of_tree_of_P_2_hv :
      forall t p v x h,
        hash_value x v h = (p, t) ->
        match_one f_t t ->
        PArray.get f (of_P p) = (lform_to_form v).
    Proof.
      intros; apply hash_value_in in H; auto.
      eapply of_tree_of_P_2; eassumption.
    Qed.

    Lemma AHof_tree_of_P_2 :
      forall t p v,
        t ! p = Some v ->
        match_one a_t t ->
        PArray.get a (of_P p) = v.
    Proof.
      intros. pose proof H0. unfold match_one in H0; intros.
      pose proof H. apply H0 in H.
      eapply of_tree_of_P; eauto with to_smt.
      eapply tree_a_wf_tree_key_wf; eauto.
    Qed.

    Lemma AHof_tree_of_P_2_hv :
      forall t p v x h,
        AH.hash_value x v h = (p, t) ->
        match_one a_t t ->
        PArray.get a (of_P p) = v.
    Proof.
      unfold match_one; intros. apply AHhash_value_in in H.
      pose proof H. apply H0 in H.
      eapply of_tree_of_P; eauto with to_smt.
      eapply tree_a_wf_tree_key_wf; eauto.
    Qed.

    Lemma is_true_Atom_wf :
      is_true (Atom.wf a).
    Proof.
      unfold is_true in *. unfold check_atom in CHKA. repeat (destruct_match; try discriminate; []); auto.
    Qed.

    Lemma is_true_Form_wf :
      is_true (wf f).
    Proof.
      unfold is_true in *. unfold check_form in CHKF. repeat (destruct_match; try discriminate; []); crush.
    Qed.

    Lemma is_true_default_a :
      PArray.default a = Acop CO_xH.
    Proof.
      unfold is_true in *. unfold check_atom in CHKA. repeat (destruct_match; try discriminate; []); auto.
    Qed.

    Lemma gt_1_in :
      forall h h1 y,
        h ! h1 = Some y ->
        match_one f_t h ->
        1 < Z.pos h1.
    Proof.
      intros. unfold match_one in H0. apply H0 in H.
      inv WFF. unfold gt_1 in *.
      inv H2. inv H4. inv H5.
      apply H2 in H. lia.
    Qed.

    Lemma gt_1_in2 :
      forall h h1 y,
        h ! h1 = Some y ->
        match_one f_t h ->
        (Z.pos h1 - 2) * 2 < wB.
    Proof.
      intros. unfold match_one in H0. apply H0 in H.
      inv WFF. apply max_key_correct in H. lia.
    Qed.

    Lemma gt_1_in3 :
      forall h h1 y,
        h ! h1 = Some y ->
        match_one f_t h ->
        (Z.pos h1 - 2) * 2 + 1 < wB.
    Proof.
      intros. unfold match_one in H0. apply H0 in H.
      inv WFF. apply max_key_correct in H. lia.
    Qed.

    #[local] Hint Resolve gt_1_in : to_smt.
    #[local] Hint Resolve gt_1_in2: to_smt.
    #[local] Hint Resolve gt_1_in3: to_smt.

    Lemma blit_lt_length :
      forall h1 h y,
        h ! h1 = Some y ->
        match_one f_t h ->
        is_true (State.Lit.blit (P_of_P h1) <? PArray.length f)%int63.
    Proof.
      intros. rewrite blit_P_of_P; eauto with to_smt.
      eapply in_tree_lt_array; eauto with to_smt.
      eapply tree_f_wf_tree_key_wf; eauto.
    Qed.

    Lemma blit_lt_length2 :
      forall h1 h y max h',
        hash_value max y h' = (h1, h) ->
        match_one f_t h ->
        is_true (State.Lit.blit (P_of_P h1) <? PArray.length f)%int63.
    Proof.
      intros. eapply hash_value_in in H; eauto using blit_lt_length.
    Qed.

    Lemma blit_lt_length_N :
      forall h1 h y,
        h ! h1 = Some y ->
        match_one f_t h ->
        is_true (State.Lit.blit (N_of_P h1) <? PArray.length f)%int63.
    Proof.
      intros. rewrite blit_N_of_P; eauto with to_smt.
      eapply in_tree_lt_array; eauto with to_smt.
      eapply tree_f_wf_tree_key_wf; eauto.
    Qed.

    Lemma blit_lt_length_N2 :
      forall h1 h y max h',
        hash_value max y h' = (h1, h) ->
        match_one f_t h ->
        is_true (State.Lit.blit (N_of_P h1) <? PArray.length f)%int63.
    Proof.
      intros. eapply hash_value_in in H; eauto using blit_lt_length_N.
    Qed.

    Lemma lt_pos_in :
      forall h1 y h,
        h ! h1 = Some y ->
        match_one f_t h ->
        0 <= (Z.pos h1 - 2) * 2 < wB.
    Proof.
      intros. inversion WFF as [BOUNDS [MAXKEY [GT [S2 S3]]]]. unfold gt_1 in GT.
      unfold match_one in *. apply H0 in H. pose proof H as X. apply GT in H.
      apply max_key_correct in X. lia.
    Qed.

    Lemma lt_pos_in2 :
      forall h1 y h max h',
        hash_value max y h' = (h1, h) ->
        match_one f_t h ->
        0 <= (Z.pos h1 - 2) * 2 < wB.
    Proof.
      intros. eapply hash_value_in in H. eapply lt_pos_in; eauto.
    Qed.

    #[local] Hint Resolve is_true_Atom_wf : to_smt.
    #[local] Hint Resolve is_true_Form_wf : to_smt.
    #[local] Hint Resolve is_true_default_a : to_smt.
    #[local] Hint Resolve blit_lt_length2 : to_smt.
    #[local] Hint Resolve lt_pos_in2 : to_smt.
    #[local] Hint Resolve blit_lt_length_N2 : to_smt.
    #[local] Hint Resolve tree_a_wf_tree_key_wf : to_smt.
    #[local] Hint Resolve tree_f_wf_tree_key_wf : to_smt.

    #[local] Opaque Z.sub.

    Lemma to_smt_i_correct :
      forall h p i,
        match_one a_t h ->
        to_smt_i h p = Some i ->
        Atom.interp_aux t_i_empty la_arr (PArray.get (Atom.t_interp t_i_empty la_arr a)) (PArray.get a i)
        = Bval _ Typ.TZ (Zval (eval_hash_pred p la)).
    Proof.
      intros * MATCH TO_SMT.
      unfold to_smt_i in TO_SMT.
      destruct_match; try discriminate; simplify.
      unfold tree_a_wf in WFA. inversion WFA as [BOUND [PROP [AT1 [AT2 AT3]]]].
      replace (of_pos 1) with (of_P 3) by auto.
      erewrite ! of_tree_of_P; try eassumption; try lia; simpl.
      rewrite Atom.t_interp_wf by auto with to_smt.
      erewrite ! of_tree_of_P; try eassumption; try lia; auto.
      repeat split; auto; try lia.
      repeat split; auto; try lia.
      unfold tree_a_wf in WFA. inversion WFA as [BOUND [PROP [AT1 [AT2 AT3]]]].
      replace (of_pos 2) with (of_P 4) by auto.
      erewrite ! of_tree_of_P; try eassumption; try lia; simpl.
      rewrite Atom.t_interp_wf by auto with to_smt.
      erewrite ! of_tree_of_P; try eassumption; try lia; simpl.
      rewrite Atom.t_interp_wf by auto with to_smt.
      erewrite ! of_tree_of_P; try eassumption; try lia; simpl. auto.
      repeat split; auto; try lia.
      repeat split; auto; try lia.
      repeat split; auto; try lia.

      repeat (destruct_match; try discriminate; []). simplify.
      apply AH.find_tree_correct in Heqo.
      erewrite ! AHof_tree_of_P_2; try eassumption; try lia; simpl.
      destruct_match.
      rewrite MATCH_LA in Heqt.
      destruct (la ! p0) eqn:?; [destruct b|]; simplify; unfold t_func_mk, Tval in Heqt;
      symmetry in Heqt; inv Heqt; eapply Eqdep.EqdepTheory.inj_pair2 in H5; subst; auto.
      lia.
    Qed.

    Lemma interp_eval_pred :
      forall h13 h11 h6 p0 i h8 h10 h9 h12,
        match_one f_t h13 ->
        match_one a_t h11 ->
        match_one a_t h6 ->
        eval_hash_pred p0 la <> Some true ->
        to_smt_i h6 p0 = Some i ->
        AH.hash_value 1%positive (Abop (BO_eq Typ.TZ) i (Int63.of_pos 1)) h8 = (h10, h11) ->
        hash_value 1%positive (LFatom (of_P h10)) h9 = (h12, h13) ->
        State.Lit.interp (interp_state_var (interp_form_hatom t_i_empty la_arr a)
                                           (interp_form_hatom_bv t_i_empty la_arr a) f)
                         (N_of_P h12) = true.
    Proof.
      intros * M1 M2 M3 EVAL TOSMT HASH1 HASH2. unfold State.Lit.interp.
      unfold State.Var.interp, interp_state_var.
      pose proof HASH1 as IN1. eapply AHhash_value_in in IN1.
      pose proof HASH2 as IN2. eapply hash_value_in in IN2.
      rewrite is_neg_N_of_P by eauto with to_smt.
      rewrite t_interp_wf by eauto with to_smt.
      rewrite blit_N_of_P by eauto with to_smt.
      erewrite ! of_tree_of_P_2 by eauto with to_smt; simpl.
      unfold interp_form_hatom, interp_hatom.
      rewrite Atom.t_interp_wf by eauto with to_smt.
      erewrite ! AHof_tree_of_P_2 by eauto with to_smt; simpl.
      rewrite !Atom.t_interp_wf by eauto with to_smt.
      erewrite to_smt_i_correct by eauto with to_smt.
      replace (of_pos 1) with (of_P 3) by auto.
      inversion WFA as [X1 [X2 [X3 [X4 X5]]]].
      erewrite of_tree_of_P;
        [idtac|idtac|eauto with to_smt|eauto with to_smt|eauto with to_smt].
      simpl. rewrite !Atom.t_interp_wf by eauto with to_smt.
      erewrite of_tree_of_P;
        [idtac|idtac|eauto with to_smt|eauto with to_smt|eauto with to_smt].
      simpl.
      destruct (eval_hash_pred p0 la) eqn:?; [destruct b|]; try discriminate; auto.
      eapply tree_a_wf_tree_key_wf; eauto.
      eapply tree_a_wf_tree_key_wf; eauto.
    Qed.

    Lemma eval_hash_pred_Pand_lt :
      forall la p1 p2,
        Zval (eval_hash_pred (p1 ∧ p2) la) =
          if Zval (eval_hash_pred p1 la) <? Zval (eval_hash_pred p2 la)
          then Zval (eval_hash_pred p1 la) else Zval (eval_hash_pred p2 la).
    Proof.
      intros. destruct (eval_hash_pred p1 la0) eqn:A; [destruct b|];
                destruct (eval_hash_pred p2 la0) eqn:B; try destruct b;
                simplify; rewrite !A; rewrite !B; auto.
    Qed.

    Lemma eval_hash_pred_Por_lt :
      forall la p1 p2,
        Zval (eval_hash_pred (p1 ∨ p2) la) =
          if Zval (eval_hash_pred p1 la) <? Zval (eval_hash_pred p2 la)
          then Zval (eval_hash_pred p2 la) else Zval (eval_hash_pred p1 la).
    Proof.
      intros. destruct (eval_hash_pred p1 la0) eqn:A; [destruct b|];
                destruct (eval_hash_pred p2 la0) eqn:B; try destruct b;
                simplify; rewrite !A; rewrite !B; auto.
    Qed.

    Lemma eval_hash_pred_Pimp_lt :
      forall la p1 p2,
        Zval (eval_hash_pred (p1 → p2) la) =
          if 1 <? 1 - Zval (eval_hash_pred p1 la) + Zval (eval_hash_pred p2 la)
          then 1 else 1 - Zval (eval_hash_pred p1 la) + Zval (eval_hash_pred p2 la).
    Proof.
      intros. destruct (eval_hash_pred p1 la0) eqn:A; [destruct b|];
                destruct (eval_hash_pred p2 la0) eqn:B; try destruct b;
                simplify; rewrite !A; rewrite !B; auto.
    Qed.

    Lemma eval_hash_pred_Pnot_lt :
      forall la p1,
        Zval (eval_hash_pred (¬ p1) la) = - Zval (eval_hash_pred p1 la).
    Proof.
      intros. destruct (eval_hash_pred p1 la0) eqn:A; [destruct b|];
                simplify; rewrite !A; auto.
    Qed.

    Lemma to_smt_and_correct :
      forall h fa0 i p1_1 i0 p1_2 i1 h0 h9 h8 h1,
        to_smt_and h0 h i i0 i1 = (h9, h8, h1) ->
        match_one f_t h9 ->
        match_one a_t h8 ->
        to_smt_i h (Pbase fa0) = Some i ->
        to_smt_i h p1_1 = Some i0 ->
        to_smt_i h p1_2 = Some i1 ->
        eval_hash_pred (equiv (Pbase fa0) (p1_1 ∧ p1_2)) la = Some true ->
        State.Lit.interp (interp_state_var (interp_form_hatom t_i_empty la_arr a)
                                           (interp_form_hatom_bv t_i_empty la_arr a) f)
                         (P_of_P h1) = true.
    Proof.
      intros * SMTAND M1 M2 SMT1 SMT2 SMT3 EVAL. unfold State.Lit.interp.
      unfold to_smt_and in SMTAND. repeat ldestruct_match; []. inversion SMTAND; clear SMTAND; subst.
      assert (match_one f_t h15) by (eapply match_one_hash_value; eauto).
      assert (match_one f_t h13) by (eapply match_one_hash_value; eauto).
      assert (match_one f_t h11) by (eapply match_one_hash_value; eauto).
      assert (match_one f_t h0) by (eapply match_one_hash_value; eauto).
      assert (match_one a_t h5) by (eapply AHmatch_one_hash_value; eauto).
      assert (match_one a_t h3) by (eapply AHmatch_one_hash_value; eauto).
      assert (match_one a_t h) by (eapply AHmatch_one_hash_value; eauto).
      rewrite is_pos_P_of_P by eauto with to_smt.
      unfold State.Var.interp. unfold interp_state_var.
      rewrite t_interp_wf by eauto with to_smt.
      rewrite blit_P_of_P.
      erewrite of_tree_of_P_2_hv; try eassumption. simpl.
      unfold State.Lit.interp, State.Var.interp.
      rewrite !is_pos_P_of_P by eauto with to_smt.
      rewrite !t_interp_wf by eauto with to_smt.
      rewrite !blit_P_of_P.
      erewrite !of_tree_of_P_2_hv; try eassumption; simpl.
      unfold interp_form_hatom, interp_hatom.
      rewrite !Atom.t_interp_wf by auto with to_smt.
      erewrite !AHof_tree_of_P_2_hv; try eassumption; simpl.
      rewrite !Atom.t_interp_wf by auto with to_smt.
      erewrite !to_smt_i_correct by eassumption. simpl.
      apply eval_equiv in EVAL.
      replace (eval_hash_pred (Pbase fa0) la) with (la ! fa0) in EVAL by auto.
      rewrite EVAL.
      rewrite !eval_hash_pred_Pand_lt.
      destruct_match; apply Typ.i_eqb_refl.
      all: match goal with
      | H: hash_value _ _ _ = (?v, _) |- _ < Z.pos ?v =>
          apply hash_value_in in H; eauto with to_smt
      | H: hash_value _ _ _ = (?v, _) |- (Z.pos ?v - _) * _ < _ =>
          apply hash_value_in in H; eauto with to_smt
      end.
    Qed.

    Lemma to_smt_and_match_one :
      forall h i i0 i1 h0 h9 h8 h1,
        to_smt_and h0 h i i0 i1 = (h9, h8, h1) ->
        match_one f_t h9 ->
        match_one f_t h0.
    Proof.
      unfold to_smt_and; intros * SMTAND M1.
      repeat ldestruct_match; []. inversion SMTAND; clear SMTAND; subst.
      repeat (eapply match_one_hash_value; try eassumption).
    Qed.

    Lemma to_smt_and_match_one2 :
      forall h i i0 i1 h0 h9 h8 h1,
        to_smt_and h0 h i i0 i1 = (h9, h8, h1) ->
        match_one a_t h8 ->
        match_one a_t h.
    Proof.
      unfold to_smt_and; intros * SMTAND M1.
      repeat ldestruct_match; []. inversion SMTAND; clear SMTAND; subst.
      repeat (eapply AHmatch_one_hash_value; try eassumption).
    Qed.

    Lemma to_smt_or_correct :
      forall h fa0 i p1_1 i0 p1_2 i1 h0 h9 h8 h1,
        to_smt_or h0 h i i0 i1 = (h9, h8, h1) ->
        match_one f_t h9 ->
        match_one a_t h8 ->
        to_smt_i h (Pbase fa0) = Some i ->
        to_smt_i h p1_1 = Some i0 ->
        to_smt_i h p1_2 = Some i1 ->
        eval_hash_pred (equiv (Pbase fa0) (p1_1 ∨ p1_2)) la = Some true ->
        State.Lit.interp (interp_state_var (interp_form_hatom t_i_empty la_arr a)
                                           (interp_form_hatom_bv t_i_empty la_arr a) f)
                         (P_of_P h1) = true.
    Proof.
      intros * SMTOR M1 M2 SMT1 SMT2 SMT3 EVAL. unfold State.Lit.interp.
      unfold to_smt_or in SMTOR. repeat ldestruct_match; []. inversion SMTOR; clear SMTOR; subst.
      assert (match_one f_t h15) by (eapply match_one_hash_value; eauto).
      assert (match_one f_t h13) by (eapply match_one_hash_value; eauto).
      assert (match_one f_t h11) by (eapply match_one_hash_value; eauto).
      assert (match_one f_t h0) by (eapply match_one_hash_value; eauto).
      assert (match_one a_t h5) by (eapply AHmatch_one_hash_value; eauto).
      assert (match_one a_t h3) by (eapply AHmatch_one_hash_value; eauto).
      assert (match_one a_t h) by (eapply AHmatch_one_hash_value; eauto).
      rewrite is_pos_P_of_P by eauto with to_smt.
      unfold State.Var.interp. unfold interp_state_var.
      rewrite t_interp_wf by eauto with to_smt.
      rewrite blit_P_of_P.
      erewrite of_tree_of_P_2_hv; try eassumption. simpl.
      unfold State.Lit.interp, State.Var.interp.
      rewrite !is_pos_P_of_P by eauto with to_smt.
      rewrite !t_interp_wf by eauto with to_smt.
      rewrite !blit_P_of_P.
      erewrite !of_tree_of_P_2_hv; try eassumption; simpl.
      unfold interp_form_hatom, interp_hatom.
      rewrite !Atom.t_interp_wf by auto with to_smt.
      erewrite !AHof_tree_of_P_2_hv; try eassumption; simpl.
      rewrite !Atom.t_interp_wf by auto with to_smt.
      erewrite !to_smt_i_correct by eassumption. simpl.
      apply eval_equiv in EVAL.
      replace (eval_hash_pred (Pbase fa0) la) with (la ! fa0) in EVAL by auto.
      rewrite EVAL.
      rewrite !eval_hash_pred_Por_lt.
      destruct_match; apply Typ.i_eqb_refl.
      all: match goal with
      | H: hash_value _ _ _ = (?v, _) |- _ < Z.pos ?v =>
          apply hash_value_in in H; eauto with to_smt
      | H: hash_value _ _ _ = (?v, _) |- (Z.pos ?v - _) * _ < _ =>
          apply hash_value_in in H; eauto with to_smt
      end.
    Qed.

    Lemma to_smt_or_match_one :
      forall h i i0 i1 h0 h9 h8 h1,
        to_smt_or h0 h i i0 i1 = (h9, h8, h1) ->
        match_one f_t h9 ->
        match_one f_t h0.
    Proof.
      unfold to_smt_or; intros * SMTOR M1.
      repeat ldestruct_match; []. inversion SMTOR; clear SMTOR; subst.
      repeat (eapply match_one_hash_value; try eassumption).
    Qed.

    Lemma to_smt_or_match_one2 :
      forall h i i0 i1 h0 h9 h8 h1,
        to_smt_or h0 h i i0 i1 = (h9, h8, h1) ->
        match_one a_t h8 ->
        match_one a_t h.
    Proof.
      unfold to_smt_or; intros * SMTOR M1.
      repeat ldestruct_match; []. inversion SMTOR; clear SMTOR; subst.
      repeat (eapply AHmatch_one_hash_value; try eassumption).
    Qed.

    Lemma to_smt_imp_correct :
      forall h fa0 i p1_1 i0 p1_2 i1 h0 h9 h8 h1,
        to_smt_imp h0 h i i0 i1 = (h9, h8, h1) ->
        match_one f_t h9 ->
        match_one a_t h8 ->
        to_smt_i h (Pbase fa0) = Some i ->
        to_smt_i h p1_1 = Some i0 ->
        to_smt_i h p1_2 = Some i1 ->
        eval_hash_pred (equiv (Pbase fa0) (p1_1 → p1_2)) la = Some true ->
        State.Lit.interp (interp_state_var (interp_form_hatom t_i_empty la_arr a)
                                           (interp_form_hatom_bv t_i_empty la_arr a) f)
                         (P_of_P h1) = true.
    Proof.
      intros * SMTIMP M1 M2 SMT1 SMT2 SMT3 EVAL. unfold State.Lit.interp.
      unfold to_smt_imp in SMTIMP. repeat ldestruct_match; []. inversion SMTIMP; clear SMTIMP; subst.
      assert (match_one f_t h19) by (eapply match_one_hash_value; eauto).
      assert (match_one f_t h17) by (eapply match_one_hash_value; eauto).
      assert (match_one f_t h15) by (eapply match_one_hash_value; eauto).
      assert (match_one f_t h0) by (eapply match_one_hash_value; eauto).
      assert (match_one a_t h11) by (eapply AHmatch_one_hash_value; eauto).
      assert (match_one a_t h7) by (eapply AHmatch_one_hash_value; eauto).
      assert (match_one a_t h5) by (eapply AHmatch_one_hash_value; eauto).
      assert (match_one a_t h3) by (eapply AHmatch_one_hash_value; eauto).
      assert (match_one a_t h) by (eapply AHmatch_one_hash_value; eauto).
      rewrite is_pos_P_of_P by eauto with to_smt.
      unfold State.Var.interp. unfold interp_state_var.
      rewrite t_interp_wf by eauto with to_smt.
      rewrite blit_P_of_P.
      erewrite of_tree_of_P_2_hv by eassumption. simpl.
      unfold State.Lit.interp, State.Var.interp.
      rewrite !is_pos_P_of_P by eauto with to_smt.
      rewrite !t_interp_wf by eauto with to_smt.
      rewrite !blit_P_of_P.
      erewrite !of_tree_of_P_2_hv by eassumption; simpl.
      unfold interp_form_hatom, interp_hatom.
      rewrite !Atom.t_interp_wf by auto with to_smt.
      erewrite !AHof_tree_of_P_2_hv by eassumption; simpl.
      rewrite !Atom.t_interp_wf by auto with to_smt.
      inversion WFA as [WFA1 [WFA2 [WFA3 [WFA4 WFA5]]]].
      erewrite !of_tree_of_P by
          (try eassumption; try (eapply tree_a_wf_tree_key_wf; eauto); lia).
      simpl.
      rewrite !Atom.t_interp_wf by auto with to_smt.
      erewrite !of_tree_of_P by
          (try eassumption; try (eapply tree_a_wf_tree_key_wf; eauto); lia).
      erewrite !AHof_tree_of_P_2_hv by eassumption.
      erewrite !to_smt_i_correct by eassumption. cbn [Atom.interp_aux].
      rewrite !Atom.t_interp_wf by auto with to_smt.
      erewrite !AHof_tree_of_P_2_hv by eassumption.
      erewrite !to_smt_i_correct by eassumption. cbn [Atom.interp_aux].
      rewrite !Atom.t_interp_wf by auto with to_smt.
      erewrite !of_tree_of_P by
          (try eassumption; try (eapply tree_a_wf_tree_key_wf; eauto); lia).
      cbn [Atom.interp_aux].
      rewrite !Atom.t_interp_wf by auto with to_smt.
      erewrite !of_tree_of_P by
          (try eassumption; try (eapply tree_a_wf_tree_key_wf; eauto); lia).
      erewrite !to_smt_i_correct by eassumption.
      cbn -[Z.sub].
      apply eval_equiv in EVAL.
      replace (eval_hash_pred (Pbase fa0) la) with (la ! fa0) in EVAL by auto.
      rewrite EVAL.
      rewrite !eval_hash_pred_Pimp_lt.
      destruct_match; auto using Z.eqb_refl.
      all: match goal with
      | H: hash_value _ _ _ = (?v, _) |- _ < Z.pos ?v =>
          apply hash_value_in in H; eauto with to_smt
      | H: hash_value _ _ _ = (?v, _) |- (Z.pos ?v - _) * _ < _ =>
          apply hash_value_in in H; eauto with to_smt
      end.
    Qed.

    Lemma to_smt_imp_match_one :
      forall h i i0 i1 h0 h9 h8 h1,
        to_smt_imp h0 h i i0 i1 = (h9, h8, h1) ->
        match_one f_t h9 ->
        match_one f_t h0.
    Proof.
      unfold to_smt_imp; intros * SMTIMP M1.
      repeat ldestruct_match; []. inversion SMTIMP; clear SMTIMP; subst.
      repeat (eapply match_one_hash_value; try eassumption).
    Qed.

    Lemma to_smt_imp_match_one2 :
      forall h i i0 i1 h0 h9 h8 h1,
        to_smt_imp h0 h i i0 i1 = (h9, h8, h1) ->
        match_one a_t h8 ->
        match_one a_t h.
    Proof.
      unfold to_smt_imp; intros * SMTIMP M1.
      repeat ldestruct_match; []. inversion SMTIMP; clear SMTIMP; subst.
      repeat (eapply AHmatch_one_hash_value; try eassumption).
    Qed.

    Lemma to_smt_not_correct :
      forall h fa0 i p1_1 i0 h0 h9 h8 h1,
        to_smt_not h0 h i i0 = (h9, h8, h1) ->
        match_one f_t h9 ->
        match_one a_t h8 ->
        to_smt_i h (Pbase fa0) = Some i ->
        to_smt_i h p1_1 = Some i0 ->
        eval_hash_pred (equiv (Pbase fa0) (¬ p1_1)) la = Some true ->
        State.Lit.interp (interp_state_var (interp_form_hatom t_i_empty la_arr a)
                                           (interp_form_hatom_bv t_i_empty la_arr a) f)
                         (P_of_P h1) = true.
    Proof.
      intros * SMTNOT M1 M2 SMT1 SMT2 EVAL. unfold State.Lit.interp.
      unfold to_smt_not in SMTNOT. repeat ldestruct_match; []. inversion SMTNOT; clear SMTNOT; subst.
      assert (match_one f_t h0) by (eapply match_one_hash_value; eauto).
      assert (match_one a_t h3) by (eapply AHmatch_one_hash_value; eauto).
      assert (match_one a_t h) by (eapply AHmatch_one_hash_value; eauto).
      rewrite is_pos_P_of_P by eauto with to_smt.
      unfold State.Var.interp. unfold interp_state_var.
      rewrite t_interp_wf by eauto with to_smt.
      rewrite blit_P_of_P.
      erewrite of_tree_of_P_2_hv by eassumption. cbn.
      unfold interp_form_hatom. unfold interp_hatom.
      rewrite Atom.t_interp_wf by eauto with to_smt.
      erewrite !AHof_tree_of_P_2_hv by eassumption. cbn.
      rewrite Atom.t_interp_wf by eauto with to_smt.
      inversion WFA as [WFA1 [WFA2 [WFA3 [WFA4 WFA5]]]].
      erewrite !to_smt_i_correct by eassumption.
      rewrite Atom.t_interp_wf by eauto with to_smt.
      erewrite !AHof_tree_of_P_2_hv by eassumption. cbn.
      rewrite Atom.t_interp_wf by eauto with to_smt.
      erewrite !to_smt_i_correct by eassumption. cbn.
      apply eval_equiv in EVAL.
      replace (eval_hash_pred (Pbase fa0) la) with (la ! fa0) in EVAL by auto.
      rewrite EVAL.
      rewrite !eval_hash_pred_Pnot_lt.
      auto using Z.eqb_refl.
      all: match goal with
           | H: hash_value _ _ _ = (?v, _) |- _ < Z.pos ?v =>
               apply hash_value_in in H; eauto with to_smt
           | H: hash_value _ _ _ = (?v, _) |- (Z.pos ?v - _) * _ < _ =>
               apply hash_value_in in H; eauto with to_smt
           end.
    Qed.

    Lemma to_smt_not_match_one :
      forall h i i0 h0 h9 h8 h1,
        to_smt_not h0 h i i0 = (h9, h8, h1) ->
        match_one f_t h9 ->
        match_one f_t h0.
    Proof.
      unfold to_smt_not; intros * SMTNOT M1.
      repeat ldestruct_match; []. inversion SMTNOT; clear SMTNOT; subst.
      repeat (eapply match_one_hash_value; try eassumption).
    Qed.

    Lemma to_smt_not_match_one2 :
      forall h i i0 h0 h9 h8 h1,
        to_smt_not h0 h i i0 = (h9, h8, h1) ->
        match_one a_t h8 ->
        match_one a_t h.
    Proof.
      unfold to_smt_not; intros * SMTNOT M1.
      repeat ldestruct_match; []. inversion SMTNOT; clear SMTNOT; subst.
      repeat (eapply AHmatch_one_hash_value; try eassumption).
    Qed.

    Lemma fold_to_smt_l_correct :
      forall l l0 h7 h6 l1 h9 h8 x,
        match_one f_t h9 -> match_one a_t h8 ->
        fold_right to_smt_l (Some (l0, h7, h6)) l = Some (l1, h9, h8) ->
        (forall y, In y l0 -> State.Lit.interp (interp_state_var
                                                  (interp_form_hatom t_i_empty la_arr a)
                                                  (interp_form_hatom_bv t_i_empty la_arr a) f) y = true) ->
        eval_hash_pred (fold_left Pand (to_equiv l) T) la = Some true ->
        In x l1 ->
        State.Lit.interp (interp_state_var
                            (interp_form_hatom t_i_empty la_arr a)
                            (interp_form_hatom_bv t_i_empty la_arr a) f) x = true.
    Proof.
      induction l as [|a0 l' IHl]; intros * M1 M2 TO_SMT_L PREV_LIST EVAL_FOLD IN. simplify; eauto.
      simpl in EVAL_FOLD.
      apply eval_hash_pred_fold_Pand4 in EVAL_FOLD. inversion EVAL_FOLD as [EVAL_FOLD' EVAL_A0].
      destruct a0 as [fa0 sa0]. cbn [fst snd] in *.
      simpl in TO_SMT_L. unfold to_smt_l in TO_SMT_L. fold to_smt_l in TO_SMT_L.
      repeat (destruct_match; try discriminate; []).
      destruct_match; try discriminate;
      repeat (destruct_match; try discriminate; []); inversion TO_SMT_L; subst;
      [ assert (match_one f_t h0) by (eapply to_smt_and_match_one; eauto);
        assert (match_one a_t h) by (eapply to_smt_and_match_one2; eauto)
      | assert (match_one f_t h0) by (eapply to_smt_or_match_one; eauto);
        assert (match_one a_t h) by (eapply to_smt_or_match_one2; eauto)
      | assert (match_one f_t h0) by (eapply to_smt_imp_match_one; eauto);
        assert (match_one a_t h) by (eapply to_smt_imp_match_one2; eauto)
      | assert (match_one f_t h0) by (eapply to_smt_not_match_one; eauto);
        assert (match_one a_t h) by (eapply to_smt_not_match_one2; eauto) ].
      all: apply in_app_or in IN; inversion IN as [INL | INP]; clear IN; [solve [eauto]|];
        inversion INP as [EQ | NIL]; clear INP; [|solve [inversion NIL]]; subst.
      - eapply to_smt_and_correct; eauto. now rewrite <- eval_hash_pred_T_Pand.
      - eapply to_smt_or_correct; eauto. now rewrite <- eval_hash_pred_T_Pand.
      - eapply to_smt_imp_correct; eauto. now rewrite <- eval_hash_pred_T_Pand.
      - eapply to_smt_not_correct; eauto. now rewrite <- eval_hash_pred_T_Pand.
    Qed.

    Lemma gt_1_fold_init :
      forall (lx: list unit) v' l0 init_forms init_atoms v l1 form_defs atom_defs,
        fold_right (fun _ => declare_atoms_with_bounds)
                 (v', l0, init_forms, init_atoms)
                 lx = (v, l1, form_defs, atom_defs) ->
        0 <= v' -> 0 <= v.
    Proof.
      induction lx; crush.
      remember (fold_right (fun _ : unit => declare_atoms_with_bounds)
        (v', l0, init_forms, init_atoms) lx) as folds.
      symmetry in Heqfolds. destruct folds as [[[A1 A2] A3] A4].
      eapply IHlx in Heqfolds; eauto. unfold declare_atoms_with_bounds in H.
      repeat (destruct_match; []). simplify. lia.
    Qed.

    Lemma fold_init_correct :
      forall (lx: list unit) l1 x init_forms init_atoms form_defs atom_defs l0 v v',
        match_one f_t form_defs -> match_one a_t atom_defs ->
        fold_right (fun _ => declare_atoms_with_bounds)
               (v', l0, init_forms, init_atoms)
               lx = (v, l1, form_defs, atom_defs) ->
        (forall y, In y l0 ->
          State.Lit.interp (interp_state_var
            (interp_form_hatom t_i_empty la_arr a)
            (interp_form_hatom_bv t_i_empty la_arr a) f) y = true) ->
        In x l1 -> 0 <= v' -> v < wB ->
        State.Lit.interp (interp_state_var
                            (interp_form_hatom t_i_empty la_arr a)
                            (interp_form_hatom_bv t_i_empty la_arr a) f) x = true.
    Proof.
      induction lx; crush. assert (VPRIME := H4). clear H4. assert (VPRIME2 := H5). clear H5.
      remember (fold_right (fun _ : unit => declare_atoms_with_bounds) (v', l0, init_forms, init_atoms) lx) as folds.
      symmetry in Heqfolds. destruct folds as [[[V R] F] A]. simpl in H1.
      repeat (destruct_match; []). simplify.
      eapply in_app in H3. inv H3. eapply IHlx in Heqfolds; eauto; try lia.
      assert (match_one f_t h4) by (eapply match_one_hash_value; eauto).
      assert (match_one f_t h10) by (eapply match_one_hash_value; eauto).
      eapply match_one_hash_value; eauto.
      assert (match_one a_t h14) by (eapply AHmatch_one_hash_value; eauto).
      assert (match_one a_t h0) by (eapply AHmatch_one_hash_value; eauto).
      eapply AHmatch_one_hash_value; eauto.
      assert (F1: match_one f_t h4) by (eapply match_one_hash_value; eauto).
      assert (F2: match_one f_t h10) by (eapply match_one_hash_value; eauto).
      assert (A1: match_one a_t h14) by (eapply AHmatch_one_hash_value; eauto).
      assert (A2: match_one a_t h0) by (eapply AHmatch_one_hash_value; eauto).
      inv H1; [|inv H3].
      unfold State.Lit.interp.
      rewrite is_pos_P_of_P by eauto with to_smt.
      unfold State.Var.interp. unfold interp_state_var.
      rewrite t_interp_wf by eauto with to_smt.
      rewrite blit_P_of_P.
      erewrite of_tree_of_P_2_hv by eassumption. cbn.
      unfold State.Lit.interp.
      rewrite !is_pos_P_of_P by eauto with to_smt.
      unfold State.Var.interp. rewrite !t_interp_wf by eauto with to_smt.
      rewrite !blit_P_of_P.
      erewrite !of_tree_of_P_2_hv by eassumption. cbn.
      unfold interp_form_hatom, interp_hatom.
      rewrite !Atom.t_interp_wf by eauto with to_smt.
      erewrite !AHof_tree_of_P_2_hv by eassumption. cbn.
      inversion WFA as [WFA1 [WFA2 [WFA3 [WFA4 WFA5]]]].
      rewrite !Atom.t_interp_wf by eauto with to_smt.
      erewrite !AHof_tree_of_P_2 by (try eassumption; reflexivity). cbn.
      rewrite !Atom.t_interp_wf by eauto with to_smt.
      erewrite !AHof_tree_of_P_2 by (try eassumption; reflexivity). cbn.
      rewrite !Atom.t_interp_wf by eauto with to_smt.
      erewrite !AHof_tree_of_P_2 by (try eassumption; reflexivity). cbn.
      erewrite !AHof_tree_of_P_2_hv by eassumption. cbn.
      repeat (destruct_match; []). repeat (ldestruct_match; []).
      assert (0 <= V).
      { eapply gt_1_fold_init; eauto. }
      replace (of_Z V) with (of_P (Z.to_pos (V + 2))) in Heqt by
        (unfold of_P; f_equal; rewrite Z2Pos.id by lia; lia).
      rewrite MATCH_LA in Heqt.
      destruct (la ! (Z.to_pos (V + 2))). destruct b.
      unfold t_func_mk, Tval in Heqt. cbn in Heqt.
      symmetry in Heqt. inv Heqt. eapply Eqdep.EqdepTheory.inj_pair2 in H5. subst.
      simpl in Heqb. unfold Bval in Heqb. symmetry in Heqb. inv Heqb.
      eapply Eqdep.EqdepTheory.inj_pair2 in H5. subst. auto.
      unfold t_func_mk, Tval in Heqt. cbn in Heqt.
      symmetry in Heqt. inv Heqt. eapply Eqdep.EqdepTheory.inj_pair2 in H5. subst.
      simpl in Heqb. unfold Bval in Heqb. symmetry in Heqb. inv Heqb.
      eapply Eqdep.EqdepTheory.inj_pair2 in H5. subst. auto.
      unfold t_func_mk, Tval in Heqt. cbn in Heqt.
      symmetry in Heqt. inv Heqt. eapply Eqdep.EqdepTheory.inj_pair2 in H5. subst.
      simpl in Heqb. unfold Bval in Heqb. symmetry in Heqb. inv Heqb.
      eapply Eqdep.EqdepTheory.inj_pair2 in H5. subst. auto.
      all: try match goal with
           | H: hash_value _ _ _ = (?v, _) |- _ < Z.pos ?v =>
               apply hash_value_in in H; eauto with to_smt
           | H: hash_value _ _ _ = (?v, _) |- (Z.pos ?v - _) * _ < _ =>
               apply hash_value_in in H; eauto with to_smt
           end.
     rewrite Z2Pos.id; lia.
  Qed.

End PROOF_MORE.

  Definition pl_leq {A} (a b: positive * A): Prop :=
    ((fst a) <= (fst b))%positive.

  Definition pl_lt {A} (a b: positive * A): Prop :=
    ((fst a) < (fst b))%positive.

  Definition pl_eq {A} (a b: positive * A): Prop :=
    fst a = fst b.

  Lemma pl_lt_trans :
    forall A (a b c: positive * A), pl_lt a b -> pl_lt b c -> pl_lt a c.
  Proof. unfold pl_lt; lia. Qed.

  Lemma pl_lt_irrefl :
    forall A (a: positive * A), ~ pl_lt a a.
  Proof. unfold pl_lt; lia. Qed.

  Lemma pl_lt_asymm :
    forall A (a b: positive * A), pl_lt a b -> pl_lt b a -> False.
  Proof. unfold pl_lt; lia. Qed.

  Definition Sorted := Sorted (@pl_lt predicate).

  Lemma pl_leq_refl :
    forall A (a: positive * A), pl_leq a a.
  Proof. unfold pl_leq; reflexivity. Qed.

  Lemma pl_leq_trans :
    forall A (a b c: positive * A), pl_leq a b -> pl_leq b c -> pl_leq a c.
  Proof. unfold pl_leq; intros; lia. Qed.

  Lemma pl_eq_refl :
    forall A (a: positive * A), pl_eq a a.
  Proof. unfold pl_leq; reflexivity. Qed.

  Lemma pl_eq_symm :
    forall A (a b: positive * A), pl_eq a b -> pl_eq b a.
  Proof. unfold pl_eq; intros; lia. Qed.

  Lemma pl_eq_trans :
    forall A (a b c: positive * A), pl_eq a b -> pl_eq b c -> pl_eq a c.
  Proof. unfold pl_eq; intros; lia. Qed.

  #[global] Instance Reflexive_pl_leq {A} : Reflexive (@pl_leq A).
  Proof. unfold Reflexive. apply pl_leq_refl. Qed.

  #[global] Instance Transitive_pl_leq {A} : Transitive (@pl_leq A).
  Proof. unfold Transitive. apply pl_leq_trans. Qed.

  #[global] Instance PreOrder_pl_leq {A} : PreOrder (@pl_leq A) := {}.

  #[global] Instance Reflexive_pl_eq {A} : Reflexive (@pl_eq A).
  Proof. unfold Reflexive. apply pl_eq_refl. Qed.

  #[global] Instance Symmetric_pl_eq {A} : Symmetric (@pl_eq A).
  Proof. unfold Symmetric. apply pl_eq_symm. Qed.

  #[global] Instance Transitive_pl_eq {A} : Transitive (@pl_eq A).
  Proof. unfold Transitive. apply pl_eq_trans. Qed.

  #[global] Instance Equivalence_pl_eq {A} : Equivalence (@pl_eq A) := {}.

  #[global] Instance Antisymmetric_pl_leq {A} : Antisymmetric (positive * A) pl_eq pl_leq.
  Proof. unfold Antisymmetric, pl_eq, pl_leq; lia. Qed.

  #[global] Instance PartialOrder_pl_leq {A} : PartialOrder (@pl_eq A) (@pl_leq A).
  Proof.
    unfold PartialOrder, relation_equivalence, predicate_equivalence. crush.
    unfold relation_conjunction, predicate_intersection. simplify. unfold pl_eq, pl_leq, Basics.flip.
    split. lia. lia.
  Qed.

  #[global] Instance Irreflexive_pl_lt {A} : Irreflexive (@pl_lt A).
  Proof. unfold Irreflexive, Reflexive, complement. apply pl_lt_irrefl. Qed.

  #[global] Instance Asymmetric_pl_lt {A} : Asymmetric (@pl_lt A).
  Proof. unfold Asymmetric. apply pl_lt_asymm. Qed.

  #[global] Instance Transitive_pl_lt {A} : Transitive (@pl_lt A).
  Proof. unfold Transitive. apply pl_lt_trans. Qed.

  #[global] Instance StrictOrder_pl_lt {A} : StrictOrder (@pl_lt A) := {}.

  Lemma eval_hash_pred_upd_asgn :
    forall l p a,
      Forall (fun x => (max_hash_pred p < fst x)%positive) l ->
      eval_hash_pred p (upd_asgn l a) = eval_hash_pred p a.
  Proof.
    induction l as [| c l IHl]; try solve [crush].
    intros * FORALL.
    inversion FORALL as [|? ? EL FORALL2]; subst; clear FORALL.
    unfold upd_asgn. cbn [fold_left]. destruct_match;
    replace ((fold_left
                (fun (a' : PTree.t bool) (el : positive * hash_pred) =>
                   match eval_hash_pred (snd el) a' with
                   | Some p_b => PTree.set (fst el) p_b a'
                   | None => a'
                   end) l a)) with (upd_asgn l a) in * by auto; eauto.
    rewrite IHl; auto.
    rewrite eval_hash_pred_gso; auto.
  Qed.

  Lemma upd_asgn_not_in :
    forall l c1 a,
      ~ In c1 (map fst l) ->
      (upd_asgn l a) ! c1 = a ! c1.
  Proof.
    induction l as [| c l IHl ]; try solve [crush].
    intros * NOTIN. simplify.
    assert (fst c <> c1).
    { unfold not; intros. subst. apply NOTIN; tauto. }
    assert (~ In c1 (map fst l)).
    { unfold not; intros. apply NOTIN; tauto. }
    destruct_match; auto.
    erewrite IHl; eauto. rewrite PTree.gso; auto.
  Qed.

  Definition equiv_list_wf l :=
    Sorted l /\ Forall (fun x => (max_hash_pred (snd x) < fst x)%positive) l.

  Lemma equiv_list_wf_inv :
    forall l a,
      equiv_list_wf (a :: l) ->
      equiv_list_wf l /\ Forall (pl_lt a) l /\ (max_hash_pred (snd a) < fst a)%positive.
  Proof.
    unfold equiv_list_wf; intros * S. inversion S as [A B].
    split; split.
    - inversion A; auto.
    - inversion B; auto.
    - apply Sorted_StronglySorted in A. inversion A; auto.
      unfold Relations_1.Transitive. apply pl_lt_trans.
    - inversion B; auto.
  Qed.

  Lemma equiv_list_wf_nil :
      equiv_list_wf nil.
  Proof.
    unfold equiv_list_wf; split; auto; apply Sorted_nil.
  Qed.

  Lemma sorted_not_in :
    forall A l c1 (c2: A),
      Forall (pl_lt (c1, c2)) l ->
      ~ In c1 (map fst l).
  Proof.
    unfold not; intros.
    eapply list_in_map_inv in H0. inv H0. inv H1.
    eapply Forall_forall in H; eauto.
    destruct x. simpl in H. unfold pl_lt in H. simpl in H. lia.
  Qed.

  Lemma upd_asgn_set_sorted :
    forall l a x,
      Forall (Pos.lt x) (map fst l) ->
      (upd_asgn l a) ! x = a ! x.
  Proof.
    induction l; auto.
    intros. cbn. inv H. erewrite IHl; auto.
    destruct_match; auto; now rewrite PTree.gso by lia.
  Qed.

  Lemma eval_hash_pred_equiv_asgn :
    forall l p a,
      eval_hash_pred p a = Some true ->
      equiv_list_wf l ->
      Forall (fun x => a ! (fst x) = None) l ->
      Forall (fun x => (max_hash_pred p < fst x)%positive) l ->
      eval_hash_pred (fold_left Pand (to_equiv l) p) (upd_asgn l a) = Some true.
  Proof.
    induction l as [|c l IHl]; [crush|]. intros p a EVAL WF FORALL MAX.
    destruct c as [c1 c2]. simpl.
    inversion FORALL as [| ? ? NONE FORALL2]; subst; cbn [fst snd] in *; clear FORALL.
    inversion MAX as [| ? ? MAXC MAX2]; subst; cbn [fst snd] in *; clear MAX.
    eapply equiv_list_wf_inv in WF. inversion WF as [WF2 [FRL MHP]]; subst; clear WF.
    cbn [snd fst] in *. destruct_match.
    - rewrite IHl; eauto.
      apply pand_true2; [|rewrite eval_hash_pred_gso by lia; auto].
      apply eval_equiv2. symmetry; rewrite eval_hash_pred_gso by crush.
      rewrite Heqo. crush. symmetry; apply PTree.gss.
      apply Forall_forall; intros. repeat match goal with H: Forall _ _ |- _ => eapply Forall_forall in H; eauto end.
      unfold pl_lt in *. simplify. rewrite PTree.gso by lia. auto.
      apply Forall_forall; intros. repeat match goal with H: Forall _ _ |- _ => eapply Forall_forall in H; eauto end.
      unfold pl_lt in *. simplify. lia.
    - eapply IHl; eauto. apply pand_true2.
      apply eval_equiv2. rewrite Heqo.
      simpl. auto. auto.
      apply Forall_forall; intros. repeat match goal with H: Forall _ _ |- _ => eapply Forall_forall in H; eauto end.
      unfold pl_lt in *. simplify. lia.
  Qed.

#[local] Opaque max_key.
#[local] Opaque Z.sub.
#[local] Opaque PTree.get.

Lemma check_tree_f_wf_correct :
  forall f,
    check_tree_f_wf f = true -> tree_f_wf f.
Proof.
  unfold check_tree_f_wf, tree_f_wf.
  simplify; auto.
  unfold gt_1; intros.
  assert ((x = 1 \/ 1 < x)%positive) by lia.
  inv H5; auto. rewrite H0 in H3. discriminate.
  repeat (destruct_match; try discriminate; []); auto.
  repeat (destruct_match; try discriminate; []); auto.
Qed.

Lemma check_tree_a_wf_correct :
  forall a,
    check_tree_a_wf a = true -> tree_a_wf a.
Proof.
  unfold check_tree_a_wf, tree_a_wf.
  simplify; auto.
  unfold gt_1; intros.
  assert ((x = 1 \/ 1 < x)%positive) by lia.
  inv H6; auto. rewrite H in H4. discriminate.
  repeat (destruct_match; try discriminate; []); auto.
  repeat (destruct_match; try discriminate; []); auto.
  subst. apply Int63.eqb_spec in H2. apply Int63.eqb_spec in H1. subst.
  auto.
  repeat (destruct_match; try discriminate; []); auto.
  subst. apply Int63.eqb_spec in H2. apply Int63.eqb_spec in H1. subst.
  auto.
Qed.

#[local] Transparent max_key.
#[local] Transparent Z.sub.
#[local] Transparent PTree.get.

Lemma to_smt_l_match_one2 :
  forall a y l0 h0 h r' f' a',
    to_smt_l a (Some (l0, h0, h)) = Some (r', f', a') ->
    match_one y a' ->
    match_one y h.
Proof.
  destruct a. destruct p0; simplify; try discriminate;
    repeat (destruct_match; try discriminate; []); simplify;
    eauto using to_smt_and_match_one2, to_smt_or_match_one2,
                to_smt_imp_match_one2, to_smt_not_match_one2.
Qed.

Lemma to_smt_l_match_one :
  forall a y l0 h0 h r' f' a',
    to_smt_l a (Some (l0, h0, h)) = Some (r', f', a') ->
    match_one y f' ->
    match_one y h0.
Proof.
  destruct a. destruct p0; simplify; try discriminate;
    repeat (destruct_match; try discriminate; []); simplify;
    eauto using to_smt_and_match_one, to_smt_or_match_one,
                to_smt_imp_match_one, to_smt_not_match_one.
Qed.

Lemma to_smt_l_fold_match_one2 :
  forall l y r f a r' f' a',
    fold_right to_smt_l (Some (r, f, a)) l = Some (r', f', a') ->
    match_one y a' ->
    match_one y a.
Proof.
  induction l; crush. remember (fold_right to_smt_l (Some (r, f, a0)) l) as folds.
  destruct folds; [|crush]; [].
  symmetry in Heqfolds.
  destruct p. destruct p. eapply IHl; eauto.
  eapply to_smt_l_match_one2; eauto.
Qed.

Lemma to_smt_l_fold_match_one :
  forall l y r f a r' f' a',
    fold_right to_smt_l (Some (r, f, a)) l = Some (r', f', a') ->
    match_one y f' ->
    match_one y f.
Proof.
  induction l; crush. remember (fold_right to_smt_l (Some (r, f, a0)) l) as folds.
  destruct folds; [|crush]; [].
  symmetry in Heqfolds.
  destruct p. destruct p. eapply IHl; eauto.
  eapply to_smt_l_match_one; eauto.
Qed.

#[local] Opaque Z.sub.

Lemma valid_to_smt : 
  forall p r f a la max la_arr,
    ~ (is_true (Euf_Checker.valid la_arr a f r)) ->
    asgn_transl_spec la la_arr ->
    to_smt max p = Some (r, f, a) ->
    eval_hash_pred (fold_left Pand (to_equiv (snd p)) T) la = Some true ->
    eval_pred_list p la = Some true.
Proof.
  intros.
  destruct (bo_dec (eval_pred_list p la) (Some true)); auto.
  exfalso. eapply H. inv H0. inv H4. assert (DEFAULT1:=H0).
  assert (DEFAULT2:=H5). clear H5. clear H0.
  unfold to_smt in H1. repeat (destruct_match; try discriminate; []).
  simplify.
  unfold is_true.
  unfold eval_pred_list in n. cbn [fst snd] in *.
  apply pand_false in n; auto; [].
  unfold Euf_Checker.valid.
  rewrite Misc.afold_left_and.
  apply forallb_forall. intros.
  eapply to_list_of_list2 in H4; [|lia].
  apply in_app_or in H4.
  (* These are all easy properties that need a bit of extra checking code inside of to_smt. *)
  assert (tree_a_wf h11) by (now apply check_tree_a_wf_correct).
  assert (tree_f_wf h13) by (now apply check_tree_f_wf_correct).
  assert (match_one h11 h8) by (now (eapply AHmatch_one_hash_value; eauto)).
  assert (match_one h13 h9) by (now (eapply match_one_hash_value; eauto)).
  inv H4.
  - eapply fold_to_smt_l_correct; eauto.
    (* This is a proof that all the variables will only be between -1 and 1, which are the only
       values allowed by Zval anyways, so there can't be larger values in the context. *)
    assert (forall y : Int63.int,
               In y l0 ->
               State.Lit.interp
                 (interp_state_var (interp_form_hatom t_i_empty la_arr a)
                                   (interp_form_hatom_bv t_i_empty la_arr a) f) y =
                 true).
    { intros. eapply fold_init_correct with (form_defs := h7) (atom_defs := h6).
      auto. auto. eassumption. eassumption. auto. auto. eauto.
      eapply to_smt_l_fold_match_one; eauto. eapply to_smt_l_fold_match_one2; eauto.
      eapply Heqp5. inversion 1. auto. lia. lia.
    } auto.
  - inv H13; [|inv H4]. eapply interp_eval_pred with (h6 := h6) (h11 := h11) (h13 := h13); eauto;
      try reflexivity; eapply to_smt_l_fold_match_one2; eauto.
Qed.

#[local] Transparent Z.sub.

  Lemma upd_asgn_get :
    forall l y x a,
      (upd_asgn l a) ! y = None ->
      (upd_asgn (l ++ (y, x) :: nil) a) ! y = eval_hash_pred x (upd_asgn l a).
  Proof.
    intros.
    unfold upd_asgn; rewrite fold_left_app; cbn [fold_left].
    cbn [fst snd]; destruct_match; auto; apply PTree.gss.
  Qed.

  Lemma list_app_cons :
    forall A l1 l2 (a: A),
      (l1 ++ a :: nil) ++ l2 = l1 ++ a :: l2.
  Proof. induction l1; crush. Qed.

  Lemma upd_asgn_app :
    forall l1 l2 a,
      upd_asgn (l1 ++ l2) a = upd_asgn l2 (upd_asgn l1 a).
  Proof. intros; unfold upd_asgn; now rewrite fold_left_app. Qed.

  Lemma upd_asgn_pred_In :
    forall p a l1 a0,
      ~ pred_In (fst a) p ->
      eval_hash_pred p (upd_asgn (l1 ++ a :: nil) a0) = eval_hash_pred p (upd_asgn l1 a0).
  Proof.
    induction p; try solve [crush].
    + intros. simpl. rewrite upd_asgn_app. simpl. destruct_match; auto.
      destruct (peq (fst a0) a); subst.
      - exfalso; apply H. constructor.
      - apply PTree.gso; auto.
    + simplify. rewrite IHp2. rewrite IHp1; auto.
      unfold not; intros; apply H. constructor; auto.
      unfold not; intros; apply H. apply pred_In_Pand2; auto.
    + simplify. rewrite IHp2. rewrite IHp1; auto.
      unfold not; intros; apply H. constructor; auto.
      unfold not; intros; apply H. apply pred_In_Por2; auto.
    + simplify. rewrite IHp2. rewrite IHp1; auto.
      unfold not; intros; apply H. constructor; auto.
      unfold not; intros; apply H. apply pred_In_Pimp2; auto.
    + simplify. rewrite IHp; auto.
      unfold not; intros; apply H. constructor; auto.
  Qed.

  Lemma upd_asgn_app1 :
    forall l2 l1 p a,
      Forall (fun x => ~ pred_In (fst x) p) l2 ->
      eval_hash_pred p (upd_asgn (l1 ++ l2) a) = eval_hash_pred p (upd_asgn l1 a).
  Proof.
    induction l2.
    - intros. now rewrite app_nil_r.
    - intros. rewrite <- list_app_cons. inv H.
      rewrite IHl2; auto.
      rewrite upd_asgn_pred_In; auto.
  Qed.

  Lemma eval_hash_pred_upd_asgn_set :
    forall l2 p a a0 a0',
      ~ pred_In a p ->
      Forall (fun x => a <> (fst x) /\ ~ pred_In a (snd x)) l2 ->
      (forall x, x <> a -> a0 ! x = a0' ! x) ->
      eval_hash_pred p (upd_asgn l2 a0) = eval_hash_pred p (upd_asgn l2 a0').
  Proof.
    induction l2; intros.
    crush. eapply eval_hash_pred_except; eauto.
    inversion H0 as [| ? ? [NEQ PRED] FRL ]; subst.
    simpl.
    assert (eval_hash_pred (snd a) a0' = eval_hash_pred (snd a) a1).
    { eapply eval_hash_pred_except; eauto. intros. symmetry. eapply H1. auto. }
    setoid_rewrite H2.
    destruct_match; setoid_rewrite Heqo; eauto.
    eapply IHl2; eauto; intros.
    destruct (peq x (fst a)); subst.
    now rewrite !PTree.gss.
    rewrite !PTree.gso by auto; eauto.
  Qed.

  Lemma eval_hash_pred_upd_asgn_set2 :
    forall l2 p a a0 y,
      ~ pred_In a p ->
      Forall (fun x => a <> (fst x) /\ ~ pred_In a (snd x)) l2 ->
      eval_hash_pred p (upd_asgn l2 (PTree.set a y a0))
        = eval_hash_pred p (upd_asgn l2 a0).
  Proof.
    intros; eapply eval_hash_pred_upd_asgn_set; eauto.
    intros; now apply PTree.gso.
  Qed.

  Lemma upd_asgn_app2 :
    forall l1 l2 p a,
      Forall (fun y => Forall (fun x => fst y <> fst x /\ ~ pred_In (fst y) (snd x)) l2) l1 ->
      (forall x, In x l1 -> ~ pred_In (fst x) p) ->
      eval_hash_pred p (upd_asgn (l1 ++ l2) a) = eval_hash_pred p (upd_asgn l2 a).
  Proof.
    induction l1; auto.
    intros; simpl.
    inv H.
    rewrite IHl1; auto.
    destruct_match; auto.
    apply eval_hash_pred_upd_asgn_set2; auto.
  Qed.

  Lemma sorted_rev :
    forall A R l (b: A) a,
      LocallySorted (Basics.flip R) (l ++ (b :: a :: nil)) ->
      R a b.
  Proof.
    induction l; crush.
    inv H. auto. inv H.
    assert (forall A (a b: list A), nil = a ++ b -> a = nil /\ b = nil).
    { induction a1; crush. }
    apply H in H2. crush.
    eapply IHl. rewrite <- H1. auto.
  Qed.

  Lemma sorted_rev2 :
    forall A R l (b: A) a,
      LocallySorted (Basics.flip R) (l ++ b :: nil) ->
      R a b ->
      LocallySorted (Basics.flip R) (l ++ (b :: a :: nil)).
  Proof.
    induction l; crush.
    constructor. constructor. auto.
    inv H.
    assert (forall A (a b: list A), nil = a ++ b -> a = nil /\ b = nil).
    { induction a1; crush. }
    apply H in H3. crush.
    replace (a :: l ++ b :: a0 :: nil) with ((a :: l ++ b :: nil) ++ a0 :: nil).
    rewrite <- H2.
    replace ((a :: b0 :: l0) ++ a0 :: nil) with (a :: b0 :: (l0 ++ a0 :: nil)).
    constructor; auto.
    replace (b0 :: l0 ++ a0 :: nil) with ((b0 :: l0) ++ a0 :: nil).
    rewrite H2.
    replace ((l ++ b :: nil) ++ a0 :: nil) with (l ++ b :: a0 :: nil).
    eapply IHl; eauto. rewrite <- H2. auto.
    rewrite list_app_cons. auto.
    rewrite app_comm_cons. auto.
    rewrite app_comm_cons. auto.
    rewrite <- app_comm_cons.
    rewrite list_app_cons. auto.
  Qed.

  Lemma sorted_rev3 :
    forall A R l,
      Sorted.LocallySorted R l ->
      Sorted.LocallySorted (Basics.flip R) (@rev A l).
  Proof.
    induction l; crush. inv H. constructor.
    inv H. crush. constructor.
    crush.
    replace ((rev l0 ++ b :: nil) ++ a :: nil) with (rev l0 ++ b :: a :: nil).
    eapply sorted_rev2; eauto.
    now rewrite list_app_cons.
  Qed.

  Lemma sorted_rev4 :
    forall A R l,
      Sorted.Sorted R l ->
      Sorted.Sorted (Basics.flip R) (@rev A l).
  Proof.
    intros. apply Sorted_LocallySorted_iff.
    apply sorted_rev3. apply Sorted_LocallySorted_iff. auto.
  Qed.

  Lemma unnest_predicate_lt_fresh :
    forall p p' fresh fresh' lp,
      unnest_predicate fresh p = (p', lp, fresh') ->
      (fresh <= fresh')%positive.
  Proof.
    induction p; crush; repeat (destruct_match; []); simplify;
    try (pose proof (IHp1 _ _ _ _ Heqp); pose proof (IHp2 _ _ _ _ Heqp4); lia).
    apply IHp in Heqp0; lia.
  Qed.

  Lemma unnest_predicate_lt_in_list :
    forall p p' fresh fresh' lp,
      unnest_predicate fresh p = (p', lp, fresh') ->
      Forall (fun x => (fresh <= fst x < fresh')%positive) lp.
  Proof.
    induction p; crush; repeat (destruct_match; []); simplify.
    - pose proof (IHp1 _ _ _ _ Heqp).
      pose proof (IHp2 _ _ _ _ Heqp4).
      constructor; cbn.
      + apply unnest_predicate_lt_fresh in Heqp4.
        apply unnest_predicate_lt_fresh in Heqp. lia.
      + apply Forall_app; split; apply Forall_forall; intros.
        * eapply Forall_forall in H0; eauto.
          apply unnest_predicate_lt_fresh in Heqp. lia.
        * eapply Forall_forall in H; eauto.
          apply unnest_predicate_lt_fresh in Heqp4. lia.
    - pose proof (IHp1 _ _ _ _ Heqp).
      pose proof (IHp2 _ _ _ _ Heqp4).
      constructor; cbn.
      + apply unnest_predicate_lt_fresh in Heqp4.
        apply unnest_predicate_lt_fresh in Heqp. lia.
      + apply Forall_app; split; apply Forall_forall; intros.
        * eapply Forall_forall in H0; eauto.
          apply unnest_predicate_lt_fresh in Heqp. lia.
        * eapply Forall_forall in H; eauto.
          apply unnest_predicate_lt_fresh in Heqp4. lia.
    - pose proof (IHp1 _ _ _ _ Heqp).
      pose proof (IHp2 _ _ _ _ Heqp4).
      constructor; cbn.
      + apply unnest_predicate_lt_fresh in Heqp4.
        apply unnest_predicate_lt_fresh in Heqp. lia.
      + apply Forall_app; split; apply Forall_forall; intros.
        * eapply Forall_forall in H0; eauto.
          apply unnest_predicate_lt_fresh in Heqp. lia.
        * eapply Forall_forall in H; eauto.
          apply unnest_predicate_lt_fresh in Heqp4. lia.
    - pose proof (IHp _ _ _ _ Heqp0).
      constructor; cbn.
      + apply unnest_predicate_lt_fresh in Heqp0. lia.
      + apply Forall_forall; intros. eapply Forall_forall in H; eauto.
      lia.
  Qed.

  Lemma unnest_predicate_lt_in_list5 :
    forall  p p' fresh fresh' lp,
      unnest_predicate fresh p = (p', lp, fresh') ->
      (max_hash_pred p < fresh)%positive ->
      (max_hash_pred p' < fresh')%positive.
  Proof. induction p; crush; repeat (destruct_match; []); crush. Qed.

  Lemma unnest_predicate_lt_in_list2 :
    forall p p' fresh fresh' lp,
      unnest_predicate fresh p = (p', lp, fresh') ->
      (max_hash_pred p < fresh)%positive ->
      Forall (fun x => (max_hash_pred (snd x) < fst x)%positive) lp.
  Proof.
    induction p; crush; repeat (destruct_match; []); simplify.
    - pose proof (unnest_predicate_lt_fresh _ _ _ _ _ Heqp).
      pose proof (unnest_predicate_lt_fresh _ _ _ _ _ Heqp4).
      pose proof (IHp1 _ _ _ _ Heqp ltac:(lia)) as X.
      pose proof (IHp2 _ _ _ _ Heqp4 ltac:(lia)) as Y.
      pose proof (unnest_predicate_lt_in_list5 _ _ _ _ _ Heqp ltac:(lia)).
      pose proof (unnest_predicate_lt_in_list5 _ _ _ _ _ Heqp4 ltac:(lia)).
      constructor; cbn; [lia|].
      apply Forall_app; split; eapply Forall_forall; intros.
      + eapply Forall_forall in Y; eauto.
      + eapply Forall_forall in X; eauto.
    - pose proof (unnest_predicate_lt_fresh _ _ _ _ _ Heqp).
      pose proof (unnest_predicate_lt_fresh _ _ _ _ _ Heqp4).
      pose proof (IHp1 _ _ _ _ Heqp ltac:(lia)) as X.
      pose proof (IHp2 _ _ _ _ Heqp4 ltac:(lia)) as Y.
      pose proof (unnest_predicate_lt_in_list5 _ _ _ _ _ Heqp ltac:(lia)).
      pose proof (unnest_predicate_lt_in_list5 _ _ _ _ _ Heqp4 ltac:(lia)).
      constructor; cbn; [lia|].
      apply Forall_app; split; eapply Forall_forall; intros.
      + eapply Forall_forall in Y; eauto.
      + eapply Forall_forall in X; eauto.
    - pose proof (unnest_predicate_lt_fresh _ _ _ _ _ Heqp).
      pose proof (unnest_predicate_lt_fresh _ _ _ _ _ Heqp4).
      pose proof (IHp1 _ _ _ _ Heqp ltac:(lia)) as X.
      pose proof (IHp2 _ _ _ _ Heqp4 ltac:(lia)) as Y.
      pose proof (unnest_predicate_lt_in_list5 _ _ _ _ _ Heqp ltac:(lia)).
      pose proof (unnest_predicate_lt_in_list5 _ _ _ _ _ Heqp4 ltac:(lia)).
      constructor; cbn; [lia|].
      apply Forall_app; split; eapply Forall_forall; intros.
      + eapply Forall_forall in Y; eauto.
      + eapply Forall_forall in X; eauto.
    - pose proof (unnest_predicate_lt_fresh _ _ _ _ _ Heqp0).
      pose proof (IHp _ _ _ _ Heqp0 ltac:(lia)) as X.
      pose proof (unnest_predicate_lt_in_list5 _ _ _ _ _ Heqp0 ltac:(lia)).
      constructor; cbn; [lia|auto].
  Qed.

  Lemma unnest_predicate_lt_in_list4 :
    forall p p' fresh fresh' lp y,
      unnest_predicate fresh p = (p', lp, fresh') ->
      pred_In y p' ->
      In y (map fst lp) \/ pred_In y p.
  Proof.
    induction p; crush; repeat (destruct_match; []); simplify.
    - inv H0. tauto.
    - inv H0. tauto.
    - inv H0. tauto.
    - inv H0. tauto.
  Qed.

  Lemma unnest_predicate_lt_in_list3 :
    forall p p' fresh fresh' lp,
      unnest_predicate fresh p = (p', lp, fresh') ->
      Forall (fun x => forall y, pred_In y (snd x) -> In y (map fst lp) \/ pred_In y p) lp.
  Proof.
    induction p; crush; repeat (destruct_match; []); simplify.
    - pose proof (IHp1 _ _ _ _ Heqp).
      pose proof (IHp2 _ _ _ _ Heqp4).
      constructor; intros; cbn [snd] in *.
      + inv H1.
        * pose proof (unnest_predicate_lt_in_list4 _ _ _ _ _ _ Heqp H4).
          inv H1. left. right. rewrite list_append_map. rewrite in_app. tauto.
          right. now apply pred_In_Pand1.
        * pose proof (unnest_predicate_lt_in_list4 _ _ _ _ _ _ Heqp4 H4).
          inv H1. left. right. rewrite list_append_map. rewrite in_app. tauto.
          right. now apply pred_In_Pand2.
      + apply Forall_app; split.
        * apply Forall_forall; intros. eapply Forall_forall in H0; eauto.
          rewrite map_app. apply H0 in H2. inv H2.
          left. right. apply in_app; tauto.
          right. now apply pred_In_Pand2.
        * apply Forall_forall; intros. eapply Forall_forall in H; eauto.
          rewrite map_app. apply H in H2. inv H2.
          left. right. apply in_app; tauto.
          right. now apply pred_In_Pand1.
    - pose proof (IHp1 _ _ _ _ Heqp).
      pose proof (IHp2 _ _ _ _ Heqp4).
      constructor; intros; cbn [snd] in *.
      + inv H1.
        * pose proof (unnest_predicate_lt_in_list4 _ _ _ _ _ _ Heqp H4).
          inv H1. left. right. rewrite list_append_map. rewrite in_app. tauto.
          right. now apply pred_In_Por1.
        * pose proof (unnest_predicate_lt_in_list4 _ _ _ _ _ _ Heqp4 H4).
          inv H1. left. right. rewrite list_append_map. rewrite in_app. tauto.
          right. now apply pred_In_Por2.
      + apply Forall_app; split.
        * apply Forall_forall; intros. eapply Forall_forall in H0; eauto.
          rewrite map_app. apply H0 in H2. inv H2.
          left. right. apply in_app; tauto.
          right. now apply pred_In_Por2.
        * apply Forall_forall; intros. eapply Forall_forall in H; eauto.
          rewrite map_app. apply H in H2. inv H2.
          left. right. apply in_app; tauto.
          right. now apply pred_In_Por1.
    - pose proof (IHp1 _ _ _ _ Heqp).
      pose proof (IHp2 _ _ _ _ Heqp4).
      constructor; intros; cbn [snd] in *.
      + inv H1.
        * pose proof (unnest_predicate_lt_in_list4 _ _ _ _ _ _ Heqp H4).
          inv H1. left. right. rewrite list_append_map. rewrite in_app. tauto.
          right. now apply pred_In_Pimp1.
        * pose proof (unnest_predicate_lt_in_list4 _ _ _ _ _ _ Heqp4 H4).
          inv H1. left. right. rewrite list_append_map. rewrite in_app. tauto.
          right. now apply pred_In_Pimp2.
      + apply Forall_app; split.
        * apply Forall_forall; intros. eapply Forall_forall in H0; eauto.
          rewrite map_app. apply H0 in H2. inv H2.
          left. right. apply in_app; tauto.
          right. now apply pred_In_Pimp2.
        * apply Forall_forall; intros. eapply Forall_forall in H; eauto.
          rewrite map_app. apply H in H2. inv H2.
          left. right. apply in_app; tauto.
          right. now apply pred_In_Pimp1.
    - pose proof (IHp _ _ _ _ Heqp0).
      constructor; intros; cbn [snd] in *.
      + inv H0.
        pose proof (unnest_predicate_lt_in_list4 _ _ _ _ _ _ Heqp0 H3).
        inv H0. tauto.
        right. now apply pred_In_Pnot.
      + apply Forall_forall; intros. eapply Forall_forall in H0; eauto.
          apply H0 in H1. inv H1; [tauto|].
          right. now apply pred_In_Pnot.
  Qed.

  Lemma unnest_predicate_sorted :
    forall p p' lp fresh' fresh,
      unnest_predicate fresh p = (p', lp, fresh') ->
      Sorted.Sorted (Basics.flip pl_lt) lp.
  Proof.
    induction p; crush; try apply Sorted_nil;
    repeat (destruct_match; []); simplify.
    - constructor.
      eapply SetoidList.SortA_app with (eqA := eq); auto.
      eapply IHp2; eassumption.
      eapply IHp1; eassumption.
      intros. apply SetoidList.InA_alt in H; simplify.
      apply SetoidList.InA_alt in H0; simplify.
      unfold Basics.flip.
      pose proof (unnest_predicate_lt_in_list _ _ _ _ _ Heqp).
      pose proof (unnest_predicate_lt_in_list _ _ _ _ _ Heqp4).
      eapply Forall_forall in H; [|eassumption].
      eapply Forall_forall in H0; [|eassumption].
      destruct x, x0; unfold pl_lt; cbn [snd fst] in *; lia.
      pose proof (unnest_predicate_lt_in_list _ _ _ _ _ Heqp).
      pose proof (unnest_predicate_lt_in_list _ _ _ _ _ Heqp4).
      apply SetoidList.InfA_app.
      + apply SetoidList.InA_InfA with (eqA := eq); auto; intros.
        apply SetoidList.InA_alt in H1; simplify.
        eapply Forall_forall in H0; [|eassumption].
        unfold Basics.flip, pl_lt; destruct x; cbn [snd fst] in *. lia.
      + apply SetoidList.InA_InfA with (eqA := eq); auto; intros.
        apply SetoidList.InA_alt in H1; simplify.
        eapply Forall_forall in H; [|eassumption].
        unfold Basics.flip, pl_lt; destruct x; cbn [snd fst] in *.
        pose proof (unnest_predicate_lt_fresh _ _ _ _ _ Heqp4). lia.
    - constructor.
      eapply SetoidList.SortA_app with (eqA := eq); auto.
      eapply IHp2; eassumption.
      eapply IHp1; eassumption.
      intros. apply SetoidList.InA_alt in H; simplify.
      apply SetoidList.InA_alt in H0; simplify.
      unfold Basics.flip.
      pose proof (unnest_predicate_lt_in_list _ _ _ _ _ Heqp).
      pose proof (unnest_predicate_lt_in_list _ _ _ _ _ Heqp4).
      eapply Forall_forall in H; [|eassumption].
      eapply Forall_forall in H0; [|eassumption].
      destruct x, x0; unfold pl_lt; cbn [snd fst] in *; lia.
      pose proof (unnest_predicate_lt_in_list _ _ _ _ _ Heqp).
      pose proof (unnest_predicate_lt_in_list _ _ _ _ _ Heqp4).
      apply SetoidList.InfA_app.
      + apply SetoidList.InA_InfA with (eqA := eq); auto; intros.
        apply SetoidList.InA_alt in H1; simplify.
        eapply Forall_forall in H0; [|eassumption].
        unfold Basics.flip, pl_lt; destruct x; cbn [snd fst] in *. lia.
      + apply SetoidList.InA_InfA with (eqA := eq); auto; intros.
        apply SetoidList.InA_alt in H1; simplify.
        eapply Forall_forall in H; [|eassumption].
        unfold Basics.flip, pl_lt; destruct x; cbn [snd fst] in *.
        pose proof (unnest_predicate_lt_fresh _ _ _ _ _ Heqp4). lia.
    - constructor.
      eapply SetoidList.SortA_app with (eqA := eq); auto.
      eapply IHp2; eassumption.
      eapply IHp1; eassumption.
      intros. apply SetoidList.InA_alt in H; simplify.
      apply SetoidList.InA_alt in H0; simplify.
      unfold Basics.flip.
      pose proof (unnest_predicate_lt_in_list _ _ _ _ _ Heqp).
      pose proof (unnest_predicate_lt_in_list _ _ _ _ _ Heqp4).
      eapply Forall_forall in H; [|eassumption].
      eapply Forall_forall in H0; [|eassumption].
      destruct x, x0; unfold pl_lt; cbn [snd fst] in *; lia.
      pose proof (unnest_predicate_lt_in_list _ _ _ _ _ Heqp).
      pose proof (unnest_predicate_lt_in_list _ _ _ _ _ Heqp4).
      apply SetoidList.InfA_app.
      + apply SetoidList.InA_InfA with (eqA := eq); auto; intros.
        apply SetoidList.InA_alt in H1; simplify.
        eapply Forall_forall in H0; [|eassumption].
        unfold Basics.flip, pl_lt; destruct x; cbn [snd fst] in *. lia.
      + apply SetoidList.InA_InfA with (eqA := eq); auto; intros.
        apply SetoidList.InA_alt in H1; simplify.
        eapply Forall_forall in H; [|eassumption].
        unfold Basics.flip, pl_lt; destruct x; cbn [snd fst] in *.
        pose proof (unnest_predicate_lt_fresh _ _ _ _ _ Heqp4). lia.
    - constructor.
      eapply IHp; eassumption.
      pose proof (unnest_predicate_lt_in_list _ _ _ _ _ Heqp0).
      apply SetoidList.InA_InfA with (eqA := eq); auto; intros.
      apply SetoidList.InA_alt in H0; simplify.
      eapply Forall_forall in H; [|eassumption].
      unfold Basics.flip, pl_lt; destruct x; cbn [snd fst] in *. lia.
  Qed.

  Lemma to_equiv_rev :
    forall l, rev (to_equiv l) = to_equiv (rev l).
  Proof. unfold to_equiv; intros. rewrite map_rev. auto. Qed.

  Lemma unnest_predicate_sorted_app :
    forall p1 p l p0 p3 p4 l0 fresh p2,
      unnest_predicate fresh p1 = (p, l, p0) ->
      unnest_predicate p0 p2 = (p3, l0, p4) ->
      Sorted.Sorted (Basics.flip pl_lt) l ->
      Sorted.Sorted (Basics.flip pl_lt) l0 ->
      Sorted.Sorted (Basics.flip pl_lt) (l0 ++ l).
  Proof.
    intros * NEST1 NEST2 SORT1 SORT2.
    apply SetoidList.SortA_app with (eqA := eq); auto.
    intros.
    apply SetoidList.InA_alt in H.
    apply SetoidList.InA_alt in H0. simplify.
    pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST1).
    pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST2).
    eapply Forall_forall in H; [|eassumption].
    eapply Forall_forall in H1; [|eassumption].
    unfold Basics.flip, pl_lt. lia.
  Qed.

  Lemma unnest_predicate_equiv_list :
    forall p p0 p1 p2 p3 p4 l l0 fresh,
      unnest_predicate fresh p1 = (p, l, p0) ->
      unnest_predicate p0 p2 = (p3, l0, p4) ->
      (Pos.max (max_hash_pred p1) (max_hash_pred p2) < fresh)%positive ->
      equiv_list_wf (rev (l0 ++ l)).
  Proof.
    intros * NEST1 NEST2 MAX.
    unfold equiv_list_wf. split. unfold Sorted.
    pose proof (unnest_predicate_sorted _ _ _ _ _ NEST1).
    pose proof (unnest_predicate_sorted _ _ _ _ _ NEST2).
    replace pl_lt with (Basics.flip (Basics.flip (@pl_lt predicate))) by (unfold Basics.flip; auto).
    apply sorted_rev4.
    eapply unnest_predicate_sorted_app; eauto.
    apply Forall_rev; apply Forall_app; split;
    eapply unnest_predicate_lt_in_list2; eauto.
    pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1).
    lia. lia.
  Qed.

  Lemma pred_in_fold :
    forall A l p y,
      @pred_In A p (fold_left Pand l y) ->
      (exists i, In i l /\ pred_In p i) \/ pred_In p y.
  Proof.
    induction l.
    intros. simplify. tauto.
    intros. simpl in *. apply IHl in H.
    inv H; simplify. left. econstructor.
    constructor. right. eauto. auto.
    inv H0; try tauto.
    do 2 econstructor; split; try eassumption; tauto.
  Qed.

  Lemma max_hash_pred_lt :
    forall p l,
      pred_In l p ->
      (l <= max_hash_pred p)%positive.
  Proof.
    induction p; intros; try inv H; crush;
      try (apply IHp1 in H2; lia);
      apply IHp2 in H2; lia.
  Qed.

  Lemma unnest_predicate_not_in :
    forall p p0 p1 p2 p3 p4 l l0 fresh y,
      unnest_predicate fresh p1 = (p, l, p0) ->
      unnest_predicate p0 p2 = (p3, l0, p4) ->
      (Pos.max (max_hash_pred p1) (max_hash_pred p2) < fresh)%positive ->
      Forall (fun x : positive * hash_pred =>
        ~ pred_In (fst x) (fold_left Pand (to_equiv (l0 ++ l)) T))
        ((p4, y) :: nil).
  Proof.
    intros * NEST1 NEST2 MAX.
    constructor; [|constructor]. cbn [fst]. unfold not; intros.
    apply pred_in_fold in H. inv H; inv H0;
    simplify. unfold to_equiv in H0. apply map_in_some in H0. simplify.
    apply in_app_or in H0; inv H0.
    pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1) as TEMP.
    pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST2 ltac:(lia)).
    pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST2).
    eapply Forall_forall in H0; [|eassumption].
    eapply Forall_forall in H2; [|eassumption]. destruct x0. cbn [snd fst] in *.
    apply max_hash_pred_lt in H1. unfold equiv in H1.
    unfold max_hash_pred in H1. fold max_hash_pred in H1. lia.
    pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST1 ltac:(lia)).
    pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST1).
    eapply Forall_forall in H0; [|eassumption].
    eapply Forall_forall in H2; [|eassumption]. destruct x0. cbn [snd fst] in *.
    apply max_hash_pred_lt in H1. unfold equiv in H1.
    unfold max_hash_pred in H1. fold max_hash_pred in H1.
    pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2). lia.
  Qed.

  Lemma unnest_predicate_not_in4 :
    forall p p0 p1 l fresh y,
      unnest_predicate fresh p1 = (p, l, p0) ->
      (max_hash_pred p1 < fresh)%positive ->
      Forall (fun x : positive * hash_pred =>
        ~ pred_In (fst x) (fold_left Pand (to_equiv l) T))
        ((p0, y) :: nil).
  Proof.
    intros * NEST1 MAX.
    constructor; [|constructor]. cbn [fst]. unfold not; intros.
    apply pred_in_fold in H. inv H; inv H0;
    simplify. unfold to_equiv in H0. apply map_in_some in H0. simplify.
    pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST1 ltac:(lia)).
    pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST1).
    eapply Forall_forall in H; [|eassumption].
    eapply Forall_forall in H2; [|eassumption]. destruct x0. cbn [snd fst] in *.
    apply max_hash_pred_lt in H1. unfold equiv in H1.
    unfold max_hash_pred in H1. fold max_hash_pred in H1. lia.
  Qed.

  Lemma unnest_predicate_in_pred :
    forall fresh p1 p l p0,
      unnest_predicate fresh p1 = (p, l, p0) ->
      (max_hash_pred p1 < fresh)%positive ->
      ~ pred_In p0 p.
  Proof.
    destruct p1; unfold not; intros.
    - inv H. inv H1.
    - inv H. inv H1.
    - inv H. inv H1.
    - inv H. crush. inv H1. lia.
    - simplify. repeat (destruct_match; []). simplify.
      inv H1. lia.
    - simplify. repeat (destruct_match; []). simplify.
      inv H1. lia.
    - simplify. repeat (destruct_match; []). simplify.
      inv H1. lia.
    - simplify. repeat (destruct_match; []). simplify.
      inv H1. lia.
  Qed.

  Lemma unnest_predicate_in_pred2 :
    forall fresh p1 p l p0,
      unnest_predicate fresh p1 = (p, l, p0) ->
      (max_hash_pred p1 < fresh)%positive ->
      (max_hash_pred p < p0)%positive.
  Proof.
    intros.
    destruct p1; crush.
    - repeat (destruct_match; []); simplify; lia.
    - repeat (destruct_match; []); simplify; lia.
    - repeat (destruct_match; []); simplify; lia.
    - repeat (destruct_match; []); simplify; lia.
  Qed.

  Lemma unnest_predicate_forall_none :
    forall p1 p2 p0 p3 l0 l p4 fresh p a,
      unnest_predicate fresh p1 = (p, l, p0) ->
      unnest_predicate p0 p2 = (p3, l0, p4) ->
      eval_hash_pred p1 a = eval_pred_list (p, l) (upd_asgn (rev l) a) ->
      eval_hash_pred p2 a = eval_pred_list (p3, l0) (upd_asgn (rev l0) a) ->
      (forall y : positive, (fresh <= y)%positive -> a ! y = None) ->
      (max_hash_pred (p1 ∧ p2) < fresh)%positive ->
      Forall (fun x : positive * predicate => a ! (fst x) = None) (rev (l0 ++ l)).
  Proof.
    intros * NEST1 NEST2 EVAL1 EVAL2 GTMAX MAXHASH.
    apply Forall_forall; intros. apply GTMAX.
    unfold max_hash_pred in *; fold max_hash_pred in *.
    pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2) as X3.
    pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1) as X4.
    pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST2 ltac:(lia)) as X1.
    pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST2) as X2.
    pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST1 ltac:(lia)) as Y1.
    pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST1) as Y2.
    apply in_rev in H. apply in_app in H. inv H.
    eapply Forall_forall in X1; eauto; [].
    eapply Forall_forall in X2; eauto; []. lia.
    eapply Forall_forall in Y1; eauto; [].
    eapply Forall_forall in Y2; eauto; []. lia.
  Qed.

  Lemma unnest_predicate_forall_gt1 :
    forall p1 p2 p0 p3 l0 l p4 fresh p a,
      unnest_predicate fresh p1 = (p, l, p0) ->
      unnest_predicate p0 p2 = (p3, l0, p4) ->
      eval_hash_pred p1 a = eval_pred_list (p, l) (upd_asgn (rev l) a) ->
      eval_hash_pred p2 a = eval_pred_list (p3, l0) (upd_asgn (rev l0) a) ->
      (forall y : positive, (fresh <= y)%positive -> a ! y = None) ->
      (max_hash_pred (p1 ∧ p2) < fresh)%positive ->
      Forall (fun x : positive * predicate => (1 < fst x)%positive) (rev (l0 ++ l)).
  Proof.
    intros * NEST1 NEST2 EVAL1 EVAL2 GTMAX MAXHASH.
    apply Forall_forall; intros.
    unfold max_hash_pred in *; fold max_hash_pred in *.
    pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2) as X3.
    pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1) as X4.
    pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST2 ltac:(lia)) as X1.
    pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST2) as X2.
    pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST1 ltac:(lia)) as Y1.
    pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST1) as Y2.
    apply in_rev in H. apply in_app in H. inv H.
    eapply Forall_forall in X1; eauto; [].
    eapply Forall_forall in X2; eauto; []. lia.
    eapply Forall_forall in Y1; eauto; [].
    eapply Forall_forall in Y2; eauto; []. lia.
  Qed.

  Lemma unnest_predicate_not_in3 :
    forall p1 p0 l fresh p a,
      unnest_predicate fresh p1 = (p, l, p0) ->
      eval_hash_pred p1 a = eval_pred_list (p, l) (upd_asgn (rev l) a) ->
      (forall y : positive, (fresh <= y)%positive -> a ! y = None) ->
      (max_hash_pred p1 < fresh)%positive ->
      ~ In p0 (map fst (rev l)).
  Proof.
    intros * NEST1 EVAL1 GTMAX MAXHASH.
    unfold not; intros.
    pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST1).
    pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST1).
    pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1).
    apply map_in_some in H. simplify.
    eapply in_rev in H.
    eapply Forall_forall in H0; eauto.
    eapply Forall_forall in H1; eauto.
    destruct x; cbn [fst snd max_hash_pred] in *.
    lia.
  Qed.

  Lemma unnest_predicate_not_in2 :
    forall p1 p2 p0 p3 l0 l p4 fresh p a,
      unnest_predicate fresh p1 = (p, l, p0) ->
      unnest_predicate p0 p2 = (p3, l0, p4) ->
      eval_hash_pred p1 a = eval_pred_list (p, l) (upd_asgn (rev l) a) ->
      eval_hash_pred p2 a = eval_pred_list (p3, l0) (upd_asgn (rev l0) a) ->
      (forall y : positive, (fresh <= y)%positive -> a ! y = None) ->
      (max_hash_pred (p1 ∧ p2) < fresh)%positive ->
      ~ In p4 (map fst (rev l ++ rev l0)).
  Proof.
    intros * NEST1 NEST2 EVAL1 EVAL2 GTMAX MAXHASH.
    unfold not; intros.

    pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1) as TMP. cbn [max_hash_pred] in *.
    pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST2 ltac:(lia)).
    pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST2).
    pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST1 ltac:(lia)).
    pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST1).
    apply map_in_some in H. simplify.
    apply in_app_or in H. inv H.
    eapply in_rev in H4.
    eapply Forall_forall in H2; eauto.
    eapply Forall_forall in H3; eauto.
    pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2).
    destruct x; cbn [fst snd] in *. lia.
    eapply in_rev in H4.
    eapply Forall_forall in H0; eauto.
    eapply Forall_forall in H1; eauto.
    pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1).
    destruct x; cbn [fst snd] in *. lia.
  Qed.

  Lemma eval_equiv_added :
    forall p1 p2 p0 p3 l0 l p4 fresh p a,
      unnest_predicate fresh p1 = (p, l, p0) ->
      unnest_predicate p0 p2 = (p3, l0, p4) ->
      eval_hash_pred p1 a = eval_pred_list (p, l) (upd_asgn (rev l) a) ->
      eval_hash_pred p2 a = eval_pred_list (p3, l0) (upd_asgn (rev l0) a) ->
      (forall y : positive, (fresh <= y)%positive -> a ! y = None) ->
      (max_hash_pred (p1 ∧ p2) < fresh)%positive ->
      eval_hash_pred (equiv (Pbase p4) (p ∧ p3)) (upd_asgn (rev l ++ rev l0 ++ (p4, p ∧ p3) :: nil) a) = Some true.
  Proof.
    intros * NEST1 NEST2 EVAL1 EVAL2 GTMAX MAXHASH.
    apply eval_equiv2. rewrite eval_hash_pred_get.
    rewrite app_assoc.
    rewrite upd_asgn_get.
    symmetry. rewrite upd_asgn_app1; auto.
    constructor; [|constructor]; simpl.
    pose proof NEST1 as X1. pose proof NEST2 as X2.
    eapply unnest_predicate_in_pred2 in X1.
    eapply unnest_predicate_in_pred2 in X2.

    2: { unfold max_hash_pred in *; fold max_hash_pred in *.
    pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1).
    pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2). lia.
    }

    2: { unfold max_hash_pred in *; fold max_hash_pred in *.
    pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1).
    pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2). lia.
    }

    pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1).
    pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2).
    unfold not; intros. apply max_hash_pred_lt in H1.
    cbn [max_hash_pred] in H1. lia.

    rewrite upd_asgn_not_in. eapply GTMAX. unfold max_hash_pred in *. fold max_hash_pred in *.
    pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1).
    pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2). lia.
    eapply unnest_predicate_not_in2; eauto.
  Qed.

  Lemma eval_equiv_added_Por :
    forall p1 p2 p0 p3 l0 l p4 fresh p a,
      unnest_predicate fresh p1 = (p, l, p0) ->
      unnest_predicate p0 p2 = (p3, l0, p4) ->
      eval_hash_pred p1 a = eval_pred_list (p, l) (upd_asgn (rev l) a) ->
      eval_hash_pred p2 a = eval_pred_list (p3, l0) (upd_asgn (rev l0) a) ->
      (forall y : positive, (fresh <= y)%positive -> a ! y = None) ->
      (max_hash_pred (p1 ∨ p2) < fresh)%positive ->
      eval_hash_pred (equiv (Pbase p4) (p ∨ p3)) (upd_asgn (rev l ++ rev l0 ++ (p4, p ∨ p3) :: nil) a) = Some true.
  Proof.
    intros * NEST1 NEST2 EVAL1 EVAL2 GTMAX MAXHASH.
    apply eval_equiv2. rewrite eval_hash_pred_get.
    rewrite app_assoc.
    rewrite upd_asgn_get.
    symmetry. rewrite upd_asgn_app1; auto.
    constructor; [|constructor]; simpl.
    pose proof NEST1 as X1. pose proof NEST2 as X2.
    eapply unnest_predicate_in_pred2 in X1.
    eapply unnest_predicate_in_pred2 in X2.

    2: { unfold max_hash_pred in *; fold max_hash_pred in *.
    pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1).
    pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2). lia.
    }

    2: { unfold max_hash_pred in *; fold max_hash_pred in *.
    pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1).
    pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2). lia.
    }

    pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1).
    pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2).
    unfold not; intros. apply max_hash_pred_lt in H1.
    cbn [max_hash_pred] in H1. lia.

    rewrite upd_asgn_not_in. eapply GTMAX. unfold max_hash_pred in *. fold max_hash_pred in *.
    pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1).
    pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2). lia.
    eapply unnest_predicate_not_in2; eauto.
  Qed.

  Lemma eval_equiv_added_Pimp :
    forall p1 p2 p0 p3 l0 l p4 fresh p a,
      unnest_predicate fresh p1 = (p, l, p0) ->
      unnest_predicate p0 p2 = (p3, l0, p4) ->
      eval_hash_pred p1 a = eval_pred_list (p, l) (upd_asgn (rev l) a) ->
      eval_hash_pred p2 a = eval_pred_list (p3, l0) (upd_asgn (rev l0) a) ->
      (forall y : positive, (fresh <= y)%positive -> a ! y = None) ->
      (max_hash_pred (p1 → p2) < fresh)%positive ->
      eval_hash_pred (equiv (Pbase p4) (p → p3)) (upd_asgn (rev l ++ rev l0 ++ (p4, p → p3) :: nil) a) = Some true.
  Proof.
    intros * NEST1 NEST2 EVAL1 EVAL2 GTMAX MAXHASH.
    apply eval_equiv2. rewrite eval_hash_pred_get.
    rewrite app_assoc.
    rewrite upd_asgn_get.
    symmetry. rewrite upd_asgn_app1; auto.
    constructor; [|constructor]; simpl.
    pose proof NEST1 as X1. pose proof NEST2 as X2.
    eapply unnest_predicate_in_pred2 in X1.
    eapply unnest_predicate_in_pred2 in X2.

    2: { unfold max_hash_pred in *; fold max_hash_pred in *.
    pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1).
    pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2). lia.
    }

    2: { unfold max_hash_pred in *; fold max_hash_pred in *.
    pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1).
    pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2). lia.
    }

    pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1).
    pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2).
    unfold not; intros. apply max_hash_pred_lt in H1.
    cbn [max_hash_pred] in H1. lia.

    rewrite upd_asgn_not_in. eapply GTMAX. unfold max_hash_pred in *. fold max_hash_pred in *.
    pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1).
    pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2). lia.
    eapply unnest_predicate_not_in2; eauto.
  Qed.

  Lemma unnest_predicate_correct_Pand :
    forall p1 p2 p0 p3 l0 l p4 fresh p a,
      unnest_predicate fresh p1 = (p, l, p0) ->
      unnest_predicate p0 p2 = (p3, l0, p4) ->
      eval_hash_pred p1 a = eval_pred_list (p, l) (upd_asgn (rev l) a) ->
      eval_hash_pred p2 a = eval_pred_list (p3, l0) (upd_asgn (rev l0) a) ->
      (forall y, (fresh <= y)%positive -> a ! y = None) ->
      (max_hash_pred (p1 ∧ p2) < fresh)%positive ->
      eval_hash_pred (p1 ∧ p2) a =
        eval_hash_pred (Pbase p4 ∧ fold_left Pand (to_equiv (l0 ++ l)) (T ∧ equiv (Pbase p4) (p ∧ p3)))
                       (upd_asgn (rev (l0 ++ l) ++ (p4, p ∧ p3) :: nil) a).
  Proof.
    intros * NEST1 NEST2 EVAL1 EVAL2 GTMAX MAXHASH.
    assert (eval_hash_pred (fold_left Pand (to_equiv (l0 ++ l)) (T ∧ equiv (Pbase p4) (p ∧ p3)))
            (upd_asgn (rev l ++ rev l0 ++ (p4, p ∧ p3) :: nil) a) = Some true).
    { apply eval_hash_pred_fold_Pand2 with (x := T).
      rewrite app_assoc.
      rewrite upd_asgn_app1; [|eapply unnest_predicate_not_in; eauto].
      replace (rev l ++ rev l0) with (rev (l0  ++ l)) by (rewrite rev_app_distr; auto).
      apply fold_left_Pand_rev.
      rewrite to_equiv_rev.
      apply eval_hash_pred_equiv_asgn; auto.
      eapply unnest_predicate_equiv_list; eauto.
      eapply unnest_predicate_forall_none; eauto.
      eapply unnest_predicate_forall_gt1; eauto.
      rewrite eval_hash_pred_T_Pand.
      eapply eval_equiv_added; eauto.
    }
    assert (eval_hash_pred (p1 ∧ p2) a = eval_hash_pred (Pbase p4)
            (upd_asgn ((rev l ++ rev l0) ++ (p4, p ∧ p3) :: nil) a)).
    { rewrite eval_hash_pred_get.
      rewrite upd_asgn_get.
      2: { rewrite upd_asgn_not_in by (eapply unnest_predicate_not_in2; eauto).
      eapply GTMAX. unfold max_hash_pred in *. fold max_hash_pred in *.
      pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1).
      pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2). lia.
      }
      apply eval_hash_pred_pand.
      { rewrite EVAL1. unfold eval_pred_list. cbn [snd fst].
        rewrite upd_asgn_app1.
        { rewrite eval_hash_pred_T_Pand2; auto.
          apply fold_left_Pand_rev. rewrite to_equiv_rev.
          apply eval_hash_pred_equiv_asgn; auto.
          { unfold equiv_list_wf, Sorted; split.
            { replace pl_lt with (Basics.flip (Basics.flip (@pl_lt predicate))) by auto.
              apply sorted_rev4. eapply unnest_predicate_sorted; eauto. }
            { apply Forall_rev. eapply unnest_predicate_lt_in_list2; eauto. cbn [max_hash_pred] in *; lia. } }
          { exploit unnest_predicate_forall_none. apply NEST1. apply NEST2.
            all: eauto. intros. cbn. rewrite rev_app_distr in H0.
            apply Forall_app in H0; crush. }
          { exploit unnest_predicate_forall_gt1. apply NEST1. apply NEST2.
            all: eauto. intros. cbn. rewrite rev_app_distr in H0.
            apply Forall_app in H0; crush. } }
        { apply Forall_rev. apply Forall_forall; intros.
          cbn [max_hash_pred] in *.
          pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1) as TMP.
          pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST2 ltac:(lia)).
          pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST2).
          pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2).
          pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1).
          eapply Forall_forall in H1; eauto. eapply Forall_forall in H2; eauto.
          unfold not; intros. apply max_hash_pred_lt in H5. destruct x; cbn [fst snd] in *.
          unfold max_hash_pred in *; fold max_hash_pred in *.
          pose proof (unnest_predicate_in_pred2 _ _ _ _ _ NEST1).
          pose proof (unnest_predicate_in_pred2 _ _ _ _ _ NEST2).
          lia.
        } }
        { rewrite EVAL2. unfold eval_pred_list. cbn [snd fst].
          rewrite upd_asgn_app2.
          { rewrite eval_hash_pred_T_Pand2; auto.
            apply fold_left_Pand_rev. rewrite to_equiv_rev.
            apply eval_hash_pred_equiv_asgn; auto.
            { unfold equiv_list_wf, Sorted; split.
              { replace pl_lt with (Basics.flip (Basics.flip (@pl_lt predicate))) by auto.
                apply sorted_rev4. eapply unnest_predicate_sorted; eauto. }
              { apply Forall_rev. eapply unnest_predicate_lt_in_list2; eauto.
                pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1).
                cbn [max_hash_pred] in *; lia. } }
            { exploit unnest_predicate_forall_none. apply NEST1. apply NEST2.
              all: eauto. intros. cbn. rewrite rev_app_distr in H0.
              apply Forall_app in H0; crush. }
            { exploit unnest_predicate_forall_gt1. apply NEST1. apply NEST2.
              all: eauto. intros. cbn. rewrite rev_app_distr in H0.
              apply Forall_app in H0; crush. } }
          { apply Forall_rev. apply Forall_forall; intros.
            apply Forall_rev. apply Forall_forall; intros. split.
            cbn [max_hash_pred] in *.
            pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1) as TMP.
            pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST2 ltac:(lia)) as X2.
            pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST2) as Y2.
            pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST1 ltac:(lia)) as X1.
            pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST1) as Y1.
            pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2) as Z2.
            pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1) as Z1.
            destruct x, x0. cbn [fst snd] in *.
            eapply Forall_forall in X2; eauto. eapply Forall_forall in Y2; eauto.
            eapply Forall_forall in X1; eauto. eapply Forall_forall in Y1; eauto.
            cbn [fst snd] in *. lia.

            pose proof (unnest_predicate_lt_in_list3 _ _ _ _ _ NEST2) as X.
            unfold not; intros Y. eapply Forall_forall in X; eauto.
            cbn [max_hash_pred] in *.
            pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1) as TMP.
            pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST2 ltac:(lia)) as X2.
            pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST2) as Y2.
            pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST1 ltac:(lia)) as X1.
            pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST1) as Y1.
            pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2) as Z2.
            pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1) as Z1.
            eapply Forall_forall in X2; eauto. eapply Forall_forall in Y2; eauto.
            eapply Forall_forall in X1; eauto. eapply Forall_forall in Y1; eauto.
            destruct x, x0. cbn [fst snd] in *.
            unfold max_hash_pred in *; fold max_hash_pred in *.
            exploit unnest_predicate_in_pred2; eauto. lia; intros.
            exploit unnest_predicate_in_pred2. eapply NEST1. lia. intros.
            pose proof Y as YY. apply X in YY. inv YY.
            eapply map_in_some in H4; simplify. destruct x; simplify.
            eapply max_hash_pred_lt in Y.
            pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST2) as X22.
            pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST2) as Y22.
            eapply Forall_forall in X22; eauto. eapply Forall_forall in Y22; eauto.
            cbn [fst snd] in *.
            cbn [max_hash_pred] in *.
            lia. lia.
            eapply max_hash_pred_lt in H4. lia.
          }
          { intros. apply in_rev in H0. destruct x; cbn [fst snd] in *.
            unfold not; intros Y.
            cbn [max_hash_pred] in *.
            pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST1 ltac:(lia)) as X1.
            pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST1) as Y1.
            pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1) as Z1.
            eapply Forall_forall in X1; eauto. eapply Forall_forall in Y1; eauto.
            cbn [max_hash_pred fst snd] in *.
            exploit unnest_predicate_in_pred2; eauto. lia; intros. intros.
            exploit unnest_predicate_in_pred2. eapply NEST1. lia. intros.
            exploit unnest_predicate_lt_in_list4. eapply NEST2. eauto. intros. inv H3.
            eapply map_in_some in H4; simplify.
            destruct x.
            cbn [max_hash_pred fst snd] in *.
            pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST2 ltac:(lia)) as X2.
            pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST2) as Y2.
            pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2) as Z2.
            eapply Forall_forall in X2; eauto. eapply Forall_forall in Y2; eauto.
            cbn [max_hash_pred fst snd] in *.
            eapply max_hash_pred_lt in Y. lia.
            eapply max_hash_pred_lt in H4. lia.
          } } }
    symmetry; rewrite eval_hash_pred_T_Pand2; rewrite rev_app_distr;
      try solve [rewrite <- app_assoc; auto]; auto.
  Qed.

  Lemma unnest_predicate_correct_Por :
    forall p1 p2 p0 p3 l0 l p4 fresh p a,
      unnest_predicate fresh p1 = (p, l, p0) ->
      unnest_predicate p0 p2 = (p3, l0, p4) ->
      eval_hash_pred p1 a = eval_pred_list (p, l) (upd_asgn (rev l) a) ->
      eval_hash_pred p2 a = eval_pred_list (p3, l0) (upd_asgn (rev l0) a) ->
      (forall y, (fresh <= y)%positive -> a ! y = None) ->
      (max_hash_pred (p1 ∨ p2) < fresh)%positive ->
      eval_hash_pred (p1 ∨ p2) a =
        eval_hash_pred (Pbase p4 ∧ fold_left Pand (to_equiv (l0 ++ l)) (T ∧ equiv (Pbase p4) (p ∨ p3)))
                       (upd_asgn (rev (l0 ++ l) ++ (p4, p ∨ p3) :: nil) a).
  Proof.
    intros * NEST1 NEST2 EVAL1 EVAL2 GTMAX MAXHASH.
    assert (eval_hash_pred (fold_left Pand (to_equiv (l0 ++ l)) (T ∧ equiv (Pbase p4) (p ∨ p3)))
            (upd_asgn (rev l ++ rev l0 ++ (p4, p ∨ p3) :: nil) a) = Some true).
    { apply eval_hash_pred_fold_Pand2 with (x := T).
      rewrite app_assoc.
      rewrite upd_asgn_app1; [|eapply unnest_predicate_not_in; eauto].
      replace (rev l ++ rev l0) with (rev (l0  ++ l)) by (rewrite rev_app_distr; auto).
      apply fold_left_Pand_rev.
      rewrite to_equiv_rev.
      apply eval_hash_pred_equiv_asgn; auto.
      eapply unnest_predicate_equiv_list; eauto.
      eapply unnest_predicate_forall_none; eauto.
      eapply unnest_predicate_forall_gt1; eauto.
      rewrite eval_hash_pred_T_Pand.
      eapply eval_equiv_added_Por; eauto.
    }
    assert (eval_hash_pred (p1 ∨ p2) a = eval_hash_pred (Pbase p4)
            (upd_asgn ((rev l ++ rev l0) ++ (p4, p ∨ p3) :: nil) a)).
    { rewrite eval_hash_pred_get.
      rewrite upd_asgn_get.
      2: { rewrite upd_asgn_not_in by (eapply unnest_predicate_not_in2; eauto).
      eapply GTMAX. unfold max_hash_pred in *. fold max_hash_pred in *.
      pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1).
      pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2). lia.
      }
      apply eval_hash_pred_por.
      { rewrite EVAL1. unfold eval_pred_list. cbn [snd fst].
        rewrite upd_asgn_app1.
        { rewrite eval_hash_pred_T_Pand2; auto.
          apply fold_left_Pand_rev. rewrite to_equiv_rev.
          apply eval_hash_pred_equiv_asgn; auto.
          { unfold equiv_list_wf, Sorted; split.
            { replace pl_lt with (Basics.flip (Basics.flip (@pl_lt predicate))) by auto.
              apply sorted_rev4. eapply unnest_predicate_sorted; eauto. }
            { apply Forall_rev. eapply unnest_predicate_lt_in_list2; eauto. cbn [max_hash_pred] in *; lia. } }
          { exploit unnest_predicate_forall_none. apply NEST1. apply NEST2.
            all: eauto. intros. cbn. rewrite rev_app_distr in H0.
            apply Forall_app in H0; crush. }
          { exploit unnest_predicate_forall_gt1. apply NEST1. apply NEST2.
            all: eauto. intros. cbn. rewrite rev_app_distr in H0.
            apply Forall_app in H0; crush. } }
        { apply Forall_rev. apply Forall_forall; intros.
          cbn [max_hash_pred] in *.
          pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1) as TMP.
          pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST2 ltac:(lia)).
          pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST2).
          pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2).
          pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1).
          eapply Forall_forall in H1; eauto. eapply Forall_forall in H2; eauto.
          unfold not; intros. apply max_hash_pred_lt in H5. destruct x; cbn [fst snd] in *.
          unfold max_hash_pred in *; fold max_hash_pred in *.
          pose proof (unnest_predicate_in_pred2 _ _ _ _ _ NEST1).
          pose proof (unnest_predicate_in_pred2 _ _ _ _ _ NEST2).
          lia.
        } }
        { rewrite EVAL2. unfold eval_pred_list. cbn [snd fst].
          rewrite upd_asgn_app2.
          { rewrite eval_hash_pred_T_Pand2; auto.
            apply fold_left_Pand_rev. rewrite to_equiv_rev.
            apply eval_hash_pred_equiv_asgn; auto.
            { unfold equiv_list_wf, Sorted; split.
              { replace pl_lt with (Basics.flip (Basics.flip (@pl_lt predicate))) by auto.
                apply sorted_rev4. eapply unnest_predicate_sorted; eauto. }
              { apply Forall_rev. eapply unnest_predicate_lt_in_list2; eauto.
                pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1).
                cbn [max_hash_pred] in *; lia. } }
            { exploit unnest_predicate_forall_none. apply NEST1. apply NEST2.
              all: eauto. intros. cbn. rewrite rev_app_distr in H0.
              apply Forall_app in H0; crush. }
            { exploit unnest_predicate_forall_gt1. apply NEST1. apply NEST2.
              all: eauto. intros. cbn. rewrite rev_app_distr in H0.
              apply Forall_app in H0; crush. } }
          { apply Forall_rev. apply Forall_forall; intros.
            apply Forall_rev. apply Forall_forall; intros. split.
            cbn [max_hash_pred] in *.
            pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1) as TMP.
            pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST2 ltac:(lia)) as X2.
            pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST2) as Y2.
            pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST1 ltac:(lia)) as X1.
            pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST1) as Y1.
            pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2) as Z2.
            pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1) as Z1.
            destruct x, x0. cbn [fst snd] in *.
            eapply Forall_forall in X2; eauto. eapply Forall_forall in Y2; eauto.
            eapply Forall_forall in X1; eauto. eapply Forall_forall in Y1; eauto.
            cbn [fst snd] in *. lia.

            pose proof (unnest_predicate_lt_in_list3 _ _ _ _ _ NEST2) as X.
            unfold not; intros Y. eapply Forall_forall in X; eauto.
            cbn [max_hash_pred] in *.
            pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1) as TMP.
            pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST2 ltac:(lia)) as X2.
            pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST2) as Y2.
            pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST1 ltac:(lia)) as X1.
            pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST1) as Y1.
            pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2) as Z2.
            pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1) as Z1.
            eapply Forall_forall in X2; eauto. eapply Forall_forall in Y2; eauto.
            eapply Forall_forall in X1; eauto. eapply Forall_forall in Y1; eauto.
            destruct x, x0. cbn [fst snd] in *.
            unfold max_hash_pred in *; fold max_hash_pred in *.
            exploit unnest_predicate_in_pred2; eauto. lia; intros.
            exploit unnest_predicate_in_pred2. eapply NEST1. lia. intros.
            pose proof Y as YY. apply X in YY. inv YY.
            eapply map_in_some in H4; simplify. destruct x; simplify.
            eapply max_hash_pred_lt in Y.
            pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST2) as X22.
            pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST2) as Y22.
            eapply Forall_forall in X22; eauto. eapply Forall_forall in Y22; eauto.
            cbn [fst snd] in *.
            cbn [max_hash_pred] in *.
            lia. lia.
            eapply max_hash_pred_lt in H4. lia.
          }
          { intros. apply in_rev in H0. destruct x; cbn [fst snd] in *.
            unfold not; intros Y.
            cbn [max_hash_pred] in *.
            pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST1 ltac:(lia)) as X1.
            pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST1) as Y1.
            pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1) as Z1.
            eapply Forall_forall in X1; eauto. eapply Forall_forall in Y1; eauto.
            cbn [max_hash_pred fst snd] in *.
            exploit unnest_predicate_in_pred2; eauto. lia; intros. intros.
            exploit unnest_predicate_in_pred2. eapply NEST1. lia. intros.
            exploit unnest_predicate_lt_in_list4. eapply NEST2. eauto. intros. inv H3.
            eapply map_in_some in H4; simplify.
            destruct x.
            cbn [max_hash_pred fst snd] in *.
            pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST2 ltac:(lia)) as X2.
            pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST2) as Y2.
            pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2) as Z2.
            eapply Forall_forall in X2; eauto. eapply Forall_forall in Y2; eauto.
            cbn [max_hash_pred fst snd] in *.
            eapply max_hash_pred_lt in Y. lia.
            eapply max_hash_pred_lt in H4. lia.
          } } }
    symmetry; rewrite eval_hash_pred_T_Pand2; rewrite rev_app_distr;
      try solve [rewrite <- app_assoc; auto]; auto.
  Qed.

Lemma unnest_predicate_correct_Pimp :
    forall p1 p2 p0 p3 l0 l p4 fresh p a,
      unnest_predicate fresh p1 = (p, l, p0) ->
      unnest_predicate p0 p2 = (p3, l0, p4) ->
      eval_hash_pred p1 a = eval_pred_list (p, l) (upd_asgn (rev l) a) ->
      eval_hash_pred p2 a = eval_pred_list (p3, l0) (upd_asgn (rev l0) a) ->
      (forall y, (fresh <= y)%positive -> a ! y = None) ->
      (max_hash_pred (p1 → p2) < fresh)%positive ->
      eval_hash_pred (p1 → p2) a =
        eval_hash_pred (Pbase p4 ∧ fold_left Pand (to_equiv (l0 ++ l)) (T ∧ equiv (Pbase p4) (p → p3)))
                       (upd_asgn (rev (l0 ++ l) ++ (p4, p → p3) :: nil) a).
  Proof.
    intros * NEST1 NEST2 EVAL1 EVAL2 GTMAX MAXHASH.
    assert (eval_hash_pred (fold_left Pand (to_equiv (l0 ++ l)) (T ∧ equiv (Pbase p4) (p → p3)))
            (upd_asgn (rev l ++ rev l0 ++ (p4, p → p3) :: nil) a) = Some true).
    { apply eval_hash_pred_fold_Pand2 with (x := T).
      rewrite app_assoc.
      rewrite upd_asgn_app1; [|eapply unnest_predicate_not_in; eauto].
      replace (rev l ++ rev l0) with (rev (l0  ++ l)) by (rewrite rev_app_distr; auto).
      apply fold_left_Pand_rev.
      rewrite to_equiv_rev.
      apply eval_hash_pred_equiv_asgn; auto.
      eapply unnest_predicate_equiv_list; eauto.
      eapply unnest_predicate_forall_none; eauto.
      eapply unnest_predicate_forall_gt1; eauto.
      rewrite eval_hash_pred_T_Pand.
      eapply eval_equiv_added_Pimp; eauto.
    }
    assert (eval_hash_pred (p1 → p2) a = eval_hash_pred (Pbase p4)
            (upd_asgn ((rev l ++ rev l0) ++ (p4, p → p3) :: nil) a)).
    { rewrite eval_hash_pred_get.
      rewrite upd_asgn_get.
      2: { rewrite upd_asgn_not_in by (eapply unnest_predicate_not_in2; eauto).
      eapply GTMAX. unfold max_hash_pred in *. fold max_hash_pred in *.
      pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1).
      pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2). lia.
      }
      apply eval_hash_pred_pimp.
      { rewrite EVAL1. unfold eval_pred_list. cbn [snd fst].
        rewrite upd_asgn_app1.
        { rewrite eval_hash_pred_T_Pand2; auto.
          apply fold_left_Pand_rev. rewrite to_equiv_rev.
          apply eval_hash_pred_equiv_asgn; auto.
          { unfold equiv_list_wf, Sorted; split.
            { replace pl_lt with (Basics.flip (Basics.flip (@pl_lt predicate))) by auto.
              apply sorted_rev4. eapply unnest_predicate_sorted; eauto. }
            { apply Forall_rev. eapply unnest_predicate_lt_in_list2; eauto.
              cbn [max_hash_pred] in *; lia. } }
          { exploit unnest_predicate_forall_none. apply NEST1. apply NEST2.
            all: eauto. intros. cbn. rewrite rev_app_distr in H0.
            apply Forall_app in H0; crush. }
          { exploit unnest_predicate_forall_gt1. apply NEST1. apply NEST2.
            all: eauto. intros. cbn. rewrite rev_app_distr in H0.
            apply Forall_app in H0; crush. } }
        { apply Forall_rev. apply Forall_forall; intros.
          cbn [max_hash_pred] in *.
          pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1) as TMP.
          pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST2 ltac:(lia)).
          pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST2).
          pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2).
          pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1).
          eapply Forall_forall in H1; eauto. eapply Forall_forall in H2; eauto.
          unfold not; intros. apply max_hash_pred_lt in H5. destruct x; cbn [fst snd] in *.
          unfold max_hash_pred in *; fold max_hash_pred in *.
          pose proof (unnest_predicate_in_pred2 _ _ _ _ _ NEST1).
          pose proof (unnest_predicate_in_pred2 _ _ _ _ _ NEST2).
          lia.
        } }
        { rewrite EVAL2. unfold eval_pred_list. cbn [snd fst].
          rewrite upd_asgn_app2.
          { rewrite eval_hash_pred_T_Pand2; auto.
            apply fold_left_Pand_rev. rewrite to_equiv_rev.
            apply eval_hash_pred_equiv_asgn; auto.
            { unfold equiv_list_wf, Sorted; split.
              { replace pl_lt with (Basics.flip (Basics.flip (@pl_lt predicate))) by auto.
                apply sorted_rev4. eapply unnest_predicate_sorted; eauto. }
              { apply Forall_rev. eapply unnest_predicate_lt_in_list2; eauto.
                pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1).
                cbn [max_hash_pred] in *; lia. } }
            { exploit unnest_predicate_forall_none. apply NEST1. apply NEST2.
              all: eauto. intros. cbn. rewrite rev_app_distr in H0.
              apply Forall_app in H0; crush. }
            { exploit unnest_predicate_forall_gt1. apply NEST1. apply NEST2.
              all: eauto. intros. cbn. rewrite rev_app_distr in H0.
              apply Forall_app in H0; crush. } }
          { apply Forall_rev. apply Forall_forall; intros.
            apply Forall_rev. apply Forall_forall; intros. split.
            cbn [max_hash_pred] in *.
            pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1) as TMP.
            pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST2 ltac:(lia)) as X2.
            pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST2) as Y2.
            pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST1 ltac:(lia)) as X1.
            pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST1) as Y1.
            pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2) as Z2.
            pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1) as Z1.
            destruct x, x0. cbn [fst snd] in *.
            eapply Forall_forall in X2; eauto. eapply Forall_forall in Y2; eauto.
            eapply Forall_forall in X1; eauto. eapply Forall_forall in Y1; eauto.
            cbn [fst snd] in *. lia.

            pose proof (unnest_predicate_lt_in_list3 _ _ _ _ _ NEST2) as X.
            unfold not; intros Y. eapply Forall_forall in X; eauto.
            cbn [max_hash_pred] in *.
            pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1) as TMP.
            pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST2 ltac:(lia)) as X2.
            pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST2) as Y2.
            pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST1 ltac:(lia)) as X1.
            pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST1) as Y1.
            pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2) as Z2.
            pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1) as Z1.
            eapply Forall_forall in X2; eauto. eapply Forall_forall in Y2; eauto.
            eapply Forall_forall in X1; eauto. eapply Forall_forall in Y1; eauto.
            destruct x, x0. cbn [fst snd] in *.
            unfold max_hash_pred in *; fold max_hash_pred in *.
            exploit unnest_predicate_in_pred2; eauto. lia; intros.
            exploit unnest_predicate_in_pred2. eapply NEST1. lia. intros.
            pose proof Y as YY. apply X in YY. inv YY.
            eapply map_in_some in H4; simplify. destruct x; simplify.
            eapply max_hash_pred_lt in Y.
            pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST2) as X22.
            pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST2) as Y22.
            eapply Forall_forall in X22; eauto. eapply Forall_forall in Y22; eauto.
            cbn [fst snd] in *.
            cbn [max_hash_pred] in *.
            lia. lia.
            eapply max_hash_pred_lt in H4. lia.
          }
          { intros. apply in_rev in H0. destruct x; cbn [fst snd] in *.
            unfold not; intros Y.
            cbn [max_hash_pred] in *.
            pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST1 ltac:(lia)) as X1.
            pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST1) as Y1.
            pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1) as Z1.
            eapply Forall_forall in X1; eauto. eapply Forall_forall in Y1; eauto.
            cbn [max_hash_pred fst snd] in *.
            exploit unnest_predicate_in_pred2; eauto. lia; intros. intros.
            exploit unnest_predicate_in_pred2. eapply NEST1. lia. intros.
            exploit unnest_predicate_lt_in_list4. eapply NEST2. eauto. intros. inv H3.
            eapply map_in_some in H4; simplify.
            destruct x.
            cbn [max_hash_pred fst snd] in *.
            pose proof (unnest_predicate_lt_in_list2 _ _ _ _ _ NEST2 ltac:(lia)) as X2.
            pose proof (unnest_predicate_lt_in_list _ _ _ _ _ NEST2) as Y2.
            pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST2) as Z2.
            eapply Forall_forall in X2; eauto. eapply Forall_forall in Y2; eauto.
            cbn [max_hash_pred fst snd] in *.
            eapply max_hash_pred_lt in Y. lia.
            eapply max_hash_pred_lt in H4. lia.
          } } }
    symmetry; rewrite eval_hash_pred_T_Pand2; rewrite rev_app_distr;
      try solve [rewrite <- app_assoc; auto]; auto.
  Qed.

  Lemma upd_asgn_nil :
    forall a, upd_asgn nil a = a.
  Proof. crush. Qed.

  #[local] Opaque eval_hash_pred.
  #[local] Opaque upd_asgn.

  Lemma unnest_predicate_correct :
    forall a p fresh p' lp fresh',
      (max_hash_pred p < fresh)%positive ->
      unnest_predicate fresh p = (p', lp, fresh') ->
      (forall y : positive, (fresh <= y)%positive -> a ! y = None) ->
      eval_hash_pred p a = eval_pred_list (p', lp) (upd_asgn (rev lp) a).
  Proof.
    induction p; try solve [crush].
    - unfold eval_pred_list. simplify.
      rewrite eval_hash_pred_T_Pand3.
      rewrite upd_asgn_nil. auto.
    - simplify.
      destruct (unnest_predicate fresh p1) eqn:?. destruct p.
      destruct (unnest_predicate p0 p2) eqn:?. destruct p3.
      unfold eval_pred_list. simplify.
      pose proof Heqp as X1. pose proof Heqp3 as X2.
      pose proof X2 as X3.
      pose proof X1 as X4.
      apply IHp1 in X1; [|lia|auto].
      apply unnest_predicate_lt_fresh in X2.
      apply unnest_predicate_lt_fresh in X4.
      apply IHp2 in X3; [|lia|intros; eapply H1; lia].
      eapply unnest_predicate_correct_Pand; eauto.
    - simplify.
      destruct (unnest_predicate fresh p1) eqn:?. destruct p.
      destruct (unnest_predicate p0 p2) eqn:?. destruct p3.
      unfold eval_pred_list. simplify.
      pose proof Heqp as X1. pose proof Heqp3 as X2.
      pose proof X2 as X3.
      pose proof X1 as X4.
      apply IHp1 in X1; [|lia|auto].
      apply unnest_predicate_lt_fresh in X2.
      apply unnest_predicate_lt_fresh in X4.
      apply IHp2 in X3; [|lia|intros; eapply H1; lia].
      eapply unnest_predicate_correct_Por; eauto.
    - simplify.
      destruct (unnest_predicate fresh p1) eqn:?. destruct p.
      destruct (unnest_predicate p0 p2) eqn:?. destruct p3.
      unfold eval_pred_list. simplify.
      pose proof Heqp as X1. pose proof Heqp3 as X2.
      pose proof X2 as X3.
      pose proof X1 as X4.
      apply IHp1 in X1; [|lia|auto].
      apply unnest_predicate_lt_fresh in X2.
      apply unnest_predicate_lt_fresh in X4.
      apply IHp2 in X3; [|lia|intros; eapply H1; lia].
      eapply unnest_predicate_correct_Pimp; eauto.
    - simplify. repeat destruct_match; simplify.
      unfold eval_pred_list; simplify.
      pose proof Heqp0 as X1.
      pose proof Heqp0 as X2.
      apply IHp in X1; [|lia|auto].
      apply unnest_predicate_lt_fresh in X2.
      symmetry; rewrite eval_hash_pred_T_Pand2; [symmetry|].
      + rewrite eval_hash_pred_get.
        rewrite upd_asgn_get;
          [|rewrite upd_asgn_not_in; auto;
            eapply unnest_predicate_not_in3; eauto]; [].
        apply eval_hash_pred_pnot. rewrite X1. unfold eval_pred_list.
        simplify.
        rewrite eval_hash_pred_T_Pand2; auto; [].
        apply fold_left_Pand_rev. rewrite to_equiv_rev.
        apply eval_hash_pred_equiv_asgn; auto.
        * unfold equiv_list_wf; split.
          ** unfold Sorted.
             replace pl_lt with (Basics.flip (Basics.flip (@pl_lt predicate))) by auto.
             apply sorted_rev4. eapply unnest_predicate_sorted; eauto.
          ** apply Forall_rev; eapply unnest_predicate_lt_in_list2; eauto.
        * apply Forall_rev. apply Forall_forall; intros. apply H1.
          apply unnest_predicate_lt_in_list in Heqp0. eapply Forall_forall in Heqp0; eauto.
          lia.
        * apply Forall_rev. apply Forall_forall; intros. simplify.
          apply unnest_predicate_lt_in_list in Heqp0. eapply Forall_forall in Heqp0; eauto.
          lia.
      + apply eval_hash_pred_fold_Pand2 with (x := T).
        * rewrite upd_asgn_app1; [|eapply unnest_predicate_not_in4; eauto]; [].
          apply fold_left_Pand_rev. rewrite to_equiv_rev.
          apply eval_hash_pred_equiv_asgn; auto.
          ** unfold equiv_list_wf; split.
             *** unfold Sorted.
                 replace pl_lt with (Basics.flip (Basics.flip (@pl_lt predicate))) by auto.
                 apply sorted_rev4. eapply unnest_predicate_sorted; eauto.
             *** apply Forall_rev; eapply unnest_predicate_lt_in_list2; eauto.
          ** apply Forall_rev. apply Forall_forall; intros. apply H1.
             apply unnest_predicate_lt_in_list in Heqp0. eapply Forall_forall in Heqp0; eauto.
             lia.
          ** apply Forall_rev. apply Forall_forall; intros. simplify.
             apply unnest_predicate_lt_in_list in Heqp0. eapply Forall_forall in Heqp0; eauto.
             lia.
        * rewrite eval_hash_pred_T_Pand.
          apply eval_equiv2. rewrite eval_hash_pred_get.
          rewrite upd_asgn_get.
          ** symmetry. rewrite upd_asgn_app1; auto.
             constructor; [|constructor]; simpl.
             pose proof Heqp0 as NEST1.
             pose proof NEST1 as Y1.
             eapply unnest_predicate_in_pred2 in Y1.
             *** pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1).
                 unfold not; intros. apply max_hash_pred_lt in H2.
                 cbn [max_hash_pred] in H2. lia.
             *** unfold max_hash_pred in *; fold max_hash_pred in *.
                 pose proof (unnest_predicate_lt_fresh _ _ _ _ _ NEST1). lia.
          ** rewrite upd_asgn_not_in; auto. eapply unnest_predicate_not_in3; eauto.
  Qed.

#[local] Transparent eval_hash_pred.
#[local] Transparent upd_asgn.

Lemma interp_aux_correct :
  forall a ba f h1 h2,
    (forall l, h1 <> Fimp l) ->
    is_true (form_eqb h1 h2) ->
    interp_aux a ba f h1 = interp_aux a ba f h2.
Proof.
  unfold is_true. intros * IMP **.
  destruct h1; unfold form_eqb in *; try destruct_match; crush; auto.
  - apply Int63.eqb_spec in H; subst; auto.
  - apply Int63.eqb_spec in H0; subst;
    apply Int63.eqb_spec in H1; subst; auto.
  - apply list_beq_spec in H. subst.
    rewrite !Misc.afold_left_and. rewrite H. auto.
    exact Int63.eqb_spec.
  - apply list_beq_spec in H. subst.
    rewrite !Misc.afold_left_or. rewrite H. auto.
    exact Int63.eqb_spec.
  - apply Int63.eqb_spec in H0. apply Int63.eqb_spec in H1. subst; auto.
  - apply Int63.eqb_spec in H0. apply Int63.eqb_spec in H1. subst; auto.
  - apply Int63.eqb_spec in H. apply Int63.eqb_spec in H1. apply Int63.eqb_spec in H2. subst; auto.
Qed.

Lemma form_eqb_symm :
  forall f1 f2,
    is_true (form_eqb f1 f2) ->
    is_true (form_eqb f2 f1).
Proof.
  unfold is_true, form_eqb. intros. repeat destruct_match; try discriminate; auto;
  repeat match goal with
    | H: Int63.eqb _ _ = true |- _ => apply Int63.eqb_spec in H
    | |- Int63.eqb _ _ = true => apply Int63.eqb_spec
    | H: list_beq _ _ _ = true |- _ => apply list_beq_spec in H; [|exact Int63.eqb_spec]
    | |- list_beq _ _ _ = true => apply list_beq_spec; [exact Int63.eqb_spec|]
    | H: _ && _ = true |- _ => simplify
    | |- _ && _ = true => apply andb_true_intro; split
    end; subst; auto.
Qed.

Lemma t_interp_check_form : (* First array might be shorter, but it's ok *)
  forall a ba f1 f2 l,
    is_true (check_array form_eqb f1 f2) ->
    is_true (check_local_form l f1) ->
    forall i,
      to_Z i < to_Z (PArray.length f1) ->
      PArray.get (t_interp a ba f1) i = PArray.get (t_interp a ba f2) i.
Proof.
  intros * TRUE CHK.
  pose proof (check_array_length _ _ _ _ TRUE) as BOUNDS.
  pose proof (length_t_interp a ba f1) as Y.
  pose proof (length_t_interp a ba f2) as Z.
  revert Y.
  unfold t_interp.
  apply Misc.foldi_ind with (P :=
    fun iter fol =>
      PArray.length fol = PArray.length f1 ->
      forall i,
        to_Z i < to_Z iter ->
        PArray.get fol i = PArray.get _ i
  ); intros.
  + apply Misc.leb_0.
  + pose proof (not_int63_lt_0 i). replace (to_Z 0) with 0 in H0 by auto. lia.
  + rewrite PArray.length_set in H2. specialize (H1 H2).
    erewrite Misc.to_Z_add_1 in H3 by eassumption.
    destruct (int_dec i i0); subst.
    - rewrite PArray.get_set_same by (now rewrite H2).
      revert H1. revert Z. unfold t_interp.
      assert (W: to_Z i0 < to_Z (PArray.length f2)).
      { apply Int63.ltb_spec in H0. lia. } revert W.
      apply Misc.foldi_ind with (P :=
        fun iter fol =>
          to_Z i0 < to_Z iter ->
          PArray.length fol = PArray.length f2 ->
          (forall i, to_Z i < to_Z i0 ->
            PArray.get a0 i = PArray.get fol i) ->
          _ = PArray.get fol i0
      ); intros.
      * apply Misc.leb_0.
      * pose proof (not_int63_lt_0 i0). replace (to_Z 0) with 0 in H1 by auto. lia.
      * rewrite PArray.length_set in H7. erewrite Misc.to_Z_add_1 in H6 by eassumption.
        destruct (int_dec i0 i); subst. rewrite PArray.get_set_same by (now rewrite H7).
        rewrite lt_form_interp_form_aux with (f2 := PArray.get a1) (i := i).
        erewrite interp_aux_correct; auto.
        eapply check_local_form_spec; eauto.
        apply form_eqb_symm. eapply check_array_correct; eauto.
        apply Int63.ltb_spec in H0. auto.
        intros. rewrite H8. rewrite PArray.get_set_other; auto.
        unfold not; intros; subst. apply Int63.ltb_spec in H9. lia.
        apply Int63.ltb_spec in H9; auto.
        unfold check_local_form, is_true in *. simplify.
        unfold check_form in *. simplify. unfold wf in *.
        eapply Misc.aforallbi_spec in H12; eauto.
        rewrite PArray.get_set_other by auto. eapply H5; auto.
        assert (to_Z i <> to_Z i0) by (unfold not; intros; apply n; now apply to_Z_inj).
        lia. intros. rewrite H8; auto. rewrite PArray.get_set_other. auto.
        unfold not; intros. subst. lia.
    - rewrite PArray.get_set_other by auto. eapply H1.
      assert (to_Z i <> to_Z i0) by (unfold not; intros; apply n; now apply to_Z_inj).
      lia.
Qed.

(* Lemma a_interp_check_form : *)
(*   forall t_i (t_func: PArray.array (tval t_i)) a ba a1 a2, *)
(*     is_true (check_array Atom.eqb a1 a2) -> *)
(*     is_true (check_array Bool.eqb (Atom.t_interp t_i t_func a1) (Atom.t_interp t_i t_func a2)). *)

(* Misc.foldi_ind2: *)
(*   forall (A B : Type) (P : Int63.int -> A -> B -> Prop) (f1 : Int63.int -> A -> A) *)
(*     (f2 : Int63.int -> B -> B) (from to : Int63.int) (a1 : A) (a2 : B), *)
(*   Int63.leb from to = true -> *)
(*   P from a1 a2 -> *)
(*   (forall (i : Int63.int) (a3 : A) (a4 : B), *)
(*    Int63.leb from i = true -> Int63.ltb i to = true -> P i a3 a4 -> P (Int63.add i 1) (f1 i a3) (f2 i a4)) -> *)
(*   P to (Misc.foldi f1 from to a1) (Misc.foldi f2 from to a2) *)

Definition ind_S A a_init j (to: Int63.int) (fold1: PArray.array A) :=
  PArray.get fold1 j = PArray.get a_init j.

Lemma ind_S_nochange :
  forall a2 j from to a_init,
    Int63.to_Z j < Int63.to_Z from <= Int63.to_Z to ->
    ind_S _ a_init j to (Misc.foldi
                  (fun (i : Int63.int) (t_a : PArray.array (bval t_i)) =>
                     PArray.set t_a i (Atom.interp_aux t_i t_func (PArray.get t_a) (PArray.get a2 i))) from to a_init).
Proof.
  intros. apply Misc.foldi_ind. apply Int63.leb_spec. lia. now unfold ind_S.
  intros. unfold ind_S. rewrite PArray.get_set_other.
  unfold ind_S in H2. auto. apply Int63.leb_spec in H0.
  unfold not. intros. assert (Int63.to_Z i = Int63.to_Z j) by (now subst).
  lia.
Qed.

Lemma foldi_array_get_constant :
  forall a2 j from to a_init,
    Int63.to_Z j < Int63.to_Z from <= Int63.to_Z to ->
    PArray.get (Misc.foldi
                  (fun (i : Int63.int) (t_a : PArray.array (bval t_i)) =>
                     PArray.set t_a i (Atom.interp_aux t_i t_func (PArray.get t_a) (PArray.get a2 i))) from to a_init) j = PArray.get a_init j.
Proof. apply ind_S_nochange; auto. Qed.

Definition interp_ind_S t_i j (to: Int63.int) (fold1: PArray.array (bval t_i)) fold2 :=
  PArray.get fold1 j = PArray.get fold2 j.

(* (Misc.foldi *)
(*        (fun (i : Int63.int) (t_a : PArray.array (bval t_i)) => *)
(*         PArray.set t_a i (Atom.interp_aux t_i t_func (PArray.get t_a) (PArray.get a2 i))) (Int63.of_Z 0) *)
(*        (PArray.length a2) (PArray.make (PArray.length a2) (interp_cop t_i CO_xH))) *)

Lemma get_t_interp :
  forall a1 a2 j,
    is_true (Atom.wf a1) ->
    is_true (check_array Atom.eqb a1 a2) ->
    Int63.to_Z j < Int63.to_Z (PArray.length a1) ->
    PArray.get (Atom.t_interp t_i t_func a1) j =
      PArray.get (Atom.t_interp t_i t_func a2) j.
Proof.
  intros * WF CHECK BOUNDS. unfold Atom.t_interp.
  pose proof (check_array_length _ _ _ _ CHECK) as ABOUNDS.
  pose proof (check_array_correct _ _ _ _ CHECK).
  generalize dependent j.
  assert (TMP: forall (A: Prop),
             A /\ ((Int63.to_Z (PArray.length (Misc.foldi
       (fun (i : Int63.int) (t_a : PArray.array (bval t_i)) =>
        PArray.set t_a i (Atom.interp_aux t_i t_func (PArray.get t_a) (PArray.get a1 i))) (Int63.of_Z 0)
       (PArray.length a1) (PArray.make (PArray.length a1) (interp_cop t_i CO_xH)))))
                   = Int63.to_Z (PArray.length a1)) -> A) by tauto. apply TMP. clear TMP.
  apply Misc.foldi_ind with
    (P := fun iter fol =>
            (forall j,
              Int63.to_Z j < Int63.to_Z iter ->
              PArray.get fol j =
                PArray.get
                  (Misc.foldi
                     (fun (i : Int63.int) (t_a : PArray.array (bval t_i)) =>
                        PArray.set t_a i (Atom.interp_aux t_i t_func (PArray.get t_a) (PArray.get a2 i)))
                     (Int63.of_Z 0)
                     (PArray.length a2) (PArray.make (PArray.length a2) (interp_cop t_i CO_xH))) j) /\
              Int63.to_Z (PArray.length fol) = Int63.to_Z (PArray.length a1)
    ).

  apply Int63.leb_spec; simpl.
  pose proof (not_int63_lt_0 (PArray.length a1)).
  rewrite Int63.to_Z_0. auto.

  split.

  intros j BOUNDS0. pose proof (not_int63_lt_0 j). simpl in BOUNDS0. rewrite Int63.to_Z_0 in BOUNDS0. lia.
  auto.

  intros i a ILEB ILTB [HIND ARRLEN]; split.

  intros j BOUNDS1.
  erewrite Misc.to_Z_add_1 in BOUNDS1 by eassumption.
  apply Int63.ltb_spec in ILTB.
  apply Int63.leb_spec in ILEB.
  assert (X: Int63.to_Z j < Int63.to_Z i \/ Int63.to_Z j = Int63.to_Z i) by lia.
  inversion X as [X1|X1]. rewrite PArray.get_set_other.
  rewrite HIND; auto; try lia.
  unfold not; intro EQ. assert (Int63.to_Z j = Int63.to_Z i) by (now subst). lia.
  assert (j = i) by (now apply Int63.to_Z_inj). subst.
  rewrite PArray.get_set_same. 2: { apply Int63.ltb_spec. lia. }
  generalize dependent HIND.
  assert (X2: Int63.to_Z i < Int63.to_Z (PArray.length a2)) by lia.
  generalize X2.
  assert (TMP: forall (A: Prop),
             A /\ ((Int63.to_Z (PArray.length (Misc.foldi
       (fun (i0 : Int63.int) (t_a : PArray.array (bval t_i)) =>
        PArray.set t_a i0 (Atom.interp_aux t_i t_func (PArray.get t_a) (PArray.get a2 i0)))
       (Int63.of_Z 0) (PArray.length a2) (PArray.make (PArray.length a2) (interp_cop t_i CO_xH)))))
                   = Int63.to_Z (PArray.length a2)) -> A) by tauto. apply TMP. clear TMP.
  apply Misc.foldi_ind with
    (P := fun iter fol =>
              (Int63.to_Z i < Int63.to_Z iter ->
              (forall j : Int63.int,
                  Int63.to_Z j < Int63.to_Z i ->
                  PArray.get a j = PArray.get fol j) ->
              Atom.interp_aux t_i t_func (PArray.get a) (PArray.get a1 i) = PArray.get fol i)
              /\ Int63.to_Z (PArray.length fol) = Int63.to_Z (PArray.length a2)
    ).

  apply Int63.leb_spec. lia.

  split. intros BOUNDS2.
  pose proof (not_int63_lt_0 i). lia. auto.

  intros i0 a0 ILEB1 ILTB1 HIND2. split.
  intros BOUNDS3 HHIND.
  erewrite Misc.to_Z_add_1 in BOUNDS3 by eassumption.
  assert (A: Int63.to_Z i < Int63.to_Z i0 \/ Int63.to_Z i = Int63.to_Z i0) by lia.
  inversion A as [A1|A1]; clear A; subst.
  rewrite PArray.get_set_other. eapply HIND2. lia.
  intros j BOUNDS4. rewrite HHIND. rewrite PArray.get_set_other; auto.
  unfold not; intros EQ. assert (U: Int63.to_Z j = Int63.to_Z i0) by (now subst). lia. lia.
  unfold not; intros EQ. assert (U: Int63.to_Z i = Int63.to_Z i0) by (now subst). lia.
  assert (U: i = i0) by (now apply Int63.to_Z_inj). subst.
  rewrite PArray.get_set_same by (apply Int63.ltb_spec; lia).
  assert (EQ: PArray.get a2 i0 = PArray.get a1 i0).
  { apply Atom.eqb_spec. apply check_array_correct; auto. }

  rewrite EQ in *.
  apply lt_interp_aux with (i := i0). intros j ILTB2.
  rewrite HHIND. apply Int63.ltb_spec in ILTB2. rewrite PArray.get_set_other.
  auto. unfold not; intros EQ1. assert (U: Int63.to_Z i0 = Int63.to_Z j) by (now subst). lia.
  apply Int63.ltb_spec in ILTB2.
  auto.
  unfold Atom.wf in WF. eapply Misc.aforallbi_spec in WF. eassumption.
  apply Int63.ltb_spec. lia.
  rewrite PArray.length_set. lia.
  rewrite PArray.length_set. lia.
Qed.

Lemma interp_form_hatom_preserved :
  forall a1 a2 x,
    is_true (Atom.wf a1) ->
    is_true (check_array Atom.eqb a1 a2) ->
    Int63.to_Z x < Int63.to_Z (PArray.length a1) ->
    interp_form_hatom t_i t_func a1 x = interp_form_hatom t_i t_func a2 x.
Proof.
  unfold interp_form_hatom. unfold interp_hatom. intros.
  erewrite get_t_interp; auto.
Qed.

(* Definition F f2 := *)
(*   (fun i fol => *)
(*             (forall x, 0 <= Int63.to_Z x < Int63.to_Z i -> *)
(*             PArray.get fol x *)
(*             = PArray.get *)
(*                 (Misc.foldi *)
(*                    (fun (i : Int63.int) (t_b : PArray.array bool) => *)
(*                       PArray.set t_b i *)
(*                                  (interp_aux (interp_form_hatom t_i t_func a1) *)
(*                                              (interp_form_hatom_bv t_i t_func a1) *)
(*                                              (PArray.get t_b) (PArray.get f2 i))) *)
(*                    (Int63.of_Z 0) (PArray.length f2) *)
(*                    (PArray.make (PArray.length f2) true)) x)). *)

Definition form_atom f P :=
  forall i a, PArray.get f i = Fatom a -> P a.

Definition single_form_atom f P :=
  forall a, f = Fatom a -> P a.

Lemma lt_form_interp_single_form_atom :
  forall a1 a2 b f h,
    single_form_atom h (fun j => a1 j = a2 j) ->
    interp_aux a1 b f h = interp_aux a2 b f h.
Proof.
  destruct h;simpl;intros; trivial. auto.
Qed.

Lemma lt_form_interp_not_bv :
  forall b1 b2 a f h,
    is_true (single_form_not_bv h) ->
    interp_aux a b1 f h = interp_aux a b2 f h.
Proof.
  destruct h;simpl;intros; trivial. discriminate.
Qed.

Lemma check_single_form_not_bv :
  forall f1 l x,
    is_true (check_local_form l f1) ->
    to_Z x < to_Z (PArray.length f1) ->
    is_true (single_form_not_bv (PArray.get f1 x)).
Proof.
  unfold check_local_form, is_true; simplify.
  eapply Misc.aforallbi_spec in H2; [|apply Int63.ltb_spec; eassumption].
  crush.
Qed.

Lemma is_true_lt_form :
  forall a b f1 x,
    to_Z a < to_Z b ->
    is_true (lt_form a (PArray.get f1 x)) ->
    is_true (lt_form b (PArray.get f1 x)).
Proof.
  unfold is_true, lt_form; intros. destruct_match; auto.
  - apply Int63.ltb_spec in H0. apply Int63.ltb_spec. lia.
  - apply Misc.aforallbi_spec; intros. eapply Misc.aforallbi_spec in H0; eauto.
    apply Int63.ltb_spec in H0. apply Int63.ltb_spec. lia.
  - apply Misc.aforallbi_spec; intros. eapply Misc.aforallbi_spec in H0; eauto.
    apply Int63.ltb_spec in H0. apply Int63.ltb_spec. lia.
  - apply Misc.aforallbi_spec; intros. eapply Misc.aforallbi_spec in H0; eauto.
    apply Int63.ltb_spec in H0. apply Int63.ltb_spec. lia.
  - simplify. apply Int63.ltb_spec in H1. apply Int63.ltb_spec in H2.
    apply andb_true_intro. split; apply Int63.ltb_spec; lia.
  - simplify. apply Int63.ltb_spec in H1. apply Int63.ltb_spec in H2.
    apply andb_true_intro. split; apply Int63.ltb_spec; lia.
  - simplify. apply Int63.ltb_spec in H2. apply Int63.ltb_spec in H3.
    apply Int63.ltb_spec in H0.
    apply andb_true_intro; split; [apply andb_true_intro;split|];
    apply Int63.ltb_spec; lia.
  - apply forallb_forall; intros. eapply forallb_forall in H0; try eassumption.
    apply Int63.ltb_spec in H0. apply Int63.ltb_spec. lia.
Qed.

Lemma get_t_interp_form :
  forall a1 a2 f1,
    is_true (check_array Atom.eqb a1 a2) ->
    is_true (check_local_form (PArray.length a1) f1) ->
    is_true (Atom.wf a1) ->
    forall x,
      Int63.to_Z x < Int63.to_Z (PArray.length f1) ->
      (PArray.get (t_interp (interp_form_hatom t_i t_func a2) (interp_form_hatom_bv t_i t_func a2) f1) x
       = PArray.get (t_interp (interp_form_hatom t_i t_func a1) (interp_form_hatom_bv t_i t_func a1) f1) x).
Proof.
  intros * TRUE LOCAL WFA.
  pose proof (length_t_interp (interp_form_hatom t_i t_func a1)
                              (interp_form_hatom_bv t_i t_func a1) f1) as Y1.
  pose proof (length_t_interp (interp_form_hatom t_i t_func a2)
                              (interp_form_hatom_bv t_i t_func a2) f1) as Y2.
  revert Y1. revert Y2.
  unfold t_interp.
  apply Misc.foldi_ind2 with (P :=
    fun i a b =>
      PArray.length a = PArray.length f1 ->
      PArray.length b = PArray.length f1 ->
      forall x,
        to_Z x < to_Z (PArray.length f1) ->
        PArray.get a x = PArray.get b x
  ).
  - apply Misc.leb_0.
  - intros. now rewrite PArray.get_make.
  - intros. rewrite PArray.length_set in H2. rewrite PArray.length_set in H3.
    specialize (H1 H2 H3).
    destruct (int_dec i x); subst.
    + symmetry. rewrite !PArray.get_set_same
        by (try rewrite H3 in *; try rewrite H2 in *; apply Int63.ltb_spec; lia); auto.
      erewrite lt_form_interp_not_bv; [|eapply check_single_form_not_bv; eauto].
      erewrite lt_form_interp_single_form_atom.
      2: { unfold single_form_atom; intros.
           rewrite interp_form_hatom_preserved with (a2 := a2). eauto.
           auto. auto. apply check_local_form_spec in LOCAL; simplify.
           eapply Int63.ltb_spec. eapply H7; eauto. }
      erewrite lt_form_interp_form_aux. eauto. intros. symmetry. eapply H1; eauto.
      apply Int63.ltb_spec in H5. eauto.
      unfold is_true in LOCAL. unfold check_local_form in LOCAL. simplify. unfold check_form in H5.
      simplify. unfold wf in H8. eapply Misc.aforallbi_spec in H8; eauto.
      eapply is_true_lt_form; eauto.
    + rewrite !PArray.get_set_other by auto; auto.
Qed.

Lemma valid_same_corr :
  forall r a1 a2 f1 f2,
    ~ is_true (Euf_Checker.valid t_func a2 f2 r) ->
    is_true (check_array Atom.eqb a1 a2) ->
    is_true (check_array form_eqb f1 f2) ->
    is_true (check_local_form (PArray.length a1) f1) ->
    is_true (Atom.wf a1) ->
    Forall (fun x => Int63.to_Z (State.Lit.blit x) < Int63.to_Z (PArray.length f1))
           (Misc.to_list r) ->
    ~ is_true (Euf_Checker.valid t_func a1 f1 r).
Proof.
  unfold is_true. intros * VAL CHKA CHKF LOCAL WFA LT.
  unfold not in *. intros * VAL2; apply VAL.
  unfold Euf_Checker.valid in *. rewrite Misc.afold_left_and in *.
  rewrite forallb_forall in *; intros x IN.
  pose proof IN as VAL3.
  apply VAL2 in VAL3.
  rewrite Forall_forall in LT.
  pose proof IN as VAL4.
  apply LT in VAL4.
  unfold interp_state_var.
  unfold State.Lit.interp.
  unfold State.Var.interp.
  pose proof CHKF as INTERP.
  eapply t_interp_check_form in INTERP; eauto.
  rewrite <- INTERP.
  now rewrite get_t_interp_form with (a1 := a1).
Qed.

End PROOF.

Lemma restrict_a :
  forall p a a',
    (forall y, (y <= max_hash_pred p)%positive -> a ! y = a' ! y) ->
    eval_hash_pred p a = eval_hash_pred p a'.
Proof.
  induction p; crush.
  - now rewrite H by lia.
  - erewrite IHp1. erewrite IHp2. eauto.
    intros. eapply H. lia.
    intros. eapply H. lia.
  - erewrite IHp1. erewrite IHp2. eauto.
    intros. eapply H. lia.
    intros. eapply H. lia.
  - erewrite IHp1. erewrite IHp2. eauto.
    intros. eapply H. lia.
    intros. eapply H. lia.
  - erewrite IHp. eauto.
    intros. eapply H. lia.
Qed.

Definition nuke_asgn p (a: PTree.t bool) :=
  PTree.fold (fun b i a =>
    if (i <=? max_hash_pred p)%positive then PTree.set i a b else b
  ) a (PTree.empty bool).

Lemma eval_hash_pred_ext:
  forall m m': PTree.t bool,
    (forall x : PTree.elt, m ! x = m' ! x) ->
    forall p,
      eval_hash_pred p m = eval_hash_pred p m'.
Proof.
  intros. eapply restrict_a; eauto.
Qed.

Lemma nuke_asgn_spec :
  forall p a,
    exists a',
      eval_hash_pred p a = eval_hash_pred p a'
      /\ (forall y, (max_hash_pred p < y)%positive -> a' ! y = None).
Proof.
  intros. exists (nuke_asgn p a).
  revert p. revert a.
  split.
  - eapply restrict_a; eauto.
    intros. unfold nuke_asgn.
    eapply PTree_Properties.fold_rec; eauto.
    + intros. rewrite <- H0; auto.
    + intros.
      case_eq ((k <=? max_hash_pred p)%positive); intros.
      * destruct (peq k y).
        -- subst. rewrite ! PTree.gss; auto.
        -- rewrite ! PTree.gso; auto.
      * rewrite POrderedType.Positive_as_DT.leb_gt in H3.
        assert (k <> y) by lia.
        rewrite PTree.gso; auto.
  - unfold nuke_asgn.
    eapply PTree_Properties.fold_rec; eauto; intros.
    + unfold PTree.empty. rewrite PTree.gleaf; auto.
    + destruct_match.
      * rewrite POrderedType.Positive_as_DT.leb_le in Heqb.
        assert (k <> y) by lia.
        rewrite PTree.gso; auto.
      * eapply H1; eauto.
Qed.

Lemma nuke_1 :
  forall p a x,
    ~ pred_In x p ->
    eval_hash_pred p a = eval_hash_pred p (PTree.remove x a).
Proof.
  induction p; crush.
  - assert (a <> x) by (unfold not; intros; subst; apply H; constructor).
    rewrite PTree.gro; auto.
  - assert (~ pred_In x p1) by (unfold not; intros; apply H; apply pred_In_Pand1; auto).
    assert (~ pred_In x p2) by (unfold not; intros; apply H; apply pred_In_Pand2; auto).
    erewrite IHp1; [|eassumption]; erewrite IHp2; eauto.
  - assert (~ pred_In x p1) by (unfold not; intros; apply H; apply pred_In_Por1; auto).
    assert (~ pred_In x p2) by (unfold not; intros; apply H; apply pred_In_Por2; auto).
    erewrite IHp1; [|eassumption]; erewrite IHp2; eauto.
  - assert (~ pred_In x p1) by (unfold not; intros; apply H; apply pred_In_Pimp1; auto).
    assert (~ pred_In x p2) by (unfold not; intros; apply H; apply pred_In_Pimp2; auto).
    erewrite IHp1; [|eassumption]; erewrite IHp2; eauto.
  - assert (~ pred_In x p) by (unfold not; intros; apply H; constructor; auto).
    erewrite IHp; eauto.
Qed.

Lemma check_atom_to_smt :
  forall a p d forms atoms,
    to_smt a p = Some (d, forms, atoms) ->
    is_true (check_atom atoms).
Proof.
  intros. unfold to_smt in *. repeat (destruct_match; try discriminate; []).
  crush.
Qed.

Lemma check_wt_extra_spec :
  forall a,
    is_true (check_atom a) ->
    is_true (check_wt_extra a) ->
    (forall i x l, PArray.get a i <> Anop x l)
    /\ (forall i n l, PArray.get a i = Aapp n l -> l = nil).
Proof.
  unfold check_wt_extra, is_true; intros.
  split; intros.
  - unfold not; intros. exploit PArray.get_not_default_lt. rewrite H1.
    unfold check_atom in H. destruct (PArray.default a); try discriminate.
    intros. eapply Misc.aforallbi_spec in H0; eauto.
    rewrite H1 in H0. discriminate.
  - unfold not; intros. exploit PArray.get_not_default_lt. rewrite H1.
    unfold check_atom in H. destruct (PArray.default a); try discriminate.
    intros. eapply Misc.aforallbi_spec in H0; eauto.
    rewrite H1 in H0. destruct_match; crush.
Qed.

Lemma pred_in_correct :
  forall p c,
    pred_in c p = true ->
    pred_In c p.
Proof.
  induction p; crush; subst.
  - constructor.
  - apply orb_prop in H. inv H; auto using pred_In_Pand1, pred_In_Pand2.
  - apply orb_prop in H. inv H; auto using pred_In_Por1, pred_In_Por2.
  - apply orb_prop in H. inv H; auto using pred_In_Pimp1, pred_In_Pimp2.
  - constructor; auto.
Qed.

Lemma pred_in_complete :
  forall p c,
    pred_In c p ->
    pred_in c p = true.
Proof.
  induction p; crush; subst; try solve [inv H].
  - inv H. apply Pos.eqb_refl.
  - apply orb_true_intro. inv H; intuition.
  - apply orb_true_intro. inv H; intuition.
  - apply orb_true_intro. inv H; intuition.
  - inv H. auto.
Qed.

Lemma max_key_upd_asgn :
  forall l a x,
    Forall (fun y => Z.pos y < x) (map fst l) ->
    (Z.pos (max_key a) < x) ->
    (Z.pos (max_key (upd_asgn l a)) < x).
Proof.
  induction l; crush.
  inv H. destruct_match. eapply IHl; auto.
  - assert (exists y, (PTree.set (fst a) b a0) ! (max_key (PTree.set (fst a) b a0)) = Some y).
    { apply max_key_in.
    destruct (PTree.bempty (PTree.set (fst a) b a0)) eqn:?; auto.
    exfalso. apply PTree.bempty_correct with (x := (fst a)) in Heqb0. rewrite PTree.gss in Heqb0. discriminate.
    }
    simplify. destruct (peq (max_key (PTree.set (fst a) b a0)) (fst a)).
    + lia.
    + rewrite PTree.gso in H1; auto.
      assert (forall x y, ~ y <= x -> x < y) by lia.
      apply H; unfold not; intros.
      assert (Z.pos (max_key a0) < Z.pos (max_key (PTree.set (fst a) b a0))) by lia.
      pose proof (max_not_present _ (max_key (PTree.set (fst a) b a0)) a0).
      rewrite H6 in H1 by lia. discriminate.
  - eapply IHl; eauto.
Qed.

Theorem valid_check_smt :
  forall p a,
    check_smt p = true -> eval_hash_pred p a = Some true.
Proof.
  intros * CHK. unfold check_smt in CHK. repeat (destruct_match; try discriminate; []).
  apply andb_prop in CHK; inversion CHK as [CHK1 H0]; clear CHK.
  apply andb_prop in CHK1; inversion CHK1 as [CHK6 CHKROOT]; clear CHK1.
  apply andb_prop in CHK6; inversion CHK6 as [CHK2 CHK_EXTRA]; clear CHK6.
  apply andb_prop in CHK2; inversion CHK2 as [CHK3 H2]; clear CHK2.
  apply andb_prop in CHK3; inversion CHK3 as [CHK4 H3]; clear CHK3.
  apply andb_prop in CHK4; inversion CHK4 as [CHK5 H4]; clear CHK4.
  apply andb_prop in CHK5; inversion CHK5 as [H H5]; clear CHK5.
  apply andb_prop in CHKROOT; inversion CHKROOT as [CHKROOT2 P1LT]; clear CHKROOT.
  apply andb_prop in CHKROOT2; inversion CHKROOT2 as [CHKROOT3 NOTPREDIN]; clear CHKROOT2.
  simplify. destruct p0.
  exploit nuke_asgn_spec. intros. inv H1. inv H6. rewrite H1.
  assert (NOTPRED: ~ pred_In 1%positive p).
  { unfold not; intros HH. apply pred_in_complete in HH. rewrite HH in NOTPREDIN. discriminate. }
  erewrite nuke_1; eauto.
  assert (ALLEQ: forall y, (max_hash_pred p < y)%positive -> (PTree.remove 1 x) ! y = None).
  { intros. destruct (peq 1 y); subst. rewrite PTree.grs. auto. rewrite PTree.gro; auto. }
  erewrite unnest_predicate_correct; try eassumption; try lia; [|intros; eapply ALLEQ; lia].
  pose proof (exists_asgn (upd_asgn (rev l) (PTree.remove 1 x))) as X.
  assert (ASSUMP1: Z.pos (max_key (upd_asgn (rev l) (PTree.remove 1 x))) - 2 < wB - 1).
  { assert (forall l a x,
      Forall (fun y => Z.pos y < x) (map fst l) ->
      (Z.pos (max_key a) < x) ->
      (Z.pos (max_key (upd_asgn l a)) < x)).
      { apply max_key_upd_asgn; auto. }
    assert (Z.pos (max_key (upd_asgn (rev l) (PTree.remove 1 x))) < wB).
    { assert (GTWB: Z.pos p1 < wB) by assumption. eapply H6. apply Forall_forall; intros.
    apply map_in_some in H8. inv H8.
      inv H9. destruct x1 in *. apply in_rev in H8.
      apply unnest_predicate_lt_in_list in Heqp0. eapply Forall_forall in Heqp0; eauto.
      cbn [fst snd] in *. lia.
    assert ((max_key (PTree.remove 1 x) <= max_hash_pred p)%positive).
    { assert (~ (max_hash_pred p < max_key (PTree.remove 1 x))%positive -> (max_key (PTree.remove 1 x) <= max_hash_pred p)%positive) by lia.
      apply H8. unfold not; intros. pose proof H9. apply ALLEQ in H9.
      destruct (PTree.bempty (PTree.remove 1 x)) eqn:?.
      - rewrite max_key_empty in * by auto. lia.
      - exploit max_key_in; try eassumption. intros. inv H11. rewrite H12 in H9. discriminate.
     }
    assert (max_hash_pred p < p1)%positive.
    { eapply unnest_predicate_lt_fresh in Heqp0. lia. }
    lia.
    }
    lia.
  }
  assert (ASSUMP2: (forall (k : positive) (x0 : bool),
    (upd_asgn (rev l) (PTree.remove 1 x)) ! k = Some x0 -> 0 <= Z.pos k - 2 < wB)).
    { intros. pose proof H6 as XXX. apply max_key_correct in H6.
      destruct (in_dec peq k (map fst l)).
      { apply map_in_some in i. inv i. inv H8. destruct x1; cbn [fst] in *.
        apply unnest_predicate_lt_in_list in Heqp0. eapply Forall_forall in Heqp0; eauto.
        cbn [fst] in *. lia.
      }
      { assert (~ In k (map fst (rev l))).
        { unfold not; intros; apply n. rewrite map_rev in H8. apply in_rev in H8. auto. }
        rewrite upd_asgn_not_in in XXX by auto.
        assert (k = 1%positive \/ (1 < k)%positive) by lia. inv H9. rewrite PTree.grs in XXX. discriminate.
        lia.
      }
    }
  assert (X2 := X). clear X.
  pose proof (X2 ASSUMP1 ASSUMP2) as X.
  inversion X as [res ASGN]; clear X.
  assert (ASSUMP3: forall (i : Int63.int) (x0 : nop) (l0 : list Int63.int),
    PArray.get a5 i <> Anop x0 l0) by (eapply check_wt_extra_spec; eauto).
  assert (ASSUMP4: forall (i n : Int63.int) (l0 : list Int63.int),
    PArray.get a5 i = Aapp n l0 -> l0 = nil) by (eapply check_wt_extra_spec; eauto).
  eapply wt_correct in H2; try eassumption.
  pose proof (Checker_Ext.checker_ext_correct _ _ _ _ _ H0) as X.
  assert (XX: is_true (Atom.wf a0)) by
    (apply check_atom_to_smt in Heqo; unfold check_atom in *;
      destruct (PArray.default a0); try discriminate;
      destruct c0; crush).
  eapply valid_same_corr in X; try eassumption.
  eapply valid_to_smt; try eassumption.
  simpl. eapply fold_left_Pand_rev.
  rewrite to_equiv_rev. eapply eval_hash_pred_equiv_asgn; auto.
  unfold equiv_list_wf, Sorted; split.
  replace pl_lt with (Basics.flip (Basics.flip (@pl_lt predicate))) by auto.
  eapply sorted_rev4. eapply unnest_predicate_sorted; eauto.
  apply Forall_rev; eapply unnest_predicate_lt_in_list2; eauto; lia.
  apply Forall_rev; apply Forall_forall; intros. eapply ALLEQ.
  pose proof (unnest_predicate_lt_in_list _ _ _ _ _ Heqp0) as Y. eapply Forall_forall in Y; eauto. lia.
  apply Forall_rev; apply Forall_forall; intros. simpl.
  pose proof (unnest_predicate_lt_in_list _ _ _ _ _ Heqp0) as Y. eapply Forall_forall in Y; eauto. lia.
  apply Forall_forall; intros. unfold check_root_index in CHKROOT3.
  eapply forallb_forall in CHKROOT3; eauto.
  lia.
Qed.

Lemma mutate_eval_correct :
  forall p a,
    eval_hash_pred (mutate1_p p) a = eval_hash_pred p a.
Proof.
  unfold mutate1_p; intros.
  repeat (destruct_match; crush).
Qed.

Theorem valid_check_smt_total :
  forall p a,
    check_smt_total p = true -> eval_hash_pred p a = Some true.
Proof.
  unfold check_smt_total; intros.
  destruct_match; auto using valid_check_smt.
  rewrite <- mutate_eval_correct.
  destruct_match; auto using valid_check_smt.
  discriminate.
Qed.