Nuprl Lemma : sorted-by-strict-unique

[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  (∀[sa,sb:T List].
     (sa sb ∈ (T List)) supposing (sorted-by(R;sa) and sorted-by(R;sb) and set-equal(T;sa;sb))) supposing 
     ((∀a:T. (R a))) and 
     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) 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: all: x:A. B[x] not: ¬A 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 prop: subtype_rel: A ⊆B so_lambda: λ2x.t[x] so_apply: x[s] all: x:A. B[x] so_lambda: λ2y.t[x; y] so_apply: x[s1;s2]
Lemmas referenced :  sorted-by-unique sorted-by_wf subtype_rel_dep_function l_member_wf subtype_rel_self set_wf set-equal_wf list_wf all_wf not_wf anti_sym_wf trans_wf sorted-by-strict-no_repeats
Rules used in proof :  cut lemma_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality introduction independent_isectElimination cumulativity applyEquality instantiate sqequalRule lambdaEquality functionEquality universeEquality setEquality setElimination rename lambdaFormation because_Cache isect_memberEquality axiomEquality equalityTransitivity equalitySymmetry

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

Date html generated: 2016_05_14-PM-01_48_04
Last ObjectModification: 2015_12_26-PM-05_35_11

Theory : list_1

Home Index