---

Step * 1 1 1 2 1 1 1 1 1 3 1 1 1 1 1 1 1 2 1 1 1 1 1 of Lemma free-dlwc-basis


1. T : Type
2. eq : EqDecider(T)
3. Cs : T ⟶ fset(fset(T))
4. x : fset(fset(T))
5. ↑fset-antichain(eq;x)
6. fset-all(x;a.fset-contains-none(eq;a;x.Cs[x]))
7. x ∈ Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))
8. deq-fset(deq-fset(eq)) ∈ EqDecider(Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])))
9. ∀s:fset(T). (s ∈ x ⇒ ({s} ∈ Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))))
10. λs.{s}"(x) ∈ fset(Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])))
11. ∀[x@0:Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))]. x@0 ≤ \/(λs.{s}"(x)) supposing x@0 ∈ λs.{s}"(x)
12. ∀[u:Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))]
      ((∀x@0:Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])). (x@0 ∈ λs.{s}"(x) ⇒ x@0 ≤ u))
      ⇒ \/(λs.{s}"(x)) ≤ u)
13. \/(λs.{s}"(x)) ≤ x
14. \/(λs.{s}"(x)) ∈ Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))
15. \/(λs.{s}"(x)) ∈ {ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.fset-contains-none(eq;a;x.Cs[x]))} 
16. ∀[P:fset(T) ⟶ 𝔹]. ∀[s:fset(fset(T))].  uiff({x ∈ s | P[x]} = {} ∈ fset(fset(T));¬(∃x:fset(T). (x ∈ s ∧ (↑P[x]))))
17. b : fset(T)
18. b ∈ \/(λs.{s}"(x))
19. ∀p:Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])). ∀b:fset(T).  (b ∈ p ∈ ℙ)
20. X : fset(Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])))@i
21. x1 : Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))@i
22. ∀a:fset(T). (a ∈ \/(X) ⇒ (↓∃p:Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])). (p ∈ X ∧ a ∈ p)))
23. ¬x1 ∈ X
24. a : fset(T)@i
25. v : Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))@i
26. \/({x1}) = v ∈ Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))
27. v1 : Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))@i
28. \/(X) = v1 ∈ Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))
29. a ∈ v ∨ v1
⊢ a ∈ v ∨ a ∈ v1
BY
{ (∀h:hyp. (RWO  "free-dlwc-point" h THENA Auto)  THEN DSetVars) }

1
1. T : Type
2. eq : EqDecider(T)
3. Cs : T ⟶ fset(fset(T))
4. x : fset(fset(T))
5. ↑fset-antichain(eq;x)
6. fset-all(x;a.fset-contains-none(eq;a;x.Cs[x]))
7. x ∈ {ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.fset-contains-none(eq;a;x.Cs[x]))} 
8. deq-fset(deq-fset(eq)) ∈ EqDecider({ac:fset(fset(T))| 
                                       (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.fset-contains-none(eq;a;x.Cs[x]))} )
9. ∀s:fset(T)
     (s ∈ x ⇒ ({s} ∈ {ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.fset-contains-none(eq;a;x.Cs[x]))} ))
10. λs.{s}"(x) ∈ fset({ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.fset-contains-none(eq;a;x.Cs[x]))} )
11. ∀[x@0:{ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.fset-contains-none(eq;a;x.Cs[x]))} ]
      x@0 ≤ \/(λs.{s}"(x)) supposing x@0 ∈ λs.{s}"(x)
12. ∀[u:{ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.fset-contains-none(eq;a;x.Cs[x]))} ]
      ((∀x@0:{ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.fset-contains-none(eq;a;x.Cs[x]))} 
          (x@0 ∈ λs.{s}"(x) ⇒ x@0 ≤ u))
      ⇒ \/(λs.{s}"(x)) ≤ u)
13. \/(λs.{s}"(x)) ≤ x
14. \/(λs.{s}"(x)) ∈ {ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.fset-contains-none(eq;a;x.Cs[x]))} 
15. \/(λs.{s}"(x)) ∈ {ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.fset-contains-none(eq;a;x.Cs[x]))} 
16. ∀[P:fset(T) ⟶ 𝔹]. ∀[s:fset(fset(T))].  uiff({x ∈ s | P[x]} = {} ∈ fset(fset(T));¬(∃x:fset(T). (x ∈ s ∧ (↑P[x]))))
17. b : fset(T)
18. b ∈ \/(λs.{s}"(x))
19. ∀p:{ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.fset-contains-none(eq;a;x.Cs[x]))} . ∀b:fset(T).
      (b ∈ p ∈ ℙ)
20. X : fset({ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.fset-contains-none(eq;a;x.Cs[x]))} )@i
21. x1 : fset(fset(T))@i
22. [%60] : (↑fset-antichain(eq;x1)) ∧ fset-all(x1;a.fset-contains-none(eq;a;x.Cs[x]))@i
23. ∀a:fset(T)
      (a ∈ \/(X)
      ⇒ (↓∃p:{ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.fset-contains-none(eq;a;x.Cs[x]))} 
            (p ∈ X ∧ a ∈ p)))
24. ¬x1 ∈ X
25. a : fset(T)@i
26. v : fset(fset(T))@i
27. [%58] : (↑fset-antichain(eq;v)) ∧ fset-all(v;a.fset-contains-none(eq;a;x.Cs[x]))@i
28. \/({x1}) = v ∈ {ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.fset-contains-none(eq;a;x.Cs[x]))} 
29. v1 : fset(fset(T))@i
30. [%56] : (↑fset-antichain(eq;v1)) ∧ fset-all(v1;a.fset-contains-none(eq;a;x.Cs[x]))@i
31. \/(X) = v1 ∈ {ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.fset-contains-none(eq;a;x.Cs[x]))} 
32. a ∈ v ∨ v1
⊢ a ∈ v ∨ a ∈ v1

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  Cs  :  T  {}\mrightarrow{}  fset(fset(T))
4.  x  :  fset(fset(T))
5.  \muparrow{}fset-antichain(eq;x)
6.  fset-all(x;a.fset-contains-none(eq;a;x.Cs[x]))
7.  x  \mmember{}  Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))
8.  deq-fset(deq-fset(eq))  \mmember{}  EqDecider(Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])))
9.  \mforall{}s:fset(T).  (s  \mmember{}  x  {}\mRightarrow{}  (\{s\}  \mmember{}  Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))))
10.  \mlambda{}s.\{s\}"(x)  \mmember{}  fset(Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])))
11.  \mforall{}[x@0:Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))]
            x@0  \mleq{}  \mbackslash{}/(\mlambda{}s.\{s\}"(x))  supposing  x@0  \mmember{}  \mlambda{}s.\{s\}"(x)
12.  \mforall{}[u:Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))]
            ((\mforall{}x@0:Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])).  (x@0  \mmember{}  \mlambda{}s.\{s\}"(x)  {}\mRightarrow{}  x@0  \mleq{}  u))
            {}\mRightarrow{}  \mbackslash{}/(\mlambda{}s.\{s\}"(x))  \mleq{}  u)
13.  \mbackslash{}/(\mlambda{}s.\{s\}"(x))  \mleq{}  x
14.  \mbackslash{}/(\mlambda{}s.\{s\}"(x))  \mmember{}  Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))
15.  \mbackslash{}/(\mlambda{}s.\{s\}"(x))  \mmember{}  \{ac:fset(fset(T))| 
                                            (\muparrow{}fset-antichain(eq;ac))  \mwedge{}  fset-all(ac;a.fset-contains-none(eq;a;x.Cs[x]))\} 
16.  \mforall{}[P:fset(T)  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[s:fset(fset(T))].
            uiff(\{x  \mmember{}  s  |  P[x]\}  =  \{\};\mneg{}(\mexists{}x:fset(T).  (x  \mmember{}  s  \mwedge{}  (\muparrow{}P[x]))))
17.  b  :  fset(T)
18.  b  \mmember{}  \mbackslash{}/(\mlambda{}s.\{s\}"(x))
19.  \mforall{}p:Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])).  \mforall{}b:fset(T).    (b  \mmember{}  p  \mmember{}  \mBbbP{})
20.  X  :  fset(Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])))@i
21.  x1  :  Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))@i
22.  \mforall{}a:fset(T)
            (a  \mmember{}  \mbackslash{}/(X)  {}\mRightarrow{}  (\mdownarrow{}\mexists{}p:Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])).  (p  \mmember{}  X  \mwedge{}  a  \mmember{}  p)))
23.  \mneg{}x1  \mmember{}  X
24.  a  :  fset(T)@i
25.  v  :  Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))@i
26.  \mbackslash{}/(\{x1\})  =  v
27.  v1  :  Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))@i
28.  \mbackslash{}/(X)  =  v1
29.  a  \mmember{}  v  \mvee{}  v1
\mvdash{}  a  \mmember{}  v  \mvee{}  a  \mmember{}  v1


By

---

Latex:
(\mforall{}h:hyp.  (RWO    "free-dlwc-point"  h  THENA  Auto)    THEN  DSetVars)

---

Home Index