---

Step * 1 of Lemma full-omega-unsat


1. fmla : int_formula()
2. inr Ax  ≤ full-omega(fmla)
3. satisfiable_int_formula(fmla)
4. ↑isl(full-omega(fmla))
⊢ False
BY
{ (MoveToConcl (-1) THEN MoveToConcl (-2) THEN (GenConclTerm ⌜full-omega(fmla)⌝⋅ THENA Auto) THEN D -2 THEN All Thin⋅) }

1
1. v : 𝔹
⊢ (inr Ax  ≤ v) ⇒ (↑isl(v)) ⇒ False

---

Latex:

---

Latex:

1.  fmla  :  int\_formula()
2.  inr  Ax    \mleq{}  full-omega(fmla)
3.  satisfiable\_int\_formula(fmla)
4.  \muparrow{}isl(full-omega(fmla))
\mvdash{}  False


By

---

Latex:
(MoveToConcl  (-1)
  THEN  MoveToConcl  (-2)
  THEN  (GenConclTerm  \mkleeneopen{}full-omega(fmla)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  -2
  THEN  All  Thin\mcdot{})

---

Home Index