Proof step 14 from proof ushort-neg (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 15:

  ⊦ i < ~1 → (m < # int2bits(i) ↔ ¬ 0 ≤ i + 2 ^ (n→i(m) - 1))

Rule argument

Additional information

Used simplifier rules: short-min-01: ⊦ ¬ s2i(sho) < ~32768;% ⊦ i + j = j + i;% ⊦ i + j + i0 = (i + j) + i0;% ⊦ ¬ i ≤ j ↔ j < i;% ⊦ (* j) ≤ i0 + (* j0) ↔ j - j0 ≤ i0;% ⊦ ¬ i < j ↔ j ≤ i;% ⊦ i < 0 → (~1 ≤ i ↔ i = ~1);% ⊦ j < i ∧ i ≤ 0 → j < 0; (forward)% ⊦ m < n → n ≠ 0; (forward)%i < 0 ⊦ int2bits((* i)) = sgn(bitsinvert(uint2bits(abs(i))) +1);% ⊦ uint2bits(1) = false + true;% ⊦ boolvar + boolvar0 = boolvar ' + boolvar0 ';% ⊦ bitsinvert(false ' + bits) = true + bitsinvert(bits);% ⊦ bitsinvert(true ') = false ';% ⊦ boolvar + bits = boolvar ' + bits;% ⊦ (bits + bits0) + bits1 = bits + bits0 + bits1;% ⊦ (bits + false ')+1 = bits + true;% ⊦ bits + boolvar = bits + boolvar ';% ⊦ sgn(true ' + true ') = true ';% ⊦ # boolvar ' = 0 +1;% ⊦ 0 < n → fillsgn(n, boolvar ') = mklist(boolvar, n);%n ≠ 0 ⊦ mklist(true, (* n)) = true ' + mklist(true, n -1);% ⊦ mklist(boolvar, 0) = [];% ⊦ bits + [] = bits;% ⊦ boolvar ' + bits ≠ [];% ⊦ #(bits + bits0) = # bits + # bits0; Used terms: s2i(sho), 16