---

Step * 1 of Lemma non-zero-component_wf


1. r : RngSig
2. eq : ∀x,y:|r|.  Dec(x = y ∈ |r|)
3. k : ℕ
4. a : {a:ℕk ⟶ |r|| ¬(a = 0 ∈ (ℕk ⟶ |r|))} 
5. r@0 : Base
6. eq@0 : Base
7. k@0 : Base
8. a@0 : Base
9. j' : Base
10. p : Base
⊢ let i,_ = p 
  in i ~ fst(p)
BY
{ Computation }

---

Latex:

---

Latex:

1.  r  :  RngSig
2.  eq  :  \mforall{}x,y:|r|.    Dec(x  =  y)
3.  k  :  \mBbbN{}
4.  a  :  \{a:\mBbbN{}k  {}\mrightarrow{}  |r||  \mneg{}(a  =  0)\} 
5.  r@0  :  Base
6.  eq@0  :  Base
7.  k@0  :  Base
8.  a@0  :  Base
9.  j'  :  Base
10.  p  :  Base
\mvdash{}  let  i,$_{}$  =  p 
    in  i  \msim{}  fst(p)


By

---

Latex:
Computation

---

Home Index