Nuprl Rule : callbyvalueIsatom1
This rule proved as lemma rule_callbyvalue_can_test_true in file rules/rules_cft_callbyvalue.v
at https://github.com/vrahli/NuprlInCoq
H ⊢ (p)↓
BY callbyvalueIsatom1 a b ()
H ⊢ 0 ≤ eval isatom1(p;a;b); 0
Definitions occuring in rule :
has-value: (a)↓,
sqle: s ≤ t,
callbyvalue: callbyvalue,
isatom1: isatom1(z;a;b),
natural_number: $n,
axiom: Ax
Latex:
H \mvdash{} (p)\mdownarrow{}
BY callbyvalueIsatom1 a b ()
H \mvdash{} 0 \mleq{} eval isatom1(p;a;b); 0
Date html generated:
2019_06_20-PM-04_12_21
Last ObjectModification:
2016_07_08-PM-03_49_04
Theory : rules
Home
Index