### 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 a))) and `
`     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)` 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: `ℙ` all: `∀x:A. B[x]` not: `¬A` 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` prop: `ℙ` subtype_rel: `A ⊆r B` so_lambda: `λ2x.t[x]` so_apply: `x[s]` all: `∀x:A. B[x]` so_lambda: `λ2x y.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

Latex:
\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