---

Step * 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. free-iso-int(s) ∈ free-vs(ℤ-rng;S) ≅ ℤ
⊢ ∃k:ℤ. (x = {<k, s>} ∈ Point(free-vs(ℤ-rng;S)))
BY
{ (RepUR ``vs-iso exists`` -1 THEN RepeatFor 3 (((MemHD (-1) THENA Auto) THEN All Reduce))) }

1
1. [S] : Type
2. ∀x,y:S.  (x = y ∈ S)
3. s : S
4. x : Point(free-vs(ℤ-rng;S))
5. (fst(free-iso-int(s))) = (fst(free-iso-int(s))) ∈ free-vs(ℤ-rng;S) ⟶ ℤ
6. (fst(snd(free-iso-int(s)))) = (fst(snd(free-iso-int(s)))) ∈ ℤ ⟶ free-vs(ℤ-rng;S)
7. (fst(snd(snd(free-iso-int(s)))))
= (fst(snd(snd(free-iso-int(s)))))
∈ (∀a:Point(free-vs(ℤ-rng;S)). (((fst(snd(free-iso-int(s)))) ((fst(free-iso-int(s))) a)) = a ∈ Point(free-vs(ℤ-rng;S))))
8. snd(snd(snd(free-iso-int(s)))) ∈ ∀b:Point(ℤ)
                                      (((fst(free-iso-int(s))) ((fst(snd(free-iso-int(s)))) b)) = b ∈ Point(ℤ))
⊢ ∃k:ℤ. (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.  free-iso-int(s)  \mmember{}  free-vs(\mBbbZ{}-rng;S)  \mcong{}  \mBbbZ{}
\mvdash{}  \mexists{}k:\mBbbZ{}.  (x  =  \{<k,  s>\})


By

---

Latex:
(RepUR  ``vs-iso  exists``  -1  THEN  RepeatFor  3  (((MemHD  (-1)  THENA  Auto)  THEN  All  Reduce)))

---

Home Index