Nuprl Lemma : quicksort-int-member

`∀L:ℤ List. ∀x:ℤ.  ((x ∈ L) `⇐⇒` (x ∈ quicksort-int(L)))`

Proof

Definitions occuring in Statement :  quicksort-int: `quicksort-int(L)` l_member: `(x ∈ l)` list: `T List` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` int: `ℤ`
Definitions unfolded in proof :  all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` implies: `P `` Q` member: `t ∈ T` squash: `↓T` uall: `∀[x:A]. B[x]` prop: `ℙ` rev_implies: `P `` Q` subtype_rel: `A ⊆r B` guard: `{T}` sq_stable: `SqStable(P)`
Lemmas referenced :  decidable__equal_int sq_stable__l_member member-permutation permutation_wf l_member_wf le_wf sorted-by_wf and_wf list_wf quicksort-int_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation independent_pairFormation cut lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality applyEquality lambdaEquality setElimination rename hypothesis sqequalRule imageMemberEquality baseClosed setEquality isectElimination intEquality introduction because_Cache imageElimination equalityTransitivity equalitySymmetry productElimination independent_functionElimination

Latex:
\mforall{}L:\mBbbZ{}  List.  \mforall{}x:\mBbbZ{}.    ((x  \mmember{}  L)  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  quicksort-int(L)))

Date html generated: 2016_05_15-PM-04_30_01
Last ObjectModification: 2016_01_16-AM-11_14_48

Theory : general

Home Index