---

Step * of Lemma find-exact-eq-constraint_wf

∀[L:ℤ List]. find-exact-eq-constraint(L) ∈ x:{x:ℤ List| x = L ∈ (ℤ List)}  × {i:ℕ+||L||| |L[i]| = 1 ∈ ℤ} ? supposing 0 <\000C ||L||
BY
{ TACTIC:(ProveWfLemma THEN MoveToConcl (-1) THEN GenConclTerm ⌜test-exact-eq-constraint(v)⌝⋅ THEN Auto) }

1
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 ∈ ℤ} 

---

Latex:

---

Latex:
\mforall{}[L:\mBbbZ{}  List].  find-exact-eq-constraint(L)  \mmember{}  x:\{x:\mBbbZ{}  List|  x  =  L\}    \mtimes{}  \{i:\mBbbN{}\msupplus{}||L|||  |L[i]|  =  1\}  ?  supposin\000Cg  0  <  ||L||


By

---

Latex:
TACTIC:(ProveWfLemma
                THEN  MoveToConcl  (-1)
                THEN  GenConclTerm  \mkleeneopen{}test-exact-eq-constraint(v)\mkleeneclose{}\mcdot{}
                THEN  Auto)

---

Home Index