### Nuprl Lemma : permute-to-front-permutation

`∀[T:Type]. ∀L:T List. ∀idxs:ℕ List.  permutation(T;L;permute-to-front(L;idxs))`

Proof

Definitions occuring in Statement :  permute-to-front: `permute-to-front(L;idxs)` permutation: `permutation(T;L1;L2)` list: `T List` nat: `ℕ` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` permute-to-front: `permute-to-front(L;idxs)` permutation: `permutation(T;L1;L2)` exists: `∃x:A. B[x]` member: `t ∈ T` prop: `ℙ` int_seg: `{i..j-}` subtype_rel: `A ⊆r B` uimplies: `b supposing a` nat: `ℕ` guard: `{T}` lelt: `i ≤ j < k` and: `P ∧ Q` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` false: `False` implies: `P `` Q` not: `¬A` top: `Top` squash: `↓T` so_lambda: `λ2x.t[x]` so_apply: `x[s]` true: `True` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` less_than: `a < b` cand: `A c∧ B` sq_type: `SQType(T)` le: `A ≤ B` less_than': `less_than'(a;b)` uiff: `uiff(P;Q)` l_disjoint: `l_disjoint(T;l1;l2)`
Lemmas referenced :  list_wf nat_wf select_wf int_seg_wf append_wf filter_wf5 upto_wf l_member_wf length_wf int-list-member_wf subtype_rel_list bnot_wf int_seg_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf length-append less_than_wf squash_wf true_wf length_upto length_wf_nat filter-split-length iff_weakening_equal decidable__lt intformless_wf int_formula_prop_less_lemma permute_list_wf equal_wf subtype_base_sq list_subtype_base set_subtype_base lelt_wf int_subtype_base no_repeats_inject int_seg_subtype false_wf intformeq_wf int_formula_prop_eq_lemma no_repeats_append_iff no_repeats_filter no_repeats_upto member_filter assert_wf not_wf assert-int-list-member iff_transitivity iff_weakening_uiff assert_of_bnot inject_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation dependent_pairFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesis cumulativity hypothesisEquality universeEquality lambdaEquality natural_numberEquality because_Cache setElimination rename dependent_functionElimination applyEquality intEquality independent_isectElimination sqequalRule setEquality productElimination unionElimination int_eqEquality isect_memberEquality voidElimination voidEquality independent_pairFormation computeAll imageElimination equalityTransitivity equalitySymmetry imageMemberEquality baseClosed independent_functionElimination instantiate productEquality impliesFunctionality functionExtensionality

Latex:
\mforall{}[T:Type].  \mforall{}L:T  List.  \mforall{}idxs:\mBbbN{}  List.    permutation(T;L;permute-to-front(L;idxs))

Date html generated: 2018_05_21-PM-07_32_07
Last ObjectModification: 2017_07_26-PM-05_07_17

Theory : general

Home Index