Nuprl Lemma : decidable__q-rel
∀r:ℤ. ∀x:ℚ. Dec(q-rel(r;x))
Proof
Definitions occuring in Statement :
q-rel: q-rel(r;x),
rationals: ℚ,
decidable: Dec(P),
all: ∀x:A. B[x],
int: ℤ
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T
Lemmas referenced :
rationals_wf,
q-rel-decider_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
lemma_by_obid,
hypothesis,
intEquality,
introduction,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
hypothesisEquality
Latex:
\mforall{}r:\mBbbZ{}. \mforall{}x:\mBbbQ{}. Dec(q-rel(r;x))
Date html generated:
2016_05_15-PM-11_18_01
Last ObjectModification:
2015_12_27-PM-07_35_01
Theory : rationals
Home
Index