---

Step * 1 1 of Lemma dM-homs-equal

.....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)
BY
{ (D -1
   THEN RenameVar `i' (-1)
   THEN ((Subst' free-dl-inc(inl i) ~ <i> 0 THENA (RW (SubC (SymbCompC [] 100)) 0 THEN Auto))
         THEN (Subst' free-dl-inc(inr i ) ~ <1-i> 0 THENA (RW (SubC (SymbCompC [] 100)) 0 THEN Auto))
         )
   THEN Auto) }

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
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  :  fset(fset(names(I)  +  names(I)))
8.  \muparrow{}fset-antichain(union-deq(names(I);names(I);NamesDeq;NamesDeq);x)
9.  \mforall{}[h:Hom(dM(I);l)].  ((h  x)  =  \mbackslash{}/(\mlambda{}s./\mbackslash{}(\mlambda{}x.(h  free-dl-inc(x))"(s))"(x)))
10.  \mforall{}x,y:Point(l).    Dec(x  =  y)
11.  s  :  fset(names(I)  +  names(I))
12.  x1  :  names(I)  +  names(I)
\mvdash{}  (h1  free-dl-inc(x1))  =  (h2  free-dl-inc(x1))


By

---

Latex:
(D  -1
  THEN  RenameVar  `i'  (-1)
  THEN  ((Subst'  free-dl-inc(inl  i)  \msim{}  <i>  0  THENA  (RW  (SubC  (SymbCompC  []  100))  0  THEN  Auto))
              THEN  (Subst'  free-dl-inc(inr  i  )  \msim{}  ə-i>  0  THENA  (RW  (SubC  (SymbCompC  []  100))  0  THEN  Auto))
              )
  THEN  Auto)

---

Home Index