Proof step 1 from proof step-L2-L3 (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  # gs.y = gs.r, gs.y + (U(alltids, gs.ghostlspmxf) ∪ gs.gspmx).toMatrix(gs.r, # gs.x) * gs.x = gs.spmx.toMatrix(gs.r, # gs.x) * gs.x, gs.ghostlspmxf(ls.tid) = ∅, pcstepf(gs, ls, L2, a) = L3, alldisjointp(alltids, gs.ghostlspmxf), disjointp(U(alltids, gs.ghostlspmxf), gs.gspmx), okspmx(gs.spmx, gs.r, # gs.x), pre(gs, ls, L2, a), U(alltids, gs.ghostlspmxf) ∪ gs.gspmx ⊆ gs.spmx ⊦ ( alldisjointp(alltids, gstepf(gs, ls, L2, a).ghostlspmxf) ∧ disjointp(U(alltids, gstepf(gs, ls, L2, a).ghostlspmxf), gstepf(gs, ls, L2, a).gspmx) ∧ gstepf(gs, ls, L2, a).y + (U(alltids, gstepf(gs, ls, L2, a).ghostlspmxf) ∪ gstepf(gs, ls, L2, a).gspmx ).toMatrix (gstepf(gs, ls, L2, a).r, # gstepf(gs, ls, L2, a).x ) * gstepf(gs, ls, L2, a).x = gstepf(gs, ls, L2, a).spmx.toMatrix(gstepf(gs, ls, L2, a).r, # gstepf(gs, ls, L2, a).x) * gstepf(gs, ls, L2, a).x ∧ U(alltids, gstepf(gs, ls, L2, a).ghostlspmxf) ∪ gstepf(gs, ls, L2, a).gspmx ⊆ gstepf(gs, ls, L2, a).spmx ∧ # gstepf(gs, ls, L2, a).y = gstepf(gs, ls, L2, a).r ∧ okspmx(gstepf(gs, ls, L2, a).spmx, gstepf(gs, ls, L2, a).r, # gstepf(gs, ls, L2, a).x)) ∧ gstepf(gs, ls, L2, a).ghostlspmxf(lstepf(gs, ls, L2, a).tid) = lstepf(gs, ls, L2, a).lspmx

Rule argument

Additional information

Proof step 2 from proof step-L2-L3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  # gs.y = gs.r, gs.y + (U(alltids, gs.ghostlspmxf) ∪ gs.gspmx).toMatrix(gs.r, # gs.x) * gs.x = gs.spmx.toMatrix(gs.r, # gs.x) * gs.x, gs.ghostlspmxf(ls.tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, gs.ghostlspmxf), disjointp(U(alltids, gs.ghostlspmxf), gs.gspmx), okspmx(gs.spmx, gs.r, # gs.x), lspmx ⊆ gs.spmx, lspmx ⊆ gs.gspmx, U(alltids, gs.ghostlspmxf) ⊆ gs.spmx, gs.gspmx ⊆ gs.spmx ⊦ alldisjointp(alltids, gs.ghostlspmxf(ls.tid; lspmx)) ∧ disjointp(U(alltids, gs.ghostlspmxf(ls.tid; lspmx)), gs.gspmx \ dom lspmx) ∧ gs.y + (U(alltids, gs.ghostlspmxf(ls.tid; lspmx)) ∪ (gs.gspmx \ dom lspmx)).toMatrix(gs.r, # gs.x) * gs.x = gs.spmx.toMatrix(gs.r, # gs.x) * gs.x ∧ U(alltids, gs.ghostlspmxf(ls.tid; lspmx)) ∪ (gs.gspmx \ dom lspmx) ⊆ gs.spmx

Rule argument

Additional information

Used simplifier rules: pcstepf-L2: ⊦ pcstepf(gs, ls, L2, a) = (∃ lspmx0. a = chooseL2(lspmx0) ⊃ L3;L1); disj-35: ⊦ L1 ≠ L3; pre-L2: ⊦ pre(gs, ls, L2, a) ↔ (∃ lspmx0. (lspmx0 ≠ ∅ ∧ lspmx0 ⊆ gs.gspmx) ∧ a = chooseL2(lspmx0)) ∨ a = τ ∧ ¬(∃ lspmx0. lspmx0 ≠ ∅ ∧ lspmx0 ⊆ gs.gspmx); inj-04: ⊦ chooseL2(lspmx) = chooseL2(lspmx0) ↔ lspmx = lspmx0; disj-07: ⊦ τ ≠ chooseL2(lspmx); updsel-30: ⊦ (gs.ghostlspmxf:= ghostlspmxf).gspmx = gs.gspmx; updsel-26: ⊦ (gs.gspmx:= spmx0).gspmx = spmx0; updsel-48: ⊦ (gs.ghostlspmxf:= ghostlspmxf).y = gs.y; updsel-44: ⊦ (gs.gspmx:= spmx0).y = gs.y; updsel-24: ⊦ (gs.ghostlspmxf:= ghostlspmxf).spmx = gs.spmx; updsel-20: ⊦ (gs.gspmx:= spmx0).spmx = gs.spmx; updsel-36: ⊦ (gs.ghostlspmxf:= ghostlspmxf).r = gs.r; updsel-32: ⊦ (gs.gspmx:= spmx0).r = gs.r; updsel-42: ⊦ (gs.ghostlspmxf:= ghostlspmxf).x = gs.x; updsel-38: ⊦ (gs.gspmx:= spmx0).x = gs.x; gstepf-L2-1: ⊦ gstepf(gs, ls, L2, chooseL2(lspmx0)) = (gs.gspmx:= (gs.gspmx \ dom (ls.lspmx:= lspmx0).lspmx)) .ghostlspmxf:= gs.ghostlspmxf((ls.lspmx:= lspmx0).tid; (ls.lspmx:= lspmx0).lspmx); updsel-11: ⊦ (ls.lspmx:= lspmx).tid = ls.tid; updsel-54: ⊦ (gs.ghostlspmxf:= ghostlspmxf).ghostlspmxf = ghostlspmxf; lstepf-L2-1: ⊦ lstepf(gs, ls, L2, chooseL2(lspmx0)) = ls.lspmx:= lspmx0; updsel-14: ⊦ (ls.lspmx:= lspmx).lspmx = lspmx; sub-trans: ⊦ st ⊆ st0 ∧ st0 ⊆ st1 → st ⊆ st1; (forward) from specification store[sparsearray] ⊦ disjointp(spmx1, spmx2) → (spmx1 ∪ spmx2 ⊆ spmx ↔ spmx1 ⊆ spmx ∧ spmx2 ⊆ spmx); (ws)

Proof step 3 from proof step-L2-L3 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 4:

  ⊦ ((((spmx = gs.spmx ∧ gspmx = gs.gspmx) ∧ r = gs.r) ∧ x = gs.x) ∧ y = gs.y) ∧ ghostlspmxf = gs.ghostlspmxf ↔ gs = mkgs(spmx, gspmx, r, x, y, ghostlspmxf)

• Proof step 5:

  # y = r, y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(r, # x) * x = spmx.toMatrix(r, # x) * x, ghostlspmxf(ls.tid) = ∅, gs = mkgs(spmx, gspmx, r, x, y, ghostlspmxf), lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, r, # x), gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx, lspmx ⊆ spmx ⊦ alldisjointp(alltids, ghostlspmxf(ls.tid; lspmx)) ∧ disjointp(U(alltids, ghostlspmxf(ls.tid; lspmx)), gspmx \ dom lspmx) ∧ y + (U(alltids, ghostlspmxf(ls.tid; lspmx)) ∪ (gspmx \ dom lspmx)).toMatrix(r, # x) * x = spmx.toMatrix(r, # x) * x ∧ U(alltids, ghostlspmxf(ls.tid; lspmx)) ∪ (gspmx \ dom lspmx) ⊆ spmx

Rule argument

Additional information

Used terms: y, gs, gspmx, ghostlspmxf, spmx, r, x

Proof step 4 from proof step-L2-L3 (previous step) (back to tree)

Lemma elim-03

Proof step 5 from proof step-L2-L3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(ls.tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx ⊦ alldisjointp(alltids, ghostlspmxf(ls.tid; lspmx)) ∧ disjointp(U(alltids, ghostlspmxf(ls.tid; lspmx)), gspmx \ dom lspmx) ∧ y + (U(alltids, ghostlspmxf(ls.tid; lspmx)) ∪ (gspmx \ dom lspmx)).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x ∧ U(alltids, ghostlspmxf(ls.tid; lspmx)) ∪ (gspmx \ dom lspmx) ⊆ spmx

Rule argument

Additional information

Used simplifier rules: sub-trans: ⊦ st ⊆ st0 ∧ st0 ⊆ st1 → st ⊆ st1; (forward) from specification store[sparsearray]

Proof step 6 from proof step-L2-L3 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 7:

  ⊦ ((tid = ls.tid ∧ lspmx = ls.lspmx) ∧ np = ls.np) ∧ val = ls.val ↔ ls = mkls(tid, lspmx, np, val)

• Proof step 8:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid) = ∅, ls = mkls(tid, lspmx0, np, val), lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx ⊦ alldisjointp(alltids, ghostlspmxf(tid; lspmx)) ∧ disjointp(U(alltids, ghostlspmxf(tid; lspmx)), gspmx \ dom lspmx) ∧ y + (U(alltids, ghostlspmxf(tid; lspmx)) ∪ (gspmx \ dom lspmx)).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x ∧ U(alltids, ghostlspmxf(tid; lspmx)) ∪ (gspmx \ dom lspmx) ⊆ spmx

Rule argument

Additional information

Used terms: val, lspmx0, np, tid, ls

Proof step 7 from proof step-L2-L3 (previous step) (back to tree)

Lemma elim-02

Proof step 8 from proof step-L2-L3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx ⊦ alldisjointp(alltids, ghostlspmxf(tid; lspmx)) ∧ disjointp(U(alltids, ghostlspmxf(tid; lspmx)), gspmx \ dom lspmx) ∧ y + (U(alltids, ghostlspmxf(tid; lspmx)) ∪ (gspmx \ dom lspmx)).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x ∧ U(alltids, ghostlspmxf(tid; lspmx)) ∪ (gspmx \ dom lspmx) ⊆ spmx

Rule argument

Additional information

Proof step 9 from proof step-L2-L3 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 10:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; lspmx)), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx ⊦ alldisjointp(alltids, ghostlspmxf(tid; lspmx)) ∧ disjointp(U(alltids, ghostlspmxf(tid; lspmx)), gspmx \ dom lspmx) ∧ y + (U(alltids, ghostlspmxf(tid; lspmx)) ∪ (gspmx \ dom lspmx)).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x ∧ U(alltids, ghostlspmxf(tid; lspmx)) ∪ (gspmx \ dom lspmx) ⊆ spmx

• Proof step 115:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx, ¬ alldisjointp(alltids, ghostlspmxf(tid; lspmx)) ⊦ alldisjointp(alltids, ghostlspmxf(tid; lspmx)) ∧ disjointp(U(alltids, ghostlspmxf(tid; lspmx)), gspmx \ dom lspmx) ∧ y + (U(alltids, ghostlspmxf(tid; lspmx)) ∪ (gspmx \ dom lspmx)).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x ∧ U(alltids, ghostlspmxf(tid; lspmx)) ∪ (gspmx \ dom lspmx) ⊆ spmx

Rule argument

Additional information

Used formulas: alldisjointp(alltids, ghostlspmxf(tid; lspmx))

Proof step 10 from proof step-L2-L3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf(tid; lspmx)), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx ⊦ disjointp(U(alltids, ghostlspmxf(tid; lspmx)), gspmx \ dom lspmx) ∧ y + (U(alltids, ghostlspmxf(tid; lspmx)) ∪ (gspmx \ dom lspmx)).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x ∧ U(alltids, ghostlspmxf(tid; lspmx)) ∪ (gspmx \ dom lspmx) ⊆ spmx

Rule argument

Additional information

Proof step 11 from proof step-L2-L3 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 12:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, U(alltids, ghostlspmxf(tid; lspmx)) = U(alltids, ghostlspmxf) ∪ lspmx, ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; lspmx)), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx ⊦ disjointp(U(alltids, ghostlspmxf(tid; lspmx)), gspmx \ dom lspmx) ∧ y + (U(alltids, ghostlspmxf(tid; lspmx)) ∪ (gspmx \ dom lspmx)).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x ∧ U(alltids, ghostlspmxf(tid; lspmx)) ∪ (gspmx \ dom lspmx) ⊆ spmx

• Proof step 82:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid) = ∅, U(alltids, ghostlspmxf(tid; lspmx)) ≠ U(alltids, ghostlspmxf) ∪ lspmx, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; lspmx)), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx ⊦ disjointp(U(alltids, ghostlspmxf(tid; lspmx)), gspmx \ dom lspmx) ∧ y + (U(alltids, ghostlspmxf(tid; lspmx)) ∪ (gspmx \ dom lspmx)).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x ∧ U(alltids, ghostlspmxf(tid; lspmx)) ∪ (gspmx \ dom lspmx) ⊆ spmx

Rule argument

Additional information

Used formulas: U(alltids, ghostlspmxf(tid; lspmx)) = U(alltids, ghostlspmxf) ∪ lspmx

Proof step 12 from proof step-L2-L3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, U(alltids, ghostlspmxf(tid; lspmx)) = U(alltids, ghostlspmxf) ∪ lspmx, ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf(tid; lspmx)), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx ⊦ disjointp(U(alltids, ghostlspmxf) ∪ lspmx, gspmx \ dom lspmx) ∧ y + ((U(alltids, ghostlspmxf) ∪ lspmx) ∪ (gspmx \ dom lspmx)).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x ∧ (U(alltids, ghostlspmxf) ∪ lspmx) ∪ (gspmx \ dom lspmx) ⊆ spmx

Rule argument

Additional information

Proof step 13 from proof step-L2-L3 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 14:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, U(alltids, ghostlspmxf(tid; lspmx)) = U(alltids, ghostlspmxf) ∪ lspmx, ghostlspmxf(tid) = ∅, (U(alltids, ghostlspmxf) ∪ lspmx) ∪ (gspmx \ dom lspmx) = U(alltids, ghostlspmxf) ∪ gspmx, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; lspmx)), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx ⊦ disjointp(U(alltids, ghostlspmxf) ∪ lspmx, gspmx \ dom lspmx) ∧ y + ((U(alltids, ghostlspmxf) ∪ lspmx) ∪ (gspmx \ dom lspmx)).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x ∧ (U(alltids, ghostlspmxf) ∪ lspmx) ∪ (gspmx \ dom lspmx) ⊆ spmx

• Proof step 23:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, U(alltids, ghostlspmxf(tid; lspmx)) = U(alltids, ghostlspmxf) ∪ lspmx, ghostlspmxf(tid) = ∅, lspmx ≠ ∅, (U(alltids, ghostlspmxf) ∪ lspmx) ∪ (gspmx \ dom lspmx) ≠ U(alltids, ghostlspmxf) ∪ gspmx, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; lspmx)), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx ⊦ disjointp(U(alltids, ghostlspmxf) ∪ lspmx, gspmx \ dom lspmx) ∧ y + ((U(alltids, ghostlspmxf) ∪ lspmx) ∪ (gspmx \ dom lspmx)).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x ∧ (U(alltids, ghostlspmxf) ∪ lspmx) ∪ (gspmx \ dom lspmx) ⊆ spmx

Rule argument

Additional information

Used formulas: (U(alltids, ghostlspmxf) ∪ lspmx) ∪ (gspmx \ dom lspmx) = U(alltids, ghostlspmxf) ∪ gspmx

Proof step 14 from proof step-L2-L3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, U(alltids, ghostlspmxf(tid; lspmx)) = U(alltids, ghostlspmxf) ∪ lspmx, ghostlspmxf(tid) = ∅, (U(alltids, ghostlspmxf) ∪ lspmx) ∪ (gspmx \ dom lspmx) = U(alltids, ghostlspmxf) ∪ gspmx, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; lspmx)), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx, ¬ disjointp(U(alltids, ghostlspmxf) ∪ lspmx, gspmx \ dom lspmx) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ disjointp(spmx1, spmx2) → (spmx1 ∪ spmx2 ⊆ spmx ↔ spmx1 ⊆ spmx ∧ spmx2 ⊆ spmx); (ws)

Proof step 15 from proof step-L2-L3 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

  ⊦ disjointp(sa1, sa2) ↔ (∀ np. np ∈ sa1 → ¬ np ∈ sa2)

• Proof step 17:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, U(alltids, ghostlspmxf(tid; lspmx)) = U(alltids, ghostlspmxf) ∪ lspmx, ghostlspmxf(tid) = ∅, (U(alltids, ghostlspmxf) ∪ lspmx) ∪ (gspmx \ dom lspmx) = U(alltids, ghostlspmxf) ∪ gspmx, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf(tid; lspmx)), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx, ∃ np. ¬(np ∈ U(alltids, ghostlspmxf) ∪ lspmx → ¬ np ∈ gspmx \ dom lspmx) ⊦

Rule argument

Additional information

Used terms: U(alltids, ghostlspmxf) ∪ lspmx, gspmx \ dom lspmx

Proof step 16 from proof step-L2-L3 (previous step) (back to tree)

A spec-lemma

Proof step 17 from proof step-L2-L3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, U(alltids, ghostlspmxf(tid; lspmx)) = U(alltids, ghostlspmxf) ∪ lspmx, ghostlspmxf(tid) = ∅, (U(alltids, ghostlspmxf) ∪ lspmx) ∪ (gspmx \ dom lspmx) = U(alltids, ghostlspmxf) ∪ gspmx, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; lspmx)), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ gspmx, np ∈ ghostlspmxf(tid0), lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx, ¬ np ∈ lspmx ⊦

Rule argument

Additional information

Used simplifier rules: alltids-all: ⊦ tid ∈ alltids; ⊦ alldisjointp(ts, f) → (np ∈ U(ts, f) ↔ (∃ tid. tid ∈ ts ∧ np ∈ f(tid))); (s) ⊦ np ∈ spmx1 ∪ spmx2 ↔ np ∈ spmx1 ∨ np ∈ spmx2; (ws) ⊦ a ∈ dom st ↔ a ∈ st; (s) ⊦ a ∈ st \ s ↔ a ∈ st ∧ ¬ a ∈ s; (ws)

Proof step 18 from proof step-L2-L3 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

  ⊦ disjointp(sa1, sa2) ↔ (∀ np. np ∈ sa1 → ¬ np ∈ sa2)

• Proof step 20:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, U(alltids, ghostlspmxf(tid; lspmx)) = U(alltids, ghostlspmxf) ∪ lspmx, ghostlspmxf(tid) = ∅, (U(alltids, ghostlspmxf) ∪ lspmx) ∪ (gspmx \ dom lspmx) = U(alltids, ghostlspmxf) ∪ gspmx, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf(tid; lspmx)), alldisjointp(alltids, ghostlspmxf), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid0), np ∈ gspmx, lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx, ¬ np ∈ lspmx, ∀ np. np ∈ U(alltids, ghostlspmxf) → ¬ np ∈ gspmx ⊦

Rule argument

Additional information

Used terms: U(alltids, ghostlspmxf), gspmx

Proof step 19 from proof step-L2-L3 (previous step) (back to tree)

A spec-lemma

Proof step 20 from proof step-L2-L3 (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And obtained the following new goals

• Proof step 21:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, U(alltids, ghostlspmxf(tid; lspmx)) = U(alltids, ghostlspmxf) ∪ lspmx, ghostlspmxf(tid) = ∅, (U(alltids, ghostlspmxf) ∪ lspmx) ∪ (gspmx \ dom lspmx) = U(alltids, ghostlspmxf) ∪ gspmx, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; lspmx)), okspmx(spmx, # y, # x), np ∈ gspmx, np ∈ ghostlspmxf(tid0), lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx, ¬ np ∈ lspmx, np ∈ U(alltids, ghostlspmxf) → ¬ np ∈ gspmx, ∀ np. np ∈ U(alltids, ghostlspmxf) → ¬ np ∈ gspmx ⊦

Rule argument

Additional information

Used terms: np

Proof step 21 from proof step-L2-L3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, U(alltids, ghostlspmxf(tid; lspmx)) = U(alltids, ghostlspmxf) ∪ lspmx, ghostlspmxf(tid) = ∅, (U(alltids, ghostlspmxf) ∪ lspmx) ∪ (gspmx \ dom lspmx) = U(alltids, ghostlspmxf) ∪ gspmx, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf(tid; lspmx)), alldisjointp(alltids, ghostlspmxf), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid0), np ∈ gspmx, lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx, ¬ np ∈ lspmx, ∀ np0. (∃ tid1. np0 ∈ ghostlspmxf(tid1)) → ¬ np0 ∈ gspmx ⊦ ∃ tid1. np ∈ ghostlspmxf(tid1)

Rule argument

Additional information

Used simplifier rules: alltids-all: ⊦ tid ∈ alltids; ⊦ alldisjointp(ts, f) → (np ∈ U(ts, f) ↔ (∃ tid. tid ∈ ts ∧ np ∈ f(tid))); (s)

Proof step 22 from proof step-L2-L3 (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: tid0

Proof step 23 from proof step-L2-L3 (previous step) (back to tree)

User applied rule weakening

And obtained the following new goals

• Proof step 24:

  U(alltids, ghostlspmxf(tid; lspmx)) = U(alltids, ghostlspmxf) ∪ lspmx, ghostlspmxf(tid) = ∅, lspmx ≠ ∅, (U(alltids, ghostlspmxf) ∪ lspmx) ∪ (gspmx \ dom lspmx) ≠ U(alltids, ghostlspmxf) ∪ gspmx, alldisjointp(alltids, ghostlspmxf(tid; lspmx)), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx ⊦

Rule argument

Additional information

Proof step 24 from proof step-L2-L3 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 25:

  ⊦ st1 = st2 ↔ (∀ a. (a ∈ st1 ↔ a ∈ st2) ∧ st1[a] = st2[a])

• Proof step 26:

  U(alltids, ghostlspmxf(tid; lspmx)) = U(alltids, ghostlspmxf) ∪ lspmx, ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; lspmx)), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx, ∃ np. ¬ ( (np ∈ (U(alltids, ghostlspmxf) ∪ lspmx) ∪ (gspmx \ dom lspmx) ↔ np ∈ U(alltids, ghostlspmxf) ∪ gspmx) ∧ ((U(alltids, ghostlspmxf) ∪ lspmx) ∪ (gspmx \ dom lspmx))[np] = (U(alltids, ghostlspmxf) ∪ gspmx)[np]) ⊦

Rule argument

Additional information

Used terms: (U(alltids, ghostlspmxf) ∪ lspmx) ∪ (gspmx \ dom lspmx), U(alltids, ghostlspmxf) ∪ gspmx

Proof step 25 from proof step-L2-L3 (previous step) (back to tree)

A spec-lemma

Proof step 26 from proof step-L2-L3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  U(alltids, ghostlspmxf(tid; lspmx)) = U(alltids, ghostlspmxf) ∪ lspmx, ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf(tid; lspmx)), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx ⊦ (np ∈ (U(alltids, ghostlspmxf) ∪ lspmx) ∪ (gspmx \ dom lspmx) ↔ np ∈ U(alltids, ghostlspmxf) ∪ gspmx) ∧ (np ∈ U(alltids, ghostlspmxf) ∪ lspmx ⊃ (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ U(alltids, ghostlspmxf)[np];lspmx[np]);(gspmx \ dom lspmx)[np]) = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ U(alltids, ghostlspmxf)[np];gspmx[np])

Rule argument

Additional information

Used simplifier rules: alltids-all: ⊦ tid ∈ alltids; ⊦ alldisjointp(ts, f) → (np ∈ U(ts, f) ↔ (∃ tid. tid ∈ ts ∧ np ∈ f(tid))); (s) ⊦ (spmx1 ∪ spmx2)[np] = (np ∈ spmx1 ⊃ spmx1[np];spmx2[np]); (s)

Proof step 27 from proof step-L2-L3 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 28:

  ⊦ st1 = st2 ↔ (∀ a. (a ∈ st1 ↔ a ∈ st2) ∧ st1[a] = st2[a])

• Proof step 29:

  ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; lspmx)), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx, ∀ np. (np ∈ U(alltids, ghostlspmxf(tid; lspmx)) ↔ np ∈ U(alltids, ghostlspmxf) ∪ lspmx) ∧ U(alltids, ghostlspmxf(tid; lspmx))[np] = (U(alltids, ghostlspmxf) ∪ lspmx)[np] ⊦ (np ∈ (U(alltids, ghostlspmxf) ∪ lspmx) ∪ (gspmx \ dom lspmx) ↔ np ∈ U(alltids, ghostlspmxf) ∪ gspmx) ∧ (np ∈ U(alltids, ghostlspmxf) ∪ lspmx ⊃ (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ U(alltids, ghostlspmxf)[np];lspmx[np]);(gspmx \ dom lspmx)[np]) = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ U(alltids, ghostlspmxf)[np];gspmx[np])

Rule argument

Additional information

Used terms: U(alltids, ghostlspmxf(tid; lspmx)), U(alltids, ghostlspmxf) ∪ lspmx

Proof step 28 from proof step-L2-L3 (previous step) (back to tree)

A spec-lemma

Proof step 29 from proof step-L2-L3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

  ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf(tid; lspmx)), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx, ∀ np0. ((∃ tid0. np0 ∈ (tid = tid0 ⊃ lspmx;ghostlspmxf(tid0))) ↔ np0 ∈ U(alltids, ghostlspmxf) ∪ lspmx) ∧ U(alltids, ghostlspmxf(tid; lspmx))[np0] = (∃ tid0. np0 ∈ ghostlspmxf(tid0) ⊃ U(alltids, ghostlspmxf)[np0];lspmx[np0]) ⊦ (np ∈ (U(alltids, ghostlspmxf) ∪ lspmx) ∪ (gspmx \ dom lspmx) ↔ np ∈ U(alltids, ghostlspmxf) ∪ gspmx) ∧ (np ∈ U(alltids, ghostlspmxf) ∪ lspmx ⊃ (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ U(alltids, ghostlspmxf)[np];lspmx[np]);(gspmx \ dom lspmx)[np]) = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ U(alltids, ghostlspmxf)[np];gspmx[np])

Rule argument

Additional information

Used simplifier rules: alltids-all: ⊦ tid ∈ alltids; ⊦ alldisjointp(ts, f) → (np ∈ U(ts, f) ↔ (∃ tid. tid ∈ ts ∧ np ∈ f(tid))); (s) ⊦ (spmx1 ∪ spmx2)[np] = (np ∈ spmx1 ⊃ spmx1[np];spmx2[np]); (s)

Proof step 30 from proof step-L2-L3 (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 31:

  ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; lspmx)), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx, (∃ tid0. np ∈ (tid = tid0 ⊃ lspmx;ghostlspmxf(tid0))) ↔ np ∈ U(alltids, ghostlspmxf) ∪ lspmx, U(alltids, ghostlspmxf(tid; lspmx))[np] = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ U(alltids, ghostlspmxf)[np];lspmx[np]) ⊦ (np ∈ (U(alltids, ghostlspmxf) ∪ lspmx) ∪ (gspmx \ dom lspmx) ↔ np ∈ U(alltids, ghostlspmxf) ∪ gspmx) ∧ (np ∈ U(alltids, ghostlspmxf) ∪ lspmx ⊃ (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ U(alltids, ghostlspmxf)[np];lspmx[np]);(gspmx \ dom lspmx)[np]) = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ U(alltids, ghostlspmxf)[np];gspmx[np])

Rule argument

Additional information

Used terms: np

Proof step 31 from proof step-L2-L3 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 32:

  ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf(tid; lspmx)), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ U(alltids, ghostlspmxf), lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx, (∃ tid0. np ∈ (tid = tid0 ⊃ lspmx;ghostlspmxf(tid0))) ↔ np ∈ U(alltids, ghostlspmxf) ∪ lspmx, U(alltids, ghostlspmxf(tid; lspmx))[np] = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ U(alltids, ghostlspmxf)[np];lspmx[np]) ⊦ (np ∈ (U(alltids, ghostlspmxf) ∪ lspmx) ∪ (gspmx \ dom lspmx) ↔ np ∈ U(alltids, ghostlspmxf) ∪ gspmx) ∧ (np ∈ U(alltids, ghostlspmxf) ∪ lspmx ⊃ (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ U(alltids, ghostlspmxf)[np];lspmx[np]);(gspmx \ dom lspmx)[np]) = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ U(alltids, ghostlspmxf)[np];gspmx[np])

• Proof step 58:

  ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf(tid; lspmx)), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx, ¬ np ∈ U(alltids, ghostlspmxf), (∃ tid0. np ∈ (tid = tid0 ⊃ lspmx;ghostlspmxf(tid0))) ↔ np ∈ U(alltids, ghostlspmxf) ∪ lspmx, U(alltids, ghostlspmxf(tid; lspmx))[np] = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ U(alltids, ghostlspmxf)[np];lspmx[np]) ⊦ (np ∈ (U(alltids, ghostlspmxf) ∪ lspmx) ∪ (gspmx \ dom lspmx) ↔ np ∈ U(alltids, ghostlspmxf) ∪ gspmx) ∧ (np ∈ U(alltids, ghostlspmxf) ∪ lspmx ⊃ (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ U(alltids, ghostlspmxf)[np];lspmx[np]);(gspmx \ dom lspmx)[np]) = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ U(alltids, ghostlspmxf)[np];gspmx[np])

Rule argument

Additional information

Used formulas: np ∈ U(alltids, ghostlspmxf)

Proof step 32 from proof step-L2-L3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

  ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; lspmx)), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid0), lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx, (∃ tid0. np ∈ (tid = tid0 ⊃ lspmx;ghostlspmxf(tid0))) ↔ np ∈ U(alltids, ghostlspmxf) ∪ lspmx, U(alltids, ghostlspmxf(tid; lspmx))[np] = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];lspmx[np]) ⊦ (np ∈ (U(alltids, ghostlspmxf) ∪ lspmx) ∪ (gspmx \ dom lspmx) ↔ np ∈ U(alltids, ghostlspmxf) ∪ gspmx) ∧ (np ∈ U(alltids, ghostlspmxf) ∪ lspmx ⊃ (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];lspmx[np]);(gspmx \ dom lspmx)[np]) = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];gspmx[np])

Rule argument

Additional information

Used simplifier rules: alltids-all: ⊦ tid ∈ alltids; ⊦ alldisjointp(ts, f) ∧ np ∈ f(tid) → U(ts, f)[np] = f(tid)[np]; (s) ⊦ alldisjointp(ts, f) → (np ∈ U(ts, f) ↔ (∃ tid. tid ∈ ts ∧ np ∈ f(tid))); (s)

Proof step 33 from proof step-L2-L3 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 34:

  ghostlspmxf(tid) = ∅, ¬(np ∈ (U(alltids, ghostlspmxf) ∪ lspmx) ∪ (gspmx \ dom lspmx) ↔ np ∈ U(alltids, ghostlspmxf) ∪ gspmx), lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf(tid; lspmx)), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid0), lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx, (∃ tid0. np ∈ (tid = tid0 ⊃ lspmx;ghostlspmxf(tid0))) ↔ np ∈ U(alltids, ghostlspmxf) ∪ lspmx, U(alltids, ghostlspmxf(tid; lspmx))[np] = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];lspmx[np]) ⊦

• Proof step 39:

  ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf(tid; lspmx)), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid0), lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx, (∃ tid0. np ∈ (tid = tid0 ⊃ lspmx;ghostlspmxf(tid0))) ↔ np ∈ U(alltids, ghostlspmxf) ∪ lspmx, U(alltids, ghostlspmxf(tid; lspmx))[np] = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];lspmx[np]) ⊦ (np ∈ U(alltids, ghostlspmxf) ∪ lspmx ⊃ (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];lspmx[np]);(gspmx \ dom lspmx)[np]) = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];gspmx[np])

Rule argument

Additional information

Proof step 34 from proof step-L2-L3 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 35:

  ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; lspmx)), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid0), np ∈ (U(alltids, ghostlspmxf) ∪ lspmx) ∪ (gspmx \ dom lspmx), lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx, ¬ np ∈ U(alltids, ghostlspmxf) ∪ gspmx, (∃ tid0. np ∈ (tid = tid0 ⊃ lspmx;ghostlspmxf(tid0))) ↔ np ∈ U(alltids, ghostlspmxf) ∪ lspmx, U(alltids, ghostlspmxf(tid; lspmx))[np] = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];lspmx[np]) ⊦

• Proof step 37:

  ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; lspmx)), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid0), np ∈ U(alltids, ghostlspmxf) ∪ gspmx, lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx, ¬ np ∈ (U(alltids, ghostlspmxf) ∪ lspmx) ∪ (gspmx \ dom lspmx), (∃ tid0. np ∈ (tid = tid0 ⊃ lspmx;ghostlspmxf(tid0))) ↔ np ∈ U(alltids, ghostlspmxf) ∪ lspmx, U(alltids, ghostlspmxf(tid; lspmx))[np] = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];lspmx[np]) ⊦

Rule argument

Additional information

Proof step 35 from proof step-L2-L3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 36:

  ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; lspmx)), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid0), np ∈ (U(alltids, ghostlspmxf) ∪ lspmx) ∪ (gspmx \ dom lspmx), np ∈ (tid = tid1 ⊃ lspmx;ghostlspmxf(tid1)), np ∈ U(alltids, ghostlspmxf) ∪ lspmx, lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx, ¬ np ∈ gspmx, U(alltids, ghostlspmxf(tid; lspmx))[np] = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];lspmx[np]) ⊦ ∃ tid1. np ∈ ghostlspmxf(tid1)

Rule argument

Additional information

Used simplifier rules: alltids-all: ⊦ tid ∈ alltids; ⊦ a ∈ st \ s ↔ a ∈ st ∧ ¬ a ∈ s; (ws) ⊦ np ∈ spmx1 ∪ spmx2 ↔ np ∈ spmx1 ∨ np ∈ spmx2; (ws) ⊦ alldisjointp(ts, f) → (np ∈ U(ts, f) ↔ (∃ tid. tid ∈ ts ∧ np ∈ f(tid))); (s)

Proof step 36 from proof step-L2-L3 (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: tid0

Proof step 37 from proof step-L2-L3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 38:

  ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf(tid; lspmx)), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ U(alltids, ghostlspmxf) ∪ gspmx, np ∈ ghostlspmxf(tid0), lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx, ¬ np ∈ gspmx \ dom lspmx, ¬ np ∈ lspmx, U(alltids, ghostlspmxf(tid; lspmx))[np] = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];∅[np]) ⊦ ∃ tid1. np ∈ ghostlspmxf(tid1), ∃ tid0. np ∈ (tid = tid0 ⊃ lspmx;ghostlspmxf(tid0))

Rule argument

Additional information

Used simplifier rules: alltids-all: ⊦ tid ∈ alltids; ⊦ alldisjointp(ts, f) → (np ∈ U(ts, f) ↔ (∃ tid. tid ∈ ts ∧ np ∈ f(tid))); (s) ⊦ np ∈ spmx1 ∪ spmx2 ↔ np ∈ spmx1 ∨ np ∈ spmx2; (ws) ⊦ ¬ a ∈ st → st[a] = ∅[a]; (s)

Proof step 38 from proof step-L2-L3 (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: tid0

Proof step 39 from proof step-L2-L3 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 40:

  ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; lspmx)), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid0), np ∈ U(alltids, ghostlspmxf) ∪ lspmx, lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx, (∃ tid0. np ∈ (tid = tid0 ⊃ lspmx;ghostlspmxf(tid0))) ↔ np ∈ U(alltids, ghostlspmxf) ∪ lspmx, U(alltids, ghostlspmxf(tid; lspmx))[np] = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];lspmx[np]) ⊦ (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];lspmx[np]) = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];gspmx[np])

• Proof step 56:

  ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; lspmx)), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid0), lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx, ¬ np ∈ U(alltids, ghostlspmxf) ∪ lspmx, (∃ tid0. np ∈ (tid = tid0 ⊃ lspmx;ghostlspmxf(tid0))) ↔ np ∈ U(alltids, ghostlspmxf) ∪ lspmx, U(alltids, ghostlspmxf(tid; lspmx))[np] = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];lspmx[np]) ⊦ (gspmx \ dom lspmx)[np] = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];gspmx[np])

Rule argument

Additional information

Proof step 40 from proof step-L2-L3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 41:

  ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf(tid; lspmx)), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ U(alltids, ghostlspmxf) ∪ lspmx, np ∈ ghostlspmxf(tid0), np ∈ (tid = tid1 ⊃ lspmx;ghostlspmxf(tid1)), lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx, U(alltids, ghostlspmxf(tid; lspmx))[np] = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];lspmx[np]) ⊦ (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];lspmx[np]) = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];gspmx[np])

Rule argument

Additional information

Proof step 41 from proof step-L2-L3 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 42:

  ghostlspmxf(tid) = ∅, tid = tid1, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; lspmx)), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid0), np ∈ U(alltids, ghostlspmxf) ∪ lspmx, np ∈ lspmx, lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx, U(alltids, ghostlspmxf(tid; lspmx))[np] = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];lspmx[np]) ⊦ (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];lspmx[np]) = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];gspmx[np])

• Proof step 48:

  ghostlspmxf(tid) = ∅, lspmx ≠ ∅, tid ≠ tid1, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; lspmx)), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid0), np ∈ U(alltids, ghostlspmxf) ∪ lspmx, np ∈ ghostlspmxf(tid1), lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx, U(alltids, ghostlspmxf(tid; lspmx))[np] = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];lspmx[np]) ⊦ (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];lspmx[np]) = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];gspmx[np])

Rule argument

Additional information

Proof step 42 from proof step-L2-L3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 43:

  ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf(tid; lspmx)), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ lspmx, np ∈ U(alltids, ghostlspmxf) ∪ lspmx, np ∈ ghostlspmxf(tid0), lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx, U(alltids, ghostlspmxf(tid; lspmx))[np] = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];lspmx[np]) ⊦ (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];lspmx[np]) = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];gspmx[np])

Rule argument

Additional information

Proof step 43 from proof step-L2-L3 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 44:

  ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; lspmx)), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid0), np ∈ U(alltids, ghostlspmxf) ∪ lspmx, np ∈ lspmx, lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx, ∃ tid0. np ∈ ghostlspmxf(tid0), U(alltids, ghostlspmxf(tid; lspmx))[np] = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];lspmx[np]) ⊦ ghostlspmxf(tid0)[np] = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];gspmx[np])

• Proof step 47:

  ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; lspmx)), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid0), np ∈ U(alltids, ghostlspmxf) ∪ lspmx, np ∈ lspmx, lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx, ∀ tid0. ¬ np ∈ ghostlspmxf(tid0), U(alltids, ghostlspmxf(tid; lspmx))[np] = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];lspmx[np]) ⊦ lspmx[np] = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];gspmx[np])

Rule argument

Additional information

Proof step 44 from proof step-L2-L3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 45:

  ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf(tid; lspmx)), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid1), np ∈ lspmx, np ∈ U(alltids, ghostlspmxf) ∪ lspmx, np ∈ ghostlspmxf(tid0), lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx, U(alltids, ghostlspmxf(tid; lspmx))[np] = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];lspmx[np]) ⊦ ghostlspmxf(tid0)[np] = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];gspmx[np])

Rule argument

Additional information

Proof step 45 from proof step-L2-L3 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 46:

  ghostlspmxf(tid) = ∅, ghostlspmxf(tid0)[np] ≠ gspmx[np], lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; lspmx)), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid0), np ∈ U(alltids, ghostlspmxf) ∪ lspmx, np ∈ lspmx, np ∈ ghostlspmxf(tid1), lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx, ∀ tid0. ¬ np ∈ ghostlspmxf(tid0), U(alltids, ghostlspmxf(tid; lspmx))[np] = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];lspmx[np]) ⊦

Rule argument

Additional information

Proof step 46 from proof step-L2-L3 (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: tid1

Proof step 47 from proof step-L2-L3 (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: tid0

Proof step 48 from proof step-L2-L3 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 49:

  U(alltids, ghostlspmxf(tid; lspmx))[np] = ghostlspmxf(tid0)[np], ghostlspmxf(tid) = ∅, lspmx ≠ ∅, tid ≠ tid1, alldisjointp(alltids, ghostlspmxf(tid; lspmx)), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid1), np ∈ U(alltids, ghostlspmxf) ∪ lspmx, np ∈ ghostlspmxf(tid0), lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx, ∃ tid0. np ∈ ghostlspmxf(tid0) ⊦ (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];lspmx[np]) = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];gspmx[np])

• Proof step 55:

  U(alltids, ghostlspmxf(tid; lspmx))[np] = lspmx[np], ghostlspmxf(tid) = ∅, lspmx ≠ ∅, tid ≠ tid1, alldisjointp(alltids, ghostlspmxf(tid; lspmx)), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid1), np ∈ U(alltids, ghostlspmxf) ∪ lspmx, np ∈ ghostlspmxf(tid0), lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx, ∀ tid0. ¬ np ∈ ghostlspmxf(tid0) ⊦ (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];lspmx[np]) = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];gspmx[np])

Rule argument

Additional information

Proof step 49 from proof step-L2-L3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 50:

  U(alltids, ghostlspmxf(tid; lspmx))[np] = ghostlspmxf(tid0)[np], ghostlspmxf(tid) = ∅, lspmx ≠ ∅, tid ≠ tid1, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; lspmx)), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid2), np ∈ ghostlspmxf(tid0), np ∈ U(alltids, ghostlspmxf) ∪ lspmx, np ∈ ghostlspmxf(tid1), lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx ⊦ (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];lspmx[np]) = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];gspmx[np])

Rule argument

Additional information

Proof step 50 from proof step-L2-L3 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 51:

  U(alltids, ghostlspmxf(tid; lspmx))[np] = ghostlspmxf(tid0)[np], ghostlspmxf(tid) = ∅, lspmx ≠ ∅, tid ≠ tid1, alldisjointp(alltids, ghostlspmxf(tid; lspmx)), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid1), np ∈ U(alltids, ghostlspmxf) ∪ lspmx, np ∈ ghostlspmxf(tid0), np ∈ ghostlspmxf(tid2), lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx, ∃ tid0. np ∈ ghostlspmxf(tid0) ⊦ ghostlspmxf(tid0)[np] = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];gspmx[np])

• Proof step 54:

  U(alltids, ghostlspmxf(tid; lspmx))[np] = ghostlspmxf(tid0)[np], ghostlspmxf(tid) = ∅, lspmx ≠ ∅, tid ≠ tid1, alldisjointp(alltids, ghostlspmxf(tid; lspmx)), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid1), np ∈ U(alltids, ghostlspmxf) ∪ lspmx, np ∈ ghostlspmxf(tid0), np ∈ ghostlspmxf(tid2), lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx, ∀ tid0. ¬ np ∈ ghostlspmxf(tid0) ⊦ lspmx[np] = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];gspmx[np])

Rule argument

Additional information

Proof step 51 from proof step-L2-L3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 52:

  U(alltids, ghostlspmxf(tid; lspmx))[np] = ghostlspmxf(tid0)[np], ghostlspmxf(tid) = ∅, lspmx ≠ ∅, tid ≠ tid1, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; lspmx)), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid3), np ∈ ghostlspmxf(tid2), np ∈ ghostlspmxf(tid0), np ∈ U(alltids, ghostlspmxf) ∪ lspmx, np ∈ ghostlspmxf(tid1), lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx ⊦ ghostlspmxf(tid0)[np] = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];gspmx[np])

Rule argument

Additional information

Proof step 52 from proof step-L2-L3 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 53:

  U(alltids, ghostlspmxf(tid; lspmx))[np] = ghostlspmxf(tid0)[np], ghostlspmxf(tid) = ∅, ghostlspmxf(tid0)[np] ≠ gspmx[np], lspmx ≠ ∅, tid ≠ tid1, alldisjointp(alltids, ghostlspmxf(tid; lspmx)), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid1), np ∈ U(alltids, ghostlspmxf) ∪ lspmx, np ∈ ghostlspmxf(tid0), np ∈ ghostlspmxf(tid2), np ∈ ghostlspmxf(tid3), lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx, ∀ tid0. ¬ np ∈ ghostlspmxf(tid0) ⊦

Rule argument

Additional information

Proof step 53 from proof step-L2-L3 (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: tid3

Proof step 54 from proof step-L2-L3 (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: tid2

Proof step 55 from proof step-L2-L3 (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: tid0

Proof step 56 from proof step-L2-L3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 57:

  ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf(tid; lspmx)), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid0), lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx, ¬ np ∈ lspmx, U(alltids, ghostlspmxf(tid; lspmx))[np] = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];∅[np]) ⊦ ∃ tid1. np ∈ ghostlspmxf(tid1), ∃ tid0. np ∈ (tid = tid0 ⊃ lspmx;ghostlspmxf(tid0)), (gspmx \ dom lspmx)[np] = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid0)[np];gspmx[np])

Rule argument

Additional information

Used simplifier rules: alltids-all: ⊦ tid ∈ alltids; ⊦ alldisjointp(ts, f) → (np ∈ U(ts, f) ↔ (∃ tid. tid ∈ ts ∧ np ∈ f(tid))); (s) ⊦ np ∈ spmx1 ∪ spmx2 ↔ np ∈ spmx1 ∨ np ∈ spmx2; (ws) ⊦ ¬ a ∈ st → st[a] = ∅[a]; (s)

Proof step 57 from proof step-L2-L3 (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: tid0

Proof step 58 from proof step-L2-L3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 59:

  U(alltids, ghostlspmxf(tid; lspmx))[np] = lspmx[np], ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; lspmx)), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx, (∃ tid0. np ∈ (tid = tid0 ⊃ lspmx;ghostlspmxf(tid0))) ↔ np ∈ U(alltids, ghostlspmxf) ∪ lspmx ⊦ ∃ tid0. np ∈ ghostlspmxf(tid0), (np ∈ (U(alltids, ghostlspmxf) ∪ lspmx) ∪ (gspmx \ dom lspmx) ↔ np ∈ U(alltids, ghostlspmxf) ∪ gspmx) ∧ (np ∈ U(alltids, ghostlspmxf) ∪ lspmx ⊃ lspmx[np];(gspmx \ dom lspmx)[np]) = gspmx[np]

Rule argument

Additional information

Used simplifier rules: alltids-all: ⊦ tid ∈ alltids; ⊦ alldisjointp(ts, f) → (np ∈ U(ts, f) ↔ (∃ tid. tid ∈ ts ∧ np ∈ f(tid))); (s)

Proof step 59 from proof step-L2-L3 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 60:

  ⊦ np ∈ spmx1 ∪ spmx2 ↔ np ∈ spmx1 ∨ np ∈ spmx2

• Proof step 61:

  U(alltids, ghostlspmxf(tid; lspmx))[np] = lspmx[np], ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf(tid; lspmx)), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx, (∃ tid0. np ∈ (tid = tid0 ⊃ lspmx;ghostlspmxf(tid0))) ↔ np ∈ U(alltids, ghostlspmxf) ∨ np ∈ lspmx ⊦ ∃ tid0. np ∈ ghostlspmxf(tid0), (np ∈ (U(alltids, ghostlspmxf) ∪ lspmx) ∪ (gspmx \ dom lspmx) ↔ np ∈ U(alltids, ghostlspmxf) ∪ gspmx) ∧ (np ∈ U(alltids, ghostlspmxf) ∨ np ∈ lspmx ⊃ lspmx[np];(gspmx \ dom lspmx)[np]) = gspmx[np]

Rule argument

Additional information

Used terms: np, U(alltids, ghostlspmxf), lspmx

Proof step 60 from proof step-L2-L3 (previous step) (back to tree)

A spec-lemma

Proof step 61 from proof step-L2-L3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 62:

  U(alltids, ghostlspmxf(tid; lspmx))[np] = lspmx[np], ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; lspmx)), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx, (∃ tid0. np ∈ (tid = tid0 ⊃ lspmx;ghostlspmxf(tid0))) ↔ np ∈ lspmx ⊦ ∃ tid0. np ∈ ghostlspmxf(tid0), (np ∈ (U(alltids, ghostlspmxf) ∪ lspmx) ∪ (gspmx \ dom lspmx) ↔ np ∈ U(alltids, ghostlspmxf) ∪ gspmx) ∧ (np ∈ lspmx ⊃ lspmx[np];(gspmx \ dom lspmx)[np]) = gspmx[np]

Rule argument

Additional information

Used simplifier rules: alltids-all: ⊦ tid ∈ alltids; ⊦ alldisjointp(ts, f) → (np ∈ U(ts, f) ↔ (∃ tid. tid ∈ ts ∧ np ∈ f(tid))); (s)

Proof step 62 from proof step-L2-L3 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 63:

  ⊦ np ∈ spmx1 ∪ spmx2 ↔ np ∈ spmx1 ∨ np ∈ spmx2

• Proof step 64:

  U(alltids, ghostlspmxf(tid; lspmx))[np] = lspmx[np], ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf(tid; lspmx)), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx, (∃ tid0. np ∈ (tid = tid0 ⊃ lspmx;ghostlspmxf(tid0))) ↔ np ∈ lspmx ⊦ ∃ tid0. np ∈ ghostlspmxf(tid0), (np ∈ U(alltids, ghostlspmxf) ∪ lspmx ∨ np ∈ gspmx \ dom lspmx ↔ np ∈ U(alltids, ghostlspmxf) ∪ gspmx) ∧ (np ∈ lspmx ⊃ lspmx[np];(gspmx \ dom lspmx)[np]) = gspmx[np]

Rule argument

Additional information

Used terms: np, U(alltids, ghostlspmxf) ∪ lspmx, gspmx \ dom lspmx

Proof step 63 from proof step-L2-L3 (previous step) (back to tree)

A spec-lemma

Proof step 64 from proof step-L2-L3 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 65:

  ⊦ np ∈ spmx1 ∪ spmx2 ↔ np ∈ spmx1 ∨ np ∈ spmx2

• Proof step 66:

  U(alltids, ghostlspmxf(tid; lspmx))[np] = lspmx[np], ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; lspmx)), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx, (∃ tid0. np ∈ (tid = tid0 ⊃ lspmx;ghostlspmxf(tid0))) ↔ np ∈ lspmx ⊦ ∃ tid0. np ∈ ghostlspmxf(tid0), ((np ∈ U(alltids, ghostlspmxf) ∨ np ∈ lspmx) ∨ np ∈ gspmx \ dom lspmx ↔ np ∈ U(alltids, ghostlspmxf) ∪ gspmx) ∧ (np ∈ lspmx ⊃ lspmx[np];(gspmx \ dom lspmx)[np]) = gspmx[np]

Rule argument

Additional information

Used terms: np, U(alltids, ghostlspmxf), lspmx

Proof step 65 from proof step-L2-L3 (previous step) (back to tree)

A spec-lemma

Proof step 66 from proof step-L2-L3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 67:

  U(alltids, ghostlspmxf(tid; lspmx))[np] = lspmx[np], ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf(tid; lspmx)), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx, (∃ tid0. np ∈ (tid = tid0 ⊃ lspmx;ghostlspmxf(tid0))) ↔ np ∈ lspmx ⊦ ∃ tid0. np ∈ ghostlspmxf(tid0), (np ∈ ghostlspmxf(tid0) ∨ np ∈ lspmx ∨ np ∈ gspmx \ dom lspmx → np ∈ U(alltids, ghostlspmxf) ∪ gspmx) ∧ (np ∈ lspmx ⊃ lspmx[np];(gspmx \ dom lspmx)[np]) = gspmx[np]

Rule argument

Additional information

Used simplifier rules: alltids-all: ⊦ tid ∈ alltids; ⊦ a ∈ dom st ↔ a ∈ st; (s) ⊦ a ∈ st \ s ↔ a ∈ st ∧ ¬ a ∈ s; (ws) ⊦ alldisjointp(ts, f) → (np ∈ U(ts, f) ↔ (∃ tid. tid ∈ ts ∧ np ∈ f(tid))); (s) ⊦ np ∈ spmx1 ∪ spmx2 ↔ np ∈ spmx1 ∨ np ∈ spmx2; (ws)

Proof step 67 from proof step-L2-L3 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 68:

  ⊦ a ∈ st \ s ↔ a ∈ st ∧ ¬ a ∈ s

• Proof step 69:

  U(alltids, ghostlspmxf(tid; lspmx))[np] = lspmx[np], ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; lspmx)), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx, (∃ tid0. np ∈ (tid = tid0 ⊃ lspmx;ghostlspmxf(tid0))) ↔ np ∈ lspmx ⊦ ∃ tid0. np ∈ ghostlspmxf(tid0), (np ∈ ghostlspmxf(tid0) ∨ np ∈ lspmx ∨ np ∈ gspmx ∧ ¬ np ∈ dom lspmx → np ∈ U(alltids, ghostlspmxf) ∪ gspmx) ∧ (np ∈ lspmx ⊃ lspmx[np];(gspmx \ dom lspmx)[np]) = gspmx[np]

Rule argument

Additional information

Used terms: np, gspmx, dom lspmx

Proof step 68 from proof step-L2-L3 (previous step) (back to tree)

A spec-lemma

Proof step 69 from proof step-L2-L3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 70:

  U(alltids, ghostlspmxf(tid; lspmx))[np] = lspmx[np], ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf(tid; lspmx)), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx, (∃ tid0. np ∈ (tid = tid0 ⊃ lspmx;ghostlspmxf(tid0))) ↔ np ∈ lspmx ⊦ ∃ tid0. np ∈ ghostlspmxf(tid0), (np ∈ ghostlspmxf(tid0) ∨ np ∈ lspmx ∨ np ∈ gspmx → np ∈ U(alltids, ghostlspmxf) ∪ gspmx) ∧ (np ∈ lspmx ⊃ lspmx[np];(gspmx \ dom lspmx)[np]) = gspmx[np]

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ dom st ↔ a ∈ st; (s)

Proof step 70 from proof step-L2-L3 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 71:

  ⊦ np ∈ spmx1 ∪ spmx2 ↔ np ∈ spmx1 ∨ np ∈ spmx2

• Proof step 72:

  U(alltids, ghostlspmxf(tid; lspmx))[np] = lspmx[np], ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; lspmx)), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx, (∃ tid0. np ∈ (tid = tid0 ⊃ lspmx;ghostlspmxf(tid0))) ↔ np ∈ lspmx ⊦ ∃ tid0. np ∈ ghostlspmxf(tid0), (np ∈ ghostlspmxf(tid0) ∨ np ∈ lspmx ∨ np ∈ gspmx → np ∈ U(alltids, ghostlspmxf) ∨ np ∈ gspmx) ∧ (np ∈ lspmx ⊃ lspmx[np];(gspmx \ dom lspmx)[np]) = gspmx[np]

Rule argument

Additional information

Used terms: np, U(alltids, ghostlspmxf), gspmx

Proof step 71 from proof step-L2-L3 (previous step) (back to tree)

A spec-lemma

Proof step 72 from proof step-L2-L3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 73:

  U(alltids, ghostlspmxf(tid; lspmx))[np] = lspmx[np], ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf(tid; lspmx)), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx, (∃ tid0. np ∈ (tid = tid0 ⊃ lspmx;ghostlspmxf(tid0))) ↔ np ∈ lspmx ⊦ ∃ tid0. np ∈ ghostlspmxf(tid0), (np ∈ ghostlspmxf(tid0) ∨ np ∈ lspmx → (∃ tid1. np ∈ ghostlspmxf(tid1)) ∨ np ∈ gspmx) ∧ (np ∈ lspmx ⊃ lspmx[np];(gspmx \ dom lspmx)[np]) = gspmx[np]

Rule argument

Additional information

Used simplifier rules: alltids-all: ⊦ tid ∈ alltids; ⊦ alldisjointp(ts, f) → (np ∈ U(ts, f) ↔ (∃ tid. tid ∈ ts ∧ np ∈ f(tid))); (s)

Proof step 73 from proof step-L2-L3 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 74:

  ⊦ st1 ⊆ st2 ↔ (∀ a. a ∈ st1 → a ∈ st2 ∧ st1[a] = st2[a])

• Proof step 75:

  U(alltids, ghostlspmxf(tid; lspmx))[np] = lspmx[np], ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; lspmx)), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, (∃ tid0. np ∈ (tid = tid0 ⊃ lspmx;ghostlspmxf(tid0))) ↔ np ∈ lspmx, ∀ np. np ∈ lspmx → np ∈ gspmx ∧ lspmx[np] = gspmx[np] ⊦ ∃ tid0. np ∈ ghostlspmxf(tid0), (np ∈ ghostlspmxf(tid0) ∨ np ∈ lspmx → (∃ tid1. np ∈ ghostlspmxf(tid1)) ∨ np ∈ gspmx) ∧ (np ∈ lspmx ⊃ lspmx[np];(gspmx \ dom lspmx)[np]) = gspmx[np]

Rule argument

Additional information

Used terms: lspmx, gspmx

Proof step 74 from proof step-L2-L3 (previous step) (back to tree)

A spec-lemma

Proof step 75 from proof step-L2-L3 (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 76:

  U(alltids, ghostlspmxf(tid; lspmx))[np] = lspmx[np], ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf(tid; lspmx)), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx, np ∈ lspmx → np ∈ gspmx ∧ lspmx[np] = gspmx[np], (∃ tid0. np ∈ (tid = tid0 ⊃ lspmx;ghostlspmxf(tid0))) ↔ np ∈ lspmx, ∀ np. np ∈ lspmx → np ∈ gspmx ∧ lspmx[np] = gspmx[np] ⊦ ∃ tid0. np ∈ ghostlspmxf(tid0), (np ∈ ghostlspmxf(tid0) ∨ np ∈ lspmx → (∃ tid1. np ∈ ghostlspmxf(tid1)) ∨ np ∈ gspmx) ∧ (np ∈ lspmx ⊃ lspmx[np];(gspmx \ dom lspmx)[np]) = gspmx[np]

Rule argument

Additional information

Used terms: np

Proof step 76 from proof step-L2-L3 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 77:

  U(alltids, ghostlspmxf(tid; lspmx))[np] = lspmx[np], ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; lspmx)), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, ¬ np ∈ lspmx, np ∈ lspmx → np ∈ gspmx ∧ lspmx[np] = gspmx[np], (∃ tid0. np ∈ (tid = tid0 ⊃ lspmx;ghostlspmxf(tid0))) ↔ np ∈ lspmx, ∀ np. np ∈ lspmx → np ∈ gspmx ∧ lspmx[np] = gspmx[np] ⊦ ∃ tid0. np ∈ ghostlspmxf(tid0), (np ∈ ghostlspmxf(tid0) ∨ np ∈ lspmx → (∃ tid1. np ∈ ghostlspmxf(tid1)) ∨ np ∈ gspmx) ∧ (np ∈ lspmx ⊃ lspmx[np];(gspmx \ dom lspmx)[np]) = gspmx[np]

Rule argument

Additional information

Used formulas: np ∈ lspmx

Proof step 77 from proof step-L2-L3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 78:

  U(alltids, ghostlspmxf(tid; lspmx))[np] = ∅[np], ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf(tid; lspmx)), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx, ¬ np ∈ lspmx, ∀ np. np ∈ lspmx → np ∈ gspmx ∧ lspmx[np] = gspmx[np] ⊦ ∃ tid0. np ∈ ghostlspmxf(tid0), ∃ tid0. np ∈ (tid = tid0 ⊃ lspmx;ghostlspmxf(tid0)), (np ∈ ghostlspmxf(tid0) → (∃ tid1. np ∈ ghostlspmxf(tid1)) ∨ np ∈ gspmx) ∧ (gspmx \ dom lspmx)[np] = gspmx[np]

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a ∈ st → st[a] = ∅[a]; (s)

Proof step 78 from proof step-L2-L3 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 79:

  ⊦ ¬ a ∈ s → (st \ s)[a] = st[a]

• Proof step 80:

  U(alltids, ghostlspmxf(tid; lspmx))[np] = ∅[np], ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; lspmx)), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, ¬ np ∈ dom lspmx, ¬ np ∈ lspmx, ∀ np. np ∈ lspmx → np ∈ gspmx ∧ lspmx[np] = gspmx[np] ⊦ ∃ tid0. np ∈ (tid = tid0 ⊃ lspmx;ghostlspmxf(tid0)), ∃ tid0. np ∈ ghostlspmxf(tid0), (np ∈ ghostlspmxf(tid0) → (∃ tid1. np ∈ ghostlspmxf(tid1)) ∨ np ∈ gspmx) ∧ gspmx[np] = gspmx[np]

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ dom st ↔ a ∈ st; (s) Used terms: gspmx, dom lspmx, np

Proof step 79 from proof step-L2-L3 (previous step) (back to tree)

A spec-lemma

Proof step 80 from proof step-L2-L3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 81:

  U(alltids, ghostlspmxf(tid; lspmx))[np] = ∅[np], ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf(tid; lspmx)), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid0), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx, ¬ np ∈ lspmx, ¬ np ∈ gspmx, ∀ np. np ∈ lspmx → np ∈ gspmx ∧ lspmx[np] = gspmx[np] ⊦ ∃ tid0. np ∈ ghostlspmxf(tid0), ∃ tid0. np ∈ (tid = tid0 ⊃ lspmx;ghostlspmxf(tid0)), ∃ tid1. np ∈ ghostlspmxf(tid1)

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ dom st ↔ a ∈ st; (s)

Proof step 81 from proof step-L2-L3 (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: tid0

Proof step 82 from proof step-L2-L3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 83:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid) = ∅, U(alltids, ghostlspmxf(tid; lspmx)) ≠ U(alltids, ghostlspmxf) ∪ lspmx, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf(tid; lspmx)), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx ⊦ disjointp(U(alltids, ghostlspmxf(tid; lspmx)), gspmx \ dom lspmx) ∧ y + (U(alltids, ghostlspmxf(tid; lspmx)) ∪ (gspmx \ dom lspmx)).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x ∧ U(alltids, ghostlspmxf(tid; lspmx)) ∪ (gspmx \ dom lspmx) ⊆ spmx

Rule argument

Additional information

Proof step 83 from proof step-L2-L3 (previous step) (back to tree)

User applied rule weakening

And obtained the following new goals

• Proof step 84:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid) = ∅, U(alltids, ghostlspmxf(tid; lspmx)) ≠ U(alltids, ghostlspmxf) ∪ lspmx, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; lspmx)), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx ⊦

Rule argument

Additional information

Proof step 84 from proof step-L2-L3 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 85:

  ⊦ st1 = st2 ↔ (∀ a. (a ∈ st1 ↔ a ∈ st2) ∧ st1[a] = st2[a])

• Proof step 86:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf(tid; lspmx)), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx, ∃ np. ¬ ( (np ∈ U(alltids, ghostlspmxf(tid; lspmx)) ↔ np ∈ U(alltids, ghostlspmxf) ∪ lspmx) ∧ U(alltids, ghostlspmxf(tid; lspmx))[np] = (U(alltids, ghostlspmxf) ∪ lspmx)[np]) ⊦

Rule argument

Additional information

Used terms: U(alltids, ghostlspmxf(tid; lspmx)), U(alltids, ghostlspmxf) ∪ lspmx

Proof step 85 from proof step-L2-L3 (previous step) (back to tree)

A spec-lemma

Proof step 86 from proof step-L2-L3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 87:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; lspmx)), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx ⊦ ((∃ tid0. np ∈ (tid = tid0 ⊃ lspmx;ghostlspmxf(tid0))) ↔ np ∈ U(alltids, ghostlspmxf) ∪ lspmx) ∧ U(alltids, ghostlspmxf(tid; lspmx))[np] = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ U(alltids, ghostlspmxf)[np];lspmx[np])

Rule argument

Additional information

Used simplifier rules: alltids-all: ⊦ tid ∈ alltids; ⊦ alldisjointp(ts, f) → (np ∈ U(ts, f) ↔ (∃ tid. tid ∈ ts ∧ np ∈ f(tid))); (s) ⊦ (spmx1 ∪ spmx2)[np] = (np ∈ spmx1 ⊃ spmx1[np];spmx2[np]); (s)

Proof step 87 from proof step-L2-L3 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 88:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf(tid; lspmx)), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx ⊦ (∃ tid0. np ∈ (tid = tid0 ⊃ lspmx;ghostlspmxf(tid0))) ↔ np ∈ U(alltids, ghostlspmxf) ∪ lspmx

• Proof step 99:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf(tid; lspmx)), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx ⊦ U(alltids, ghostlspmxf(tid; lspmx))[np] = (∃ tid0. np ∈ ghostlspmxf(tid0) ⊃ U(alltids, ghostlspmxf)[np];lspmx[np])

Rule argument

Additional information

Proof step 88 from proof step-L2-L3 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 89:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; lspmx)), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx, ¬ np ∈ U(alltids, ghostlspmxf) ∪ lspmx, ∃ tid0. np ∈ (tid = tid0 ⊃ lspmx;ghostlspmxf(tid0)) ⊦

• Proof step 92:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; lspmx)), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ U(alltids, ghostlspmxf) ∪ lspmx, lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx ⊦ ∃ tid0. np ∈ (tid = tid0 ⊃ lspmx;ghostlspmxf(tid0))

Rule argument

Additional information

Proof step 89 from proof step-L2-L3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 90:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf(tid; lspmx)), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ (tid = tid0 ⊃ lspmx;ghostlspmxf(tid0)), lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx, ¬ np ∈ lspmx ⊦ ∃ tid1. np ∈ ghostlspmxf(tid1)

Rule argument

Additional information

Used simplifier rules: alltids-all: ⊦ tid ∈ alltids; ⊦ alldisjointp(ts, f) → (np ∈ U(ts, f) ↔ (∃ tid. tid ∈ ts ∧ np ∈ f(tid))); (s) ⊦ np ∈ spmx1 ∪ spmx2 ↔ np ∈ spmx1 ∨ np ∈ spmx2; (ws)

Proof step 90 from proof step-L2-L3 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 91:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid) = ∅, lspmx ≠ ∅, tid ≠ tid0, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; lspmx)), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid0), lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx, ¬ np ∈ lspmx ⊦ ∃ tid1. np ∈ ghostlspmxf(tid1)

Rule argument

Additional information

Proof step 91 from proof step-L2-L3 (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: tid0

Proof step 92 from proof step-L2-L3 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 93:

  ⊦ np ∈ spmx1 ∪ spmx2 ↔ np ∈ spmx1 ∨ np ∈ spmx2

• Proof step 94:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf(tid; lspmx)), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx, np ∈ U(alltids, ghostlspmxf) ∨ np ∈ lspmx ⊦ ∃ tid0. np ∈ (tid = tid0 ⊃ lspmx;ghostlspmxf(tid0))

Rule argument

Additional information

Used terms: np, U(alltids, ghostlspmxf), lspmx

Proof step 93 from proof step-L2-L3 (previous step) (back to tree)

A spec-lemma

Proof step 94 from proof step-L2-L3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 95:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; lspmx)), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx, np ∈ ghostlspmxf(tid0) ∨ np ∈ lspmx ⊦ ∃ tid0. np ∈ (tid = tid0 ⊃ lspmx;ghostlspmxf(tid0))

Rule argument

Additional information

Used simplifier rules: alltids-all: ⊦ tid ∈ alltids; ⊦ alldisjointp(ts, f) → (np ∈ U(ts, f) ↔ (∃ tid. tid ∈ ts ∧ np ∈ f(tid))); (s)

Proof step 95 from proof step-L2-L3 (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 96:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf(tid; lspmx)), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx, ¬ np ∈ (tid = tid0 ⊃ lspmx;ghostlspmxf(tid0)), np ∈ ghostlspmxf(tid0) ∨ np ∈ lspmx ⊦ ∃ tid0. np ∈ (tid = tid0 ⊃ lspmx;ghostlspmxf(tid0))

Rule argument

Additional information

Used terms: tid0

Proof step 96 from proof step-L2-L3 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 97:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid) = ∅, lspmx ≠ ∅, tid ≠ tid0, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; lspmx)), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx, ¬ np ∈ ghostlspmxf(tid0), np ∈ ghostlspmxf(tid0) ∨ np ∈ lspmx ⊦ ∃ tid0. np ∈ (tid = tid0 ⊃ lspmx;ghostlspmxf(tid0))

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a ∈ ∅; (s)

Proof step 97 from proof step-L2-L3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 98:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid) = ∅, lspmx ≠ ∅, tid ≠ tid0, alldisjointp(alltids, ghostlspmxf(tid; lspmx)), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ lspmx, lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx, ¬ np ∈ ghostlspmxf(tid0) ⊦ ∃ tid0. np ∈ (tid = tid0 ⊃ lspmx;ghostlspmxf(tid0))

Rule argument

Additional information

Proof step 98 from proof step-L2-L3 (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: tid

Proof step 99 from proof step-L2-L3 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 100:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid) = ∅, U(alltids, ghostlspmxf(tid; lspmx))[np] ≠ U(alltids, ghostlspmxf)[np], lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; lspmx)), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx, ∃ tid0. np ∈ ghostlspmxf(tid0) ⊦

• Proof step 107:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid) = ∅, U(alltids, ghostlspmxf(tid; lspmx))[np] ≠ lspmx[np], lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; lspmx)), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx, ∀ tid0. ¬ np ∈ ghostlspmxf(tid0) ⊦

Rule argument

Additional information

Proof step 100 from proof step-L2-L3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 101:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid) = ∅, U(alltids, ghostlspmxf(tid; lspmx))[np] ≠ ghostlspmxf(tid0)[np], lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf(tid; lspmx)), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid0), lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ alldisjointp(ts, f) ∧ np ∈ f(tid) → U(ts, f)[np] = f(tid)[np]; (s)

Proof step 101 from proof step-L2-L3 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 102:

  ⊦ alldisjointp(ts, f) ∧ np ∈ f(tid) → U(ts, f)[np] = f(tid)[np]

• Proof step 103:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid) = ∅, U(alltids, ghostlspmxf(tid; lspmx))[np] ≠ ghostlspmxf(tid0)[np], lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; lspmx)), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid0), lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx ⊦ alldisjointp(alltids, ghostlspmxf(tid; lspmx)) ∧ np ∈ ghostlspmxf(tid; lspmx)(tid0)

• Proof step 105:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid) = ∅, ghostlspmxf(tid; lspmx)(tid0)[np] ≠ ghostlspmxf(tid0)[np], lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; lspmx)), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid0), np ∈ ghostlspmxf(tid; lspmx)(tid0), lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx ⊦

Rule argument

Additional information

Used terms: alltids, ghostlspmxf(tid; lspmx), np, tid0

Proof step 102 from proof step-L2-L3 (previous step) (back to tree)

A spec-lemma

Proof step 103 from proof step-L2-L3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 104:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid) = ∅, U(alltids, ghostlspmxf(tid; lspmx))[np] ≠ ghostlspmxf(tid0)[np], lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf(tid; lspmx)), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid0), lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx, ¬ np ∈ (tid = tid0 ⊃ lspmx;ghostlspmxf(tid0)) ⊦

Rule argument

Additional information

Proof step 104 from proof step-L2-L3 (previous step) (back to tree)

User applied rule case distinction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a ∈ ∅; (s)

Proof step 105 from proof step-L2-L3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 106:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid) = ∅, (tid = tid0 ⊃ lspmx;ghostlspmxf(tid0))[np] ≠ ghostlspmxf(tid0)[np], lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf(tid; lspmx)), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid0), np ∈ (tid = tid0 ⊃ lspmx;ghostlspmxf(tid0)), lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx ⊦

Rule argument

Additional information

Proof step 106 from proof step-L2-L3 (previous step) (back to tree)

User applied rule case distinction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a ∈ ∅; (s)

Proof step 107 from proof step-L2-L3 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 108:

  ⊦ alldisjointp(ts, f) ∧ np ∈ f(tid) → U(ts, f)[np] = f(tid)[np]

• Proof step 109:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid) = ∅, U(alltids, ghostlspmxf(tid; lspmx))[np] ≠ lspmx[np], lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf(tid; lspmx)), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx, ∀ tid0. ¬ np ∈ ghostlspmxf(tid0) ⊦ alldisjointp(alltids, ghostlspmxf(tid; lspmx)) ∧ np ∈ ghostlspmxf(tid; lspmx)(tid)

Rule argument

Additional information

Used terms: tid, alltids, ghostlspmxf(tid; lspmx), np

Proof step 108 from proof step-L2-L3 (previous step) (back to tree)

A spec-lemma

Proof step 109 from proof step-L2-L3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 110:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid) = ∅, U(alltids, ghostlspmxf(tid; lspmx))[np] ≠ ∅[np], lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; lspmx)), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx, ¬ np ∈ lspmx, ∀ tid0. ¬ np ∈ ghostlspmxf(tid0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a ∈ st → st[a] = ∅[a]; (s)

Proof step 110 from proof step-L2-L3 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 111:

  ⊦ ¬ a ∈ st → st[a] = ∅[a]

• Proof step 112:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid) = ∅, U(alltids, ghostlspmxf(tid; lspmx))[np] ≠ ∅[np], lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf(tid; lspmx)), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ U(alltids, ghostlspmxf(tid; lspmx)), lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx, ¬ np ∈ lspmx, ∀ tid0. ¬ np ∈ ghostlspmxf(tid0) ⊦

Rule argument

Additional information

Used terms: U(alltids, ghostlspmxf(tid; lspmx)), np

Proof step 111 from proof step-L2-L3 (previous step) (back to tree)

A spec-lemma

Proof step 112 from proof step-L2-L3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 113:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid) = ∅, U(alltids, ghostlspmxf(tid; lspmx))[np] ≠ ∅[np], lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; lspmx)), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ (tid = tid0 ⊃ lspmx;ghostlspmxf(tid0)), lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx, ¬ np ∈ lspmx, ∀ tid0. ¬ np ∈ ghostlspmxf(tid0) ⊦

Rule argument

Additional information

Used simplifier rules: alltids-all: ⊦ tid ∈ alltids; ⊦ alldisjointp(ts, f) → (np ∈ U(ts, f) ↔ (∃ tid. tid ∈ ts ∧ np ∈ f(tid))); (s)

Proof step 113 from proof step-L2-L3 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 114:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid) = ∅, U(alltids, ghostlspmxf(tid; lspmx))[np] ≠ ∅[np], lspmx ≠ ∅, tid ≠ tid0, alldisjointp(alltids, ghostlspmxf(tid; lspmx)), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid0), lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx, ¬ np ∈ lspmx, ∀ tid0. ¬ np ∈ ghostlspmxf(tid0) ⊦

Rule argument

Additional information

Proof step 114 from proof step-L2-L3 (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: tid0

Proof step 115 from proof step-L2-L3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 116:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx, ¬ alldisjointp(alltids, ghostlspmxf(tid; lspmx)) ⊦

Rule argument

Additional information

Proof step 116 from proof step-L2-L3 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 117:

  ⊦ alldisjointp(ts, f) → ( alldisjointp(ts, f0) ↔ (∀ tid1, tid2, np. (tid1 ∈ ts ∧ tid2 ∈ ts ∧ tid1 ≠ tid2 ∧ np ∈ f(tid1) → ¬ np ∈ f(tid2)) → tid1 ∈ ts ∧ tid2 ∈ ts ∧ tid1 ≠ tid2 ∧ np ∈ f0(tid1) → ¬ np ∈ f0(tid2)))

• Proof step 118:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid) = ∅, lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx, ∃ tid1, tid2, np. ¬ ( (tid1 ∈ alltids ∧ tid2 ∈ alltids ∧ tid1 ≠ tid2 ∧ np ∈ ghostlspmxf(tid1) → ¬ np ∈ ghostlspmxf(tid2)) → tid1 ∈ alltids ∧ tid2 ∈ alltids ∧ tid1 ≠ tid2 ∧ np ∈ ghostlspmxf(tid; lspmx)(tid1) → ¬ np ∈ ghostlspmxf(tid; lspmx)(tid2)) ⊦

Rule argument

Additional information

Used terms: ghostlspmxf, alltids, ghostlspmxf(tid; lspmx)

Proof step 117 from proof step-L2-L3 (previous step) (back to tree)

A spec-lemma

Proof step 118 from proof step-L2-L3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 119:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid) = ∅, lspmx ≠ ∅, tid1 ≠ tid2, alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ (tid = tid2 ⊃ lspmx;ghostlspmxf(tid2)), np ∈ (tid = tid1 ⊃ lspmx;ghostlspmxf(tid1)), lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx, np ∈ ghostlspmxf(tid1) → ¬ np ∈ ghostlspmxf(tid2) ⊦

Rule argument

Additional information

Used simplifier rules: alltids-all: ⊦ tid ∈ alltids;

Proof step 119 from proof step-L2-L3 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 120:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid) = ∅, tid = tid2, lspmx ≠ ∅, tid1 ≠ tid2, alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ (tid = tid1 ⊃ lspmx;ghostlspmxf(tid1)), np ∈ lspmx, lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx, np ∈ ghostlspmxf(tid1) → ¬ np ∈ ghostlspmxf(tid2) ⊦

• Proof step 126:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid) = ∅, lspmx ≠ ∅, tid ≠ tid2, tid1 ≠ tid2, alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ (tid = tid1 ⊃ lspmx;ghostlspmxf(tid1)), np ∈ ghostlspmxf(tid2), lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx, np ∈ ghostlspmxf(tid1) → ¬ np ∈ ghostlspmxf(tid2) ⊦

Rule argument

Additional information

Proof step 120 from proof step-L2-L3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 121:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid2) = ∅, lspmx ≠ ∅, tid1 ≠ tid2, alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid1), np ∈ lspmx, lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a ∈ ∅; (s)

Proof step 121 from proof step-L2-L3 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 122:

  ⊦ disjointp(sa1, sa2) ↔ (∀ np. np ∈ sa1 → ¬ np ∈ sa2)

• Proof step 123:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid2) = ∅, lspmx ≠ ∅, tid1 ≠ tid2, alldisjointp(alltids, ghostlspmxf), okspmx(spmx, # y, # x), np ∈ lspmx, np ∈ ghostlspmxf(tid1), lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx, ∀ np. np ∈ U(alltids, ghostlspmxf) → ¬ np ∈ gspmx ⊦

Rule argument

Additional information

Used terms: U(alltids, ghostlspmxf), gspmx

Proof step 122 from proof step-L2-L3 (previous step) (back to tree)

A spec-lemma

Proof step 123 from proof step-L2-L3 (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 124:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid2) = ∅, lspmx ≠ ∅, tid1 ≠ tid2, alldisjointp(alltids, ghostlspmxf), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid1), np ∈ lspmx, lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx, np ∈ U(alltids, ghostlspmxf) → ¬ np ∈ gspmx ⊦

Rule argument

Additional information

Used terms: np

Proof step 124 from proof step-L2-L3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 125:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid2) = ∅, lspmx ≠ ∅, tid1 ≠ tid2, alldisjointp(alltids, ghostlspmxf), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid1), np ∈ lspmx, np ∈ gspmx, lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx ⊦ ∃ tid. np ∈ ghostlspmxf(tid)

Rule argument

Additional information

Used simplifier rules: alltids-all: ⊦ tid ∈ alltids; ⊦ b ∈ st ∧ ¬ b ∈ st0 → ¬ st ⊆ st0; (s) ⊦ alldisjointp(ts, f) → (np ∈ U(ts, f) ↔ (∃ tid. tid ∈ ts ∧ np ∈ f(tid))); (s)

Proof step 125 from proof step-L2-L3 (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: tid1

Proof step 126 from proof step-L2-L3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 127:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid) = ∅, lspmx ≠ ∅, tid ≠ tid2, tid1 ≠ tid2, alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid2), np ∈ (tid = tid1 ⊃ lspmx;ghostlspmxf(tid1)), lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx, ¬ np ∈ ghostlspmxf(tid1) ⊦

Rule argument

Additional information

Proof step 127 from proof step-L2-L3 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 128:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid) = ∅, tid = tid1, lspmx ≠ ∅, tid ≠ tid2, tid1 ≠ tid2, alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid2), np ∈ lspmx, lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx, ¬ np ∈ ghostlspmxf(tid1) ⊦

Rule argument

Additional information

Proof step 128 from proof step-L2-L3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 129:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid1) = ∅, lspmx ≠ ∅, tid1 ≠ tid2, alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid2), np ∈ lspmx, lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a ∈ ∅; (s)

Proof step 129 from proof step-L2-L3 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 130:

  ⊦ disjointp(sa1, sa2) ↔ (∀ np. np ∈ sa1 → ¬ np ∈ sa2)

• Proof step 131:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid1) = ∅, lspmx ≠ ∅, tid1 ≠ tid2, alldisjointp(alltids, ghostlspmxf), okspmx(spmx, # y, # x), np ∈ lspmx, np ∈ ghostlspmxf(tid2), lspmx ⊆ gspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx ⊆ spmx, ∀ np. np ∈ U(alltids, ghostlspmxf) → ¬ np ∈ gspmx ⊦

Rule argument

Additional information

Used terms: U(alltids, ghostlspmxf), gspmx

Proof step 130 from proof step-L2-L3 (previous step) (back to tree)

A spec-lemma

Proof step 131 from proof step-L2-L3 (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 132:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid1) = ∅, lspmx ≠ ∅, tid1 ≠ tid2, alldisjointp(alltids, ghostlspmxf), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid2), np ∈ lspmx, lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx, np ∈ U(alltids, ghostlspmxf) → ¬ np ∈ gspmx ⊦

Rule argument

Additional information

Used terms: np

Proof step 132 from proof step-L2-L3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 133:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid1) = ∅, lspmx ≠ ∅, tid1 ≠ tid2, alldisjointp(alltids, ghostlspmxf), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid2), np ∈ lspmx, np ∈ gspmx, lspmx ⊆ spmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx ⊆ gspmx ⊦ ∃ tid. np ∈ ghostlspmxf(tid)

Rule argument

Additional information

Used simplifier rules: alltids-all: ⊦ tid ∈ alltids; ⊦ b ∈ st ∧ ¬ b ∈ st0 → ¬ st ⊆ st0; (s) ⊦ alldisjointp(ts, f) → (np ∈ U(ts, f) ↔ (∃ tid. tid ∈ ts ∧ np ∈ f(tid))); (s)

Proof step 133 from proof step-L2-L3 (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: tid2