Abstraction function

Representation invariant

• $I(a,t,s)\; ==\; t\; =\; length(s)\; /\backslash \; t\; >=\; 0\; /\backslash \; s\; =\; \%a(a,t)$