Nuprl Rule : computationStep

H  ⊢ a ~ b

  BY computationStep ()

     CallLisp(COMPUTATION-STEP)
  No Subgoals

Definitions occuring in rule : sqequal: s ~ t, axiom: Ax

Latex:
H \mvdash{} a \msim{} b BY computationStep () CallLisp(COMPUTATION-STEP) No Subgoals Date html generated: 2019_06_20-PM-04_11_40 Last ObjectModification: 2015_11_25-PM-03_37_49 Theory : rules Home Index