Theory CDCL.CDCL_W_Full

theory CDCL_W_Full
imports CDCL_W_Termination CDCL_WNOT
begin

context conflict_driven_clause_learning⇩W
begin
lemma rtranclp_cdcl⇩W_merge_stgy_distinct_mset_clauses:
  assumes
    invR: "cdcl⇩W_all_struct_inv R" and
    st: "cdcl⇩W_s'⇧*⇧* R S" and
    smaller: ‹no_smaller_propa R› and
    dist: "distinct_mset (clauses R)"
  shows "distinct_mset (clauses S)"
  using rtranclp_cdcl⇩W_stgy_distinct_mset_clauses[OF _ invR dist smaller]
  invR st rtranclp_mono[of cdcl⇩W_s' "cdcl⇩W_stgy⇧*⇧*"] cdcl⇩W_s'_is_rtranclp_cdcl⇩W_stgy
  by (auto dest!: cdcl⇩W_s'_is_rtranclp_cdcl⇩W_stgy)
end

end