<?xml version="1.0" encoding="UTF-8"?>
<Assert xmlns="http://www.ruleml.org/0.88/xsd" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:schemaLocation="http://www.ruleml.org/0.88/xsd 
http://www.ruleml.org/0.88/xsd/equalog.xsd">
<!-- a flattened factorial definition -->
<content>
<And innerclose="universal">
<formula>
<Equal>
<side>
<Nano>
<opf>
<Fun>fac</Fun>
</opf>
<arg index="1">
<Ind>0</Ind>
</arg>
</Nano>
</side>
<side>
<Ind>1</Ind>
</side>
</Equal>
</formula>
<formula>
<Implies>
<head>
<Equal>
<side>
<Nano>
<opf>
<Fun>fac</Fun>
</opf>
<arg index="1">
<Var>n</Var>
</arg>
</Nano>
</side>
<side>
<Var>r</Var>
</side>
</Equal>
</head>
<body>
<And>
<formula>
<Atom>
<opr>
<Rel>greater</Rel>
</opr>
<arg index="1">
<Var>n</Var>
</arg>
<arg index="2">
<Ind>0</Ind>
</arg>
</Atom>
</formula>
<formula>
<Equal>
<side>
<Var>m</Var>
</side>
<side>
<Nano>
<opf>
<Fun>-</Fun>
</opf>
<arg index="1">
<Var>n</Var>
</arg>
<arg index="2">
<Ind>1</Ind>
</arg>
</Nano>
</side>
</Equal>
</formula>
<formula>
<Equal>
<side>
<Var>f</Var>
</side>
<side>
<Nano>
<opf>
<Fun>fac</Fun>
</opf>
<arg index="1">
<Var>m</Var>
</arg>
</Nano>
</side>
</Equal>
</formula>
<formula>
<Equal>
<side>
<Var>r</Var>
</side>
<side>
<Nano>
<opf>
<Fun>*</Fun>
</opf>
<arg index="1">
<Var>n</Var>
</arg>
<arg index="2">
<Var>f</Var>
</arg>
</Nano>
</side>
</Equal>
</formula>
</And>
</body>
</Implies>
</formula>
</And>
</content>
</Assert>