Nuprl Lemma : fixpoint-induction-bottom-base
∀E,S:Type. ∀G,g:Base.
((G ∈ S ⟶ partial(E)) ⇒ (g ∈ S ⟶ S) ⇒ value-type(E) ⇒ mono(E) ⇒ (⊥ ∈ S) ⇒ (G fix(g) ∈ partial(E)))
Proof
Definitions occuring in Statement :
partial: partial(T),
mono: mono(T),
value-type: value-type(T),
bottom: ⊥,
all: ∀x:A. B[x],
implies: P ⇒ Q,
member: t ∈ T,
apply: f a,
fix: fix(F),
function: x:A ⟶ B[x],
base: Base,
universe: Type
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
member: t ∈ T,
prop: ℙ,
uall: ∀[x:A]. B[x],
uimplies: b supposing a,
not: ¬A,
false: False,
subtype_rel: A ⊆r B,
nat: ℕ,
so_lambda: λ2x.t[x],
so_apply: x[s],
mono: mono(T),
is-above: is-above(T;a;z),
exists: ∃x:A. B[x],
and: P ∧ Q,
cand: A c∧ B,
top: Top
Lemmas referenced :
mono_wf,
value-type_wf,
base_wf,
partial_wf,
equal-wf-base,
base-member-partial,
fix-not-exception,
partial-not-exception,
fun_exp_wf,
is-exception_wf,
set_subtype_base,
le_wf,
int_subtype_base,
nat_wf,
has-value_wf_base,
termination,
fixpoint-upper-bound,
equal-wf-base-T,
sqle_wf_base
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
sqequalHypSubstitution,
hypothesis,
introduction,
extract_by_obid,
isectElimination,
thin,
hypothesisEquality,
universeEquality,
baseClosed,
functionEquality,
independent_isectElimination,
sqequalRule,
baseApply,
closedConclusion,
applyEquality,
independent_functionElimination,
voidElimination,
intEquality,
lambdaEquality,
natural_numberEquality,
because_Cache,
Error :isect_memberFormation_alt,
axiomEquality,
equalityTransitivity,
equalitySymmetry,
Error :universeIsType,
compactness,
dependent_functionElimination,
dependent_pairFormation,
independent_pairFormation,
sqleRule,
divergentSqle,
sqleReflexivity,
isect_memberEquality,
voidEquality,
productEquality
Latex:
\mforall{}E,S:Type. \mforall{}G,g:Base.
((G \mmember{} S {}\mrightarrow{} partial(E))
{}\mRightarrow{} (g \mmember{} S {}\mrightarrow{} S)
{}\mRightarrow{} value-type(E)
{}\mRightarrow{} mono(E)
{}\mRightarrow{} (\mbot{} \mmember{} S)
{}\mRightarrow{} (G fix(g) \mmember{} partial(E)))
Date html generated:
2019_06_20-PM-00_34_04
Last ObjectModification:
2018_09_26-PM-01_13_26
Theory : partial_1
Home
Index