### Nuprl Lemma : decomp-map-if-has-value

`∀[t,f:Base].  if ispair(t) then t ~ <fst(t), snd(t)> else t ~ Ax fi  supposing (map(f;t))↓`

Proof

Definitions occuring in Statement :  map: `map(f;as)` has-value: `(a)↓` ifthenelse: `if b then t else f fi ` bfalse: `ff` btrue: `tt` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` pi1: `fst(t)` pi2: `snd(t)` ispair: `if z is a pair then a otherwise b` pair: `<a, b>` base: `Base` sqequal: `s ~ t` axiom: `Ax`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` map: `map(f;as)` list_ind: list_ind has-value: `(a)↓` prop: `ℙ` ifthenelse: `if b then t else f fi ` all: `∀x:A. B[x]` implies: `P `` Q` bool: `𝔹` or: `P ∨ Q` pi1: `fst(t)` pi2: `snd(t)` btrue: `tt` bfalse: `ff` not: `¬A` false: `False`
Lemmas referenced :  has-value-if-has-value-map ispair-bool-if-has-value has-value_wf_base base_wf equal_wf bool_wf has-value-implies-dec-ispair has-value-implies-dec-isaxiom bottom_diverge
Rules used in proof :  cut introduction extract_by_obid sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isectElimination thin hypothesisEquality independent_isectElimination hypothesis sqequalRule callbyvalueCallbyvalue callbyvalueReduce because_Cache sqequalIntensionalEquality baseApply closedConclusion baseClosed instantiate isect_memberFormation lambdaFormation unionElimination sqequalAxiom equalityTransitivity equalitySymmetry dependent_functionElimination independent_functionElimination isect_memberEquality voidElimination

Latex:
\mforall{}[t,f:Base].    if  ispair(t)  then  t  \msim{}  <fst(t),  snd(t)>  else  t  \msim{}  Ax  fi    supposing  (map(f;t))\mdownarrow{}

Date html generated: 2018_05_21-PM-10_19_16
Last ObjectModification: 2017_07_26-PM-06_36_54

Theory : eval!all

Home Index