### Nuprl Lemma : iseg_filter_last

`∀[T:Type]`
`  ∀P:T ⟶ 𝔹. ∀L_1,L_2:T List.`
`    (0 < ||L_2||`
`    `` L_2 ≤ filter(P;L_1)`
`    `` (∃L_3:T List. (L_3 ≤ L_1 ∧ (L_2 = filter(P;L_3) ∈ (T List)) ∧ 0 < ||L_3|| ∧ (last(L_2) = last(L_3) ∈ T))))`

Proof

Definitions occuring in Statement :  iseg: `l1 ≤ l2` last: `last(L)` length: `||as||` filter: `filter(P;l)` list: `T List` bool: `𝔹` less_than: `a < b` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` function: `x:A ⟶ B[x]` natural_number: `\$n` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` member: `t ∈ T` so_lambda: `λ2x.t[x]` prop: `ℙ` implies: `P `` Q` subtype_rel: `A ⊆r B` so_apply: `x[s]` uimplies: `b supposing a` istype: `istype(T)` exists: `∃x:A. B[x]` and: `P ∧ Q` or: `P ∨ Q` assert: `↑b` ifthenelse: `if b then t else f fi ` btrue: `tt` less_than: `a < b` squash: `↓T` less_than': `less_than'(a;b)` false: `False` cons: `[a / b]` bfalse: `ff` not: `¬A` bool: `𝔹` unit: `Unit` it: `⋅` uiff: `uiff(P;Q)` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb` iff: `P `⇐⇒` Q` top: `Top` length: `||as||` list_ind: list_ind nil: `[]` decidable: `Dec(P)` cand: `A c∧ B` ge: `i ≥ j ` le: `A ≤ B` satisfiable_int_formula: `satisfiable_int_formula(fmla)` true: `True` rev_implies: `P `` Q` nat_plus: `ℕ+` iseg: `l1 ≤ l2` append: `as @ bs` so_lambda: so_lambda3 so_apply: `x[s1;s2;s3]`
Lemmas referenced :  list_induction list_wf less_than_wf length_wf iseg_wf filter_wf5 subtype_rel_dep_function bool_wf l_member_wf equal_wf last_wf list-cases null_nil_lemma length_of_nil_lemma product_subtype_list null_cons_lemma length_of_cons_lemma istype-void filter_nil_lemma nil_wf istype-less_than filter_cons_lemma eqtt_to_assert eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot istype-universe iseg_nil cons_iseg decidable__lt cons_wf non_neg_length full-omega-unsat intformand_wf intformnot_wf intformless_wf itermConstant_wf itermAdd_wf itermVar_wf intformle_wf istype-int int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_add_lemma int_term_value_var_lemma int_formula_prop_le_lemma int_formula_prop_wf squash_wf true_wf last_cons assert_elim null_wf bfalse_wf btrue_neq_bfalse istype-assert subtype_rel_self iff_weakening_equal add_nat_plus length_wf_nat nat_plus_properties add-is-int-iff intformeq_wf int_formula_prop_eq_lemma false_wf list_decomp reduce_tl_cons_lemma reduce_hd_cons_lemma filter_trivial l_all_cons assert_wf l_all_nil not_wf list_ind_cons_lemma list_ind_nil_lemma append_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt lambdaFormation_alt cut thin introduction extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality sqequalRule lambdaEquality_alt functionEquality hypothesis natural_numberEquality applyEquality because_Cache universeIsType setEquality setIsType independent_isectElimination setElimination rename productEquality applyLambdaEquality closedConclusion dependent_functionElimination unionElimination imageElimination productElimination voidElimination promote_hyp hypothesis_subsumption Error :memTop,  independent_functionElimination inhabitedIsType equalityElimination equalityTransitivity equalitySymmetry dependent_pairFormation_alt equalityIstype instantiate cumulativity functionIsType productIsType universeEquality isect_memberEquality_alt independent_pairFormation addEquality approximateComputation int_eqEquality imageMemberEquality baseClosed equalityIsType1 dependent_set_memberEquality_alt pointwiseFunctionality baseApply

Latex:
\mforall{}[T:Type]
\mforall{}P:T  {}\mrightarrow{}  \mBbbB{}.  \mforall{}L\$_{1}\$,L\$_{2}\$:T  List.
(0  <  ||L\$_{2}\$||
{}\mRightarrow{}  L\$_{2}\$  \mleq{}  filter(P;L\$_{1}\$)
{}\mRightarrow{}  (\mexists{}L\$_{3}\$:T  List.  (L\$_{3}\$  \mleq{}  L\$_{1}\mbackslash{}f\000Cf24  \mwedge{}  (L\$_{2}\$  =  filter(P;L\$_{3}\$))  \mwedge{}  0  <  ||L\$_{\000C3}\$||  \mwedge{}  (last(L\$_{2}\$)  =  last(L\$_{3}\$)))))

Date html generated: 2020_05_19-PM-09_42_41
Last ObjectModification: 2019_12_31-PM-00_12_27

Theory : list_1

Home Index