Nuprl Lemma : rec-value-ext
rec-value() ≡ atomic-values() ⋃ (rec-value() × rec-value()) ⋃ (rec-value() + rec-value())
Proof
Definitions occuring in Statement :
rec-value: rec-value(),
atomic-values: atomic-values(),
b-union: A ⋃ B,
ext-eq: A ≡ B,
product: x:A × B[x],
union: left + right
Definitions unfolded in proof :
ext-eq: A ≡ B,
and: P ∧ Q,
subtype_rel: A ⊆r B,
member: t ∈ T,
uall: ∀[x:A]. B[x],
rec-value: rec-value(),
guard: {T},
uimplies: b supposing a,
b-union: A ⋃ B,
tunion: ⋃x:A.B[x],
bool: 𝔹,
unit: Unit,
ifthenelse: if b then t else f fi ,
pi2: snd(t),
btrue: tt,
bfalse: ff,
co-value-height: co-value-height(t),
has-value: (a)↓,
all: ∀x:A. B[x],
implies: P ⇒ Q,
nat: ℕ,
so_lambda: λ2x.t[x],
so_apply: x[s],
prop: ℙ,
outl: outl(x),
outr: outr(x),
atomic-values: atomic-values(),
rec-value-height: rec-value-height(v),
Value: Value(),
top: Top,
is-atomic: is-atomic(x),
assert: ↑b,
false: False
Lemmas referenced :
top_wf,
is-exception_wf,
has-value_wf_base,
rec-value-height_wf,
subtype_rel_union,
subtype_rel_product,
subtype_rel_self,
subtype_rel_b-union,
set-value-type,
has-value_wf-partial,
int-value-type,
value-type-has-value,
int_subtype_base,
le_wf,
set_subtype_base,
nat_wf,
subtype_partial_sqtype_base,
co-value-height_wf,
add-wf-partial-nat,
bfalse_wf,
ifthenelse_wf,
btrue_wf,
subtype_rel_weakening,
co-value_wf,
ext-eq_inversion,
co-value-ext,
atomic-values_wf,
b-union_wf,
rec-value_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
independent_pairFormation,
lambdaEquality,
cut,
lemma_by_obid,
hypothesis,
sqequalHypSubstitution,
isectElimination,
thin,
productEquality,
unionEquality,
setElimination,
rename,
hypothesis_subsumption,
independent_isectElimination,
hypothesisEquality,
applyEquality,
sqequalRule,
imageElimination,
productElimination,
unionElimination,
equalityElimination,
imageMemberEquality,
dependent_pairEquality,
instantiate,
universeEquality,
baseClosed,
equalityTransitivity,
equalitySymmetry,
because_Cache,
independent_pairEquality,
dependent_set_memberEquality,
callbyvalueAdd,
dependent_functionElimination,
independent_functionElimination,
intEquality,
natural_numberEquality,
inlEquality,
inrEquality,
lambdaFormation,
introduction,
axiomSqleEquality,
addEquality,
ispairCases,
divergentSqle,
isect_memberFormation,
sqequalAxiom,
isect_memberEquality,
voidElimination,
voidEquality,
isinlCases,
isinrCases,
sqleReflexivity
Latex:
rec-value() \mequiv{} atomic-values() \mcup{} (rec-value() \mtimes{} rec-value()) \mcup{} (rec-value() + rec-value())
Date html generated:
2016_05_14-PM-03_20_59
Last ObjectModification:
2016_01_14-PM-08_01_05
Theory : rec_values
Home
Index