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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

Proof step 2 from proof rely-L2-L1 (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.tid ≠ tid0, alldisjointp(alltids, gs.ghostlspmxf), disjointp(U(alltids, gs.ghostlspmxf), gs.gspmx), okspmx(gs.spmx, gs.r, # gs.x), U(alltids, gs.ghostlspmxf) ⊆ gs.spmx, gs.gspmx ⊆ gs.spmx, lspmx0 ≠ ∅ ∧ lspmx0 ⊆ gs.gspmx ∧ a = chooseL2(lspmx0) ∨ a = τ ∧ ¬(∃ lspmx0. lspmx0 ≠ ∅ ∧ lspmx0 ⊆ gs.gspmx) ⊦ ∃ lspmx0. a = chooseL2(lspmx0), gs.ghostlspmxf(tid0) = gstepf(gs, ls, L2, a).ghostlspmxf(tid0) ∧ gstepf(gs, ls, L2, a).gspmx ⊆ gs.gspmx

Rule argument

Additional information

Used simplifier rules: pcstepf-L2: ⊦ pcstepf(gs, ls, L2, a) = (∃ lspmx0. a = chooseL2(lspmx0) ⊃ L3;L1); disj-35: ⊦ L1 ≠ L3; pre-L2: ⊦ pre(gs, ls, L2, a) ↔ (∃ lspmx0. (lspmx0 ≠ ∅ ∧ lspmx0 ⊆ gs.gspmx) ∧ a = chooseL2(lspmx0)) ∨ a = τ ∧ ¬(∃ lspmx0. lspmx0 ≠ ∅ ∧ lspmx0 ⊆ gs.gspmx); ⊦ disjointp(spmx1, spmx2) → (spmx1 ∪ spmx2 ⊆ spmx ↔ spmx1 ⊆ spmx ∧ spmx2 ⊆ spmx); (ws)

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 4:

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

• Proof step 5:

  # y = r, y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(r, # x) * x = spmx.toMatrix(r, # x) * x, ghostlspmxf(ls.tid) = ∅, gs = mkgs(spmx, gspmx, r, x, y, ghostlspmxf), ls.tid ≠ tid0, alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, r, # x), gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx0 ≠ ∅ ∧ lspmx0 ⊆ gspmx ∧ a = chooseL2(lspmx0) ∨ a = τ ∧ ¬(∃ lspmx0. lspmx0 ≠ ∅ ∧ lspmx0 ⊆ gspmx) ⊦ ∃ lspmx0. a = chooseL2(lspmx0), ghostlspmxf(tid0) = gstepf(gs, ls, L2, a).ghostlspmxf(tid0) ∧ gstepf(gs, ls, L2, a).gspmx ⊆ gspmx

Rule argument

Additional information

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

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

Lemma elim-03

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(ls.tid) = ∅, ls.tid ≠ tid0, alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx0 ≠ ∅ ∧ lspmx0 ⊆ gspmx ∧ a = chooseL2(lspmx0) ∨ a = τ ∧ ¬(∃ lspmx0. lspmx0 ≠ ∅ ∧ lspmx0 ⊆ gspmx) ⊦ ∃ lspmx0. a = chooseL2(lspmx0), ghostlspmxf(tid0) = gstepf(mkgs(spmx, gspmx, # y, x, y, ghostlspmxf), ls, L2, a).ghostlspmxf(tid0) ∧ gstepf(mkgs(spmx, gspmx, # y, x, y, ghostlspmxf), ls, L2, a).gspmx ⊆ gspmx

Rule argument

Additional information

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 7:

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

• Proof step 8:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid) = ∅, ls = mkls(tid, lspmx, np, val), tid ≠ tid0, alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx0 ≠ ∅ ∧ lspmx0 ⊆ gspmx ∧ a = chooseL2(lspmx0) ∨ a = τ ∧ ¬(∃ lspmx0. lspmx0 ≠ ∅ ∧ lspmx0 ⊆ gspmx) ⊦ ∃ lspmx0. a = chooseL2(lspmx0), ghostlspmxf(tid0) = gstepf(mkgs(spmx, gspmx, # y, x, y, ghostlspmxf), ls, L2, a).ghostlspmxf(tid0) ∧ gstepf(mkgs(spmx, gspmx, # y, x, y, ghostlspmxf), ls, L2, a).gspmx ⊆ gspmx

Rule argument

Additional information

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

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

Lemma elim-02

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid) = ∅, tid ≠ tid0, alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, lspmx0 ≠ ∅ ∧ lspmx0 ⊆ gspmx ∧ a = chooseL2(lspmx0) ∨ a = τ ∧ ¬(∃ lspmx0. lspmx0 ≠ ∅ ∧ lspmx0 ⊆ gspmx) ⊦ ∃ lspmx0. a = chooseL2(lspmx0), ghostlspmxf(tid0) = gstepf(mkgs(spmx, gspmx, # y, x, y, ghostlspmxf), mkls(tid, lspmx, np, val), L2, a).ghostlspmxf(tid0) ∧ gstepf(mkgs(spmx, gspmx, # y, x, y, ghostlspmxf), mkls(tid, lspmx, np, val), L2, a).gspmx ⊆ gspmx

Rule argument

Additional information

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 10:

  ⊦ ((((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 11:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, ghostlspmxf(tid) = ∅, gstepf(mkgs(spmx, gspmx, # y, x, y, ghostlspmxf), mkls(tid, lspmx, np, val), L2, a) = mkgs(spmx0, gspmx0, r, x0, y0, ghostlspmxf0), tid ≠ tid0, alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, lspmx0 ≠ ∅ ∧ lspmx0 ⊆ gspmx ∧ a = chooseL2(lspmx0) ∨ a = τ ∧ ¬(∃ lspmx0. lspmx0 ≠ ∅ ∧ lspmx0 ⊆ gspmx) ⊦ ∃ lspmx0. a = chooseL2(lspmx0), ghostlspmxf(tid0) = ghostlspmxf0(tid0) ∧ gspmx0 ⊆ gspmx

Rule argument

Additional information

Used terms: y0, gstepf(mkgs(spmx, gspmx, # y, x, y, ghostlspmxf), mkls(tid, lspmx, np, val), L2, a), gspmx0, ghostlspmxf0, spmx0, r, x0

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

Lemma elim-03

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

User applied rule case distinction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: gstepf-L2-1: ⊦ gstepf(gs, ls, L2, chooseL2(lspmx0)) = (gs.gspmx:= (gs.gspmx \ dom (ls.lspmx:= lspmx0).lspmx)) .ghostlspmxf:= gs.ghostlspmxf((ls.lspmx:= lspmx0).tid; (ls.lspmx:= lspmx0).lspmx); sel-12: ⊦ mkgs(spmx, spmx0, r, x, x0, ghostlspmxf).gspmx = spmx0; upd-08: ⊦ mkgs(spmx, spmx0, r, x, x0, ghostlspmxf).gspmx:= spmx2 = mkgs(spmx, spmx2, r, x, x0, ghostlspmxf); sel-16: ⊦ mkgs(spmx, spmx0, r, x, x0, ghostlspmxf).ghostlspmxf = ghostlspmxf; sel-08: ⊦ mkls(tid, lspmx, np, val).tid = tid; upd-05: ⊦ mkls(tid, lspmx, np, val).lspmx:= lspmx0 = mkls(tid, lspmx0, np, val); sel-09: ⊦ mkls(tid, lspmx, np, val).lspmx = lspmx; upd-12: ⊦ mkgs(spmx, spmx0, r, x, x0, ghostlspmxf).ghostlspmxf:= ghostlspmxf0 = mkgs(spmx, spmx0, r, x, x0, ghostlspmxf0); inj-07: ⊦ mkgs(spmx, spmx0, r, x, x0, ghostlspmxf) = mkgs(spmx1, spmx2, r0, x1, x2, ghostlspmxf0) ↔ spmx = spmx1 ∧ spmx0 = spmx2 ∧ r = r0 ∧ x = x1 ∧ x0 = x2 ∧ ghostlspmxf = ghostlspmxf0; inj-04: ⊦ chooseL2(lspmx) = chooseL2(lspmx0) ↔ lspmx = lspmx0; gstepf-L2-0: ⊦ gstepf(gs, ls, L2, τ) = gs; inj-07: ⊦ mkgs(spmx, spmx0, r, x, x0, ghostlspmxf) = mkgs(spmx1, spmx2, r0, x1, x2, ghostlspmxf0) ↔ spmx = spmx1 ∧ spmx0 = spmx2 ∧ r = r0 ∧ x = x1 ∧ x0 = x2 ∧ ghostlspmxf = ghostlspmxf0; disj-07: ⊦ τ ≠ chooseL2(lspmx); ⊦ st ⊆ st; (s)