Nuprl Rule : atom2_eqExceptionCases
H ⊢ a = b ∈ T
BY atom2_eqExceptionCases x y t u z w ()
H ⊢ is-exception(if t=2 u then z else w)
H x:(t ∈ Atom2), y:(u ∈ Atom2) ⊢ a = b ∈ T
H x:(t ∈ Atom2), y:is-exception(u) ⊢ a = b ∈ T
H x:is-exception(t) ⊢ a = b ∈ T
H ⊢ t ∈ Base
H ⊢ u ∈ Base
Definitions occuring in rule :
atom_eq: atomeqn def,
atom: Atom$n
,
is-exception: is-exception(t)
,
equal: s = t ∈ T
,
member: t ∈ T
,
base: Base
,
axiom: Ax
Latex:
H \mvdash{} a = b
BY atom2\_eqExceptionCases x y t u z w ()
H \mvdash{} is-exception(if t=2 u then z else w)
H x:(t \mmember{} Atom2), y:(u \mmember{} Atom2) \mvdash{} a = b
H x:(t \mmember{} Atom2), y:is-exception(u) \mvdash{} a = b
H x:is-exception(t) \mvdash{} a = b
H \mvdash{} t \mmember{} Base
H \mvdash{} u \mmember{} Base
Date html generated:
2019_06_20-PM-04_12_00
Last ObjectModification:
2015_11_25-PM-03_47_04
Theory : rules
Home
Index