proof_of_subsumes

Mathlib.Tactic.Sat.FromLRAT

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

Lean4

/-- If `f` subsumes `c` (i.e. `c ∈ f`), then `f.proof c`. -/
theorem proof_of_subsumes {f : Fmla} {c : Clause} (H : Fmla.subsumes f (Fmla.one c)) : f.proof c := fun _ h ↦
  h.1 _ <| H.1 _ <| List.Mem.head ..

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

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

Разделы

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

Аффилиация

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