### 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: `b supposing a` uall: `∀[x:A]. B[x]` prop: `ℙ` and: `P ∧ Q` 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` and: `P ∧ Q` uimplies: `b supposing a` all: `∀x:A. B[x]` implies: `P `` Q` subtype_rel: `A ⊆r B` guard: `{T}` so_lambda: `λ2x.t[x]` so_apply: `x[s]` top: `Top` pi2: `snd(t)` pi1: `fst(t)` cand: `A c∧ B` squash: `↓T` prop: `ℙ` iff: `P `⇐⇒` Q` has-value: `(a)↓` nat: `ℕ` false: `False` ge: `i ≥ j ` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` decidable: `Dec(P)` or: `P ∨ Q` true: `True` rev_implies: `P `` 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