Vars	i w v u
1	((forall u1, v1 ((plus 0 u1 v1) => (plus u1 0 v1))) => (forall m, p ((plus i m p) => (plus m i p))))
2	(nat v)
3	(plus u v w)
Thus	((forall u1, v1 ((plus 0 u1 v1) => (plus u1 0 v1))) => (forall m, p ((plus (s i) m p) => (plus m (s i) p))))

Vars	i w v u
1	(forall u1, v1 ((plus 0 u1 v1) => (plus u1 0 v1)))
2	((forall u1, v1 ((plus 0 u1 v1) => (plus u1 0 v1))) => (forall m, p ((plus i m p) => (plus m i p))))
3	(nat v)
4	(plus u v w)
Thus	(forall m, p ((plus (s i) m p) => (plus m (s i) p)))

Vars	i w v u
1	(forall u1, v1 ((plus 0 u1 v1) => (plus u1 0 v1)))
2	((forall u1, v1 ((plus 0 u1 v1) => (plus u1 0 v1))) => (forall m, p ((plus i m p) => (plus m i p))))
3	(nat v)
4	(plus u v w)
Thus	(forall u1, v1 ((plus 0 u1 v1) => (plus u1 0 v1)))

Vars	i w v u
1	(forall m, p ((plus i m p) => (plus m i p)))
2	(forall u1, v1 ((plus 0 u1 v1) => (plus u1 0 v1)))
3	(nat v)
4	(plus u v w)
Thus	(forall m, p ((plus (s i) m p) => (plus m (s i) p)))

Vars	p m i w v u
1	(plus (s i) m p)
2	(forall m1, p1 ((plus i m1 p1) => (plus m1 i p1)))
3	(forall u1, v1 ((plus 0 u1 v1) => (plus u1 0 v1)))
4	(nat v)
5	(plus u v w)
Thus	(plus m (s i) p)