common-addends-<の公理を使うことで、<の引数にある2つの(wt (cdr x))をキャンセルできると思います。 (if (atom x) 't (if (atom (car x)) (< (wt (cdr x)) (+ (+ (wt (car x)) (wt (car x))) (wt (cdr x)))) (< (wt (rotate x)) (wt x)))) これを (dethm …