Nuprl Lemma : itermSubtract_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 itermSubtract: 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 itermSubtract: 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_minus_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_10
Last ObjectModification: 2018_01_25-PM-02_18_59

Theory : rings_1

Home Index