Nuprl Lemma : oal_merge_preserves_lt

s:LOSet. ∀g:OCMon. ∀ps,qs,rs:|oal(s;g)|.  ((qs << rs)  ((ps ++ qs) << (ps ++ rs)))


Proof




Definitions occuring in Statement :  oal_lt: ps << qs oal_merge: ps ++ qs oalist: oal(a;b) all: x:A. B[x] implies:  Q ocmon: OCMon loset: LOSet set_car: |p|
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q oal_lt: ps << qs exists: x:A. B[x] and: P ∧ Q member: t ∈ T prop: uall: [x:A]. B[x] subtype_rel: A ⊆B dset: DSet squash: T ocmon: OCMon abmonoid: AbMon mon: Mon true: True uimplies: supposing a guard: {T} iff: ⇐⇒ Q rev_implies:  Q loset: LOSet poset: POSet{i} qoset: QOSet so_lambda: λ2x.t[x] 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 so_apply: x[s] infix_ap: y
Lemmas referenced :  oal_lt_wf set_car_wf oalist_wf ocmon_subtype_abdmonoid dset_wf ocmon_wf loset_wf equal_wf squash_wf true_wf grp_car_wf lookup_merge iff_weakening_equal set_lt_wf grp_lt_wf grp_sig_wf all_wf lookup_wf grp_id_wf oal_merge_wf grp_op_wf infix_ap_wf dset_of_mon_wf0 grp_op_preserves_lt
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalHypSubstitution productElimination thin cut introduction extract_by_obid dependent_functionElimination hypothesisEquality hypothesis isectElimination applyEquality sqequalRule lambdaEquality setElimination rename because_Cache dependent_pairFormation independent_pairFormation imageElimination equalityTransitivity equalitySymmetry universeEquality natural_numberEquality imageMemberEquality baseClosed independent_isectElimination independent_functionElimination productEquality functionEquality

Latex:
\mforall{}s:LOSet.  \mforall{}g:OCMon.  \mforall{}ps,qs,rs:|oal(s;g)|.    ((qs  <<  rs)  {}\mRightarrow{}  ((ps  ++  qs)  <<  (ps  ++  rs)))



Date html generated: 2017_10_01-AM-10_04_22
Last ObjectModification: 2017_03_03-PM-01_07_45

Theory : polynom_2


Home Index