Nuprl Rule : reverse_direct_computation

H  ⊢ ext t

  BY reverse_direct_computation S
     
     Let CallLisp(REVERSE-DIRECT-COMPUTATION)
  H  ⊢ ext t


Latex:
H    \mvdash{}  T  ext  t

    BY  reverse\_direct\_computation  S
         
          Let  C  =  CallLisp(REVERSE-DIRECT-COMPUTATION)
    H    \mvdash{}  C  ext  t



Date html generated: 2019_06_20-PM-04_12_11
Last ObjectModification: 2015_11_25-PM-03_37_49

Theory : rules


Home Index