### Nuprl Lemma : permutation-invariant

`∀[T:Type]. ∀[P:(T List) ⟶ ℙ].`
`  ((∀as:T List. ∀a:T.  (P[[a / as]] `` P[as @ [a]]))`
`  `` (∀as:T List. ∀a1,a2:T.  (P[[a1; [a2 / as]]] `` P[[a2; [a1 / as]]]))`
`  `` (∀as,bs:T List.  (permutation(T;as;bs) `` (P[as] `⇐⇒` P[bs]))))`

Proof

Definitions occuring in Statement :  permutation: `permutation(T;L1;L2)` append: `as @ bs` cons: `[a / b]` nil: `[]` list: `T List` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` implies: `P `` Q` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` implies: `P `` Q` member: `t ∈ T` so_lambda: `λ2x y.t[x; y]` prop: `ℙ` so_apply: `x[s]` so_apply: `x[s1;s2]` trans: `Trans(T;x,y.E[x; y])` all: `∀x:A. B[x]` refl: `Refl(T;x,y.E[x; y])` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` so_lambda: `λ2x.t[x]` guard: `{T}`
Lemmas referenced :  permutation-invariant2 list_wf permutation_inversion permutation_wf all_wf cons_wf append_wf nil_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality sqequalRule lambdaEquality functionEquality applyEquality hypothesis independent_functionElimination because_Cache independent_pairFormation dependent_functionElimination cumulativity universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[P:(T  List)  {}\mrightarrow{}  \mBbbP{}].
((\mforall{}as:T  List.  \mforall{}a:T.    (P[[a  /  as]]  {}\mRightarrow{}  P[as  @  [a]]))
{}\mRightarrow{}  (\mforall{}as:T  List.  \mforall{}a1,a2:T.    (P[[a1;  [a2  /  as]]]  {}\mRightarrow{}  P[[a2;  [a1  /  as]]]))
{}\mRightarrow{}  (\mforall{}as,bs:T  List.    (permutation(T;as;bs)  {}\mRightarrow{}  (P[as]  \mLeftarrow{}{}\mRightarrow{}  P[bs]))))

Date html generated: 2016_05_14-PM-02_30_59
Last ObjectModification: 2015_12_26-PM-04_23_11

Theory : list_1

Home Index