[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Specification term
data specification 
   comment: definition of the free data type of terms. Instead
of (t1 t2) we write t1 _ t2 (the selectors are .1 and .2,
ap tests a term to be an application).;
   using nat
   term =  . _ . ( . .1 : term;  . .2 : term) prio 9 left  with ap | K | S;
   variables 
      t : term; 
   size functions # : term → nat;
end data specification