| # sgn(bits) = 2 + i→n(i), bits2int(bits) < i, bits2int(bits) < 2 ^ i, 0 < 2 ^ i, bits2int(bits) + 1 < 2 ^ i, bits2int(bits) < 2 ^ i * 2, bits2int(bits) + 1 < 2 ^ i * 2, 0 ≤ bits2int(bits) + 2 ^ i * 2, bits2int(bits) + 2 ^ i < 0, # bits ≤ 8, bits2int(bits) < ~128, bits2int(bits) + 2 ^ i < i, bits2int(bits) < ~1, bits2int(bits) < 0, 6 < i, 0 < i, 0 ≤ i, (bits2int(bits) + 2 ^ i) + 1 < i, bits2int(bits) + 1 < i ⊦ bits = [], i = ~1 |
Used simplifier rules: bits2int-first-01: bits ≠ [] ⊦ bits2int(bits) < 0 → bits.first;% ⊦ i + j = i + i0 ↔ j = i0;% ⊦ 0 < i → n→i(i→n(i)) = i;% ⊦ n→i(m + n) = n→i(m) + n→i(n);% ⊦ i - j = i0 ↔ i = i0 + j;%0 ≤ i ⊦ n→i(n) = (* i) ↔ n = i→n(i);% ⊦ # bits = 1 ↔ bits = bits.first + [];% ⊦ bits ≠ [] → (sgn(bits).first ↔ bits.first);% ⊦ boolvar + bits = boolvar ' + bits;% ⊦ bits + [] = bits;% ⊦ (bits + bits0) + bits1 = bits + bits0 + bits1;% ⊦ bits ≠ [] → (sgn(bits) = boolvar ' ↔ ¬ (¬ boolvar) ∈ bits);% ⊦ i < j - i0 ↔ i + i0 < j;% ⊦ i + j + i0 = (i + j) + i0;% ⊦ i + j = j + i;%0 ≤ i ⊦ (* i) < n→i(n) ↔ i→n(i) < n;% ⊦ i ≤ j - i0 ↔ i + i0 ≤ j;%0 ≤ i ⊦ (* i) ≤ n→i(n) ↔ i→n(i) ≤ n;% ⊦ m < n → m ≤ n;% ⊦ i + j < i0 ∧ ¬ j < j0 → i + j0 < i0;% ⊦ m < n ∧ n = n0 → m < n0; (forward)% ⊦ m < n → n ≠ 0; (forward)% ⊦ i < j ∧ j ≤ j0 → i < j0; (forward)% ⊦ i < j ∧ j < i0 → i +1 < i0; (forward)% ⊦ i < j ∧ j < j0 → i < j0; (forward)% ⊦ m ≤ n ∧ n < n0 → m < n0; (forward)% ⊦ # bits = 0 ↔ bits = [];% ⊦ sgn(bits) = [] ↔ bits = [];% ⊦ m < m + n ↔ n ≠ 0;% ⊦ i→n(i) = 0 ↔ i = 0;% ⊦ (m + n0) + n1 = m + n0 + n1;% ⊦ m + n = n + m;%n0 < n ⊦ (* n) < m0 + (* n0) ↔ n - n0 < m0;% ⊦ i < i + j ↔ 0 < j;% ⊦ 0 < i → (0 < i * j ↔ 0 < j);% ⊦ i * j * j0 = (i * j) * j0;% ⊦ i * j = j * i;% ⊦ i +1 = i + 1;% ⊦ ¬ # bits < # sgn(bits); Used formulas: i = n→i(# sgn(bits)) - 2