### Nuprl Lemma : list_ind_reverse_unfold

`∀[A,B:Type].`
`  ∀nilcase:B. ∀F:B ⟶ (A List) ⟶ A ⟶ B. ∀L:A List.`
`    ((||L|| > 0)`
`    `` (list_ind_reverse(L;nilcase;F) ~ F list_ind_reverse(firstn(||L|| - 1;L);nilcase;F) firstn(||L|| - 1;L) last(L)))`

Proof

Definitions occuring in Statement :  list_ind_reverse: `list_ind_reverse(L;nilcase;R)` firstn: `firstn(n;as)` last: `last(L)` length: `||as||` list: `T List` uall: `∀[x:A]. B[x]` gt: `i > j` all: `∀x:A. B[x]` implies: `P `` Q` apply: `f a` function: `x:A ⟶ B[x]` subtract: `n - m` natural_number: `\$n` universe: `Type` sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` implies: `P `` Q` list_ind_reverse: `list_ind_reverse(L;nilcase;R)` prop: `ℙ` gt: `i > j` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` ifthenelse: `if b then t else f fi ` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` not: `¬A` top: `Top` bfalse: `ff` or: `P ∨ Q` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb` assert: `↑b`
Lemmas referenced :  gt_wf length_wf list_wf eq_int_wf bool_wf eqtt_to_assert assert_of_eq_int satisfiable-full-omega-tt intformand_wf intformeq_wf itermVar_wf itermConstant_wf intformless_wf int_formula_prop_and_lemma int_formula_prop_eq_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_less_lemma int_formula_prop_wf eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_int
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation sqequalRule hypothesis extract_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality natural_numberEquality functionEquality lambdaEquality dependent_functionElimination sqequalAxiom because_Cache universeEquality isect_memberEquality unionElimination equalityElimination equalityTransitivity equalitySymmetry productElimination independent_isectElimination dependent_pairFormation int_eqEquality intEquality voidElimination voidEquality independent_pairFormation computeAll promote_hyp instantiate independent_functionElimination

Latex:
\mforall{}[A,B:Type].
\mforall{}nilcase:B.  \mforall{}F:B  {}\mrightarrow{}  (A  List)  {}\mrightarrow{}  A  {}\mrightarrow{}  B.  \mforall{}L:A  List.
((||L||  >  0)
{}\mRightarrow{}  (list\_ind\_reverse(L;nilcase;F)  \msim{}  F  list\_ind\_reverse(firstn(||L||  -  1;L);nilcase;F)
firstn(||L||  -  1;L)
last(L)))

Date html generated: 2017_04_17-AM-08_44_17
Last ObjectModification: 2017_02_27-PM-05_01_25

Theory : list_1

Home Index