Go up to 4 ATerm-instances for CASL and ELAN
Go forward to 4.2 Efix

4.1 FCasEnv

FCasEnv ATerms are term-like structures used to represent the output parse trees of flat CASL specifications. The FCasEnv format has been designed for the interaction with theorem-provers and automated deduction tools like rewrite engines. It is generated by the CASL tool set 3 developed in Bremen [Mos00]. For instance, given the CASL specification presented in Example 3.1.2, we obtain the following FCasEnv, which includes what we are interested in: 
fcasenv(f-global-entry-tuple*([
 f-global-entry-tuple(
  WORDS("GT_pred"),
  f-spec-defn-env(
   ...,
   ext-signature(
    signature(
     local-env(
      subsort-env(subsort-entry-tuple*([
       CASFIX-subsort-entry-tuple("Integ")])),
      var-env(var-entry-tuple*([])),
      fun-env(fun-entry-tuple*([
       CASFIX-fun-entry-tuple("plus: Integ * Integ -> Integ"),
       CASFIX-fun-entry-tuple("s: Integ -> Integ"),
       CASFIX-fun-entry-tuple("zero : Integ")])),
      pred-env(pred-entry-tuple*([
       CASFIX-pred-entry-tuple("__ > __ : Integ * Integ")]))),
     anno*([])
    ),
    ...,
    formula*([
     CASFIX-formula("plus(zero,y) = y"),
     CASFIX-formula("plus(s(x),y) = s(plus(x,y))"),
     CASFIX-formula("s(x) > s(y) <=> x > y"),
     CASFIX-formula("s(x) > zero"),
     CASFIX-formula("not (zero > s(x))"),
     CASFIX-formula("not (zero > zero)")]),
 ...])))
Subterms with CASFIX-... top symbols denote terms which are not detailed here for sake of conciseness.
CoFI Note: T-9 -- Version: 1 -- November 10, 2000.
Comments to FirstName.LastName@loria.fr

Go up to 4 ATerm-instances for CASL and ELAN
Go forward to 4.2 Efix