Nuprl Rule : callbyvalueSpread
This rule proved as lemma rule_halt_spread_true in file rules/rules_halts_spread.v
at https://github.com/vrahli/NuprlInCoq
H ⊢ p ∈ Top × Top
BY callbyvalueSpread y,z.a ()
H ⊢ 0 ≤ eval let y,z = p in a; 0
Definitions occuring in rule :
member: t ∈ T,
product: x:A × B[x],
top: Top,
sqle: s ≤ t,
callbyvalue: callbyvalue,
spread: spread def,
natural_number: $n,
axiom: Ax
Latex:
H \mvdash{} p \mmember{} Top \mtimes{} Top
BY callbyvalueSpread y,z.a ()
H \mvdash{} 0 \mleq{} eval let y,z = p in a; 0
Date html generated:
2019_06_20-PM-04_12_00
Last ObjectModification:
2016_07_08-PM-03_49_02
Theory : rules
Home
Index