Nuprl Lemma : permutation_functionality_wrt_permutation

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

Proof

Definitions occuring in Statement :  permutation: `permutation(T;L1;L2)` 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]` all: `∀x:A. B[x]` implies: `P `` Q` iff: `P `⇐⇒` Q` and: `P ∧ Q` member: `t ∈ T` guard: `{T}` prop: `ℙ` rev_implies: `P `` Q`
Lemmas referenced :  permutation_inversion permutation_transitivity permutation_wf list_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation independent_pairFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality dependent_functionElimination independent_functionElimination hypothesis universeEquality

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

Date html generated: 2016_05_14-PM-02_20_10
Last ObjectModification: 2015_12_26-PM-04_28_23

Theory : list_1

Home Index