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

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


Definitions occuring in Statement :  is-list-if-has-value-rec: is-list-if-has-value-rec(t) has-value: (a)↓ ifthenelse: if then else fi  bfalse: ff btrue: tt uimplies: supposing a uall: [x:A]. B[x] pi1: fst(t) pi2: snd(t) ispair: if is pair then otherwise b pair: <a, b> base: Base sqequal: t axiom: Ax
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: 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:  Q prop: all: x:A. B[x] top: Top or: P ∨ Q has-value: (a)↓ pi1: fst(t) pi2: snd(t) ifthenelse: if then else 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

    (if  ispair(t)  then  t  \msim{}  <fst(t),  snd(t)>  else  t  \msim{}  Ax  fi  )  supposing 
          ((t)\mdownarrow{}  and 

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

Theory : eval!all

Home Index