---

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


1. T : Type@i'
2. eq : EqDecider(T)@i
3. Cs : T ⟶ fset(fset(T))@i
4. x : Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))@i
5. y : Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))@i
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])))
BY
{ ((RWO "free-dlwc-1" (-1) THENA Auto)
   THEN (Assert ⌜{} ∈ x ∨ {} ∈ y⌝⋅ THENM (ParallelLast THEN BLemma `free-dlwc-1` THEN Auto))
   ) }

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

---

Latex:

---

Latex:

1.  T  :  Type@i'
2.  eq  :  EqDecider(T)@i
3.  Cs  :  T  {}\mrightarrow{}  fset(fset(T))@i
4.  x  :  Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))@i
5.  y  :  Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))@i
6.  x  \mvee{}  y  =  1
\mvdash{}  (x  =  1)  \mvee{}  (y  =  1)


By

---

Latex:
((RWO  "free-dlwc-1"  (-1)  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}\{\}  \mmember{}  x  \mvee{}  \{\}  \mmember{}  y\mkleeneclose{}\mcdot{}  THENM  (ParallelLast  THEN  BLemma  `free-dlwc-1`  THEN  Auto))
  )

---

Home Index