<Group>
<sentence>
<Forall>
<declare><Var>T</Var></declare>
<declare><Var>P</Var></declare>
<declare><Var>N</Var></declare>
<formula>
<Implies>
<if>
<And>
<formula>
<Exists>
<declare><Var>X</Var></declare>
<formula>
<Frame>
<object>
<Member>
<lower><Var>T</Var></lower>
<upper><Const type="rif:iri">tree:t</Const></upper>
</Member>
</object>
<slot>
<Prop>
<key><Const type="rif:iri">tree:p</Const></key>
<val><Var>P</Var></val>
</Prop>
</slot>
<slot>
<Prop>
<key><Const type="rif:iri">tree:n</Const></key>
<val><Var>N</Var></val>
</Prop>
</slot>
</Frame>
</formula>
</Exists>
</formula>
<formula>
<Equal>
<side><Var>P</Var></side>
<side><Var>X</Var></side>
</Equal>
</formula>
</And>
</if>
<then>
<Atom>
<op><Const type="rif:iri">op:assert</Const></op>
<arg>
<External>
<content>
<Expr>
<op><Const type="rif:iri">f</Const></op>
<arg><Var>N</Var></arg>
</Expr>
</content>
</External>
</arg>
</Atom>
</then>
</Implies>
</formula>
</Forall>
</sentence>
<sentence>
<Forall>
<declare><Var>F</Var></declare>
<formula>
<Implies>
<if>
<And>
<formula>
<Exists>
<declare><Var>T</Var></declare>
<declare><Var>P</Var></declare>
<declare><Var>N</Var></declare>
<formula>
<Frame>
<object>
<Member>
<lower><Var>T</Var></lower>
<upper><Const type="rif:iri">tree:t</Const></upper>
</Member>
</object>
<slot>
<Prop>
<key><Const type="rif:iri">tree:p</Const></key>
<val><Var>P</Var></val>
</Prop>
</slot>
<slot>
<Prop>
<key><Const type="rif:iri">tree:n</Const></key>
<val><Var>N</Var></val>
</Prop>
</slot>
</Frame>
</formula>
</Exists>
</formula>
<formula>
<External>
<content>
<Atom>
<op><Const type="rif:iri">f</Const></op>
<arg><Var>F</Var></arg>
</Atom>
<content>
</External>
</formula>
<formula>
<Equal>
<side><Var>P</Var></side>
<side><Var>F</Var></side>
</Equal>
</formula>
<formula>
<External>
<content>
<Atom>
<op><Const type="rif:iri">op:not-equal</Const></op>
<arg><Var>N</Var></arg>
<arg><Var>F</Var></arg>
</Atom>
</content>
</External>
</formula>
</And>
</if>
<then>
<Atom>
<op><Const type="rif:iri">op:assert</Const></op>
<arg>
<External>
<content>
<Expr>
<op><Const type="rif:iri">f</Const></op>
<arg><Var>N</Var></arg>
</Expr>
</content>
</External>
</arg>
</Atom>
</then>
</Implies>
</formula>
</Forall>
</sentence>
</Group>
Powrót