fml ::=
        | atomic_fml
        | UNOP fml
        | QUANT VAR fml
        | fml BINOP fml
        | LPAR fml RPAR
        | LBR fml RBR

atomic_fml ::=
        | PREFIX_PRED
        | PREFIX_PRED par_terms
        | term INFIX_PRED term
        | term NEG_INFIX_PRED term

par_terms ::=
        | LPAR terms RPAR
        | LBR terms RBR

terms ::=
        | term
        | term COMMA terms

term ::=
        | VAR
        | PREFIX_FUNC
        | PREFIX_FUNC par_terms
        | term INFIX_FUNC term
        | term POSTFIX_FUNC
        | LPAR term RPAR
        | LBR term RBR


UNOP ::=
        | "¬" | "\neg" | "~"

QUANT ::=
        | "∀" | "\forall" | "\A"
        | "∃" | "\exists" | "\E"

BINOP ::=
        | "→" | "\to"   | "\rightarrow" | "->"
        | "∧" | "\land" | "\wedge"      | "&"
        | "∨" | "\lor"  | "\vee"
        | "↔" | "\leftrightarrow"       | "<->"

LPAR ::= "("

RPAR ::= ")"

LBR ::= "["

RBR ::= "]"

COMMA ::= ","

VAR ::= ['u' - 'z'] (['_' '.'] | ['a' - 'z'] | ['0' - '9'] | subscript)*

PREFIX_PRED ::= (['A' - 'Z'] | upper_case_greek) (['_' '.'] | ['A' - 'Z'] | ['a' - 'z'] | ['0' - '9'] | subscript | upper_case_greek | lower_case_greek)*

INFIX_PRED ::=
        | "="
        | "<"
        | ">"
        | "≤" | "\leq" 
        | "≥" | "\geq"
        | "∈" | "\in"
        | "⊂" | "\subset"
        | "⊆" | "\subseteq"

NEG_INFIX_PRED ::=
        | "≠" | "\neq" 
        | "∉" | "\not\in" | "\not \in" | "\notin"

PREFIX_FUNC ::=
        | (['a' - 't'] | lower_case_greek) (['_' '.'] | ['a' - 'z'] | ['0' - '9'] | subscript | lower_case_greek)*
        | ['0' - '9']+

INFIX_FUNC ::=
        | "+"
        | "×" | "\times" 
        | "*"
        | "·" | "\cdot" 
        | "-"
        | "∩" | "\cap" 
        | "∪" | "\cup"
        | "^"

POSTFIX_FUNC ::=
        | "'"
        | superscript

subscript ::= "₀" | "₁" | "₂" | "₃" | "₄" | "₅" | "₆" | "₇" | "₈" | "₉"
superscript ::= "⁰" | "¹" | "²" | "³" | "⁴" | "⁵" | "⁶" | "⁷" | "⁸" | "⁹"
upper_case_greek ::= "Γ" | "Δ" | "Φ" | "Λ" | "Ω" | "Π" | "Σ" | "Θ" | "Ψ"
lower_case_greek ::= "α" | "β" | "γ" | "δ" | "φ" | "ψ" | "κ" | "λ" | "ω" | "ρ" | "σ" | "τ" | "π" | "χ" | "ι" | "η"