Currently, the only rewrite rules on exponents define base cases: E^1=E, 1^E=1, E^0=1. If we have E^n, we can't do anything with it in proofs. We should at least have a rewrite rule E^n=E*E^(n-1), for n>0.
This rule has been implemented and merged in commit [53cd8c].
Commit: [53cd8c]
Log in to post a comment.
This rule has been implemented and merged in commit [53cd8c].
Related
Commit: [53cd8c]