Hi Jim,

I decided to use Larch and LP in my course for undergraduated students
(this is the best way to learn something). I have a few small problems.
One of them is the example of your book on p. 141.

FinSet: trait
		empty: -> S
		insert: S, E -> S
		singleton: E -> S
		__ \U __: S, S -> S
		__\in __: E, S -> Bool
		__ \subseteq __: S, S -> Bool
		S generated by empty, insert
		S partitioned by \in
		\forall s, s1: S, e, e1: E
			singleton(e) == insert(empty, e);
			s \U empty == s;
			s \U insert(s1, e) == insert(s \U s1, e);
			~(e \in empty);
			e \in insert(s, e1) == e \in s \/ e = e1;
			empty \subseteq s;
			insert(s, e) \subseteq s1 == s \subseteq s1 /\ e \in s1
		S partitioned by \subseteq
		S generated by empty, singleton, \U

According to the text on the same page, if I type LP commands

	execute FinSet_Axioms
	prove sort S partitioned by \subseteq

LP translates the partitioned by into a deduction rule, and then, if I type
complete, LP should finish the proof. However, this is not the case.
It seems to me that the proof of this property is much more complicated.
Am I right?