2008/05/22

Simple Identity Proved

I've been puzzled by a naïve-looking identity ΛR . C = Λ(R . C) . C (where C is a coreflexive) for a few days. Since its truth is evident when one examines it in the pointwise way, I believed that it can be proven using tabulations, and luckily I was right. The key is to tabulate C as f . fº, which can be easily justified:

  f . gº ⊆ id
≡   { shunting of functions }
  f ⊆ g
≡   { inclusion of functions is equality }
  f = g
Now we reason:
  Λ(R . C) . C
=   { tabulate C as f . fº }
  Λ(R . f . fº) . f . fº
=   { fusion }
  Λ(R . f . fº . f) . fº
=   { f is simple }
  Λ(R . f) . fº
=   { fusion (backwards) }
  ΛR . f . fº
=   { tabulation of C }
  ΛR . C
And the puzzle is solved.

--
Is it possible to prove the identity without using tabulations?

Labels: