Nuprl Lemma : length-unshuffle

∀[T:Type]. ∀[L:T List]. (||unshuffle(L)|| ~ ||L|| ÷ 2)

Proof

Definitions occuring in Statement : unshuffle: unshuffle(L), length: ||as||, list: T List, uall: ∀[x:A]. B[x], divide: n ÷ m, natural_number: $n, universe: Type, sqequal: s ~ t
Definitions unfolded in proof : uall: ∀[x:A]. B[x], member: t ∈ T, all: ∀x:A. B[x], nat: ℕ, implies: P ⇒ Q, false: False, ge: i ≥ j , uimplies: b supposing a, not: ¬A, satisfiable_int_formula: satisfiable_int_formula(fmla), exists: ∃x:A. B[x], top: Top, and: P ∧ Q, prop: ℙ, guard: {T}, int_seg: {i..j^-}, lelt: i ≤ j < k, le: A ≤ B, decidable: Dec(P), or: P ∨ Q, subtype_rel: A ⊆r B, so_lambda: λ₂x.t[x], so_apply: x[s], sq_type: SQType(T), less_than: a < b, squash: ↓T, unshuffle: unshuffle(L), bool: 𝔹, unit: Unit, it: ⋅, btrue: tt, uiff: uiff(P;Q), ifthenelse: if b then t else f fi , less_than': less_than'(a;b), bfalse: ff, true: True, cons: [a / b], iff: P ⇐⇒ Q, rev_implies: P ⇐ Q, divide: n ÷ m, nat_plus: ℕ⁺, int_nzero: ℤ^-^o, nequal: a ≠ b ∈ T , subtract: n - m
Lemmas referenced : nat_properties, full-omega-unsat, intformand_wf, intformle_wf, itermConstant_wf, itermVar_wf, intformless_wf, istype-int, int_formula_prop_and_lemma, istype-void, int_formula_prop_le_lemma, int_term_value_constant_lemma, int_term_value_var_lemma, int_formula_prop_less_lemma, int_formula_prop_wf, ge_wf, istype-less_than, int_seg_properties, int_seg_wf, subtract-1-ge-0, decidable__equal_int, subtract_wf, subtype_base_sq, set_subtype_base, int_subtype_base, intformnot_wf, intformeq_wf, itermSubtract_wf, int_formula_prop_not_lemma, int_formula_prop_eq_lemma, int_term_value_subtract_lemma, decidable__le, decidable__lt, istype-le, subtype_rel_self, non_neg_length, length_wf, nat_wf, le_wf, lt_int_wf, uiff_transitivity, equal-wf-T-base, bool_wf, assert_wf, less_than_wf, eqtt_to_assert, assert_of_lt_int, length_of_nil_lemma, istype-false, le_int_wf, bnot_wf, eqff_to_assert, assert_functionality_wrt_uiff, bnot_of_lt_int, assert_of_le_int, length_of_cons_lemma, tl_wf, list-cases, reduce_tl_nil_lemma, product_subtype_list, reduce_tl_cons_lemma, length_tl, add-is-int-iff, itermAdd_wf, int_term_value_add_lemma, false_wf, iff_weakening_equal, add_nat_wf, divide_wf, equal_wf, divide_wfa, nequal_wf, div_rec_case, add-associates, add-swap, add-commutes, zero-add, istype-nat, length_wf_nat, list_wf, istype-universe
Rules used in proof : sqequalSubstitution, sqequalTransitivity, computationStep, sqequalReflexivity, Error :isect_memberFormation_alt, introduction, cut, thin, Error :lambdaFormation_alt, extract_by_obid, sqequalHypSubstitution, isectElimination, hypothesisEquality, hypothesis, setElimination, rename, intWeakElimination, natural_numberEquality, independent_isectElimination, approximateComputation, independent_functionElimination, Error :dependent_pairFormation_alt, Error :lambdaEquality_alt, int_eqEquality, dependent_functionElimination, Error :isect_memberEquality_alt, voidElimination, sqequalRule, independent_pairFormation, Error :universeIsType, axiomSqEquality, Error :functionIsTypeImplies, Error :inhabitedIsType, productElimination, unionElimination, applyEquality, instantiate, because_Cache, equalityTransitivity, equalitySymmetry, applyLambdaEquality, Error :dependent_set_memberEquality_alt, Error :productIsType, hypothesis_subsumption, imageElimination, cumulativity, intEquality, equalityElimination, baseClosed, promote_hyp, pointwiseFunctionality, baseApply, closedConclusion, addEquality, imageMemberEquality, Error :equalityIstype, sqequalBase, Error :isectIsTypeImplies, universeEquality

Latex:
\mforall{}[T:Type]. \mforall{}[L:T List]. (||unshuffle(L)|| \msim{} ||L|| \mdiv{} 2) Date html generated: 2019_06_20-PM-01_47_34 Last ObjectModification: 2019_03_06-AM-10_30_07 Theory : list_1 Home Index