Proof step 1 from proof step-L4-L0 (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, L4, a) = L0, ls.lspmx ≠ ∅, alldisjointp(alltids, gs.ghostlspmxf), disjointp(U(alltids, gs.ghostlspmxf), gs.gspmx), okspmx(gs.spmx, gs.r, # gs.x), pre(gs, ls, L4, a), U(alltids, gs.ghostlspmxf) ∪ gs.gspmx ⊆ gs.spmx ⊦

Rule argument

Additional information

Proof step 2 from proof step-L4-L0 (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.lspmx ≠ ∅, 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, np0 ∈ ls.lspmx ∧ a = chooseL4(np0) ∨ a = τ ∧ ¬(∃ np0. np0 ∈ ls.lspmx) ⊦ ∃ np0. a = chooseL4(np0)

Rule argument

Additional information

Used simplifier rules: pcstepf-L4: ⊦ pcstepf(gs, ls, L4, a) = (∃ np0. a = chooseL4(np0) ⊃ L5;L0); disj-26: ⊦ L5 ≠ L0; pre-L4: ⊦ pre(gs, ls, L4, a) ↔ (∃ np0. np0 ∈ ls.lspmx ∧ a = chooseL4(np0)) ∨ a = τ ∧ ¬(∃ np0. np0 ∈ ls.lspmx); ⊦ disjointp(spmx1, spmx2) → (spmx1 ∪ spmx2 ⊆ spmx ↔ spmx1 ⊆ spmx ∧ spmx2 ⊆ spmx); (ws)

Proof step 3 from proof step-L4-L0 (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) = ls.lspmx, gs = mkgs(spmx, gspmx, r, x, y, ghostlspmxf), ls.lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, r, # x), gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, np0 ∈ ls.lspmx ∧ a = chooseL4(np0) ∨ a = τ ∧ ¬(∃ np0. np0 ∈ ls.lspmx) ⊦ ∃ np0. a = chooseL4(np0)

Rule argument

Additional information

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

Proof step 4 from proof step-L4-L0 (previous step) (back to tree)

Lemma elim-03

Proof step 5 from proof step-L4-L0 (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.lspmx, ls.lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, np0 ∈ ls.lspmx ∧ a = chooseL4(np0) ∨ a = τ ∧ ¬(∃ np0. np0 ∈ ls.lspmx) ⊦ ∃ np0. a = chooseL4(np0)

Rule argument

Additional information

Proof step 6 from proof step-L4-L0 (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), lspmx ≠ ∅, alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, np0 ∈ lspmx ∧ a = chooseL4(np0) ∨ a = τ ∧ ¬(∃ np0. np0 ∈ lspmx) ⊦ ∃ np0. a = chooseL4(np0)

Rule argument

Additional information

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

Proof step 7 from proof step-L4-L0 (previous step) (back to tree)

Lemma elim-02

Proof step 8 from proof step-L4-L0 (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) ≠ ∅, alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx, np0 ∈ ghostlspmxf(tid) ∧ a = chooseL4(np0) ∨ a = τ ∧ ¬(∃ np0. np0 ∈ ghostlspmxf(tid)) ⊦ ∃ np0. a = chooseL4(np0)

Rule argument

Additional information

Proof step 9 from proof step-L4-L0 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 10:

  y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(# y, # x) * x = spmx.toMatrix(# y, # x) * x, a = τ, ghostlspmxf(tid) ≠ ∅, alldisjointp(alltids, ghostlspmxf), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx ⊦ ∃ np0. a = chooseL4(np0), ∃ np0. np0 ∈ ghostlspmxf(tid)

Rule argument

Additional information

Used simplifier rules: inj-03: ⊦ chooseL4(np) = chooseL4(np0) ↔ np = np0;

Proof step 10 from proof step-L4-L0 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

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

Rule argument

Additional information

Used simplifier rules: disj-08: ⊦ τ ≠ chooseL4(np);

Proof step 11 from proof step-L4-L0 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

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

• Proof step 13:

  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), gspmx ⊆ spmx, U(alltids, ghostlspmxf) ⊆ spmx, ∃ np. ¬((np ∈ ghostlspmxf(tid) ↔ np ∈ ∅) ∧ ghostlspmxf(tid)[np] = ∅[np]) ⊦ ∃ np0. np0 ∈ ghostlspmxf(tid)

Rule argument

Additional information

Used terms: ghostlspmxf(tid), ∅

Proof step 12 from proof step-L4-L0 (previous step) (back to tree)

A spec-lemma

Proof step 13 from proof step-L4-L0 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

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), disjointp(U(alltids, ghostlspmxf), gspmx), okspmx(spmx, # y, # x), np ∈ ghostlspmxf(tid), U(alltids, ghostlspmxf) ⊆ spmx, gspmx ⊆ spmx ⊦ ∃ np0. np0 ∈ ghostlspmxf(tid)

Rule argument

Additional information

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

Proof step 14 from proof step-L4-L0 (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: np