Nuprl Rule : lessCases
H ⊢ C ext !((!\\x.if (t1) < (t2) then ea else eb) Ax)
BY lessCases x t1 t2 u v ()
H ⊢ t1 ∈ ℤ
H ⊢ t2 ∈ ℤ
H x:(∀[u,v:Base]. (if (t1) < (t2) then u else v ~ u)) ⊢ C ext ea
H x:(∀[u,v:Base]. (if (t1) < (t2) then u else v ~ v)) ⊢ C ext eb
Definitions occuring in rule :
member: t ∈ T,
int: ℤ,
axiom: Ax,
uall: ∀[x:A]. B[x],
base: Base,
sqequal: s ~ t,
less: if (a) < (b) then c else d
Latex:
H \mvdash{} C ext !((!\mbackslash{}\mbackslash{}x.if (t1) < (t2) then ea else eb) Ax)
BY lessCases x t1 t2 u v ()
H \mvdash{} t1 \mmember{} \mBbbZ{}
H \mvdash{} t2 \mmember{} \mBbbZ{}
H x:(\mforall{}[u,v:Base]. (if (t1) < (t2) then u else v \msim{} u)) \mvdash{} C ext ea
H x:(\mforall{}[u,v:Base]. (if (t1) < (t2) then u else v \msim{} v)) \mvdash{} C ext eb
Date html generated:
2019_06_20-PM-04_11_57
Last ObjectModification:
2015_11_25-PM-03_47_06
Theory : rules
Home
Index