Module ZIntervals

Require Import Coqlib Utf8 ToString PrintPos FastArith.
Require Import Util AdomLib.
Require Import Integers.
Require Psatz.

Inductive zitv : Type :=
| ZITV: Zfast -> Zfast -> zitv.

Instance ZitvToString : ToString zitv :=
  { to_string i :=
      let 'ZITV min max := i in
      ("[" ++ to_string min ++ "," ++ to_string max ++ "]")%string
  }.

Instance leb_zitv : leb_op zitv := fun (i1 i2: zitv) =>
  let 'ZITV min1 max1 := i1 in
  let 'ZITV min2 max2 := i2 in
  Zfastleb min2 min1 && Zfastleb max1 max2.

Lemma leb_eq:
  ∀ i:zitv, i ⊑ i = true.

Instance join_zitv : join_op zitv zitv := fun i1 i2 =>
  let 'ZITV min1 max1 := i1 in
  let 'ZITV min2 max2 := i2 in
  match Zfastcompare min1 min2, Zfastcompare max1 max2 with
  | (Lt | Eq), (Eq | Gt) => i1
  | (Eq | Gt), Lt | Gt, Eq => i2
  | Lt, Lt => ZITV min1 max2
  | Gt, Gt => ZITV min2 max1
  end.

Lemma join_eq:
  ∀ x:zitv, x ⊔ x = x.

Instance meet_zitv : meet_op zitv (zitv+⊥) := fun i1 i2 =>
  let 'ZITV min1 max1 := i1 in
  let 'ZITV min2 max2 := i2 in
  match Zfastcompare min1 min2, Zfastcompare max1 max2 with
  | (Eq | Gt), (Lt | Eq) => NotBot i1
  | (Lt | Eq), Gt | Lt, Eq => NotBot i2
  | Gt, Gt => if Zfastleb min1 max2 then NotBot (ZITV min1 max2) else Bot
  | Lt, Lt => if Zfastleb min2 max1 then NotBot (ZITV min2 max1) else Bot
  end.

Definition widening_hints : list Zfast :=
  (- Z.shiftl 1 63 : Zfast) ::
  (- Z.shiftl 1 31 : Zfast) ::
  (- Z.shiftl 1 15 : Zfast) ::
  (- Z.shiftl 1 7 : Zfast) ::
  (F0:Zfast) :: (F1:Zfast) ::
  (Z.shiftl 1 7 - 1 : Zfast) ::
  (Z.shiftl 1 8 - 1 : Zfast) ::
  (Z.shiftl 1 15 - 1 : Zfast) ::
  (Z.shiftl 1 16 - 1 : Zfast) ::
  (Z.shiftl 1 31 - 1 : Zfast) ::
  (Z.shiftl 1 32 - 1 : Zfast) ::
  (Z.shiftl 1 63 - 1 : Zfast) :: nil.

Definition widening_hints_rev : list Zfast :=
  List.rev_append widening_hints nil.

Definition next_larger z :=
  List.find (Zfastleb z) widening_hints.

Lemma next_larger_larger:
  ∀ n m, next_larger n = Some m -> n <= m.

Definition next_smaller z :=
  List.find (fun x => Zfastleb x z) widening_hints_rev.

Lemma next_smaller_smaller:
  ∀ n m, next_smaller n = Some m -> m <= n.

Definition widen_zitv i1 i2 :=
  let 'ZITV min1 max1 := i1 in
  let 'ZITV min2 max2 := i2 in
  let lemin := Zfastleb min1 min2 in
  let lemax := Zfastleb max2 max1 in
  if lemin && lemax then Just i1
  else
    let min :=
      if lemin then Some min1
      else next_smaller min2
    in
    let max :=
      if lemax then Some max1
      else next_larger max2
    in
    match min, max with
    | Some min, Some max => Just (ZITV min max)
    | _, _ => All
    end.

Lemma widen_eq:
  ∀ x:zitv, widen_zitv x x = Just x.

Instance gamma_zitv : gamma_op zitv Z := fun i v =>
  let 'ZITV m M := i in m <= v <= M.

Instance leb_zitv_correct : leb_op_correct zitv Z.

Instance join_zitv_correct : join_op_correct zitv zitv Z.

Lemma widen_incr:
  ∀ ab1 ab2, γ ab1 ⊆ γ (widen_zitv ab1 ab2).

Instance meet_zitv_correct: meet_op_correct zitv (zitv+⊥) Z.

Definition forward_neg (x:zitv+⊤) : zitv+⊤ :=
  match x with
  | Just (ZITV mx Mx) => Just (ZITV (Zfastopp Mx) (Zfastopp mx))
  | All => All
  end.

Lemma forward_neg_correct:
  ∀ x x_ab, x ∈ γ x_ab -> (-x) ∈ γ (forward_neg x_ab) .

Definition forward_mult (x y:zitv+⊤) : zitv+⊤+⊥ :=
  match x, y with
  | Just (ZITV mx Mx), Just (ZITV my My) =>
    let b1 := Zfastmul mx my in let b2 := Zfastmul mx My in
    let b3 := Zfastmul Mx my in let b4 := Zfastmul Mx My in
    NotBot (Just (ZITV (Zfastmin (Zfastmin b1 b4) (Zfastmin b3 b2))
                       (Zfastmax (Zfastmax b1 b4) (Zfastmax b3 b2))))
  | All, Just (ZITV m M) | Just (ZITV m M), All =>
     if (Zfasteqb m F0 && Zfasteqb M F0) then NotBot (Just (ZITV F0 F0))
     else NotBot All
  | All, All => NotBot All
  end.

Lemma Mult_interval_correct_min_max :
  forall a b c d x y : Z,
    a <= x <= b ->
    c <= y <= d ->
    Zmin (Zmin (a*c) (b*d)) (Zmin (b*c) (a*d)) <= x * y
        <= Zmax (Zmax (a*c) (b*d)) (Zmax (b*c) (a*d)).

Lemma forward_mult_correct:
  ∀ x x_ab, x ∈ γ x_ab ->
  ∀ y y_ab, y ∈ γ y_ab ->
    (x * y)%Z ∈ γ (forward_mult x_ab y_ab).

Definition forward_div_pos (x:zitv+⊤) (my My:Zfast) : zitv+⊤ :=
  match x with
  | Just (ZITV mx Mx) =>
    Just (ZITV (Zfastquot mx (if Zfastleb F0 mx then My else my))
               (Zfastquot Mx (if Zfastleb F0 Mx then my else My)))
  | All => All
  end.

Lemma Zquot_le_compat_l_neg:
  ∀ p q r : Z, p < 0 -> 0 < q <= r -> p ÷ q <= p ÷ r.

Lemma forward_div_pos_correct:
  ∀ x x_ab, x ∈ γ x_ab ->
  ∀ y my My, 0 < my /\ my <= y <= My ->
    (x ÷ y) ∈ γ (forward_div_pos x_ab my My).

Definition forward_div_neg (x:zitv+⊤) (my My:Zfast) : zitv+⊤ :=
  forward_neg (forward_div_pos x (Zfastopp My) (Zfastopp my)).

Lemma forward_div_neg_correct:
  ∀ x x_ab, x ∈ γ x_ab ->
  ∀ y my My, My < 0 /\ my <= y <= My ->
    (x ÷ y) ∈ γ (forward_div_neg x_ab my My).

Definition forward_div (x y:zitv+⊤) : zitv+⊤+⊥ :=
  if y ⊑ Just (ZITV F0 F0) then Bot
  else if x ⊑ Just (ZITV F0 F0) then NotBot (Just (ZITV F0 F0))
  else match y with
       | All => NotBot All
       | Just (ZITV my My) =>
         let p :=
           if Zfastleb My F0 then Bot
           else NotBot (forward_div_pos x (Zfastmax F1 my) My)
         in
         let n :=
           if Zfastleb F0 my then Bot
           else NotBot (forward_div_neg x my (Zfastmin Fm1 My))
         in p ⊔ n
       end.

Lemma forward_div_correct:
  ∀ x x_ab, x ∈ γ x_ab ->
  ∀ y y_ab, y ∈ γ y_ab ->
    y ≠ 0 ->
    (x ÷ y) ∈ γ (forward_div x_ab y_ab).

Definition forward_mod_pos_pos (x:zitv+⊤) (my My:Zfast) : zitv+⊤+⊥ :=
  match x with
  | All => NotBot (Just (ZITV F0 (Zfastsub My F1)))
  | Just (ZITV mx Mx) =>
    if Zfastleb F0 Mx then
    if (if Zfasteqb mx Mx then Zfasteqb my My else false)
    then
      let m := Zfastmod mx my in
      NotBot (Just (ZITV m m))
    else
      NotBot (Just (ZITV (if Zfastleb my Mx then F0 else Zfastmax F0 mx)
                         (Zfastmin (Zfastsub My F1) Mx)))
    else Bot
  end.

Lemma forward_mod_pos_pos_correct:
  ∀ x x_ab, x ∈ γ x_ab -> 0 <= x ->
  ∀ y my My, 0 < my /\ my <= y <= My ->
    (Z.rem x y) ∈ γ (forward_mod_pos_pos x_ab my My).

Definition forward_mod_pos (x:zitv+⊤) (my My:Zfast) : zitv+⊤+⊥ :=
  forward_mod_pos_pos x my My ⊔
  fmap forward_neg (forward_mod_pos_pos (forward_neg x) my My).

Lemma forward_mod_pos_correct:
  ∀ x x_ab, x ∈ γ x_ab ->
  ∀ y my My, 0 < my /\ my <= y <= My ->
    (Z.rem x y) ∈ γ (forward_mod_pos x_ab my My).

Definition forward_mod_neg (x:zitv+⊤) (my My:Zfast) : zitv+⊤+⊥ :=
  forward_mod_pos x (Zfastopp My) (Zfastopp my).

Lemma forward_mod_neg_correct:
  ∀ x x_ab, x ∈ γ x_ab ->
  ∀ y my My, My < 0 /\ my <= y <= My ->
    (Z.rem x y) ∈ γ (forward_mod_neg x_ab my My).

Definition forward_mod (x y:zitv+⊤) : zitv+⊤+⊥ :=
  if y ⊑ Just (ZITV F0 F0) then Bot
  else match y with
       | All =>
         match x with
         | All => NotBot All
         | Just (ZITV mx Mx) =>
           let M := Zfast_of_Nfast (Nfastmax (Zfastabs mx) (Zfastabs Mx)) in
           NotBot (Just (ZITV (Zfastopp M) M))
         end
       | Just (ZITV my My) =>
         let p :=
           if Zfastleb My F0 then Bot
           else forward_mod_pos x (Zfastmax F1 my) My
         in
         let n :=
           if Zfastleb F0 my then Bot
           else forward_mod_neg x my (Zfastmin Fm1 My)
         in p ⊔ n
       end.

Lemma forward_mod_correct:
  ∀ x x_ab, x ∈ γ x_ab ->
  ∀ y y_ab, y ∈ γ y_ab ->
    y ≠ 0 ->
    (Z.rem x y) ∈ γ (forward_mod x_ab y_ab).

Definition forward_lnot (x:zitv+⊤) : zitv+⊤ :=
  match x with
  | Just (ZITV mx Mx) => Just (ZITV (Zfastsub Fm1 Mx) (Zfastsub Fm1 mx))
  | All => All
  end.

Lemma forward_lnot_correct:
  ∀ x x_ab, x ∈ γ x_ab -> (Z.lnot x) ∈ γ (forward_lnot x_ab) .

Lemma le_common_bits :
  ∀ m p M, (m <= p <= M)%N ->
  ∀ i, (N.size (N.lxor m M) <= i)%N ->
  N.testbit m i = N.testbit p i /\ N.testbit p i = N.testbit M i.

Definition forward_and_pos (mx Mx my My:Nfast) : Nfast * Nfast :=
  let cx := N.size (Nfastlxor mx Mx) in
  let cy := N.size (Nfastlxor my My) in
  let c := Nfastmax cx cy in
  let onesc := Nfastones c in
  let high:Nfast := Nfastldiff (Nfastland mx my) onesc in
  (high, Nfastlor high (Nfastmin (Nfastland Mx onesc) (Nfastland My onesc))).

Lemma forward_and_pos_correct:
  ∀ mx x Mx, (mx <= x <= Mx)%N ->
  ∀ my y My, (my <= y <= My)%N ->
  ∀ r R, forward_and_pos mx Mx my My = (r, R) ->
  (r <= N.land x y <= R)%N.

Definition forward_or_pos (mx Mx my My:Nfast) : Nfast * Nfast :=
  let N := Nfastones (Nfastmax (N.size Mx) (N.size My)) in
  let (m, M) := forward_and_pos (Nfastldiff N Mx) (Nfastldiff N mx)
                                (Nfastldiff N My) (Nfastldiff N my) in
  (Nfastldiff N M, Nfastldiff N m)%N.

Lemma forward_or_pos_correct:
  ∀ mx x Mx, (mx <= x <= Mx)%N ->
  ∀ my y My, (my <= y <= My)%N ->
  ∀ r R, forward_or_pos mx Mx my My = (r, R) ->
  (r <= N.lor x y <= R)%N.

Definition forward_diff_pos (mx Mx my My:Nfast) : Nfast * Nfast :=
  let N := Nfastones (Nfastmax (N.size Mx) (N.size My)) in
  forward_and_pos mx Mx (Nfastldiff N My) (Nfastldiff N my).

Lemma forward_diff_pos_correct:
  ∀ mx x Mx, (mx <= x <= Mx)%N ->
  ∀ my y My, (my <= y <= My)%N ->
  ∀ r R, forward_diff_pos mx Mx my My = (r, R) ->
  (r <= N.ldiff x y <= R)%N.

Definition positive_part (i:zitv+⊤) : zitv+⊤+⊥ :=
  match i with
  | Just (ZITV x y) => if Zfastleb F0 y then NotBot (Just (ZITV (Zfastmax F0 x) y)) else Bot
  | All => NotBot All
  end.

Lemma positive_part_correct:
  ∀ i n, n ∈ γ i -> 0 <= n ->
  n ∈ γ (positive_part i).

Definition pos_bind fJJ fJA fAJ x y : zitv+⊤+⊥ :=
  do x <- positive_part x;
  do y <- positive_part y;
  match x, y return zitv+⊤+⊥ with
  | Just (ZITV mx Mx), Just (ZITV my My) =>
    let '(m, M) := fJJ (Nfast_of_Zfast mx) (Nfast_of_Zfast Mx)
                       (Nfast_of_Zfast my) (Nfast_of_Zfast My) in
    NotBot (Just (ZITV (Zfast_of_Nfast m) (Zfast_of_Nfast M)))
  | Just (ZITV mx Mx), All =>
    match fJA (Nfast_of_Zfast mx) (Nfast_of_Zfast Mx) with
    | None => NotBot All
    | Some (m, M) =>
      NotBot (Just (ZITV (Zfast_of_Nfast m) (Zfast_of_Nfast M)))
    end
  | All, Just (ZITV my My) =>
    match fAJ (Nfast_of_Zfast my) (Nfast_of_Zfast My) with
    | None => NotBot All
    | Some (m, M) =>
      NotBot (Just (ZITV (Zfast_of_Nfast m) (Zfast_of_Nfast M)))
    end
  | All, All => NotBot All
  end.

Lemma pos_bind_spec:
  ∀ x_ab x, Z.of_N x ∈ γ x_ab ->
  ∀ y_ab y, Z.of_N y ∈ γ y_ab ->
  ∀ (fJJ:Nfast -> Nfast -> Nfast -> Nfast -> Nfast * Nfast)
    (fAJ fJA:Nfast -> Nfast -> option (Nfast * Nfast)) f,
  (∀ mx x Mx, (mx <= x <= Mx)%N ->
   ∀ my y My, (my <= y <= My)%N ->
   ∀ r R, fJJ mx Mx my My = (r, R) ->
          (r <= f x y <= R)%N) ->
  (∀ mx x Mx, (mx <= x <= Mx)%N ->
   ∀ y r R, fJA mx Mx = Some (r, R) ->
          (r <= f x y <= R)%N) ->
  (∀ x my y My, (my <= y <= My)%N ->
   ∀ r R, fAJ my My = Some (r, R) ->
          (r <= f x y <= R)%N) ->
  Z.of_N (f x y) ∈ γ (pos_bind fJJ fJA fAJ x_ab y_ab).

Definition forward_land (x y:zitv+⊤) : zitv+⊤+⊥ :=
  pos_bind forward_and_pos (fun _ M => Some (F0, M))
                           (fun _ M => Some (F0, M)) x y ⊔
  pos_bind forward_diff_pos (fun _ M => Some (F0, M))
                            (fun _ _ => None) x (forward_lnot y) ⊔
  pos_bind forward_diff_pos (fun _ M => Some (F0, M))
                            (fun _ _ => None) y (forward_lnot x) ⊔
  fmap forward_lnot
    (pos_bind forward_or_pos (fun _ _ => None) (fun _ _ => None)
              (forward_lnot x) (forward_lnot y)).

Lemma forward_land_correct:
  ∀ x x_ab, x ∈ γ x_ab ->
  ∀ y y_ab, y ∈ γ y_ab ->
  Z.land x y ∈ γ (forward_land x_ab y_ab).

Definition forward_lor (x y:zitv+⊤) : zitv+⊤+⊥ :=
  fmap forward_lnot (forward_land (forward_lnot x) (forward_lnot y)).

Lemma forward_lor_correct:
  ∀ x x_ab, x ∈ γ x_ab ->
  ∀ y y_ab, y ∈ γ y_ab ->
  Z.lor x y ∈ γ (forward_lor x_ab y_ab).

Definition forward_lxor (x y:zitv+⊤) : zitv+⊤+⊥ :=
  do A <- forward_land x (forward_lnot y);
  do B <- forward_land (forward_lnot x) y;
  forward_lor A B.

Lemma forward_lxor_correct:
  ∀ x x_ab, x ∈ γ x_ab ->
  ∀ y y_ab, y ∈ γ y_ab ->
  Z.lxor x y ∈ γ (forward_lxor x_ab y_ab).

Definition forward_shl (x y:zitv+⊤) : zitv+⊤+⊥ :=
  match x with
  | All => NotBot All
  | Just (ZITV mx Mx) =>
    if (Zfastleb F0 mx && Zfastleb Mx F0)%bool then NotBot (Just (ZITV F0 F0))
    else
      match y with
      | All => NotBot All
      | Just (ZITV my My) =>
        if (Zfastleb (Zfastopp F64) my && Zfastleb My F64)%bool then
          NotBot (Just (ZITV (Zfastshl mx (if Zfastleb F0 mx then my else My))
                             (Zfastshl Mx (if Zfastleb F0 Mx then My else my))))
        else
          NotBot All
      end
  end.

Lemma forward_shl_correct:
  ∀ x x_ab, x ∈ γ x_ab ->
  ∀ y y_ab, y ∈ γ y_ab ->
  Z.shiftl x y ∈ γ (forward_shl x_ab y_ab).

Definition forward_shr (x y:zitv+⊤) : zitv+⊤+⊥ :=
  forward_shl x (forward_neg y).

Lemma forward_shr_correct:
  ∀ x x_ab, x ∈ γ x_ab ->
  ∀ y y_ab, y ∈ γ y_ab ->
  Z.shiftr x y ∈ γ (forward_shr x_ab y_ab).

Definition backward_cmp_l (c:comparison) (x y:zitv+⊤) : zitv+⊤+⊥ :=
  match c with
  | Ceq =>
    match x, y with
    | Just (ZITV mx Mx), Just (ZITV my My) =>
      if Zfastleb my Mx && Zfastleb mx My then NotBot y else Bot
    | _, _ => NotBot y
    end
  | Cne =>
    match y with
    | Just (ZITV my My) =>
      if Zfastleb My my then
        match x with
        | Just (ZITV mx Mx) =>
          if Zfastleb mx my && Zfastleb my mx then
            if Zfastleb Mx my && Zfastleb my Mx then Bot
            else NotBot (Just (ZITV (Zfastadd mx F1) Mx))
          else
            if Zfastleb Mx my && Zfastleb my Mx then
              NotBot (Just (ZITV mx (Zfastsub Mx F1)))
            else NotBot All
        | All => NotBot All
        end
      else NotBot All
    | All => NotBot All
    end
  | Cle =>
    match x, y with
    | Just (ZITV mx _), Just (ZITV _ My) =>
      if Zfastleb mx My then NotBot (Just (ZITV mx My)) else Bot
    | _, _ => NotBot All
    end
  | Cge =>
    match x, y with
    | Just (ZITV _ Mx), Just (ZITV my _) =>
      if Zfastleb my Mx then NotBot (Just (ZITV my Mx)) else Bot
    | _, _ => NotBot All
    end
  | Clt =>
    match x, y with
    | Just (ZITV mx _), Just (ZITV _ My) =>
      let Mx' := Zfastsub My F1 in
      if Zfastleb mx Mx' then NotBot (Just (ZITV mx Mx')) else Bot
    | _, _ => NotBot All
    end
  | Cgt =>
    match x, y with
    | Just (ZITV _ Mx), Just (ZITV my _) =>
      let mx' := Zfastadd my F1 in
      if Zfastleb mx' Mx then NotBot (Just (ZITV mx' Mx)) else Bot
    | _, _ => NotBot All
    end
  end.

Definition Zcmp (c:comparison) (z1 z2:Z) : bool :=
  match c, z1 ?= z2 with
  | Ceq, Eq | Clt, Lt | Cgt, Gt
  | Cle, (Lt|Eq) | Cge, (Gt|Eq)
  | Cne, (Lt|Gt) => true
  | _, _ => false
  end.

Lemma backward_cmp_l_correct:
  ∀ x x_ab, x ∈ γ x_ab ->
  ∀ y y_ab, y ∈ γ y_ab ->
  ∀ c, Zcmp c x y = true ->
    x ∈ γ (backward_cmp_l c x_ab y_ab).

Definition backward_mul_pos (res x:zitv+⊤) (my My:Zfast) : zitv+⊤+⊥ :=
  match res with
  | Just (ZITV mres Mres) =>
    let mx := Zfastopp (Zfastdiv (Zfastopp mres)
                                 (if Zfastleb F0 mres then My else my)) in
    let Mx := Zfastdiv Mres (if Zfastleb F0 Mres then my else My) in
    Just (ZITV mx Mx) ⊓ x
  | All => NotBot x
  end.

Lemma backward_mul_pos_correct:
  ∀ x x_ab, x ∈ γ x_ab ->
  ∀ y my My, 0 < my /\ my <= y <= My ->
  ∀ res_ab, (x * y)%Z ∈ γ res_ab ->
    x ∈ γ (backward_mul_pos res_ab x_ab my My).

Definition backward_mul_neg (res x:zitv+⊤) (my My:Zfast) : zitv+⊤+⊥ :=
  backward_mul_pos (forward_neg res) x (Zfastopp My) (Zfastopp my).

Lemma backward_mul_neg_correct:
  ∀ x x_ab, x ∈ γ x_ab ->
  ∀ y my My, My < 0 /\ my <= y <= My ->
  ∀ res_ab, (x * y)%Z ∈ γ res_ab ->
    x ∈ γ (backward_mul_neg res_ab x_ab my My).

Definition backward_mul_0 (res:zitv+⊤) : zitv+⊤+⊥ :=
  if Just (ZITV F0 F0) ⊑ res then NotBot All else Bot.

Lemma backward_mul_0_correct:
  ∀ x,
  ∀ y, 0 <= y <= 0 ->
  ∀ res_ab, (x * y)%Z ∈ γ res_ab ->
    x ∈ γ (backward_mul_0 res_ab).

Definition backward_mul_l (res x y:zitv+⊤) : zitv+⊤+⊥ :=
  match y with
  | All => NotBot All
  | Just (ZITV my My) =>
    let p :=
      if Zfastleb My F0 then Bot
      else backward_mul_pos res x (Zfastmax F1 my) My
    in
    let n :=
      if Zfastleb F0 my then Bot
      else backward_mul_neg res x my (Zfastmin Fm1 My)
    in
    let z :=
      if Zfastleb my F0 && Zfastleb F0 My then backward_mul_0 res
      else Bot
    in
    p ⊔ n ⊔ z
  end.

Lemma backward_mul_l_correct:
  ∀ x x_ab, x ∈ γ x_ab ->
  ∀ y y_ab, y ∈ γ y_ab ->
  ∀ res_ab, (x * y)%Z ∈ γ res_ab ->
    x ∈ γ (backward_mul_l res_ab x_ab y_ab).

Definition backward_or (res x y: zitv+⊤) : (zitv+⊤ * zitv+⊤)+⊥ :=
  match res with
  | Just (ZITV 0 0) =>
    do x' <- x ⊓ res;
    do y' <- y ⊓ res;
    NotBot (x', y')
  | _ => NotBot (x, y)
  end.

Lemma backward_or_correct:
  ∀ x x_ab, x ∈ γ x_ab ->
  ∀ y y_ab, y ∈ γ y_ab ->
  ∀ res_ab, (Z.lor x y) ∈ γ res_ab ->
    (x, y) ∈ γ (backward_or res_ab x_ab y_ab).