Nuprl Rule : isAtom1ReduceTrue
H ⊢ isatom1(z;a;b) ~ a
BY isAtom1ReduceTrue ()
H ⊢ z = z ∈ Atom1
Definitions occuring in rule :
sqequal: s ~ t,
isatom1: isatom1(z;a;b),
equal: s = t ∈ T,
atom: Atom$n,
axiom: Ax
Latex:
H \mvdash{} isatom1(z;a;b) \msim{} a
BY isAtom1ReduceTrue ()
H \mvdash{} z = z
Date html generated:
2019_06_20-PM-04_12_27
Last ObjectModification:
2015_11_25-PM-03_44_28
Theory : rules
Home
Index