proposition: Lemma case_split_rew : forall (st: state) (g : option HFormula) (cl: list literal), case_split cl st g = match cl with | nil => Backjump false (hconsmap st) nil LitSet.empty | f :: cl => match ProverT (insert_unit (annot_hyp f) st) g with | Success (m,prf,ann') => if negb (has_lit f ann') && annot_holds (units st) ann' then Backjump true m prf ann' else match augment_clauses prf (set_hmap m st) with | Success (m,d') => Backjump true m prf d' | Progress st' => match case_split cl st' g with | Failure f => Failure f | Backjump b m' prf' d' => Backjump b m' (prf++prf') (if b then d' else (LitSet.union d' (if (has_lit f ann') then (remove_lit f ann') else ann'))) end | Fail f => Failure f end | Fail f => Failure f | Progress st => Failure OutOfFuel end end.
proof: Proof. destruct cl ; reflexivity. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause