Example: > (len . concat)(a, b) (len · concat)(a, b) (len · concat)(a)(b) (concat[len] · (len · fst, len · snd))(a)(b) (add · (len · fst, l

Example: > (len . concat)(a, b) (len · concat)(a, b) (len · concat)(a)(b) (concat[len] · (len · fst, len · snd))(a)(b) (add · (len · fst, len · snd))(a)(b) <=> add((len · fst)(a)(b), (len · snd)(a)(b)) > add((len · fst)(a)(b), (len · snd)(a)(b)) add((len · fst)(a)(b), (len · snd)(a)(b)) add((len · fst)(a)(b))((len · snd)(a)(b)) add(len(a))((len · snd)(a)(b)) add(len(a))(len(b)) This raises a few questions: 1. How is this supposed to be point-free? a and b are clearly arguments. Wouldn't you replace them with obscure projection functions if you really believed that being point-free was useful? 2. What about this are inputs of the system, and what are the outputs? I'm guessing > marks what the user input, and the other lines are rewrites produced by the system. In that case, why did it stop after a few steps when it was clearly able to continue? 3. Don't you need induction to prove this theorem? Where is the induction step? Where is the base case? 4. Are some of the rewrites based on lemmas already proved and stored in the system? If so, wouldn't it be useful to mark such rewrites?