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