Proof step 84 from proof byte-mult-256 (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 85:

  ⊦ ~128 ≤ i ∧ i ≤ 127 → b2i(i2b(i)) = i

• Proof step 86:

  ~128 ≤ i1 ∧ i1 ≤ 127, ¬(~256 < i1 ∧ i1 < ~128), i0 + i = ~1, i1 < 0, ~256 ≤ i1, i < 0, 0 ≤ i0 ⊦ i = 0, i1 = b2i(i2b(i1 + 256))

Rule argument

Additional information

Used simplifier rules: byte-equal: ⊦ b2i(byi) = b2i(byj) ↔ byi = byj;%num-i2b-neg: i < ~128 ⊦ i2b((* i)) = i2b(bits2int(lastn(8, int2bits(i))));%num-i2b-equal: ~128 ≤ i, i ≤ 127, ~128 ≤ j, j ≤ 127 ⊦ i2b((* i)) = i2b((* j)) ↔ i = j;% ⊦ ¬ i < j ↔ j ≤ i;% ⊦ i ≤ j → (j ≤ i ↔ i = j);%i < 0 ⊦ int2bits((* i)) = sgn(bitsinvert(uint2bits(abs(i))) +1);%1 < i ⊦ uint2bits((* i)) = uint2bits(i / 2) + (i % 2 = 1);% ⊦ uint2bits(1) = false + true;% ⊦ boolvar + boolvar0 = boolvar ' + boolvar0 ';% ⊦ bits + boolvar = bits + boolvar ';% ⊦ bitsinvert(false ' + bits) = true + bitsinvert(bits);% ⊦ bitsinvert(true ' + bits) = false + bitsinvert(bits);% ⊦ bitsinvert(false ') = true ';% ⊦ boolvar + bits = boolvar ' + bits;% ⊦ (bits + bits0) + bits1 = bits + bits0 + bits1;% ⊦ (bits + true ')+1 = bits +1 + false;% ⊦ (bits + false ')+1 = bits + true;% ⊦ sgn(boolvar ' + boolvar ' + bits) = sgn(boolvar ' + bits);% ⊦ sgn(true ' + false ' + bits) = true ' + false ' + bits;%0 < n ⊦ lastn((* n), bits + boolvar ') = lastn(n -1, bits) + boolvar ';% ⊦ lastn(1, bits) = bits.last ';% ⊦ (bits + boolvar ').last ↔ boolvar;% ⊦ bits2int(false ' + bits) = bits2uint(bits);% ⊦ bits2uint(bits + false ') = bits2uint(bits) * 2;% ⊦ bits2uint(false ') = 0;%i0 ≠ 0, i0 ≤ i ⊦ (* i) ≤ j → (* i0) ≤ j;% ⊦ ¬ i ≤ j ↔ j < i;% ⊦ i < j ∧ ¬ i0 < j → ¬ i0 < i; Used terms: i1