Usage
=====

Usage: fort-h [OPTION...] FORMULA FILE.trs...

  -h, -?   --help              print usage information
  -v       --verbose           verbose output
  -w       --witness           enable witness generation
  -c FILE  --certificate=FILE  write certificate to FILE
  -i       --info              enable additional information in the certificate

FILE Syntax
-----------

The TRS file syntax follow the format used by COPS
  TRS Format: http://project-coco.uibk.ac.at/problems/trs.php

It also support two TRSs per FILE with the COM format
  COM Format: http://project-coco.uibk.ac.at/2019/categories/commutation.php


FORMULA Syntax
--------------

The syntax for <formula> is given by the following EBNF:

<formula>     = <property>
              | <var> <relation> <var>
              | '~' <formula>
              | <formula> <connective> <formula>
              | <quantifier> <varlist> ( <formula> )
              | <indices> <formula>
              | ( <formula> )
<connective>  = '&' | '|' | '=>' | '<=>'
<relation>    = '->' | '->=' | '->+' | '->*' | '->!' | '-||->'
              | '->e' | '->be' | '->e+' | '->be+' | '->e*' | '->be*'
              | '<->' | '<->*' | 'join' | 'meet' | '='
              | '<-' | '=<-' | '+<-' | '*<-' | '<-!' | '<-||-'
              | 'e<-' | 'be<-' | '+e<-' | '+be<-' | '*e<-' | '*be<-'
              | '->e=' | '->be=' | '=e<-' | '=be<-'
<quantifier>  = forall | exists
<property>    = CR | WCR | SCR | SCR(<gtt_rel>) | WN | UN | UN(<gtt_rel>)
              | UNC | NFP | SN | diamond | diamond(<formula2>)
              | Com(<indices>, <indices>) | LCom(<indices>, <indices>)
              | GCR | GWCR | WSCR | GSCR(<gtt_rel>) | GUN | GUN(<gtt_rel>)
              | GUNC | GNFP | Gdiamond | Gdiamond(<formula2>)
              | GCom(<indices>, <indices>) | GLCom(<indices>, <indices>)
              | WCR(<gtt_rel>) | GWCR(<gtt_rel>)

              | CR(<var>) | WCR(<var>) | SCR(<var>)
              | SCR(<gtt_rel>, <var>) | WN(<var>) | UN(<var>)
              | UN(<gtt_rel>, <var>) | NFP(<var>) | SN(<var>)
              | diamond(<var>) | diamond(<formula2>, <var>)
              | NF(<var>) | Fin(<formula2>, <var>)
              | Inf(<formula2>, <var>)
<formula2>    = <relation>
              | '~' <formula2>
              | <formula2> <connective> <formula2>
              | ( <formula2> )
<gtt_rel>     = '-||->' | '->'
<indices>     = '['<nat_list>']'

Here <nat> denotes a natural number, and <var> any nonempty sequence of
alphanumeric symbols starting with a letter. <nat_list> and
<var_list> are comma separated lists of <nat>s or <var>s, respectively.

Any <relation> denotes the expected rewrite relation.
The addition of 'e' (as in '->e') denotes rewriting at the root,
'be' ('->be') below the root.