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

`∀t:ListLike`
`  ((t)↓`
`  `` (((↑isaxiom(t)) ∧ (t = Ax ∈ Unit)) ∨ ((↑ispair(t)) ∧ (∃a:Top. ∃b:ListLike. (t = <a, b> ∈ (Top × ListLike))))))`

Proof

Definitions occuring in Statement :  is-list-if-has-value: `ListLike` has-value: `(a)↓` assert: `↑b` bfalse: `ff` btrue: `tt` top: `Top` ispair: `if z is a pair then a otherwise b` isaxiom: `if z = Ax then a otherwise b` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` or: `P ∨ Q` and: `P ∧ Q` unit: `Unit` pair: `<a, b>` product: `x:A × B[x]` equal: `s = t ∈ T` axiom: `Ax`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` uall: `∀[x:A]. B[x]` prop: `ℙ` b-union: `A ⋃ B` tunion: `⋃x:A.B[x]` bool: `𝔹` unit: `Unit` ifthenelse: `if b then t else f fi ` pi2: `snd(t)` or: `P ∨ Q` assert: `↑b` btrue: `tt` and: `P ∧ Q` true: `True` exists: `∃x:A. B[x]` bfalse: `ff` false: `False` subtype_rel: `A ⊆r B` so_apply: `x[s]` so_lambda: `λ2x.t[x]` uimplies: `b supposing a` ext-eq: `A ≡ B`
Lemmas referenced :  is-list-if-has-value-hv-prp is-list-if-has-value_wf istype-assert istype-top istype-void product-value-type equal-value-type bunion-value-type top_wf unit_wf2 b-union_wf termination is-list-if-has-value-ext bfalse_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt universeIsType cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis inhabitedIsType imageElimination productElimination unionElimination equalityElimination sqequalRule inlEquality_alt closedConclusion independent_pairEquality axiomEquality natural_numberEquality productIsType equalityIsType2 because_Cache baseClosed inrEquality_alt dependent_pairEquality_alt equalityIsType1 voidElimination equalityTransitivity equalitySymmetry dependent_functionElimination independent_functionElimination applyEquality lambdaEquality_alt intEquality independent_isectElimination productEquality

Latex:
\mforall{}t:ListLike
((t)\mdownarrow{}  {}\mRightarrow{}  (((\muparrow{}isaxiom(t))  \mwedge{}  (t  =  Ax))  \mvee{}  ((\muparrow{}ispair(t))  \mwedge{}  (\mexists{}a:Top.  \mexists{}b:ListLike.  (t  =  <a,  b>)))))

Date html generated: 2019_10_16-AM-11_38_04
Last ObjectModification: 2018_10_31-PM-02_27_33

Theory : eval!all

Home Index