- To make Ivy work in ACL2-2.6 and ACL2-2.7, in the book paramod.lisp (defthm len-0-list-forward (implies (and (true-listp l) (equal (+ n (len l)) n)) (equal l nil)) :rule-classes :forward-chaining) should be replaced by (defthm len-0-list-forward (implies (and (true-listp l) (equal (len l) 0)) (equal l nil)) :rule-classes :forward-chaining)