Nuprl Rule : decideEquality
H ⊢ case e1 of inl(x1) => l1 | inr(y1) => r1 = case e2 of inl(x2) => l2 | inr(y2) => r2 ∈ T[e1/z]
BY decideEquality z.T (A + B) u v w ()
H ⊢ e1 = e2 ∈ (A + B)
H u:A, w:(e1 = (inl u) ∈ (A + B)) ⊢ l1[u/x1] = l2[u/x2] ∈ T[inl u/z]
H v:B, w:(e1 = (inr v ) ∈ (A + B)) ⊢ r1[v/y1] = r2[v/y2] ∈ T[inr v /z]
Definitions occuring in rule :
decide: case b of inl(x) => s[x] | inr(y) => t[y],
inl: inl x,
union: left + right,
equal: s = t ∈ T,
inr: inr x ,
axiom: Ax
Latex:
H \mvdash{} case e1 of inl(x1) => l1 | inr(y1) => r1 = case e2 of inl(x2) => l2 | inr(y2) => r2
BY decideEquality z.T (A + B) u v w ()
H \mvdash{} e1 = e2
H u:A, w:(e1 = (inl u)) \mvdash{} l1[u/x1] = l2[u/x2]
H v:B, w:(e1 = (inr v )) \mvdash{} r1[v/y1] = r2[v/y2]
Date html generated:
2017_09_29-PM-05_44_46
Last ObjectModification:
2015_11_25-PM-03_37_43
Theory : rules
Home
Index