notes

notes/to do

@@ -96,6 +96,8 @@ and then fix up all uses of the lemma - the transformation above
 should then clean up everything.
 
 look at gt6 - ground joinability testing goes really slow
+also, after a while "a" becomes redundant - but we still keep deriving
+stuff from it
 rob006-1 too
 
 * adjust CP depth so that simplifications of rules get the same depth
@@ -174,4 +176,4 @@ forces all variables to have size one.
 When we discover the crucial lemma, it causes bajillions of existing
 rules to be discarded. Can we somehow use this as a similar/boringness
 metric on these existing rules? (The fact that there is a single rule
-which will generalise them all.)
+which will generalise them all.)