Proof of Nuprl Lemma : KozenSilva-lemma

Step * 1 of Lemma KozenSilva-lemma

1. r : CRng
2. x : Atom
3. y : Atom
4. h : PowerSeries(r)
5. n : ℕ
6. m : ℕ
7. n ≤ m
8. ¬(x = y ∈ Atom)
⊢ [([h]_n(y:=1)*Δ(x,y))]_m = ([h]_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m - n)) ∈ PowerSeries(r)
BY
{ xxx(InstLemma `fps-linear-ucont-equal` [⌜Atom⌝;⌜AtomDeq⌝;⌜r⌝;⌜λ₂h.[([h]_n(y:=1)*Δ(x,y))]_m⌝;
      ⌜λ₂h.([h]_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m - n))⌝]⋅
      THENA Auto'
      )⋅xxx }

1
1. r : CRng
2. x : Atom
3. y : Atom
4. h : PowerSeries(r)
5. n : ℕ
6. m : ℕ
7. n ≤ m
8. ¬(x = y ∈ Atom)
⊢ fps-ucont(Atom;AtomDeq;r;f.[([f]_n(y:=1)*Δ(x,y))]_m)

2
1. r : CRng
2. x : Atom
3. y : Atom
4. h : PowerSeries(r)
5. n : ℕ
6. m : ℕ
7. n ≤ m
8. ¬(x = y ∈ Atom)
9. fps-ucont(Atom;AtomDeq;r;f.[([f]_n(y:=1)*Δ(x,y))]_m)
⊢ fps-ucont(Atom;AtomDeq;r;f.([f]_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m - n)))

3
1. r : CRng
2. x : Atom
3. y : Atom
4. h : PowerSeries(r)
5. n : ℕ
6. m : ℕ
7. n ≤ m
8. ¬(x = y ∈ Atom)
9. fps-ucont(Atom;AtomDeq;r;f.[([f]_n(y:=1)*Δ(x,y))]_m)
10. fps-ucont(Atom;AtomDeq;r;f.([f]_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m - n)))
11. f : PowerSeries(r)
12. g : PowerSeries(r)
⊢ [([(f+g)]_n(y:=1)*Δ(x,y))]_m = ([([f]_n(y:=1)*Δ(x,y))]_m+[([g]_n(y:=1)*Δ(x,y))]_m) ∈ PowerSeries(r)

4
1. r : CRng
2. x : Atom
3. y : Atom
4. h : PowerSeries(r)
5. n : ℕ
6. m : ℕ
7. n ≤ m
8. ¬(x = y ∈ Atom)
9. fps-ucont(Atom;AtomDeq;r;f.[([f]_n(y:=1)*Δ(x,y))]_m)
10. fps-ucont(Atom;AtomDeq;r;f.([f]_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m - n)))
11. ∀f,g:PowerSeries(r).

      ([([(f+g)]_n(y:=1)*Δ(x,y))]_m = ([([f]_n(y:=1)*Δ(x,y))]_m+[([g]_n(y:=1)*Δ(x,y))]_m) ∈ PowerSeries(r))

12. f : PowerSeries(r)
13. g : PowerSeries(r)
⊢ ([(f+g)]_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m - n))

= (([f]_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m - n))+([g]_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m - n)))

∈ PowerSeries(r)

5
1. r : CRng
2. x : Atom
3. y : Atom
4. h : PowerSeries(r)
5. n : ℕ
6. m : ℕ
7. n ≤ m
8. ¬(x = y ∈ Atom)
9. fps-ucont(Atom;AtomDeq;r;f.[([f]_n(y:=1)*Δ(x,y))]_m)
10. fps-ucont(Atom;AtomDeq;r;f.([f]_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m - n)))
11. ∀f,g:PowerSeries(r).

      ([([(f+g)]_n(y:=1)*Δ(x,y))]_m = ([([f]_n(y:=1)*Δ(x,y))]_m+[([g]_n(y:=1)*Δ(x,y))]_m) ∈ PowerSeries(r))

12. ∀f,g:PowerSeries(r).
(([(f+g)]_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m - n))

      = (([f]_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m - n))+([g]_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m

- n)))
∈ PowerSeries(r))
13. c : |r|
14. f : PowerSeries(r)
⊢ [([(c)*f]_n(y:=1)*Δ(x,y))]_m = (c)*[([f]_n(y:=1)*Δ(x,y))]_m ∈ PowerSeries(r)

6
1. r : CRng
2. x : Atom
3. y : Atom
4. h : PowerSeries(r)
5. n : ℕ
6. m : ℕ
7. n ≤ m
8. ¬(x = y ∈ Atom)
9. fps-ucont(Atom;AtomDeq;r;f.[([f]_n(y:=1)*Δ(x,y))]_m)
10. fps-ucont(Atom;AtomDeq;r;f.([f]_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m - n)))
11. ∀f,g:PowerSeries(r).

      ([([(f+g)]_n(y:=1)*Δ(x,y))]_m = ([([f]_n(y:=1)*Δ(x,y))]_m+[([g]_n(y:=1)*Δ(x,y))]_m) ∈ PowerSeries(r))

12. ∀f,g:PowerSeries(r).
(([(f+g)]_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m - n))

      = (([f]_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m - n))+([g]_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m

- n)))
∈ PowerSeries(r))

13. ∀c:|r|. ∀f:PowerSeries(r).  ([([(c)*f]_n(y:=1)*Δ(x,y))]_m = (c)*[([f]_n(y:=1)*Δ(x,y))]_m ∈ PowerSeries(r))

14. c : |r|
15. f : PowerSeries(r)
⊢ ([(c)*f]_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m - n))
= (c)*([f]_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m - n))
∈ PowerSeries(r)

7
1. r : CRng
2. x : Atom
3. y : Atom
4. h : PowerSeries(r)
5. n : ℕ
6. m : ℕ
7. n ≤ m
8. ¬(x = y ∈ Atom)
9. fps-ucont(Atom;AtomDeq;r;f.[([f]_n(y:=1)*Δ(x,y))]_m)
10. fps-ucont(Atom;AtomDeq;r;f.([f]_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m - n)))
11. ∀f,g:PowerSeries(r).

      ([([(f+g)]_n(y:=1)*Δ(x,y))]_m = ([([f]_n(y:=1)*Δ(x,y))]_m+[([g]_n(y:=1)*Δ(x,y))]_m) ∈ PowerSeries(r))

12. ∀f,g:PowerSeries(r).
(([(f+g)]_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m - n))

      = (([f]_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m - n))+([g]_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m

- n)))
∈ PowerSeries(r))

13. ∀c:|r|. ∀f:PowerSeries(r).  ([([(c)*f]_n(y:=1)*Δ(x,y))]_m = (c)*[([f]_n(y:=1)*Δ(x,y))]_m ∈ PowerSeries(r))

14. ∀c:|r|. ∀f:PowerSeries(r).
      (([(c)*f]_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m - n))
      = (c)*([f]_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m - n))
      ∈ PowerSeries(r))
15. b : bag(Atom)
⊢ [([<b>]_n(y:=1)*Δ(x,y))]_m = ([<b>]_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m - n)) ∈ PowerSeries(r)

8
1. r : CRng
2. x : Atom
3. y : Atom
4. h : PowerSeries(r)
5. n : ℕ
6. m : ℕ
7. n ≤ m
8. ¬(x = y ∈ Atom)
9. λ₂h.[([h]_n(y:=1)*Δ(x,y))]_m
= λ₂h.([h]_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m - n))
∈ (PowerSeries(r) ⟶ PowerSeries(r))
⊢ [([h]_n(y:=1)*Δ(x,y))]_m = ([h]_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(m - n)) ∈ PowerSeries(r)

Latex:

Latex:
1. r : CRng 2. x : Atom 3. y : Atom 4. h : PowerSeries(r) 5. n : \mBbbN{} 6. m : \mBbbN{} 7. n \mleq{} m 8. \mneg{}(x = y) \mvdash{} [([h]\_n(y:=1)*\mDelta{}(x,y))]\_m = ([h]\_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))\^{}(m - n)) By Latex: xxx(InstLemma `fps-linear-ucont-equal` [\mkleeneopen{}Atom\mkleeneclose{};\mkleeneopen{}AtomDeq\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}h.[([h]\_n(y:=1)*\mDelta{}(x,y))]\_m\mkleeneclose{}; \mkleeneopen{}\mlambda{}\msubtwo{}h.([h]\_n(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))\^{}(m - n))\mkleeneclose{}]\mcdot{} THENA Auto' )\mcdot{}xxx Home Index