Nuprl Lemma : has-value-equality-fix

[T,E,S:Type].  ∀[G:T ⟶ partial(E)]. ∀[g:T ⟶ T].  ((G fix(g))↓ ∈ ℙsupposing value-type(E) ∧ (⊥ ∈ T)


Proof




Definitions occuring in Statement :  partial: partial(T) value-type: value-type(T) has-value: (a)↓ bottom: uimplies: supposing a uall: [x:A]. B[x] prop: and: P ∧ Q member: t ∈ T apply: a fix: fix(F) function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  member: t ∈ T all: x:A. B[x] implies:  Q uall: [x:A]. B[x] and: P ∧ Q subtype_rel: A ⊆B guard: {T} so_lambda: λ2x.t[x] so_apply: x[s] uimplies: supposing a top: Top pi2: snd(t) pi1: fst(t) cand: c∧ B squash: T prop: true: True iff: ⇐⇒ Q has-value: (a)↓ nat: rev_implies:  Q
Lemmas referenced :  pair-eta subtype_rel_product partial_wf top_wf istype-top istype-void has-value_wf_base member_wf istype-universe value-type_wf has-value-extensionality fun_exp0_lemma equal_wf squash_wf true_wf fun_exp_wf nat_wf le_weakening2 le_wf subtype_rel_self iff_weakening_equal int_subtype_base istype-int less_than_wf primrec-wf2 equal-wf-base has-value_wf-partial is-exception_wf fixpoint-upper-bound has-value-monotonic set_subtype_base
Rules used in proof :  cut sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity independent_pairEquality hypothesisEquality Error :inhabitedIsType,  hypothesis Error :lambdaFormation_alt,  thin pointwiseFunctionality sqequalRule introduction extract_by_obid sqequalHypSubstitution isectElimination productElimination equalityTransitivity equalitySymmetry applyEquality functionEquality Error :lambdaEquality_alt,  because_Cache Error :functionIsType,  Error :universeIsType,  independent_isectElimination Error :isect_memberEquality_alt,  voidElimination baseApply closedConclusion baseClosed applyLambdaEquality independent_pairFormation instantiate imageElimination universeEquality natural_numberEquality imageMemberEquality Error :equalityIsType1,  dependent_functionElimination independent_functionElimination Error :productIsType,  Error :equalityIsType4,  Error :isect_memberFormation_alt,  axiomEquality compactness rename setElimination Error :dependent_set_memberEquality_alt,  Error :setIsType,  axiomSqleEquality hyp_replacement sqleRule divergentSqle sqleReflexivity intEquality

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



Date html generated: 2019_06_20-PM-00_34_02
Last ObjectModification: 2018_10_07-PM-09_32_01

Theory : partial_1


Home Index