Nuprl Lemma : face-lattice1-is-inc
∀T:Type. ∀eq:EqDecider(T). ∀x:T. ((x=1) ~ free-dlwc-inc(union-deq(T;T;eq;eq);a.face-lattice-constraints(a);inr x ))
Proof
Definitions occuring in Statement :
face-lattice1: (x=1),
face-lattice-constraints: face-lattice-constraints(x),
free-dlwc-inc: free-dlwc-inc(eq;a.Cs[a];x),
union-deq: union-deq(A;B;a;b),
deq: EqDecider(T),
all: ∀x:A. B[x],
inr: inr x ,
universe: Type,
sqequal: s ~ t
Definitions unfolded in proof :
all: ∀x:A. B[x],
face-lattice-constraints: face-lattice-constraints(x),
free-dlwc-inc: free-dlwc-inc(eq;a.Cs[a];x),
face-lattice1: (x=1),
fset-singleton: {x},
fset-filter: {x ∈ s | P[x]},
fset-null: fset-null(s),
member: t ∈ T,
top: Top,
uall: ∀[x:A]. B[x],
uimplies: b supposing a,
deq-f-subset: deq-f-subset(eq),
isl: isl(x),
decidable__f-subset,
decidable__all_fset,
decidable_functionality,
iff_preserves_decidability,
iff_weakening_uiff,
fset-all-iff,
decidable__assert,
null: null(as),
filter: filter(P;l),
reduce: reduce(f;k;as),
list_ind: list_ind,
fset-pair: {a,b},
cons: [a / b],
ifthenelse: if b then t else f fi ,
bnot: ¬bb,
decidable__fset-member,
assert-deq-fset-member,
deq-fset-member: a ∈b s,
deq-member: x ∈b L,
bor: p ∨bq,
union-deq: union-deq(A;B;a;b),
sumdeq: sumdeq(a;b),
bfalse: ff,
nil: [],
it: ⋅,
btrue: tt,
sq_type: SQType(T),
implies: P ⇒ Q,
guard: {T}
Lemmas referenced :
filter_cons_lemma,
istype-void,
filter_nil_lemma,
subtype_base_sq,
bool_wf,
bool_subtype_base,
bfalse_wf,
null_nil_lemma,
deq_wf,
istype-universe,
decidable__f-subset,
decidable__all_fset,
decidable_functionality,
iff_preserves_decidability,
iff_weakening_uiff,
fset-all-iff,
decidable__assert,
decidable__fset-member,
assert-deq-fset-member
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
cut,
sqequalRule,
introduction,
extract_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
isect_memberEquality_alt,
voidElimination,
hypothesis,
instantiate,
isectElimination,
cumulativity,
independent_isectElimination,
equalityTransitivity,
equalitySymmetry,
independent_functionElimination,
universeIsType,
hypothesisEquality,
universeEquality
Latex:
\mforall{}T:Type. \mforall{}eq:EqDecider(T). \mforall{}x:T.
((x=1) \msim{} free-dlwc-inc(union-deq(T;T;eq;eq);a.face-lattice-constraints(a);inr x ))
Date html generated:
2019_10_31-AM-07_21_52
Last ObjectModification:
2018_11_08-PM-06_00_38
Theory : lattices
Home
Index