| # ndx = # gndx, gndx + mkgnode(nd, n, ndx = [], false) ' = mkgnode(nd0, m, boolvar, boolvar0) ' + gndx0, gndx.head = mkgnode(nd2, m1, true, boolvar4), gndx0[# gndx - 1] = mkgnode(nd1, m0, boolvar1, boolvar2), gndx[# gndx] = mkgnode(nd4, m3, boolvar7, boolvar8), (mkgnode(nd0, m, true, boolvar0) ' + gndx0)[n0] = mkgnode(nd3, m2, boolvar5, boolvar6), mkgnode(nd0, m, boolvar, boolvar0) ∈ gndx, mkgnode(nd, n, ndx = [], false) ∈ gndx0, ∀ n0. (n0 ≠ 0 ∧ n0 < # gndx → ¬ gndx[n0].start) ∧ (n0 < # gndx → ¬ gndx[n0].end) ⊦ gndx = [], nd1 = nd, ndx1 = [] |
Used simplifier rules: ⊦ gnd + gndx = gnd ' + gndx; (s)% ⊦ #(gnd ' + gndx) = (# gndx)+1; (s)% ⊦ m +1 = m + 1; (s)%a: ⊦ (gndx + gndx0) + gndx1 = gndx + gndx0 + gndx1; from specification list[group-store]% ⊦ n ≤ m → m + n0 - n = (m - n) + n0; (s)% ⊦ n + 0 = n; (s)%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic%c: ⊦ m + n = n + m; from specification nat-basic% ⊦ (gnd ' + gndx)[n + 1] = gndx[n]; (s)% ⊦ gnd ' + gndx = gnd0 ' + gndx0 ↔ gnd = gnd0 ∧ gndx = gndx0; (ws)%⊦ mkgnode(nd, m, boolvar, boolvar0) = mkgnode(nd0, m0, boolvar1, boolvar2) ↔ nd = nd0 ∧ m = m0 ∧ (boolvar ↔ boolvar1) ∧ (boolvar0 ↔ boolvar2); (ws)% ⊦ gnd ' + gndx ≠ []; (s)% ⊦ gnd ∈ gnd0 ' + gndx ↔ gnd = gnd0 ∨ gnd ∈ gndx; (s)% ⊦ m < n + 1 ↔ ¬ n < m; (s)%in-15: ⊦ gndx + gnd ' = gndx0 → gnd ∈ gndx0; (forward) from specification list[group-store]% ⊦ (gndx + gnd ')[# gndx] = gnd; (s)%gndx ≠ [] ⊦ gnd = gndx.head ∧ gndx0 = gndx.tail ↔ gndx = gnd + gndx0; (elim) Used terms: gndx, gnd, gndx1