Nuprl Lemma : lookup_oal_eq_id

a:LOSet. ∀b:AbDMon. ∀k:|a|. ∀ps:|oal(a;b)|.  ((¬↑(k ∈b dom(ps)))  ((ps[k]) e ∈ |b|))


Proof




Definitions occuring in Statement :  lookup: as[k] oal_dom: dom(ps) oalist: oal(a;b) mset_mem: mset_mem assert: b all: x:A. B[x] not: ¬A implies:  Q equal: t ∈ T abdmonoid: AbDMon grp_id: e grp_car: |g| loset: LOSet set_car: |p|
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q member: t ∈ T loset: LOSet poset: POSet{i} qoset: QOSet uall: [x:A]. B[x] abdmonoid: AbDMon dmon: DMon mon: Mon subtype_rel: A ⊆B oalist: oal(a;b) dset_set: dset_set mk_dset: mk_dset(T, eq) set_car: |p| pi1: fst(t) dset_list: List set_prod: s × t dset_of_mon: g↓set dset: DSet prop: oal_dom: dom(ps) mset_mem: mset_mem mk_mset: mk_mset(as)
Lemmas referenced :  lookup_fails grp_car_wf grp_id_wf set_car_wf oalist_wf dset_wf not_wf assert_wf mset_mem_wf oal_dom_wf abdmonoid_abmonoid abdmonoid_wf loset_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin setElimination rename hypothesisEquality isectElimination hypothesis applyEquality lambdaEquality sqequalRule independent_functionElimination because_Cache

Latex:
\mforall{}a:LOSet.  \mforall{}b:AbDMon.  \mforall{}k:|a|.  \mforall{}ps:|oal(a;b)|.    ((\mneg{}\muparrow{}(k  \mmember{}\msubb{}  dom(ps)))  {}\mRightarrow{}  ((ps[k])  =  e))



Date html generated: 2016_05_16-AM-08_16_53
Last ObjectModification: 2015_12_28-PM-06_27_32

Theory : polynom_2


Home Index