### Nuprl Lemma : interleaving_as_filter

[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L,L1,L2:T List].
({(L2 filter(P;L) ∈ (T List)) ∧ (L1 filter(λx.(¬b(P x));L) ∈ (T List))}) supposing
((∀x∈L1.¬↑(P x)) and
(∀x∈L2.↑(P x)) and
interleaving(T;L1;L2;L))

Proof

Definitions occuring in Statement :  interleaving: interleaving(T;L1;L2;L) l_all: (∀x∈L.P[x]) filter: filter(P;l) list: List bnot: ¬bb assert: b bool: 𝔹 uimplies: supposing a uall: [x:A]. B[x] guard: {T} not: ¬A and: P ∧ Q apply: a lambda: λx.A[x] function: x:A ⟶ B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  guard: {T} uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a and: P ∧ Q cand: c∧ B prop: so_lambda: λ2x.t[x] so_apply: x[s] all: x:A. B[x] implies:  Q subtype_rel: A ⊆B iff: ⇐⇒ Q l_all: (∀x∈L.P[x]) int_seg: {i..j-} lelt: i ≤ j < k decidable: Dec(P) or: P ∨ Q not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False top: Top less_than: a < b squash: T uiff: uiff(P;Q) rev_uimplies: rev_uimplies(P;Q)
Lemmas referenced :  l_all_wf not_wf assert_wf l_member_wf interleaving_wf list_wf bool_wf filter_interleaving filter_trivial filter_is_nil nil_interleaving filter_wf5 subtype_rel_dep_function subtype_rel_self set_wf bnot_wf assert_of_bnot select_wf int_seg_properties length_wf decidable__le full-omega-unsat 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 decidable__lt intformless_wf int_formula_prop_less_lemma int_seg_wf not_functionality_wrt_uiff false_wf nil_interleaving2
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut independent_pairFormation hypothesis sqequalHypSubstitution productElimination thin independent_pairEquality axiomEquality extract_by_obid isectElimination hypothesisEquality lambdaEquality applyEquality setElimination rename setEquality isect_memberEquality because_Cache equalityTransitivity equalitySymmetry functionEquality universeEquality dependent_functionElimination independent_functionElimination independent_isectElimination lambdaFormation functionExtensionality cumulativity natural_numberEquality unionElimination approximateComputation dependent_pairFormation int_eqEquality intEquality voidElimination voidEquality imageElimination

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[L,L1,L2:T  List].
(\{(L2  =  filter(P;L))  \mwedge{}  (L1  =  filter(\mlambda{}x.(\mneg{}\msubb{}(P  x));L))\})  supposing
((\mforall{}x\mmember{}L1.\mneg{}\muparrow{}(P  x))  and
(\mforall{}x\mmember{}L2.\muparrow{}(P  x))  and
interleaving(T;L1;L2;L))

Date html generated: 2019_10_15-AM-10_56_47
Last ObjectModification: 2018_09_17-PM-06_33_10

Theory : list!

Home Index