### Nuprl Lemma : hd-rev-pcs-mon-vars

`∀X:polynomial-constraints(). (0 < ||rev(pcs-mon-vars(X))|| ∧ (hd(rev(pcs-mon-vars(X))) = [] ∈ (ℤ List)))`

Proof

Definitions occuring in Statement :  pcs-mon-vars: `pcs-mon-vars(X)` polynomial-constraints: `polynomial-constraints()` hd: `hd(l)` length: `||as||` reverse: `rev(as)` nil: `[]` list: `T List` less_than: `a < b` all: `∀x:A. B[x]` and: `P ∧ Q` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` uall: `∀[x:A]. B[x]` so_lambda: `λ2x.t[x]` implies: `P `` Q` prop: `ℙ` and: `P ∧ Q` subtype_rel: `A ⊆r B` uimplies: `b supposing a` iPolynomial: `iPolynomial()` int_seg: `{i..j-}` sq_stable: `SqStable(P)` lelt: `i ≤ j < k` squash: `↓T` guard: `{T}` so_apply: `x[s]` iMonomial: `iMonomial()` top: `Top` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` or: `P ∨ Q` assert: `↑b` ifthenelse: `if b then t else f fi ` btrue: `tt` less_than: `a < b` less_than': `less_than'(a;b)` false: `False` cons: `[a / b]` bfalse: `ff` not: `¬A` cand: `A c∧ B` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` pi2: `snd(t)` sq_type: `SQType(T)` nat: `ℕ` le: `A ≤ B` decidable: `Dec(P)` uiff: `uiff(P;Q)` subtract: `n - m` true: `True` ge: `i ≥ j ` polynomial-mon-vars: `polynomial-mon-vars(init;p)` colength: `colength(L)` nil: `[]` it: `⋅` polynomial-constraints: `polynomial-constraints()` pcs-mon-vars: `pcs-mon-vars(X)` last: `last(L)` select: `L[n]` length: `||as||` list_ind: list_ind
Lemmas referenced :  polynomial-constraints_wf list_induction iPolynomial_wf all_wf list_wf less_than_wf length_wf equal-wf-base list_accum_wf top_wf subtype_rel_list subtype_rel_set iMonomial_wf int_seg_wf imonomial-less_wf select_wf sq_stable__le less_than_transitivity2 le_weakening2 subtype_rel_product int_nzero_wf sorted_wf subtype_rel_self polynomial-mon-vars_wf equal-wf-T-base last_wf list-cases null_nil_lemma length_of_nil_lemma product_subtype_list null_cons_lemma length_of_cons_lemma false_wf equal_wf list_accum_nil_lemma list_accum_cons_lemma list_subtype_base int_subtype_base member-polynomial-mon-vars l_exists_wf equal-wf-base-T l_member_wf subtype_base_sq last_member nil_member length_wf_nat nat_wf decidable__lt not-lt-2 condition-implies-le minus-add minus-one-mul zero-add minus-one-mul-top add-commutes add_functionality_wrt_le add-associates add-zero le-add-cancel nil_wf squash_wf true_wf nat_properties less_than_transitivity1 less_than_irreflexivity ge_wf colength_wf_list spread_cons_lemma le_antisymmetry_iff decidable__le not-le-2 le_wf subtract_wf not-ge-2 less-iff-le minus-minus add-swap set_subtype_base insert_wf list-deq_wf int-deq_wf iff_weakening_equal non_nil_length insert-not-nil last-insert ite_rw_false cons_wf length-reverse hd-reverse-is-last pcs-mon-vars_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid hypothesis thin sqequalHypSubstitution isectElimination sqequalRule lambdaEquality intEquality functionEquality natural_numberEquality because_Cache hypothesisEquality productEquality applyEquality independent_isectElimination setElimination rename independent_functionElimination productElimination imageMemberEquality baseClosed imageElimination dependent_functionElimination setEquality isect_memberEquality voidElimination voidEquality unionElimination promote_hyp hypothesis_subsumption equalityTransitivity equalitySymmetry independent_pairFormation baseApply closedConclusion inlFormation instantiate cumulativity addEquality minusEquality addLevel hyp_replacement universeEquality equalityUniverse levelHypothesis intWeakElimination axiomEquality applyLambdaEquality dependent_set_memberEquality

Latex:
\mforall{}X:polynomial-constraints().  (0  <  ||rev(pcs-mon-vars(X))||  \mwedge{}  (hd(rev(pcs-mon-vars(X)))  =  []))

Date html generated: 2017_04_14-AM-09_03_44
Last ObjectModification: 2017_02_27-PM-03_44_20

Theory : omega

Home Index