Nuprl Rule : isintReduceAtom
H ⊢ if z is an integer then a else b ~ b
BY isintReduceAtom ()
H ⊢ z = z ∈ Atom
Definitions occuring in rule :
sqequal: s ~ t,
isint: isint def,
equal: s = t ∈ T,
atom: Atom,
axiom: Ax
Latex:
H \mvdash{} if z is an integer then a else b \msim{} b
BY isintReduceAtom ()
H \mvdash{} z = z
Date html generated:
2019_06_20-PM-04_12_06
Last ObjectModification:
2015_11_25-PM-03_44_28
Theory : rules
Home
Index