(* Generated by Frama-C WP *)

Goal typed_ref_lemma_AdjacentDifferenceInverse.
Hint AdjacentDifferenceInverse,property.
Proof.
  intros n L K A B.
  intros H.

  apply natlike_rec2 with (z := n); auto with zarith.
  {
    intros.
    unfold P_Unchanged_2_ in *.
    unfold P_Unchanged_1_ in *.
    intros.
    intuition.
  }
  {
    intros.
    Require Import Psatz.
    replace (Z.succ z) with (1+z) in * by lia.

    assert(X: P_Unchanged_2_ L K A z). {
      apply H1; auto with zarith.
      - apply Q_UnchangedSection with (i := 1+z); auto with zarith.
      - apply Q_PartialSumSection with (i := 1+z); auto with zarith.
      - apply Q_AdjacentDifferenceSection with (i := 1+z); auto with zarith.
    } 

    unfold P_Unchanged_2_.
    unfold P_Unchanged_1_.
    intros.

    assert(Y: i < z \/ i = z) by lia.
    destruct Y as [less|equal].
    {
      apply X; auto with zarith.
    }
    {
      rewrite equal.
      rewrite H3; auto with zarith.
      rewrite Q_AccumulateDefaultNext; auto with zarith.
      rewrite H2; auto with zarith.
      rewrite <- H4; auto with zarith.

      assert (Z: z = 0 \/ z > 0) by lia.
      destruct Z as [zero|pos].
      {
        rewrite zero.
        rewrite Q_DifferenceEmptyOrSingle; auto with zarith.
        rewrite <- Q_AccumulateDefault0.
        lia.
      }
      {
        rewrite Q_DifferenceNext; auto with zarith.
        cut ((K .[ shift_sint32 A (z - 1)]) = L_Accumulate_2_ L B z).
        - lia.
        - rewrite <- X; auto with zarith.
          rewrite H3; auto with zarith.
          replace (1 + (z-1)) with z by lia.
          trivial.
      }
    }
  }











Qed.