Library ibw_aux



Set Implicit Arguments.

Require Import Bool.
Require Import Omega.
Require Import misc.
Require Import ibw_def.

Definition well_formed_ibw (w:ibw) := w 0 = false.

Definition delay (d:nat) (w:ibw) : ibw :=
  fun i => w (i - d).

Definition non_null_stream (w: ibw) :=
  forall i: nat, exists j: nat, j > i /\ w j = true.

Inductive index_of_one (w: ibw) (j: nat) (i: nat) : Prop :=
  iof: ones w i = j -> (forall i', ones w i' = j -> i <= i') -> index_of_one w j i.

Property index_of_one_functional:
  forall w j i i',
  index_of_one w j i -> index_of_one w j i' -> i = i'.
Proof.
  intros.
  inversion H.
  inversion H0.
  apply le_antisym;
    [ apply H2 | apply H4 ]; assumption.
Qed.

Definition well_formed_ones (ones_w: nat -> nat) :=
  ones_w 0 = 0
  /\
  forall i, (ones_w (S i) = S (ones_w i) \/ ones_w (S i) = ones_w i).

Section ones_properties.

  Property ones_impl_well_formed_ones:
    forall w: ibw,
    well_formed_ones (ones w).
  Proof.
    intros.
    split.
      simpl.
      reflexivity.

      intro.
      simpl.
      case_eq (w (S i)).
        intro H_w.
        left.
        simpl.
        reflexivity.

        intro H_w.
        right.
        simpl.
        reflexivity.
  Qed.

  Property red_ones:
    forall w: ibw,
    forall i,
      ones w i =
      match i with
      | 0 => 0
      | S i' =>
        let w_i := if w i then 1 else 0 in
        w_i + ones w i'
      end.
  Proof.
    intros.
    induction i.
      simpl.
      reflexivity.

      simpl.
      reflexivity.
  Qed.

  Property ones_S_i_eq_S_ones_i:
    forall (w:ibw),
    forall i,
    forall H_w_S_i_eq_1: w (S i) = true,
    ones w (S i) = 1 + ones w i.
  Proof.
    intros.
    simpl.
    rewrite H_w_S_i_eq_1.
    trivial.
  Qed.

  Property ones_S_i_eq_ones_i:
    forall (w:ibw) i,
    forall H_w_S_i_eq_0: w (S i) = false,
    ones w (S i) = ones w i.
  Proof.
    intros.
    simpl.
    rewrite H_w_S_i_eq_0.
    trivial.
  Qed.

  Property ones_pred_i_eq_pred_ones_i:
    forall (w:ibw),
    forall i,
    forall H_w_S_i_eq_1: w i = true,
    ones w (pred i) = pred (ones w i).
  Proof.
    intros.
    case_eq i.
      compute.
      reflexivity.

      intros i' H_i.
      simpl.
      rewrite <- H_i.
      rewrite H_w_S_i_eq_1.
      simpl.
      reflexivity.
  Qed.

  Property ones_pred_i_eq_ones_i:
    forall (w:ibw),
    forall i,
    forall H_w_S_i_eq_1: w i = false,
    ones w (pred i) = ones w i.
  Proof.
    intros.
    case_eq i.
      compute.
      reflexivity.

      intros i' H_i.
      simpl.
      rewrite <- H_i.
      rewrite H_w_S_i_eq_1.
      simpl.
      reflexivity.
  Qed.

  Remark le_prop_aux:
    forall i j x,
    forall H_i_le_j: i <= j,
    i <= x + j.
  Proof.
    intros.
    omega.
  Qed.

  Property ones_increasing_one:
    forall (w:ibw) i,
    ones w i <= ones w (S i).
  Proof.
    intros.
    simpl.
    eapply le_prop_aux.
    trivial.
  Qed.

  Property ones_increasing_x:
    forall (w:ibw) i x,
    ones w i <= ones w (x + i).
  Proof.
    intros.
    induction x.
      simpl.
      trivial.

     assert (H_add: S x + i = S (x + i)); auto with arith.
     rewrite H_add.
     simpl.
     eapply le_prop_aux.
     trivial.
  Qed.

  Property ones_increasing:
    forall (w:ibw) i j,
    forall (H_i_le_j: i <= j),
    ones w i <= ones w j.
  Proof.
    intros.
    case_eq j.
      case_eq i.
        trivial.

        intros n H_i_pos H_j.
        rewrite H_i_pos in H_i_le_j.
        rewrite H_j in H_i_le_j.
        absurd (S n <= 0); auto with arith.

      intros j' H_j.
      rewrite H_j in H_i_le_j.
      assert (exists x, j = x + i).
          exists (S j' - i).
          omega.
      inversion H.
      rewrite <- H_j.
      rewrite H0.
      eapply ones_increasing_x.
  Qed.

  Property ones_increasing_rev:
    forall (w:ibw) i j,
    forall (H_ones_i_le_ones_j: ones w i < ones w j),
    i <= j.
  Proof.
    intros.
    elim (le_lt_dec i j); auto.
    intros H_j_lt_i.
    absurd (ones w i < ones w j); auto.
    apply le_not_lt.
    apply ones_increasing.
    apply lt_le_weak.
    assumption.
  Qed.

  Property ones_i_le_i_aux:
    forall w:ibw,
    forall i,
    ones w i <= i.
  Proof.
    intros.
    induction i.
      simpl.
      trivial.

      case_eq (w (S i)).
        intro H_w.
        rewrite ones_S_i_eq_S_ones_i; auto.
        simpl.
        auto with arith.

        intro H_w.
        rewrite ones_S_i_eq_ones_i; trivial.
        auto with arith.
  Qed.

  Property w_i_eq_true_impl_ones_pos:
    forall w:ibw,
    forall i,
    forall H_i_ge_1: i > 0,
    forall H_w: w i = true,
    ones w i > 0.
  Proof.
    intros.
    case_eq i.
      intro H_i.
      rewrite H_i in H_i_ge_1.
      absurd (0 > 0); auto with arith.

      intros n H_i.
      simpl.
      rewrite H_i in H_w.
      rewrite H_w.
      auto with arith.
  Qed.

  Property ones_eq_0_impl_w_eq_false:
    forall w: ibw,

    forall i,
    forall H_i_ge_1: i > 0,
    forall H_ones_eq_0: ones w i = 0,
    w i = false.
  Proof.
    intros.
    case_eq i.
      intros H_i.
      rewrite H_i in H_i_ge_1.
      absurd (0 > 0); auto with arith.

      intros i' H_i.
      rewrite H_i in H_ones_eq_0.
      clear H_i H_i_ge_1 i.
      induction i'.
        simpl in H_ones_eq_0.
        case_eq (w 1).
          intro H_w.
          rewrite H_w in H_ones_eq_0.
          simpl in H_ones_eq_0.
          congruence.

          trivial.

        assert (H_S_i'_ge_1: S i' >= 1);
          auto with arith.
        assert (H_ones_S_i'_eq_0: ones w (S i') = 0).
          assert (H_tmp: 0 = ones w (S i')).
            apply le_n_O_eq.
            rewrite <- H_ones_eq_0.
            apply ones_increasing_one.
          auto.
        rewrite red_ones in H_ones_eq_0.
        rewrite H_ones_S_i'_eq_0 in H_ones_eq_0.
        simpl in H_ones_eq_0.
        case_eq (w (S (S i'))).
          intro H_w.
          rewrite H_w in H_ones_eq_0.
          simpl in H_ones_eq_0.
          congruence.

          trivial.
  Qed.

  Property ones_i_eq_0_impl_w_i'_eq_false:
    forall w: ibw,

    forall i,
    forall H_ones_eq_0: ones w i = 0,
    forall i',
    forall H_i'_ge_1: i' > 0,
    forall H_i'_le_i: i' <= i,
    w i' = false.
  Proof.
    intros.
    apply ones_eq_0_impl_w_eq_false; auto.
    assert (H_cc: 0 = ones w i').
      apply le_n_O_eq.
      rewrite <- H_ones_eq_0.
      apply ones_increasing.
      assumption.
    auto.
  Qed.

  Property w_i'_eq_false_impl_ones_i_eq_0:
    forall w: ibw,
    forall i,
    forall H_w: (forall i', forall H_i'_le_i: i' <= i, w i' = false),
    ones w i = 0.
  Proof.
    induction i.
      intros.
      simpl.
      trivial.

      intros.
      rewrite ones_S_i_eq_ones_i.
        rewrite IHi; auto.

        apply H_w.
        apply le_refl.
  Qed.

  Property non_null_impl_ones_i_ge_j:
    forall w: ibw,
    forall H_non_null_stream: non_null_stream w,
    forall j,
    exists i,
    ones w i >= j.
  Proof.
    induction j.
      exists 0.
      simpl.
      unfold ge.
      apply le_refl.

      elim IHj.
      intros i IH.
      elim (H_non_null_stream i).
      intros i' H_tmp.
      destruct H_tmp.
      exists i'.
      assert (H_aux: i' = S (pred i')).
        apply (S_pred i' i).
        assumption.
      rewrite H_aux.
      rewrite H_aux in H0.
      rewrite ones_S_i_eq_S_ones_i; auto.
      simpl.
      unfold ge.
      apply le_n_S.
      apply
        (le_trans
          j
          (ones w i)
          (ones w (pred i'))); auto.
      apply ones_increasing.
      apply lt_n_Sm_le.
      rewrite <- H_aux.
      assumption.
  Qed.

  Property non_null_impl_ones_i_le_j:
    forall w: ibw,
    forall H_non_null_stream: non_null_stream w,
    forall j,
    exists i,
    ones w i <= j.
  Proof.
    intros.
    exists 0.
    simpl.
    auto with arith.
  Qed.

  Lemma ones_continuous:
    forall w: ibw,
    forall k i,
    forall H_k_le_ones: k <= ones w i,
    exists j, j <= i /\ ones w j = k.
  Proof.
   induction i.
   simpl; intro; exists 0; split; simpl; try omega.
   case_eq (w (S i)); intro Hw; simpl; rewrite Hw; simpl.
   intro Hlt; inversion Hlt.
   exists (S i); split; auto. simpl; rewrite Hw; reflexivity.
   destruct (IHi H0) as [j [Hj1 Hj2]].
   exists j; split; omega.
   intro H; destruct (IHi H) as [j [Hj1 Hj2]].
   exists j; split; auto.
  Qed.

  Property non_null_impl_ones_i_eq_j:
    forall w: ibw,
    forall H_non_null_stream: non_null_stream w,
    forall j,
    exists i,
    ones w i = j.
  Proof.
    intros.
    elim (non_null_impl_ones_i_ge_j H_non_null_stream j).
    intros i H_ones_ge_j.
    unfold ge in H_ones_ge_j.
    elim (ones_continuous w i H_ones_ge_j).
    intros i_cc H_tmp.
    destruct H_tmp.
    exists i_cc.
    assumption.
  Qed.

  Property w_eq_impl_ones_eq:
    forall w1 w2: ibw,
    forall H_ones_eq: (forall i, i > 0 -> w1 i = w2 i),
    forall i,
    ones w1 i = ones w2 i.
  Proof.
    induction i.
      simpl.
      reflexivity.

      simpl.
      rewrite IHi.
      rewrite (H_ones_eq (S i)); auto with arith.
  Qed.

  Property ones_eq_impl_w_eq:
    forall (w1: ibw) ,
    forall (w2: ibw) ,
    forall H_ones_eq: (forall i, ones w1 i = ones w2 i),
    forall i,
    forall H_i_ge_1: i > 0,
    w1 i = w2 i.
  Proof.
    intros.
    case_eq i.
      intro H_i.
      rewrite H_i in H_i_ge_1.
      absurd (0 > 0); auto with arith.

      intros i' H_i.
      clear H_i H_i_ge_1 i.
      case_eq (w1 (S i'));
      case_eq (w2 (S i')).
        trivial.

        intros H_w2 H_w1.
        absurd (ones w1 (S i') = ones w2 (S i')); auto.
        simpl.
        rewrite H_w1, H_w2.
        simpl.
        rewrite (H_ones_eq i');
        auto.

        intros H_w2 H_w1.
        absurd (ones w1 (S i') = ones w2 (S i')); auto.
        simpl.
        rewrite H_w1, H_w2.
        simpl.
        rewrite (H_ones_eq i').
        auto.

        trivial.
  Qed.

  Property ibw_of_ones_ones_w_eq_w:
    forall w: ibw,

    forall i,
    forall H_i_ge_1: i > 0,
    ibw_of_ones (ones w) i = w i.
  Proof.
    induction i.
      intro H_i_ge_1.
      absurd (0 > 0); auto with arith.

      simpl.
      case_eq (w (S i)).
        intro H_w.
        change (1 + ones w i) with (S (ones w i)).
        rewrite S_n_nbeq_n.
        simpl.
        reflexivity.

        intro H_w.
        simpl.
        rewrite <- beq_nat_refl.
        simpl.
        reflexivity.
  Qed.

  Property ones_ibw_of_ones_ones_w_eq_ones_w:
    forall ones_w: nat -> nat,
    forall H_wf_ones: well_formed_ones ones_w,
    forall i,
    ones (ibw_of_ones ones_w) i = ones_w i.
  Proof.
    induction i.
      simpl.
      destruct H_wf_ones.
      rewrite H.
      reflexivity.

      simpl.
      rewrite IHi.
      destruct H_wf_ones.
      elim (H0 i).
        intro H_ones.
        rewrite H_ones.
        rewrite S_n_nbeq_n.
        simpl.
        reflexivity.

        intro H_ones.
        rewrite H_ones.
        rewrite <- beq_nat_refl.
        simpl.
        reflexivity.
  Qed.

End ones_properties.

Fixpoint zeros (w:ibw) (i:nat) { struct i } :=
  match i with
  | 0 => 0
  | S i' =>
    let not_w_i := if w i then 0 else 1 in
     not_w_i + zeros w i'
  end.

Theorem zeros_def:
  forall w: ibw,
  forall i,
  zeros w i = i - ones w i.
Proof.
  intros.
  induction i.
    simpl.
    reflexivity.

    case_eq (w (S i)).
      intro H_w_S_i.
      simpl.
      rewrite H_w_S_i.
      simpl.
      exact IHi.

      intro H_w_S_i.
      simpl.
      rewrite H_w_S_i.
      simpl.
      case_eq (ones w i).
        intro H_ones.
        rewrite H_ones in IHi.
        replace (i - 0) with i in IHi.
        rewrite <- IHi at 2.
        reflexivity.
        auto with arith.

        intros n H_ones.
        rewrite H_ones in IHi.
        assert (H_cc: S (zeros w i) = S (i - S n)).
          auto with arith.
        rewrite minus_Sn_m in H_cc;
          try solve [ rewrite <- H_ones;
                      apply ones_i_le_i_aux ].
        change ( S i - S n) with (i - n) in H_cc.
        exact H_cc.
Qed.

Section delay_properties.

  Property delay_d_w_eq_w:
    forall w: ibw,
    forall d,
    forall i,
    (delay d w) (i + d) = w i.
  Proof.
    intros.
    unfold delay.
    replace (i + d - d) with i; auto.
    omega.
  Qed.

  Property delay_d_w_eq_false:
    forall w: ibw,
    forall H_wf: well_formed_ibw w,
    forall d,
    forall i,
    forall H_i_le_d: i <= d,
    (delay d w) i = false.
  Proof.
    intros.
    unfold delay.
    assert (H_aux: i - d = 0).
      omega.
    rewrite H_aux; clear H_aux.
    assumption.
  Qed.

  Property ones_delay_d_w_eq_0:
    forall w: ibw,
    forall H_wf: well_formed_ibw w,
    forall d,
    forall i,
    forall H_i_le_d: i <= d,
    ones (delay d w) i = 0.
  Proof.
    intros.
    generalize (delay_d_w_eq_false H_wf H_i_le_d).
    intro.
    apply w_i'_eq_false_impl_ones_i_eq_0.
    intros.
    apply delay_d_w_eq_false; auto.
    apply (le_trans i' i d); auto.
  Qed.

  Property ones_delay_d_w_eq_ones_w:
    forall w: ibw,
    forall H_wf: well_formed_ibw w,
    forall d,
    forall i,
    ones (delay d w) (i + d) = ones w i.
  Proof.
    double induction d i.
      replace (i + 0) with i; auto.

      intros i' IHi.
      simpl.
      rewrite IHi.
      unfold delay.
      replace (S (i' + 0) - 0) with (S i'); auto.
      omega.

      intros d' IHd.
      rewrite <- (IHd 0).
      simpl.
      repeat rewrite ones_delay_d_w_eq_0; auto.
      unfold delay.
      replace (S d' - S d') with 0; auto with arith.
      rewrite H_wf.
      trivial.

      intros i' IH1 d' IH2.
      replace (S i' + S d') with (S (i' + S d')); auto.
      rewrite red_ones.
      rewrite IH1; auto.
      simpl.
      unfold delay.
      replace (S (i' + S d') - S d') with (S i'); auto.
      omega.
  Qed.

  Property ones_delay_d_w_i_eq_ones_w_i_m_d:
    forall w: ibw,
    forall H_wf: well_formed_ibw w,
    forall d,
    forall i,
    ones (delay d w) i = ones w (i - d).
  Proof.
    intros.
    elim (le_lt_dec i d).
      intro H_i_le_d.
      rewrite ones_delay_d_w_eq_0; auto.
      replace (i - d) with 0;
        try solve [ simpl; reflexivity ].
      omega.

     intro H_d_lt_i.
     replace i with ((i - d) + d); try omega.
     rewrite ones_delay_d_w_eq_ones_w; auto.
     replace (i - d + d - d) with (i - d); try omega.
  Qed.

  Property ones_w_le_ones_delay_d_w_p_d:
    forall w: ibw,
    forall H_wf: well_formed_ibw w,
    forall d,
    forall i,
    ones w i <= ones (delay d w) i + d.
  Proof.
    double induction d i.
      simpl.
      apply le_refl.

      intros i' IH.
      rewrite <- (ones_delay_d_w_eq_ones_w H_wf 0 (S i')).
      replace (S i' + 0) with (S i'); auto.
      replace (ones (delay 0 w) (S i') + 0) with (ones (delay 0 w) (S i')); auto.

      intros d' IH.
      simpl.
      auto with arith.

      intros i' IH1 d' IH2.
      apply
        (le_trans
          (ones w (S i'))
          (ones (delay d' w) (S i') + d')
          (ones (delay (S d') w) (S i') + S d'));
        auto.
      elim (le_lt_dec (S i') d').
        intro H_i_le_d.
        repeat rewrite ones_delay_d_w_eq_0; auto.
        simpl.
        auto.

        intro H_d_lt_i.
        assert (H_aux: S i' = (S i' - d') + d').
          omega.
          auto with arith.
        rewrite H_aux at 1; clear H_aux.
        rewrite ones_delay_d_w_eq_ones_w; auto.

        assert (H_aux: S i' = (S i' - S d') + S d').
          omega.
          auto with arith.
        rewrite H_aux at 2; clear H_aux.
        rewrite ones_delay_d_w_eq_ones_w; auto.

        rewrite <- minus_Sn_m; auto with arith.
        replace (S i' - S d') with (i' - d'); auto.
        replace (ones w (i' - d') + S d')
        with (S (ones w (i' - d') + d')); auto.

        case_eq (w (S (i' - d'))).
          intro H_w.
          rewrite ones_S_i_eq_S_ones_i; auto.

          intro H_w.
          rewrite ones_S_i_eq_ones_i; auto.
  Qed.

  Property ones_w_m_d_le_ones_delay_d_w:
    forall w: ibw,
    forall H_wf: well_formed_ibw w,
    forall d: nat,
    forall i: nat,
    (ones w i - d <= ones (delay d w) i)%Z.
  Proof.
    intros.
    unfold Zminus.
    apply <- Zle_plus_swap.
    unfold Zminus.
    rewrite Zopp_involutive.
    generalize (ones_w_le_ones_delay_d_w_p_d H_wf d i).
    intro.
    auto with zarith.
  Qed.

End delay_properties.


Definition w_true :=
  (fun i:nat =>
    match i with
    | 0 => false
    | _ => true
    end).

Definition w_false := (fun i:nat => false).

Section true_and_false_properties.

  Property w_true_well_formed:
    well_formed_ibw w_true.
  Proof.
    unfold well_formed_ibw.
    simpl.
    reflexivity.
  Qed.

  Property w_false_well_formed:
    well_formed_ibw w_false.
  Proof.
    unfold well_formed_ibw.
    simpl.
    reflexivity.
  Qed.

  Property ones_true_i_eq_i:
    forall i, ones w_true i = i.
  Proof.
    induction i.
      simpl.
      reflexivity.

      simpl.
      rewrite IHi.
      reflexivity.
  Qed.

  Property ones_false_i_eq_0:
    forall i, ones w_false i = 0.
  Proof.
    induction i.
      simpl.
      reflexivity.

      simpl.
      rewrite IHi.
      reflexivity.
  Qed.

End true_and_false_properties.


Section not_properties.

  Theorem ones_not_def:
    forall (w: ibw) i,
    ones (not w) i = i - ones w i.
  Proof.
    intros.
    induction i.
      simpl.
      trivial.

      case_eq (w (S i)).
        intro H_w.
        assert (H_not_w: not w (S i) = false).
          unfold not.
          rewrite H_w.
          simpl.
          trivial.
        rewrite ones_S_i_eq_ones_i; auto.
        rewrite ones_S_i_eq_S_ones_i; auto.

        intro H_w.
        assert (H_not_w: not w (S i) = true).
          unfold not.
          rewrite H_w.
          simpl.
          trivial.
        rewrite ones_S_i_eq_S_ones_i; auto.
        rewrite ones_S_i_eq_ones_i; auto.
        rewrite IHi.
        assert (H_aux: 1 + (i - ones w i) = S (i - ones w i)).
          simpl.
          trivial.
        rewrite H_aux; clear H_aux.
        generalize (ones_i_le_i_aux w i).
        intro H_f'_i_le_i.
        rewrite minus_Sn_m; auto.
  Qed.

  Property not_wf_compat:
    forall (w: ibw),
    well_formed_ibw (not w).
  Proof.
    intros.
    unfold well_formed_ibw.
    simpl.
    trivial.
  Qed.

End not_properties.


Section on_properties.

  Property on_eq_1_impl_w1_eq_1:
    forall (w1:ibw) (w2:ibw) i,
    forall (H_on_eq_1: on w1 w2 i = true),
    w1 i = true.
  Proof.
    intros.
    unfold on in H_on_eq_1.
    case_eq (w1 i).
      trivial.

      intro.
      rewrite H in H_on_eq_1.
      congruence.
  Qed.

  Property on_eq_1_impl_w2_eq_1:
    forall (w1:ibw) (w2:ibw) i,
    forall (H_on_eq_1: on w1 w2 i = true),
    w2 (ones w1 i) = true.
  Proof.
    intros.
    generalize (on_eq_1_impl_w1_eq_1 w1 w2 i H_on_eq_1).
    intro H_w1_eq_1.
    unfold on in H_on_eq_1.
    rewrite H_w1_eq_1 in H_on_eq_1.
    trivial.
  Qed.

  Property on_eq_0_and_w1_eq_1_impl_w2_eq_0:
    forall (w1:ibw) (w2:ibw) i,
    forall (H_on_eq_0: on w1 w2 i = false),
    forall (H_w1_eq_1: w1 i = true),
    w2 (ones w1 i) = false.
  Proof.
    intros.
    unfold on in H_on_eq_0.
    rewrite H_w1_eq_1 in H_on_eq_0.
    trivial.
  Qed.

  Theorem ones_on_def:
    forall w1 w2 :ibw,
    forall i,
    ones (on w1 w2) i = ones w2 (ones w1 i).
  Proof.
    intros.
    induction i.
    simpl.
    trivial.

    case_eq (on w1 w2 (S i)).
      intro H_on_eq_1.
      generalize (on_eq_1_impl_w1_eq_1 w1 w2 (S i) H_on_eq_1).
      intro H_w1_eq_1.
      generalize (on_eq_1_impl_w2_eq_1 w1 w2 (S i) H_on_eq_1).
      intro H_w2_eq_1.
      simpl.
      rewrite H_w1_eq_1.
      rewrite H_on_eq_1.
      unfold ones at 2.
      simpl.
      simpl in IHi.
      rewrite IHi.
      apply trans_eq with (1+ones w2 (ones w1 i)); auto with arith.
      rewrite <- ones_S_i_eq_S_ones_i with w2 (ones w1 i); auto.
      rewrite ones_S_i_eq_S_ones_i in H_w2_eq_1.
      simpl in H_w2_eq_1; assumption.
      exact H_w1_eq_1.

      intro H_on_eq_0.
      simpl.
      rewrite H_on_eq_0.
      simpl.
      simpl in IHi.
      rewrite IHi.
      case_eq (w1 (S i)).
        intro H_w1_eq_1.
        generalize (on_eq_0_and_w1_eq_1_impl_w2_eq_0 w1 w2 (S i) H_on_eq_0 H_w1_eq_1).
        intro H_w2_eq_0.
        simpl in H_w2_eq_0.
        rewrite H_w1_eq_1 in H_w2_eq_0.
        simpl in H_w2_eq_0.
        simpl.
        case_eq (ones w1 i);
          intros;
          rewrite H in H_w2_eq_0;
          simpl;
          rewrite H_w2_eq_0;
          trivial.

        intro H_w1_eq_0.
        trivial.
  Qed.

  Property ones_on_le_ones_w1:
    forall w1 w2 i, ones (on w1 w2) i <= ones w1 i.
  Proof.
    intros.
    induction i.
      unfold on.
      simpl.
      case_eq (w1 0).
        intro H_w1.
        simpl.
        case_eq (w2 0).
          trivial.
          auto with arith.
        trivial.

      simpl.
      case_eq (w1 (S i)).
        intro H_w1.
        unfold on at 1.
        simpl.
        rewrite H_w1.
        simpl.
        case_eq (w2 (S (ones w1 i))).
          intro H_w2.
          simpl.
          auto with arith.
          intro H_w2.
          simpl.
          auto with arith.

        intro H_w1.
        unfold on at 1.
        rewrite H_w1.
        simpl.
        trivial.
  Qed.

  Property ones_on_le_ones_w2:
    forall (w1:ibw) (w2:ibw) i, ones (on w1 w2) i <= ones w2 i.
  Proof.
    intros.
    rewrite ones_on_def.
    eapply ones_increasing.
    eapply ones_i_le_i_aux.
  Qed.

  Lemma on_le_i:
    forall (w1:ibw) (w2:ibw) i,
    forall (H_on: on w1 w2 i = true),
    (ones (on w1 w2) i <= i)%nat.
  Proof.
    intros.
    eapply ones_i_le_i_aux.
  Qed.

  Property on_wf_compat:
    forall (w1: ibw) (H_wf1: well_formed_ibw w1),
    forall (w2: ibw),
    well_formed_ibw (on w1 w2).
  Proof.
    intros.
    unfold well_formed_ibw.
    unfold on.
    rewrite H_wf1.
    trivial.
  Qed.

 Property on_w_true:
   forall w: ibw,

   forall i,
   forall H_i_ge_1: i > 0,
   (on w w_true) i = w i.
  Proof.
    intros.
    apply ones_eq_impl_w_eq; auto.
    clear H_i_ge_1 i.
    intros.
    rewrite ones_on_def.
    induction (ones w i).
      simpl.
      reflexivity.

      simpl.
      rewrite IHn.
      reflexivity.
  Qed.

  Property on_true_w:
    forall w: ibw,

    forall i,
    forall H_i_ge_1: i > 0,
    (on w_true w) i = w i.
  Proof.
    intros.
    apply ones_eq_impl_w_eq; auto.
    clear H_i_ge_1 i.
    intros.
    rewrite ones_on_def.
    rewrite ones_true_i_eq_i.
    reflexivity.
  Qed.

  Property on_w_false:
    forall w: ibw,

    forall i,
    forall H_i_ge_1: i > 0,
    (on w w_false) i = w_false i.
  Proof.
    intros.
    apply ones_eq_impl_w_eq; auto.
    clear H_i_ge_1 i.
    intros.
    rewrite ones_on_def.
    repeat rewrite ones_false_i_eq_0.
    reflexivity.
  Qed.

  Property on_false_w:
    forall w: ibw,
    forall i,
    forall H_i_ge_1: i > 0,
    (on w_false w) i = w_false i.
  Proof.
    intros.
    apply ones_eq_impl_w_eq; auto.
  Qed.

  Property on_assoc_aux:
    forall w1 w2 w3: ibw,

    forall i,
    forall H_i_ge_1: i > 0,
    (on (on w1 w2) w3) i = (on w1 (on w2 w3)) i.
  Proof.
    intros.
    apply ones_eq_impl_w_eq; auto.
    intro.
    repeat rewrite ones_on_def.
    reflexivity.
  Qed.

End on_properties.


Section prec_properties.

  Lemma prec_refl:
    forall w: ibw,
    prec w w.
  Proof.
    intros.
    unfold prec.
    intros.
    unfold ge.
    apply le_refl.
  Qed.

  Lemma prec_trans:
    forall w1 w2 w3: ibw,
    forall H_prec_w1_w2: prec w1 w2,
    forall H_prec_w2_w3: prec w2 w3,
    prec w1 w3.
  Proof.
    intros.
    unfold prec.
    intros.
    unfold ge.
    apply
      (le_trans
        (ones w3 i)
        (ones w2 i)
        (ones w1 i)).
    apply H_prec_w2_w3.
    apply H_prec_w1_w2.
  Qed.

  Lemma prec_antisym:
    forall (w1: ibw) ,
    forall (w2: ibw) ,
    forall H_prec_w1_w2: prec w1 w2,
    forall H_prec_w2_w1: prec w2 w1,
    forall i,
    forall H_i_ge_1: i > 0,
    w1 i = w2 i.
  Proof.
    intros w1 w2 H_prec_w1_w2 H_prec_w2_w1 i H_i_ge_1.
    apply ones_eq_impl_w_eq; auto.
    intro.
    apply le_antisym.
      apply H_prec_w2_w1.
      apply H_prec_w1_w2.
  Qed.

  Lemma on_prec_compat:
    forall w1 w2 w1' w2': ibw,
    forall H_prec_w1_w2: prec w1 w2,
    forall H_prec_w1'_w2': prec w1' w2',
    prec (on w1 w1') (on w2 w2').
  Proof.
    intros.
    unfold prec.
    intros.
    repeat rewrite ones_on_def.
    apply
      (le_trans
        (ones w2' (ones w2 i))
        (ones w2' (ones w1 i))
        (ones w1' (ones w1 i))).
      apply ones_increasing.
      apply H_prec_w1_w2.

      apply H_prec_w1'_w2'.
  Qed.

  Lemma on_prec_reg_l:
    forall w1 w2 w3: ibw,
    forall H_non_null: non_null_stream w3,
    forall H_prec_on: prec (on w3 w1) (on w3 w2),
    prec w1 w2.
  Proof.
    unfold prec.
    intros.
    elim (non_null_impl_ones_i_eq_j H_non_null i).
    intros i' H_i.
    pose (H_cc:= H_prec_on i').
    repeat rewrite (ones_on_def ) in H_cc.
    rewrite H_i in H_cc.
    exact H_cc.
  Qed.

  Property supremum_well_formed:
    forall w1 w2: ibw,
    well_formed_ibw (supremum w1 w2).
  Proof.
    intros.
    unfold well_formed_ibw.
    simpl.
    trivial.
  Qed.

  Property infimum_well_formed:
    forall w1 w2: ibw,
    well_formed_ibw (infimum w1 w2).
  Proof.
    intros.
    unfold well_formed_ibw.
    simpl.
    trivial.
  Qed.

  Property ones_supremum_well_formed:
    forall w1 w2: ibw,
    well_formed_ones (ones_supremum w1 w2).
  Proof.
    unfold well_formed_ones.
    split.
      unfold ones_supremum.
      simpl.
      reflexivity.

      intros.
      case_eq (w1 (S i)); intro H_w1;
      case_eq (w2 (S i)); intro H_w2.
        left.
        unfold ones_supremum.
        simpl.
        rewrite H_w1, H_w2.
        simpl.
        reflexivity.

        unfold ones_supremum.
        simpl.
        rewrite H_w1, H_w2.
        elim (lt_eq_lt_dec (ones w1 i) (ones w2 i)).
        intro H_tmp.
        elim H_tmp; clear H_tmp.
          intro H_cmp.
          left.
          repeat rewrite Min.min_l; try omega.

          intro H_cmp.
          right.
          repeat rewrite Min.min_r; try omega.

          intro H_cmp.
          right.
          repeat rewrite Min.min_r; try omega.

        unfold ones_supremum.
        simpl.
        rewrite H_w1, H_w2.
        elim (lt_eq_lt_dec (ones w1 i) (ones w2 i)).
        intro H_tmp.
        elim H_tmp; clear H_tmp.
          intro H_cmp.
          right.
          repeat rewrite Min.min_l; try omega.

          intro H_cmp.
          right.
          repeat rewrite Min.min_l; try omega.

          intro H_cmp.
          left.
          repeat rewrite Min.min_r; try omega.

        right.
        unfold ones_supremum.
        simpl.
        rewrite H_w1, H_w2.
        simpl.
        reflexivity.
  Qed.

  Property ones_infimum_well_formed:
    forall w1 w2: ibw,
    well_formed_ones (ones_infimum w1 w2).
  Proof.
    unfold well_formed_ones.
    split.
      unfold ones_infimum.
      simpl.
      reflexivity.

      intros.
      case_eq (w1 (S i)); intro H_w1;
      case_eq (w2 (S i)); intro H_w2.
        left.
        unfold ones_infimum.
        simpl.
        rewrite H_w1, H_w2.
        simpl.
        reflexivity.

        unfold ones_infimum.
        simpl.
        rewrite H_w1, H_w2.
        elim (lt_eq_lt_dec (ones w1 i) (ones w2 i)).
        intro H_tmp.
        elim H_tmp; clear H_tmp.
          intro H_cmp.
          right.
          repeat rewrite Max.max_r; try omega.

          intro H_cmp.
          left.
          repeat rewrite Max.max_l; try omega.

          intro H_cmp.
          left.
          repeat rewrite Max.max_l; try omega.

        unfold ones_infimum.
        simpl.
        rewrite H_w1, H_w2.
        elim (lt_eq_lt_dec (ones w1 i) (ones w2 i)).
        intro H_tmp.
        elim H_tmp; clear H_tmp.
          intro H_cmp.
          left.
          repeat rewrite Max.max_r; try omega.

          intro H_cmp.
          left.
          repeat rewrite Max.max_r; try omega.

          intro H_cmp.
          right.
          repeat rewrite Max.max_l; try omega.

        right.
        unfold ones_infimum.
        simpl.
        rewrite H_w1, H_w2.
        simpl.
        reflexivity.
  Qed.

  Property ones_supremum_correctness:
    forall w1 w2: ibw,
    forall i,
    ones (supremum w1 w2) i = (ones_supremum w1 w2) i.
  Proof.
    induction i.
      unfold ones_supremum.
      simpl.
      reflexivity.

      simpl.
      rewrite IHi.
      case_eq (beq_nat (ones_supremum w1 w2 (S i)) (ones_supremum w1 w2 i)).
        intro H_cmp.
        simpl.
        rewrite (beq_nat_true _ _ H_cmp).
        reflexivity.

        intro H_cmp.
        simpl.
        elim (ones_supremum_well_formed w1 w2).
        intros H_ones_0 H_tmp.
        elim (H_tmp i); clear H_tmp.
          intro H_ones.
          rewrite H_ones.
          reflexivity.

          intro H_ones.
          absurd (ones_supremum w1 w2 (S i) = ones_supremum w1 w2 i);
            auto.
          apply beq_nat_false.
          assumption.
  Qed.

  Property ones_infimum_correctness:
    forall w1 w2: ibw,
    forall i,
    ones (infimum w1 w2) i = (ones_infimum w1 w2) i.
  Proof.
    induction i.
      unfold ones_infimum.
      simpl.
      reflexivity.

      simpl.
      rewrite IHi.
      case_eq (beq_nat (ones_infimum w1 w2 (S i)) (ones_infimum w1 w2 i)).
        intro H_cmp.
        simpl.
        rewrite (beq_nat_true _ _ H_cmp).
        reflexivity.

        intro H_cmp.
        simpl.
        elim (ones_infimum_well_formed w1 w2).
        intros H_ones_0 H_tmp.
        elim (H_tmp i); clear H_tmp.
          intro H_ones.
          rewrite H_ones.
          reflexivity.

          intro H_ones.
          absurd (ones_infimum w1 w2 (S i) = ones_infimum w1 w2 i);
            auto.
          apply beq_nat_false.
          assumption.
  Qed.

  Property prec_w1_supremum:
    forall w1 w2: ibw,
    prec w1 (supremum w1 w2).
  Proof.
    intros.
    unfold prec.
    intros.
    rewrite ones_supremum_correctness.
    unfold ones_supremum.
    unfold ge.
    apply Min.le_min_l.
  Qed.

  Property prec_w2_supremum:
    forall w1 w2: ibw,
    prec w2 (supremum w1 w2).
  Proof.
    intros.
    unfold prec.
    intros.
    rewrite ones_supremum_correctness.
    unfold ones_supremum.
    unfold ge.
    apply Min.le_min_r.
  Qed.

  Property prec_infimum_w1:
    forall w1 w2: ibw,
    prec (infimum w1 w2) w1.
  Proof.
    intros.
    unfold prec.
    intros.
    rewrite ones_infimum_correctness.
    unfold ones_infimum.
    unfold ge.
    apply Max.le_max_l.
  Qed.

  Property prec_infimum_w2:
    forall w1 w2: ibw,
    prec (infimum w1 w2) w2.
  Proof.
    intros.
    unfold prec.
    intros.
    rewrite ones_infimum_correctness.
    unfold ones_infimum.
    unfold ge.
    apply Max.le_max_r.
  Qed.

  Property on_supremum_distr_r:
    forall (w1: ibw) ,
    forall w2 w3: ibw,
    forall i,
    forall H_i_ge_1: i > 0,
    on w1 (supremum w2 w3) i = supremum (on w1 w2) (on w1 w3) i.
  Proof.
    intros w1 w2 w3 i H_i_ge_1.
    apply ones_eq_impl_w_eq; auto.
    intros.
    rewrite ones_on_def.
    repeat rewrite ones_supremum_correctness.
    unfold ones_supremum.
    repeat rewrite ones_on_def.
    reflexivity.
  Qed.

  Property on_supremum_distr_l:
    forall w1 w2 w3: ibw,
    forall i,
    forall H_i_ge_1: i > 0,
    on (supremum w1 w2) w3 i = supremum (on w1 w3) (on w2 w3) i.
  Proof.
    intros w1 w2 w3 i.
    apply ones_eq_impl_w_eq; auto.
    clear i.
    intros.
    rewrite ones_on_def.
    repeat rewrite ones_supremum_correctness.
    unfold ones_supremum.
    repeat rewrite ones_on_def.
    elim (le_ge_dec (ones w1 i) (ones w2 i)); intro H_cmp.
      rewrite Min.min_l; auto.
      symmetry.
      apply Min.min_l.
      apply ones_increasing.
      exact H_cmp.

      rewrite Min.min_r; auto.
      symmetry.
      apply Min.min_r.
      apply ones_increasing.
      exact H_cmp.
  Qed.

  Property on_infimum_distr_r:
    forall (w1: ibw),
    forall w2 w3: ibw,
    forall i,
    forall H_i_ge_1: i > 0,
    on w1 (infimum w2 w3) i = infimum (on w1 w2) (on w1 w3) i.
  Proof.
    intros w1 w2 w3 i H_i_ge_1.
    apply ones_eq_impl_w_eq; auto.
    intros.
    rewrite ones_on_def.
    repeat rewrite ones_infimum_correctness.
    unfold ones_infimum.
    repeat rewrite ones_on_def.
    reflexivity.
  Qed.

  Property on_infimum_distr_l:
    forall w1 w2 w3: ibw,
    forall i,
    forall H_i_ge_1: i > 0,
    on (infimum w1 w2) w3 i = infimum (on w1 w3) (on w2 w3) i.
  Proof.
    intros w1 w2 w3 i H_i_ge_1.
    apply ones_eq_impl_w_eq; auto.
    clear H_i_ge_1 i.
    intros.
    rewrite ones_on_def.
    repeat rewrite ones_infimum_correctness.
    unfold ones_infimum.
    repeat rewrite ones_on_def.
    elim (le_ge_dec (ones w1 i) (ones w2 i)); intro H_cmp.
      rewrite Max.max_r; auto.
      symmetry.
      apply Max.max_r.
      apply ones_increasing.
      exact H_cmp.

      rewrite Max.max_l; auto.
      symmetry.
      apply Max.max_l.
      apply ones_increasing.
      exact H_cmp.
  Qed.

End prec_properties.

Definition sync_popl (w1 w2: ibw) : Prop :=
  exists d1,
  exists d2,
  prec w1 (delay d2 w2)
  /\
  prec w2 (delay d1 w1).

Section sync_properties.

  Property sync_popl_impl_sync:
    forall w1: ibw,
    forall H_wf_1: well_formed_ibw w1,
    forall w2: ibw,
    forall H_wf_2: well_formed_ibw w2,
    forall H_sync: sync_popl w1 w2,
    sync w1 w2.
  Proof.
    intros.
    elim H_sync.
    intros d1 H_tmp.
    elim H_tmp; clear H_tmp.
    intros d2 H_tmp.
    elim H_tmp; clear H_tmp.
    intros H_prec_w1_w2 H_prec_w2_w1.
    unfold sync.
    unfold prec in H_prec_w1_w2, H_prec_w2_w1.

    exists (- d1)%Z.
    exists d2.
    intros.
    split.

      apply Zle_left_rev.
      replace (ones w2 i - ones w1 i + - - d1)%Z
      with (ones w2 i + - (ones w1 i - d1))%Z;
        auto with zarith.
      apply Zle_left.
      apply
        (Zle_trans
          (ones w1 i - d1)%Z
          (ones (delay d1 w1) i)%Z
          (ones w2 i)%Z);
        try solve [ apply inj_le;
                    apply H_prec_w2_w1 ].
      apply ones_w_m_d_le_ones_delay_d_w; auto.

      apply Zle_left_rev.
      replace (d2 + - (ones w2 i - ones w1 i))%Z
      with (ones w1 i + - (ones w2 i - d2))%Z;
        auto with zarith.
      apply Zle_left.
      apply
        (Zle_trans
          (ones w2 i - d2)%Z
          (ones (delay d2 w2) i)%Z
          (ones w1 i)%Z);
        try solve [ apply inj_le;
                    apply H_prec_w1_w2 ].
      apply ones_w_m_d_le_ones_delay_d_w; auto.
  Qed.

  Property sync_sym:
    forall w1 w2: ibw,
    sync w1 w2 -> sync w2 w1.
  Proof.
    intros w1 w2 H_sync.
    unfold sync.
    elim H_sync.
    intros b1 H_tmp.
    elim H_tmp; clear H_tmp.
    intros b2 H_cmp.
    exists (-b2)%Z.
    exists (-b1)%Z.
    intros.
    destruct (H_cmp i); auto.
    split; omega.
  Qed.

  Property sync_refl:
    forall w: ibw,
    sync w w.
  Proof.
    intros.
    unfold sync.
    exists 0.
    exists 0.
    intros.
    split; auto with zarith.
    apply Zle_minus_le_0.
    apply Zle_refl.
  Qed.

  Property sync_trans:
    forall w1 w2 w3: ibw,
    forall H_sync12: sync w1 w2,
    forall H_sync23: sync w2 w3,
    sync w1 w3.
  Proof.
    intros.
    elim H_sync12.
    intros b1 H_tmp.
    elim H_tmp; clear H_tmp.
    intros b2 H_cmp12.
    elim H_sync23.
    intros b1' H_tmp.
    elim H_tmp; clear H_tmp.
    intros b2' H_cmp23.
    unfold sync.
    exists (b1 + b1')%Z.
    exists (b2 + b2')%Z.
    intros.
    destruct (H_cmp12 i); auto.
    destruct (H_cmp23 i); auto.
    assert (H_aux:
      (ones w3 i - ones w1 i =
       (ones w3 i - ones w2 i) + (ones w2 i - ones w1 i))%Z).
      omega.
    rewrite H_aux; clear H_aux.
    split; omega.
  Qed.

  Lemma on_sync_compat:
    forall (w1: ibw),
    forall (w2: ibw),
    forall (w1': ibw) (H_wf1': well_formed_ibw w1'),
    forall (w2': ibw) (H_wf2': well_formed_ibw w2'),
    forall H_sync_w1_w2: sync w1 w2,
    forall H_sync_w1'_w2': sync w1' w2',
    sync (on w1 w1') (on w2 w2').
  Proof.
    intros.
    elim H_sync_w1_w2.
    intros b1 H_tmp.
    elim H_tmp; clear H_tmp.
    intros b2 H_b1_le_ones_diff_le_b2.

    elim H_sync_w1'_w2'.
    intros b1' H_tmp.
    elim H_tmp; clear H_tmp.
    intros b2' H_b1'_le_ones_diff_le_b2'.

    unfold sync.

    pose (m_min_0_b1:= Zabs_nat (Zmin 0 b1)).
    pose (max_0_b2:= Zabs_nat (Zmax 0 b2)).
    exists (- m_min_0_b1 + b1')%Z.
    exists (max_0_b2 + b2')%Z.
    intro.
    repeat rewrite ones_on_def.
    split.
      apply
        (Zle_trans
          (- m_min_0_b1 + b1')%Z
          (ones w2' (ones w1 i - m_min_0_b1) - ones w1' (ones w1 i))%Z
          (ones w2' (ones w2 i) - ones w1' (ones w1 i))%Z).
        apply
          (Zle_trans
            (- m_min_0_b1 + b1')%Z
            (ones w2' (ones w1 i) - m_min_0_b1 - ones w1' (ones w1 i))%Z
            (ones w2' (ones w1 i - m_min_0_b1) - ones w1' (ones w1 i))%Z).
        destruct (H_b1'_le_ones_diff_le_b2' (ones w1 i)); auto.
        replace (ones w2' (ones w1 i) - m_min_0_b1 - ones w1' (ones w1 i))%Z
        with (- m_min_0_b1 + (ones w2' (ones w1 i) - ones w1' (ones w1 i)))%Z;
          auto with zarith.
        apply Zplus_le_compat; try solve [ apply Zle_refl ].
        generalize (ones_w_m_d_le_ones_delay_d_w H_wf2' m_min_0_b1 (ones w1 i)).
        rewrite ones_delay_d_w_i_eq_ones_w_i_m_d; auto.

        unfold Zminus.
        apply Zplus_le_compat_r.
        apply inj_le.
        apply ones_increasing.
        apply inj_le_rev.
        assert (H_cmp: (ones w1 i + b1 <= ones w2 i)%Z).
          destruct (H_b1_le_ones_diff_le_b2 i).
          apply Zle_0_minus_le.
          replace (ones w2 i - (ones w1 i + b1))%Z
          with (ones w2 i - ones w1 i + - b1)%Z; auto with zarith.

        unfold m_min_0_b1.
        elim (Zmin_spec 0 b1).
          intro H_tmp.
          elim H_tmp; clear H_tmp.
          intros H_0_le_b1 H_min.
          rewrite H_min.
          simpl.
          replace (ones w1 i - 0)%nat with (ones w1 i); auto with arith.
          apply (Zle_trans (ones w1 i) (ones w1 i + b1) (ones w2 i));
            try omega.

          intro H_tmp.
          elim H_tmp; clear H_tmp.
          intros H_0_gt_b1 H_min.
          rewrite H_min.
          elim (le_lt_dec (Zabs_nat b1) (ones w1 i)).
            intro H_diff.
            rewrite inj_minus1; auto.
            unfold Zminus.
            assert (H_aux: (- Zabs_nat b1 = b1)%Z).
              rewrite inj_Zabs_nat.
              elim (Zabs_spec b1).
                intro H_tmp.
                destruct H_tmp.
                congruence.
                intro H_tmp.
                destruct H_tmp.
                rewrite H0.
                auto with zarith.
            rewrite H_aux; clear H_aux.
            exact H_cmp.

            intro H_diff.
            apply
              (Zle_trans
                (ones w1 i - Zabs_nat b1)%nat
                0
                (ones w2 i)); try omega.
            rewrite inj_minus2; try solve [apply Zle_refl].
            unfold gt.
            exact H_diff.

      apply
        (Zle_trans
          (ones w2' (ones w2 i) - ones w1' (ones w1 i))%Z
          (ones w2' (ones w2 i) - ones w1' (ones w2 i - max_0_b2))%Z
          (max_0_b2 + b2')%Z).
        apply Zplus_le_compat; try solve [ apply Zle_refl ].
        assert (H_cc:
          (ones w1' (ones w2 i - max_0_b2) <= ones w1' (ones w1 i))%Z).
          apply inj_le.
          apply ones_increasing.
          unfold max_0_b2.
          destruct (H_b1_le_ones_diff_le_b2 i).
          elim (Zmax_spec 0 b2).
            intro H_tmp.
            elim H_tmp; clear H_tmp.
            intros H_b2 H_max.
            rewrite H_max.
            simpl.
            omega.

            intro H_tmp.
            elim H_tmp; clear H_tmp.
            intros H_b2 H_max.
            rewrite H_max.
            apply inj_le_rev.
            elim (le_lt_dec (Zabs_nat b2) (ones w2 i)).
              intro H_diff.
              rewrite inj_minus1; auto.
              rewrite inj_Zabs_nat.
              elim (Zabs_spec b2).
                intro H_tmp.
                destruct H_tmp.
                rewrite H2.
                auto with zarith.

                intro H_tmp.
                destruct H_tmp.
                congruence.

              intro H_diff.
              apply
                (Zle_trans
                  (ones w2 i - Zabs_nat b2)%nat
                  0
                  (ones w1 i)); try omega.
              rewrite inj_minus2; try solve [apply Zle_refl].
              unfold gt.
              exact H_diff.
        omega.

        apply
          (Zle_trans
            (ones w2' (ones w2 i) - ones w1' (ones w2 i - max_0_b2))%Z
            (ones w2' (ones w2 i) - (ones w1' (ones w2 i) - max_0_b2))%Z
            (max_0_b2 + b2')).
          apply Zplus_le_compat; try solve [ apply Zle_refl ].
          assert (H_cc:
            ((ones w1' (ones w2 i) - max_0_b2) <= ones w1' (ones w2 i - max_0_b2))%Z).
            generalize (ones_w_m_d_le_ones_delay_d_w H_wf1' max_0_b2 (ones w2 i)).
            rewrite ones_delay_d_w_i_eq_ones_w_i_m_d; auto.
          omega.

          destruct (H_b1'_le_ones_diff_le_b2' (ones w2 i)).
          omega.
  Qed.

End sync_properties.

Section subtyping_properties.

  Lemma on_subtyping_compat:
    forall (w1: ibw),
    forall (w2: ibw),
    forall (w1': ibw) (H_wf1': well_formed_ibw w1'),
    forall (w2': ibw) (H_wf2': well_formed_ibw w2'),
    forall H_sub_w1_w2: subtyping w1 w2,
    forall H_sub_w1'_w2': subtyping w1' w2',
    subtyping (on w1 w1') (on w2 w2').
  Proof.
    intros.
    destruct H_sub_w1_w2.
    destruct H_sub_w1'_w2'.
    split.
      apply on_prec_compat; auto.
      apply on_sync_compat; auto.
  Qed.

End subtyping_properties.