fmod FG-FUN is
 protecting NAT .
 op F : Nat -> Nat .
 op G : Nat -> Nat .
 vars X Y : Nat .

 ceq F(X) = 5 if X <= 7 [metadata "CA-1"].
 ceq F(X) = 1 if 8 <= X [metadata "CA-2"].

 ceq G(Y) = 2 if Y <= 4 [metadata "CA-a"].
 ceq G(Y) = 7 if 5 <= Y [metadata "CA-b"]. 
endfm