Proof step 60 from proof cast-help-comm (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 61:

  # int2bits(j) < i→n(i0), # int2bits(j) < i→n(i), 1 < i0, 0 < i0, 0 < i, i < i0, i ≤ i0, ¬ 0 ≤ j → j < 0 ⊦ bits2int(restn(i→n(i0) - i→n(i), mklist(¬ 0 ≤ j, i→n(i0) - # int2bits(j)) + int2bits(j))) = j, i→n(i0) = # int2bits(j), mklist(¬ 0 ≤ j, i→n(i) - # int2bits(j)) + int2bits(j) = [], i = 0, i0 = 0

Rule argument

Additional information

Used simplifier rules: ⊦ i→n(i) = 0 ↔ i = 0;% ⊦ m < n → n ≠ 0; (forward)% ⊦ 1 < i → abs(i) = i;% ⊦ 0 < j → abs(j) = j;% ⊦ i→n(i) ≤ i→n(j) ↔ abs(i) ≤ abs(j);% ⊦ n < m → (m - n) + n = m;% ⊦ m ≠ n → (m ≤ n ↔ m < n);% ⊦ m + n = n + m;% ⊦ (m + n0) + n1 = m + n0 + n1;% ⊦ m ≤ n → (n - m = 0 ↔ n = m);% ⊦ m < m + n ↔ n ≠ 0;% ⊦ m < n ∧ n ≤ n0 → m < n0; (forward)% ⊦ ¬ i ≤ j ↔ j < i;% ⊦ (bits + bits0) + bits1 = bits + bits0 + bits1;% ⊦ # mklist(boolvar, n) = n;% ⊦ #(bits + bits0) = # bits + # bits0;