<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

pl/miw/miw08_xtt_rif/rif_minicases/fst.txt · ostatnio zmienione: 2019/06/27 15:50 (edycja zewnętrzna)
www.chimeric.de Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0