Proof step 4 from proof int2bits-neg-02 (previous step)

j < 0, j < 0 ⊦ sgn(int2bits(2 ^ n→i(# int2bits(~ j)) + j).rest) = int2bits(2 ^ n→i(# int2bits(~ j)) + j).rest, ∃ i. 2 ^ i + j = 0

User applied rule insert lemma

Proof step 5:
¬(∃ i. 2 ^ i = j), 0 ≤ j ⊦ sgn(int2bits(2 ^ n→i(# int2bits(j)) - j).rest) = int2bits(2 ^ n→i(# int2bits(j)) - j).rest
Proof step 6:
j < 0, j < 0 ⊦ ¬(∃ i. 2 ^ i = ~ j) ∧ 0 ≤ ~ j, sgn(int2bits(2 ^ n→i(# int2bits(~ j)) + j).rest) = int2bits(2 ^ n→i(# int2bits(~ j)) + j).rest, ∃ i. 2 ^ i + j = 0
Proof step 8:
sgn(int2bits(2 ^ n→i(# int2bits(~ j)) - ~ j).rest) = int2bits(2 ^ n→i(# int2bits(~ j)) - ~ j).rest, j < 0, j < 0 ⊦ sgn(int2bits(2 ^ n→i(# int2bits(~ j)) + j).rest) = int2bits(2 ^ n→i(# int2bits(~ j)) + j).rest, ∃ i. 2 ^ i + j = 0

name: int2bits-restsgn subst: [j] → [~ j]

Used terms: ~ j