NAMING CONVENTIONS FOR METAVARIABLES

A,B    : arity
C,D    : candidate of reducibility
E,F    : RTM environment
G      : global environment 
H      : reserved: transient premise
IH     : reserved: inductive premise
I,J    : item
K,L    : local environment
M,N    : reserved: future use
O,P,Q  :
R      : generic predicate (relation)
S      : RTM stack
T,U,V,W: term
X,Y,Z  : reserved: transient objet denoted by a capital letter

a,b    : binder polarity
c      : reserved: future use (lambda_delta 3)
d      : relocation depth
e      : relocation height
f      :
g      : sort degree parameter
h      : sort hierarchy parameter
i,j    : local reference position index (de Bruijn's)
k      : sort index
l      : term degree
m,n    : reserved: future use
o      :
p,q    : global reference position
r,s    :
t,u    : local reference position level (de Bruijn's)
v,w    :
x,y,z  : reserved: transient objet denoted by a small letter

NAMING CONVENTIONS FOR CONSTRUCTORS

0: atomic
2: binary

A: application to vector

a: application
b: binder
d: abbreviation
f: flat
l: abstraction
n: native type annotation

NAMING CONVENTIONS FOR TRANSFORMATIONS AND RELATED FORMS

- first letter

c: contex-sensitive for terms
f: context-freee for closures
l: sn contex-sensitive for local environments
r: dx contex-sensitive for local environments
t: context-free for terms

-second letter

i: irreducible form
n: normal form
p: parallel transformation
r: reducible form
s: sequential transformation

- third letter

c: conversion
d: decomposed extended reduction
q: restricted reduction
r: reduction
s: substitution
x: extended reduction

- forth letter (if present)

p: non-reflexive transitive closure (plus)
q: reflexive closure                (question)
s: reflexive transitive closure     (star)