logic PL
spec SP =
x : i.
f : i -> o.
. f x
end