---

Step * of Lemma rng-pp-nontriv1_wf

∀[r:IntegDom{i}]. ∀[eq:EqDecider(|r|)]. ∀[l:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} ].
  (rng-pp-nontriv1(r;eq;l) ∈ ∃a,b,c:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
                              ((¬¬((a . l) = 0 ∈ |r|))
                              ∧ (¬¬((b . l) = 0 ∈ |r|))
                              ∧ (¬¬((c . l) = 0 ∈ |r|))
                              ∧ (∃l:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
                                  ((¬¬((a . l) = 0 ∈ |r|)) ∧ (¬((b . l) = 0 ∈ |r|))))
                              ∧ (∃l:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
                                  ((¬¬((b . l) = 0 ∈ |r|)) ∧ (¬((c . l) = 0 ∈ |r|))))
                              ∧ (∃l:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
                                  ((¬¬((c . l) = 0 ∈ |r|)) ∧ (¬((a . l) = 0 ∈ |r|))))))
BY
{ (Auto THEN (Subst' rng-pp-nontriv1(r;eq;l) ~ TERMOF{rng-pp-nontrivial-3-ext:o, \\v:l, i:l} r eq l 0 THENM Auto)) }

1
.....equality..... 
1. r : IntegDom{i}
2. eq : EqDecider(|r|)
3. l : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
⊢ rng-pp-nontriv1(r;eq;l) ~ TERMOF{rng-pp-nontrivial-3-ext:o, \\v:l, i:l} r eq l

---

Latex:

---

Latex:
\mforall{}[r:IntegDom\{i\}].  \mforall{}[eq:EqDecider(|r|)].  \mforall{}[l:\{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}  ].
    (rng-pp-nontriv1(r;eq;l)  \mmember{}  \mexists{}a,b,c:\{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\} 
                                                            ((\mneg{}\mneg{}((a  .  l)  =  0))
                                                            \mwedge{}  (\mneg{}\mneg{}((b  .  l)  =  0))
                                                            \mwedge{}  (\mneg{}\mneg{}((c  .  l)  =  0))
                                                            \mwedge{}  (\mexists{}l:\{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}  .  ((\mneg{}\mneg{}((a  .  l)  =  0))  \mwedge{}  (\mneg{}((b  .  l)  =  0)))\000C)
                                                            \mwedge{}  (\mexists{}l:\{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}  .  ((\mneg{}\mneg{}((b  .  l)  =  0))  \mwedge{}  (\mneg{}((c  .  l)  =  0)))\000C)
                                                            \mwedge{}  (\mexists{}l:\{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\} 
                                                                    ((\mneg{}\mneg{}((c  .  l)  =  0))  \mwedge{}  (\mneg{}((a  .  l)  =  0))))))


By

---

Latex:
(Auto
  THEN  (Subst'  rng-pp-nontriv1(r;eq;l)  \msim{}  TERMOF\{rng-pp-nontrivial-3-ext:o,  \mbackslash{}\mbackslash{}v:l,  i:l\}  r  eq  l  0
            THENM  Auto
            )
  )

---

Home Index