---

Step * 1 2 of Lemma dM-hom-invariant

.....subterm..... T:t
2:n
1. I : fset(ℕ)
2. J : {J:fset(ℕ)| I ⊆ J} 
3. h : Hom(dM(J);dM(I))
4. ∀i:names(I). (((h <i>) = <i> ∈ Point(dM(I))) ∧ ((h <1-i>) = <1-i> ∈ Point(dM(I))))
5. x : Point(dM(I))
⊢ λs./\(λx.(h free-dl-inc(x))"(s))"(x) = λs./\(λx.free-dl-inc(x)"(s))"(x) ∈ fset(Point(dM(I)))
BY
{ ((RWO "dM-point" (-1) THENA Auto) THEN D -1) }

1
1. I : fset(ℕ)
2. J : {J:fset(ℕ)| I ⊆ J} 
3. h : Hom(dM(J);dM(I))
4. ∀i:names(I). (((h <i>) = <i> ∈ Point(dM(I))) ∧ ((h <1-i>) = <1-i> ∈ Point(dM(I))))
5. x : fset(fset(names(I) + names(I)))
6. ↑fset-antichain(union-deq(names(I);names(I);NamesDeq;NamesDeq);x)
⊢ λs./\(λx.(h free-dl-inc(x))"(s))"(x) = λs./\(λx.free-dl-inc(x)"(s))"(x) ∈ fset(Point(dM(I)))

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  I  :  fset(\mBbbN{})
2.  J  :  \{J:fset(\mBbbN{})|  I  \msubseteq{}  J\} 
3.  h  :  Hom(dM(J);dM(I))
4.  \mforall{}i:names(I).  (((h  <i>)  =  <i>)  \mwedge{}  ((h  ə-i>)  =  ə-i>))
5.  x  :  Point(dM(I))
\mvdash{}  \mlambda{}s./\mbackslash{}(\mlambda{}x.(h  free-dl-inc(x))"(s))"(x)  =  \mlambda{}s./\mbackslash{}(\mlambda{}x.free-dl-inc(x)"(s))"(x)


By

---

Latex:
((RWO  "dM-point"  (-1)  THENA  Auto)  THEN  D  -1)

---

Home Index