Nuprl Lemma : filter_is_interleaving

`∀[T:Type]. ∀P:T ⟶ 𝔹. ∀L:T List.  interleaving(T;filter(λx.(¬b(P x));L);filter(P;L);L)`

Proof

Definitions occuring in Statement :  interleaving: `interleaving(T;L1;L2;L)` filter: `filter(P;l)` list: `T List` bnot: `¬bb` bool: `𝔹` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` apply: `f a` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` member: `t ∈ T` int_seg: `{i..j-}` uimplies: `b supposing a` guard: `{T}` lelt: `i ≤ j < k` and: `P ∧ Q` decidable: `Dec(P)` or: `P ∨ Q` not: `¬A` implies: `P `` Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` top: `Top` prop: `ℙ` less_than: `a < b` squash: `↓T` iff: `P `⇐⇒` Q` l_all: `(∀x∈L.P[x])` so_apply: `x[s]` interleaving_occurence: `interleaving_occurence(T;L1;L2;L;f1;f2)`
Lemmas referenced :  interleaving_split assert_wf select_wf int_seg_properties length_wf decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf istype-int int_formula_prop_and_lemma istype-void 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 decidable__assert list_wf istype-universe bool_wf occurence_implies_interleaving interleaving_as_filter_2 interleaving_symmetry filter_trivial2 nil_wf filter_is_nil not_wf interleaving_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt lambdaFormation_alt cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality dependent_functionElimination lambdaEquality_alt applyEquality setElimination rename because_Cache hypothesis independent_isectElimination natural_numberEquality productElimination unionElimination approximateComputation independent_functionElimination dependent_pairFormation_alt int_eqEquality isect_memberEquality_alt voidElimination sqequalRule independent_pairFormation universeIsType imageElimination functionIsType universeEquality equalitySymmetry hyp_replacement applyLambdaEquality equalityTransitivity

Latex:
\mforall{}[T:Type].  \mforall{}P:T  {}\mrightarrow{}  \mBbbB{}.  \mforall{}L:T  List.    interleaving(T;filter(\mlambda{}x.(\mneg{}\msubb{}(P  x));L);filter(P;L);L)

Date html generated: 2019_10_15-AM-10_57_29
Last ObjectModification: 2018_10_09-AM-09_58_35

Theory : list!

Home Index