### Nuprl Lemma : fixpoint-induction-bottom

`∀[E,S:Type].`
`  (∀[G:S ⟶ partial(E)]. ∀[g:S ⟶ S].  (G fix(g) ∈ partial(E))) supposing ((⊥ ∈ S) and mono(E) and value-type(E))`

Proof

Definitions occuring in Statement :  partial: `partial(T)` mono: `mono(T)` value-type: `value-type(T)` bottom: `⊥` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` member: `t ∈ T` apply: `f a` fix: `fix(F)` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` prop: `ℙ` all: `∀x:A. B[x]` implies: `P `` Q` so_lambda: `λ2x.t[x]` so_apply: `x[s]` and: `P ∧ Q` cand: `A c∧ B` top: `Top` guard: `{T}` subtype_rel: `A ⊆r B` squash: `↓T` true: `True` iff: `P `⇐⇒` Q` sq_stable: `SqStable(P)` rev_implies: `P `` Q` nat: `ℕ` mono: `mono(T)` is-above: `is-above(T;a;z)` exists: `∃x:A. B[x]` false: `False` not: `¬A`
Lemmas referenced :  partial_wf equal-wf-base mono_wf value-type_wf pi2_wf pi1_wf equal_wf fixpoint-induction-bottom-base top_wf subtype_rel_product pair-eta member_wf base-equal-partial sq_stable__has-value has-value_wf_base has-value_wf-partial fun_exp_wf is-exception_wf fixpoint_ub has-value-monotonic set_subtype_base le_wf int_subtype_base and_wf termination fixpoint-upper-bound equal-wf-base-T sqle_wf_base termination-equality-base nat_wf partial-not-exception fix-not-exception
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut sqequalHypSubstitution hypothesis sqequalRule axiomEquality equalityTransitivity equalitySymmetry Error :functionIsType,  Error :inhabitedIsType,  hypothesisEquality isect_memberEquality isectElimination thin functionEquality Error :universeIsType,  extract_by_obid because_Cache baseClosed universeEquality independent_pairEquality productEquality lambdaFormation pointwiseFunctionality applyLambdaEquality lambdaEquality independent_pairFormation productElimination dependent_functionElimination independent_functionElimination closedConclusion baseApply voidEquality voidElimination independent_isectElimination cumulativity applyEquality imageElimination natural_numberEquality imageMemberEquality compactness hyp_replacement sqleRule divergentSqle sqleReflexivity intEquality dependent_set_memberEquality setElimination rename dependent_pairFormation

Latex:
\mforall{}[E,S:Type].
(\mforall{}[G:S  {}\mrightarrow{}  partial(E)].  \mforall{}[g:S  {}\mrightarrow{}  S].    (G  fix(g)  \mmember{}  partial(E)))  supposing
((\mbot{}  \mmember{}  S)  and
mono(E)  and
value-type(E))

Date html generated: 2019_06_20-PM-00_34_08
Last ObjectModification: 2018_09_26-PM-01_21_20

Theory : partial_1

Home Index