Nuprl Lemma : int-rem-exception

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


Proof




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

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



Date html generated: 2019_06_20-AM-11_22_00
Last ObjectModification: 2018_10_12-PM-03_56_40

Theory : arithmetic


Home Index