Step
*
1
1
1
2
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
⊢ x = \/(λs.{s}"(x)) ∈ Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))
BY
{ Assert ⌜x ≤ \/(λs.{s}"(x))⌝⋅ }
1
.....assertion.....
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
⊢ x ≤ \/(λs.{s}"(x))
2
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. x ≤ \/(λs.{s}"(x))
⊢ x = \/(λs.{s}"(x)) ∈ Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))
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
\mvdash{} x = \mbackslash{}/(\mlambda{}s.\{s\}"(x))
By
Latex:
Assert \mkleeneopen{}x \mleq{} \mbackslash{}/(\mlambda{}s.\{s\}"(x))\mkleeneclose{}\mcdot{}
Home
Index