Nuprl Rule : exceptionAtomeq
H ⊢ if x=exception(u; v) then y else z fi ~ exception(u; v)
BY exceptionAtomeq ()
H ⊢ x ∈ Atom
Definitions occuring in rule :
sqequal: s ~ t,
atom_eq: if a=b then c else d fi ,
member: t ∈ T,
atom: Atom,
axiom: Ax
Latex:
H \mvdash{} if x=exception(u; v) then y else z fi \msim{} exception(u; v)
BY exceptionAtomeq ()
H \mvdash{} x \mmember{} Atom
Date html generated:
2019_06_20-PM-04_12_20
Last ObjectModification:
2015_11_25-PM-03_47_02
Theory : rules
Home
Index