Nuprl Rule : isAtom2ReduceTrue

H  ⊢ isatom2(z;a;b) ~ a

  BY isAtom2ReduceTrue ()
  
  H  ⊢ z = z ∈ Atom2


Definitions occuring in rule :  sqequal: s ~ t,  isatom2: isatom2(z;a;b),  equal: s = t ∈ T,  atom: Atom$n,  axiom: Ax
Latex:
H    \mvdash{}  isatom2(z;a;b)  \msim{}  a

    BY  isAtom2ReduceTrue  ()
   
    H    \mvdash{}  z  =  z


Date html generated: 2019_06_20-PM-04_12_22
Last ObjectModification: 2015_11_25-PM-03_44_28

Theory : rules


Home Index