Nuprl Rule : applyInt
This rule proved as lemma rule_apply_int_true in file rules/rules_apply_callbyvalue.v
at https://github.com/vrahli/NuprlInCoq
H ⊢ m b ≤ ⊥
BY applyInt ()
H ⊢ m ∈ ℤ
Definitions occuring in rule :
sqle: s ≤ t,
apply: f a,
bottom: ⊥,
member: t ∈ T,
int: ℤ,
axiom: Ax
Latex:
H \mvdash{} m b \mleq{} \mbot{}
BY applyInt ()
H \mvdash{} m \mmember{} \mBbbZ{}
Date html generated:
2019_06_20-PM-04_12_27
Last ObjectModification:
2016_07_08-PM-03_49_07
Theory : rules
Home
Index