---

Step * of Lemma free-dlwc-1-join-irreducible

∀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 = 1 ∈ Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))
  ⇐⇒ (x = 1 ∈ Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])))
      ∨ (y = 1 ∈ Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))))
BY
{ Auto }

1
1. T : Type
2. eq : EqDecider(T)
3. Cs : T ⟶ fset(fset(T))
4. x : Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))
5. y : Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))
6. x ∨ y = 1 ∈ Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))
⊢ (x = 1 ∈ Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])))
∨ (y = 1 ∈ Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])))

2
1. T : Type
2. eq : EqDecider(T)
3. Cs : T ⟶ fset(fset(T))
4. x : Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))
5. y : Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))
6. (x = 1 ∈ Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])))
∨ (y = 1 ∈ Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])))
⊢ x ∨ y = 1 ∈ 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{}x,y:Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])).
    (x  \mvee{}  y  =  1  \mLeftarrow{}{}\mRightarrow{}  (x  =  1)  \mvee{}  (y  =  1))


By

---

Latex:
Auto

---

Home Index