[Termtools] Suggestion for new output

[H. Zantema]

As you know there are new rules for the output of the tools for the 
competitition, requiring explicit references to theorems.

As a suggestion how to deal with these new rules please look at
http://www.win.tue.nl/~hzantema/torpatech.pdf

Here you see a list of theorems identified by [A], [B], [C],....
used by TORPA, while the TORPA output refers to them in the following way:

YES
pre-version of TORPA 1.6 is applied to
a b  -> c ,
c  -> b a a ,

[J] Reduce rhs: apply rule 2 on rhs of rule 1, result:
a b  -> b a a
c  -> b a a
[A] Choose polynomial interpretation   c: lambda x.x+1,  rest identity
remove: c  -> b a a
[AC] Reverse every lhs and rhs and choose polynomial interpretation:
b: lambda x.10x,  rest lambda x.x+1
remove: a b  -> b a a
Terminating since no rules remain.


Well, just a suggestion.

-- 

 		Best regards, Hans Zantema.

+--------------------------------------+-----------------------------+
|                                      |                             |
|   Dr Hans Zantema                    |   Hoofdgebouw   kamer 6.73  |
|   Faculteit Wiskunde en Informatica  |   tel (040)2472749          |
|   Technische Universiteit Eindhoven  |   fax (040)2468508          |
|   Postbus 513     5600 MB Eindhoven  |   e-mail  H.Zantema at tue.nl  |
|   The Netherlands                    |   www.win.tue.nl/~hzantema  |
|                                      |                             |
+--------------------------------------+-----------------------------+
_______________________________________________
Termtools mailing list
Termtools at serveur-listes.lri.fr
http://serveur-listes.lri.fr/mailman/listinfo/termtools