---

Step * of Lemma lattice-extend-wc-join

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[Cs:T ⟶ fset(fset(T))]. ∀[L:BoundedDistributiveLattice]. ∀[eqL:EqDecider(Point(L))].
∀[f:T ⟶ Point(L)]. ∀[a,b:Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))].
  lattice-extend-wc(L;eq;eqL;f;a ∨ b) ≤ lattice-extend-wc(L;eq;eqL;f;a) ∨ lattice-extend-wc(L;eq;eqL;f;b)
BY
{ (Auto
   THEN (InstLemma `lattice-extend-join` [⌜T⌝;⌜eq⌝;⌜L⌝;⌜eqL⌝;⌜f⌝;⌜a⌝;⌜b⌝]⋅ THENA Auto)
   THEN Unfold `lattice-extend-wc` 0
   THEN NthHypSq (-1)
   THEN RepeatFor 2 ((EqCD THEN Try (Trivial)))) }

1
1. T : Type
2. eq : EqDecider(T)
3. Cs : T ⟶ fset(fset(T))
4. L : BoundedDistributiveLattice
5. eqL : EqDecider(Point(L))
6. f : T ⟶ Point(L)
7. a : Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))
8. b : Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))
9. lattice-extend(L;eq;eqL;f;a ∨ b) ≤ lattice-extend(L;eq;eqL;f;a) ∨ lattice-extend(L;eq;eqL;f;b)
⊢ a ∨ b ~ a ∨ b

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[Cs:T  {}\mrightarrow{}  fset(fset(T))].  \mforall{}[L:BoundedDistributiveLattice].
\mforall{}[eqL:EqDecider(Point(L))].  \mforall{}[f:T  {}\mrightarrow{}  Point(L)].
\mforall{}[a,b:Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))].
    lattice-extend-wc(L;eq;eqL;f;a  \mvee{}  b) 
    \mleq{}  lattice-extend-wc(L;eq;eqL;f;a)  \mvee{}  lattice-extend-wc(L;eq;eqL;f;b)


By

---

Latex:
(Auto
  THEN  (InstLemma  `lattice-extend-join`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}eqL\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Unfold  `lattice-extend-wc`  0
  THEN  NthHypSq  (-1)
  THEN  RepeatFor  2  ((EqCD  THEN  Try  (Trivial))))

---

Home Index