(* 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.