{ This is what it would look like in a sane term-rewriting system:

Seq (Seq a b) c => Seq a (Seq b c);
Tag q (Tag q a) => Tag q a;
Seq (Tag q a) (Tag q b) => Tag q (Seq a b);

Tag Emph (Tag Bold a) => Tag Bold (Tag Emph a);
Tag Maj (Tag Bold a) => Tag Bold (Tag Maj a);
Tag Maj (Tag Emph a) => Tag Emph (Tag Maj a);

SNF a => a;
}

{ This is what it looks like in O'Cult: }

Down A => Up A;
Down B => Up B;

Down (Seq a b) => Seq (Down a) b;
Down (Tag q a) => Tag q (Down a);

Seq (Up a) b => Seq a (Down b);

Seq (Seq a b) (Up c) => Seq a (Down (Seq b c));
Tag q (Up (Tag q a)) => (Up (Tag q a));
Seq (Tag q a) (Up (Tag q b)) => Tag q (Down (Seq a b));

Tag Emph (Up (Tag Bold a)) => Tag Bold (Down (Tag Emph a));
Tag Maj (Up (Tag q a)) => Tag q (Down (Tag Maj a));

Seq a (Up b) => Up (Seq a b);
Tag q (Up a) => Up (Tag q a);

SNF x => Down (x);

Up (x) => x;

.
EOF