Nuprl Definition : decide2
case x,y
of inl(a),inl(b) => ll[a; b]
| inl(a),inr(b) => lr[a; b]
| inr(a),inl(b) => rl[a; b]
| inr(a),inr(b) => rr[a; b] ==
case x
of inl(a) =>
case y of inl(b) => ll[a; b] | inr(b) => lr[a; b]
| inr(a) =>
case y of inl(b) => rl[a; b] | inr(b) => rr[a; b]
Definitions occuring in Statement :
decide: case b of inl(x) => s[x] | inr(y) => t[y]
Definitions occuring in definition :
decide: case b of inl(x) => s[x] | inr(y) => t[y]
FDL editor aliases :
decide2
Latex:
case x,y
of inl(a),inl(b) => ll[a; b]
| inl(a),inr(b) => lr[a; b]
| inr(a),inl(b) => rl[a; b]
| inr(a),inr(b) => rr[a; b] ==
case x
of inl(a) =>
case y of inl(b) => ll[a; b] | inr(b) => lr[a; b]
| inr(a) =>
case y of inl(b) => rl[a; b] | inr(b) => rr[a; b]
Date html generated:
2016_05_15-PM-05_30_13
Last ObjectModification:
2015_09_23-AM-07_54_48
Theory : general
Home
Index