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