---

Step * 3 1 of Lemma fps-pascal-elim

.....subterm..... T:t
3:n
1. r : CRng
2. x : Atom
3. y : Atom
4. x ≠ y ∈ Atom 
5. ¬(x = y ∈ Atom)
6. ¬(1 = 0 ∈ |r|)
7. ↑(AtomDeq x x)
⊢ (1-0) = 1 ∈ PowerSeries(r)
BY
{ xxx((InstLemma `neg_id_fps` [⌜Atom⌝;⌜r⌝]⋅ THENM Unfold `fps-sub` 0) THEN Auto)xxx }

---

Latex:

---

Latex:
.....subterm.....  T:t
3:n
1.  r  :  CRng
2.  x  :  Atom
3.  y  :  Atom
4.  x  \mneq{}  y  \mmember{}  Atom 
5.  \mneg{}(x  =  y)
6.  \mneg{}(1  =  0)
7.  \muparrow{}(AtomDeq  x  x)
\mvdash{}  (1-0)  =  1


By

---

Latex:
xxx((InstLemma  `neg\_id\_fps`  [\mkleeneopen{}Atom\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{}]\mcdot{}  THENM  Unfold  `fps-sub`  0)  THEN  Auto)xxx

---

Home Index