Nuprl Rule : reverse_direct_computation_hypothesis

x:A @lvl, J ⊢ ext t

  BY reverse_direct_computation_hypothesis #$i S
     
     Let CallLisp(REVERSE-DIRECT-COMPUTATION-HYPOTHESIS)
  x:B @lvl, J ⊢ ext t


Latex:
H  x:A  @lvl,  J  \mvdash{}  T  ext  t

    BY  reverse\_direct\_computation\_hypothesis  \#\$i  S
         
          Let  B  =  CallLisp(REVERSE-DIRECT-COMPUTATION-HYPOTHESIS)
    H  x:B  @lvl,  J  \mvdash{}  T  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