proposition: Lemma check_diseqs_complete_false_spec : forall dist t, check_diseqs_complete dist t = false <-> exists x y, In2 x y dist /\ forall i, i <? length t -> (t.[i] <> Some (x,y) /\ t.[i] <> Some (y,x)).
proof: Proof. intros dist t; induction dist as [ |a q IHq]; simpl; split; try discriminate. intros [x [y [H _]]]; inversion H. case_eq (check_diseqs_complete_aux a q t). rewrite IHq; clear IHq; intros _ [x [y [H2 H3]]]; inversion H2; clear H2; subst q; exists x; exists y; split; auto; constructor 2. constructor 1; auto. constructor 2; auto. rewrite check_diseqs_complete_aux_false_spec; intros [y [H1 H2]] _; clear IHq; exists a; exists y; split; auto; constructor; auto. intros [x [y [H1 H2]]]; case_eq (check_diseqs_complete_aux a q t); auto; rewrite IHq; clear IHq; inversion H1; clear H1. subst x q; rewrite check_diseqs_complete_aux_spec; intro H; destruct (H _ H0) as [i [H1 H3]]; elim (H2 _ H1); intros H4 H5; destruct H3; [elim H4|elim H5]; auto. subst k q; intros _; exists x; exists y; split; auto. Qed.
imports: List PArray Bool Int63 ZMicromega Misc State SMT_terms