### Nuprl Lemma : no_repeats_functionality_wrt_permutation

`∀[A:Type]. ∀as1,as2:A List.  (permutation(A;as1;as2) `` (no_repeats(A;as1) `⇐⇒` no_repeats(A;as2)))`

Proof

Definitions occuring in Statement :  permutation: `permutation(T;L1;L2)` no_repeats: `no_repeats(T;l)` list: `T List` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` implies: `P `` Q` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` implies: `P `` Q` iff: `P `⇐⇒` Q` and: `P ∧ Q` prop: `ℙ` rev_implies: `P `` Q` permutation: `permutation(T;L1;L2)` exists: `∃x:A. B[x]` no_repeats: `no_repeats(T;l)` uimplies: `b supposing a` not: `¬A` false: `False` nat: `ℕ` ge: `i ≥ j ` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` top: `Top` int_seg: `{i..j-}` lelt: `i ≤ j < k` le: `A ≤ B` true: `True` squash: `↓T` subtype_rel: `A ⊆r B` guard: `{T}` less_than': `less_than'(a;b)` inject: `Inj(A;B;f)`
Lemmas referenced :  no_repeats_witness no_repeats_wf permutation_wf list_wf length_wf_nat equal_wf nat_wf select_wf nat_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf not_wf less_than_wf length_wf permute_list_wf int_seg_wf permute_list_length lelt_wf squash_wf true_wf permute_list_select iff_weakening_equal non_neg_length decidable__lt int_seg_properties intformless_wf int_formula_prop_less_lemma int_seg_subtype_nat false_wf decidable__equal_int intformeq_wf int_formula_prop_eq_lemma permutation_inversion
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule sqequalHypSubstitution lambdaEquality dependent_functionElimination thin hypothesisEquality productElimination independent_pairEquality extract_by_obid isectElimination independent_functionElimination hypothesis cumulativity universeEquality lambdaFormation dependent_set_memberEquality hyp_replacement equalitySymmetry applyLambdaEquality setElimination rename voidElimination because_Cache equalityTransitivity independent_isectElimination natural_numberEquality unionElimination dependent_pairFormation int_eqEquality intEquality isect_memberEquality voidEquality independent_pairFormation computeAll functionExtensionality applyEquality imageElimination imageMemberEquality baseClosed

Latex:
\mforall{}[A:Type].  \mforall{}as1,as2:A  List.    (permutation(A;as1;as2)  {}\mRightarrow{}  (no\_repeats(A;as1)  \mLeftarrow{}{}\mRightarrow{}  no\_repeats(A;as2)))

Date html generated: 2017_04_17-AM-08_12_17
Last ObjectModification: 2017_02_27-PM-04_39_38

Theory : list_1

Home Index