Nuprl Rule : callbyvalueReduce
This rule proved as lemma rule_callbyvalue_reduce_true3 in file rules_callbyvalue.v
at https://github.com/vrahli/NuprlInCoq ⋅
H ⊢ eval x = a in B ~ t
BY callbyvalueReduce ()
H ⊢ B[a/x] ~ t
H ⊢ 0 ≤ eval x = a in 0
Definitions occuring in rule :
sqequal: s ~ t,
sqle: s ≤ t,
callbyvalue: callbyvalue,
natural_number: $n,
axiom: Ax
Latex:
H \mvdash{} eval x = a in B \msim{} t
BY callbyvalueReduce ()
H \mvdash{} B[a/x] \msim{} t
H \mvdash{} 0 \mleq{} eval x = a in 0
Date html generated:
2019_06_20-PM-04_11_55
Last ObjectModification:
2016_07_09-PM-05_33_54
Theory : rules
Home
Index