### 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