Nuprl Lemma : free-dl_wf
∀[X:Type]. (free-dl(X) ∈ BoundedDistributiveLattice)
Proof
Definitions occuring in Statement :
free-dl: free-dl(X),
bdd-distributive-lattice: BoundedDistributiveLattice,
uall: ∀[x:A]. B[x],
member: t ∈ T,
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
free-dl: free-dl(X),
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
uimplies: b supposing a,
and: P ∧ Q,
cand: A c∧ B,
subtype_rel: A ⊆r B,
free-dl-type: free-dl-type(X),
all: ∀x:A. B[x],
prop: ℙ,
implies: P ⇒ Q,
quotient: x,y:A//B[x; y],
squash: ↓T,
true: True,
guard: {T},
equiv_rel: EquivRel(T;x,y.E[x; y]),
refl: Refl(T;x,y.E[x; y]),
dlattice-eq: dlattice-eq(X;as;bs),
exists: ∃x:A. B[x],
so_lambda: λ2x.t[x],
so_apply: x[s],
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
l_subset: l_subset(T;as;bs),
or: P ∨ Q,
free-dl-join: free-dl-join(as;bs),
top: Top,
trans: Trans(T;x,y.E[x; y]),
free-dl-meet: free-dl-meet(as;bs),
append: as @ bs,
so_lambda: so_lambda(x,y,z.t[x; y; z]),
so_apply: x[s1;s2;s3]
Lemmas referenced :
dlattice-eq-equiv,
mk-bounded-distributive-lattice_wf,
free-dl-type_wf,
free-dl-meet_wf,
free-dl-join_wf,
nil_wf,
list_wf,
subtype_quotient,
dlattice-eq_wf,
cons_wf,
quotient-member-eq,
free-dl-meet_wf_list,
equal-wf-base,
equal_wf,
squash_wf,
true_wf,
exists_wf,
l_member_wf,
append_wf,
all_wf,
l_subset_wf,
member-free-dl-meet,
dlattice-order-iff,
dlattice-order_wf,
length_wf_nat,
nat_wf,
l_subset_append,
member_append,
equiv_rel_functionality_wrt_iff,
append_assoc,
l_subset_append2,
l_subset_refl,
iff_weakening_equal,
list_accum_cons_lemma,
list_ind_nil_lemma,
list_accum_nil_lemma,
list_induction,
map_wf,
map_nil_lemma,
map_cons_lemma,
append-nil,
subtype_rel_list,
top_wf,
or_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
sqequalRule,
cumulativity,
hypothesis,
lambdaEquality,
because_Cache,
independent_isectElimination,
isect_memberEquality,
axiomEquality,
independent_pairFormation,
universeEquality,
applyEquality,
promote_hyp,
lambdaFormation,
equalityTransitivity,
equalitySymmetry,
dependent_functionElimination,
independent_functionElimination,
pointwiseFunctionality,
pertypeElimination,
productElimination,
productEquality,
imageElimination,
natural_numberEquality,
imageMemberEquality,
baseClosed,
functionEquality,
addLevel,
impliesFunctionality,
allFunctionality,
existsFunctionality,
andLevelFunctionality,
dependent_pairFormation,
dependent_set_memberEquality,
hyp_replacement,
applyLambdaEquality,
setElimination,
rename,
inrFormation,
inlFormation,
unionElimination,
levelHypothesis,
existsLevelFunctionality,
voidElimination,
voidEquality,
equalityUniverse,
orFunctionality,
orLevelFunctionality
Latex:
\mforall{}[X:Type]. (free-dl(X) \mmember{} BoundedDistributiveLattice)
Date html generated:
2017_10_05-AM-00_32_26
Last ObjectModification:
2017_07_28-AM-09_13_28
Theory : lattices
Home
Index