### Nuprl Lemma : permutation-split

`∀[A:Type]. ∀p:A ⟶ 𝔹. ∀L:A List.  permutation(A;filter(λx.p[x];L) @ filter(λx.(¬bp[x]);L);L)`

Proof

Definitions occuring in Statement :  permutation: `permutation(T;L1;L2)` filter: `filter(P;l)` append: `as @ bs` list: `T List` bnot: `¬bb` bool: `𝔹` uall: `∀[x:A]. B[x]` so_apply: `x[s]` all: `∀x:A. B[x]` lambda: `λx.A[x]` 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]` so_apply: `x[s]` prop: `ℙ` implies: `P `` Q` top: `Top` append: `as @ bs` so_lambda: `so_lambda(x,y,z.t[x; y; z])` so_apply: `x[s1;s2;s3]` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` ifthenelse: `if b then t else f fi ` bnot: `¬bb` bfalse: `ff` iff: `P `⇐⇒` Q` rev_implies: `P `` Q`
Lemmas referenced :  list_induction permutation_wf append_wf filter_wf5 l_member_wf bnot_wf list_wf filter_nil_lemma list_ind_nil_lemma permutation-nil filter_cons_lemma bool_wf eqtt_to_assert list_ind_cons_lemma uiff_transitivity equal-wf-T-base assert_wf not_wf eqff_to_assert assert_of_bnot equal_wf cons_wf nil_wf permutation_weakening permutation_functionality_wrt_permutation append_functionality_wrt_permutation permutation-rotate
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut thin introduction extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality sqequalRule lambdaEquality cumulativity applyEquality functionExtensionality setElimination rename hypothesis setEquality because_Cache independent_functionElimination dependent_functionElimination isect_memberEquality voidElimination voidEquality functionEquality universeEquality unionElimination equalityElimination equalityTransitivity equalitySymmetry productElimination independent_isectElimination baseClosed

Latex:
\mforall{}[A:Type].  \mforall{}p:A  {}\mrightarrow{}  \mBbbB{}.  \mforall{}L:A  List.    permutation(A;filter(\mlambda{}x.p[x];L)  @  filter(\mlambda{}x.(\mneg{}\msubb{}p[x]);L);L)

Date html generated: 2017_04_17-AM-08_25_15
Last ObjectModification: 2017_02_27-PM-04_46_25

Theory : list_1

Home Index