---

Step * of Lemma lattice-fset-meet-free-dlwc-inc

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[Cs:T ⟶ fset(fset(T))]. ∀[s:fset(T)].
  /\(λx.free-dlwc-inc(eq;a.Cs[a];x)"(s)) = {s} ∈ Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])) 
  supposing ↑fset-contains-none(eq;s;x.Cs[x])
BY
{ (Auto
   THEN (Assert deq-fset(deq-fset(eq)) ∈ EqDecider(Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))) BY
               (RWO "free-dlwc-point" 0 THEN Auto))
   THEN (Assert {s} ∈ Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])) BY
               (RWO  "free-dlwc-point" 0
                THEN Auto
                THEN MemTypeCD
                THEN Auto
                THEN Using [`eq',⌜deq-fset(eq)⌝] (BLemma `fset-all-iff`)⋅
                THEN Auto
                THEN RWO "member-fset-singleton" (-1)
                THEN Auto
                THEN HypSubst' (-1) 0
                THEN Auto))
   THEN (InstLemma `lattice-fset-meet-is-glb` [⌜free-dist-lattice-with-constraints(T;eq;x.Cs[x])⌝;
         ⌜deq-fset(deq-fset(eq))⌝]⋅
         THENA Auto
         )
   THEN D -1
   THEN (InstHyp [⌜λx.free-dlwc-inc(eq;a.Cs[a];x)"(s)⌝;⌜{s}⌝] (-1)⋅
         THENA (Auto THEN (RWO "member-fset-image-iff" (-1)  THENA Auto))
         )) }

1
1. T : Type
2. eq : EqDecider(T)
3. Cs : T ⟶ fset(fset(T))
4. s : fset(T)
5. ↑fset-contains-none(eq;s;x.Cs[x])
6. deq-fset(deq-fset(eq)) ∈ EqDecider(Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])))
7. {s} ∈ Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))
8. ∀[s:fset(Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])))].
   ∀[x:Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))].
     /\(s) ≤ x supposing x ∈ s
9. ∀[s:fset(Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])))].
   ∀[v:Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))].
     ((∀x:Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])). (x ∈ s ⇒ v ≤ x)) ⇒ v ≤ /\(s))
10. x : Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))
11. ↓∃x1:T
      (x1 ∈ s ∧ (x = ((λx.free-dlwc-inc(eq;a.Cs[a];x)) x1) ∈ Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))))
⊢ {s} ≤ x

2
1. T : Type
2. eq : EqDecider(T)
3. Cs : T ⟶ fset(fset(T))
4. s : fset(T)
5. ↑fset-contains-none(eq;s;x.Cs[x])
6. deq-fset(deq-fset(eq)) ∈ EqDecider(Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])))
7. {s} ∈ Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))
8. ∀[s:fset(Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])))].
   ∀[x:Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))].
     /\(s) ≤ x supposing x ∈ s
9. ∀[s:fset(Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])))].
   ∀[v:Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))].
     ((∀x:Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])). (x ∈ s ⇒ v ≤ x)) ⇒ v ≤ /\(s))
10. {s} ≤ /\(λx.free-dlwc-inc(eq;a.Cs[a];x)"(s))
⊢ /\(λx.free-dlwc-inc(eq;a.Cs[a];x)"(s)) = {s} ∈ Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[Cs:T  {}\mrightarrow{}  fset(fset(T))].  \mforall{}[s:fset(T)].
    /\mbackslash{}(\mlambda{}x.free-dlwc-inc(eq;a.Cs[a];x)"(s))  =  \{s\}  supposing  \muparrow{}fset-contains-none(eq;s;x.Cs[x])


By

---

Latex:
(Auto
  THEN  (Assert  deq-fset(deq-fset(eq))
                            \mmember{}  EqDecider(Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])))  BY
                          (RWO  "free-dlwc-point"  0  THEN  Auto))
  THEN  (Assert  \{s\}  \mmember{}  Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))  BY
                          (RWO    "free-dlwc-point"  0
                            THEN  Auto
                            THEN  MemTypeCD
                            THEN  Auto
                            THEN  Using  [`eq',\mkleeneopen{}deq-fset(eq)\mkleeneclose{}]  (BLemma  `fset-all-iff`)\mcdot{}
                            THEN  Auto
                            THEN  RWO  "member-fset-singleton"  (-1)
                            THEN  Auto
                            THEN  HypSubst'  (-1)  0
                            THEN  Auto))
  THEN  (InstLemma  `lattice-fset-meet-is-glb`  [\mkleeneopen{}free-dist-lattice-with-constraints(T;eq;x.Cs[x])\mkleeneclose{};
              \mkleeneopen{}deq-fset(deq-fset(eq))\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  D  -1
  THEN  (InstHyp  [\mkleeneopen{}\mlambda{}x.free-dlwc-inc(eq;a.Cs[a];x)"(s)\mkleeneclose{};\mkleeneopen{}\{s\}\mkleeneclose{}]  (-1)\mcdot{}
              THENA  (Auto  THEN  (RWO  "member-fset-image-iff"  (-1)    THENA  Auto))
              ))

---

Home Index