Nuprl Lemma : free-dma-lift-id
∀T:Type. ∀eq:EqDecider(T).
(free-dma-lift(T;eq;free-DeMorgan-algebra(T;eq);free-dml-deq(T;eq);λi.<i>)
= (λx.x)
∈ dma-hom(free-DeMorgan-algebra(T;eq);free-DeMorgan-algebra(T;eq)))
Proof
Definitions occuring in Statement :
free-dma-lift: free-dma-lift(T;eq;dm;eq2;f),
free-DeMorgan-algebra: free-DeMorgan-algebra(T;eq),
dma-hom: dma-hom(dma1;dma2),
dminc: <i>,
free-dml-deq: free-dml-deq(T;eq),
deq: EqDecider(T),
all: ∀x:A. B[x],
lambda: λx.A[x],
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
all: ∀x:A. B[x],
uall: ∀[x:A]. B[x],
member: t ∈ T,
deq: EqDecider(T),
lattice-point: Point(l),
record-select: r.x,
free-DeMorgan-algebra: free-DeMorgan-algebra(T;eq),
mk-DeMorgan-algebra: mk-DeMorgan-algebra(L;n),
record-update: r[x := v],
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
bfalse: ff,
free-DeMorgan-lattice: free-DeMorgan-lattice(T;eq),
free-dist-lattice: free-dist-lattice(T; eq),
mk-bounded-distributive-lattice: mk-bounded-distributive-lattice,
mk-bounded-lattice: mk-bounded-lattice(T;m;j;z;o),
btrue: tt,
bool: 𝔹,
iff: P ⇐⇒ Q,
and: P ∧ Q,
implies: P ⇒ Q,
assert: ↑b,
rev_implies: P ⇐ Q,
uimplies: b supposing a
Lemmas referenced :
free-dma-lift-unique,
free-DeMorgan-algebra_wf,
free-dml-deq_wf,
dminc_wf,
id-is-dma-hom,
deq_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
sqequalRule,
lambdaEquality,
cumulativity,
because_Cache,
independent_isectElimination,
universeEquality
Latex:
\mforall{}T:Type. \mforall{}eq:EqDecider(T).
(free-dma-lift(T;eq;free-DeMorgan-algebra(T;eq);free-dml-deq(T;eq);\mlambda{}i.<i>) = (\mlambda{}x.x))
Date html generated:
2020_05_20-AM-08_57_21
Last ObjectModification:
2018_05_20-PM-10_14_22
Theory : lattices
Home
Index