(* Round 2: arithmetic layer of the per-step invariant J (standalone, no TM). *)
(* BEGIN standalone header (dropped when merged) *)
Require Import Arith Lia List ZifyNat.
Import ListNotations.
(* END standalone header *)
Local Open Scope nat_scope.

Notation tri := (nat * nat * bool)%type.
Definition bv (d : bool) : nat := if d then 1 else 0.

Fixpoint dv (P : list tri) : nat :=
  match P with
  | [] => 0
  | (_,_,d) :: P' => bv d + 2 * dv P'
  end.

Definition dig (x : tri) : bool := let '(_,_,d) := x in d.
Definition dig0 (x : tri) : Prop := dig x = false.

(* BEGIN copies of kill-file definitions (dropped when merged) *)
Definition touch (x : tri) : tri := let '(p,q,d) := x in (S p, pred q, negb d).
Fixpoint ovp (q : nat) (Z : list (nat*nat*bool)) (t : nat) : list (nat*nat*bool) :=
  match Z with
  | [] => [(q, S t, true)]
  | (p',q',_) :: Z' => (q, p', true) :: ovp q' Z' t
  end.
Fixpoint ovpX (q : nat) (Z : list (nat*nat*bool)) (pa : nat) : list (nat*nat*bool) :=
  match Z with
  | [] => [(q, pa, false)]
  | (p',q',_) :: Z' => (q, p', true) :: ovpX q' Z' pa
  end.
Definition okR (x : nat*nat*bool) : Prop := let '(p,q,d) := x in d = false /\ 1 <= q.
Definition okL (x : nat*nat*bool) : Prop := let '(p,q,d) := x in d = false /\ 2 <= q.
Definition okO (x : nat*nat*bool) : Prop := let '(p,q,d) := x in 1 <= p /\ 1 <= q.
(* END copies *)

Lemma dv_lt P : dv P < 2 ^ length P.
Proof.
  induction P as [|[[p q] d] P IH]; cbn [dv length]; [cbn; lia|].
  rewrite Nat.pow_succ_r'. destruct d; cbn [bv]; lia.
Qed.

Lemma dv_zeros Z R : Forall dig0 Z -> dv (Z ++ R) = 2 ^ length Z * dv R.
Proof.
  induction Z as [|[[p q] d] Z IH]; intros HZ; cbn [app dv length]; [cbn; lia|].
  inversion HZ as [|? ? Hd HZ']; subst. unfold dig0, dig in Hd. subst d. rewrite IH by exact HZ'.
  rewrite Nat.pow_succ_r'. cbn [bv]. nia.
Qed.

Lemma dv_tz Z R : Forall dig0 Z -> dv (map touch Z ++ R) + 1 = 2 ^ length Z + 2 ^ length Z * dv R.
Proof.
  induction Z as [|[[p q] d] Z IH]; intros HZ; cbn [map app dv length touch]; [cbn; lia|].
  inversion HZ as [|? ? Hd HZ']; subst. unfold dig0, dig in Hd. subst d. cbn [negb bv].
  specialize (IH HZ'). rewrite Nat.pow_succ_r'. nia.
Qed.

(** every element, with its 1-based index and the list to its right *)
Fixpoint AllI (Pr : nat -> tri -> list tri -> Prop) (i : nat) (P : list tri) : Prop :=
  match P with
  | [] => True
  | x :: Y => Pr i x Y /\ AllI Pr (S i) Y
  end.

Lemma AllI_app Pr Z : forall i R, AllI Pr i (Z ++ R) -> AllI Pr (i + length Z) R.
Proof.
  induction Z as [|x Z IH]; intros i R H; cbn [app length] in *.
  - rewrite Nat.add_0_r. exact H.
  - destruct H as [_ H]. replace (i + S (length Z)) with (S i + length Z) by lia. apply IH, H.
Qed.

Lemma AllI_mono (Pr Pr' : nat -> tri -> list tri -> Prop) P : forall i,
  (forall j x Y, i <= j -> Pr j x Y -> Pr' j x Y) -> AllI Pr i P -> AllI Pr' i P.
Proof.
  induction P as [|x P IH]; intros i Hm H; cbn in *; [exact I|].
  destruct H as [H1 H2]. split; [apply Hm; [lia | exact H1]|].
  apply IH; [|exact H2]. intros j y Y Hj. apply Hm. lia.
Qed.

Lemma AllI_shift (Pr Pr' : nat -> tri -> list tri -> Prop) P : forall i,
  (forall j x Y, i <= j -> Pr (S j) x Y -> Pr' j x Y) -> AllI Pr (S i) P -> AllI Pr' i P.
Proof.
  induction P as [|x P IH]; intros i Hm H; cbn in *; [exact I|].
  destruct H as [H1 H2]. split; [apply Hm; [lia | exact H1]|].
  apply IH; [|exact H2]. intros j y Y Hj. apply Hm. lia.
Qed.

(** the touched prefix Z (all digits 0) of a rule; R becomes R' *)
Lemma AllI_touchZ (Pr Pr' : nat -> tri -> list tri -> Prop) R R' : forall Z i,
  Forall dig0 Z ->
  (forall j p q Zr, Forall dig0 Zr -> j + S (length Zr) = i + length Z ->
     Pr j (p,q,false) (Zr ++ R) -> Pr' j (S p, pred q, true) (map touch Zr ++ R')) ->
  AllI Pr i (Z ++ R) -> AllI Pr' (i + length Z) R' -> AllI Pr' i (map touch Z ++ R').
Proof.
  induction Z as [|[[p q] d] Z IH]; intros i HZ Hob HA HR; cbn [app map length] in *.
  - rewrite Nat.add_0_r in HR. exact HR.
  - inversion HZ as [|? ? Hd HZ']; subst. unfold dig0, dig in Hd. subst d. destruct HA as [H1 H2].
    cbn [touch negb]. split.
    + apply Hob; [exact HZ' | lia | exact H1].
    + apply IH; [exact HZ' | | exact H2 | ].
      * intros j p' q' Zr HZr Hj. apply Hob; [exact HZr | lia].
      * replace (S i + length Z) with (i + S (length Z)) by lia. exact HR.
Qed.

(** * The per-pair clause.  n = number of pairs to the right, w = 2^n, tv = value of the digits
    from this pair to the top (this pair least significant, so tv = d mod 2).  Rt = tv + (phase
    term) is the number of touches the pair still gets before the next re-pairing if no merge
    happens; p + Rt and q - Rt are invariant under touches. *)

Inductive phase := E1 | E2 | E1t | E2t | T0 | L1 | L2 | LX.

(** clauses that depend on n (not on the index) *)
Definition PN (ph : phase) (c4 : bool) (p q n tv : nat) : Prop :=
  match ph with
  | E1 => match n with
          | 0 => q >= tv + 2 ^ n + 1 /\ p + tv + 2 ^ n >= 3
          | S _ => q >= tv + 3 * 2 ^ n + 1 /\ (p + tv) mod 2 = 1 /\ p + tv + 2 ^ n >= 3 * 2 ^ n
          end
  | E2 => match n with
          | 0 => q >= tv + 1 /\ p + tv >= 3
          | S _ => q >= tv + 2 * 2 ^ n + 1 /\ (p + tv) mod 2 = 1 /\ p + tv >= 3 * 2 ^ n
          end
  | E1t => match n with
          | 0 => q >= tv + 2 ^ n + 1 /\ p + tv + 2 ^ n = 5
          | S _ => q >= tv + 2 * 2 ^ n + 1 /\ (p + tv) mod 2 = 1 /\ p + tv + 2 ^ n >= 3 * 2 ^ n
          end
  | E2t => match n with
          | 0 => q >= tv + 1 /\ p + tv = 5
          | S _ => q >= tv + 2 ^ n + 1 /\ (p + tv) mod 2 = 1 /\ p + tv >= 3 * 2 ^ n
          end
  | T0 => q >= tv + 7 * 2 ^ n + 1 /\ p + tv + 5 * 2 ^ n >= 6 * 2 ^ n /\
          match n with
          | 0 => tv = 0 /\ p mod 2 = 0
          | S _ => (p + tv) mod 2 = 1
          end
  | L1 => q + 2 ^ n >= tv + 2 /\
          match n with
          | 0 => q = tv + 2 ^ n
          | 1 => p + tv + 2 ^ n >= (if c4 then 4 else 5) * 2 ^ n /\
                 (q >= tv + 2 ^ n + 1 \/ (q + tv) mod 2 = 0) /\ (if c4 then q = tv + 2 ^ n else True)
          | S (S _) => p + tv + 2 ^ n >= (if c4 then 4 else 5) * 2 ^ n /\ (q + tv) mod 2 = 0
          end
  | LX => match n with
          | 0 => q = tv + 1
          | 1 => p + tv >= 4 * 2 ^ n /\ q = tv + 1
          | S (S _) => p + tv >= 4 * 2 ^ n /\ (q + tv) mod 2 = 0
          end
  | L2 => p + tv >= (if c4 then 4 else 5) * (2 * 2 ^ n) /\
          match n with
          | 0 => (q >= tv + 1 \/ (q + tv) mod 2 = 0) /\ (if c4 then q = tv else True)
          | S _ => (q + tv) mod 2 = 0
          end
  end.

(** clauses for pairs 1 and 2 (h only matters for pair 1) *)
Definition PI (ph : phase) (h i p q n tv : nat) : Prop :=
  match i with
  | 1 => h mod 2 = 0 /\
         match ph with
         | E1 | E1t => 2 <= n /\ p + tv + 2 ^ n + 3 >= 11 * 2 ^ n /\ h + 4 * (tv + 2 ^ n) + 6 >= 12 * 2 ^ n
         | E2 | E2t => 2 <= n /\ p + tv + 3 >= 11 * 2 ^ n /\ h + 4 * tv + 6 >= 12 * 2 ^ n
         | T0 => 2 <= n /\ p + tv + 5 * 2 ^ n + 3 >= 22 * 2 ^ n /\ h + 4 * (tv + 5 * 2 ^ n) + 6 >= 24 * 2 ^ n
         | L1 => 2 <= n /\ q >= tv + 3 * 2 ^ n /\ h + 4 * (tv + 2 ^ n) + 6 >= 8 * 2 ^ n
         | LX => 3 <= n /\ q >= tv + 2 * 2 ^ n /\ h + 4 * tv + 6 >= 8 * 2 ^ n
         | L2 => 1 <= n /\ q >= tv + 4 * 2 ^ n /\ h + 4 * tv + 6 >= 16 * 2 ^ n
         end
  | 2 => match ph with
         | E1 | E1t => p + tv + 2 ^ n + 1 >= 7 * 2 ^ n
         | E2 | E2t => p + tv + 1 >= 7 * 2 ^ n
         | T0 => p + tv + 5 * 2 ^ n + 1 >= 14 * 2 ^ n
         | L1 => q >= tv + 2 ^ n + 1
         | LX | L2 => q >= tv + 1
         end
  | _ => True
  end.

Definition PC (ph : phase) (c4 : bool) (h i p q n tv : nat) : Prop :=
  1 <= p /\ 1 <= q /\ PN ph c4 p q n tv /\ PI ph h i p q n tv.

Definition Lift (Pr : nat -> nat -> nat -> nat -> nat -> Prop) (i : nat) (x : tri) (Y : list tri) : Prop :=
  let '(p,q,d) := x in Pr i p q (length Y) (dv (x :: Y)).

Definition PCx (ph : phase) (c4 : bool) (h : nat) := Lift (PC ph c4 h).

Ltac dP := unfold PC, PN, PI in *.
Ltac unfL := unfold PCx, Lift in *; cbv beta iota in *.
Ltac unfLg := unfold PCx, Lift; cbv beta iota.
Ltac unfLh H := unfold PCx, Lift in H; cbv beta iota in H.
Ltac splitH := repeat match goal with H : _ /\ _ |- _ => destruct H end.
Ltac cr := cbn - [Nat.modulo] in *; splitH; repeat split; try lia.

Lemma pow_pos n : 1 <= 2 ^ n.
Proof. pose proof (Nat.pow_nonzero 2 n). lia. Qed.

(** a touch (every touched pair of a Dec step) *)
Lemma ob_touch ph c4 h i p q n tv : 1 <= tv -> 2 <= q ->
  PC ph c4 h i p q n tv -> PC ph c4 (4 + h) i (S p) (pred q) n (tv - 1).
Proof.
  intros Ht Hq [H1 [H2 [HN HI]]]. pose proof (pow_pos n). split; [lia|]. split; [lia|]. split.
  - clear HI. unfold PN in *. destruct ph; try destruct c4; destruct n as [|[|n]]; cr.
  - clear HN. unfold PI in *. destruct i as [|[|[|i]]]; try exact I; destruct ph; cr.
Qed.

Lemma pow_S n : 2 ^ S n = 2 * 2 ^ n.
Proof. reflexivity. Qed.

Ltac prePC := match goal with H : PC _ _ _ _ _ _ _ _ |- _ => destruct H as (Hp & Hq0 & HN & HI) end;
  split; [lia|]; split; [lia|]; split.

(** a pair left of a DecMerge (L phases): n+1 -> n pairs to the right,
    tv = u + 2U -> u - 1 + U with u = 2^a (a >= 1), U = u * H *)
Lemma ob_merge ph c4 h i p q n u U :
  (ph = L1 \/ ph = L2 \/ ph = LX) ->
  1 <= n -> 2 <= u -> u mod 2 = 0 -> U mod 2 = 0 -> U + u <= 2 * 2 ^ n ->
  (ph = L1 -> U + u <= 2 ^ n) -> (ph = LX -> 2 <= n) -> (ph = L1 -> c4 = true -> 2 <= n) ->
  (i = 1 -> 2 <= n) -> (ph = LX -> i = 1 -> 3 <= n) -> 2 <= q ->
  PC ph c4 h i p q (S n) (u + 2 * U) -> PC ph c4 (4 + h) i (S p) (pred q) n (u - 1 + U).
Proof.
  intros Hph Hn Hu Hu2 HU2 HUu HL1 HLX Hc4 Hi1 HiX Hq H. pose proof (pow_pos n).
  prePC.
  - clear HI. unfold PN in *. repeat rewrite pow_S in *.
    destruct Hph as [-> | [-> | ->]]; try destruct c4; destruct n as [|[|n]]; cr.
  - clear HN. unfold PI in *. repeat rewrite pow_S in *.
    destruct i as [|[|[|i]]]; try exact I; destruct Hph as [-> | [-> | ->]]; cr.
Qed.

(** a pair left of a DecMergeTail (L2): tv = 2^(n+1) -> 2^(n+1) - 1, and c4 is cleared *)
Lemma ob_mt c4 h i p q n : 2 <= q -> (i = 1 -> 1 <= n) ->
  PC L2 c4 h i p q (S n) (2 * 2 ^ n) -> PC L2 false (4 + h) i (S p) (pred q) n (2 * 2 ^ n - 1).
Proof.
  intros Hq Hi1 H. pose proof (pow_pos n). prePC.
  - clear HI. unfold PN in *. repeat rewrite pow_S in *. destruct c4; destruct n as [|n]; cr.
  - clear HN. unfold PI in *. repeat rewrite pow_S in *. destruct i as [|[|[|i]]]; try exact I; cr.
Qed.

(** the fused pair inherits the right pair's suffix *)
Lemma ob_fuse ph c4 h h' k p p' q' n tv : (ph = L1 \/ ph = L2 \/ ph = LX) -> 3 <= k ->
  PC ph c4 h (S k) p' q' n tv -> PC ph c4 h' k (p + p' + 3) q' n tv.
Proof.
  intros Hph Hk H. pose proof (pow_pos n). prePC.
  - clear HI. unfold PN in *. destruct Hph as [-> | [-> | ->]]; try destruct c4; destruct n as [|[|n]]; cr.
  - unfold PI. destruct k as [|[|[|k]]]; try lia; exact I.
Qed.

(** pairs far from the head: the index and h do not matter *)
Lemma ob_far ph c4 h h' i j p q n tv : 3 <= i -> 3 <= j ->
  PC ph c4 h i p q n tv -> PC ph c4 h' j p q n tv.
Proof.
  intros Hi Hj [H1 [H2 [H3 _]]]. split; [lia|]. split; [lia|]. split; [exact H3|].
  unfold PI. destruct j as [|[|[|j]]]; try lia; exact I.
Qed.

(** End (E1 -> E2, E1t -> E2t) *)
Definition endtr (ph ph' : phase) : Prop := (ph = E1 /\ ph' = E2) \/ (ph = E1t /\ ph' = E2t).

Lemma ob_end ph ph' h i p q n : endtr ph ph' -> 1 <= n -> 2 <= q ->
  PC ph false h i p q n 0 -> PC ph' false (4 + h) i (S p) (pred q) n (2 ^ n - 1).
Proof.
  intros Hph Hn Hq H. pose proof (pow_pos n). prePC.
  - clear HI. unfold PN in *. destruct Hph as [[-> ->]|[-> ->]]; destruct n as [|n]; cr.
  - clear HN. unfold PI in *. destruct i as [|[|[|i]]]; try exact I; destruct Hph as [[-> ->]|[-> ->]]; cr.
Qed.

Lemma ob_end_top ph ph' h i p q : endtr ph ph' -> 3 <= i ->
  PC ph false h i p (S (S q)) 0 0 -> PC ph' false (4 + h) i (S p) (S q) 0 0.
Proof.
  intros Hph Hi H. prePC.
  - clear HI. unfold PN in *. destruct Hph as [[-> ->]|[-> ->]]; cr.
  - unfold PI. destruct i as [|[|[|i]]]; try lia; exact I.
Qed.

(** EndLast (L1 -> L2) *)
Lemma ob_endlast c4 h i p q n : 2 <= q ->
  PC L1 c4 h i p q (S n) 0 -> PC L2 c4 (4 + h) i (S p) (pred q) n (2 * 2 ^ n - 1).
Proof.
  intros Hq H. pose proof (pow_pos n). prePC.
  - clear HI. unfold PN in *. repeat rewrite pow_S in *. destruct c4; destruct n as [|n]; cr.
  - clear HN. unfold PI in *. repeat rewrite pow_S in *. destruct i as [|[|[|i]]]; try exact I; cr.
Qed.

(** X2 (T0 -> E1t) *)
Lemma ob_x2 h i p q n : 1 <= n -> 2 <= q ->
  PC T0 false h i p q n 0 -> PC E1t false (4 + h) i (S p) (pred q) (S n) (3 * 2 ^ n - 1).
Proof.
  intros Hn Hq H. pose proof (pow_pos n). prePC.
  - clear HI. unfold PN in *. repeat rewrite pow_S in *. destruct n as [|n]; cr.
  - clear HN. unfold PI in *. repeat rewrite pow_S in *. destruct i as [|[|[|i]]]; try exact I; cr.
Qed.

Lemma ob_x2_top h i p q : 3 <= i ->
  PC T0 false h i p (S (S q)) 0 0 -> PC E1t false (4 + h) i (S p) (S q) 1 2.
Proof.
  intros Hi H. prePC.
  - clear HI. unfold PN in *. cr.
  - unfold PI. destruct i as [|[|[|i]]]; try lia; exact I.
Qed.

Lemma ob_x2_new h i k : 3 <= i -> 3 <= k -> PC E1t false h i 3 k 0 1.
Proof.
  intros Hi Hk. split; [lia|]. split; [lia|]. split.
  - unfold PN. cr.
  - unfold PI. destruct i as [|[|[|i]]]; try lia; exact I.
Qed.

(** Ov (E2 -> L1/LX, E2t -> L1 with c4, L2 -> E1).  Xp: condition on the old far p (= x). *)
Definition ovtr (ph ph' : phase) (c4' : bool) (Xp : nat -> Prop) : Prop :=
  (ph = E2 /\ ph' = L1 /\ c4' = false /\ Xp = (fun x => x <> 4)) \/
  (ph = E2 /\ ph' = LX /\ c4' = false /\ Xp = (fun x => x = 4)) \/
  (ph = E2t /\ ph' = L1 /\ c4' = true /\ Xp = (fun _ => True)) \/
  (ph = L2 /\ ph' = E1 /\ c4' = false /\ Xp = (fun _ => True)).

Lemma ob_ov_head ph ph' c4' Xp h p1 q1 n : ovtr ph ph' c4' Xp ->
  PC ph false h 1 (S (S p1)) q1 n 0 -> PC ph' c4' 2 1 (h + 5) (S p1) (S n) (2 * (2 * 2 ^ n) - 2).
Proof.
  intros Htr H. pose proof (pow_pos n). prePC.
  - unfold PN, PI in *. repeat rewrite pow_S in *.
    destruct Htr as [(-> & -> & -> & _)|[(-> & -> & -> & _)|[(-> & -> & -> & _)|(-> & -> & -> & _)]]];
      destruct n as [|[|n]]; cr.
  - unfold PN, PI in *. repeat rewrite pow_S in *.
    destruct Htr as [(-> & -> & -> & _)|[(-> & -> & -> & _)|[(-> & -> & -> & _)|(-> & -> & -> & _)]]];
      destruct n as [|[|n]]; cr.
Qed.

Lemma ob_ov_step ph ph' c4' Xp h i pp q p' q' m : ovtr ph ph' c4' Xp -> 1 <= i ->
  PC ph false h i pp q (S m) 0 -> PC ph false h (S i) p' q' m 0 -> (m = 0 -> Xp p') ->
  PC ph' c4' 2 (S i) q p' (S m) (2 * (2 * 2 ^ m) - 1).
Proof.
  intros Htr Hi H H' HX. pose proof (pow_pos m). destruct H as (Hp & Hq & HN & HI).
  destruct H' as (Hp' & Hq' & HN' & HI').
  split; [lia|]. split; [lia|]. split.
  - clear HI HI'. unfold PN in *. repeat rewrite pow_S in *.
    destruct Htr as [(-> & -> & -> & ->)|[(-> & -> & -> & ->)|[(-> & -> & -> & ->)|(-> & -> & -> & ->)]]];
      destruct m as [|[|m]]; cr.
  - unfold PI. destruct i as [|[|i]]; [lia| |exact I].
    unfold PN, PI in *. repeat rewrite pow_S in *.
    destruct Htr as [(-> & -> & -> & ->)|[(-> & -> & -> & ->)|[(-> & -> & -> & ->)|(-> & -> & -> & ->)]]];
      destruct m as [|[|m]]; cr.
Qed.

Lemma ob_ov_base ph ph' c4' Xp h i pp q t : ovtr ph ph' c4' Xp -> 1 <= i ->
  (ph = L2 -> 2 <= t) -> (ph <> L2 -> t = 1) ->
  PC ph false h i pp q 0 0 -> PC ph' c4' 2 (S i) q (S t) 0 1.
Proof.
  intros Htr Hi Ht1 Ht2 H. unfold PC in H. splitH. split; [lia|]. split; [lia|].
  unfold PN, PI in *.
  destruct Htr as [(-> & -> & -> & ->)|[(-> & -> & -> & ->)|[(-> & -> & -> & ->)|(-> & -> & -> & ->)]]];
    destruct i as [|[|[|i]]]; cr; try (specialize (Ht2 ltac:(discriminate)); lia);
    specialize (Ht1 eq_refl); lia.
Qed.

(** X1 (LX -> T0) *)
Lemma ob_x1_head h p1 q1 n :
  PC LX false h 1 (S (S p1)) q1 (S (S n)) 0 -> PC T0 false 2 1 (h + 5) (S p1) (S n) (2 * 2 ^ n - 2).
Proof.
  intros H. pose proof (pow_pos n). prePC; unfold PN, PI in *; repeat rewrite pow_S in *;
  destruct n as [|[|n]]; cr.
Qed.

Lemma ob_x1_step h i pp q p' q' m : 1 <= i ->
  PC LX false h i pp q (S (S (S m))) 0 -> PC LX false h (S i) p' q' (S (S m)) 0 ->
  PC T0 false 2 (S i) q p' (S m) (2 * 2 ^ m - 1).
Proof.
  intros Hi H H'. pose proof (pow_pos m). unfold PC in H, H'. splitH. split; [lia|]. split; [lia|].
  unfold PN, PI in *. repeat rewrite pow_S in *. destruct m as [|m]; destruct i as [|[|[|i]]]; cr.
Qed.

Lemma ob_x1_base h i pp q pa : 1 <= i ->
  PC LX false h i pp q 2 0 -> PC LX false h (S i) (S pa) 1 1 0 -> PC T0 false 2 (S i) q (S pa) 0 0.
Proof.
  intros Hi H H'. unfold PC in H, H'. splitH. split; [lia|]. split; [lia|].
  unfold PN, PI in *. destruct i as [|[|[|i]]]; cr.
Qed.

(** * List-level preservation, one lemma per rule *)

Lemma dv_zero Z : Forall dig0 Z -> dv Z = 0.
Proof. intros H. pose proof (dv_zeros Z [] H). rewrite app_nil_r in H0. cbn in H0. lia. Qed.

Lemma dv_tz' Z R : Forall dig0 Z -> dv (map touch Z ++ R) = 2 ^ length Z - 1 + 2 ^ length Z * dv R.
Proof. intros H. pose proof (dv_tz Z R H). lia. Qed.

Lemma ovp_len q Z t : length (ovp q Z t) = S (length Z).
Proof. revert q. induction Z as [|[[p q'] d] Z IH]; intros q; cbn; [reflexivity|]. rewrite IH. reflexivity. Qed.

Lemma ovp_dv q Z t : dv (ovp q Z t) + 1 = 2 ^ S (length Z).
Proof.
  revert q. induction Z as [|[[p q'] d] Z IH]; intros q; cbn [ovp dv bv length]; [cbn; lia|].
  specialize (IH q'). rewrite (pow_S (S (length Z))). lia.
Qed.

Lemma ovpX_len q Z pa : length (ovpX q Z pa) = S (length Z).
Proof. revert q. induction Z as [|[[p q'] d] Z IH]; intros q; cbn; [reflexivity|]. rewrite IH. reflexivity. Qed.

Lemma ovpX_dv q Z pa : dv (ovpX q Z pa) + 1 = 2 ^ length Z.
Proof.
  revert q. induction Z as [|[[p q'] d] Z IH]; intros q; cbn [ovpX dv bv length]; [cbn; lia|].
  specialize (IH q'). rewrite (pow_S (length Z)). lia.
Qed.

Fixpoint lastOK (Xp : nat -> Prop) (Z : list tri) : Prop :=
  match Z with
  | [] => True
  | [(p,_,_)] => Xp p
  | _ :: Z' => lastOK Xp Z'
  end.

Lemma lastOK_cons Xp p q d Z : lastOK Xp ((p,q,d) :: Z) -> (Z = [] -> Xp p) /\ lastOK Xp Z.
Proof. destruct Z as [|z Z]; cbn; [tauto|]. intros H. split; [discriminate | exact H]. Qed.

Lemma lastOK_dec Z : lastOK (fun x => x = 4) Z \/ lastOK (fun x => x <> 4) Z.
Proof.
  induction Z as [|[[p q] d] Z IH]; [left; exact I|].
  destruct Z as [|z Z]; [cbn; lia | exact IH].
Qed.

Lemma AllI_ovp ph ph' c4' Xp h t : ovtr ph ph' c4' Xp -> (ph = L2 -> 2 <= t) -> (ph <> L2 -> t = 1) ->
  forall Z i pp q, 1 <= i -> Forall dig0 Z -> lastOK Xp Z -> PC ph false h i pp q (length Z) 0 ->
  AllI (PCx ph false h) (S i) Z -> AllI (PCx ph' c4' 2) (S i) (ovp q Z t).
Proof.
  intros Htr Ht1 Ht2. induction Z as [|[[p' q'] d'] Z IH]; intros i pp q Hi HZ HX H HA.
  - cbn [ovp AllI]. split; [|exact I]. unfL. cbn [length dv bv].
    eapply ob_ov_base; eauto.
  - cbn [ovp AllI]. inversion HZ as [|? ? Hd HZ']; subst. unfold dig0, dig in Hd. subst d'.
    destruct HA as [Hh HA]. apply lastOK_cons in HX. destruct HX as [HX1 HX2].
    unfL. cbn [length] in H. rewrite dv_zero in Hh by (constructor; [reflexivity | exact HZ']).
    split.
    + unfL. rewrite ovp_len.
      replace (dv ((q, p', true) :: ovp q' Z t)) with (2 * (2 * 2 ^ length Z) - 1)
        by (cbn [dv bv]; pose proof (ovp_dv q' Z t) as E; rewrite pow_S in E; lia).
      eapply ob_ov_step; eauto. intros E. apply HX1. destruct Z; [reflexivity | discriminate].
    + apply (IH (S i) p'); auto.
Qed.

Lemma AllI_ovpX h pa pb : forall Z i pp q, 1 <= i -> Forall dig0 Z ->
  PC LX false h i pp q (S (S (length Z))) 0 ->
  AllI (PCx LX false h) (S i) (Z ++ [(S pa, 1, false); (pb, 1, false)]) ->
  AllI (PCx T0 false 2) (S i) (ovpX q Z (S pa)).
Proof.
  induction Z as [|[[p' q'] d'] Z IH]; intros i pp q Hi HZ H HA.
  - cbn [ovpX AllI app] in *. split; [|exact I]. destruct HA as [Ha _].
    unfL. cbn [length dv bv] in *. eapply ob_x1_base; eauto.
  - cbn [ovpX AllI app] in *. inversion HZ as [|? ? Hd HZ']; subst. unfold dig0, dig in Hd. subst d'.
    destruct HA as [Hh HA]. unfL.
    rewrite length_app in Hh. cbn [length] in Hh.
    rewrite dv_zero in Hh
      by (constructor; [reflexivity|]; apply Forall_app; split; [exact HZ'|]; repeat constructor).
    split.
    + unfL. rewrite ovpX_len.
      replace (dv ((q, p', true) :: ovpX q' Z (S pa))) with (2 * 2 ^ length Z - 1)
        by (cbn [dv bv]; pose proof (ovpX_dv q' Z (S pa)) as E; lia).
      eapply ob_x1_step; eauto. replace (length Z + 2) with (S (S (length Z))) in Hh by lia. exact Hh.
    + apply (IH (S i) p'); auto. replace (length Z + 2) with (S (S (length Z))) in Hh by lia. exact Hh.
Qed.

(** pass-through pairs (digit 0 below a digit 1) have q >= 2 *)
Lemma passq ph c4 h i p q n tv : PC ph c4 h i p q n tv -> 2 <= tv -> tv mod 2 = 0 -> 2 <= q.
Proof.
  intros (Hp & Hq & HN & _) Ht Ht2. pose proof (pow_pos n). unfold PN in HN.
  destruct ph; try destruct c4; destruct n as [|[|n]]; cr.
Qed.

Lemma Z_okL ph c4 h : forall Z i x R, Forall dig0 Z -> dig x = true ->
  AllI (PCx ph c4 h) i (Z ++ x :: R) -> Forall okL Z.
Proof.
  induction Z as [|[[p q] d] Z IH]; intros i x R HZ Hx HA; [constructor|].
  inversion HZ as [|? ? Hd HZ']; subst. unfold dig0, dig in Hd. subst d.
  cbn [app AllI] in HA. destruct HA as [Hh HA]. constructor; [|eapply IH; eauto].
  cbn. split; [reflexivity|]. unfL. eapply passq; [exact Hh| |].
  - cbn [dv bv]. rewrite dv_zeros by exact HZ'. destruct x as [[px qx] dx]. cbn in Hx. subst dx.
    cbn [dv bv]. pose proof (pow_pos (length Z)). nia.
  - cbn [dv bv]. lia.
Qed.

(** a digit-1 pair with q = 1 (a run-out): only in L phases, never pairs 1 and 2 *)
Lemma borrow1 ph c4 h k p n tv : 1 <= k -> tv mod 2 = 1 -> PC ph c4 h k p 1 n tv ->
  (ph = L1 \/ ph = L2 \/ ph = LX) /\ 3 <= k /\
  (ph = L1 -> 1 <= n /\ tv + 1 <= 2 ^ n /\ (c4 = true -> 2 <= n)) /\ (ph = LX -> 2 <= n).
Proof.
  intros Hk Ht (Hp & Hq & HN & HI). pose proof (pow_pos n).
  assert (Hph : ph = L1 \/ ph = L2 \/ ph = LX).
  { clear HI. unfold PN in HN. destruct ph; try (left; reflexivity); try (right; left; reflexivity);
      try (right; right; reflexivity); exfalso; destruct n as [|n]; cr. }
  split; [exact Hph|]. split.
  - clear HN. unfold PI in HI. destruct k as [|[|[|k]]]; try lia;
      destruct Hph as [-> | [-> | ->]]; cr.
  - clear HI. unfold PN in HN. split; intros ->; [destruct c4|]; destruct n as [|[|n]]; cr; discriminate.
Qed.

Lemma even2 x : (2 * x) mod 2 = 0.
Proof. lia. Qed.

Lemma pc_len (Pr : nat -> tri -> list tri -> Prop) i P : AllI Pr i P -> True.
Proof. auto. Qed.

Ltac dvs := cbn [dv bv length app map] in *; repeat rewrite length_app in *; repeat rewrite length_map in *;
  cbn [length] in *.

Lemma inv_Dec ph c4 h Z p q R : Forall dig0 Z ->
  AllI (PCx ph c4 h) 1 (Z ++ (p, S (S q), true) :: R) ->
  AllI (PCx ph c4 (4 + h)) 1 (map touch Z ++ (S p, S q, false) :: R).
Proof.
  intros HZ HA. pose proof (AllI_app _ _ _ _ HA) as HB. cbn [AllI] in HB. destruct HB as [Hx HR].
  apply (AllI_touchZ (PCx ph c4 h) (PCx ph c4 (4 + h)) ((p, S (S q), true) :: R) ((S p, S q, false) :: R)); [exact HZ | | exact HA | ].
  - intros j p0 q0 Zr HZr Hj H. unfL. dvs.
    rewrite dv_zeros in H by exact HZr. rewrite dv_tz' by exact HZr. cbn [dv bv] in *.
    pose proof (pow_pos (length Zr)).
    replace (1 + 2 * (2 ^ length Zr - 1 + 2 ^ length Zr * (0 + 2 * dv R)))
      with (2 * (2 ^ length Zr * (1 + 2 * dv R)) - 1) by nia.
    apply (ob_touch ph c4 h j p0 q0); [nia| |exact H]. eapply passq; [exact H| nia | apply even2].
  - cbn [AllI]. split.
    + unfL. cbn [dv bv] in *.
      replace (0 + 2 * dv R) with (1 + 2 * dv R - 1) by lia.
      apply (ob_touch ph c4 h (1 + length Z) p (S (S q)) (length R) (1 + 2 * dv R)); [lia|lia|exact Hx].
    + eapply AllI_mono; [|exact HR]. intros j y Y Hj Hy. destruct y as [[py qy] dy].
      unfL. destruct Hy as (Hp & Hq & HN & HI). split; [lia|]. split; [lia|].
      split; [exact HN|]. unfold PI in *. destruct j as [|[|[|j]]]; try lia; try exact HI; exact I.
Qed.

Lemma snoc_nn (Z : list tri) y : Z ++ [y] <> [].
Proof. destruct Z; discriminate. Qed.

Definition minlen (ph : phase) : nat := match ph with LX => 3 | L2 => 1 | _ => 2 end.

Lemma head_len ph c4 h x Y : PCx ph c4 h 1 x Y -> minlen ph <= length Y.
Proof.
  destruct x as [[p q] d]. intros H. unfLh H. destruct H as (_ & _ & _ & HI). unfold PI in HI.
  destruct ph; cbn [minlen]; cr.
Qed.

Lemma AllI_len ph c4 h P : P <> [] -> AllI (PCx ph c4 h) 1 P -> S (minlen ph) <= length P.
Proof.
  destruct P as [|x Y]; [congruence|]. intros _ [H _]. apply head_len in H. cbn. lia.
Qed.

Lemma q2_V0 ph c4 h i p q n : PC ph c4 h i p q n 0 -> 1 <= n -> (ph = LX -> 2 <= n) -> 2 <= q.
Proof.
  intros (Hp & Hq & HN & _) Hn HX. pose proof (pow_pos n). unfold PN in HN.
  destruct ph; try destruct c4; destruct n as [|[|n]]; cr; specialize (HX eq_refl); lia.
Qed.

Lemma p1_V0 ph c4 h p q n : PC ph c4 h 1 p q n 0 -> (ph = E2 \/ ph = E2t \/ ph = L2 \/ ph = LX) -> 2 <= p.
Proof.
  intros (Hp & Hq & HN & HI) Hph. pose proof (pow_pos n). unfold PN, PI in *.
  destruct Hph as [-> | [-> | [-> | ->]]]; try destruct c4; destruct n as [|[|n]]; cr.
Qed.

Lemma L2_c4_V0 h i p q : PC L2 true h i p q 0 0 -> False.
Proof. intros (Hp & Hq & HN & _). unfold PN in HN. cr. Qed.

Lemma AllI_okRO ph c4 h : forall Z i, Forall dig0 Z -> AllI (PCx ph c4 h) i Z -> Forall okR Z /\ Forall okO Z.
Proof.
  induction Z as [|[[p q] d] Z IH]; intros i HZ HA; [split; constructor|].
  inversion HZ as [|? ? Hd HZ']; subst. unfold dig0, dig in Hd. subst d.
  destruct HA as [Hh HA]. destruct (IH (S i) HZ' HA) as [H1 H2]. unfLh Hh. destruct Hh as (Hp & Hq & _).
  split; constructor; auto; cbn; lia.
Qed.

Lemma inv_Merge ph c4 h Z p p' q' d' R0 : Forall dig0 Z ->
  AllI (PCx ph c4 h) 1 (Z ++ (p, 1, true) :: (p', q', d') :: R0) ->
  AllI (PCx ph c4 (4 + h)) 1 (map touch Z ++ (p + p' + 3, q', d') :: R0).
Proof.
  intros HZ HA. pose proof (AllI_app _ _ _ _ HA) as HB. cbn [AllI] in HB. destruct HB as [Hx [Hy HR]].
  pose proof (dv_lt ((p', q', d') :: R0)) as Hlt. cbn [length] in Hlt.
  set (Hd := dv ((p', q', d') :: R0)) in *.
  assert (Hx' := Hx). unfLh Hx'. cbn [length] in Hx'.
  change (dv ((p, 1, true) :: (p', q', d') :: R0)) with (1 + 2 * Hd) in Hx'.
  destruct (borrow1 ph c4 h (1 + length Z) p (S (length R0)) (1 + 2 * Hd)) as (Hph & Hk & HL1 & HLX);
    [lia | lia | exact Hx' |].
  apply (AllI_touchZ (PCx ph c4 h) (PCx ph c4 (4 + h)) ((p, 1, true) :: (p', q', d') :: R0)
           ((p + p' + 3, q', d') :: R0)); [exact HZ | | exact HA | ].
  - intros j p0 q0 Zr HZr Hj H0. unfLh H0. unfLg. rewrite !length_app, !length_map in *. cbn [length] in *. cbn [dv bv] in H0 |- *.
    rewrite dv_zeros in H0 by exact HZr. rewrite dv_tz' by exact HZr. cbn [dv bv] in H0 |- *.
    change (bv d' + 2 * dv R0) with Hd in H0 |- *.
    set (A := 2 ^ length Zr) in *. set (B := 2 ^ length R0) in *.
    assert (HA1 : 1 <= A) by apply pow_pos. assert (HB1 : 1 <= B) by apply pow_pos.
    assert (Hn : 2 ^ (length Zr + S (length R0)) = A * (2 * B)) by (rewrite Nat.pow_add_r; reflexivity).
    rewrite pow_S in Hlt. fold B in Hlt.
    replace (length Zr + S (S (length R0))) with (S (length Zr + S (length R0))) in H0 by lia.
    replace (0 + 2 * (A * (1 + 2 * Hd))) with (2 * A + 2 * (2 * A * Hd)) in H0 by ring.
    replace (1 + 2 * (A - 1 + A * Hd)) with (2 * A - 1 + 2 * A * Hd) by (clear - HA1; nia).
    assert (Hq2 : 2 <= q0).
    { eapply passq; [exact H0 | nia |]. replace (2 * A + 2 * (2 * A * Hd)) with (2 * (A + 2 * A * Hd)) by ring.
      apply even2. }
    eapply ob_merge; [exact Hph | lia | lia | | | | | | | | | exact Hq2 | exact H0].
    + apply even2.
    + replace (2 * A * Hd) with (2 * (A * Hd)) by ring. apply even2.
    + rewrite Hn. nia.
    + intros ->. destruct (HL1 eq_refl) as (_ & Hb & _). rewrite pow_S in Hb. fold B in Hb. rewrite Hn. nia.
    + intros ->. specialize (HLX eq_refl). lia.
    + intros -> Hc. destruct (HL1 eq_refl) as (_ & _ & Hc2). specialize (Hc2 Hc). lia.
    + intros ->. lia.
    + intros -> ->. specialize (HLX eq_refl). lia.
  - cbn [AllI]. split.
    + unfLh Hy. unfLg. change (dv ((p + p' + 3, q', d') :: R0)) with (dv ((p', q', d') :: R0)).
      replace (length Z + 1) with (1 + length Z) by lia.
      eapply ob_fuse; [exact Hph | lia | exact Hy].
    + eapply AllI_shift; [|exact HR]. intros j y Y Hj Hy0. destruct y as [[py qy] dy].
      unfLh Hy0. unfLg. eapply ob_far; [| | exact Hy0]; lia.
Qed.

Lemma inv_MT c4 h Z p : Forall dig0 Z -> AllI (PCx L2 c4 h) 1 (Z ++ [(p, 1, true)]) ->
  AllI (PCx L2 false (4 + h)) 1 (map touch Z) /\ 2 <= length Z.
Proof.
  intros HZ HA. pose proof (AllI_app _ _ _ _ HA) as HB. cbn [AllI] in HB. destruct HB as [Hx _].
  assert (Hx' := Hx). unfLh Hx'. cbn [length dv bv] in Hx'.
  destruct (borrow1 L2 c4 h (1 + length Z) p 0 (1 + 2 * 0)) as (_ & Hk & _); [lia | lia | exact Hx' |].
  split; [|lia]. rewrite <- (app_nil_r (map touch Z)).
  apply (AllI_touchZ (PCx L2 c4 h) (PCx L2 false (4 + h)) [(p, 1, true)] []); [exact HZ | | exact HA | exact I].
  intros j p0 q0 Zr HZr Hj H0. unfLh H0. unfLg. rewrite !length_app, !length_map in *. cbn [length] in *. cbn [dv bv] in H0 |- *.
  rewrite dv_zeros in H0 by exact HZr. rewrite dv_tz' by exact HZr. cbn [dv bv] in H0 |- *.
  pose proof (pow_pos (length Zr)).
  replace (length Zr + 1) with (S (length Zr)) in H0 by lia. rewrite Nat.add_0_r.
  replace (0 + 2 * (2 ^ length Zr * (1 + 2 * 0))) with (2 * 2 ^ length Zr) in H0 by ring.
  replace (1 + 2 * (2 ^ length Zr - 1 + 2 ^ length Zr * 0)) with (2 * 2 ^ length Zr - 1) by lia.
  apply (ob_mt c4); [| lia | exact H0].
  eapply passq; [exact H0 | lia | apply even2].
Qed.

Lemma inv_End ph ph' h Z p q : endtr ph ph' -> Forall dig0 Z ->
  AllI (PCx ph false h) 1 (Z ++ [(p, S (S q), false)]) ->
  AllI (PCx ph' false (4 + h)) 1 (map touch Z ++ [(S p, S q, false)]).
Proof.
  intros Htr HZ HA. pose proof (AllI_len _ _ _ _ (snoc_nn Z _) HA) as Hlen.
  rewrite length_app in Hlen. cbn [length] in Hlen.
  assert (Hm : minlen ph = 2) by (destruct Htr as [[-> _]|[-> _]]; reflexivity).
  pose proof (AllI_app _ _ _ _ HA) as HB. cbn [AllI] in HB. destruct HB as [Hx _].
  apply (AllI_touchZ (PCx ph false h) (PCx ph' false (4 + h)) [(p, S (S q), false)] [(S p, S q, false)]);
    [exact HZ | | exact HA | ].
  - intros j p0 q0 Zr HZr Hj H0. unfLh H0. unfLg. rewrite !length_app, !length_map in *. cbn [length] in *. cbn [dv bv] in H0 |- *.
    rewrite dv_zeros in H0 by exact HZr. rewrite dv_tz' by exact HZr. cbn [dv bv] in H0 |- *.
    pose proof (pow_pos (length Zr)).
    replace (0 + 2 * (2 ^ length Zr * (0 + 2 * 0))) with 0 in H0 by ring.
    replace (1 + 2 * (2 ^ length Zr - 1 + 2 ^ length Zr * (0 + 2 * 0))) with (2 ^ (length Zr + 1) - 1)
      by (rewrite Nat.add_1_r, pow_S; lia).
    apply (ob_end ph ph'); [exact Htr | lia | | exact H0].
    eapply q2_V0; [exact H0 | lia | intros ->; destruct Htr as [[? _]|[? _]]; discriminate].
  - cbn [AllI]. split; [|exact I]. unfLh Hx. unfLg. cbn [length dv bv] in *.
    apply (ob_end_top ph ph'); [exact Htr | lia | exact Hx].
Qed.

Lemma inv_X2 h Z p q k : Forall dig0 Z -> 3 <= k ->
  AllI (PCx T0 false h) 1 (Z ++ [(p, S (S q), false)]) ->
  AllI (PCx E1t false (4 + h)) 1 (map touch Z ++ [(S p, S q, false); (3, k, true)]).
Proof.
  intros HZ Hk HA. pose proof (AllI_len _ _ _ _ (snoc_nn Z _) HA) as Hlen.
  rewrite length_app in Hlen. cbn [length minlen] in Hlen.
  pose proof (AllI_app _ _ _ _ HA) as HB. cbn [AllI] in HB. destruct HB as [Hx _].
  apply (AllI_touchZ (PCx T0 false h) (PCx E1t false (4 + h)) [(p, S (S q), false)]
           [(S p, S q, false); (3, k, true)]); [exact HZ | | exact HA | ].
  - intros j p0 q0 Zr HZr Hj H0. unfLh H0. unfLg. rewrite !length_app, !length_map in *. cbn [length] in *. cbn [dv bv] in H0 |- *.
    rewrite dv_zeros in H0 by exact HZr. rewrite dv_tz' by exact HZr. cbn [dv bv] in H0 |- *.
    pose proof (pow_pos (length Zr)).
    replace (0 + 2 * (2 ^ length Zr * (0 + 2 * 0))) with 0 in H0 by ring.
    replace (1 + 2 * (2 ^ length Zr - 1 + 2 ^ length Zr * (0 + 2 * (1 + 2 * 0))))
      with (3 * 2 ^ (length Zr + 1) - 1) by (rewrite Nat.add_1_r, pow_S; lia).
    replace (length Zr + 2) with (S (length Zr + 1)) by lia.
    apply ob_x2; [lia | | exact H0].
    eapply q2_V0; [exact H0 | lia | discriminate].
  - cbn [AllI]. split; [|split; [|exact I]].
    + unfLh Hx. unfLg. cbn [length dv bv] in *. apply ob_x2_top; [lia | exact Hx].
    + unfLg. cbn [length dv bv]. apply ob_x2_new; lia.
Qed.

Lemma inv_EndLast c4 h Z p : Forall dig0 Z -> AllI (PCx L1 c4 h) 1 (Z ++ [(p, 1, false)]) ->
  AllI (PCx L2 c4 (4 + h)) 1 (map touch Z) /\ 2 <= length Z.
Proof.
  intros HZ HA. pose proof (AllI_len _ _ _ _ (snoc_nn Z _) HA) as Hlen.
  rewrite length_app in Hlen. cbn [length minlen] in Hlen.
  split; [|lia]. rewrite <- (app_nil_r (map touch Z)).
  apply (AllI_touchZ (PCx L1 c4 h) (PCx L2 c4 (4 + h)) [(p, 1, false)] []); [exact HZ | | exact HA | exact I].
  intros j p0 q0 Zr HZr Hj H0. unfLh H0. unfLg. rewrite !length_app, !length_map in *. cbn [length] in *. cbn [dv bv] in H0 |- *.
  rewrite dv_zeros in H0 by exact HZr. rewrite dv_tz' by exact HZr. cbn [dv bv] in H0 |- *.
  pose proof (pow_pos (length Zr)).
  replace (0 + 2 * (2 ^ length Zr * (0 + 2 * 0))) with 0 in H0 by ring.
  replace (length Zr + 1) with (S (length Zr)) in H0 by lia. rewrite Nat.add_0_r.
  replace (1 + 2 * (2 ^ length Zr - 1 + 2 ^ length Zr * 0)) with (2 * 2 ^ length Zr - 1) by lia.
  apply ob_endlast; [| exact H0].
  eapply q2_V0; [exact H0 | lia | discriminate].
Qed.

Lemma inv_Ov ph ph' c4' Xp h p1 q1 Z t : ovtr ph ph' c4' Xp -> (ph = L2 -> 2 <= t) -> (ph <> L2 -> t = 1) ->
  Forall dig0 Z -> lastOK Xp Z ->
  AllI (PCx ph false h) 1 ((S (S p1), q1, false) :: Z) ->
  AllI (PCx ph' c4' 2) 1 ((h + 5, S p1, false) :: ovp q1 Z t).
Proof.
  intros Htr Ht1 Ht2 HZ HX HA. cbn [AllI] in HA |- *. destruct HA as [Hh HA].
  assert (Hh' := Hh). unfLh Hh'. rewrite dv_zero in Hh' by (constructor; [reflexivity | exact HZ]).
  split.
  - unfLg. rewrite ovp_len.
    replace (dv ((h + 5, S p1, false) :: ovp q1 Z t)) with (2 * (2 * 2 ^ length Z) - 2)
      by (cbn [dv bv]; pose proof (ovp_dv q1 Z t) as E; rewrite pow_S in E; lia).
    eapply ob_ov_head; [exact Htr | exact Hh'].
  - eapply (AllI_ovp ph ph' c4' Xp h t Htr Ht1 Ht2 Z 1 (S (S p1)) q1); auto.
Qed.

Lemma inv_X1 h p1 q1 Z pa pb : Forall dig0 Z ->
  AllI (PCx LX false h) 1 ((S (S p1), q1, false) :: Z ++ [(S pa, 1, false); (pb, 1, false)]) ->
  AllI (PCx T0 false 2) 1 ((h + 5, S p1, false) :: ovpX q1 Z (S pa)).
Proof.
  intros HZ HA. cbn [AllI] in HA |- *. destruct HA as [Hh HA].
  assert (Hh' := Hh). unfLh Hh'.
  rewrite dv_zero in Hh'
    by (constructor; [reflexivity|]; apply Forall_app; split; [exact HZ|]; repeat constructor).
  rewrite length_app in Hh'. cbn [length] in Hh'. replace (length Z + 2) with (S (S (length Z))) in Hh' by lia.
  split.
  - unfLg. rewrite ovpX_len.
    replace (dv ((h + 5, S p1, false) :: ovpX q1 Z (S pa))) with (2 * 2 ^ length Z - 2)
      by (cbn [dv bv]; pose proof (ovpX_dv q1 Z (S pa)) as E; lia).
    exact (ob_x1_head _ _ _ _ Hh').
  - eapply (AllI_ovpX h pa pb Z 1 (S (S p1)) q1); auto.
Qed.