modal/examples/arithmetic.modal

<> (add (s ?x) (s ?y)) (s (add ?x (s ?y)))
<> (add (s ?x) (0)) (s ?x)
<> (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)))))

factorial (s (s (s (s (s (0))))))