Certificates use an s-expression based format:
| ⟨nat⟩ ::= | 0 | 1 | 2 | ... | ||
| ⟨trs⟩ ::= | ⟨nat⟩ | ⟨nat⟩- | ||
| ⟨gtt⟩ ::= | (root-step(⟨trs⟩ + )) | (gsteps(⟨trs⟩ + )) | (inverse⟨gtt⟩) | ||
| | | (union⟨gtt⟩⟨gtt⟩) | (acomp⟨gtt⟩⟨gtt⟩) | (gcomp⟨gtt⟩⟨gtt⟩) | ||
| | | (inter⟨gtt⟩⟨gtt⟩) | (atc⟨gtt⟩) | (gtc⟨gtt⟩) | (acomplement⟨gtt⟩) | ||
| ⟨pos⟩ ::= | >= | e | > | ||
| ⟨num⟩ ::= | >= | 1 | > | ||
| ⟨rr1⟩ ::= | (terms) | (nf(⟨trs⟩ + )) | (inf⟨rr2⟩) | ||
| | | (proj(1|2)⟨rr2⟩) | (union⟨rr1⟩⟨rr1⟩) | ||
| | | (inter⟨rr1⟩⟨rr1⟩) | (diff⟨rr1⟩⟨rr1⟩) | ||
| ⟨rr2⟩ ::= | (gtt⟨gtt⟩⟨pos⟩⟨num⟩) | (product⟨rr1⟩⟨rr1⟩) | (id⟨rr1⟩) | ||
| | | (union⟨rr2⟩⟨rr2⟩) | (inter⟨rr2⟩⟨rr2⟩) | (diff⟨rr2⟩⟨rr2⟩) | ||
| | | (comp⟨rr2⟩⟨rr2⟩) | (inverse⟨rr2⟩) | (equality) | (reflcl⟨rr2⟩) | ||
| | | (step(⟨trs⟩ + )) | (step=(⟨trs⟩ + )) | (step+(⟨trs⟩ + )) | ||
| | | (step*(⟨trs⟩ + )) | (step!(⟨trs⟩ + )) | (par-step(⟨trs⟩ + )) | ||
| | | (root-step(⟨trs⟩ + )) | (root-step=(⟨trs⟩ + )) | ||
| | | (root-step+(⟨trs⟩ + )) | (root-step*(⟨trs⟩ + )) | ||
| | | (non-root-step(⟨trs⟩ + )) | (non-root-step=(⟨trs⟩ + )) | ||
| | | (non-root-step+(⟨trs⟩ + )) | (non-root-step*(⟨trs⟩ + )) | ||
| | | (meet(⟨trs⟩ + )) | (join(⟨trs⟩ + )) | ||
| ⟨var⟩ ::= | ⟨nat⟩ | ||
| ⟨term⟩ ::= | ⟨var⟩ | ||
| ⟨formula⟩ ::= | (rr1⟨rr1⟩⟨term⟩) | (rr2⟨rr2⟩⟨term⟩⟨term⟩) | ||
| | | (and⟨formula⟩*) | (or⟨formula⟩*) | (not⟨formula⟩) | ||
| | | (forall⟨formula⟩) | (exists⟨formula⟩) | (true) | (false) | ||
| | | (restrict⟨formula⟩(⟨trs⟩ + )) | ||
| ⟨item⟩ ::= | ⟨nat⟩ | ||
| ⟨itemref⟩ ::= | ⟨nat⟩ | ||
| ⟨fpos⟩ ::= | (⟨nat⟩ + ) | ||
| ⟨equivalence⟩ ::= | distrib-and-or | distrib-or-and | ||
| ⟨inference⟩ ::= | (rr1⟨rr1⟩⟨term⟩) | (rr2⟨rr2⟩⟨term⟩⟨term⟩) | (and⟨itemref⟩*) | ||
| | | (or⟨itemref⟩*) | (not⟨itemref⟩) | (exists⟨itemref⟩) | ||
| | | (rename⟨itemref⟩(⟨var⟩*)) | (nnf⟨itemref⟩) | ||
| | | (replace⟨itemref⟩⟨fpos⟩⟨equivalence⟩) | ||
| ⟨info⟩ ::= | (size⟨nat⟩⟨nat⟩⟨nat⟩) | ||
| ⟨proof⟩ ::= | (⟨item⟩⟨inference⟩⟨formula⟩⟨info⟩*)⟨proof⟩ | ||
| | | (empty)⟨itemref⟩) | (nonempty⟨itemref⟩) | ||