Predykat

start

 
definition
  let x1 be Θ1;
   .....
  let xn be Θn;
  pred a1,...,am ≈ am+1,...,ak means Φ(x1,...,xn,it);
end;

gdzie {a₁,...,a_k} ⊆ {x₁,...,x_n-1} oraz domknięcie zbioru {a₁,...,a_m} ze względu na zależność typów daje cały {x₁,...,x_n-1}.

Predykat (a₁,...,a_m) ≈ (a_m+1,...,a_k) słuźy do tworzenia formuł atomowych (τ₁,...,τ_m) &asimp; (τ_m+1,...,τ_k).

Przykłady:

x < y, x = y, h is_homomorphism A,B, X misses Y, mmlquery