Nuprl Lemma : itermMultiply_functionality_wrt_req

[a,b,c,d:int_term()].  (a (*) c ≡ (*) d) supposing (a ≡ and c ≡ d)


Proof




Definitions occuring in Statement :  req_int_terms: t1 ≡ t2 itermMultiply: left (*) right int_term: int_term() uimplies: supposing a uall: [x:A]. B[x]
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a req_int_terms: t1 ≡ t2 all: x:A. B[x] real_term_value: real_term_value(f;t) itermMultiply: left (*) right int_term_ind: int_term_ind implies:  Q prop: uiff: uiff(P;Q) and: P ∧ Q rev_uimplies: rev_uimplies(P;Q)
Lemmas referenced :  real_wf req_witness real_term_value_wf itermMultiply_wf req_int_terms_wf int_term_wf rmul_wf req_weakening req_functionality rmul_functionality
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution lambdaFormation hypothesis dependent_functionElimination thin hypothesisEquality sqequalRule functionEquality intEquality extract_by_obid lambdaEquality isectElimination functionExtensionality applyEquality independent_functionElimination isect_memberEquality because_Cache equalityTransitivity equalitySymmetry independent_isectElimination productElimination

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



Date html generated: 2017_10_02-PM-07_18_50
Last ObjectModification: 2017_04_02-PM-11_36_57

Theory : reals


Home Index