---

Step * of Lemma non-zero-component_wf

∀[r:RngSig]. ∀[eq:∀x,y:|r|.  Dec(x = y ∈ |r|)]. ∀[k:ℕ]. ∀[a:{a:ℕk ⟶ |r|| ¬(a = 0 ∈ (ℕk ⟶ |r|))} ].
  (non-zero-component(r;eq;k;a) ∈ {i:ℕk| ¬((a i) = 0 ∈ |r|)} )
BY
{ (Auto
   THEN Unfold `non-zero-component` 0
   THEN (Subst' λr,eq,k,a. eval j' = k in
                           case letrec G(x)=if (x) < (j')
                                               then if eq (a x) 0 then G (x + 1) else inl <x, λ_.Ax> fi 
                                               else (inr (λx.Ax) ) in
                                 G(0)
                            of inl(p) =>
                            let i,_ = p 
                            in i
                            | inr(_) =>
                            ⊥ ~ TERMOF{non-zero-vector-implies-ext:o, 1:l, i:l} 0
         THENA Computation
         )
   THEN Auto) }

1
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)

---

Latex:

---

Latex:
\mforall{}[r:RngSig].  \mforall{}[eq:\mforall{}x,y:|r|.    Dec(x  =  y)].  \mforall{}[k:\mBbbN{}].  \mforall{}[a:\{a:\mBbbN{}k  {}\mrightarrow{}  |r||  \mneg{}(a  =  0)\}  ].
    (non-zero-component(r;eq;k;a)  \mmember{}  \{i:\mBbbN{}k|  \mneg{}((a  i)  =  0)\}  )


By

---

Latex:
(Auto
  THEN  Unfold  `non-zero-component`  0
  THEN  (Subst'  \mlambda{}r,eq,k,a.  eval  j'  =  k  in
                                                  case  letrec  G(x)=if  (x)  <  (j')
                                                                                          then  if  eq  (a  x)  0  then  G  (x  +  1)  else  inl  <x,  \mlambda{}$\mbackslash{}f\000Cf5f{}$.Ax>  fi 
                                                                                          else  (inr  (\mlambda{}x.Ax)  )  in
                                                              G(0)
                                                    of  inl(p)  =>
                                                    let  i,$_{}$  =  p 
                                                    in  i
                                                    |  inr($_{}$)  =>
                                                    \mbot{}  \msim{}  TERMOF\{non-zero-vector-implies-ext:o,  1:l,  i:l\}  0
              THENA  Computation
              )
  THEN  Auto)

---

Home Index