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 a b) and 
     Trans(T;a,b.R a b))


Proof



Definitions occuring in Statement :  sorted-by: sorted-by(R;L),  set-equal: set-equal(T;x;y),  no_repeats: no_repeats(T;l),  list: T List,  anti_sym: AntiSym(T;x,y.R[x; y]),  trans: Trans(T;x,y.E[x; y]),  uimplies: b supposing a,  uall: ∀[x:A]. B[x],  prop: ℙ,  apply: f a,  function: x:A ⟶ B[x],  universe: Type,  equal: s = t ∈ T
Definitions unfolded in proof :  uall: ∀[x:A]. B[x],  member: t ∈ T,  uimplies: b supposing a,  so_lambda: λ2x.t[x],  prop: ℙ,  subtype_rel: A ⊆r B,  so_apply: x[s],  all: ∀x:A. B[x],  implies: P ⇒ Q,  so_lambda: λ2x y.t[x; y],  so_apply: x[s1;s2],  top: Top,  iff: P ⇐⇒ Q,  and: P ∧ Q,  or: P ∨ Q,  assert: ↑b,  ifthenelse: if b then t else f 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: P ⇐ Q,  guard: {T},  anti_sym: AntiSym(T;x,y.R[x; y]),  cand: A 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
Latex:
\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