---

Step * 1 of Lemma full-omega_wf


1. fmla : int_formula()
2. v : polynomial-constraints() List
3. int_formula_dnf(fmla) = v ∈ (polynomial-constraints() List)
⊢ valueall-type(polynomial-constraints() List)
BY
{ TACTIC:Auto }

---

Latex:

---

Latex:

1.  fmla  :  int\_formula()
2.  v  :  polynomial-constraints()  List
3.  int\_formula\_dnf(fmla)  =  v
\mvdash{}  valueall-type(polynomial-constraints()  List)


By

---

Latex:
TACTIC:Auto

---

Home Index