up | previous | next | detailed contents | brief contents

Definition of subset

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






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

I define subset pair(x, y) = p1 if there is no z such that x z = p1 but y z != p1. The idioms used in the lambda-term below should by now be quite familiar, so I let it speak for itself.
(lambda (x y)
  (a eq (pair (k p2)
              (lambda z
                (a eq (pair (pair p1
                                  p2)
                            (pair (a x z)
                                  (a (a isp1 y) z))))))))

up | previous | next | detailed contents | brief contents