---

Step * of Lemma full-omega-unsat

∀[fmla:int_formula()]. ¬satisfiable_int_formula(fmla) supposing inr Ax  ≤ full-omega(fmla)
BY
{ (Auto THEN (D 0 THENA Auto) THEN (InstLemma `satisfiable-full-omega-tt` [⌜fmla⌝]⋅ THENA Auto)) }

1
1. fmla : int_formula()
2. inr Ax  ≤ full-omega(fmla)
3. satisfiable_int_formula(fmla)
4. ↑isl(full-omega(fmla))
⊢ False

---

Latex:

---

Latex:
\mforall{}[fmla:int\_formula()].  \mneg{}satisfiable\_int\_formula(fmla)  supposing  inr  Ax    \mleq{}  full-omega(fmla)


By

---

Latex:
(Auto  THEN  (D  0  THENA  Auto)  THEN  (InstLemma  `satisfiable-full-omega-tt`  [\mkleeneopen{}fmla\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index