### Nuprl Lemma : list_decomp_rev_wf

`∀[T:Type]. ∀[l:T List].  list_decomp_rev{i:l}(l) ∈ {p:T × (T List)| l = ((snd(p)) @ [fst(p)]) ∈ (T List)}  supposing 0 <\000C ||l||`

Proof

Definitions occuring in Statement :  list_decomp_rev: `list_decomp_rev{i:l}(l)` length: `||as||` append: `as @ bs` cons: `[a / b]` nil: `[]` list: `T List` less_than: `a < b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` pi1: `fst(t)` pi2: `snd(t)` member: `t ∈ T` set: `{x:A| B[x]} ` product: `x:A × B[x]` natural_number: `\$n` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` list_decomp_rev: `list_decomp_rev{i:l}(l)` so_lambda: `λ2x.t[x]` prop: `ℙ` so_apply: `x[s]` subtype_rel: `A ⊆r B` all: `∀x:A. B[x]` implies: `P `` Q` exists: `∃x:A. B[x]` pi2: `snd(t)` pi1: `fst(t)` and: `P ∧ Q` squash: `↓T` true: `True`
Lemmas referenced :  list_decomp_reverse uall_wf all_wf list_wf isect_wf less_than_wf length_wf exists_wf equal_wf append_wf cons_wf nil_wf uimplies_subtype and_wf squash_wf true_wf pi2_wf pi1_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut thin instantiate extract_by_obid hypothesis sqequalHypSubstitution isectElimination universeEquality sqequalRule lambdaEquality cumulativity hypothesisEquality natural_numberEquality because_Cache applyEquality lambdaFormation equalityTransitivity equalitySymmetry isectEquality functionEquality independent_isectElimination productElimination dependent_set_memberEquality independent_pairFormation applyLambdaEquality setElimination rename imageElimination imageMemberEquality baseClosed independent_pairEquality dependent_functionElimination independent_functionElimination axiomEquality isect_memberEquality

Latex:
\mforall{}[T:Type].  \mforall{}[l:T  List].    list\_decomp\_rev\{i:l\}(l)  \mmember{}  \{p:T  \mtimes{}  (T  List)|  l  =  ((snd(p))  @  [fst(p)])\}    supp\000Cosing  0  <  ||l||

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

Theory : list_1

Home Index