Nuprl Lemma : q-constraint-negative

[x:ℕ ⟶ ℚ]. ∀[r:ℤ]. ∀[k:ℕ+]. ∀[y:ℚ List].
  (uiff(q-rel(r;q-linear(k;j.x j;y));q-rel(r;-(y[k 1]) ((-1/x k) q-linear(k 1;j.x j;y))))) supposing 
     (x k < and 
     (k ≤ ||y||))


Proof




Definitions occuring in Statement :  q-rel: q-rel(r;x) q-linear: q-linear(k;i.X[i];y) qless: r < s qdiv: (r/s) qmul: s qadd: s rationals: select: L[n] length: ||as|| list: List nat_plus: + nat: uiff: uiff(P;Q) uimplies: supposing a uall: [x:A]. B[x] le: A ≤ B apply: a function: x:A ⟶ B[x] subtract: m minus: -n natural_number: $n int:
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a subtype_rel: A ⊆B nat: nat_plus: + all: x:A. B[x] decidable: Dec(P) or: P ∨ Q not: ¬A implies:  Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False and: P ∧ Q prop: qless: r < s grp_lt: a < b set_lt: a <b assert: b ifthenelse: if then else fi  set_blt: a <b b band: p ∧b q infix_ap: y set_le: b pi2: snd(t) oset_of_ocmon: g↓oset dset_of_mon: g↓set grp_le: b pi1: fst(t) qadd_grp: <ℚ+> q_le: q_le(r;s) callbyvalueall: callbyvalueall evalall: evalall(t) bor: p ∨bq qpositive: qpositive(r) qsub: s qadd: s qmul: s btrue: tt lt_int: i <j bnot: ¬bb bfalse: ff qeq: qeq(r;s) eq_int: (i =z j) true: True uiff: uiff(P;Q) rev_uimplies: rev_uimplies(P;Q) q-rel: q-rel(r;x) squash: T so_lambda: λ2x.t[x] so_apply: x[s] guard: {T} iff: ⇐⇒ Q bool: 𝔹 le: A ≤ B rev_implies:  Q unit: Unit it: qge: a ≥ b qgt: a > b
Lemmas referenced :  qmul_reverses_qless qmul_wf nat_plus_properties decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf intformless_wf istype-int int_formula_prop_and_lemma int_formula_prop_not_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 istype-le q-rel_wf squash_wf true_wf rationals_wf q-linear-unroll istype-nat iff_weakening_equal eq_int_wf qadd_wf select_wf subtract_wf itermSubtract_wf int_term_value_subtract_lemma decidable__lt length_wf qdiv_wf nat_plus_subtype_nat q-linear_wf qle_witness qle_wf qless_witness qless_wf ifthenelse_wf int-subtype-rationals list_wf nat_plus_wf qless_transitivity_2_qorder qle_weakening_eq_qorder qless_irreflexivity equal-wf-base bool_wf int_subtype_base assert_wf bnot_wf not_wf istype-assert istype-void qmul_zero_qrng subtype_rel_self qinv_inv_q uiff_transitivity eqtt_to_assert assert_of_eq_int iff_transitivity iff_weakening_uiff eqff_to_assert assert_of_bnot qmul-preserves-eq equal_wf istype-universe qmul_over_minus_qrng qmul_over_plus_qrng qadd_comm_q qmul-qdiv-cancel3 qmul_assoc qmul_one_qrng qmul_preserves_qle qmul_preserves_qle2 qle-minus qinv_id_q qle_functionality_wrt_implies qle_weakening_lt_qorder qmul_preserves_qless
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin because_Cache minusEquality natural_numberEquality hypothesis applyEquality sqequalRule hypothesisEquality dependent_set_memberEquality_alt setElimination rename dependent_functionElimination unionElimination independent_isectElimination approximateComputation independent_functionElimination dependent_pairFormation_alt lambdaEquality_alt int_eqEquality Error :memTop,  independent_pairFormation universeIsType voidElimination productElimination imageElimination equalityTransitivity equalitySymmetry imageMemberEquality baseClosed inhabitedIsType lambdaFormation_alt axiomEquality equalityIstype closedConclusion sqequalBase instantiate universeEquality promote_hyp independent_pairEquality isect_memberEquality_alt isectIsTypeImplies functionIsType baseApply intEquality equalityElimination applyLambdaEquality

Latex:
\mforall{}[x:\mBbbN{}  {}\mrightarrow{}  \mBbbQ{}].  \mforall{}[r:\mBbbZ{}].  \mforall{}[k:\mBbbN{}\msupplus{}].  \mforall{}[y:\mBbbQ{}  List].
    (uiff(q-rel(r;q-linear(k;j.x  j;y));q-rel(r;-(y[k  -  1])
          +  ((-1/x  k)  *  q-linear(k  -  1;j.x  j;y)))))  supposing 
          (x  k  <  0  and 
          (k  \mleq{}  ||y||))



Date html generated: 2020_05_20-AM-09_27_28
Last ObjectModification: 2020_01_31-AM-11_08_04

Theory : rationals


Home Index