PrALT18n
Premises:
(= (+ a (+ b 1)) (+ (+ a b) 1) ) (= (+ (+ a b) 1) (+ (+ b a) 1) ) (= (+ (+ b a) 1) (+ b (+ a 1)) ) (= (+ b (+ a 1)) (+ b (+ 1 a)) ) (= (+ b (+ 1 a)) (+ (+ b 1) a) )
Conclusion:
(= (+ a (+ b 1)) (+ (+ b 1) a) )