---

Step * 2 1 1 of Lemma index-min_wf


1. u : ℤ
2. v : ℤ List
3. 0 < ||v|| ⇒ (index-min(v) ∈ i:ℕ||v|| × {x:ℤ| (x = v[i] ∈ ℤ) ∧ (∀z:ℤ. ((z ∈ v) ⇒ (x ≤ z)))} )
⊢ if v = Ax then <0, u> otherwise let i,x = index-min(v) 
                   in if (u) < (x)  then <0, u>  else eval j = i + 1 in <j, x> ∈ i:ℕ||v|| + 1 × {x:ℤ| 
                                                                               (x = [u / v][i] ∈ ℤ)
                                                                               ∧ (∀z:ℤ. ((z ∈ [u / v]) ⇒ (x ≤ z)))} 
BY
{ (D 2 THEN Reduce 0) }

1
1. u : ℤ
2. 0 < ||[]|| ⇒ (index-min([]) ∈ i:ℕ||[]|| × {x:ℤ| (x = [][i] ∈ ℤ) ∧ (∀z@0:ℤ. ((z@0 ∈ []) ⇒ (x ≤ z@0)))} )
⊢ <0, u> ∈ i:ℕ1 × {x:ℤ| (x = [u][i] ∈ ℤ) ∧ (∀z@0:ℤ. ((z@0 ∈ [u]) ⇒ (x ≤ z@0)))} 

2
1. u : ℤ
2. u1 : ℤ
3. v : ℤ List
4. 0 < ||[u1 / v]||
⇒ (index-min([u1 / v]) ∈ i:ℕ||[u1 / v]|| × {x:ℤ| (x = [u1 / v][i] ∈ ℤ) ∧ (∀z:ℤ. ((z ∈ [u1 / v]) ⇒ (x ≤ z)))} )
⊢ let i,x = index-min([u1 / v]) 
  in if (u) < (x)  then <0, u>  else eval j = i + 1 in <j, x> ∈ i:ℕ(||v|| + 1) + 1 × {x:ℤ| 
                                                                    (x = [u; [u1 / v]][i] ∈ ℤ)
                                                                    ∧ (∀z:ℤ. ((z ∈ [u; [u1 / v]]) ⇒ (x ≤ z)))} 

---

Latex:

---

Latex:

1.  u  :  \mBbbZ{}
2.  v  :  \mBbbZ{}  List
3.  0  <  ||v||  {}\mRightarrow{}  (index-min(v)  \mmember{}  i:\mBbbN{}||v||  \mtimes{}  \{x:\mBbbZ{}|  (x  =  v[i])  \mwedge{}  (\mforall{}z:\mBbbZ{}.  ((z  \mmember{}  v)  {}\mRightarrow{}  (x  \mleq{}  z)))\}  )
\mvdash{}  if  v  =  Ax  then  ɘ,  u>  otherwise  let  i,x  =  index-min(v) 
                                      in  if  (u)  <  (x)    then  ɘ,  u>    else  eval  j  =  i  +  1  in  <j,  x>  \mmember{}  i:\mBbbN{}||v||  +  1  \mtimes{}  \{x:\mBbbZ{}\000C| 
                                                                                                                                                              (x  =  [u  /  v][i])
                                                                                                                                                              \mwedge{}  (\mforall{}z:\mBbbZ{}
                                                                                                                                                                        ((z  \mmember{}  [u  /  v])
                                                                                                                                                                        {}\mRightarrow{}  (x  \mleq{}  z)))\} 


By

---

Latex:
(D  2  THEN  Reduce  0)

---

Home Index