Nuprl Lemma : permutation-sorted-by-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 permutation(T;sa;sb)) 
  supposing Linorder(T;a,b.R b)


Definitions occuring in Statement :  permutation: permutation(T;L1;L2) sorted-by: sorted-by(R;L) list: List linorder: Linorder(T;x,y.R[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] iff: ⇐⇒ Q and: P ∧ Q top: Top not: ¬A false: False ge: i ≥  le: A ≤ B satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] or: P ∨ Q l_contains: A ⊆ B rev_implies:  Q guard: {T} linorder: Linorder(T;x,y.R[x; y]) order: Order(T;x,y.R[x; y]) 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 permutation_wf sorted-by_wf subtype_rel_dep_function l_member_wf subtype_rel_self set_wf equal_wf linorder_wf permutation-nil-iff nil_wf sorted-by_wf_nil null_nil_lemma btrue_wf member-implies-null-eq-bfalse and_wf null_wf btrue_neq_bfalse cons_wf permutation-length length_of_cons_lemma length_of_nil_lemma non_neg_length satisfiable-full-omega-tt intformand_wf intformle_wf itermConstant_wf itermVar_wf intformeq_wf itermAdd_wf int_formula_prop_and_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_eq_lemma int_term_value_add_lemma int_formula_prop_wf sorted-by-cons permutation-contains permutation_inversion l_contains_cons cons_member l_all_iff cons_cancel_wrt_permutation 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 productElimination voidElimination voidEquality dependent_set_memberEquality independent_pairFormation hyp_replacement Error :applyLambdaEquality,  natural_numberEquality dependent_pairFormation int_eqEquality intEquality computeAll unionElimination inlFormation imageElimination imageMemberEquality baseClosed

\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  permutation(T;sa;sb)) 
    supposing  Linorder(T;a,b.R  a  b)

Date html generated: 2016_10_21-AM-10_24_14
Last ObjectModification: 2016_07_12-AM-05_38_29

Theory : list_1

Home Index