RewritingNonConfluent3.agda:20,13-23
Global confluence check failed: suc m + 0 can be rewritten to
either suc (m + 0) or suc m.
Possible fix: add a rewrite rule with left-hand side suc m + 0 to
resolve the ambiguity.
when checking confluence of the rewrite rule plus-suc-l with
plus-0r
RewritingNonConfluent3.agda:21,13-23
Global confluence check failed: suc m + suc n can be rewritten to
either suc (suc m + n) or suc (m + suc n).
Possible fix: add a rewrite rule with left-hand side suc m + suc n
to resolve the ambiguity.
when checking confluence of the rewrite rule plus-suc-r with
plus-suc-l
RewritingNonConfluent3.agda:21,13-23
Global confluence check failed: 0 + suc n can be rewritten to
either suc (0 + n) or suc n.
Possible fix: add a rewrite rule with left-hand side 0 + suc n to
resolve the ambiguity.
when checking confluence of the rewrite rule plus-suc-r with
plus-0l
RewritingNonConfluent3.agda:22,13-23
Global confluence check failed: (k + l) + suc n can be rewritten to
either k + (l + suc n) or suc ((k + l) + n).
Possible fix: add a rewrite rule with left-hand side
(k + l) + suc n to resolve the ambiguity.
when checking confluence of the rewrite rule plus-assoc with
plus-suc-r
RewritingNonConfluent3.agda:22,13-23
Global confluence check failed: (k + l) + 0 can be rewritten to
either k + (l + 0) or k + l.
Possible fix: add a rewrite rule with left-hand side (k + l) + 0 to
resolve the ambiguity.
when checking confluence of the rewrite rule plus-assoc with
plus-0r
RewritingNonConfluent3.agda:22,13-23
Global confluence check failed: ((k + l) + l₁) + m can be rewritten
to either (k + l) + (l₁ + m) or (k + (l + l₁)) + m.
Possible fix: add a rewrite rule with left-hand side
((k + l) + l₁) + m to resolve the ambiguity.
when checking confluence of the rewrite rule plus-assoc with itself
RewritingNonConfluent3.agda:22,13-23
Global confluence check failed: (k + suc n) + m can be rewritten to
either k + (suc n + m) or suc (k + n) + m.
Possible fix: add a rewrite rule with left-hand side
(k + suc n) + m to resolve the ambiguity.
when checking confluence of the rewrite rule plus-assoc with
plus-suc-r
RewritingNonConfluent3.agda:22,13-23
Global confluence check failed: (suc m + l) + m₁ can be rewritten
to either suc m + (l + m₁) or suc (m + l) + m₁.
Possible fix: add a rewrite rule with left-hand side
(suc m + l) + m₁ to resolve the ambiguity.
when checking confluence of the rewrite rule plus-assoc with
plus-suc-l
RewritingNonConfluent3.agda:22,13-23
Global confluence check failed: (k + 0) + m can be rewritten to
either k + (0 + m) or k + m.
Possible fix: add a rewrite rule with left-hand side (k + 0) + m to
resolve the ambiguity.
when checking confluence of the rewrite rule plus-assoc with
plus-0r
RewritingNonConfluent3.agda:22,13-23
Global confluence check failed: (0 + l) + m can be rewritten to
either 0 + (l + m) or l + m.
Possible fix: add a rewrite rule with left-hand side (0 + l) + m to
resolve the ambiguity.
when checking confluence of the rewrite rule plus-assoc with
plus-0l
RewritingNonConfluent3.agda:22,13-23
Global confluence check failed: ((k + l) + l₁) + m can be rewritten
to either (k + l) + (l₁ + m) or (k + (l + l₁)) + m.
Possible fix: add a rewrite rule with left-hand side
((k + l) + l₁) + m to resolve the ambiguity.
when checking confluence of the rewrite rule plus-assoc with itself
RewritingNonConfluent3.agda:36,13-23
Global confluence check failed: suc m * 0 can be rewritten to
either 0 + (m * 0) or 0.
Possible fix: add a rewrite rule with left-hand side suc m * 0 to
resolve the ambiguity.
when checking confluence of the rewrite rule mult-suc-l with
mult-0r
RewritingNonConfluent3.agda:37,13-23
Global confluence check failed: suc m * suc n can be rewritten to
either (suc m * n) + suc m or suc n + (m * suc n).
Possible fix: add a rewrite rule with left-hand side suc m * suc n
to resolve the ambiguity.
when checking confluence of the rewrite rule mult-suc-r with
mult-suc-l
RewritingNonConfluent3.agda:37,13-23
Global confluence check failed: 0 * suc n can be rewritten to
either (0 * n) + 0 or 0.
Possible fix: add a rewrite rule with left-hand side 0 * suc n to
resolve the ambiguity.
when checking confluence of the rewrite rule mult-suc-r with
mult-0l
RewritingNonConfluent3.agda:38,13-30
Global confluence check failed: suc m * (l + m₁) can be rewritten
to either (suc m * l) + (suc m * m₁) or (l + m₁) + (m * (l + m₁)).
Possible fix: add a rewrite rule with left-hand side
suc m * (l + m₁) to resolve the ambiguity.
when checking confluence of the rewrite rule plus-mult-distr-l with
mult-suc-l
RewritingNonConfluent3.agda:38,13-30
Global confluence check failed: 0 * (l + m) can be rewritten to
either (0 * l) + (0 * m) or 0.
Possible fix: add a rewrite rule with left-hand side 0 * (l + m) to
resolve the ambiguity.
when checking confluence of the rewrite rule plus-mult-distr-l with
mult-0l
RewritingNonConfluent3.agda:38,13-30
Global confluence check failed: k * ((k₁ + l) + m) can be rewritten
to either (k * (k₁ + l)) + (k * m) or k * (k₁ + (l + m)).
Possible fix: add a rewrite rule with left-hand side
k * ((k₁ + l) + m) to resolve the ambiguity.
when checking confluence of the rewrite rule plus-mult-distr-l with
plus-assoc
RewritingNonConfluent3.agda:38,13-30
Global confluence check failed: k * (l + suc n) can be rewritten to
either (k * l) + (k * suc n) or k * suc (l + n).
Possible fix: add a rewrite rule with left-hand side
k * (l + suc n) to resolve the ambiguity.
when checking confluence of the rewrite rule plus-mult-distr-l with
plus-suc-r
RewritingNonConfluent3.agda:38,13-30
Global confluence check failed: k * (suc m + m₁) can be rewritten
to either (k * suc m) + (k * m₁) or k * suc (m + m₁).
Possible fix: add a rewrite rule with left-hand side
k * (suc m + m₁) to resolve the ambiguity.
when checking confluence of the rewrite rule plus-mult-distr-l with
plus-suc-l
RewritingNonConfluent3.agda:38,13-30
Global confluence check failed: k * (l + 0) can be rewritten to
either (k * l) + (k * 0) or k * l.
Possible fix: add a rewrite rule with left-hand side k * (l + 0) to
resolve the ambiguity.
when checking confluence of the rewrite rule plus-mult-distr-l with
plus-0r
RewritingNonConfluent3.agda:38,13-30
Global confluence check failed: k * (0 + m) can be rewritten to
either (k * 0) + (k * m) or k * m.
Possible fix: add a rewrite rule with left-hand side k * (0 + m) to
resolve the ambiguity.
when checking confluence of the rewrite rule plus-mult-distr-l with
plus-0l
