{ 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