### Nuprl Lemma : two-mul

`∀[x:Top]. (x + x ~ 2 * x)`

Proof

Definitions occuring in Statement :  uall: `∀[x:A]. B[x]` top: `Top` multiply: `n * m` add: `n + m` natural_number: `\$n` sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` top: `Top` has-value: `(a)↓` and: `P ∧ Q` uimplies: `b supposing a` implies: `P `` Q` false: `False`
Lemmas referenced :  top_wf int-value-type value-type-has-value exception-not-value is-exception_wf has-value_wf_base one-mul mul-distributes-right
Rules used in proof :  cut sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction hypothesis sqequalAxiom intEquality sqequalRule hypothesisEquality isect_memberEquality voidElimination voidEquality lemma_by_obid sqequalHypSubstitution isectElimination thin sqequalSqle sqleRule divergentSqle callbyvalueAdd baseApply closedConclusion baseClosed productElimination equalityTransitivity equalitySymmetry sqleReflexivity addExceptionCases axiomSqleEquality exceptionSqequal callbyvalueMultiply multiplyExceptionCases independent_isectElimination natural_numberEquality independent_functionElimination

Latex:
\mforall{}[x:Top].  (x  +  x  \msim{}  2  *  x)

Date html generated: 2016_05_13-PM-03_29_27
Last ObjectModification: 2016_01_14-PM-06_41_47

Theory : arithmetic

Home Index