Exercise 13.7 Modify the depth-bound meta-interpreter of Figure 13.12

(page 587) so that

(a) the bound is on the total length of the proof, where the length is the total number of instances of base-level atoms that appear in the proof.

(b) different base-level atoms can incur different costs on the bound. For example, most atoms could have zero cost, and some atoms could incur a positive cost.

Discuss why either of these may be better or worse than using the depth of the tree.

What conditions on the atom costs would guarantee that, when a positive bound is given, the proof procedure does not go into an infinite loop?