Injections
Set of all functions from a finite domain to a finite range
General Form:
(injections domain range)
where domain and range are true-lists of symbols (actually the members
of domain need not be symbols). The result is a list of alists,
representing all functions from domain to range. The following
example illustrates this function: either
- b maps to c and a maps to d or e, or
- b maps to d and a maps to c or e, or
- b maps to e and a maps to c or d.
ACL2 !>(injections '(a b) '(c d e))
(((A . D) (B . C))
((A . E) (B . C))
((A . C) (B . D))
((A . E) (B . D))
((A . C) (B . E))
((A . D) (B . E)))
ACL2 !>
