Nuprl Lemma : int-mul-exception

[x:ℤ]. ∀[u,v:Top].  (x (exception(u; v)) exception(u; v))


Proof




Definitions occuring in Statement :  uall: [x:A]. B[x] top: Top multiply: m int: sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T
Lemmas referenced :  top_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut exceptionMultiply hypothesisEquality hypothesis axiomSqEquality Error :inhabitedIsType,  sqequalRule sqequalHypSubstitution Error :isect_memberEquality_alt,  isectElimination thin Error :isectIsTypeImplies,  Error :universeIsType,  extract_by_obid intEquality

Latex:
\mforall{}[x:\mBbbZ{}].  \mforall{}[u,v:Top].    (x  *  (exception(u;  v))  \msim{}  exception(u;  v))



Date html generated: 2019_06_20-AM-11_21_58
Last ObjectModification: 2018_10_15-PM-03_33_16

Theory : arithmetic


Home Index