---

Step * 1 of Lemma dM-hom-invariant


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)) ∈ Point(dM(I))
BY
{ EqCD }

1
.....subterm..... T:t
1: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))
⊢ dM(I) = free-DeMorgan-lattice(names(I);NamesDeq) ∈ BoundedLattice

2
.....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)))

3
.....antecedent..... 
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))
⊢ ∀x,y:Point(dM(I)).  Dec(x = y ∈ Point(dM(I)))

---

Latex:

---

Latex:

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{}  \mbackslash{}/(\mlambda{}s./\mbackslash{}(\mlambda{}x.(h  free-dl-inc(x))"(s))"(x))  =  \mbackslash{}/(\mlambda{}s./\mbackslash{}(\mlambda{}x.free-dl-inc(x)"(s))"(x))


By

---

Latex:
EqCD

---

Home Index