Alphabet

nil:list
cons:[nat × list] ⟶ list
op:[nat → nat × nat → nat] ⟶ nat → nat
implode:[list × nat → nat × nat] ⟶ nat
explode:[list × nat → nat × nat] ⟶ nat

Variables

F:nat → nat
G:nat → nat
H:nat
T:list
X:nat

Rules

op(F, G) · X⇒F · (G · X)
implode(nil, F, X)⇒X
implode(cons(H, T), F, X)⇒implode(T, F, F · X)
explode(nil, F, X)⇒X
explode(cons(H, T), F, X)⇒explode(T, op(F, F), F · X)