Nuprl Rule : computeAll

H  ⊢ a ~ b

  BY computeAll ()
     
     CallLisp(COMPUTE-ALL)
  No Subgoals


Definitions occuring in rule :  sqequal: s ~ t,  axiom: Ax
Latex:
H    \mvdash{}  a  \msim{}  b

    BY  computeAll  ()
         
          CallLisp(COMPUTE-ALL)
    No  Subgoals


Date html generated: 2019_06_20-PM-04_11_51
Last ObjectModification: 2016_01_06-PM-03_17_19

Theory : rules


Home Index