Dear Themos, Alasdair,
trying to debug the freeOf? pattern, I discovered that Themos' pattern suffers
from the same problem:
tt:=operator 'tt; ttrules := rule tt(n/(n^a+(X | integer?(a) and (n-1)^a = n^a
+X))) == 1/t^a
(100) -> ttrules tt(n/(n^6+anything))
1
(100) --
6
t
Type: Expression Integer
The problem seems to be that the syntactic sugar for the suchThat operation "|"
only works if we have a function of a single variable. Of course, calling
suchThat without sugar, axiom does the right thing:
(101) -> ttrules := suchThat(rule tt(n/(n^a+X)) == 1/t^a, [a, X], l +->
integer? first
l and (n-1)^(first l) = n^(first l) + second l)
n 1
(101) tt(------) == --
a a
n + X t
Type: RewriteRule(Integer,Integer,Expression Integer)
(102) -> ttrules tt(n/(n^6+anything))
n
(102) tt(-------------)
6
n + anything
Type: Expression Integer
(103) -> ttrules tt(n/((n-1)^6))
1
(103) --
6
t
Type: Expression Integer
_______________________________________________
Axiom-developer mailing list
[email protected]
http://lists.nongnu.org/mailman/listinfo/axiom-developer
