Proof step 8 from proof cast-law-shift-snd-l (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  6 < # int2bits(31), 5 ≤ i, 0 < i, 0 ≤ i, i < n→i(# int2bits(31) - 1) ⊦ # int2bits(31) - 1 = 1, # int2bits(31) - 1 = 0, bits2int(int2bits(j0) + mklist(false, i→n(band(j, 31)))) = bits2int(int2bits(j0) + mklist(false, i→n(band(cast(i, j), 31))))

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (forward)%n0 ≤ n ⊦ m < n - n0 ↔ m + n0 < n;% ⊦ ¬ m ≤ n ↔ n < m;% ⊦ m < 1 ↔ m = 0;% ⊦ # bits = 0 ↔ bits = [];% ⊦ int2bits(j) ≠ [];% ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1);% ⊦ 0 < n ↔ n ≠ 0;%0 ≤ i ⊦ (* i) < n→i(n) ↔ i→n(i) < n;% ⊦ i ≤ j ∧ j < j0 → i < j0; (forward)% ⊦ i < j ∧ 0 < i → 0 < j ∧ 1 < j; (forward)% ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward)% ⊦ ¬ i ≤ j ↔ j < i;% ⊦ n -1 = n - 1;