Nuprl Definition : dm-neg
¬(x) ==
lattice-extend(opposite-lattice(free-DeMorgan-lattice(T;eq));union-deq(T;T;eq;eq);
deq-fset(deq-fset(union-deq(T;T;eq;eq)));λz.case z of inl(a) => {{inr a }} | inr(a) => {{inl a}};x)
Definitions occuring in Statement :
free-DeMorgan-lattice: free-DeMorgan-lattice(T;eq),
opposite-lattice: opposite-lattice(L),
lattice-extend: lattice-extend(L;eq;eqL;f;ac),
deq-fset: deq-fset(eq),
fset-singleton: {x},
union-deq: union-deq(A;B;a;b),
lambda: λx.A[x],
decide: case b of inl(x) => s[x] | inr(y) => t[y],
inr: inr x ,
inl: inl x
Definitions occuring in definition :
lattice-extend: lattice-extend(L;eq;eqL;f;ac),
opposite-lattice: opposite-lattice(L),
free-DeMorgan-lattice: free-DeMorgan-lattice(T;eq),
deq-fset: deq-fset(eq),
union-deq: union-deq(A;B;a;b),
lambda: λx.A[x],
decide: case b of inl(x) => s[x] | inr(y) => t[y],
inr: inr x ,
fset-singleton: {x},
inl: inl x
FDL editor aliases :
dm-neg
Latex:
\mneg{}(x) ==
lattice-extend(opposite-lattice(free-DeMorgan-lattice(T;eq));union-deq(T;T;eq;eq);
deq-fset(deq-fset(union-deq(T;T;eq;eq)));\mlambda{}z.case z
of inl(a) =>
\{\{inr a \}\}
| inr(a) =>
\{\{inl a\}\};x)
Date html generated:
2020_05_20-AM-08_54_21
Last ObjectModification:
2015_10_09-PM-08_45_33
Theory : lattices
Home
Index