Nuprl Rule : callbyvalueIntEq
H ⊢ (a ∈ ℤ) ∧ (b ∈ ℤ) ext <Ax, Ax>
BY callbyvalueIntEq 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,
int_eq: 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 callbyvalueIntEq 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