Nuprl Rule : direct_computation_hypothesis

H x:A @lvl, J ⊢ T ext t

  BY direct_computation_hypothesis #$i S
     
     Let B = CallLisp(DIRECT-COMPUTATION-HYPOTHESIS)
  H x:B @lvl, J ⊢ T ext t

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

    BY  direct\_computation\_hypothesis  \#\$i  S
         
          Let  B  =  CallLisp(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