Nuprl Rule : callbyvalueAtom
H ⊢ 0 ≤ eval x = a in 0
BY callbyvalueAtom ()
H ⊢ a ∈ Atom
Definitions occuring in rule :
sqle: s ≤ t,
callbyvalue: callbyvalue,
natural_number: $n,
member: t ∈ T,
atom: Atom,
axiom: Ax
Latex:
H \mvdash{} 0 \mleq{} eval x = a in 0
BY callbyvalueAtom ()
H \mvdash{} a \mmember{} Atom
Date html generated:
2019_06_20-PM-04_12_27
Last ObjectModification:
2015_11_25-PM-03_46_58
Theory : rules
Home
Index