Nuprl Rule : callbyvalueInt

This rule proved as lemma rule_callbyvalue_int_true3 in file rules/rules_number.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ 0 ≤ eval in 0

  BY callbyvalueInt ()
  
  H  ⊢ a ∈ ℤ



Definitions occuring in rule :  sqle: s ≤ t callbyvalue: callbyvalue natural_number: $n member: t ∈ T int: axiom: Ax

Latex:
H    \mvdash{}  0  \mleq{}  eval  x  =  a  in  0

    BY  callbyvalueInt  ()
   
    H    \mvdash{}  a  \mmember{}  \mBbbZ{}



Date html generated: 2019_06_20-PM-04_12_26
Last ObjectModification: 2016_07_08-PM-03_49_04

Theory : rules


Home Index