Nuprl Lemma : add-associates

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


Proof




Definitions occuring in Statement :  uall: [x:A]. B[x] top: Top add: m sqequal: t
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T uall: [x:A]. B[x] has-value: (a)↓ and: P ∧ Q implies:  Q uimplies: supposing a prop: sq_type: SQType(T) guard: {T} top: Top
Lemmas referenced :  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 addAssociative hypothesisEquality hypothesis intEquality isect_memberFormation introduction sqequalSqle sqleRule thin divergentSqle callbyvalueAdd sqequalHypSubstitution sqequalRule baseApply closedConclusion baseClosed productElimination equalityTransitivity equalitySymmetry extract_by_obid isectElimination independent_isectElimination dependent_functionElimination independent_functionElimination instantiate cumulativity sqleReflexivity addExceptionCases axiomSqleEquality exceptionSqequal sqequalAxiom isect_memberEquality because_Cache voidElimination voidEquality addEquality

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



Date html generated: 2017_04_14-AM-07_16_09
Last ObjectModification: 2017_02_27-PM-02_51_17

Theory : arithmetic


Home Index