---

Step * of Lemma shadow_inequalities_wf

∀[n:{2...}]. ∀[ineqs:{L:ℤ List| ||L|| = n ∈ ℤ}  List].  (shadow_inequalities(ineqs) ∈ {L:ℤ List| ||L|| = (n - 1) ∈ ℤ}  L\000Cist)
BY
{ TACTIC:(ProveWfLemma THEN D -1 THEN Reduce 0 THEN Auto) }

1
1. n : {2...}
2. u : {L:ℤ List| ||L|| = n ∈ ℤ} 
⊢ index-of-min(max_tl_coeffs([u])) + 1 ∈ ℕn

2
1. n : {2...}
2. u : {L:ℤ List| ||L|| = n ∈ ℤ} 
3. u1 : {L:ℤ List| ||L|| = n ∈ ℤ} 
4. v : {L:ℤ List| ||L|| = n ∈ ℤ}  List
⊢ index-of-min(max_tl_coeffs([u; [u1 / v]])) + 1 ∈ ℕn

---

Latex:

---

Latex:
\mforall{}[n:\{2...\}].  \mforall{}[ineqs:\{L:\mBbbZ{}  List|  ||L||  =  n\}    List].
    (shadow\_inequalities(ineqs)  \mmember{}  \{L:\mBbbZ{}  List|  ||L||  =  (n  -  1)\}    List)


By

---

Latex:
TACTIC:(ProveWfLemma  THEN  D  -1  THEN  Reduce  0  THEN  Auto)

---

Home Index