Nuprl Lemma : function-not-int
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[f:a:A ⟶ B[a]]. (isint(f) ~ ff) supposing ↓∃a:A. value-type(B[a])
Proof
Definitions occuring in Statement :
value-type: value-type(T),
bfalse: ff,
btrue: tt,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
so_apply: x[s],
isint: isint def,
exists: ∃x:A. B[x],
squash: ↓T,
function: x:A ⟶ B[x],
universe: Type,
sqequal: s ~ t
Definitions unfolded in proof :
so_lambda: λ2x.t[x],
prop: ℙ,
guard: {T},
implies: P ⇒ Q,
all: ∀x:A. B[x],
sq_type: SQType(T),
has-value: (a)↓,
so_apply: x[s],
exists: ∃x:A. B[x],
squash: ↓T,
uimplies: b supposing a,
member: t ∈ T,
uall: ∀[x:A]. B[x],
or: P ∨ Q,
top: Top,
false: False,
not: ¬A
Lemmas referenced :
value-type_wf,
exists_wf,
squash_wf,
bottom_diverge,
value-type-has-value,
bool_subtype_base,
bool_wf,
subtype_base_sq,
bfalse_wf,
has-value-implies-dec-isint,
bottom-sqle,
equal_wf,
equal-wf-base
Rules used in proof :
universeEquality,
lambdaEquality,
because_Cache,
isect_memberEquality,
sqequalRule,
functionEquality,
axiomSqEquality,
independent_functionElimination,
equalitySymmetry,
equalityTransitivity,
dependent_functionElimination,
callbyvalueApply,
hypothesisEquality,
applyEquality,
productElimination,
imageElimination,
independent_isectElimination,
hypothesis,
cumulativity,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
instantiate,
thin,
cut,
introduction,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
pointwiseFunctionality,
unionElimination,
baseClosed,
voidEquality,
voidElimination,
sqequalSqle,
applyInt,
lambdaFormation
Latex:
\mforall{}[A:Type]. \mforall{}[B:A {}\mrightarrow{} Type]. \mforall{}[f:a:A {}\mrightarrow{} B[a]]. (isint(f) \msim{} ff) supposing \mdownarrow{}\mexists{}a:A. value-type(B[a])
Date html generated:
2019_06_20-AM-11_21_35
Last ObjectModification:
2018_10_16-PM-02_56_26
Theory : call!by!value_1
Home
Index