| # lpt = # avol, n0 < # avol ∧ lpf2 = LP_GROUP_NODES ↔ n0 ∈ gstore, lpt[n0] = mklp(m12, m13, lpf2, m14), gstore[n0] = groupblock(gndx2, lax2, m11), gstore[n] = groupblock(gndx0, lax0, m3), lpt[n] = mklp(m4, m5, lpf0, m6), gstore[n, groupblock(gndx, lax, m)][n0] = groupblock(gndx1, lax1, m7), lpt[n, mklp(m0, m1, lpf, m2)][n0] = mklp(m8, m9, lpf1, m10), n < # avol, ¬ n ∈ ginval ∧ (lpf0 = LP_GROUP_NODES → abs-leb(avol[n], groupblock(gndx0, lax0, m3), mklp(m4, m5, LP_GROUP_NODES, m6))) → abs-leb(aleb, groupblock(gndx, lax, m), mklp(m0, m1, lpf, m2)), (lpf0 = LP_GROUP_NODES → m4 = m3) → m0 = m ∧ lpf = LP_GROUP_NODES, n0 ∈ gstore ∧ ¬ n0 ∈ ginval → abs-leb(avol[n0], groupblock(gndx2, lax2, m11), mklp(m12, m13, lpf2, m14)), n0 ∈ gstore → m12 = m11 ⊦ (n0 < # avol ∧ lpf1 = LP_GROUP_NODES ↔ n0 ∈ gstore[n, groupblock(gndx, lax, m)]) ∧ (n0 ∈ gstore[n, groupblock(gndx, lax, m)] ∧ ¬ n0 ∈ ginval → abs-leb(avol[n, aleb][n0], groupblock(gndx1, lax1, m7), mklp(m8, m9, lpf1, m10))) ∧ (n0 ∈ gstore[n, groupblock(gndx, lax, m)] → m8 = m7) |
Used simplifier rules: ⊦ n ≠ n0 → gstore[n0, gblock][n] = gstore[n]; (s)% ⊦ m ≠ n → lpt[n, lp][m] = lpt[m]; (s)% ⊦ n ≠ n0 → (n ∈ gstore[n0, gblock] ↔ n ∈ gstore); (s)% ⊦ m ≠ n → avol[n, aleb][m] = avol[m]; (s)%⊦ groupblock(gndx, lax, m) = groupblock(gndx0, lax0, m0) ↔ gndx = gndx0 ∧ lax = lax0 ∧ m = m0; (ws)%⊦ mklp(m, m0, lpf, m1) = mklp(m2, m3, lpf0, m4) ↔ m = m2 ∧ m0 = m3 ∧ lpf = lpf0 ∧ m1 = m4; (ws)% ⊦ gstore[n, gblock][n] = gblock; (s)% ⊦ m < n ↔ ¬ n ≤ m; (ss)% ⊦ m < n → (n ≤ m ↔ false); (s)%m < # lpt ⊦ lpt[m, lp][m] = lp; (s)% ⊦ n ∈ gstore[n, gblock]; (s)% ⊦ m < # avol → avol[m, aleb][m] = aleb; (s) Used formulas: n0 = n