---

Step * 1 1 1 1 of Lemma free-1-normal-form


1. [S] : Type
2. ∀x,y:S.  (x = y ∈ S)
3. s : S
4. x : Point(free-vs(ℤ-rng;S))
5. λx.Σ(p∈x). let k,s = p 
              in k ∈ free-vs(ℤ-rng;S) ⟶ ℤ
6. λk.{<k, s>} ∈ ℤ ⟶ free-vs(ℤ-rng;S)
7. λb.Ax ∈ ∀a:Point(free-vs(ℤ-rng;S)). ({<Σ(p∈a). let k,s = p in k, s>} = a ∈ Point(free-vs(ℤ-rng;S)))
8. λa.Ax ∈ ∀b:Point(ℤ). (Σ(p∈{<b, s>}). let k,s = p in k = b ∈ Point(ℤ))
⊢ ∃k:ℤ. (x = {<k, s>} ∈ Point(free-vs(ℤ-rng;S)))
BY
{ D 0 With ⌜(λx.Σ(p∈x). let k,s = p in k) x⌝  }

1
.....wf..... 
1. S : Type
2. ∀x,y:S.  (x = y ∈ S)
3. s : S
4. x : Point(free-vs(ℤ-rng;S))
5. λx.Σ(p∈x). let k,s = p 
              in k ∈ free-vs(ℤ-rng;S) ⟶ ℤ
6. λk.{<k, s>} ∈ ℤ ⟶ free-vs(ℤ-rng;S)
7. λb.Ax ∈ ∀a:Point(free-vs(ℤ-rng;S)). ({<Σ(p∈a). let k,s = p in k, s>} = a ∈ Point(free-vs(ℤ-rng;S)))
8. λa.Ax ∈ ∀b:Point(ℤ). (Σ(p∈{<b, s>}). let k,s = p in k = b ∈ Point(ℤ))
⊢ (λx.Σ(p∈x). let k,s = p in k) x ∈ ℤ

2
1. S : Type
2. ∀x,y:S.  (x = y ∈ S)
3. s : S
4. x : Point(free-vs(ℤ-rng;S))
5. λx.Σ(p∈x). let k,s = p 
              in k ∈ free-vs(ℤ-rng;S) ⟶ ℤ
6. λk.{<k, s>} ∈ ℤ ⟶ free-vs(ℤ-rng;S)
7. λb.Ax ∈ ∀a:Point(free-vs(ℤ-rng;S)). ({<Σ(p∈a). let k,s = p in k, s>} = a ∈ Point(free-vs(ℤ-rng;S)))
8. λa.Ax ∈ ∀b:Point(ℤ). (Σ(p∈{<b, s>}). let k,s = p in k = b ∈ Point(ℤ))
⊢ x = {<(λx.Σ(p∈x). let k,s = p in k) x, s>} ∈ Point(free-vs(ℤ-rng;S))

3
.....wf..... 
1. S : Type
2. ∀x,y:S.  (x = y ∈ S)
3. s : S
4. x : Point(free-vs(ℤ-rng;S))
5. λx.Σ(p∈x). let k,s = p 
              in k ∈ free-vs(ℤ-rng;S) ⟶ ℤ
6. λk.{<k, s>} ∈ ℤ ⟶ free-vs(ℤ-rng;S)
7. λb.Ax ∈ ∀a:Point(free-vs(ℤ-rng;S)). ({<Σ(p∈a). let k,s = p in k, s>} = a ∈ Point(free-vs(ℤ-rng;S)))
8. λa.Ax ∈ ∀b:Point(ℤ). (Σ(p∈{<b, s>}). let k,s = p in k = b ∈ Point(ℤ))
9. k : ℤ
⊢ istype(x = {<k, s>} ∈ Point(free-vs(ℤ-rng;S)))

---

Latex:

---

Latex:

1.  [S]  :  Type
2.  \mforall{}x,y:S.    (x  =  y)
3.  s  :  S
4.  x  :  Point(free-vs(\mBbbZ{}-rng;S))
5.  \mlambda{}x.\mSigma{}(p\mmember{}x).  let  k,s  =  p 
                            in  k  \mmember{}  free-vs(\mBbbZ{}-rng;S)  {}\mrightarrow{}  \mBbbZ{}
6.  \mlambda{}k.\{<k,  s>\}  \mmember{}  \mBbbZ{}  {}\mrightarrow{}  free-vs(\mBbbZ{}-rng;S)
7.  \mlambda{}b.Ax  \mmember{}  \mforall{}a:Point(free-vs(\mBbbZ{}-rng;S)).  (\{<\mSigma{}(p\mmember{}a).  let  k,s  =  p  in  k,  s>\}  =  a)
8.  \mlambda{}a.Ax  \mmember{}  \mforall{}b:Point(\mBbbZ{}).  (\mSigma{}(p\mmember{}\{<b,  s>\}).  let  k,s  =  p  in  k  =  b)
\mvdash{}  \mexists{}k:\mBbbZ{}.  (x  =  \{<k,  s>\})


By

---

Latex:
D  0  With  \mkleeneopen{}(\mlambda{}x.\mSigma{}(p\mmember{}x).  let  k,s  =  p  in  k)  x\mkleeneclose{} 

---

Home Index