Nuprl Lemma : decidable__q-constraints-squash
∀k:ℕ. ∀A:(ℕ ⟶ ℚ × ℤ) List. Dec(∃y:{ℚ List| q-constraints(k;A;y)})
Proof
Definitions occuring in Statement :
q-constraints: q-constraints(k;A;y),
rationals: ℚ,
list: T List,
nat: ℕ,
decidable: Dec(P),
all: ∀x:A. B[x],
sq_exists: ∃x:{A| B[x]},
function: x:A ⟶ B[x],
product: x:A × B[x],
int: ℤ
Lemmas referenced :
decidable__q-constraints
Rules used in proof :
cut,
lemma_by_obid,
hypothesis
Latex:
\mforall{}k:\mBbbN{}. \mforall{}A:(\mBbbN{} {}\mrightarrow{} \mBbbQ{} \mtimes{} \mBbbZ{}) List. Dec(\mexists{}y:\{\mBbbQ{} List| q-constraints(k;A;y)\})
Date html generated:
2016_05_15-PM-11_31_08
Last ObjectModification:
2015_12_27-PM-07_29_46
Theory : rationals
Home
Index