---

Step * of Lemma free-dlwc-inc_wf

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[Cs:T ⟶ fset(fset(T))]. ∀[x:T].
  (free-dlwc-inc(eq;a.Cs[a];x) ∈ Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])))
BY
{ (((RWO "free-dlwc-point" 0 THEN Auto) THEN ProveWfLemma) THEN MemTypeCD THEN Auto) }

1
1. T : Type
2. eq : EqDecider(T)
3. Cs : T ⟶ fset(fset(T))
4. x : T
5. ↑fset-null({c ∈ Cs[x] | deq-f-subset(eq) c {x}})
6. ↑fset-antichain(eq;{{x}})
⊢ fset-all({{x}};a.fset-contains-none(eq;a;x.Cs[x]))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[Cs:T  {}\mrightarrow{}  fset(fset(T))].  \mforall{}[x:T].
    (free-dlwc-inc(eq;a.Cs[a];x)  \mmember{}  Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])))


By

---

Latex:
(((RWO  "free-dlwc-point"  0  THEN  Auto)  THEN  ProveWfLemma)  THEN  MemTypeCD  THEN  Auto)

---

Home Index