Nuprl Rule : callbyvalueDecide
This rule proved as lemma rule_halt_decide_true3 in file rules/rules_halts_decide.v
at https://github.com/vrahli/NuprlInCoq
H ⊢ d ∈ Top + Top
BY callbyvalueDecide y.a z.b ()
H ⊢ 0 ≤ eval case d of inl(y) => a | inr(z) => b; 0
H ⊢ d ∈ Base
Definitions occuring in rule :
union: left + right,
top: Top,
sqle: s ≤ t,
callbyvalue: callbyvalue,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
natural_number: $n,
member: t ∈ T,
base: Base,
axiom: Ax
Latex:
H \mvdash{} d \mmember{} Top + Top
BY callbyvalueDecide y.a z.b ()
H \mvdash{} 0 \mleq{} eval case d of inl(y) => a | inr(z) => b; 0
H \mvdash{} d \mmember{} Base
Date html generated:
2019_06_20-PM-04_11_48
Last ObjectModification:
2016_07_08-PM-03_49_05
Theory : rules
Home
Index