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.
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
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?