---

Step * of Lemma non-zero-component-exists

∀r:RngSig
  ((∀x,y:|r|.  Dec(x = y ∈ |r|)) ⇒ (∀k:ℕ. {∀a:ℕk ⟶ |r|. ((¬(a = 0 ∈ (ℕk ⟶ |r|))) ⇒ (∃i:ℕk. (¬((a i) = 0 ∈ |r|))))}))
BY
{ (Auto
   THEN RenameVar `eq' (-2)
   THEN (Unfold `guard` 0 THEN Auto)
   THEN D 0 With ⌜non-zero-component(r;eq;k;a)⌝ 
   THEN Try ((GenConclTerm ⌜non-zero-component(r;eq;k;a)⌝⋅ THEN Auto))) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  RenameVar  `eq'  (-2)
  THEN  (Unfold  `guard`  0  THEN  Auto)
  THEN  D  0  With  \mkleeneopen{}non-zero-component(r;eq;k;a)\mkleeneclose{} 
  THEN  Try  ((GenConclTerm  \mkleeneopen{}non-zero-component(r;eq;k;a)\mkleeneclose{}\mcdot{}  THEN  Auto)))

---

Home Index