[SMT-LIB] How do I rewrite the following Simplify syntax into SMT-LIB?

[Ewa Rom]

I know Simplify and in Simplify syntax I can create recursive functions such as:(BG_PUSH (EQ (factorial 1) 1))
(BG_PUSH (FORALL (n ) (IMPLIES (> n 1) (EQ (factorial n) (* (factorial (- n 1)) n)))))
(EQ (factorial 5) 120)When I feed Z3 with Simplify syntax it returns Valid.I would like to use SMT-LIB format with Z3.How can I rewrite this in SMT-LIB format?I looked into the smt-lib standard document and I see :funs and :extrafuns, but I cannot figure out how to define these functions.
Thank you

Ewa Romanowicz

_________________________________________________________________
Keep in touch and up to date with friends and family. Make the connection now.
http://www.microsoft.com/windows/windowslive/