---

Step * of Lemma NextNonZero_wf

∀[T:Type]. ∀[L:(T × ℤ) List].
  (NextNonZero(L) ∈ {L':(T × ℤ) List| 
                     ∃Z:(T × {z:ℤ| z = 0 ∈ ℤ} ) List
                      ((L = (Z @ L') ∈ ((T × ℤ) List)) ∧ (0 < ||L'|| ⇒ (¬((snd(hd(L'))) = 0 ∈ ℤ))))} )
BY
{ (InductionOnList THEN Unfold `NextNonZero` 0 THEN Reduce 0) }

1
1. T : Type
⊢ [] ∈ {L':(T × ℤ) List| 
        ∃Z:(T × {z:ℤ| z = 0 ∈ ℤ} ) List
         (([] = (Z @ L') ∈ ((T × ℤ) List)) ∧ (0 < ||L'|| ⇒ (¬((snd(hd(L'))) = 0 ∈ ℤ))))} 

2
1. T : Type
2. u : T × ℤ
3. v : (T × ℤ) List
4. NextNonZero(v) ∈ {L':(T × ℤ) List| 
                     ∃Z:(T × {z:ℤ| z = 0 ∈ ℤ} ) List
                      ((v = (Z @ L') ∈ ((T × ℤ) List)) ∧ (0 < ||L'|| ⇒ (¬((snd(hd(L'))) = 0 ∈ ℤ))))} 
⊢ if snd(u)=0 then NextNonZero(v) else [u / v] ∈ {L':(T × ℤ) List| 
                                                  ∃Z:(T × {z:ℤ| z = 0 ∈ ℤ} ) List
                                                   (([u / v] = (Z @ L') ∈ ((T × ℤ) List))
                                                   ∧ (0 < ||L'|| ⇒ (¬((snd(hd(L'))) = 0 ∈ ℤ))))} 

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:(T  \mtimes{}  \mBbbZ{})  List].
    (NextNonZero(L)  \mmember{}  \{L':(T  \mtimes{}  \mBbbZ{})  List| 
                                          \mexists{}Z:(T  \mtimes{}  \{z:\mBbbZ{}|  z  =  0\}  )  List
                                            ((L  =  (Z  @  L'))  \mwedge{}  (0  <  ||L'||  {}\mRightarrow{}  (\mneg{}((snd(hd(L')))  =  0))))\}  )


By

---

Latex:
(InductionOnList  THEN  Unfold  `NextNonZero`  0  THEN  Reduce  0)

---

Home Index