Step
*
1
1
1
2
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. x@0 : fset(T)
17. x@0 ∈ x
⊢ ¬↑fset-null({y ∈ \/(λs.{s}"(x)) | deq-f-subset(eq) y x@0})
BY
{ ((D 0 THENA Auto) THEN (RWO "assert-fset-null" (-1) THENA Auto)) }
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 ∈ 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. x@0 : fset(T)
17. x@0 ∈ x
18. {y ∈ \/(λs.{s}"(x)) | deq-f-subset(eq) y x@0} = {} ∈ fset(fset(T))
⊢ False
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. x@0 : fset(T)
17. x@0 \mmember{} x
\mvdash{} \mneg{}\muparrow{}fset-null(\{y \mmember{} \mbackslash{}/(\mlambda{}s.\{s\}"(x)) | deq-f-subset(eq) y x@0\})
By
Latex:
((D 0 THENA Auto) THEN (RWO "assert-fset-null" (-1) THENA Auto))
Home
Index