Definition of notp1


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






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

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


The combinator notp1 sends the characteristic function of a set to the characteristic function of the complement of that set. It is derived from the following lambda-term:

(lambda x
  (lambda y
    (a eq (pair p2
                (a (a isp1 x) y)))))

up show outline