proposition: Lemma shorten_clauses_not_stuck : forall df u st, shorten_clauses df u st = Fail Stuck -> False.
proof: Proof. unfold shorten_clauses. intros df u st. rewrite WMap.fold_elements. assert (Acc : (Progress st: dresult) <> Fail Stuck). { congruence. } revert Acc. generalize ((Progress st: dresult)). set (F:= (fun (a : dresult) (p : int * Annot.t watched_clause) => update_watched_clause df (fst p) (snd p) a)). induction (WMap.elements u nil). - simpl. congruence. - simpl. intros. revert H. apply IHl. unfold F. unfold update_watched_clause. destruct d. congruence. congruence. unfold insert_watched_clause. set (cl':= (normalise_watched_clause (Some df) (units (remove_watched_clause (fst a) (Annot.elt (snd a)) st0)) (Annot.deps (snd a)) (Annot.elt (snd a)))). unfold insert_normalised_clause. destruct (Annot.elt cl') ; try congruence. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause