Proof step 95 from proof bitsand-cast (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 96:

  n = # fillsgn(n, mklist(true, n0 - 1) + true ' + false ' + bits1), sgn(mklist(true, n0 - 1) + true ' + false ' + bits1) = true ' + false ' + bits1, # bits = 2 + # bits1, n0 + 1 + # bits1 < n ⊦ n0 = 0, lastn(n, fillsgn(n, bitsand(bits2 + bits, true ' + false ' + bits1))) = lastn(n, fillsgn(n, bitsand(mklist(true, n0 - 1) + true ' + false ' + bits1, bits2 + bits))), bits2 = [], bits2 + bits = []

Rule argument

Additional information

Used simplifier rules: ⊦ boolvar ∈ boolvar0 ' ↔ boolvar ↔ boolvar0;% ⊦ boolvar ∈ bits + bits0 ↔ ¬ ¬(boolvar ∈ bits ∨ boolvar ∈ bits0);% ⊦ bits = bits0 + boolvar ' + bits1 → boolvar ∈ bits;% ⊦ bits = bits0 + boolvar ' + bits1 → boolvar ∈ bits; (forward)% ⊦ boolvar ' + bits = bits0 → boolvar ∈ bits0; (forward)% ⊦ m ≤ m;% ⊦ ¬ m < n ↔ n ≤ m;% ⊦ ¬ n < n;% ⊦ m + n < m + n0 ↔ n < n0;%n < n0 ⊦ (* n) ≠ m0 + (* n0);% ⊦ m < n → n ≠ 0; (forward)% ⊦ m < n ∧ n = n0 → m < n0; (forward)% ⊦ m < n ∧ m = n0 → n0 < n; (forward)% ⊦ (boolvar ' + bits).first ↔ boolvar;% ⊦ boolvar ' ≠ [];% ⊦ ¬ bits + bits0 ≠ [] ↔ bits = [] ∧ bits0 = [];% ⊦ m + n = n + m;% ⊦ (m + n0) + n1 = m + n0 + n1;% ⊦ ¬ m ≤ n ↔ n < m;% ⊦ (bits + bits0) + bits1 = bits + bits0 + bits1;% ⊦ # boolvar ' = 0 +1;% ⊦ #(bits + bits0) = # bits + # bits0;