Theory CDCL.CDCL_W_Full

theory CDCL_W_Full
imports CDCL_W_Termination CDCL_WNOT
begin

context conflict_driven_clause_learningW
begin
lemma rtranclp_cdclW_merge_stgy_distinct_mset_clauses:
  assumes
    invR: "cdclW_all_struct_inv R" and
    st: "cdclW_s'** R S" and
    smaller: no_smaller_propa R and
    dist: "distinct_mset (clauses R)"
  shows "distinct_mset (clauses S)"
  using rtranclp_cdclW_stgy_distinct_mset_clauses[OF _ invR dist smaller]
  invR st rtranclp_mono[of cdclW_s' "cdclW_stgy**"] cdclW_s'_is_rtranclp_cdclW_stgy
  by (auto dest!: cdclW_s'_is_rtranclp_cdclW_stgy)
end

end