proposition: Lemma prover_opt_rew : forall (thy: ThyP) (use_prover: bool) (n:nat) (st:state) (g : option HFormula), prover_opt thy use_prover n st g = match n with | O => Fail OutOfFuel | S n => let ProverTRec := prover_opt thy use_prover n in match unit_propagation n g st with | Success (hm,d) => Success(hm,nil,d) | Progress st' => (seq_prover (prover_case_split ProverTRec) (seq_prover (prover_impl_arrows ProverTRec) (prover_thy ProverTRec thy use_prover))) st' g | Fail f => Fail f end end.
proof: Proof. destruct n ; reflexivity. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause