Nuprl Lemma : permutation-filter

[A:Type]. ∀L1,L2:A List.  (permutation(A;L1;L2)  (∀p:A ⟶ 𝔹permutation({a:A| ↑(p a)} ;filter(p;L1);filter(p;L2))))


Proof




Definitions occuring in Statement :  permutation: permutation(T;L1;L2) filter: filter(P;l) list: List assert: b bool: 𝔹 uall: [x:A]. B[x] all: x:A. B[x] implies:  Q set: {x:A| B[x]}  apply: a function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] member: t ∈ T so_lambda: λ2x.t[x] implies:  Q prop: so_apply: x[s] top: Top or: P ∨ Q cons: [a b] uimplies: supposing a bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) and: P ∧ Q ifthenelse: if then else fi  ge: i ≥  le: A ≤ B satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False not: ¬A bfalse: ff sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b iff: ⇐⇒ Q rev_implies:  Q cand: c∧ B
Lemmas referenced :  list_induction all_wf list_wf permutation_wf bool_wf assert_wf filter_type filter_nil_lemma nil_wf filter_cons_lemma cons_wf list-cases product_subtype_list permutation_weakening permutation-length length_of_nil_lemma length_of_cons_lemma eqtt_to_assert 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 eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot permutation-cons filter_append_sq append_wf length_wf length-append exists_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut thin introduction extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality sqequalRule lambdaEquality cumulativity hypothesis functionEquality setEquality applyEquality functionExtensionality independent_functionElimination dependent_functionElimination isect_memberEquality voidElimination voidEquality because_Cache rename universeEquality unionElimination promote_hyp hypothesis_subsumption productElimination independent_isectElimination equalityElimination equalityTransitivity equalitySymmetry natural_numberEquality dependent_pairFormation int_eqEquality intEquality independent_pairFormation computeAll instantiate hyp_replacement applyLambdaEquality dependent_set_memberEquality productEquality

Latex:
\mforall{}[A:Type]
    \mforall{}L1,L2:A  List.
        (permutation(A;L1;L2)  {}\mRightarrow{}  (\mforall{}p:A  {}\mrightarrow{}  \mBbbB{}.  permutation(\{a:A|  \muparrow{}(p  a)\}  ;filter(p;L1);filter(p;L2))))



Date html generated: 2017_04_17-AM-08_24_46
Last ObjectModification: 2017_02_27-PM-04_46_50

Theory : list_1


Home Index