### Nuprl Lemma : is-list-if-has-value-rec-decomp

`∀[t:Base]. (if ispair(t) then t ~ <fst(t), snd(t)> else t ~ Ax fi ) supposing ((t)↓ and is-list-if-has-value-rec(t))`

Proof

Definitions occuring in Statement :  is-list-if-has-value-rec: `is-list-if-has-value-rec(t)` 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` is-list-if-has-value-rec: `is-list-if-has-value-rec(t)` is-list-if-has-value-fun: `is-list-if-has-value-fun(t;n)` nat: `ℕ` le: `A ≤ B` and: `P ∧ Q` less_than': `less_than'(a;b)` false: `False` not: `¬A` implies: `P `` Q` prop: `ℙ` all: `∀x:A. B[x]` top: `Top` or: `P ∨ Q` has-value: `(a)↓` pi1: `fst(t)` pi2: `snd(t)` ifthenelse: `if b then t else f fi ` btrue: `tt` bfalse: `ff` bool: `𝔹` assert: `↑b` exposed-it: `exposed-it` unit: `Unit` it: `⋅` uiff: `uiff(P;Q)` sq_type: `SQType(T)` guard: `{T}` exists: `∃x:A. B[x]` bnot: `¬bb`
Lemmas referenced :  false_wf le_wf primrec1_lemma has-value-implies-dec-ispair-2 top_wf ispair-bool-if-has-value equal_wf has-value_wf_base is-list-if-has-value-rec_wf bool_wf base_wf has-value-implies-dec-isaxiom-2 btrue_wf eqtt_to_assert subtype_base_sq subtype_rel_self isaxiom-implies eqff_to_assert bool_cases_sqequal bool_subtype_base
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution sqequalRule isectElimination thin dependent_set_memberEquality natural_numberEquality independent_pairFormation lambdaFormation hypothesis extract_by_obid hypothesisEquality dependent_functionElimination isect_memberEquality voidElimination voidEquality independent_isectElimination independent_functionElimination unionElimination because_Cache sqequalAxiom sqequalIntensionalEquality baseApply closedConclusion baseClosed equalityTransitivity equalitySymmetry instantiate equalityElimination productElimination cumulativity dependent_pairFormation promote_hyp

Latex:
\mforall{}[t:Base]
(if  ispair(t)  then  t  \msim{}  <fst(t),  snd(t)>  else  t  \msim{}  Ax  fi  )  supposing
((t)\mdownarrow{}  and
is-list-if-has-value-rec(t))

Date html generated: 2018_05_21-PM-10_19_30
Last ObjectModification: 2017_07_26-PM-06_37_02

Theory : eval!all

Home Index