Nuprl Lemma : oalist_car_properties

a:LOSet. ∀b:AbDMon. ∀ws:|oal(a;b)|.  ((↑sd_ordered(map(λx.(fst(x));ws))) ∧ (¬↑(e ∈b map(λx.(snd(x));ws))))


Proof




Definitions occuring in Statement :  oalist: oal(a;b) sd_ordered: sd_ordered(as) mem: a ∈b as map: map(f;as) assert: b pi1: fst(t) pi2: snd(t) all: x:A. B[x] not: ¬A and: P ∧ Q lambda: λx.A[x] dset_of_mon: g↓set abdmonoid: AbDMon grp_id: e loset: LOSet set_car: |p|
Definitions unfolded in proof :  pi2: snd(t) mon: Mon dmon: DMon prop: false: False not: ¬A squash: T sq_stable: SqStable(P) implies:  Q dset_of_mon: g↓set dset_list: List set_prod: s × t dset: DSet subtype_rel: A ⊆B abdmonoid: AbDMon qoset: QOSet poset: POSet{i} loset: LOSet member: t ∈ T uall: [x:A]. B[x] pi1: fst(t) set_car: |p| mk_dset: mk_dset(T, eq) dset_set: dset_set oalist: oal(a;b) cand: c∧ B and: P ∧ Q all: x:A. B[x]
Lemmas referenced :  sq_stable_from_decidable assert_wf sd_ordered_wf map_wf set_car_wf set_prod_wf dset_of_mon_wf decidable__assert mem_wf grp_id_wf dset_of_mon_wf0 oalist_wf dset_wf abdmonoid_wf loset_wf
Rules used in proof :  voidElimination independent_pairFormation imageElimination baseClosed imageMemberEquality introduction independent_functionElimination lambdaEquality applyEquality because_Cache hypothesis hypothesisEquality dependent_functionElimination productElimination isectElimination lemma_by_obid rename thin setElimination sqequalRule sqequalHypSubstitution cut lambdaFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}a:LOSet.  \mforall{}b:AbDMon.  \mforall{}ws:|oal(a;b)|.
    ((\muparrow{}sd\_ordered(map(\mlambda{}x.(fst(x));ws)))  \mwedge{}  (\mneg{}\muparrow{}(e  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));ws))))



Date html generated: 2016_05_16-AM-08_15_31
Last ObjectModification: 2016_01_16-PM-11_58_31

Theory : polynom_2


Home Index