Nuprl Lemma : minus-add

[x,y:Top].  (-(x y) (-x) (-y))


Proof




Definitions occuring in Statement :  uall: [x:A]. B[x] top: Top add: m minus: -n sqequal: t
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T uall: [x:A]. B[x] implies:  Q top: Top has-value: (a)↓ uimplies: supposing a prop: and: P ∧ Q sq_type: SQType(T) guard: {T}
Lemmas referenced :  add-inverse-unique minus-one-mul add-associates add-swap add-mul-special zero-mul value-type-has-value int-value-type equal_wf subtype_base_sq int_subtype_base has-value_wf_base is-exception_wf top_wf int-add-exception
Rules used in proof :  cut sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation hypothesis intEquality equalitySymmetry introduction extract_by_obid sqequalHypSubstitution isectElimination thin addEquality hypothesisEquality minusEquality independent_functionElimination sqequalRule isect_memberEquality voidElimination voidEquality natural_numberEquality isect_memberFormation sqequalSqle sqleRule divergentSqle callbyvalueMinus baseApply closedConclusion baseClosed equalityTransitivity independent_isectElimination dependent_functionElimination callbyvalueAdd productElimination instantiate cumulativity sqleReflexivity minusExceptionCases axiomSqleEquality addExceptionCases exceptionSqequal because_Cache sqequalAxiom

Latex:
\mforall{}[x,y:Top].    (-(x  +  y)  \msim{}  (-x)  +  (-y))



Date html generated: 2017_04_14-AM-07_16_20
Last ObjectModification: 2017_02_27-PM-02_51_10

Theory : arithmetic


Home Index