channel CIO {
	out payment(p, purchase(x)) == x
}

channel C1 {
	in payment(p, update1(y)) == y
	out loyalty(l, update1(y)) == floor(y * 0.05)
}

channel C2 {
	in payment(p, update2(z)) == z
	out history(h, update2(z)) == cons(z, h)
}

channel C3 {
	in history(h, update3(u)) == u
	out total(t, update3(u)) == sum(u)
}