---

Step * of Lemma free-dlwc-le

∀[T:Type]
  ∀eq:EqDecider(T). ∀cs:T ⟶ fset(fset(T)). ∀x,y:Point(free-dist-lattice-with-constraints(T;eq;x.cs[x])).
    (x ≤ y ⇐⇒ fset-ac-le(eq;x;y))
BY
{ ((Intros THEN Try ((RWO "free-dlwc-point" 0 THEN Auto)))
   THEN (RWO "free-dlwc-point" (-2) THENA Auto)
   THEN (RWO "free-dlwc-point" (-1) THENA Auto)
   THEN Unfold `lattice-le` 0
   THEN (RWW "free-dlwc-meet free-dlwc-point" 0 THENA Auto)
   THEN (InstLemma `fset-ac-order-constrained` [⌜T⌝;⌜eq⌝;⌜λ2s.fset-contains-none(eq;s;x.cs[x])⌝]⋅ THENA Auto)
   THEN (InstLemma `fset-constrained-ac-glb-is-glb` [⌜T⌝;⌜eq⌝;⌜λs.fset-contains-none(eq;s;x.cs[x])⌝;⌜x⌝;⌜y⌝]⋅
         THENA Auto
         )
   THEN All Reduce
   THEN Try ((FLemma `fset-contains-none-closed-downward` [-1;-2] THEN Auto))
   THEN Try ((All (RepUR ``so_apply``) THEN Trivial))
   THEN (D -1 THEN Auto)
   THEN BackThruSomeHyp'
   THEN (BackThruSomeHyp' THEN Auto)
   THEN All (RepUR ``so_apply``)
   THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}eq:EqDecider(T).  \mforall{}cs:T  {}\mrightarrow{}  fset(fset(T)).
    \mforall{}x,y:Point(free-dist-lattice-with-constraints(T;eq;x.cs[x])).
        (x  \mleq{}  y  \mLeftarrow{}{}\mRightarrow{}  fset-ac-le(eq;x;y))


By

---

Latex:
((Intros  THEN  Try  ((RWO  "free-dlwc-point"  0  THEN  Auto)))
  THEN  (RWO  "free-dlwc-point"  (-2)  THENA  Auto)
  THEN  (RWO  "free-dlwc-point"  (-1)  THENA  Auto)
  THEN  Unfold  `lattice-le`  0
  THEN  (RWW  "free-dlwc-meet  free-dlwc-point"  0  THENA  Auto)
  THEN  (InstLemma  `fset-ac-order-constrained`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}s.fset-contains-none(eq;s;x.cs[x])\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  (InstLemma  `fset-constrained-ac-glb-is-glb`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}\mlambda{}s.fset-contains-none(eq;s;x.cs[x])\mkleeneclose{};
              \mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  All  Reduce
  THEN  Try  ((FLemma  `fset-contains-none-closed-downward`  [-1;-2]  THEN  Auto))
  THEN  Try  ((All  (RepUR  ``so\_apply``)  THEN  Trivial))
  THEN  (D  -1  THEN  Auto)
  THEN  BackThruSomeHyp'
  THEN  (BackThruSomeHyp'  THEN  Auto)
  THEN  All  (RepUR  ``so\_apply``)
  THEN  Trivial)

---

Home Index