Definition of isp1


list(demodulators).
isp1 = a(a(abst,k(a(abst,k(eq)))),pair(k(k(p1)),pair(p1,p2))).
end_of_list.






 Click button to load the definition of isp1 into TRC applet.

The combinator isp1 is defined as follows: isp1 x y = p1 if x y = p1, and isp1 x y = p2 if x y != p1.


The combinator isp1 is a natural projection from all the functions to just the characteristic functions. It is defined by the stratified lambda-term

(lambda x
  (lambda y
    (a eq (pair p1 
                (a x y)))))

up show outline