---

Step * 1 1 1 1 2 3 of Lemma free-iso-int_wf


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

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

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

---

Latex:

---

Latex:

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


By

---

Latex:
Auto

---

Home Index