theorem shlshl (a b c: nat): $ shl (shl a b) c = shl a (b + c) $;
Step | Hyp | Ref | Expression |
---|---|---|---|
2 |
a * 2 ^ b * 2 ^ c = a * (2 ^ b * 2 ^ c) |
||
3 |
conv shl |
shl (shl a b) c = a * (2 ^ b * 2 ^ c) |
|
5 |
2 ^ (b + c) = 2 ^ b * 2 ^ c -> a * 2 ^ (b + c) = a * (2 ^ b * 2 ^ c) |
||
6 |
conv shl |
2 ^ (b + c) = 2 ^ b * 2 ^ c -> shl a (b + c) = a * (2 ^ b * 2 ^ c) |
|
7 |
2 ^ (b + c) = 2 ^ b * 2 ^ c |
||
8 |
shl a (b + c) = a * (2 ^ b * 2 ^ c) |
||
9 |
shl (shl a b) c = shl a (b + c) |