---

Step * 1 of Lemma find-exact-eq-constraint_wf


1. u : ℤ
2. v : ℤ List
3. x : ∃i:ℕ||v|| [(|v[i]| = 1 ∈ ℤ)]
4. test-exact-eq-constraint(v) = (inl x) ∈ (∃i:ℕ||v|| [(|v[i]| = 1 ∈ ℤ)]?)
5. 0 < ||[u / v]||
⊢ x + 1 ∈ {i:ℕ+||v|| + 1| |[u / v][i]| = 1 ∈ ℤ} 
BY
{ TACTIC:(D -3 THEN Auto) }

---

Latex:

---

Latex:

1.  u  :  \mBbbZ{}
2.  v  :  \mBbbZ{}  List
3.  x  :  \mexists{}i:\mBbbN{}||v||  [(|v[i]|  =  1)]
4.  test-exact-eq-constraint(v)  =  (inl  x)
5.  0  <  ||[u  /  v]||
\mvdash{}  x  +  1  \mmember{}  \{i:\mBbbN{}\msupplus{}||v||  +  1|  |[u  /  v][i]|  =  1\} 


By

---

Latex:
TACTIC:(D  -3  THEN  Auto)

---

Home Index