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