Commit b86c405a authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft
Browse files

fix proof

parent d7df4f76
......@@ -1243,8 +1243,8 @@ module N
assert { value r !i + (power radix !i) * !c =
value x !i * y
by
value r !i + (power radix !i) * !c
= value r k + (power radix k) * res
value r !i + !c * (power radix !i)
= value r k + res * (power radix k)
+ (power radix !i) * !c
= value r k + (power radix k) * res
+ (power radix k) * radix * !c
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment