### Nuprl Lemma : null-filter

`∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L:T List].  uiff(↑null(filter(P;L));(∀x∈L.¬↑P[x]))`

Proof

Definitions occuring in Statement :  l_all: `(∀x∈L.P[x])` null: `null(as)` filter: `filter(P;l)` list: `T List` assert: `↑b` bool: `𝔹` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` so_apply: `x[s]` not: `¬A` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` member: `t ∈ T` uall: `∀[x:A]. B[x]` so_lambda: `λ2x.t[x]` implies: `P `` Q` prop: `ℙ` subtype_rel: `A ⊆r B` so_apply: `x[s]` all: `∀x:A. B[x]` top: `Top` assert: `↑b` ifthenelse: `if b then t else f fi ` btrue: `tt` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` cand: `A c∧ B` or: `P ∨ Q` sq_type: `SQType(T)` guard: `{T}` not: `¬A` false: `False` bfalse: `ff` bool: `𝔹` unit: `Unit` it: `⋅` exists: `∃x:A. B[x]` bnot: `¬bb` l_all: `(∀x∈L.P[x])` int_seg: `{i..j-}` sq_stable: `SqStable(P)` lelt: `i ≤ j < k` squash: `↓T`
Lemmas referenced :  list_induction assert_wf null_wf filter_wf5 l_all_wf not_wf l_member_wf list_wf filter_nil_lemma null_nil_lemma l_all_nil true_wf filter_cons_lemma l_all_cons bool_cases subtype_base_sq bool_wf bool_subtype_base eqtt_to_assert assert_elim cons_wf subtype_rel_dep_function subtype_rel_self set_wf null_cons_lemma bfalse_wf btrue_neq_bfalse eqff_to_assert assert_of_bnot iff_imp_equal_bool equal_wf bool_cases_sqequal and_wf ifthenelse_wf false_wf assert-bnot null_filter assert_witness select_wf sq_stable__le int_seg_wf length_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity independent_pairFormation isect_memberFormation introduction cut thin extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality sqequalRule lambdaEquality functionEquality cumulativity applyEquality because_Cache hypothesis functionExtensionality setElimination rename setEquality independent_functionElimination dependent_functionElimination isect_memberEquality voidElimination voidEquality lambdaFormation productElimination unionElimination instantiate independent_isectElimination equalityTransitivity equalitySymmetry addLevel levelHypothesis equalityElimination dependent_pairFormation promote_hyp dependent_set_memberEquality applyLambdaEquality natural_numberEquality imageMemberEquality baseClosed imageElimination universeEquality independent_pairEquality

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[L:T  List].    uiff(\muparrow{}null(filter(P;L));(\mforall{}x\mmember{}L.\mneg{}\muparrow{}P[x]))

Date html generated: 2017_04_14-AM-08_52_28
Last ObjectModification: 2017_02_27-PM-03_38_29

Theory : list_0

Home Index