Term-Ersetzung drückt nicht alle Aspekte der üblichen mathematischen/logischen Sprache aus:
es fehlen Variablen (die sind zwar in den Regeln, aber nicht in den Termen, auf die diese angewendet werden)
gebundene Variablen in der ...
static int foo (int x) { ... }