Nuprl Lemma : itermAdd_functionality_wrt_ringeq

[r:Rng]. ∀[a,b,c,d:int_term()].  (a (+) c ≡ (+) d) supposing (a ≡ and c ≡ d)


Definitions occuring in Statement :  ringeq_int_terms: t1 ≡ t2 rng: Rng itermAdd: left (+) right int_term: int_term() uimplies: supposing a uall: [x:A]. B[x]
Definitions unfolded in proof :  implies:  Q rev_implies:  Q and: P ∧ Q iff: ⇐⇒ Q guard: {T} subtype_rel: A ⊆B true: True infix_ap: y rng: Rng prop: squash: T int_term_ind: int_term_ind itermAdd: left (+) right ring_term_value: ring_term_value(f;t) all: x:A. B[x] ringeq_int_terms: t1 ≡ t2 uimplies: supposing a member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  rng_wf int_term_wf ringeq_int_terms_wf iff_weakening_equal infix_ap_wf rng_plus_wf rng_car_wf true_wf squash_wf equal_wf
Rules used in proof :  isect_memberEquality axiomEquality intEquality functionEquality independent_functionElimination productElimination independent_isectElimination baseClosed imageMemberEquality natural_numberEquality because_Cache rename setElimination universeEquality equalitySymmetry equalityTransitivity isectElimination extract_by_obid imageElimination lambdaEquality applyEquality sqequalRule hypothesisEquality thin dependent_functionElimination hypothesis lambdaFormation sqequalHypSubstitution cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

\mforall{}[r:Rng].  \mforall{}[a,b,c,d:int\_term()].    (a  (+)  c  \mequiv{}  b  (+)  d)  supposing  (a  \mequiv{}  b  and  c  \mequiv{}  d)

Date html generated: 2018_05_21-PM-03_16_07
Last ObjectModification: 2018_01_25-PM-02_18_51

Theory : rings_1

Home Index