Nuprl Lemma : permutation-split2

`∀[A:Type]`
`  ∀p,q:A ⟶ 𝔹.  ((∀a:A. (↑q[a] `⇐⇒` ¬↑p[a])) `` (∀L:A List. permutation(A;filter(λx.p[x];L) @ filter(λx.q[x];L);L)))`

Proof

Definitions occuring in Statement :  permutation: `permutation(T;L1;L2)` filter: `filter(P;l)` append: `as @ bs` list: `T List` assert: `↑b` bool: `𝔹` uall: `∀[x:A]. B[x]` so_apply: `x[s]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` not: `¬A` implies: `P `` Q` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` implies: `P `` Q` prop: `ℙ` squash: `↓T` so_apply: `x[s]` uimplies: `b supposing a` iff: `P `⇐⇒` Q` and: `P ∧ Q` not: `¬A` false: `False` rev_implies: `P `` Q` uiff: `uiff(P;Q)` true: `True` so_lambda: `λ2x.t[x]` guard: `{T}`
Lemmas referenced :  permutation-split permutation_wf squash_wf true_wf list_wf append_wf filter_wf5 l_member_wf iff_imp_equal_bool bnot_wf assert_wf not_wf assert_of_bnot iff_wf all_wf bool_wf
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality lambdaFormation dependent_functionElimination hyp_replacement equalitySymmetry sqequalRule applyEquality lambdaEquality imageElimination equalityTransitivity universeEquality because_Cache cumulativity setElimination rename functionExtensionality setEquality independent_isectElimination independent_pairFormation independent_functionElimination voidElimination addLevel productElimination impliesFunctionality imageMemberEquality baseClosed natural_numberEquality functionEquality

Latex:
\mforall{}[A:Type]
\mforall{}p,q:A  {}\mrightarrow{}  \mBbbB{}.
((\mforall{}a:A.  (\muparrow{}q[a]  \mLeftarrow{}{}\mRightarrow{}  \mneg{}\muparrow{}p[a]))
{}\mRightarrow{}  (\mforall{}L:A  List.  permutation(A;filter(\mlambda{}x.p[x];L)  @  filter(\mlambda{}x.q[x];L);L)))

Date html generated: 2016_10_21-AM-10_24_58
Last ObjectModification: 2016_07_12-AM-05_37_41

Theory : list_1

Home Index