---

Step * of Lemma non-zero-vector-implies-ext

∀r:RngSig
  ((∀x,y:|r|.  Dec(x = y ∈ |r|)) ⇒ (∀k:ℕ. ∀a:{a:ℕk ⟶ |r|| ¬(a = 0 ∈ (ℕk ⟶ |r|))} .  (∃i:ℕk [(¬((a i) = 0 ∈ |r|))])))
BY
{ Extract of Obid: non-zero-vector-implies
  not unfolding  rng_zero
  finishing with Auto
  normalizes to:
  
  λr,%,k,a. eval j' = k in
            case letrec G(x)=if (x) < (j')  then if % (a x) 0 then G (x + 1) else inl <x, λ%.Ax> fi   else (inr (λx.Ax) \000C) in
                  G(0)
             of inl(%2) =>
             fst(%2)
             | inr(%2) =>
             fst(Ax) }

---

Latex:

---

Latex:
\mforall{}r:RngSig
    ((\mforall{}x,y:|r|.    Dec(x  =  y))  {}\mRightarrow{}  (\mforall{}k:\mBbbN{}.  \mforall{}a:\{a:\mBbbN{}k  {}\mrightarrow{}  |r||  \mneg{}(a  =  0)\}  .    (\mexists{}i:\mBbbN{}k  [(\mneg{}((a  i)  =  0))])))


By

---

Latex:
Extract  of  Obid:  non-zero-vector-implies
not  unfolding    rng\_zero
finishing  with  Auto
normalizes  to:

\mlambda{}r,\%,k,a.  eval  j'  =  k  in
                    case  letrec  G(x)=if  (x)  <  (j')
                                                            then  if  \%  (a  x)  0  then  G  (x  +  1)  else  inl  <x,  \mlambda{}\%.Ax>  fi 
                                                            else  (inr  (\mlambda{}x.Ax)  )  in
                                G(0)
                      of  inl(\%2)  =>
                      fst(\%2)
                      |  inr(\%2)  =>
                      fst(Ax)

---

Home Index