### (no subject)

Went to D's. It was fun for a while, but they turned up the music kind of loud and it got irritating. A pity, since a lot of people were there that weren't there usually and I didn't get much chance to talk to them.

I left feeling really bad because I thought I spotted a flaw in the math — I'm noticing this familiar pattern where my entire emotional state is temporarily contingent on the math working or not — but I got home and attacked it a little more in TeX, and I think I've got it working even more beautifully than before.

The structure I need on the set N of "occurrence contracts" for variables is currently the following:

I think this last axiom, particularly the way it has emerged as a requirement for two different lemmas in completely different ways, is very cute.

I left feeling really bad because I thought I spotted a flaw in the math — I'm noticing this familiar pattern where my entire emotional state is temporarily contingent on the math working or not — but I got home and attacked it a little more in TeX, and I think I've got it working even more beautifully than before.

The structure I need on the set N of "occurrence contracts" for variables is currently the following:

- There is an element 0 in N, for "variable must not occur".
- There is an element 1 in N, for "variable must occur exactly once".
- There is a preorder ≤ on the set N, which intuitively means "is more restrictive than"
- There is a ternary operation (x,y,z) ⇒ x + y z from triples in N to N
- This operation is ≤-monotone in all three arguments simultaneously
- The following algebraic identities hold, for all x,y,a,b,c,d:
- 0 + 1 a = a
- a + 0 b = a
- (a + x b) + (c + x d) y = (a + c y) + x (b + d y)

I think this last axiom, particularly the way it has emerged as a requirement for two different lemmas in completely different ways, is very cute.