---

Step * 2 2 of Lemma rng-pp-nontrivial-1


1. r : IntegDom{i}@i'
2. eq : ∀x,y:|r|.  Dec(x = y ∈ |r|)@i
3. l : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} @i
4. [%2] : ¬((l 1) = 0 ∈ |r|)
5. ∀i,j:ℕ3.
     ((¬((l i) = 0 ∈ |r|))
     ⇒ (¬(i = j ∈ ℤ))
     ⇒ (λx.if (x =z j) then l i
            if (x =z i) then -r (l j)
            else 0
            fi  ∈ {p:ℕ3 ⟶ |r|| (¬(p = 0 ∈ (ℕ3 ⟶ |r|))) ∧ ((p . l) = 0 ∈ |r|)} ))
⊢ ∃a:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} . (∃b:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))}  [(((a . l) = 0 ∈ |r|) ∧ ((b . l)\000C = 0 ∈ |r|) ∧ (¬((a x b) = 0 ∈ (ℕ3 ⟶ |r|))))])
BY
{ ((InstHyp [⌜1⌝;⌜0⌝] (-1)⋅ THENA Auto)
   THEN (InstHyp [⌜1⌝;⌜2⌝] (-2)⋅ THENA Auto)
   THEN (InstConcl [λx.if (x =z 0) then l 1
                       if (x =z 1) then -r (l 0)
                       else 0
                       fi 
                   ; λx.if (x =z 2) then l 1
                        if (x =z 1) then -r (l 2)
                        else 0
                        fi ]⋅
         THENA Auto
         )
   THEN Auto
   THEN Try ((GenConclAtAddr [2;3] THEN Auto))) }

1
1. r : IntegDom{i}@i'
2. eq : ∀x,y:|r|.  Dec(x = y ∈ |r|)@i
3. l : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} @i
4. ¬((l 1) = 0 ∈ |r|)
5. ∀i,j:ℕ3.
     ((¬((l i) = 0 ∈ |r|))
     ⇒ (¬(i = j ∈ ℤ))
     ⇒ (λx.if (x =z j) then l i
            if (x =z i) then -r (l j)
            else 0
            fi  ∈ {p:ℕ3 ⟶ |r|| (¬(p = 0 ∈ (ℕ3 ⟶ |r|))) ∧ ((p . l) = 0 ∈ |r|)} ))
6. λx.if (x =z 0) then l 1
      if (x =z 1) then -r (l 0)
      else 0
      fi  ∈ {p:ℕ3 ⟶ |r|| (¬(p = 0 ∈ (ℕ3 ⟶ |r|))) ∧ ((p . l) = 0 ∈ |r|)} 
7. λx.if (x =z 2) then l 1
      if (x =z 1) then -r (l 2)
      else 0
      fi  ∈ {p:ℕ3 ⟶ |r|| (¬(p = 0 ∈ (ℕ3 ⟶ |r|))) ∧ ((p . l) = 0 ∈ |r|)} 
8. (λx.if (x =z 0) then l 1 if (x =z 1) then -r (l 0) else 0 fi  . l) = 0 ∈ |r|
9. (λx.if (x =z 2) then l 1 if (x =z 1) then -r (l 2) else 0 fi  . l) = 0 ∈ |r|
⊢ ¬((λx.if (x =z 0) then l 1
        if (x =z 1) then -r (l 0)
        else 0
        fi  x λx.if (x =z 2) then l 1
                 if (x =z 1) then -r (l 2)
                 else 0
                 fi )
= 0
∈ (ℕ3 ⟶ |r|))

---

Latex:

---

Latex:

1.  r  :  IntegDom\{i\}@i'
2.  eq  :  \mforall{}x,y:|r|.    Dec(x  =  y)@i
3.  l  :  \{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}  @i
4.  [\%2]  :  \mneg{}((l  1)  =  0)
5.  \mforall{}i,j:\mBbbN{}3.
          ((\mneg{}((l  i)  =  0))
          {}\mRightarrow{}  (\mneg{}(i  =  j))
          {}\mRightarrow{}  (\mlambda{}x.if  (x  =\msubz{}  j)  then  l  i
                        if  (x  =\msubz{}  i)  then  -r  (l  j)
                        else  0
                        fi    \mmember{}  \{p:\mBbbN{}3  {}\mrightarrow{}  |r||  (\mneg{}(p  =  0))  \mwedge{}  ((p  .  l)  =  0)\}  ))
\mvdash{}  \mexists{}a:\{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}  .  (\mexists{}b:\{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}    [(((a  .  l)  =  0)  \mwedge{}  ((b  .  l)  =  0)  \mwedge{}  (\mneg{}((a  \000Cx  b)  =  0)))])


By

---

Latex:
((InstHyp  [\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
  THEN  (InstConcl  [\mlambda{}x.if  (x  =\msubz{}  0)  then  l  1
                                          if  (x  =\msubz{}  1)  then  -r  (l  0)
                                          else  0
                                          fi 
                                  ;  \mlambda{}x.if  (x  =\msubz{}  2)  then  l  1
                                            if  (x  =\msubz{}  1)  then  -r  (l  2)
                                            else  0
                                            fi  ]\mcdot{}
              THENA  Auto
              )
  THEN  Auto
  THEN  Try  ((GenConclAtAddr  [2;3]  THEN  Auto)))

---

Home Index