Nuprl Lemma : gcd-reduce-ineq-constraints

Nuprl Lemma : gcd-reduce-ineq-constraints_wf2

∀[n:ℕ]. ∀[LL,sat:{L:ℤ List| ||L|| = (n + 1) ∈ ℤ} List].
(gcd-reduce-ineq-constraints(sat;LL) ∈ {L:ℤ List| ||L|| = (n + 1) ∈ ℤ} List?)

Proof

Definitions occuring in Statement : gcd-reduce-ineq-constraints: gcd-reduce-ineq-constraints(sat;LL), length: ||as||, list: T List, nat: ℕ, uall: ∀[x:A]. B[x], unit: Unit, member: t ∈ T, set: {x:A| B[x]} , union: left + right, add: n + m, natural_number: $n, int: ℤ, equal: s = t ∈ T
Definitions unfolded in proof : uall: ∀[x:A]. B[x], member: t ∈ T, gcd-reduce-ineq-constraints: gcd-reduce-ineq-constraints(sat;LL), prop: ℙ, so_lambda: λ₂x y.t[x; y], all: ∀x:A. B[x], subtype_rel: A ⊆r B, uimplies: b supposing a, nat: ℕ, so_lambda: λ₂x.t[x], so_apply: x[s], or: P ∨ Q, nil: [], it: ⋅, sq_stable: SqStable(P), implies: P ⇒ Q, squash: ↓T, uiff: uiff(P;Q), and: P ∧ Q, guard: {T}, subtract: n - m, top: Top, le: A ≤ B, not: ¬A, less_than': less_than'(a;b), true: True, false: False, cons: [a / b], exposed-bfalse: exposed-bfalse, bool: 𝔹, unit: Unit, btrue: tt, less_than: a < b, bfalse: ff, exists: ∃x:A. B[x], sq_type: SQType(T), bnot: ¬_bb, ifthenelse: if b then t else f fi , assert: ↑b, rev_implies: P ⇐ Q, iff: P ⇐⇒ Q, has-value: (a)↓, int_nzero: ℤ^-^o, cand: A c∧ B, nequal: a ≠ b ∈ T , rev_uimplies: rev_uimplies(P;Q), decidable: Dec(P), so_apply: x[s1;s2]
Lemmas referenced : accumulate_abort_wf, list_wf, equal-wf-base, unit_wf2, list_subtype_base, int_subtype_base, set_subtype_base, le_wf, istype-int, list-cases, length_of_nil_lemma, sq_stable__le, le_antisymmetry_iff, condition-implies-le, minus-add, istype-void, minus-one-mul, zero-add, minus-one-mul-top, add-commutes, add_functionality_wrt_le, add-associates, add-zero, le-add-cancel, product_subtype_list, lt_int_wf, eqtt_to_assert, assert_of_lt_int, istype-top, it_wf, eqff_to_assert, bool_cases_sqequal, subtype_base_sq, bool_wf, bool_subtype_base, assert-bnot, iff_weakening_uiff, assert_wf, less_than_wf, istype-less_than, cons_wf, nil_wf, value-type-has-value, nat_wf, set-value-type, int-value-type, absval_wf, gcd-list_wf, cons-listp, eager_map_cons_lemma, div_floor_wf, not-equal-2, decidable__le, istype-le, istype-false, not-le-2, less-iff-le, add-swap, le-add-cancel2, nequal_wf, divide_wfa, list-value-type, eager-map_wf, list-valueall-type, set-valueall-type, int-valueall-type, istype-nat, length_of_cons_lemma, map-length, eager-map-is-map
Rules used in proof : sqequalSubstitution, sqequalTransitivity, computationStep, sqequalReflexivity, Error :isect_memberFormation_alt, introduction, cut, sqequalRule, extract_by_obid, sqequalHypSubstitution, isectElimination, thin, setEquality, closedConclusion, intEquality, hypothesis, because_Cache, Error :inlEquality_alt, hypothesisEquality, Error :universeIsType, Error :lambdaEquality_alt, Error :lambdaFormation_alt, baseApply, baseClosed, applyEquality, independent_isectElimination, natural_numberEquality, setElimination, rename, dependent_functionElimination, unionElimination, independent_functionElimination, imageMemberEquality, imageElimination, addEquality, productElimination, Error :isect_memberEquality_alt, voidElimination, minusEquality, promote_hyp, hypothesis_subsumption, Error :inhabitedIsType, equalityElimination, lessCases, axiomSqEquality, Error :isectIsTypeImplies, independent_pairFormation, Error :inrEquality_alt, equalityTransitivity, equalitySymmetry, Error :dependent_pairFormation_alt, Error :equalityIstype, instantiate, cumulativity, Error :dependent_set_memberEquality_alt, sqequalBase, callbyvalueReduce, Error :inlFormation_alt, Error :inrFormation_alt, Error :setIsType, axiomEquality

Latex:
\mforall{}[n:\mBbbN{}]. \mforall{}[LL,sat:\{L:\mBbbZ{} List| ||L|| = (n + 1)\} List]. (gcd-reduce-ineq-constraints(sat;LL) \mmember{} \{L:\mBbbZ{} List| ||L|| = (n + 1)\} List?) Date html generated: 2019_06_20-PM-00_50_54 Last ObjectModification: 2019_03_06-PM-10_43_37 Theory : omega Home Index