---

Step * 1 of Lemma dM-homs-equal


1. I : fset(ℕ)
2. l : BoundedLattice
3. eq : EqDecider(Point(l))
4. h1 : Hom(dM(I);l)
5. h2 : Hom(dM(I);l)
6. ∀i:names(I). (((h1 <i>) = (h2 <i>) ∈ Point(l)) ∧ ((h1 <1-i>) = (h2 <1-i>) ∈ Point(l)))
7. x : Point(dM(I))
8. ∀[h:Hom(dM(I);l)]. ((h x) = \/(λs./\(λx.(h free-dl-inc(x))"(s))"(x)) ∈ Point(l))
⊢ (h1 x) = (h2 x) ∈ Point(l)
BY
{ ((Assert ⌜∀x,y:Point(l).  Dec(x = y ∈ Point(l))⌝⋅ THENA (BLemma `deq-implies` THEN Auto))
   THEN (RWO "-2" 0 THENA Auto)
   THEN EqCD
   THEN Auto
   THEN OnVar `x' (\h. ((RWO "dM-point" h THENA Auto) THEN D h))⋅
   THEN RepeatFor 5 ((EqCD THEN Auto))) }

1
.....subterm..... T:t
1:n
1. I : fset(ℕ)
2. l : BoundedLattice
3. eq : EqDecider(Point(l))
4. h1 : Hom(dM(I);l)
5. h2 : Hom(dM(I);l)
6. ∀i:names(I). (((h1 <i>) = (h2 <i>) ∈ Point(l)) ∧ ((h1 <1-i>) = (h2 <1-i>) ∈ Point(l)))
7. x : fset(fset(names(I) + names(I)))
8. ↑fset-antichain(union-deq(names(I);names(I);NamesDeq;NamesDeq);x)
9. ∀[h:Hom(dM(I);l)]. ((h x) = \/(λs./\(λx.(h free-dl-inc(x))"(s))"(x)) ∈ Point(l))
10. ∀x,y:Point(l).  Dec(x = y ∈ Point(l))
11. s : fset(names(I) + names(I))
12. x1 : names(I) + names(I)
⊢ (h1 free-dl-inc(x1)) = (h2 free-dl-inc(x1)) ∈ Point(l)

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  l  :  BoundedLattice
3.  eq  :  EqDecider(Point(l))
4.  h1  :  Hom(dM(I);l)
5.  h2  :  Hom(dM(I);l)
6.  \mforall{}i:names(I).  (((h1  <i>)  =  (h2  <i>))  \mwedge{}  ((h1  ə-i>)  =  (h2  ə-i>)))
7.  x  :  Point(dM(I))
8.  \mforall{}[h:Hom(dM(I);l)].  ((h  x)  =  \mbackslash{}/(\mlambda{}s./\mbackslash{}(\mlambda{}x.(h  free-dl-inc(x))"(s))"(x)))
\mvdash{}  (h1  x)  =  (h2  x)


By

---

Latex:
((Assert  \mkleeneopen{}\mforall{}x,y:Point(l).    Dec(x  =  y)\mkleeneclose{}\mcdot{}  THENA  (BLemma  `deq-implies`  THEN  Auto))
  THEN  (RWO  "-2"  0  THENA  Auto)
  THEN  EqCD
  THEN  Auto
  THEN  OnVar  `x'  (\mbackslash{}h.  ((RWO  "dM-point"  h  THENA  Auto)  THEN  D  h))\mcdot{}
  THEN  RepeatFor  5  ((EqCD  THEN  Auto)))

---

Home Index