|
Show: |
((Rz(x) & Rz(y) & Rz(z) & Sr(x, y) & Sr(y, z)) => r(x+y+z) = r(x) + r(y) + r(z))(x, y, z) |
|
|
hypth: |
|
rule: |
|
0H |
((Rz(x) & Rz(y) & Sr(x, y) => r(x+y) = r(x) + r(y))(x, y) & ((Rz(x) & Rz(y) & Sr(x, y)) => Rz(x+y))(x, y) & ((Rz(x) & Rz(y) & Rz(z) & Sr(x, y) & Sr(y, z)) => Sr(x+y, z))(x, y, z) |
|
|
1H |
Rz(a) & Rz(b) & Rz(c) & Sr(a, b) & Sr(b, c) |
|
|
|
Rz(a) & Rz(b) & Rz(c) |
& out |
|
|
Sr(a, b) & Sr(b, c) |
& out |
|
|
Sr(a, b) |
& out |
|
|
Sr(b, c) |
& out |
|
|
Rz(a) & Rz(b) |
& out |
|
|
Rz(c) |
& out |
|
|
Rz(a) |
& out |
|
|
Rz(b) |
& out |
|
|
((Rz(x) & Rz(y) & Sr(x, y) => r(x+y) = r(x) + r(y))(x, y) |
rep |
|
|
((Rz(x) & Rz(b) & Sr(x, b) => r(x+b) = r(x) + r(b))(x) |
A out |
|
|
((Rz(a) & Rz(b) & Sr(a, b) => r(a+b) = r(a) + r(b) |
A out |
|
|
Rz(a) & Rz(b) |
rep |
|
|
Rz(a) & Rz(b) & Sr(a, b) |
& in |
|
|
r(a+b) = r(a) + r(b) |
mp |
|
|
((Rz(x) & Rz(y) & Sr(x, y)) => Rz(x+y))(x, y) |
rep |
|
|
((Rz(x) & Rz(b) & Sr(x, b)) => Rz(x+b))(x) |
A out |
|
|
(Rz(a) & Rz(b) & Sr(a, b)) => Rz(a+b) |
A out |
|
|
Rz(a) & Rz(b) |
rep |
|
|
Rz(a) & Rz(b) & Sr(a, b) |
& in |
|
|
Rz(a+b) |
mp |
|
|
((Rz(x) & Rz(y) & Rz(z) & Sr(x, y) & Sr(y, z)) => Sr(x+y, z))(x, y, z) |
rep |
|
|
((Rz(x) & Rz(y) & Rz(c) & Sr(x, y) & Sr(y, c)) => Sr(x+y, c))(x, y) |
A out |
|
|
|
|
|
|
|
|
|
|
((Rz(x) & Rz(b) & Rz(c) & Sr(x, b) & Sr(b, c)) => Sr(x+b, c))(x) |
A out |
|
|
(Rz(a) & Rz(b) & Rz(c) & Sr(a, b) & Sr(b, c)) => Sr(a+b, c) |
A out |
|
|
Rz(a) & Rz(b) & Rz(c) & Sr(a, b) & Sr(b, c) |
rep |
|
|
Sr(a+b, c) |
mp |
|
|
((Rz(x) & Rz(y) & Sr(x, y) => r(x+y) = r(x) + r(y))(x, y) |
rep |
|
|
((Rz(x) & Rz(c) & Sr(x, c) => r(x+c) = r(x) + r(c))(x) |
A out |
|
|
(Rz(a+b) & Rz(c) & Sr(a+b, c) => r(a+b+c) = r(a+b) + r(c) |
A out |
|
|
Rz(a+b) |
rep |
|
|
Rz(a+b) & Rz(c) |
& in |
|
|
Rz(a+b) & Rz(c) & Sr(a+b, c) |
& in |
|
|
r(a+b+c) = r(a+b) + r(c) |
mp |
|
|
r(a+b) = r(a) + r(b) |
rep |
|
|
r(a+b+c) = r(a) + r(b) + r(c) |
subst |
|
-1H |
(Rz(a) & Rz(b) & Rz(c) & Sr(a, b) & Sr(b, c)) => r(a+b+c) = r(a) + r(b) + r(c) |
=> in |
|
|
((Rz(x) & Rz(b) & Rz(c) & Sr(x, b) & Sr(b, c)) => r(x+b+c) = r(x) + r(b) + r(c))(x) |
A in |
|
|
((Rz(x) & Rz(y) & Rz(c) & Sr(x, y) & Sr(y, c)) => r(x+y+c) = r(x) + r(y) + r(c))(x, y) |
A in |
|
|
((Rz(x) & Rz(y) & Rz(z) & Sr(x, y) & Sr(y, z)) => r(x+y+z) = r(x) + r(y) + r(z))(x, y, z) |
A in |
|
-0H |
[((Rz(x) & Rz(y) & Sr(x, y) => r(x+y) = r(x) + r(y))(x, y) & ((Rz(x) & Rz(y) & Sr(x, y)) => Rz(x+y))(x, y) & ((Rz(x) & Rz(y) & Rz(z) & Sr(x, y) & Sr(y, z)) => Sr(x+y, z))(x, y, z)] ==>
((Rz(x) & Rz(y) & Rz(z) & Sr(x, y) & Sr(y, z)) => r(x+y+z) = r(x) + r(y) + r(z))(x, y, z) |
=> in |
|
|
|
|
|
|
|
|