Nuprl Rule : approximateComputation

H  ⊢ C ext !((!\\v.e) Ax)

  BY approximateComputation t v
     
     Let a () = CallLisp(LISP-COMPUTATION)
  H v:(a ≤ t) ⊢ C ext e


Definitions occuring in rule :  axiom: Ax,  sqle: s ≤ t
Latex:
H    \mvdash{}  C  ext  !((!\mbackslash{}\mbackslash{}v.e)  Ax)

    BY  approximateComputation  t  v
         
          Let  a  ()  =  CallLisp(LISP-COMPUTATION)
    H  v:(a  \mleq{}  t)  \mvdash{}  C  ext  e


Date html generated: 2019_06_20-PM-04_11_54
Last ObjectModification: 2017_05_26-PM-03_41_01

Theory : rules


Home Index