### Nuprl Lemma : strict-majority_functionality

`∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L1,L2:T List].`
`  (strict-majority(eq;L1) = strict-majority(eq;L2) ∈ (T?)) supposing `
`     ((||L1|| = ||L2|| ∈ ℤ) and `
`     (∀x:T. (||filter(λy.(eq y x);L1)|| = ||filter(λy.(eq y x);L2)|| ∈ ℤ)))`

Proof

Definitions occuring in Statement :  strict-majority: `strict-majority(eq;L)` length: `||as||` filter: `filter(P;l)` list: `T List` deq: `EqDecider(T)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` unit: `Unit` apply: `f a` lambda: `λx.A[x]` union: `left + right` int: `ℤ` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` prop: `ℙ` so_lambda: `λ2x.t[x]` all: `∀x:A. B[x]` deq: `EqDecider(T)` so_apply: `x[s]` implies: `P `` Q` uiff: `uiff(P;Q)` and: `P ∧ Q` squash: `↓T` true: `True` subtype_rel: `A ⊆r B` guard: `{T}` iff: `P `⇐⇒` Q`
Lemmas referenced :  equal_wf length_wf all_wf filter_wf5 l_member_wf strict-majority-property strict-majority_wf unit_wf2 less_than_wf squash_wf true_wf iff_weakening_equal equal-unit
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut hypothesis extract_by_obid sqequalHypSubstitution isectElimination thin intEquality cumulativity hypothesisEquality sqequalRule isect_memberEquality axiomEquality because_Cache equalityTransitivity equalitySymmetry lambdaEquality lambdaFormation setElimination rename applyEquality setEquality unionEquality unionElimination dependent_functionElimination independent_functionElimination productElimination independent_pairFormation independent_isectElimination imageElimination multiplyEquality natural_numberEquality imageMemberEquality baseClosed universeEquality inrEquality

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[L1,L2:T  List].
(strict-majority(eq;L1)  =  strict-majority(eq;L2))  supposing
((||L1||  =  ||L2||)  and
(\mforall{}x:T.  (||filter(\mlambda{}y.(eq  y  x);L1)||  =  ||filter(\mlambda{}y.(eq  y  x);L2)||)))

Date html generated: 2017_04_17-AM-09_09_36
Last ObjectModification: 2017_02_27-PM-05_17_32

Theory : decidable!equality

Home Index