Nuprl Lemma : is-list-if-has-value-ext
ListLike ≡ partial(Unit ⋃ (Top × ListLike))
Proof
Definitions occuring in Statement :
is-list-if-has-value: ListLike,
partial: partial(T),
b-union: A ⋃ B,
ext-eq: A ≡ B,
top: Top,
unit: Unit,
product: x:A × B[x]
Definitions unfolded in proof :
is-list-if-has-value: ListLike,
uall: ∀[x:A]. B[x],
so_lambda: λ2x.t[x],
member: t ∈ T,
so_apply: x[s],
uimplies: b supposing a,
continuous-monotone: ContinuousMonotone(T.F[T]),
and: P ∧ Q,
type-monotone: Monotone(T.F[T]),
subtype_rel: A ⊆r B,
top: Top,
all: ∀x:A. B[x],
strong-type-continuous: Continuous+(T.F[T]),
type-continuous: Continuous(T.F[T]),
guard: {T},
ext-eq: A ≡ B,
unit: Unit,
not: ¬A,
implies: P ⇒ Q,
false: False,
exists: ∃x:A. B[x],
nat: ℕ,
le: A ≤ B,
less_than': less_than'(a;b),
prop: ℙ,
uiff: uiff(P;Q)
Lemmas referenced :
corec-ext,
partial_wf,
b-union_wf,
unit_wf2,
top_wf,
subtype_rel_partial,
subtype_rel_b-union,
subtype_rel_self,
subtype_rel_product,
subtype_rel_wf,
subtype_rel_weakening,
nat_wf,
partial-type-continuous,
bunion-value-type,
equal-value-type,
product-value-type,
value-type_wf,
strong-continuous-b-union,
continuous-constant,
strong-continuous-product,
continuous-id,
unit-product-disjoint,
isect2_wf,
isect-value-type,
false_wf,
le_wf,
subtype_rel_transitivity,
subtype_rel_isect
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
cut,
lemma_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
sqequalRule,
lambdaEquality,
hypothesis,
productEquality,
hypothesisEquality,
universeEquality,
independent_isectElimination,
independent_pairFormation,
isect_memberFormation,
introduction,
because_Cache,
isect_memberEquality,
voidElimination,
voidEquality,
lambdaFormation,
axiomEquality,
equalityTransitivity,
equalitySymmetry,
isectEquality,
applyEquality,
functionEquality,
cumulativity,
productElimination,
independent_pairEquality,
intEquality,
natural_numberEquality,
dependent_set_memberEquality,
independent_functionElimination,
dependent_pairFormation
Latex:
ListLike \mequiv{} partial(Unit \mcup{} (Top \mtimes{} ListLike))
Date html generated:
2016_05_15-PM-10_08_22
Last ObjectModification:
2015_12_27-PM-06_00_21
Theory : eval!all
Home
Index