blob: ace51337a9d5b34324aea922976213f5d15a679a (
plain)
1
2
3
4
5
6
7
8
9
10
|
;; IVY operation: PROVE
;;
;; From basis S and K, show that a combinator Wxy=xyy exists.
(imp (and (all x (= x x))
(all x (all y (all z (= (a (a (a (S) x) y) z)
(a (a x z) (a y z))))))
(all x (all y (= (a (a (K) x) y) x))))
(exists W (all x (all y (= (a (a W x) y) (a (a x y) y))))))
|
