Nuprl Rule : isatomReduceTrue

H  ⊢ if z is an atom then a otherwise b ~ a

  BY isatomReduceTrue ()
  
  H  ⊢ z = z ∈ Atom


Definitions occuring in rule :  sqequal: s ~ t,  isatom: if z is an atom then a otherwise b,  equal: s = t ∈ T,  atom: Atom,  axiom: Ax
Latex:
H    \mvdash{}  if  z  is  an  atom  then  a  otherwise  b  \msim{}  a

    BY  isatomReduceTrue  ()
   
    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