Nuprl Rule : tryReduceValue
This rule proved as lemma rule_try_reduce_value_true in file rules/rules_exception2.v
at https://github.com/vrahli/NuprlInCoq
H ⊢ t1?n:x.t2 ~ if n=2 n then t1 else ⊥
BY tryReduceValue ()
H ⊢ 0 ≤ eval t1; 0
Definitions occuring in rule :
sqequal: s ~ t,
atom_eq: atomeqn def,
bottom: ⊥,
sqle: s ≤ t,
callbyvalue: callbyvalue,
natural_number: $n,
axiom: Ax
Latex:
H \mvdash{} t1?n:x.t2 \msim{} if n=2 n then t1 else \mbot{}
BY tryReduceValue ()
H \mvdash{} 0 \mleq{} eval t1; 0
Date html generated:
2019_06_20-PM-04_12_17
Last ObjectModification:
2016_07_08-PM-03_48_46
Theory : rules
Home
Index