Nuprl Lemma : test-decide-normalize
∀[a,B:Top].
(case a of inl(_) => a + 1 | inr(y) => B[y] + a ~ case a of inl(x) => (inl x) + 1 | inr(y) => B[y] + (inr y ))
Proof
Definitions occuring in Statement :
uall: ∀[x:A]. B[x],
top: Top,
so_apply: x[s],
decide: case b of inl(x) => s[x] | inr(y) => t[y],
inr: inr x ,
inl: inl x,
add: n + m,
natural_number: $n,
sqequal: s ~ t
Definitions unfolded in proof :
top: Top,
member: t ∈ T,
all: ∀x:A. B[x],
implies: P ⇒ Q,
has-value: (a)↓,
uall: ∀[x:A]. B[x],
prop: ℙ
Lemmas referenced :
top_wf,
equal_wf,
has-value_wf_base,
is-exception_wf
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
cut,
sqequalTransitivity,
computationStep,
isect_memberEquality,
voidElimination,
voidEquality,
thin,
introduction,
extract_by_obid,
hypothesis,
lambdaFormation,
sqequalSqle,
divergentSqle,
callbyvalueDecide,
sqequalHypSubstitution,
hypothesisEquality,
unionEquality,
unionElimination,
sqleReflexivity,
isectElimination,
equalityTransitivity,
equalitySymmetry,
dependent_functionElimination,
independent_functionElimination,
decideExceptionCases,
axiomSqleEquality,
exceptionSqequal,
baseApply,
closedConclusion,
baseClosed,
isect_memberFormation,
sqequalAxiom,
because_Cache
Latex:
\mforall{}[a,B:Top].
(case a of inl($_{}$) => a + 1 | inr(y) => B[y] + a \msim{} case a
of inl(x) =>
(inl x) + 1
| inr(y) =>
B[y] + (inr y ))
Date html generated:
2017_04_14-AM-07_35_19
Last ObjectModification:
2017_02_27-PM-03_08_13
Theory : fun_1
Home
Index