Nuprl Lemma : oal_lk_wf

s:LOSet. ∀g:AbDMon. ∀ps:|oal(s;g)|.  ((¬(ps 00 ∈ |oal(s;g)|))  (lk(ps) ∈ |s|))


Proof




Definitions occuring in Statement :  oal_lk: lk(ps) oal_nil: 00 oalist: oal(a;b) all: x:A. B[x] not: ¬A implies:  Q member: t ∈ T equal: t ∈ T abdmonoid: AbDMon loset: LOSet set_car: |p|
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q member: t ∈ T oal_lk: lk(ps) uall: [x:A]. B[x] uimplies: supposing a oalist: oal(a;b) dset_set: dset_set mk_dset: mk_dset(T, eq) set_car: |p| pi1: fst(t) dset_list: List loset: LOSet poset: POSet{i} qoset: QOSet abdmonoid: AbDMon subtype_rel: A ⊆B or: P ∨ Q set_prod: s × t dset_of_mon: g↓set top: Top assert: b ifthenelse: if then else fi  btrue: tt bfalse: ff false: False and: P ∧ Q not: ¬A nil: [] it: oal_nil: 00 cons: [a b] guard: {T} nat: ge: i ≥  decidable: Dec(P) iff: ⇐⇒ Q rev_implies:  Q prop: uiff: uiff(P;Q) sq_stable: SqStable(P) squash: T subtract: m le: A ≤ B less_than': less_than'(a;b) true: True dset: DSet so_lambda: λ2x.t[x] dmon: DMon mon: Mon so_apply: x[s]
Lemmas referenced :  hd_wf set_car_wf set_prod_wf dset_of_mon_wf list-cases length_of_nil_lemma map_nil_lemma sd_ordered_nil_lemma mem_nil_lemma oal_nil_wf product_subtype_list length_of_cons_lemma length_wf_nat nat_wf decidable__le false_wf not-ge-2 sq_stable__le condition-implies-le minus-add minus-one-mul add-swap minus-one-mul-top add-associates add-commutes add_functionality_wrt_le add-zero le-add-cancel2 equal_wf pi1_wf dset_of_mon_wf0 not_wf oalist_wf dset_wf abdmonoid_wf loset_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut sqequalRule introduction extract_by_obid sqequalHypSubstitution isectElimination thin because_Cache independent_isectElimination setElimination rename hypothesisEquality hypothesis applyEquality dependent_functionElimination unionElimination isect_memberEquality voidElimination voidEquality productElimination independent_functionElimination lambdaEquality promote_hyp hypothesis_subsumption natural_numberEquality addEquality independent_pairFormation imageMemberEquality baseClosed imageElimination minusEquality equalityTransitivity equalitySymmetry independent_pairEquality

Latex:
\mforall{}s:LOSet.  \mforall{}g:AbDMon.  \mforall{}ps:|oal(s;g)|.    ((\mneg{}(ps  =  00))  {}\mRightarrow{}  (lk(ps)  \mmember{}  |s|))



Date html generated: 2017_10_01-AM-10_03_27
Last ObjectModification: 2017_03_03-PM-01_06_43

Theory : polynom_2


Home Index