Nuprl Rule : callbyvalueLess
H ⊢ (a ∈ ℤ) ∧ (b ∈ ℤ) ext <Ax, Ax>
BY callbyvalueLess u v ()
H ⊢ 0 ≤ eval if (a) < (b) then u else v; 0
H ⊢ a ∈ Base
H ⊢ b ∈ Base
Definitions occuring in rule :
and: P ∧ Q,
int: ℤ,
pair: <a, b>,
sqle: s ≤ t,
callbyvalue: callbyvalue,
less: if (a) < (b) then c else d,
natural_number: $n,
member: t ∈ T,
base: Base,
axiom: Ax
Latex:
H \mvdash{} (a \mmember{} \mBbbZ{}) \mwedge{} (b \mmember{} \mBbbZ{}) ext <Ax, Ax>
BY callbyvalueLess u v ()
H \mvdash{} 0 \mleq{} eval if (a) < (b) then u else v; 0
H \mvdash{} a \mmember{} Base
H \mvdash{} b \mmember{} Base
Date html generated:
2019_06_20-PM-04_12_04
Last ObjectModification:
2015_11_25-PM-03_46_59
Theory : rules
Home
Index