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

Add Z y => y;
Add (S x) y => S (Add x y);

Mult Z y => Z;
Mult (S x) y => Add y (Mult x y);

Compute x => x;
}

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

Down Z => Up Z;
Down (S x) => S (Down x);
Down (Add x y) => Add (Down x) y;
Down (Mult x y) => Mult (Down x) y;

S (Up x) => Up (S x);

Add (Up Z) x => Down x;
Add (Up (S x)) y => S (Down (Add x y));

Mult (Up Z) y => Up Z;
Mult (Up (S x)) y => Down (Add y (Mult x y));

Compute x => Down (x);

Up (x) => x;

.
EOF