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