Nuprl Rule : int_eqReduceTrueSq

H  ⊢ if a=b then else u

  BY int_eqReduceTrueSq ()
  
  H  ⊢ u
  H  ⊢ b ∈ ℤ



Definitions occuring in rule :  int_eq: if a=b then else d sqequal: t equal: t ∈ T int: axiom: Ax

Latex:
H    \mvdash{}  if  a=b  then  s  else  t  \msim{}  u

    BY  int\_eqReduceTrueSq  ()
   
    H    \mvdash{}  s  \msim{}  u
    H    \mvdash{}  a  =  b



Date html generated: 2019_06_20-PM-04_11_58
Last ObjectModification: 2015_11_24-PM-01_52_04

Theory : rules


Home Index