Proof step 54 from proof shiftzero-pos (previous step)

User applied rule cut formula

And obtained the following new goals

• Proof step 55:

  mklist(false, i→n(j)) + mklist(false, n - i→n(j)) + int2bits(i) = mklist(false, n) + int2bits(i), # int2bits(i) = i→n(j), 0 ≤ i, i→n(j) < n ⊦ bits2int(firstn(n, mklist(false, i→n(j)) + mklist(false, n - i→n(j)) + int2bits(i))) = 0, j = 0

• Proof step 62:

  # int2bits(i) = i→n(j), 0 ≤ i, i→n(j) < n ⊦ mklist(false, i→n(j)) + mklist(false, n - i→n(j)) + int2bits(i) = mklist(false, n) + int2bits(i), bits2int(firstn(n, mklist(false, i→n(j)) + mklist(false, n - i→n(j)) + int2bits(i))) = 0, j = 0

Rule argument

Additional information

Used formulas: mklist(false, i→n(j)) + mklist(false, n - i→n(j)) + int2bits(i) = mklist(false, n) + int2bits(i)