---

Step * of Lemma Pascal-completion-property

∀[r:CRng]. ∀[f,g:PowerSeries(r)]. ∀[x,y:Atom].
  ((Pascal-completion(r;f;g;x;y)(x:=0) = f ∈ PowerSeries(r))
  ∧ (Pascal-completion(r;f;g;x;y)(y:=0) = g ∈ PowerSeries(r))
  ∧ fps-Pascal(r;x;y;Pascal-completion(r;f;g;x;y)))
  ∧ (∀h:PowerSeries(r)
       (fps-Pascal(r;x;y;h)
       ⇒ (h(x:=0) = f ∈ PowerSeries(r))
       ⇒ (h(y:=0) = g ∈ PowerSeries(r))
       ⇒ (h = Pascal-completion(r;f;g;x;y) ∈ PowerSeries(r)))) 
  supposing (¬(1 = 0 ∈ |r|))
  ∧ (¬(x = y ∈ Atom))
  ∧ (f(x:=0) = f ∈ PowerSeries(r))
  ∧ (g(y:=0) = g ∈ PowerSeries(r))
  ∧ (f(y:=0) = g(x:=0) ∈ PowerSeries(r))
BY
{ Auto }

1
1. r : CRng
2. f : PowerSeries(r)
3. g : PowerSeries(r)
4. x : Atom
5. y : Atom
6. ¬(1 = 0 ∈ |r|)
7. ¬(x = y ∈ Atom)
8. f(x:=0) = f ∈ PowerSeries(r)
9. g(y:=0) = g ∈ PowerSeries(r)
10. f(y:=0) = g(x:=0) ∈ PowerSeries(r)
⊢ Pascal-completion(r;f;g;x;y)(x:=0) = f ∈ PowerSeries(r)

2
1. r : CRng
2. f : PowerSeries(r)
3. g : PowerSeries(r)
4. x : Atom
5. y : Atom
6. ¬(1 = 0 ∈ |r|)
7. ¬(x = y ∈ Atom)
8. f(x:=0) = f ∈ PowerSeries(r)
9. g(y:=0) = g ∈ PowerSeries(r)
10. f(y:=0) = g(x:=0) ∈ PowerSeries(r)
11. Pascal-completion(r;f;g;x;y)(x:=0) = f ∈ PowerSeries(r)
⊢ Pascal-completion(r;f;g;x;y)(y:=0) = g ∈ PowerSeries(r)

3
1. r : CRng
2. f : PowerSeries(r)
3. g : PowerSeries(r)
4. x : Atom
5. y : Atom
6. ¬(1 = 0 ∈ |r|)
7. ¬(x = y ∈ Atom)
8. f(x:=0) = f ∈ PowerSeries(r)
9. g(y:=0) = g ∈ PowerSeries(r)
10. f(y:=0) = g(x:=0) ∈ PowerSeries(r)
11. Pascal-completion(r;f;g;x;y)(x:=0) = f ∈ PowerSeries(r)
12. Pascal-completion(r;f;g;x;y)(y:=0) = g ∈ PowerSeries(r)
⊢ fps-Pascal(r;x;y;Pascal-completion(r;f;g;x;y))

4
1. r : CRng
2. f : PowerSeries(r)
3. g : PowerSeries(r)
4. x : Atom
5. y : Atom
6. ¬(1 = 0 ∈ |r|)
7. ¬(x = y ∈ Atom)
8. f(x:=0) = f ∈ PowerSeries(r)
9. g(y:=0) = g ∈ PowerSeries(r)
10. f(y:=0) = g(x:=0) ∈ PowerSeries(r)
11. Pascal-completion(r;f;g;x;y)(x:=0) = f ∈ PowerSeries(r)
12. Pascal-completion(r;f;g;x;y)(y:=0) = g ∈ PowerSeries(r)
13. fps-Pascal(r;x;y;Pascal-completion(r;f;g;x;y))
14. h : PowerSeries(r)
15. fps-Pascal(r;x;y;h)
16. h(x:=0) = f ∈ PowerSeries(r)
17. h(y:=0) = g ∈ PowerSeries(r)
⊢ h = Pascal-completion(r;f;g;x;y) ∈ PowerSeries(r)

---

Latex:

---

Latex:
\mforall{}[r:CRng].  \mforall{}[f,g:PowerSeries(r)].  \mforall{}[x,y:Atom].
    ((Pascal-completion(r;f;g;x;y)(x:=0)  =  f)
    \mwedge{}  (Pascal-completion(r;f;g;x;y)(y:=0)  =  g)
    \mwedge{}  fps-Pascal(r;x;y;Pascal-completion(r;f;g;x;y)))
    \mwedge{}  (\mforall{}h:PowerSeries(r)
              (fps-Pascal(r;x;y;h)
              {}\mRightarrow{}  (h(x:=0)  =  f)
              {}\mRightarrow{}  (h(y:=0)  =  g)
              {}\mRightarrow{}  (h  =  Pascal-completion(r;f;g;x;y)))) 
    supposing  (\mneg{}(1  =  0))  \mwedge{}  (\mneg{}(x  =  y))  \mwedge{}  (f(x:=0)  =  f)  \mwedge{}  (g(y:=0)  =  g)  \mwedge{}  (f(y:=0)  =  g(x:=0))


By

---

Latex:
Auto

---

Home Index