---

Step * of Lemma exact-reduce-constraints_wf2

No Annotations
∀[n:ℕ]. ∀[w:{l:ℤ List| ||l|| = (n + 1) ∈ ℤ} ]. ∀[j:ℕ||w||]. ∀[L:{l:ℤ List| ||l|| = (n + 1) ∈ ℤ}  List].
  (exact-reduce-constraints(w;j;L) ∈ {l:ℤ List| ||l|| = ((n - 1) + 1) ∈ ℤ}  List)
BY
{ Auto }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[n:\mBbbN{}].  \mforall{}[w:\{l:\mBbbZ{}  List|  ||l||  =  (n  +  1)\}  ].  \mforall{}[j:\mBbbN{}||w||].  \mforall{}[L:\{l:\mBbbZ{}  List|  ||l||  =  (n  +  1)\}    List].
    (exact-reduce-constraints(w;j;L)  \mmember{}  \{l:\mBbbZ{}  List|  ||l||  =  ((n  -  1)  +  1)\}    List)


By

---

Latex:
Auto

---

Home Index