### Nuprl Lemma : filter_before

`∀[A:Type]. ∀L:A List. ∀P:A ⟶ 𝔹. ∀x,y:A.  (x before y ∈ filter(P;L) `⇐⇒` (↑(P x)) ∧ (↑(P y)) ∧ x before y ∈ L)`

Proof

Definitions occuring in Statement :  l_before: `x before y ∈ l` filter: `filter(P;l)` list: `T List` assert: `↑b` bool: `𝔹` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  top: `Top` implies: `P `` Q` and: `P ∧ Q` uimplies: `b supposing a` prop: `ℙ` so_apply: `x[s]` subtype_rel: `A ⊆r B` so_lambda: `λ2x.t[x]` member: `t ∈ T` all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` false: `False` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` true: `True` bfalse: `ff` ifthenelse: `if b then t else f fi ` uiff: `uiff(P;Q)` btrue: `tt` it: `⋅` unit: `Unit` bool: `𝔹` guard: `{T}` or: `P ∨ Q` cand: `A c∧ B` istype: `istype(T)` not: `¬A`
Lemmas referenced :  filter_cons_lemma filter_nil_lemma list_wf assert_wf set_wf subtype_rel_self l_member_wf subtype_rel_dep_function filter_wf5 l_before_wf iff_wf bool_wf all_wf list_induction nil_wf nil_before false_wf assert_of_bnot eqff_to_assert uiff_transitivity eqtt_to_assert not_wf bnot_wf equal-wf-T-base cons_wf cons_before equal_wf or_wf assert_witness member_filter member_filter_2 assert_elim not_assert_elim btrue_neq_bfalse
Rules used in proof :  universeEquality voidEquality voidElimination isect_memberEquality dependent_functionElimination independent_functionElimination productEquality rename setElimination independent_isectElimination setEquality because_Cache applyEquality hypothesis functionEquality lambdaEquality sqequalRule hypothesisEquality isectElimination sqequalHypSubstitution extract_by_obid introduction thin cut lambdaFormation isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution cumulativity promote_hyp productElimination independent_pairFormation natural_numberEquality equalityElimination unionElimination inrFormation baseClosed equalitySymmetry equalityTransitivity applyLambdaEquality hyp_replacement inlFormation_alt lambdaEquality_alt inhabitedIsType setIsType universeIsType lambdaFormation_alt inrFormation_alt productIsType equalityIstype dependent_set_memberEquality_alt

Latex:
\mforall{}[A:Type]
\mforall{}L:A  List.  \mforall{}P:A  {}\mrightarrow{}  \mBbbB{}.  \mforall{}x,y:A.    (x  before  y  \mmember{}  filter(P;L)  \mLeftarrow{}{}\mRightarrow{}  (\muparrow{}(P  x))  \mwedge{}  (\muparrow{}(P  y))  \mwedge{}  x  before  y  \mmember{}  L)

Date html generated: 2019_10_15-AM-10_21_49
Last ObjectModification: 2019_08_20-PM-05_00_31

Theory : list_1

Home Index