Function Space
Function Space Builder: ?, collects the functions from a domain A to a domain B, creating the domain A ?B.
Disassembly: _ ( _ ):(A ? B) x A ? B which takes an f ?A ? Band an a ?A and produces f(a) ?B
Extensionality: for any f and g in A ? B, if for all a ?A , f(a) = g(a) then f = g
Assembly: if e is an expression containing occurences of an identifier x, such that whenever a value a ?A replaces the occurences of x in e then the value [a/x] e ?B results, then (?x.e)is an element in A ? B
[n ? v] r abbreviates (? m.m equal n ? v []r(m))
i.e. if this function r is applied to n the result is v otherwise is the
result is r applied to m.