Proof step 1 from proof step-L6-L7 (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) = ls.lspmx, pcstepf(gs, ls, L6, a) = L7, alldisjointp(alltids, gs.ghostlspmxf), disjointp(U(alltids, gs.ghostlspmxf), gs.gspmx), okspmx(gs.spmx, gs.r, # gs.x), pre(gs, ls, L6, a), ls.np ∈ ls.lspmx, U(alltids, gs.ghostlspmxf) ∪ gs.gspmx ⊆ gs.spmx ⊦ ( alldisjointp(alltids, gstepf(gs, ls, L6, a).ghostlspmxf) ∧ disjointp(U(alltids, gstepf(gs, ls, L6, a).ghostlspmxf), gstepf(gs, ls, L6, a).gspmx) ∧ gstepf(gs, ls, L6, a).y + (U(alltids, gstepf(gs, ls, L6, a).ghostlspmxf) ∪ gstepf(gs, ls, L6, a).gspmx ).toMatrix (gstepf(gs, ls, L6, a).r, # gstepf(gs, ls, L6, a).x ) * gstepf(gs, ls, L6, a).x = gstepf(gs, ls, L6, a).spmx.toMatrix(gstepf(gs, ls, L6, a).r, # gstepf(gs, ls, L6, a).x) * gstepf(gs, ls, L6, a).x ∧ U(alltids, gstepf(gs, ls, L6, a).ghostlspmxf) ∪ gstepf(gs, ls, L6, a).gspmx ⊆ gstepf(gs, ls, L6, a).spmx ∧ # gstepf(gs, ls, L6, a).y = gstepf(gs, ls, L6, a).r ∧ okspmx(gstepf(gs, ls, L6, a).spmx, gstepf(gs, ls, L6, a).r, # gstepf(gs, ls, L6, a).x)) ∧ lstepf(gs, ls, L6, a).np ∈ lstepf(gs, ls, L6, a).lspmx ∧ gstepf(gs, ls, L6, a).ghostlspmxf(lstepf(gs, ls, L6, a).tid) = lstepf(gs, ls, L6, a).lspmx -- lstepf(gs, ls, L6, a).np

Rule argument

Additional information

Proof step 2 from proof step-L6-L7 (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) = ls.lspmx, ls.val = gs.y[ls.np.r], alldisjointp(alltids, gs.ghostlspmxf), disjointp(U(alltids, gs.ghostlspmxf), gs.gspmx), okspmx(gs.spmx, gs.r, # gs.x), ls.np ∈ ls.lspmx, gs.gspmx ⊆ gs.spmx, U(alltids, gs.ghostlspmxf) ⊆ gs.spmx ⊦ alldisjointp(alltids, gs.ghostlspmxf(ls.tid; ls.lspmx -- ls.np)) ∧ disjointp(U(alltids, gs.ghostlspmxf(ls.tid; ls.lspmx -- ls.np)), gs.gspmx) ∧ gs.y[ls.np.r, ls.val + ls.lspmx[ls.np] * gs.x[ls.np.c]] + (U(alltids, gs.ghostlspmxf(ls.tid; ls.lspmx -- ls.np)) ∪ gs.gspmx).toMatrix(gs.r, # gs.x) * gs.x = gs.spmx.toMatrix(gs.r, # gs.x) * gs.x ∧ U(alltids, gs.ghostlspmxf(ls.tid; ls.lspmx -- ls.np)) ⊆ gs.spmx

Rule argument

Additional information

Used simplifier rules: pcstepf-L6: ⊦ pcstepf(gs, ls, L6, a) = (ls.val = gs.y[ls.np.r] ⊃ L7;L3); disj-16: ⊦ L3 ≠ L7; pre-L6: ⊦ pre(gs, ls, L6, a) ↔ a = τ; updsel-30: ⊦ (gs.ghostlspmxf:= ghostlspmxf).gspmx = gs.gspmx; updsel-29: ⊦ (gs.y:= x0).gspmx = gs.gspmx; updsel-48: ⊦ (gs.ghostlspmxf:= ghostlspmxf).y = gs.y; updsel-47: ⊦ (gs.y:= x0).y = x0; updsel-24: ⊦ (gs.ghostlspmxf:= ghostlspmxf).spmx = gs.spmx; updsel-23: ⊦ (gs.y:= x0).spmx = gs.spmx; updsel-36: ⊦ (gs.ghostlspmxf:= ghostlspmxf).r = gs.r; updsel-35: ⊦ (gs.y:= x0).r = gs.r; updsel-42: ⊦ (gs.ghostlspmxf:= ghostlspmxf).x = gs.x; updsel-41: ⊦ (gs.y:= x0).x = gs.x; gstepf-L6: ⊦ gstepf(gs, ls, L6, a) = (ls.val = gs.y[ls.np.r] ⊃ (gs.y:= gs.y[ls.np.r, ls.val + ls.lspmx[ls.np] * gs.x[ls.np.c]]) .ghostlspmxf:= gs.ghostlspmxf(ls.tid; gs.ghostlspmxf(ls.tid) -- ls.np) ;gs ); updsel-54: ⊦ (gs.ghostlspmxf:= ghostlspmxf).ghostlspmxf = ghostlspmxf; lstepf-L6: ⊦ lstepf(gs, ls, L6, a) = ls; ⊦ # ar[n, a] = # ar; (s) ⊦ disjointp(spmx1, spmx2) → (spmx1 ∪ spmx2 ⊆ spmx ↔ spmx1 ⊆ spmx ∧ spmx2 ⊆ spmx); (ws)

Proof step 3 from proof step-L6-L7 (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, ls.val = y[ls.np.r], ghostlspmxf(ls.tid) = ls.lspmx, gs = mkgs(spmx, gspmx, r, x, y, ghostlspmxf), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, r, # x), ls.np ∈ ls.lspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx ⊦ alldisjointp(alltids, ghostlspmxf(ls.tid; ls.lspmx -- ls.np)) ∧ disjointp(U(alltids, ghostlspmxf(ls.tid; ls.lspmx -- ls.np)), gspmx) ∧ y[ls.np.r, ls.val + ls.lspmx[ls.np] * x[ls.np.c]] + (U(alltids, ghostlspmxf(ls.tid; ls.lspmx -- ls.np)) ∪ gspmx).toMatrix(r, # x) * x = spmx.toMatrix(r, # x) * x ∧ U(alltids, ghostlspmxf(ls.tid; ls.lspmx -- ls.np)) ⊆ spmx

Rule argument

Additional information

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

Proof step 4 from proof step-L6-L7 (previous step) (back to tree)

Lemma elim-03

Proof step 5 from proof step-L6-L7 (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, ls.val = y[ls.np.r], ghostlspmxf(ls.tid) = ls.lspmx, alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), ls.np ∈ ls.lspmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx ⊦ alldisjointp(alltids, ghostlspmxf(ls.tid; ls.lspmx -- ls.np)) ∧ disjointp(U(alltids, ghostlspmxf(ls.tid; ls.lspmx -- ls.np)), gspmx) ∧ y[ls.np.r, ls.val + ls.lspmx[ls.np] * x[ls.np.c]] + (U(alltids, ghostlspmxf(ls.tid; ls.lspmx -- ls.np)) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x ∧ U(alltids, ghostlspmxf(ls.tid; ls.lspmx -- ls.np)) ⊆ spmx

Rule argument

Additional information

Proof step 6 from proof step-L6-L7 (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) = lspmx, ls = mkls(tid, lspmx, np, val), val = y[np.r], alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ lspmx, U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx ⊦ alldisjointp(alltids, ghostlspmxf(tid; lspmx -- np)) ∧ disjointp(U(alltids, ghostlspmxf(tid; lspmx -- np)), gspmx) ∧ y[np.r, val + lspmx[np] * x[np.c]] + (U(alltids, ghostlspmxf(tid; lspmx -- np)) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x ∧ U(alltids, ghostlspmxf(tid; lspmx -- np)) ⊆ spmx

Rule argument

Additional information

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

Proof step 7 from proof step-L6-L7 (previous step) (back to tree)

Lemma elim-02

Proof step 8 from proof step-L6-L7 (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, alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid), gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx ⊦ alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- np)) ∧ disjointp(U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- np)), gspmx) ∧ y[np.r, y[np.r] + ghostlspmxf(tid)[np] * x[np.c]] + (U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- np)) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x ∧ U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- np)) ⊆ spmx

Rule argument

Additional information

Proof step 9 from proof step-L6-L7 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 10:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, np = r × r0, alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx ⊦ alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- np)) ∧ disjointp(U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- np)), gspmx) ∧ y[r, y[r] + ghostlspmxf(tid)[np] * x[r0]] + (U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- np)) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x ∧ U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- np)) ⊆ spmx

Rule argument

Additional information

Used simplifier rules: ⊦ r = np.r ∧ c = np.c ↔ np = r × c; (elim) Used terms: np, r, c

Proof step 10 from proof step-L6-L7 (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, alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx ⊦ alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))) ∧ disjointp(U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), gspmx) ∧ y[r, y[r] + ghostlspmxf(tid)[r × r0] * x[r0]] + (U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x ∧ U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))) ⊆ spmx

Rule argument

Additional information

Proof step 11 from proof step-L6-L7 (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, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx ⊦ alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))) ∧ disjointp(U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), gspmx) ∧ y[r, y[r] + ghostlspmxf(tid)[r × r0] * x[r0]] + (U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x ∧ U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))) ⊆ spmx

• Proof step 132:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, ¬ alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))) ⊦ alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))) ∧ disjointp(U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), gspmx) ∧ y[r, y[r] + ghostlspmxf(tid)[r × r0] * x[r0]] + (U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x ∧ U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))) ⊆ spmx

Rule argument

Additional information

Used formulas: alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0)))

Proof step 12 from proof step-L6-L7 (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, alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx ⊦ disjointp(U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), gspmx) ∧ y[r, y[r] + ghostlspmxf(tid)[r × r0] * x[r0]] + (U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x ∧ U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))) ⊆ spmx

Rule argument

Additional information

Proof step 13 from proof step-L6-L7 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 14:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, ¬ disjointp(U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), gspmx) ⊦

• Proof step 21:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, y[r, y[r] + ghostlspmxf(tid)[r × r0] * x[r0]] + (U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))) ∪ gspmx).toMatrix(# y, # x) * x ≠ spmx.toMatrix(# y, # x) * x, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx ⊦

• Proof step 115:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, ¬ U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))) ⊆ spmx ⊦

Rule argument

Additional information

Proof step 14 from proof step-L6-L7 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

  ⊦ disjointp(spmx1, spmx2) → (disjointp(spmx3, spmx4) ↔ (∀ np. (np ∈ spmx1 → ¬ np ∈ spmx2) → np ∈ spmx3 → ¬ np ∈ spmx4))

• Proof step 16:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, ∃ np. ¬((np ∈ U(alltids, ghostlspmxf) → ¬ np ∈ gspmx) → np ∈ U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))) → ¬ np ∈ gspmx) ⊦

Rule argument

Additional information

Used terms: U(alltids, ghostlspmxf), gspmx, U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), gspmx

Proof step 15 from proof step-L6-L7 (previous step) (back to tree)

A spec-lemma

Proof step 16 from proof step-L6-L7 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), np ∈ gspmx, np ∈ (tid = tid0 ⊃ ghostlspmxf(tid0) -- (r × r0);ghostlspmxf(tid0)), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx ⊦ ∃ 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 17 from proof step-L6-L7 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 18:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, tid = tid0, alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ gspmx, r × r0 ∈ ghostlspmxf(tid), np ∈ ghostlspmxf(tid0) -- (r × r0), gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx ⊦ ∃ tid1. np ∈ ghostlspmxf(tid1)

• Proof step 20:

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

Rule argument

Additional information

Proof step 18 from proof step-L6-L7 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, np ≠ r × r0, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid0; ghostlspmxf(tid0) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid0), np ∈ gspmx, np ∈ ghostlspmxf(tid0), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx ⊦ ∃ tid1. np ∈ ghostlspmxf(tid1)

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ st -- b ↔ a ≠ b ∧ a ∈ st; (s)

Proof step 19 from proof step-L6-L7 (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 20 from proof step-L6-L7 (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 21 from proof step-L6-L7 (previous step) (back to tree)

User applied rule cut formula

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; ghostlspmxf(tid) -- (r × r0))) ∪ gspmx = (U(alltids, ghostlspmxf) ∪ gspmx) -- (r × r0), y[r, y[r] + ghostlspmxf(tid)[r × r0] * x[r0]] + (U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))) ∪ gspmx).toMatrix(# y, # x) * x ≠ spmx.toMatrix(# y, # x) * x, alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx ⊦

• Proof step 50:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, y[r, y[r] + ghostlspmxf(tid)[r × r0] * x[r0]] + (U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))) ∪ gspmx).toMatrix(# y, # x) * x ≠ spmx.toMatrix(# y, # x) * x, U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))) ∪ gspmx ≠ (U(alltids, ghostlspmxf) ∪ gspmx) -- (r × r0), alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx ⊦

Rule argument

Additional information

Used formulas: U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))) ∪ gspmx = (U(alltids, ghostlspmxf) ∪ gspmx) -- (r × r0)

Proof step 22 from proof step-L6-L7 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))) ∪ gspmx = (U(alltids, ghostlspmxf) ∪ gspmx) -- (r × r0), y[r, y[r] + ghostlspmxf(tid)[r × r0] * x[r0]] + ((U(alltids, ghostlspmxf) ∪ gspmx) -- (r × r0)).toMatrix(# y, # x) * x ≠ spmx.toMatrix(# y, # x) * x, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx ⊦

Rule argument

Additional information

Proof step 23 from proof step-L6-L7 (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 24:

  U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))) ∪ gspmx = (U(alltids, ghostlspmxf) ∪ gspmx) -- (r × r0), y[r, y[r] + ghostlspmxf(tid)[r × r0] * x[r0]] + ((U(alltids, ghostlspmxf) ∪ gspmx) -- (r × r0)).toMatrix(# y, # x) * x ≠ y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x, alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx ⊦

Rule argument

Additional information

Proof step 24 from proof step-L6-L7 (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 25:

  ⊦ r × c ∈ spmx ∧ c < # x ∧ r < # y → y[r, y[r] + spmx[r × c] * x[c]] + (spmx -- (r × c)).toMatrix(# y, # x) * x = y + spmx.toMatrix(# y, # x) * x

• Proof step 26:

  U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))) ∪ gspmx = (U(alltids, ghostlspmxf) ∪ gspmx) -- (r × r0), y[r, y[r] + ghostlspmxf(tid)[r × r0] * x[r0]] + ((U(alltids, ghostlspmxf) ∪ gspmx) -- (r × r0)).toMatrix(# y, # x) * x ≠ y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, r × r0 ∈ U(alltids, ghostlspmxf) ∪ gspmx ∧ r0 < # x ∧ r < # y → y[r, y[r] + (U(alltids, ghostlspmxf) ∪ gspmx)[r × r0] * x[r0]] + ((U(alltids, ghostlspmxf) ∪ gspmx) -- (r × r0)).toMatrix(# y, # x) * x = y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x ⊦

Rule argument

Additional information

Used terms: y, U(alltids, ghostlspmxf) ∪ gspmx, r0, r, x

Proof step 25 from proof step-L6-L7 (previous step) (back to tree)

A spec-lemma

Proof step 26 from proof step-L6-L7 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))) ∪ gspmx = (U(alltids, ghostlspmxf) ∪ gspmx) -- (r × r0), y[r, y[r] + ghostlspmxf(tid)[r × r0] * x[r0]] + ((U(alltids, ghostlspmxf) ∪ gspmx) -- (r × r0)).toMatrix(# y, # x) * x ≠ y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x, alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, r × r0 ∈ U(alltids, ghostlspmxf) ∪ gspmx ∧ r0 < # x ∧ r < # y → y[r, y[r] + (∃ tid0. r × r0 ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid)[r × r0];gspmx[r × r0]) * x[r0]] + ((U(alltids, ghostlspmxf) ∪ gspmx) -- (r × r0)).toMatrix(# y, # x) * x = y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x ⊦

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) ⊦ (spmx1 ∪ spmx2)[np] = (np ∈ spmx1 ⊃ spmx1[np];spmx2[np]); (s)

Proof step 27 from proof step-L6-L7 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 28:

  U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))) ∪ gspmx = (U(alltids, ghostlspmxf) ∪ gspmx) -- (r × r0), y[r, y[r] + ghostlspmxf(tid)[r × r0] * x[r0]] + ((U(alltids, ghostlspmxf) ∪ gspmx) -- (r × r0)).toMatrix(# y, # x) * x ≠ y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x, r0 < # x, r < # y, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), r × r0 ∈ U(alltids, ghostlspmxf), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, r × r0 ∈ U(alltids, ghostlspmxf) ∪ gspmx ∧ r0 < # x ∧ r < # y → y[r, y[r] + (∃ tid0. r × r0 ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid)[r × r0];gspmx[r × r0]) * x[r0]] + ((U(alltids, ghostlspmxf) ∪ gspmx) -- (r × r0)).toMatrix(# y, # x) * x = y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x ⊦

• Proof step 34:

  U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))) ∪ gspmx = (U(alltids, ghostlspmxf) ∪ gspmx) -- (r × r0), y[r, y[r] + ghostlspmxf(tid)[r × r0] * x[r0]] + ((U(alltids, ghostlspmxf) ∪ gspmx) -- (r × r0)).toMatrix(# y, # x) * x ≠ y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, r × r0 ∈ U(alltids, ghostlspmxf) ∪ gspmx ∧ r0 < # x ∧ r < # y → y[r, y[r] + (∃ tid0. r × r0 ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid)[r × r0];gspmx[r × r0]) * x[r0]] + ((U(alltids, ghostlspmxf) ∪ gspmx) -- (r × r0)).toMatrix(# y, # x) * x = y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x ⊦ r × r0 ∈ U(alltids, ghostlspmxf) ∧ r0 < # x ∧ r < # y

Rule argument

Additional information

Used formulas: r × r0 ∈ U(alltids, ghostlspmxf) ∧ r0 < # x ∧ r < # y

Proof step 28 from proof step-L6-L7 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))) ∪ gspmx = (U(alltids, ghostlspmxf) ∪ gspmx) -- (r × r0), y[r, y[r] + ghostlspmxf(tid)[r × r0] * x[r0]] + ((U(alltids, ghostlspmxf) ∪ gspmx) -- (r × r0)).toMatrix(# y, # x) * x ≠ y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x, r0 < # x, r < # y, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid0), r × r0 ∈ ghostlspmxf(tid), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, r × r0 ∈ U(alltids, ghostlspmxf) ∪ gspmx → y[r, y[r] + (∃ tid0. r × r0 ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid)[r × r0];gspmx[r × r0]) * x[r0]] + ((U(alltids, ghostlspmxf) ∪ gspmx) -- (r × r0)).toMatrix(# y, # x) * x = y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x ⊦

Rule argument

Additional information

Used simplifier rules: alltids-all: ⊦ tid ∈ alltids; ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ alldisjointp(ts, f) → (np ∈ U(ts, f) ↔ (∃ tid. tid ∈ ts ∧ np ∈ f(tid))); (s)

Proof step 29 from proof step-L6-L7 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 30:

  U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))) ∪ gspmx = (U(alltids, ghostlspmxf) ∪ gspmx) -- (r × r0), y[r, y[r] + ghostlspmxf(tid)[r × r0] * x[r0]] + ((U(alltids, ghostlspmxf) ∪ gspmx) -- (r × r0)).toMatrix(# y, # x) * x ≠ y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x, r < # y, r0 < # x, alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), r × r0 ∈ ghostlspmxf(tid0), gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, ¬ r × r0 ∈ U(alltids, ghostlspmxf) ∪ gspmx ⊦

• Proof step 32:

  U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))) ∪ gspmx = (U(alltids, ghostlspmxf) ∪ gspmx) -- (r × r0), y[r, y[r] + ghostlspmxf(tid)[r × r0] * x[r0]] + ((U(alltids, ghostlspmxf) ∪ gspmx) -- (r × r0)).toMatrix(# y, # x) * x ≠ y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x, r < # y, r0 < # x, alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), r × r0 ∈ ghostlspmxf(tid0), gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, y[r, y[r] + (∃ tid0. r × r0 ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid)[r × r0];gspmx[r × r0]) * x[r0]] + ((U(alltids, ghostlspmxf) ∪ gspmx) -- (r × r0)).toMatrix(# y, # x) * x = y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x ⊦

Rule argument

Additional information

Proof step 30 from proof step-L6-L7 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))) ∪ gspmx = U(alltids, ghostlspmxf) ∪ gspmx, y[r, y[r] + ghostlspmxf(tid)[r × r0] * x[r0]] + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x ≠ y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x, r0 < # x, r < # y, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid0), r × r0 ∈ ghostlspmxf(tid), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, ¬ r × r0 ∈ gspmx ⊦ ∃ tid1. r × r0 ∈ 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) ⊦ ¬ a ∈ st → st -- a = st; (s)

Proof step 31 from proof step-L6-L7 (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: tid

Proof step 32 from proof step-L6-L7 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 33:

  y[r, y[r] + gspmx[r × r0] * x[r0]] + ((U(alltids, ghostlspmxf) ∪ gspmx) -- (r × r0)).toMatrix(# y, # x) * x = y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x, U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))) ∪ gspmx = (U(alltids, ghostlspmxf) ∪ gspmx) -- (r × r0), y[r, y[r] + ghostlspmxf(tid)[r × r0] * x[r0]] + ((U(alltids, ghostlspmxf) ∪ gspmx) -- (r × r0)).toMatrix(# y, # x) * x ≠ y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x, r0 < # x, r < # y, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid0), r × r0 ∈ ghostlspmxf(tid), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, ∀ tid0. ¬ r × r0 ∈ ghostlspmxf(tid0) ⊦

Rule argument

Additional information

Proof step 33 from proof step-L6-L7 (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: tid

Proof step 34 from proof step-L6-L7 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

  U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))) ∪ gspmx = (U(alltids, ghostlspmxf) ∪ gspmx) -- (r × r0), y[r, y[r] + ghostlspmxf(tid)[r × r0] * x[r0]] + ((U(alltids, ghostlspmxf) ∪ gspmx) -- (r × r0)).toMatrix(# y, # x) * x ≠ y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x, alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, r × r0 ∈ U(alltids, ghostlspmxf) ∪ gspmx ∧ r0 < # x ∧ r < # y → y[r, y[r] + (∃ tid0. r × r0 ∈ ghostlspmxf(tid0) ⊃ ghostlspmxf(tid)[r × r0];gspmx[r × r0]) * x[r0]] + ((U(alltids, ghostlspmxf) ∪ gspmx) -- (r × r0)).toMatrix(# y, # x) * x = y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x ⊦ (∃ tid0. r × r0 ∈ ghostlspmxf(tid0)) ∧ r0 < # x ∧ r < # y

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 35 from proof step-L6-L7 (previous step) (back to tree)

User applied rule weakening

And obtained the following new goals

• Proof step 36:

  alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx ⊦ (∃ tid0. r × r0 ∈ ghostlspmxf(tid0)) ∧ r0 < # x ∧ r < # y

Rule argument

Additional information

Proof step 36 from proof step-L6-L7 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 37:

  ⊦ okspmx(spmx, r, c) ↔ (∀ np. np ∈ spmx → np.r < r ∧ np.c < c)

• Proof step 38:

  alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), r × r0 ∈ ghostlspmxf(tid), gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, ∀ np. np ∈ spmx → np.r < # y ∧ np.c < # x ⊦ (∃ tid0. r × r0 ∈ ghostlspmxf(tid0)) ∧ r0 < # x ∧ r < # y

Rule argument

Additional information

Used terms: spmx, # y, # x

Proof step 37 from proof step-L6-L7 (previous step) (back to tree)

A spec-lemma

Proof step 38 from proof step-L6-L7 (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 39:

  alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), r × r0 ∈ ghostlspmxf(tid), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, r × r0 ∈ spmx → (r × r0).r < # y ∧ (r × r0).c < # x ⊦ (∃ tid0. r × r0 ∈ ghostlspmxf(tid0)) ∧ r0 < # x ∧ r < # y

Rule argument

Additional information

Used terms: r × r0

Proof step 39 from proof step-L6-L7 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 40:

  alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), r × r0 ∈ ghostlspmxf(tid), gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, r × r0 ∈ spmx → r < # y ∧ r0 < # x ⊦ (∃ tid0. r × r0 ∈ ghostlspmxf(tid0)) ∧ r0 < # x ∧ r < # y

Rule argument

Additional information

Used simplifier rules: ⊦ (n × n0).c = n0; (s) ⊦ (n × n0).r = n; (s)

Proof step 40 from proof step-L6-L7 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 41:

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

• Proof step 42:

  alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), r × r0 ∈ ghostlspmxf(tid), gspmx ⊆ spmx, r × r0 ∈ spmx → r < # y ∧ r0 < # x, ∀ np. np ∈ U(alltids, ghostlspmxf) → np ∈ spmx ∧ U(alltids, ghostlspmxf)[np] = spmx[np] ⊦ (∃ tid0. r × r0 ∈ ghostlspmxf(tid0)) ∧ r0 < # x ∧ r < # y

Rule argument

Additional information

Used terms: U(alltids, ghostlspmxf), spmx

Proof step 41 from proof step-L6-L7 (previous step) (back to tree)

A spec-lemma

Proof step 42 from proof step-L6-L7 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 43:

  alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), r × r0 ∈ ghostlspmxf(tid), gspmx ⊆ spmx, r × r0 ∈ spmx → r < # y ∧ r0 < # x, ∀ np. (∃ tid0. np ∈ ghostlspmxf(tid0)) → np ∈ spmx ∧ U(alltids, ghostlspmxf)[np] = spmx[np] ⊦ (∃ tid0. r × r0 ∈ ghostlspmxf(tid0)) ∧ r0 < # x ∧ r < # y

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 43 from proof step-L6-L7 (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 44:

  alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), r × r0 ∈ ghostlspmxf(tid), gspmx ⊆ spmx, r × r0 ∈ spmx → r < # y ∧ r0 < # x, (∃ tid0. r × r0 ∈ ghostlspmxf(tid0)) → r × r0 ∈ spmx ∧ U(alltids, ghostlspmxf)[r × r0] = spmx[r × r0] ⊦ (∃ tid0. r × r0 ∈ ghostlspmxf(tid0)) ∧ r0 < # x ∧ r < # y

Rule argument

Additional information

Used terms: r × r0

Proof step 44 from proof step-L6-L7 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 45:

  alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), r × r0 ∈ ghostlspmxf(tid), gspmx ⊆ spmx, r × r0 ∈ spmx → r < # y ∧ r0 < # x, (∃ tid0. r × r0 ∈ ghostlspmxf(tid0)) → r × r0 ∈ spmx ∧ ghostlspmxf(tid)[r × r0] = spmx[r × r0] ⊦ (∃ tid0. r × r0 ∈ ghostlspmxf(tid0)) ∧ r0 < # x ∧ r < # y

Rule argument

Additional information

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

Proof step 45 from proof step-L6-L7 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 46:

  alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), r × r0 ∈ ghostlspmxf(tid), gspmx ⊆ spmx, r × r0 ∈ spmx → r < # y ∧ r0 < # x ⊦ ∃ tid0. r × r0 ∈ ghostlspmxf(tid0), (∃ tid0. r × r0 ∈ ghostlspmxf(tid0)) ∧ r0 < # x ∧ r < # y

• Proof step 48:

  ghostlspmxf(tid)[r × r0] = spmx[r × r0], alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), r × r0 ∈ ghostlspmxf(tid), r × r0 ∈ spmx, gspmx ⊆ spmx, r × r0 ∈ spmx → r < # y ∧ r0 < # x ⊦ (∃ tid0. r × r0 ∈ ghostlspmxf(tid0)) ∧ r0 < # x ∧ r < # y

Rule argument

Additional information

Proof step 46 from proof step-L6-L7 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 47:

  alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), r × r0 ∈ ghostlspmxf(tid), gspmx ⊆ spmx, r × r0 ∈ spmx → r < # y ∧ r0 < # x ⊦ ∃ tid0. r × r0 ∈ ghostlspmxf(tid0)

Rule argument

Additional information

Proof step 47 from proof step-L6-L7 (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: tid

Proof step 48 from proof step-L6-L7 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 49:

  ghostlspmxf(tid)[r × r0] = spmx[r × r0], r0 < # x, r < # y, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), r × r0 ∈ ghostlspmxf(tid), r × r0 ∈ spmx, gspmx ⊆ spmx ⊦ ∃ tid0. r × r0 ∈ ghostlspmxf(tid0)

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 49 from proof step-L6-L7 (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: tid

Proof step 50 from proof step-L6-L7 (previous step) (back to tree)

User applied rule weakening

And obtained the following new goals

• Proof step 51:

  U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))) ∪ gspmx ≠ (U(alltids, ghostlspmxf) ∪ gspmx) -- (r × r0), alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx ⊦

Rule argument

Additional information

Proof step 51 from proof step-L6-L7 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 52:

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

• Proof step 53:

  alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, ∃ np. ¬ ( (np ∈ U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))) ∪ gspmx ↔ np ∈ (U(alltids, ghostlspmxf) ∪ gspmx) -- (r × r0)) ∧ (U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))) ∪ gspmx)[np] = ((U(alltids, ghostlspmxf) ∪ gspmx) -- (r × r0))[np]) ⊦

Rule argument

Additional information

Used terms: U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))) ∪ gspmx, (U(alltids, ghostlspmxf) ∪ gspmx) -- (r × r0)

Proof step 52 from proof step-L6-L7 (previous step) (back to tree)

A spec-lemma

Proof step 53 from proof step-L6-L7 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 54:

  alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx ⊦ (np ∈ U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))) ∪ gspmx ↔ np ≠ r × r0 ∧ np ∈ U(alltids, ghostlspmxf) ∪ gspmx) ∧ (∃ tid0. np ∈ (tid = tid0 ⊃ ghostlspmxf(tid0) -- (r × r0);ghostlspmxf(tid0)) ⊃ U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0)))[np] ;gspmx[np] ) = ((U(alltids, ghostlspmxf) ∪ gspmx) -- (r × r0))[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) ⊦ a ∈ st -- b ↔ a ≠ b ∧ a ∈ st; (s)

Proof step 54 from proof step-L6-L7 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 55:

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

• Proof step 56:

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

Rule argument

Additional information

Used terms: np, U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), gspmx

Proof step 55 from proof step-L6-L7 (previous step) (back to tree)

A spec-lemma

Proof step 56 from proof step-L6-L7 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 57:

  alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx ⊦ ((∃ tid0. np ∈ (tid = tid0 ⊃ ghostlspmxf(tid0) -- (r × r0);ghostlspmxf(tid0))) ∨ np ∈ gspmx ↔ np ≠ r × r0 ∧ np ∈ U(alltids, ghostlspmxf) ∪ gspmx) ∧ (∃ tid0. np ∈ (tid = tid0 ⊃ ghostlspmxf(tid0) -- (r × r0);ghostlspmxf(tid0)) ⊃ U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0)))[np] ;gspmx[np] ) = ((U(alltids, ghostlspmxf) ∪ gspmx) -- (r × r0))[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 57 from proof step-L6-L7 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 58:

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

• Proof step 88:

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

Rule argument

Additional information

Used formulas: (∃ tid0. np ∈ (tid = tid0 ⊃ ghostlspmxf(tid0) -- (r × r0);ghostlspmxf(tid0))) ∨ np ∈ gspmx ↔ np ≠ r × r0 ∧ np ∈ U(alltids, ghostlspmxf) ∪ gspmx

Proof step 58 from proof step-L6-L7 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 59:

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

Rule argument

Additional information

Proof step 59 from proof step-L6-L7 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 60:

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

• Proof step 81:

  gspmx[np] ≠ ((U(alltids, ghostlspmxf) ∪ gspmx) -- (r × r0))[np], alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, (∃ tid0. np ∈ (tid = tid0 ⊃ ghostlspmxf(tid0) -- (r × r0);ghostlspmxf(tid0))) ∨ np ∈ gspmx ↔ np ≠ r × r0 ∧ np ∈ U(alltids, ghostlspmxf) ∪ gspmx, ∀ tid0. ¬ np ∈ (tid = tid0 ⊃ ghostlspmxf(tid0) -- (r × r0);ghostlspmxf(tid0)) ⊦

Rule argument

Additional information

Proof step 60 from proof step-L6-L7 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 61:

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

Rule argument

Additional information

Proof step 61 from proof step-L6-L7 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 62:

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

• Proof step 68:

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

Rule argument

Additional information

Proof step 62 from proof step-L6-L7 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 63:

  np ≠ r × r0, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid0; ghostlspmxf(tid0) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid0), np ∈ ghostlspmxf(tid0), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, (∃ tid1. np ∈ (tid0 = tid1 ⊃ ghostlspmxf(tid1) -- (r × r0);ghostlspmxf(tid1))) ∨ np ∈ gspmx ↔ np ∈ U(alltids, ghostlspmxf) ∪ gspmx ⊦ U(alltids, ghostlspmxf(tid0; ghostlspmxf(tid0) -- (r × r0)))[np] = (∃ tid. np ∈ ghostlspmxf(tid) ⊃ 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) ⊦ a ∈ st -- b ↔ a ≠ b ∧ a ∈ st; (s) ⊦ alldisjointp(ts, f) → (np ∈ U(ts, f) ↔ (∃ tid. tid ∈ ts ∧ np ∈ f(tid))); (s) ⊦ (spmx1 ∪ spmx2)[np] = (np ∈ spmx1 ⊃ spmx1[np];spmx2[np]); (s) a ≠ b ⊦ (st -- b)[a] = st[a]; (s)

Proof step 63 from proof step-L6-L7 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 64:

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

• Proof step 65:

  np ≠ r × r0, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid0; ghostlspmxf(tid0) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid0), r × r0 ∈ ghostlspmxf(tid0), np ∈ ghostlspmxf(tid0; ghostlspmxf(tid0) -- (r × r0))(tid0), gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, (∃ tid1. np ∈ (tid0 = tid1 ⊃ ghostlspmxf(tid1) -- (r × r0);ghostlspmxf(tid1))) ∨ np ∈ gspmx ↔ np ∈ U(alltids, ghostlspmxf) ∪ gspmx ⊦ ghostlspmxf(tid0; ghostlspmxf(tid0) -- (r × r0))(tid0)[np] = (∃ tid. np ∈ ghostlspmxf(tid) ⊃ ghostlspmxf(tid0)[np];gspmx[np])

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ st -- b ↔ a ≠ b ∧ a ∈ st; (s) Used terms: tid0, alltids, ghostlspmxf(tid0; ghostlspmxf(tid0) -- (r × r0)), np

Proof step 64 from proof step-L6-L7 (previous step) (back to tree)

A spec-lemma

Proof step 65 from proof step-L6-L7 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 66:

  np ≠ r × r0, alldisjointp(alltids, ghostlspmxf(tid0; ghostlspmxf(tid0) -- (r × r0))), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid0), np ∈ ghostlspmxf(tid0), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, (∃ tid1. np ∈ (tid0 = tid1 ⊃ ghostlspmxf(tid1) -- (r × r0);ghostlspmxf(tid1))) ∨ np ∈ gspmx ↔ np ∈ U(alltids, ghostlspmxf) ∪ gspmx ⊦ ghostlspmxf(tid0)[np] = (∃ tid. np ∈ ghostlspmxf(tid) ⊃ ghostlspmxf(tid0)[np];gspmx[np])

Rule argument

Additional information

Used simplifier rules: ⊦ a ≠ b → (st -- b)[a] = st[a]; (s) ⊦ a ∈ st -- b ↔ a ≠ b ∧ a ∈ st; (s)

Proof step 66 from proof step-L6-L7 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 67:

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

Rule argument

Additional information

Proof step 67 from proof step-L6-L7 (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 68 from proof step-L6-L7 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 69:

  ⊦ a ≠ b → (st -- b)[a] = st[a]

• Proof step 70:

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

• Proof step 75:

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

Rule argument

Additional information

Used terms: U(alltids, ghostlspmxf) ∪ gspmx, r × r0, np

Proof step 69 from proof step-L6-L7 (previous step) (back to tree)

A spec-lemma

Proof step 70 from proof step-L6-L7 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 71:

  U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0)))[r × r0] ≠ ∅[r × r0], tid ≠ tid0, alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), r × r0 ∈ ghostlspmxf(tid0), gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, ¬ r × r0 ∈ gspmx ⊦ ∃ tid0. r × r0 ∈ (tid = tid0 ⊃ ghostlspmxf(tid0) -- (r × r0);ghostlspmxf(tid0))

Rule argument

Additional information

Used simplifier rules: ⊦ (st -- a)[a] = ∅[a]; (s)

Proof step 71 from proof step-L6-L7 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 72:

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

• Proof step 73:

  U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0)))[r × r0] ≠ ∅[r × r0], tid ≠ tid0, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), r × r0 ∈ ghostlspmxf(tid0), r × r0 ∈ ghostlspmxf(tid), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, ¬ r × r0 ∈ gspmx ⊦ ∃ tid0. r × r0 ∈ (tid = tid0 ⊃ ghostlspmxf(tid0) -- (r × r0);ghostlspmxf(tid0))

Rule argument

Additional information

Used terms: U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), r × r0

Proof step 72 from proof step-L6-L7 (previous step) (back to tree)

A spec-lemma

Proof step 73 from proof step-L6-L7 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 74:

  U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0)))[r × r0] ≠ ∅[r × r0], tid ≠ tid0, alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), r × r0 ∈ ghostlspmxf(tid0), r × r0 ∈ (tid = tid1 ⊃ ghostlspmxf(tid1) -- (r × r0);ghostlspmxf(tid1)), gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, ¬ r × r0 ∈ gspmx ⊦ ∃ tid0. r × r0 ∈ (tid = tid0 ⊃ ghostlspmxf(tid0) -- (r × r0);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 74 from proof step-L6-L7 (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 75 from proof step-L6-L7 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 76:

  np ≠ r × r0, tid ≠ tid0, alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), np ∈ ghostlspmxf(tid0), gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, (∃ tid0. np ∈ (tid = tid0 ⊃ ghostlspmxf(tid0) -- (r × r0);ghostlspmxf(tid0))) ∨ np ∈ gspmx ↔ np ∈ U(alltids, ghostlspmxf) ∪ gspmx ⊦ U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0)))[np] = (∃ tid1. np ∈ ghostlspmxf(tid1) ⊃ 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) ⊦ (spmx1 ∪ spmx2)[np] = (np ∈ spmx1 ⊃ spmx1[np];spmx2[np]); (s)

Proof step 76 from proof step-L6-L7 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 77:

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

• Proof step 78:

  np ≠ r × r0, tid ≠ tid0, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid0), r × r0 ∈ ghostlspmxf(tid), np ∈ ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))(tid0), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, (∃ tid0. np ∈ (tid = tid0 ⊃ ghostlspmxf(tid0) -- (r × r0);ghostlspmxf(tid0))) ∨ np ∈ gspmx ↔ np ∈ U(alltids, ghostlspmxf) ∪ gspmx ⊦ ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))(tid0)[np] = (∃ tid1. np ∈ ghostlspmxf(tid1) ⊃ ghostlspmxf(tid0)[np];gspmx[np])

Rule argument

Additional information

Used terms: alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0)), np, tid0

Proof step 77 from proof step-L6-L7 (previous step) (back to tree)

A spec-lemma

Proof step 78 from proof step-L6-L7 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 79:

  np ≠ r × r0, tid ≠ tid0, alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), np ∈ ghostlspmxf(tid0), gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, (∃ tid0. np ∈ (tid = tid0 ⊃ ghostlspmxf(tid0) -- (r × r0);ghostlspmxf(tid0))) ∨ np ∈ gspmx ↔ np ∈ U(alltids, ghostlspmxf) ∪ gspmx ⊦ ghostlspmxf(tid0)[np] = (∃ tid1. np ∈ ghostlspmxf(tid1) ⊃ ghostlspmxf(tid0)[np];gspmx[np])

Rule argument

Additional information

Proof step 79 from proof step-L6-L7 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 80:

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

Rule argument

Additional information

Proof step 80 from proof step-L6-L7 (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 81 from proof step-L6-L7 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 82:

  ⊦ a ≠ b → (st -- b)[a] = st[a]

• Proof step 83:

  gspmx[np] ≠ (U(alltids, ghostlspmxf) ∪ gspmx)[np], np ≠ r × r0, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, (∃ tid0. np ∈ (tid = tid0 ⊃ ghostlspmxf(tid0) -- (r × r0);ghostlspmxf(tid0))) ∨ np ∈ gspmx ↔ np ≠ r × r0 ∧ np ∈ U(alltids, ghostlspmxf) ∪ gspmx, ∀ tid0. ¬ np ∈ (tid = tid0 ⊃ ghostlspmxf(tid0) -- (r × r0);ghostlspmxf(tid0)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ (st -- a)[a] = ∅[a]; (s) ⊦ ¬ a ∈ st → st[a] = ∅[a]; (s) Used terms: U(alltids, ghostlspmxf) ∪ gspmx, r × r0, np

Proof step 82 from proof step-L6-L7 (previous step) (back to tree)

A spec-lemma

Proof step 83 from proof step-L6-L7 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 84:

  np ≠ r × r0, alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, (∃ tid0. np ∈ (tid = tid0 ⊃ ghostlspmxf(tid0) -- (r × r0);ghostlspmxf(tid0))) ∨ np ∈ gspmx ↔ np ∈ U(alltids, ghostlspmxf) ∪ gspmx, ∀ tid0. ¬ np ∈ (tid = tid0 ⊃ ghostlspmxf(tid0) -- (r × r0);ghostlspmxf(tid0)) ⊦ gspmx[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 84 from proof step-L6-L7 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 85:

  gspmx[np] ≠ U(alltids, ghostlspmxf)[np], np ≠ r × r0, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, (∃ tid0. np ∈ (tid = tid0 ⊃ ghostlspmxf(tid0) -- (r × r0);ghostlspmxf(tid0))) ∨ np ∈ gspmx ↔ np ∈ U(alltids, ghostlspmxf) ∪ gspmx, ∀ tid0. ¬ np ∈ (tid = tid0 ⊃ ghostlspmxf(tid0) -- (r × r0);ghostlspmxf(tid0)), ∃ tid0. np ∈ ghostlspmxf(tid0) ⊦

Rule argument

Additional information

Proof step 85 from proof step-L6-L7 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 86:

  gspmx[np] ≠ ghostlspmxf(tid0)[np], np ≠ r × r0, alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid0), r × r0 ∈ ghostlspmxf(tid), gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, (∃ tid0. np ∈ (tid = tid0 ⊃ ghostlspmxf(tid0) -- (r × r0);ghostlspmxf(tid0))) ∨ np ∈ gspmx ↔ np ∈ U(alltids, ghostlspmxf) ∪ gspmx, ∀ tid0. ¬ np ∈ (tid = tid0 ⊃ ghostlspmxf(tid0) -- (r × r0);ghostlspmxf(tid0)) ⊦

Rule argument

Additional information

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

Proof step 86 from proof step-L6-L7 (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 87:

  gspmx[np] ≠ ghostlspmxf(tid0)[np], np ≠ r × r0, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), np ∈ ghostlspmxf(tid0), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, ¬ np ∈ (tid = tid0 ⊃ ghostlspmxf(tid0) -- (r × r0);ghostlspmxf(tid0)), (∃ tid0. np ∈ (tid = tid0 ⊃ ghostlspmxf(tid0) -- (r × r0);ghostlspmxf(tid0))) ∨ np ∈ gspmx ↔ np ∈ U(alltids, ghostlspmxf) ∪ gspmx, ∀ tid0. ¬ np ∈ (tid = tid0 ⊃ ghostlspmxf(tid0) -- (r × r0);ghostlspmxf(tid0)) ⊦

Rule argument

Additional information

Used terms: tid0

Proof step 87 from proof step-L6-L7 (previous step) (back to tree)

User applied rule case distinction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ st -- b ↔ a ≠ b ∧ a ∈ st; (s)

Proof step 88 from proof step-L6-L7 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 89:

  alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx ⊦ (∃ tid0. np ∈ (tid = tid0 ⊃ ghostlspmxf(tid0) -- (r × r0);ghostlspmxf(tid0))) ∨ np ∈ gspmx ↔ np ≠ r × r0 ∧ np ∈ U(alltids, ghostlspmxf) ∪ gspmx

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) a ≠ b ⊦ (st -- b)[a] = st[a]; (s) ⊦ a ∈ st -- b ↔ a ≠ b ∧ a ∈ st; (s)

Proof step 89 from proof step-L6-L7 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 90:

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

• Proof step 91:

  alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx ⊦ (∃ tid0. np ∈ (tid = tid0 ⊃ ghostlspmxf(tid0) -- (r × r0);ghostlspmxf(tid0))) ∨ np ∈ gspmx ↔ np ≠ r × r0 ∧ (np ∈ U(alltids, ghostlspmxf) ∨ np ∈ gspmx)

Rule argument

Additional information

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

Proof step 90 from proof step-L6-L7 (previous step) (back to tree)

A spec-lemma

Proof step 91 from proof step-L6-L7 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 92:

  alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx ⊦ (∃ tid0. np ∈ (tid = tid0 ⊃ ghostlspmxf(tid0) -- (r × r0);ghostlspmxf(tid0))) ∨ np ∈ gspmx ↔ np ≠ r × r0 ∧ ((∃ tid0. np ∈ ghostlspmxf(tid0)) ∨ np ∈ gspmx)

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 92 from proof step-L6-L7 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 93:

  alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, (∃ tid0. np ∈ (tid = tid0 ⊃ ghostlspmxf(tid0) -- (r × r0);ghostlspmxf(tid0))) ∨ np ∈ gspmx ⊦ np ≠ r × r0 ∧ ((∃ tid0. np ∈ ghostlspmxf(tid0)) ∨ np ∈ gspmx)

• Proof step 112:

  np ≠ r × r0, alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, ¬ np ∈ gspmx, (∃ tid0. np ∈ ghostlspmxf(tid0)) ∨ np ∈ gspmx ⊦ ∃ tid0. np ∈ (tid = tid0 ⊃ ghostlspmxf(tid0) -- (r × r0);ghostlspmxf(tid0))

Rule argument

Additional information

Proof step 93 from proof step-L6-L7 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 94:

  alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, np ∈ (tid = tid0 ⊃ ghostlspmxf(tid0) -- (r × r0);ghostlspmxf(tid0)) ∨ np ∈ gspmx ⊦ np ≠ r × r0 ∧ ((∃ tid0. np ∈ ghostlspmxf(tid0)) ∨ np ∈ gspmx)

Rule argument

Additional information

Proof step 94 from proof step-L6-L7 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 95:

  alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), np ∈ (tid = tid0 ⊃ ghostlspmxf(tid0) -- (r × r0);ghostlspmxf(tid0)), gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx ⊦ np ≠ r × r0 ∧ ((∃ tid0. np ∈ ghostlspmxf(tid0)) ∨ np ∈ gspmx)

• Proof step 105:

  alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), np ∈ gspmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx ⊦ np ≠ r × r0 ∧ ((∃ tid0. np ∈ ghostlspmxf(tid0)) ∨ np ∈ gspmx)

Rule argument

Additional information

Proof step 95 from proof step-L6-L7 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 96:

  tid = tid0, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), np ∈ ghostlspmxf(tid0) -- (r × r0), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx ⊦ np ≠ r × r0 ∧ ((∃ tid0. np ∈ ghostlspmxf(tid0)) ∨ np ∈ gspmx)

• Proof step 98:

  tid ≠ tid0, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), np ∈ ghostlspmxf(tid0), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx ⊦ np ≠ r × r0 ∧ ((∃ tid0. np ∈ ghostlspmxf(tid0)) ∨ np ∈ gspmx)

Rule argument

Additional information

Proof step 96 from proof step-L6-L7 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 97:

  np ≠ r × r0, alldisjointp(alltids, ghostlspmxf(tid0; ghostlspmxf(tid0) -- (r × r0))), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid0), np ∈ ghostlspmxf(tid0), gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, ¬ np ∈ gspmx ⊦ ∃ tid0. np ∈ ghostlspmxf(tid0)

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ st -- b ↔ a ≠ b ∧ a ∈ st; (s)

Proof step 97 from proof step-L6-L7 (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 98 from proof step-L6-L7 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 99:

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

• Proof step 100:

  tid ≠ tid0, alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid0), r × r0 ∈ ghostlspmxf(tid), gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, ∀ tid1, tid2, np. tid1 ∈ alltids ∧ tid2 ∈ alltids ∧ np ∈ ghostlspmxf(tid1) ∧ tid1 ≠ tid2 → ¬ np ∈ ghostlspmxf(tid2) ⊦ np ≠ r × r0 ∧ ((∃ tid0. np ∈ ghostlspmxf(tid0)) ∨ np ∈ gspmx)

Rule argument

Additional information

Used terms: alltids, ghostlspmxf

Proof step 99 from proof step-L6-L7 (previous step) (back to tree)

A spec-lemma

Proof step 100 from proof step-L6-L7 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 101:

  tid ≠ tid0, alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), np ∈ ghostlspmxf(tid0), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, ∀ tid1, tid2, np0. np0 ∈ ghostlspmxf(tid1) ∧ tid1 ≠ tid2 → ¬ np0 ∈ ghostlspmxf(tid2) ⊦ np ≠ r × r0 ∧ ((∃ tid0. np ∈ ghostlspmxf(tid0)) ∨ np ∈ gspmx)

Rule argument

Additional information

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

Proof step 101 from proof step-L6-L7 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 102:

  np = r × r0, tid ≠ tid0, alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid0), r × r0 ∈ ghostlspmxf(tid), gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, ∀ tid1, tid2, np0. np0 ∈ ghostlspmxf(tid1) ∧ tid1 ≠ tid2 → ¬ np0 ∈ ghostlspmxf(tid2) ⊦

• Proof step 104:

  tid ≠ tid0, alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid0), r × r0 ∈ ghostlspmxf(tid), gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, ¬ np ∈ gspmx, ∀ tid1, tid2, np0. np0 ∈ ghostlspmxf(tid1) ∧ tid1 ≠ tid2 → ¬ np0 ∈ ghostlspmxf(tid2) ⊦ ∃ tid0. np ∈ ghostlspmxf(tid0)

Rule argument

Additional information

Proof step 102 from proof step-L6-L7 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 103:

  tid ≠ tid0, alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), r × r0 ∈ ghostlspmxf(tid0), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, ∀ tid1, tid2, np0. np0 ∈ ghostlspmxf(tid1) ∧ tid1 ≠ tid2 → ¬ np0 ∈ ghostlspmxf(tid2) ⊦

Rule argument

Additional information

Proof step 103 from proof step-L6-L7 (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: tid, tid0, r × r0

Proof step 104 from proof step-L6-L7 (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 105 from proof step-L6-L7 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 106:

  alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), r × r0 ∈ gspmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx ⊦

Rule argument

Additional information

Proof step 106 from proof step-L6-L7 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 107:

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

• Proof step 108:

  alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), okspmx(spmx, # y, # x), r × r0 ∈ gspmx, r × r0 ∈ ghostlspmxf(tid), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, ∀ np. np ∈ U(alltids, ghostlspmxf) → ¬ np ∈ gspmx ⊦

Rule argument

Additional information

Used terms: U(alltids, ghostlspmxf), gspmx

Proof step 107 from proof step-L6-L7 (previous step) (back to tree)

A spec-lemma

Proof step 108 from proof step-L6-L7 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 109:

  alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), alldisjointp(alltids, ghostlspmxf), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), r × r0 ∈ gspmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, ∀ np. (∃ tid0. np ∈ ghostlspmxf(tid0)) → ¬ np ∈ gspmx ⊦

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 109 from proof step-L6-L7 (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 110:

  alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), okspmx(spmx, # y, # x), r × r0 ∈ gspmx, r × r0 ∈ ghostlspmxf(tid), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, (∃ tid0. r × r0 ∈ ghostlspmxf(tid0)) → ¬ r × r0 ∈ gspmx ⊦

Rule argument

Additional information

Used terms: r × r0

Proof step 110 from proof step-L6-L7 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 111:

  alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), alldisjointp(alltids, ghostlspmxf), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), r × r0 ∈ gspmx, gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx ⊦ ∃ tid0. r × r0 ∈ ghostlspmxf(tid0)

Rule argument

Additional information

Proof step 111 from proof step-L6-L7 (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: tid

Proof step 112 from proof step-L6-L7 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 113:

  np ≠ r × r0, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), np ∈ ghostlspmxf(tid0), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, ¬ np ∈ gspmx ⊦ ∃ tid0. np ∈ (tid = tid0 ⊃ ghostlspmxf(tid0) -- (r × r0);ghostlspmxf(tid0))

Rule argument

Additional information

Proof step 113 from proof step-L6-L7 (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 114:

  np ≠ r × r0, alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid0), r × r0 ∈ ghostlspmxf(tid), gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, ¬ np ∈ (tid = tid0 ⊃ ghostlspmxf(tid0) -- (r × r0);ghostlspmxf(tid0)), ¬ np ∈ gspmx ⊦ ∃ tid0. np ∈ (tid = tid0 ⊃ ghostlspmxf(tid0) -- (r × r0);ghostlspmxf(tid0))

Rule argument

Additional information

Used terms: tid0

Proof step 114 from proof step-L6-L7 (previous step) (back to tree)

User applied rule case distinction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ st -- b ↔ a ≠ b ∧ a ∈ st; (s)

Proof step 115 from proof step-L6-L7 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 116:

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

• Proof step 117:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, ∃ np. ¬ ( np ∈ U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))) → np ∈ spmx ∧ U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0)))[np] = spmx[np]) ⊦

Rule argument

Additional information

Used terms: U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), spmx

Proof step 116 from proof step-L6-L7 (previous step) (back to tree)

A spec-lemma

Proof step 117 from proof step-L6-L7 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 118:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), np ∈ (tid = tid0 ⊃ ghostlspmxf(tid0) -- (r × r0);ghostlspmxf(tid0)), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx ⊦ np ∈ spmx ∧ U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0)))[np] = spmx[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 118 from proof step-L6-L7 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 119:

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

• Proof step 120:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ (tid = tid0 ⊃ ghostlspmxf(tid0) -- (r × r0);ghostlspmxf(tid0)), r × r0 ∈ ghostlspmxf(tid), gspmx ⊆ spmx, ∀ np. np ∈ U(alltids, ghostlspmxf) → np ∈ spmx ∧ U(alltids, ghostlspmxf)[np] = spmx[np] ⊦ np ∈ spmx ∧ U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0)))[np] = spmx[np]

Rule argument

Additional information

Used terms: U(alltids, ghostlspmxf), spmx

Proof step 119 from proof step-L6-L7 (previous step) (back to tree)

A spec-lemma

Proof step 120 from proof step-L6-L7 (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, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), np ∈ (tid = tid0 ⊃ ghostlspmxf(tid0) -- (r × r0);ghostlspmxf(tid0)), gspmx ⊆ spmx, ∀ np0. (∃ tid1. np0 ∈ ghostlspmxf(tid1)) → np0 ∈ spmx ∧ U(alltids, ghostlspmxf)[np0] = spmx[np0] ⊦ np ∈ spmx ∧ U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0)))[np] = spmx[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 121 from proof step-L6-L7 (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 122:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ (tid = tid0 ⊃ ghostlspmxf(tid0) -- (r × r0);ghostlspmxf(tid0)), r × r0 ∈ ghostlspmxf(tid), gspmx ⊆ spmx, (∃ tid1. np ∈ ghostlspmxf(tid1)) → np ∈ spmx ∧ U(alltids, ghostlspmxf)[np] = spmx[np] ⊦ np ∈ spmx ∧ U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0)))[np] = spmx[np]

Rule argument

Additional information

Used terms: np

Proof step 122 from proof step-L6-L7 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 123:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), np ∈ (tid = tid0 ⊃ ghostlspmxf(tid0) -- (r × r0);ghostlspmxf(tid0)), gspmx ⊆ spmx ⊦ ∃ tid1. np ∈ ghostlspmxf(tid1), np ∈ spmx ∧ U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0)))[np] = spmx[np]

• Proof step 127:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, U(alltids, ghostlspmxf)[np] = spmx[np], alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), np ∈ (tid = tid0 ⊃ ghostlspmxf(tid0) -- (r × r0);ghostlspmxf(tid0)), np ∈ spmx, gspmx ⊆ spmx ⊦ np ∈ spmx ∧ U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0)))[np] = spmx[np]

Rule argument

Additional information

Proof step 123 from proof step-L6-L7 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 124:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, tid = tid0, alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), np ∈ ghostlspmxf(tid0) -- (r × r0), gspmx ⊆ spmx ⊦ ∃ tid1. np ∈ ghostlspmxf(tid1), np ∈ spmx ∧ U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0)))[np] = spmx[np]

• Proof step 126:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, tid ≠ tid0, alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))), alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), np ∈ ghostlspmxf(tid0), gspmx ⊆ spmx ⊦ ∃ tid1. np ∈ ghostlspmxf(tid1), np ∈ spmx ∧ U(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0)))[np] = spmx[np]

Rule argument

Additional information

Proof step 124 from proof step-L6-L7 (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, np ≠ r × r0, alldisjointp(alltids, ghostlspmxf), alldisjointp(alltids, ghostlspmxf(tid0; ghostlspmxf(tid0) -- (r × r0))), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid0), np ∈ ghostlspmxf(tid0), gspmx ⊆ spmx ⊦ ∃ tid1. np ∈ ghostlspmxf(tid1), np ∈ spmx ∧ U(alltids, ghostlspmxf(tid0; ghostlspmxf(tid0) -- (r × r0)))[np] = spmx[np]

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ st -- b ↔ a ≠ b ∧ a ∈ st; (s)

Proof step 125 from proof step-L6-L7 (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 126 from proof step-L6-L7 (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 127 from proof step-L6-L7 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 128:

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

Rule argument

Additional information

Proof step 128 from proof step-L6-L7 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 129:

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

• Proof step 130:

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

Rule argument

Additional information

Used terms: alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0)), np, tid0

Proof step 129 from proof step-L6-L7 (previous step) (back to tree)

A spec-lemma

Proof step 130 from proof step-L6-L7 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 131:

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

Rule argument

Additional information

Proof step 131 from proof step-L6-L7 (previous step) (back to tree)

User applied rule case distinction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ alldisjointp(ts, f) ∧ np ∈ f(tid) → U(ts, f)[np] = f(tid)[np]; (s) a ≠ b ⊦ (st -- b)[a] = st[a]; (s) ⊦ a ∈ st -- b ↔ a ≠ b ∧ a ∈ st; (s)

Proof step 132 from proof step-L6-L7 (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, alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), r × r0 ∈ ghostlspmxf(tid), gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, ¬ alldisjointp(alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))) ⊦

Rule argument

Additional information

Proof step 133 from proof step-L6-L7 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 134:

  ⊦ 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 135:

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

Rule argument

Additional information

Used terms: ghostlspmxf, alltids, ghostlspmxf(tid; ghostlspmxf(tid) -- (r × r0))

Proof step 134 from proof step-L6-L7 (previous step) (back to tree)

A spec-lemma

Proof step 135 from proof step-L6-L7 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 136:

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

Rule argument

Additional information

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

Proof step 136 from proof step-L6-L7 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 137:

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

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ st -- b ↔ a ≠ b ∧ a ∈ st; (s)

Proof step 137 from proof step-L6-L7 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 138:

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

Rule argument

Additional information

Proof step 138 from proof step-L6-L7 (previous step) (back to tree)

User applied rule case distinction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ st -- b ↔ a ≠ b ∧ a ∈ st; (s)