---

Step * 1 1 1 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, λk.{<k * 1, s>}, λb.Ax, λa.Ax> ∈ f:free-vs(ℤ-rng;S) ⟶ ℤ
   × g:ℤ ⟶ free-vs(ℤ-rng;S)
   × ((∀a:Point(free-vs(ℤ-rng;S)). ((g (f a)) = a ∈ Point(free-vs(ℤ-rng;S))))
     ∧ (∀b:Point(ℤ). ((f (g b)) = b ∈ Point(ℤ))))
⊢ <λx.Σ(p∈x). let k,s = p in k * 1, λk.{<k * 1, s>}, λb.Ax, λa.Ax>
= <λx.Σ(p∈x). let k,s = p in k, λk.{<k, s>}, λb.Ax, λa.Ax>
∈ (f:free-vs(ℤ-rng;S) ⟶ ℤ
  × g:ℤ ⟶ free-vs(ℤ-rng;S)
  × ((∀a:Point(free-vs(ℤ-rng;S)). ((g (f a)) = a ∈ Point(free-vs(ℤ-rng;S))))
    ∧ (∀b:Point(ℤ). ((f (g b)) = b ∈ Point(ℤ)))))
BY
{ RepeatFor 3 (((MemHD (-1) THENA Auto) THEN All Reduce THEN All (Fold `member`))) }

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(ℤ))
⊢ <λx.Σ(p∈x). let k,s = p in k * 1, λk.{<k * 1, s>}, λb.Ax, λa.Ax>
= <λx.Σ(p∈x). let k,s = p in k, λk.{<k, s>}, λb.Ax, λa.Ax>
∈ (f:free-vs(ℤ-rng;S) ⟶ ℤ
  × g:ℤ ⟶ free-vs(ℤ-rng;S)
  × ((∀a:Point(free-vs(ℤ-rng;S)). ((g (f a)) = a ∈ Point(free-vs(ℤ-rng;S))))
    ∧ (∀b:Point(ℤ). ((f (g b)) = b ∈ 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,  \mlambda{}k.\{<k  *  1,  s>\},  \mlambda{}b.Ax,  \mlambda{}a.Ax>  \mmember{}  f:free-vs(\mBbbZ{}-rng;S)  {}\mrightarrow{}  \mBbbZ{}
      \mtimes{}  g:\mBbbZ{}  {}\mrightarrow{}  free-vs(\mBbbZ{}-rng;S)
      \mtimes{}  ((\mforall{}a:Point(free-vs(\mBbbZ{}-rng;S)).  ((g  (f  a))  =  a))  \mwedge{}  (\mforall{}b:Point(\mBbbZ{}).  ((f  (g  b))  =  b)))
\mvdash{}  <\mlambda{}x.\mSigma{}(p\mmember{}x).  let  k,s  =  p  in  k  *  1,  \mlambda{}k.\{<k  *  1,  s>\},  \mlambda{}b.Ax,  \mlambda{}a.Ax>
=  <\mlambda{}x.\mSigma{}(p\mmember{}x).  let  k,s  =  p  in  k,  \mlambda{}k.\{<k,  s>\},  \mlambda{}b.Ax,  \mlambda{}a.Ax>


By

---

Latex:
RepeatFor  3  (((MemHD  (-1)  THENA  Auto)  THEN  All  Reduce  THEN  All  (Fold  `member`)))

---

Home Index