Step
*
1
of Lemma
free-dist-lattice_wf
1. T : Type
2. eq : EqDecider(T)
3. Order({ac:fset(fset(T))| ↑fset-antichain(eq;ac)} ;x,y.fset-ac-le(eq;x;y))
4. ∀[a,b:{ac:fset(fset(T))| ↑fset-antichain(eq;ac)} ].
least-upper-bound({ac:fset(fset(T))| ↑fset-antichain(eq;ac)} ;x,y.fset-ac-le(eq;x;y);a;b;fset-ac-lub(eq;a;b))
5. ∀[a,b:{ac:fset(fset(T))| ↑fset-antichain(eq;ac)} ].
greatest-lower-bound({ac:fset(fset(T))| ↑fset-antichain(eq;ac)} ;x,y.fset-ac-le(eq;x;y);a;b;fset-ac-glb(eq;a;b))
6. ∀[a:{ac:fset(fset(T))| ↑fset-antichain(eq;ac)} ]. fset-ac-le(eq;a;{{}})
7. a : {ac:fset(fset(T))| ↑fset-antichain(eq;ac)}
⊢ fset-ac-le(eq;{};a)
BY
{ (RWO "empty-fset-ac-le" 0 THEN Auto) }
Latex:
Latex:
1. T : Type
2. eq : EqDecider(T)
3. Order(\{ac:fset(fset(T))| \muparrow{}fset-antichain(eq;ac)\} ;x,y.fset-ac-le(eq;x;y))
4. \mforall{}[a,b:\{ac:fset(fset(T))| \muparrow{}fset-antichain(eq;ac)\} ].
least-upper-bound(\{ac:fset(fset(T))| \muparrow{}fset-antichain(eq;ac)\} ;x,y.fset-ac-le(eq;x;y);
a;b;fset-ac-lub(eq;a;b))
5. \mforall{}[a,b:\{ac:fset(fset(T))| \muparrow{}fset-antichain(eq;ac)\} ].
greatest-lower-bound(\{ac:fset(fset(T))| \muparrow{}fset-antichain(eq;ac)\} ;x,y.fset-ac-le(eq;x;y);a;b;fse\000Ct-ac-glb(eq;a;b))
6. \mforall{}[a:\{ac:fset(fset(T))| \muparrow{}fset-antichain(eq;ac)\} ]. fset-ac-le(eq;a;\{\{\}\})
7. a : \{ac:fset(fset(T))| \muparrow{}fset-antichain(eq;ac)\}
\mvdash{} fset-ac-le(eq;\{\};a)
By
Latex:
(RWO "empty-fset-ac-le" 0 THEN Auto)
Home
Index