### Nuprl Lemma : filter_interleaving_occurence

`∀[T:Type]`
`  ∀P:T ⟶ 𝔹. ∀L:T List.`
`    ∃f1:ℕ||filter(λx.(¬b(P x));L)|| ⟶ ℕ||L||`
`     ∃f2:ℕ||filter(P;L)|| ⟶ ℕ||L||`
`      (interleaving_occurence(T;filter(λx.(¬b(P x));L);filter(P;L);L;f1;f2)`
`      ∧ ((∀i:ℕ||L||. ∃k:ℕ||filter(P;L)||. ((i = (f2 k) ∈ ℤ) ∧ (L[i] = filter(P;L)[k] ∈ T)) supposing ↑(P L[i]))`
`        ∧ (∀i:ℕ||L||`
`             ∃k:ℕ||filter(λx.(¬b(P x));L)||. ((i = (f1 k) ∈ ℤ) ∧ (L[i] = filter(λx.(¬b(P x));L)[k] ∈ T)) `
`             supposing ¬↑(P L[i])))`
`      ∧ (∀i:ℕ||filter(λx.(¬b(P x));L)||. (¬↑(P L[f1 i])))`
`      ∧ (∀i:ℕ||filter(P;L)||. (↑(P L[f2 i]))))`

Proof

Definitions occuring in Statement :  interleaving_occurence: `interleaving_occurence(T;L1;L2;L;f1;f2)` select: `L[n]` length: `||as||` filter: `filter(P;l)` list: `T List` int_seg: `{i..j-}` bnot: `¬bb` assert: `↑b` bool: `𝔹` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` not: `¬A` and: `P ∧ Q` apply: `f a` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` natural_number: `\$n` int: `ℤ` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  member: `t ∈ T` all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` implies: `P `` Q` uimplies: `b supposing a` so_apply: `x[s]` so_lambda: `λ2x.t[x]` subtype_rel: `A ⊆r B` prop: `ℙ` nat: `ℕ` le: `A ≤ B` ge: `i ≥ j ` squash: `↓T` less_than: `a < b` top: `Top` not: `¬A` false: `False` satisfiable_int_formula: `satisfiable_int_formula(fmla)` or: `P ∨ Q` decidable: `Dec(P)` lelt: `i ≤ j < k` guard: `{T}` int_seg: `{i..j-}` cand: `A c∧ B` and: `P ∧ Q` exists: `∃x:A. B[x]` istype: `istype(T)` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` true: `True` less_than': `less_than'(a;b)` l_member: `(x ∈ l)` interleaving_occurence: `interleaving_occurence(T;L1;L2;L;f1;f2)` uiff: `uiff(P;Q)` sq_type: `SQType(T)` btrue: `tt` ifthenelse: `if b then t else f fi ` bnot: `¬bb`
Lemmas referenced :  bool_wf list_wf filter_is_interleaving set_wf subtype_rel_self subtype_rel_dep_function l_member_wf bnot_wf filter_wf5 interleaving_implies_occurence equal_wf exists_wf isect_wf all_wf interleaving_occurence_wf nat_properties length_wf_nat lelt_wf non_neg_length not_wf int_seg_wf assert_wf int_formula_prop_less_lemma intformless_wf decidable__lt int_formula_prop_wf int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma itermVar_wf itermConstant_wf intformle_wf intformnot_wf intformand_wf satisfiable-full-omega-tt decidable__le length_wf int_seg_properties select_wf assert_witness interleaving_occurence_onto int_formula_prop_eq_lemma intformeq_wf iff_weakening_equal less_than_wf le_wf true_wf squash_wf false_wf int_seg_subtype_nat member_filter assert_of_bnot int_subtype_base subtype_base_sq btrue_neq_bfalse and_wf bfalse_wf assert_elim
Rules used in proof :  universeEquality functionEquality hypothesis hypothesisEquality cumulativity thin isectElimination sqequalHypSubstitution extract_by_obid introduction cut lambdaFormation isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution independent_functionElimination independent_isectElimination sqequalRule because_Cache setEquality rename setElimination functionExtensionality applyEquality lambdaEquality dependent_functionElimination productEquality applyLambdaEquality equalitySymmetry equalityTransitivity dependent_set_memberEquality imageElimination computeAll voidEquality voidElimination isect_memberEquality intEquality int_eqEquality unionElimination natural_numberEquality independent_pairFormation dependent_pairFormation productElimination lambdaFormation_alt universeIsType setIsType lambdaEquality_alt baseClosed imageMemberEquality instantiate levelHypothesis addLevel

Latex:
\mforall{}[T:Type]
\mforall{}P:T  {}\mrightarrow{}  \mBbbB{}.  \mforall{}L:T  List.
\mexists{}f1:\mBbbN{}||filter(\mlambda{}x.(\mneg{}\msubb{}(P  x));L)||  {}\mrightarrow{}  \mBbbN{}||L||
\mexists{}f2:\mBbbN{}||filter(P;L)||  {}\mrightarrow{}  \mBbbN{}||L||
(interleaving\_occurence(T;filter(\mlambda{}x.(\mneg{}\msubb{}(P  x));L);filter(P;L);L;f1;f2)
\mwedge{}  ((\mforall{}i:\mBbbN{}||L||
\mexists{}k:\mBbbN{}||filter(P;L)||.  ((i  =  (f2  k))  \mwedge{}  (L[i]  =  filter(P;L)[k]))  supposing  \muparrow{}(P  L[i]))
\mwedge{}  (\mforall{}i:\mBbbN{}||L||
\mexists{}k:\mBbbN{}||filter(\mlambda{}x.(\mneg{}\msubb{}(P  x));L)||.  ((i  =  (f1  k))  \mwedge{}  (L[i]  =  filter(\mlambda{}x.(\mneg{}\msubb{}(P  x));L)[k]))
supposing  \mneg{}\muparrow{}(P  L[i])))
\mwedge{}  (\mforall{}i:\mBbbN{}||filter(\mlambda{}x.(\mneg{}\msubb{}(P  x));L)||.  (\mneg{}\muparrow{}(P  L[f1  i])))
\mwedge{}  (\mforall{}i:\mBbbN{}||filter(P;L)||.  (\muparrow{}(P  L[f2  i]))))

Date html generated: 2020_05_20-AM-07_48_54
Last ObjectModification: 2020_01_25-AM-09_00_33

Theory : list!

Home Index