<> (add (s ?x) (s ?y)) ((s add ?x (s ?y))) <> (add (s ?y) (0)) ((s ?y)) <> (add (0) (s ?y)) ((s ?y)) <> (add (0) (0)) (0) <> (subtract (s ?x) (s ?y)) (subtract ?x ?y) <> (subtract (s ?x) (0)) (s ?x) <> (subtract (0) (s ?y)) (s ?y) <> (subtract (0) (0)) (0) <> (multiply (s ?x) (s ?y)) (add (s ?x) (multiply (s ?x) (subtract (s ?y) (s (0)))) <> (multiply (s ?x) (s (0)) (s ?x) <> (multiply (s (0)) (s ?y) (s ?y) <> (multiply (s ?x) (0)) (0) <> (multiply (0) (s ?x)) (0) <> (?x + ?y) (add ?x ?y) <> (?x - ?y) (subtract ?x ?y) <> (?x * ?y) (multiply ?x ?y) <> (factorial (s (0))) ((s (0))) <> (factorial (s ?x)) ((s ?x) * factorial ((s ?x) - (s (0)))) (s (0)) * (s (s (0)))