a,b:
, c:
. ((a -- b) -- c) = (a -- (b+c))a,b,c:. imax(a;b)+c = imax(a+c;b+c)a,b:. a+b = b+aa,b,c:. imax(a;imax(b;c)) = imax(imax(a;b);c)| Theorem | Name |
|
Thm* a,b:, c:. ((a -- b) -- c) = (a -- (b+c)) | [ndiff_ndiff] |
| cites | |
|
Thm* a,b,c:. imax(a;b)+c = imax(a+c;b+c) | [imax_add_r] |
| Thm* a,b:. a+b = b+a | [add_com] |
|
Thm* a,b,c:. imax(a;imax(b;c)) = imax(imax(a;b);c) | [imax_assoc] |