### Nuprl Lemma : not-has-value-decidable-quot

`∀[E:(∀x:Base. ((x)↓ ∨ (¬(x)↓))) ⟶ (∀x:Base. ((x)↓ ∨ (¬(x)↓))) ⟶ ℙ]`
`  ¬(f,g:∀x:Base. ((x)↓ ∨ (¬(x)↓))//E[f;g]) supposing EquivRel(∀x:Base. ((x)↓ ∨ (¬(x)↓));f,g.E[f;g])`

Proof

Definitions occuring in Statement :  equiv_rel: `EquivRel(T;x,y.E[x; y])` quotient: `x,y:A//B[x; y]` has-value: `(a)↓` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` not: `¬A` or: `P ∨ Q` function: `x:A ⟶ B[x]` base: `Base`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` not: `¬A` implies: `P `` Q` false: `False` so_lambda: `λ2x.t[x]` so_apply: `x[s]` or: `P ∨ Q` all: `∀x:A. B[x]` prop: `ℙ` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` quotient: `x,y:A//B[x; y]` and: `P ∧ Q` subtype_rel: `A ⊆r B`
Lemmas referenced :  quotient_wf all_wf base_wf or_wf has-value_wf_base not_wf equiv_rel_wf false_wf equal_wf equal-wf-base not_has-value_decidable_on_base
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation thin rename because_Cache hypothesis sqequalHypSubstitution independent_functionElimination voidElimination lemma_by_obid isectElimination sqequalRule lambdaEquality hypothesisEquality applyEquality independent_isectElimination dependent_functionElimination isect_memberEquality equalityTransitivity equalitySymmetry functionEquality cumulativity universeEquality pointwiseFunctionalityForEquality pertypeElimination productElimination productEquality

Latex:
\mforall{}[E:(\mforall{}x:Base.  ((x)\mdownarrow{}  \mvee{}  (\mneg{}(x)\mdownarrow{})))  {}\mrightarrow{}  (\mforall{}x:Base.  ((x)\mdownarrow{}  \mvee{}  (\mneg{}(x)\mdownarrow{})))  {}\mrightarrow{}  \mBbbP{}]
\mneg{}(f,g:\mforall{}x:Base.  ((x)\mdownarrow{}  \mvee{}  (\mneg{}(x)\mdownarrow{}))//E[f;g])  supposing  EquivRel(\mforall{}x:Base.  ((x)\mdownarrow{}  \mvee{}  (\mneg{}(x)\mdownarrow{}));f,g.E[f;g])

Date html generated: 2016_05_14-AM-06_08_32
Last ObjectModification: 2015_12_26-AM-11_48_21

Theory : quot_1

Home Index