Vars | w v u |
1 | (nat u) |
2 | (nat v) |
3 | (plus u v w) |
Thus | (plus v u w) |
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) |