Nuprl Rule : isatom1Cases
H ⊢ C ext !((!\\x.isatom1(t;ea;eb)) Ax)
BY isatom1Cases x t u v ()
H ⊢ 0 ≤ eval x = t in 0
H ⊢ t ∈ Base
H x:(t ∈ Atom1) ⊢ C ext ea
H x:(∀[u,v:Base]. (isatom1(t;u;v) ~ v)) ⊢ C ext eb
Definitions occuring in rule :
sqle: s ≤ t,
callbyvalue: callbyvalue,
natural_number: $n,
axiom: Ax,
member: t ∈ T,
atom: Atom$n,
uall: ∀[x:A]. B[x],
base: Base,
sqequal: s ~ t,
isatom1: isatom1(z;a;b)
Latex:
H \mvdash{} C ext !((!\mbackslash{}\mbackslash{}x.isatom1(t;ea;eb)) Ax)
BY isatom1Cases x t u v ()
H \mvdash{} 0 \mleq{} eval x = t in 0
H \mvdash{} t \mmember{} Base
H x:(t \mmember{} Atom1) \mvdash{} C ext ea
H x:(\mforall{}[u,v:Base]. (isatom1(t;u;v) \msim{} v)) \mvdash{} C ext eb
Date html generated:
2019_06_20-PM-04_12_28
Last ObjectModification:
2015_11_25-PM-03_47_05
Theory : rules
Home
Index