reify_and

Mathlib.Tactic.Sat.FromLRAT

URI: https://scilib.ai/kg/mathlib#Sat.Clause.reify_and

Lean4

/-- Negation turns OR into AND, so `¬⟦l ∨ c⟧_v ≡ ¬⟦l⟧_v ∧ ¬⟦c⟧_v`. -/
theorem reify_and {l : Literal} {a : Prop} {c : Clause} {b : Prop} (h₁ : Literal.reify v l a)
    (h₂ : Clause.reify v c b) : Clause.reify v (Clause.cons l c) (a ∧ b) :=
  ⟨fun H ↦ ⟨h₁.1 (by_contra fun hn ↦ H hn.elim), h₂.1 fun h ↦ H fun _ ↦ h⟩⟩

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru