### Nuprl Lemma : list_ind_reverse_unfold1

`∀[A,B:Type].`
`  ∀nilcase:B. ∀F:B ⟶ (A List) ⟶ A ⟶ B. ∀L:A List.`
`    (list_ind_reverse(L;nilcase;F) ~ if (||L|| =z 0)`
`    then nilcase`
`    else F list_ind_reverse(firstn(||L|| - 1;L);nilcase;F) firstn(||L|| - 1;L) last(L)`
`    fi )`

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` ifthenelse: `if b then t else f fi ` eq_int: `(i =z j)` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` 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]` list_ind_reverse: `list_ind_reverse(L;nilcase;R)`
Lemmas referenced :  list_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation sqequalRule hypothesis lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality functionEquality lambdaEquality dependent_functionElimination sqequalAxiom because_Cache universeEquality isect_memberEquality

Latex:
\mforall{}[A,B:Type].
\mforall{}nilcase:B.  \mforall{}F:B  {}\mrightarrow{}  (A  List)  {}\mrightarrow{}  A  {}\mrightarrow{}  B.  \mforall{}L:A  List.
(list\_ind\_reverse(L;nilcase;F)  \msim{}  if  (||L||  =\msubz{}  0)
then  nilcase
else  F  list\_ind\_reverse(firstn(||L||  -  1;L);nilcase;F)  firstn(||L||  -  1;L)  last(L)
fi  )

Date html generated: 2016_05_14-PM-02_59_55
Last ObjectModification: 2015_12_26-PM-01_58_35

Theory : list_1

Home Index