Nuprl Rule : exceptionInteq
H  ⊢ if x=exception(u; v) then y else z ~ exception(u; v)
  BY exceptionInteq ()
  
  H  ⊢ x ∈ ℤ
Definitions occuring in rule : 
sqequal: s ~ t
, 
int_eq: if a=b then c else d
, 
member: t ∈ T
, 
int: ℤ
, 
axiom: Ax
Latex:
H    \mvdash{}  if  x=exception(u;  v)  then  y  else  z  \msim{}  exception(u;  v)
    BY  exceptionInteq  ()
   
    H    \mvdash{}  x  \mmember{}  \mBbbZ{}
Date html generated:
2019_06_20-PM-04_12_13
Last ObjectModification:
2015_11_25-PM-03_47_02
Theory : rules
Home
Index