### 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