Nuprl Lemma : member-gcd-reduce-ineq-constraints

n:ℕ+. ∀ineqs,sat:{L:ℤ List| ||L|| n ∈ ℤ}  List. ∀cc:{L:ℤ List| ||L|| n ∈ ℤ.
  ((↑isl(gcd-reduce-ineq-constraints(sat;ineqs)))  (cc ∈ sat)  (cc ∈ outl(gcd-reduce-ineq-constraints(sat;ineqs))))


Proof




Definitions occuring in Statement :  gcd-reduce-ineq-constraints: gcd-reduce-ineq-constraints(sat;LL) l_member: (x ∈ l) listp: List+ length: ||as|| list: List nat_plus: + outl: outl(x) assert: b isl: isl(x) all: x:A. B[x] implies:  Q set: {x:A| B[x]}  int: equal: t ∈ T
Definitions unfolded in proof :  all: x:A. B[x] uall: [x:A]. B[x] member: t ∈ T prop: so_lambda: λ2x.t[x] subtype_rel: A ⊆B uimplies: supposing a nat_plus: + so_apply: x[s] implies:  Q listp: List+ and: P ∧ Q less_than: a < b squash: T cand: c∧ B guard: {T} isl: isl(x) outl: outl(x) not: ¬A false: False gcd-reduce-ineq-constraints: gcd-reduce-ineq-constraints(sat;LL) so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] assert: b ifthenelse: if then else fi  btrue: tt or: P ∨ Q cons: [a b] decidable: Dec(P) nil: [] it: bfalse: ff eager-map: eager-map(f;as) list_ind: list_ind true: True top: Top less_than': less_than'(a;b) le: A ≤ B uiff: uiff(P;Q) rev_implies:  Q iff: ⇐⇒ Q callbyvalueall: callbyvalueall evalall: evalall(t) outr: outr(x) has-value: (a)↓ has-valueall: has-valueall(a) nat: subtract: m int_nzero: -o nequal: a ≠ b ∈  rev_uimplies: rev_uimplies(P;Q)
Lemmas referenced :  list_induction list_wf equal-wf-base all_wf list_subtype_base int_subtype_base set_subtype_base less_than_wf istype-int assert_wf gcd-reduce-ineq-constraints_wf subtype_rel_list listp_wf subtype_rel_sets_simple length_wf less_than_transitivity1 le_weakening btrue_wf bfalse_wf l_member_wf istype-less_than assert_elim btrue_neq_bfalse accumulate_abort_nil_lemma istype-true istype-assert nat_plus_wf accumulate_abort_cons_lemma list-cases product_subtype_list less_than_irreflexivity length_of_nil_lemma spread_cons_lemma decidable__assert null_wf eager_map_cons_lemma null_cons_lemma null_nil_lemma istype-void eager_map_nil_lemma length_of_cons_lemma cons-listp le-add-cancel zero-add add-commutes add-swap add-associates add_functionality_wrt_le le_antisymmetry_iff not-lt-2 istype-false cons_member length-singleton nil_wf cons_wf void-valueall-type int-valueall-type list-valueall-type union-valueall-type valueall-type-has-valueall top_wf it_wf decidable__lt istype-top accumulate_abort-aborted evalall-reduce absval_wf gcd-list_wf length_wf_nat condition-implies-le minus-add minus-one-mul minus-one-mul-top add-zero value-type-has-value int-value-type list-value-type eager-map_wf divide_wfa not-equal-2 decidable__le istype-le not-le-2 less-iff-le le-add-cancel2 nequal_wf div_floor_wf map-length map_wf eager-map-is-map
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt cut thin introduction extract_by_obid sqequalHypSubstitution isectElimination setEquality intEquality hypothesis because_Cache sqequalRule lambdaEquality_alt closedConclusion baseApply baseClosed hypothesisEquality applyEquality independent_isectElimination natural_numberEquality universeIsType setElimination rename functionEquality inhabitedIsType equalityTransitivity equalitySymmetry independent_pairFormation imageElimination productElimination dependent_functionElimination equalityIstype sqequalBase unionElimination independent_functionElimination dependent_set_memberEquality_alt productIsType applyLambdaEquality voidElimination setIsType Error :memTop,  functionIsType promote_hyp hypothesis_subsumption callbyvalueReduce sqleReflexivity isect_memberEquality_alt inrFormation_alt addEquality inlEquality_alt voidEquality unionEquality lessCases isect_memberFormation_alt axiomSqEquality isectIsTypeImplies imageMemberEquality minusEquality inlFormation_alt

Latex:
\mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}ineqs,sat:\{L:\mBbbZ{}  List|  ||L||  =  n\}    List.  \mforall{}cc:\{L:\mBbbZ{}  List|  ||L||  =  n\}  .
    ((\muparrow{}isl(gcd-reduce-ineq-constraints(sat;ineqs)))
    {}\mRightarrow{}  (cc  \mmember{}  sat)
    {}\mRightarrow{}  (cc  \mmember{}  outl(gcd-reduce-ineq-constraints(sat;ineqs))))



Date html generated: 2020_05_19-PM-09_38_54
Last ObjectModification: 2020_01_01-AM-10_05_20

Theory : omega


Home Index