Nuprl Lemma : add-commutes

[x:ℤ]. ∀[y:Top].  (x x)


Proof




Definitions occuring in Statement :  uall: [x:A]. B[x] top: Top add: m int: sqequal: t
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T uall: [x:A]. B[x] has-value: (a)↓ subtype_rel: A ⊆B and: P ∧ Q uimplies: supposing a sq_type: SQType(T) implies:  Q guard: {T} false: False top: Top
Lemmas referenced :  int-add-exception top_wf int-value-type value-type-has-value exception-not-value is-exception_wf has-value_wf_base subtype_base_sq int_subtype_base
Rules used in proof :  cut sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation addCommutative hypothesisEquality hypothesis intEquality isect_memberFormation introduction sqequalSqle sqleRule thin divergentSqle callbyvalueAdd sqequalHypSubstitution sqequalRule baseApply closedConclusion baseClosed applyEquality lemma_by_obid productElimination dependent_functionElimination equalityTransitivity equalitySymmetry instantiate isectElimination cumulativity independent_isectElimination independent_functionElimination sqleReflexivity because_Cache addExceptionCases axiomSqleEquality voidElimination sqequalAxiom isect_memberEquality exceptionSqequal voidEquality

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



Date html generated: 2016_05_13-PM-03_28_48
Last ObjectModification: 2016_01_14-PM-06_42_07

Theory : arithmetic


Home Index