Nuprl Rule : reverse_direct_computation

H  ⊢ T ext t

  BY reverse_direct_computation S
     
     Let C = CallLisp(REVERSE-DIRECT-COMPUTATION)
  H  ⊢ C 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