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: supposing a uall: [x:A]. B[x] member: t ∈ T apply: a fix: fix(F) function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a prop: all: x:A. B[x] implies:  Q so_lambda: λ2x.t[x] so_apply: x[s] and: P ∧ Q cand: c∧ B top: Top guard: {T} subtype_rel: A ⊆B squash: T true: True iff: ⇐⇒ Q sq_stable: SqStable(P) rev_implies:  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