Nuprl Lemma : sorted-by-unique

[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  (∀[sa,sb:T List].
     (sa sb ∈ (T List)) supposing 
        (no_repeats(T;sa) and 
        sorted-by(R;sa) and 
        no_repeats(T;sb) and 
        sorted-by(R;sb) and 
        set-equal(T;sa;sb))) supposing 
     (AntiSym(T;a,b.R b) and 
     Trans(T;a,b.R b))


Definitions occuring in Statement :  sorted-by: sorted-by(R;L) set-equal: set-equal(T;x;y) no_repeats: no_repeats(T;l) list: List anti_sym: AntiSym(T;x,y.R[x; y]) trans: Trans(T;x,y.E[x; y]) uimplies: supposing a uall: [x:A]. B[x] prop: apply: a function: x:A ⟶ B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a so_lambda: λ2x.t[x] prop: subtype_rel: A ⊆B so_apply: x[s] all: x:A. B[x] implies:  Q so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] top: Top iff: ⇐⇒ Q and: P ∧ Q or: P ∨ Q assert: b ifthenelse: if then else fi  btrue: tt cons: [a b] bfalse: ff false: False not: ¬A uiff: uiff(P;Q) set-equal: set-equal(T;x;y) rev_implies:  Q guard: {T} anti_sym: AntiSym(T;x,y.R[x; y]) cand: c∧ B squash: T true: True
Lemmas referenced :  list_induction uall_wf list_wf isect_wf set-equal_wf sorted-by_wf subtype_rel_dep_function l_member_wf subtype_rel_self set_wf no_repeats_wf equal_wf anti_sym_wf trans_wf nil_wf sorted-by_wf_nil set-equal-nil list-cases null_nil_lemma product_subtype_list null_cons_lemma cons_wf set-equal-nil2 assert_elim null_wf bfalse_wf btrue_neq_bfalse no_repeats_cons sorted-by-cons cons_member l_all_iff or_wf squash_wf true_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut thin extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality sqequalRule lambdaEquality cumulativity hypothesis because_Cache applyEquality instantiate functionEquality universeEquality setEquality independent_isectElimination setElimination rename lambdaFormation independent_functionElimination dependent_functionElimination isect_memberEquality axiomEquality equalityTransitivity equalitySymmetry functionExtensionality voidElimination voidEquality productElimination unionElimination promote_hyp hypothesis_subsumption inlFormation independent_pairFormation inrFormation hyp_replacement Error :applyLambdaEquality,  imageElimination natural_numberEquality imageMemberEquality baseClosed

\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    (\mforall{}[sa,sb:T  List].
          (sa  =  sb)  supposing 
                (no\_repeats(T;sa)  and 
                sorted-by(R;sa)  and 
                no\_repeats(T;sb)  and 
                sorted-by(R;sb)  and 
                set-equal(T;sa;sb)))  supposing 
          (AntiSym(T;a,b.R  a  b)  and 
          Trans(T;a,b.R  a  b))

Date html generated: 2016_10_21-AM-10_11_26
Last ObjectModification: 2016_07_12-AM-05_30_13

Theory : list_1

Home Index