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.