Nuprl Lemma : ipolynomial-term-cons-ringeq

`∀[r:Rng]. ∀[m:iMonomial()]. ∀[p:iMonomial() List].`
`  ipolynomial-term([m / p]) ≡ imonomial-term(m) (+) ipolynomial-term(p)`

Proof

Definitions occuring in Statement :  ringeq_int_terms: `t1 ≡ t2` rng: `Rng` ipolynomial-term: `ipolynomial-term(p)` imonomial-term: `imonomial-term(m)` iMonomial: `iMonomial()` itermAdd: `left (+) right` cons: `[a / b]` list: `T List` uall: `∀[x:A]. B[x]`
Definitions unfolded in proof :  rng: `Rng` ringeq_int_terms: `t1 ≡ t2` cons: `[a / b]` btrue: `tt` bfalse: `ff` ifthenelse: `if b then t else f fi ` so_apply: `x[s1;s2]` so_lambda: `λ2x y.t[x; y]` top: `Top` ipolynomial-term: `ipolynomial-term(p)` or: `P ∨ Q` all: `∀x:A. B[x]` member: `t ∈ T` uall: `∀[x:A]. B[x]` and: `P ∧ Q` int_nzero: `ℤ-o` iMonomial: `iMonomial()` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` guard: `{T}` true: `True` squash: `↓T` so_apply: `x[s]` uimplies: `b supposing a` subtype_rel: `A ⊆r B` prop: `ℙ` implies: `P `` Q` so_lambda: `λ2x.t[x]` uiff: `uiff(P;Q)` rev_uimplies: `rev_uimplies(P;Q)`
Lemmas referenced :  rng_wf list_wf rng_car_wf list_accum_cons_lemma product_subtype_list list_accum_nil_lemma null_nil_lemma spread_cons_lemma null_cons_lemma list-cases iMonomial_wf imonomial-term_wf ring_term_value_wf rng_plus_zero int-to-ring-zero ring_term_value_const_lemma ring_term_value_add_lemma iff_weakening_equal rng_plus_assoc rng_plus_wf infix_ap_wf true_wf squash_wf equal_wf subtype_rel_self sorted_wf int_nzero_wf subtype_rel_product subtype_rel_list list_accum_wf itermAdd_wf ringeq_int_terms_wf int_term_wf all_wf list_induction ringeq_int_terms_functionality itermAdd_functionality_wrt_ringeq ringeq_int_terms_weakening
Rules used in proof :  because_Cache rename setElimination intEquality functionEquality axiomEquality lambdaEquality productElimination hypothesis_subsumption promote_hyp voidEquality voidElimination isect_memberEquality sqequalRule unionElimination hypothesisEquality dependent_functionElimination thin isectElimination sqequalHypSubstitution hypothesis extract_by_obid cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution independent_pairEquality applyEquality functionExtensionality equalitySymmetry lambdaFormation baseClosed imageMemberEquality natural_numberEquality universeEquality equalityTransitivity imageElimination independent_functionElimination setEquality independent_isectElimination productEquality

Latex:
\mforall{}[r:Rng].  \mforall{}[m:iMonomial()].  \mforall{}[p:iMonomial()  List].
ipolynomial-term([m  /  p])  \mequiv{}  imonomial-term(m)  (+)  ipolynomial-term(p)

Date html generated: 2018_05_21-PM-03_16_32
Last ObjectModification: 2018_01_25-PM-02_19_52

Theory : rings_1

Home Index