Step
*
2
1
of Lemma
lattice-fset-meet-free-dlwc-inc
.....assertion.....
1. T : Type
2. eq : EqDecider(T)
3. Cs : T ⟶ fset(fset(T))
4. s : fset(T)
5. ↑fset-contains-none(eq;s;x.Cs[x])
6. deq-fset(deq-fset(eq)) ∈ EqDecider(Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])))
7. {s} ∈ Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))
8. ∀[s:fset(Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])))].
∀[x:Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))].
/\(s) ≤ x supposing x ∈ s
9. ∀[s:fset(Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])))].
∀[v:Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))].
((∀x:Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])). (x ∈ s
⇒ v ≤ x))
⇒ v ≤ /\(s))
10. {s} ≤ /\(λx.free-dlwc-inc(eq;a.Cs[a];x)"(s))
⊢ /\(λx.free-dlwc-inc(eq;a.Cs[a];x)"(s)) ≤ {s}
BY
{ (((Assert /\(λx.free-dlwc-inc(eq;a.Cs[a];x)"(s)) ∈ Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])) BY
Auto)
THEN (RWO "free-dlwc-point" (-1) THENA Auto)
)
THEN Auto
) }
1
1. T : Type
2. eq : EqDecider(T)
3. Cs : T ⟶ fset(fset(T))
4. s : fset(T)
5. ↑fset-contains-none(eq;s;x.Cs[x])
6. deq-fset(deq-fset(eq)) ∈ EqDecider(Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])))
7. {s} ∈ Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))
8. ∀[s:fset(Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])))].
∀[x:Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))].
/\(s) ≤ x supposing x ∈ s
9. ∀[s:fset(Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])))].
∀[v:Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))].
((∀x:Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])). (x ∈ s
⇒ v ≤ x))
⇒ v ≤ /\(s))
10. {s} ≤ /\(λx.free-dlwc-inc(eq;a.Cs[a];x)"(s))
11. /\(λx.free-dlwc-inc(eq;a.Cs[a];x)"(s))
∈ {ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.fset-contains-none(eq;a;x.Cs[x]))}
⊢ /\(λx.free-dlwc-inc(eq;a.Cs[a];x)"(s)) ≤ {s}
Latex:
Latex:
.....assertion.....
1. T : Type
2. eq : EqDecider(T)
3. Cs : T {}\mrightarrow{} fset(fset(T))
4. s : fset(T)
5. \muparrow{}fset-contains-none(eq;s;x.Cs[x])
6. deq-fset(deq-fset(eq)) \mmember{} EqDecider(Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])))
7. \{s\} \mmember{} Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))
8. \mforall{}[s:fset(Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])))].
\mforall{}[x:Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))].
/\mbackslash{}(s) \mleq{} x supposing x \mmember{} s
9. \mforall{}[s:fset(Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])))].
\mforall{}[v:Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))].
((\mforall{}x:Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])). (x \mmember{} s {}\mRightarrow{} v \mleq{} x)) {}\mRightarrow{} v \mleq{} /\mbackslash{}(s))
10. \{s\} \mleq{} /\mbackslash{}(\mlambda{}x.free-dlwc-inc(eq;a.Cs[a];x)"(s))
\mvdash{} /\mbackslash{}(\mlambda{}x.free-dlwc-inc(eq;a.Cs[a];x)"(s)) \mleq{} \{s\}
By
Latex:
(((Assert /\mbackslash{}(\mlambda{}x.free-dlwc-inc(eq;a.Cs[a];x)"(s))
\mmember{} Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])) BY
Auto)
THEN (RWO "free-dlwc-point" (-1) THENA Auto)
)
THEN Auto
)
Home
Index