a suggestion was added to avoid 1 pseudo reduction at the cost of 40 proper

reductions :(

diff --git a/helm/software/helena/examples/grundlagen/grundlagen.aut b/helm/software/helena/examples/grundlagen/grundlagen.aut
index 4a856c2454454abafef49c36af35960d94636082..d38532d369ee0903476d1406f88bd83b3af51f1b 100644 (file)
--- a/helm/software/helena/examples/grundlagen/grundlagen.aut
+++ b/helm/software/helena/examples/grundlagen/grundlagen.aut
@@ -2,6 +2,7 @@
 # Copyright (C) 1977, L.S. van Benthem Jutting
 #               1992, revised by F. Wiedijk (http://www.cs.ru.nl/~freek/aut/)
 #               2008, revised by F. Guidi to remove the eta-reductions
+#               2014, revised by F. Guidi to suggest @-typing removal
 
 +l
 @[a:'prop'][b:'prop']
@@ -681,8 +682,12 @@ th2:=[x:a]cone(<x>b,mp"l"(a,con,x,n)):imp(a,b)
 b@ec:=[x:a]not(<x>b):'prop'
 [n:not(a)]
 eci1:=[x:a]cone(not(<x>b),mp"l"(a,con,x,n)):ec(a,b)
-b@[a1:and(a,b)]
-ande2:=<ande1(a,b,a1)>ande2"l"(a,b,a1):<ande1(a,b,a1)>b
+%suggestion by Guidi to remove @-typing
+b@[a1:and(a,b)] %original line
+ande2:=<ande1(a,b,a1)>ande2"l"(a,b,a1):<ande1(a,b,a1)>b %original line
+%b@[a1:and(a,[x:a]<x>b)]
+%ande2:=<ande1(a,[x:a]<x>b,a1)>ande2"l"(a,[x:a]<x>b,a1):<ande1(a,[x:a]<x>b,a1)>[x:a]<x>b
+%end of suggestion
 a@[ksi:'type']
 +ite
 [x1:ksi][y1:ksi]