for all a, b, c, d, if a > b > c > d, then a > d
you get the following things:
(1) ◇◇◇A |- ◇A
(2) ◇◇0 |- ◇0
I put (1) there because it's "what you expect", from supertransitivity. (2) is the surprise, and it follows from ◇ allowing you to get access to the 0 on the left not because it's at a world that you can actually get the right-hand-side to be located at, but because hypothetically under a sequence of imaginary ◇L invocations, you could. This baked-in transitivity-ish behavior I find weird.
But! Yesterday I think I more or less figured out how to incorporate it into my focus-preserving-encoding worldview, and so I can sleep again at night. This means that my earlier suspicion that it didn't cut eliminate was wrong, but it's also the case that the funny side condition on 0 can be permuted up to a side condition on the ◇L rule, meaning that my general intuition about nonstandard 0 rules is still corroborated by this experience.
