#ignore + - \ / ^ & #axiom S(0,0) #rules S(a,c)->F(0)-[[S(a+1,0)]+S(a+1,0)]+F(0)[+F(0)S(a+1,0)]-S(a+1,0) F(x) -> F(x+1)F(x+1)