Nuprl Lemma : co-value-ext
co-value() ≡ atomic-values() ⋃ (co-value() × co-value()) ⋃ (co-value() + co-value())
Proof
Definitions occuring in Statement :
co-value: co-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 :
co-value: co-value(),
uall: ∀[x:A]. B[x],
so_lambda: λ2x.t[x],
member: t ∈ T,
so_apply: x[s],
uimplies: b supposing a
Lemmas referenced :
corec-ext,
b-union_wf,
atomic-values_wf,
continuous-monotone-co-value
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
cut,
lemma_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
sqequalRule,
lambdaEquality,
hypothesis,
productEquality,
hypothesisEquality,
unionEquality,
universeEquality,
independent_isectElimination
Latex:
co-value() \mequiv{} atomic-values() \mcup{} (co-value() \mtimes{} co-value()) \mcup{} (co-value() + co-value())
Date html generated:
2016_05_14-PM-03_20_44
Last ObjectModification:
2015_12_26-PM-02_27_01
Theory : rec_values
Home
Index