Problem 1
a)
set-equalp = (and (set-equalp x x)
((set-equalp x y) => (set-equalp y x))
((and (set-equalp x y) (set-equalp y z)) => (set-equalp x z)))
Reflexive (set-equalp x x) = T
Proof -
(set-equalp x x)
|| by def. of setequalp
(and (set-subsetp x x)
(set-subsetp x x)))
|| by def. of set-subsetp
(and
(if (endp x)
t
(and (set-memberp (car x) x)
(set-subsetp (cdr x) x))))
(if (endp x)
t
(and (set-memberp (car x) x)
(set-subsetp (cdr x) x))))
|| I chose not to expand this any further (by def. of set-memberp), just because it would become too messy and unreadable. However, (set-subsetp x x) always returns T. This is because (set-memberp (car x) x) obviously always returns true because an element of set “x” is always going to be in set “x”. Eventually (set-subsetp x x) will run (set-memberp) on every element of x and the function will return T
(and (T
(T))
|| and axiom
T.. Therefore, set-equalp is reflexive