Nuprl Lemma : has-value-equality-fix-bar

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


Proof




Definitions occuring in Statement :  bar: bar(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 :  uall: [x:A]. B[x] member: t ∈ T and: P ∧ Q uimplies: supposing a all: x:A. B[x] implies:  Q subtype_rel: A ⊆B guard: {T} so_lambda: λ2x.t[x] so_apply: x[s] top: Top pi2: snd(t) pi1: fst(t) cand: c∧ B squash: T prop: iff: ⇐⇒ Q has-value: (a)↓ nat: false: False ge: i ≥  not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] decidable: Dec(P) or: P ∨ Q true: True rev_implies:  Q
Lemmas referenced :  istype-universe bar_wf value-type_wf pair-eta subtype_rel_product top_wf istype-top istype-void has-value_wf_base pi1_wf_top member_wf has-value-extensionality nat_properties full-omega-unsat intformand_wf intformle_wf itermConstant_wf itermVar_wf intformless_wf istype-int int_formula_prop_and_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf ge_wf less_than_wf fun_exp0_lemma subtract-1-ge-0 equal_wf fun_exp_wf squash_wf true_wf nat_wf decidable__equal_int intformnot_wf intformeq_wf int_formula_prop_not_lemma int_formula_prop_eq_lemma decidable__le le_wf iff_weakening_equal has-value_wf-bar is-exception_wf fixpoint-upper-bound has-value-monotonic set_subtype_base int_subtype_base
Rules used in proof :  functionIsType cut introduction extract_by_obid sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isectElimination thin hypothesisEquality hypothesis inhabitedIsType universeIsType sqequalRule productIsType equalityIsType4 baseClosed because_Cache universeEquality isect_memberFormation_alt axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality_alt independent_pairEquality lambdaFormation_alt pointwiseFunctionality productElimination applyEquality functionEquality lambdaEquality_alt closedConclusion independent_isectElimination voidElimination baseApply applyLambdaEquality independent_pairFormation instantiate imageElimination compactness setElimination rename intWeakElimination natural_numberEquality approximateComputation independent_functionElimination dependent_pairFormation_alt int_eqEquality dependent_functionElimination functionIsTypeImplies unionElimination dependent_set_memberEquality_alt imageMemberEquality axiomSqleEquality equalityIsType1 hyp_replacement sqleRule divergentSqle sqleReflexivity intEquality

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



Date html generated: 2019_10_16-AM-11_37_45
Last ObjectModification: 2018_10_11-PM-11_40_03

Theory : bar!type


Home Index