Nuprl Lemma : decidable__q-constraints
∀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: ℤ
Definitions unfolded in proof :
subtype_rel: A ⊆r B,
so_apply: x[s1;s2],
so_lambda: λ2x y.t[x; y],
sq_exists: ∃x:A [B[x]],
top: Top,
false: False,
satisfiable_int_formula: satisfiable_int_formula(fmla),
not: ¬A,
or: P ∨ Q,
decidable: Dec(P),
ge: i ≥ j ,
less_than: a < b,
le: A ≤ B,
and: P ∧ Q,
lelt: i ≤ j < k,
int_seg: {i..j-},
nat: ℕ,
prop: ℙ,
squash: ↓T,
exists: ∃x:A. B[x],
so_apply: x[s],
so_lambda: λ2x.t[x],
uimplies: b supposing a,
member: t ∈ T,
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
all: ∀x:A. B[x],
guard: {T},
sq_type: SQType(T),
iff: P ⇐⇒ Q,
cand: A c∧ B,
rev_implies: P ⇐ Q,
true: True,
q-constraints: q-constraints(k;A;y),
less_than': less_than'(a;b),
bool: 𝔹,
ifthenelse: if b then t else f fi ,
q-rel: q-rel(r;x),
sq_stable: SqStable(P),
pi1: fst(t),
pi2: snd(t),
cons: [a / b],
l_all: (∀x∈L.P[x]),
nat_plus: ℕ+,
select: L[n],
qsub: r - s,
qdiv: (r/s),
uiff: uiff(P;Q),
evalall: evalall(t),
callbyvalueall: callbyvalueall,
qmul: r * s,
bfalse: ff,
it: ⋅,
unit: Unit,
btrue: tt,
eq_int: (i =z j),
q-rel-lub: q-rel-lub(r1;r2),
rev_uimplies: rev_uimplies(P;Q),
band: p ∧b q,
mapfilter: mapfilter(f;P;L),
assert: ↑b,
qeq: qeq(r;s),
qbetween: a ≤ b ≤ c,
q-between: a < b < c,
bnot: ¬bb,
lt_int: i <z j,
qadd: r + s,
qpositive: qpositive(r),
bor: p ∨bq,
q_le: q_le(r;s),
qadd_grp: <ℚ+>,
grp_le: ≤b,
dset_of_mon: g↓set,
oset_of_ocmon: g↓oset,
set_le: ≤b,
infix_ap: x f y,
set_blt: a <b b,
set_lt: a <p b,
grp_lt: a < b,
qless: r < s
Lemmas referenced :
subtype_rel_self,
subtype_rel_function,
natrec_wf,
istype-nat,
istype-le,
int_formula_prop_wf,
int_term_value_var_lemma,
int_term_value_constant_lemma,
int_formula_prop_le_lemma,
int_formula_prop_not_lemma,
istype-void,
int_formula_prop_and_lemma,
istype-int,
itermVar_wf,
itermConstant_wf,
intformle_wf,
intformnot_wf,
intformand_wf,
full-omega-unsat,
decidable__le,
nat_properties,
int_seg_properties,
int_seg_wf,
q-constraints_wf,
sq_exists_wf,
decidable_wf,
valueall-type-value-type,
equal_wf,
set-value-type,
evalall-reduce,
list_wf,
int-valueall-type,
rationals-value-type,
function-valueall-type,
product-valueall-type,
rationals_wf,
nat_wf,
list-valueall-type,
int_subtype_base,
subtype_base_sq,
decidable__equal_int,
iff_weakening_equal,
q-linear-base,
q-rel_wf,
l_all_wf2,
istype-universe,
true_wf,
squash_wf,
l_member_wf,
top_wf,
subtype_rel_product,
pi1_wf_top,
pi2_wf,
le_wf,
set_subtype_base,
length_wf_nat,
equal-wf-base,
decidable__q-rel,
decidable__l_all-better-extract,
length_of_nil_lemma,
nil_wf,
ifthenelse_wf,
qless_wf,
qless_witness,
qle_wf,
qle_witness,
eq_int_wf,
sq_stable_from_decidable,
sq_stable__l_all,
istype-less_than,
int_formula_prop_less_lemma,
intformless_wf,
decidable__lt,
int_formula_prop_eq_lemma,
int_term_value_subtract_lemma,
intformeq_wf,
itermSubtract_wf,
subtract_wf,
evalall-equal,
member_wf,
int-subtype-rationals,
decidable__equal_rationals,
decidable__not,
decidable__cand,
equal-wf-T-base,
not_wf,
decidable__l_exists_better-extract,
l_exists_iff,
qdiv_wf,
qmul_wf,
qsub_wf,
map_wf,
product_subtype_list,
list-cases,
q-linear_wf,
cons_wf,
append_wf,
int_term_value_add_lemma,
itermAdd_wf,
length_of_cons_lemma,
length-append,
length_wf,
select_wf,
subtype_rel_list,
select-map,
map-length,
q-linear-unroll,
select_append_back,
qadd_wf,
select_append_front,
q-linear-equal,
q-linear-times,
q-linear-sum,
qmul_comm_qrng,
qmul_ac_1_qrng,
qmul_assoc_qrng,
qmul_over_minus_qrng,
istype-assert,
assert-qeq,
qeq_wf2,
assert_wf,
iff_weakening_uiff,
qinv_wf,
sq_stable__equal,
sq_stable__and,
assert_of_null,
null_wf3,
length_of_not_nil,
last_lemma,
false_wf,
add-is-int-iff,
last_wf,
length_append,
l_all_iff,
member_map,
less_than_wf,
q-constraint-times,
q-constraint-sum,
assert_of_bnot,
eqff_to_assert,
iff_transitivity,
assert_of_eq_int,
eqtt_to_assert,
uiff_transitivity,
bnot_wf,
bool_wf,
q-constraint-zero,
qmul_assoc,
qmul_com,
qmul_inv,
qadd_minus,
qmul_ident,
product-map,
member_filter,
l_exists_wf,
q-rel-lub_wf,
q_less_wf,
filter_wf5,
assert-q_less-eq,
member_append,
normalize-constraints-eq,
normalize-constraints_wf,
decidable__qless,
qless_irreflexivity,
qle_weakening_eq_qorder,
qless_transitivity_2_qorder,
qneginv-positive,
qinv-positive,
qmul-positive,
qinv_inv_q,
qmul_one_qrng,
qmul-qdiv-cancel2,
qmul-qdiv-cancel4,
qmul_over_plus_qrng,
qadd_comm_q,
assert_of_bor,
bnot_thru_band,
assert_of_band,
bor_wf,
bfalse_wf,
btrue_wf,
band_wf,
bool_subtype_base,
bool_cases,
qle_weakening_lt_qorder,
int_formula_prop_or_lemma,
intformor_wf,
mapfilter_wf,
q-max-exists,
null-map,
member_null,
member_map_filter,
q-min-exists,
length-singleton,
qle-minus,
qinverse_q,
qadd_preserves_qle,
average-qbetween,
mon_ident_q,
qadd_ac_1_q,
qle_transitivity_qorder,
qadd_preserves_qless,
qle_antisymmetry,
qless_complement_qorder,
average-q-between,
qless_transitivity_1_qorder,
qadd_inv_assoc_q,
qadd_com,
qless_trichot_qorder,
q-constraint-positive,
q-constraint-negative,
mon_assoc_q,
qmul_zero_qrng,
uiff_transitivity2,
qinv_id_q,
qless-minus
Rules used in proof :
functionExtensionality,
applyEquality,
voidElimination,
isect_memberEquality_alt,
int_eqEquality,
dependent_pairFormation_alt,
approximateComputation,
unionElimination,
imageElimination,
productElimination,
natural_numberEquality,
applyLambdaEquality,
hyp_replacement,
dependent_functionElimination,
because_Cache,
rename,
setElimination,
equalityIstype,
dependent_set_memberEquality_alt,
cutEval,
equalitySymmetry,
equalityTransitivity,
baseClosed,
imageMemberEquality,
independent_pairFormation,
independent_functionElimination,
universeIsType,
hypothesisEquality,
inhabitedIsType,
functionIsType,
lambdaEquality_alt,
sqequalRule,
independent_isectElimination,
intEquality,
hypothesis,
functionEquality,
productEquality,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
thin,
cut,
lambdaFormation_alt,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
cumulativity,
instantiate,
universeEquality,
productIsType,
setIsType,
inrFormation_alt,
sqequalBase,
inlFormation_alt,
dependent_set_memberFormation_alt,
functionIsTypeImplies,
axiomEquality,
isect_memberFormation_alt,
promote_hyp,
independent_pairEquality,
spreadEquality,
hypothesis_subsumption,
closedConclusion,
minusEquality,
equalityElimination,
addEquality,
baseApply,
pointwiseFunctionality,
unionIsType,
unionEquality,
Error :memTop
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:
2020_05_20-AM-09_30_24
Last ObjectModification:
2020_02_01-AM-11_56_25
Theory : rationals
Home
Index