Nuprl Lemma : sd_ordered_char

āˆ€s:QOSet. āˆ€us:|s| List.  sd_ordered(us) HTFor{<š”¹,āˆ§b>v::vs āˆˆ us. āˆ€bw(:|s|) āˆˆ vs. (w <b v)


Proof




Definitions occuring in Statement :  sd_ordered: sd_ordered(as) ball: ball mon_htfor: HTFor{g} h::t āˆˆ as. f[h; t] list: List bool: š”¹ all: āˆ€x:A. B[x] equal: t āˆˆ T band_mon: <š”¹,āˆ§b> qoset: QOSet set_blt: a <b b set_car: |p|
Definitions unfolded in proof :  all: āˆ€x:A. B[x] uall: āˆ€[x:A]. B[x] member: t āˆˆ T qoset: QOSet dset: DSet so_lambda: Ī»2x.t[x] subtype_rel: A āŠ†B so_lambda: Ī»2y.t[x; y] so_apply: x[s] band_mon: <š”¹,āˆ§b> grp_car: |g| pi1: fst(t) so_apply: x[s1;s2] implies: ā‡’ Q top: Top grp_id: e pi2: snd(t) grp_op: * infix_ap: y prop: ā„™ squash: ā†“T bool: š”¹ unit: Unit it: ā‹… btrue: tt band: p āˆ§b q ifthenelse: if then else fi  bfalse: ff true: True uimplies: supposing a guard: {T} iff: ā‡ā‡’ Q and: P āˆ§ Q rev_implies: ā‡ Q ball: ball uiff: uiff(P;Q) or: P āˆØ Q assert: ā†‘b cons: [a b] cand: cāˆ§ B rev_uimplies: rev_uimplies(P;Q)
Lemmas referenced :  list_induction set_car_wf equal_wf bool_wf sd_ordered_wf mon_htfor_wf band_mon_wf ball_wf set_blt_wf list_wf sd_ordered_nil_lemma mon_htfor_nil_lemma btrue_wf sd_ordered_cons_lemma mon_htfor_cons_lemma qoset_wf squash_wf true_wf before_wf band_wf iff_weakening_equal iff_imp_equal_bool assert_wf assert_of_band iff_wf list-cases ball_nil_lemma nil_wf product_subtype_list ball_cons_lemma cons_wf before_cons_lemma iff_transitivity assert_of_set_lt set_lt_wf iff_weakening_uiff assert_functionality_wrt_uiff ball_char mem_wf set_lt_transitivity_2 set_leq_weakening_lt before_nil_lemma mem_cons_lemma bor_wf set_eq_wf or_wf assert_of_bor assert_of_dset_eq
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut thin introduction extract_by_obid sqequalHypSubstitution isectElimination setElimination rename because_Cache hypothesis sqequalRule lambdaEquality dependent_functionElimination hypothesisEquality applyEquality independent_functionElimination isect_memberEquality voidElimination voidEquality imageElimination equalityTransitivity equalitySymmetry universeEquality equalityUniverse levelHypothesis unionElimination equalityElimination natural_numberEquality imageMemberEquality baseClosed independent_isectElimination productElimination independent_pairFormation productEquality addLevel impliesFunctionality promote_hyp hypothesis_subsumption orFunctionality inlFormation

Latex:
\mforall{}s:QOSet.  \mforall{}us:|s|  List.    sd\_ordered(us)  =  HTFor\{<\mBbbB{},\mwedge{}\msubb{}>\}  v::vs  \mmember{}  us.  \mforall{}\msubb{}w(:|s|)  \mmember{}  vs.  (w  <\msubb{}  v)



Date html generated: 2017_10_01-AM-10_01_32
Last ObjectModification: 2017_03_03-PM-01_04_08

Theory : polynom_2


Home Index