reify_one

Mathlib.Tactic.Sat.FromLRAT

URI: https://scilib.ai/kg/mathlib#Sat.Fmla.reify_one

Lean4

/-- Reification of a single clause formula. -/
theorem reify_one {c : Clause} {a : Prop} (h : Clause.reify v c a) : Fmla.reify v (Fmla.one c) a :=
  ⟨fun H ↦
    h.1 fun h ↦
      H
        ⟨fun
          | _, List.Mem.head .. => h⟩⟩

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

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

Разделы

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

Аффилиация

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