Nuprl Lemma : test3-cform-normalize
∀[a,B:Top].
(if a is inl then <B[if a is inl then 1
else 2]
, B[if a = Ax then 3 otherwise if a is a pair then 3
otherwise if a is an integer then 3
else if a is an atom then 3
otherwise isatom1(a;3;isatom2(a;3;4))]
>
else B[if a is inl then 1
else 2] ~ if a is inl then <B[1], B[4]>
else B[2])
Proof
Definitions occuring in Statement :
uall: ∀[x:A]. B[x],
top: Top,
so_apply: x[s],
isatom1: isatom1(z;a;b),
isatom2: isatom2(z;a;b),
isatom: if z is an atom then a otherwise b,
ispair: if z is a pair then a otherwise b,
isaxiom: if z = Ax then a otherwise b,
isinl: isinl def,
isint: isint def,
pair: <a, b>,
natural_number: $n,
sqequal: s ~ t
Definitions unfolded in proof :
has-value: (a)↓,
all: ∀x:A. B[x],
member: t ∈ T,
implies: P ⇒ Q,
or: P ∨ Q,
uall: ∀[x:A]. B[x],
top: Top
Lemmas referenced :
top_wf,
is-exception_wf,
has-value_wf_base,
has-value-implies-dec-isinl-2
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
cut,
sqequalSqle,
divergentSqle,
callbyvalueIsinl,
sqequalHypSubstitution,
sqequalTransitivity,
computationStep,
hypothesis,
lemma_by_obid,
dependent_functionElimination,
thin,
hypothesisEquality,
independent_functionElimination,
unionElimination,
sqleReflexivity,
isectElimination,
baseApply,
closedConclusion,
baseClosed,
lambdaFormation,
isect_memberEquality,
voidElimination,
voidEquality,
because_Cache,
introduction,
isinlExceptionCases,
axiomSqleEquality,
exceptionSqequal,
isect_memberFormation,
sqequalAxiom
Latex:
\mforall{}[a,B:Top].
(if a is inl then <B[if a is inl then 1
else 2]
, B[if a = Ax then 3
otherwise if a is a pair then 3
otherwise if a is an integer then 3
else if a is an atom then 3
otherwise isatom1(a;3;isatom2(a;3;4))]
>
else B[if a is inl then 1
else 2] \msim{} if a is inl then <B[1], B[4]>
else B[2])
Date html generated:
2016_05_13-PM-04_08_11
Last ObjectModification:
2016_01_14-PM-07_46_28
Theory : fun_1
Home
Index