---

Step * 1 1 of Lemma free-dl-basis

.....assertion..... 
1. T : Type
2. eq : EqDecider(T)
3. x : Point(free-dist-lattice(T; eq))
⊢ x = \/(λs.{s}"(x)) ∈ Point(free-dist-lattice(T; eq))
BY
{ ((Assert ∀s:fset(T). ({s} ∈ Point(free-dist-lattice(T; eq))) BY
          (RWO "free-dl-point" 0 THEN Auto))
   THEN (Assert x ∈ fset(fset(T)) BY
               (RWO "free-dl-point" 3 THEN Auto))
   THEN (Assert deq-fset(deq-fset(eq)) ∈ EqDecider(Point(free-dist-lattice(T; eq))) BY
               (RWO "free-dl-point" 0 THEN Auto))
   THEN (InstLemma `lattice-fset-join-is-lub` [⌜free-dist-lattice(T; eq)⌝;⌜deq-fset(deq-fset(eq))⌝]⋅ THENA Auto)
   THEN D -1
   THEN RepeatFor 2 (((InstHyp [⌜λs.{s}"(x)⌝] (-2)⋅ THENA Auto) THEN Thin (-3)))) }

1
1. T : Type
2. eq : EqDecider(T)
3. x : Point(free-dist-lattice(T; eq))
4. ∀s:fset(T). ({s} ∈ Point(free-dist-lattice(T; eq)))
5. x ∈ fset(fset(T))
6. deq-fset(deq-fset(eq)) ∈ EqDecider(Point(free-dist-lattice(T; eq)))
7. ∀[x@0:Point(free-dist-lattice(T; eq))]. x@0 ≤ \/(λs.{s}"(x)) supposing x@0 ∈ λs.{s}"(x)
8. ∀[u:Point(free-dist-lattice(T; eq))]
     ((∀x@0:Point(free-dist-lattice(T; eq)). (x@0 ∈ λs.{s}"(x) ⇒ x@0 ≤ u)) ⇒ \/(λs.{s}"(x)) ≤ u)
⊢ x = \/(λs.{s}"(x)) ∈ Point(free-dist-lattice(T; eq))

---

Latex:

---

Latex:
.....assertion..... 
1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  x  :  Point(free-dist-lattice(T;  eq))
\mvdash{}  x  =  \mbackslash{}/(\mlambda{}s.\{s\}"(x))


By

---

Latex:
((Assert  \mforall{}s:fset(T).  (\{s\}  \mmember{}  Point(free-dist-lattice(T;  eq)))  BY
                (RWO  "free-dl-point"  0  THEN  Auto))
  THEN  (Assert  x  \mmember{}  fset(fset(T))  BY
                          (RWO  "free-dl-point"  3  THEN  Auto))
  THEN  (Assert  deq-fset(deq-fset(eq))  \mmember{}  EqDecider(Point(free-dist-lattice(T;  eq)))  BY
                          (RWO  "free-dl-point"  0  THEN  Auto))
  THEN  (InstLemma  `lattice-fset-join-is-lub`  [\mkleeneopen{}free-dist-lattice(T;  eq)\mkleeneclose{};\mkleeneopen{}deq-fset(deq-fset(eq))\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  D  -1
  THEN  RepeatFor  2  (((InstHyp  [\mkleeneopen{}\mlambda{}s.\{s\}"(x)\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)  THEN  Thin  (-3))))

---

Home Index