Proof step 1 from proof init (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  gspmx = spmx, y = mkvector(r), okspmx(spmx, r, # x), ∀ tid. ghostlspmxf(tid) = ∅ ⊦ alldisjointp(alltids, ghostlspmxf) ∧ disjointp(U(alltids, ghostlspmxf), gspmx) ∧ y + (U(alltids, ghostlspmxf) ∪ gspmx).toMatrix(r, # x) * x = spmx.toMatrix(r, # x) * x ∧ U(alltids, ghostlspmxf) ∪ gspmx ⊆ spmx ∧ # y = r ∧ okspmx(spmx, r, # x)

Rule argument

Additional information

Proof step 2 from proof init (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  okspmx(spmx, r, # x), ∀ tid. ghostlspmxf(tid) = ∅ ⊦ alldisjointp(alltids, ghostlspmxf) ∧ disjointp(U(alltids, ghostlspmxf), spmx) ∧ mkvector(r) + (U(alltids, ghostlspmxf) ∪ spmx).toMatrix(r, # x) * x = spmx.toMatrix(r, # x) * x ∧ U(alltids, ghostlspmxf) ∪ spmx ⊆ spmx

Rule argument

Additional information

Used simplifier rules: ⊦ # mkvector(n) = n; (s)

Proof step 3 from proof init (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 4:

  alldisjointp(alltids, ghostlspmxf), okspmx(spmx, r, # x), ∀ tid. ghostlspmxf(tid) = ∅ ⊦ alldisjointp(alltids, ghostlspmxf) ∧ disjointp(U(alltids, ghostlspmxf), spmx) ∧ mkvector(r) + (U(alltids, ghostlspmxf) ∪ spmx).toMatrix(r, # x) * x = spmx.toMatrix(r, # x) * x ∧ U(alltids, ghostlspmxf) ∪ spmx ⊆ spmx

• Proof step 18:

  okspmx(spmx, r, # x), ¬ alldisjointp(alltids, ghostlspmxf), ∀ tid. ghostlspmxf(tid) = ∅ ⊦ alldisjointp(alltids, ghostlspmxf) ∧ disjointp(U(alltids, ghostlspmxf), spmx) ∧ mkvector(r) + (U(alltids, ghostlspmxf) ∪ spmx).toMatrix(r, # x) * x = spmx.toMatrix(r, # x) * x ∧ U(alltids, ghostlspmxf) ∪ spmx ⊆ spmx

Rule argument

Additional information

Used formulas: alldisjointp(alltids, ghostlspmxf)

Proof step 4 from proof init (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  alldisjointp(alltids, ghostlspmxf), okspmx(spmx, r, # x), ∀ tid. ghostlspmxf(tid) = ∅ ⊦ disjointp(U(alltids, ghostlspmxf), spmx) ∧ mkvector(r) + (U(alltids, ghostlspmxf) ∪ spmx).toMatrix(r, # x) * x = spmx.toMatrix(r, # x) * x ∧ U(alltids, ghostlspmxf) ∪ spmx ⊆ spmx

Rule argument

Additional information

Proof step 5 from proof init (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 6:

  U(alltids, ghostlspmxf) = ∅, alldisjointp(alltids, ghostlspmxf), okspmx(spmx, r, # x), ∀ tid. ghostlspmxf(tid) = ∅ ⊦ disjointp(U(alltids, ghostlspmxf), spmx) ∧ mkvector(r) + (U(alltids, ghostlspmxf) ∪ spmx).toMatrix(r, # x) * x = spmx.toMatrix(r, # x) * x ∧ U(alltids, ghostlspmxf) ∪ spmx ⊆ spmx

• Proof step 11:

  U(alltids, ghostlspmxf) ≠ ∅, alldisjointp(alltids, ghostlspmxf), okspmx(spmx, r, # x), ∀ tid. ghostlspmxf(tid) = ∅ ⊦ disjointp(U(alltids, ghostlspmxf), spmx) ∧ mkvector(r) + (U(alltids, ghostlspmxf) ∪ spmx).toMatrix(r, # x) * x = spmx.toMatrix(r, # x) * x ∧ U(alltids, ghostlspmxf) ∪ spmx ⊆ spmx

Rule argument

Additional information

Used formulas: U(alltids, ghostlspmxf) = ∅

Proof step 6 from proof init (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  U(alltids, ghostlspmxf) = ∅, mkvector(r) + spmx.toMatrix(r, # x) * x ≠ spmx.toMatrix(r, # x) * x, alldisjointp(alltids, ghostlspmxf), okspmx(spmx, r, # x), ∀ tid. ghostlspmxf(tid) = ∅ ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ st ⊆ st; (s) ⊦ ∅ ∪ spmx = spmx; (s) ⊦ disjointp(∅, spmx1); (s)

Proof step 7 from proof init (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

  ⊦ # x = n → mkvector(n) + x = x

• Proof step 9:

  U(alltids, ghostlspmxf) = ∅, #(spmx.toMatrix(r, # x) * x) ≠ r, mkvector(r) + spmx.toMatrix(r, # x) * x ≠ spmx.toMatrix(r, # x) * x, alldisjointp(alltids, ghostlspmxf), okspmx(spmx, r, # x), ∀ tid. ghostlspmxf(tid) = ∅ ⊦

Rule argument

Additional information

Used terms: r, spmx.toMatrix(r, # x) * x

Proof step 8 from proof init (previous step) (back to tree)

A spec-lemma

Proof step 9 from proof init (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ #c mx = # vec → #(mx * vec) = #r mx

Rule argument

Additional information

Used simplifier rules: ⊦ #c spmx.toMatrix(r, c) = c; (s) ⊦ #r spmx.toMatrix(r, c) = r; (s) Used terms: spmx.toMatrix(r, # x), x

Proof step 10 from proof init (previous step) (back to tree)

A spec-lemma

Proof step 11 from proof init (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:

  alldisjointp(alltids, ghostlspmxf), okspmx(spmx, r, # x), ∀ tid. ghostlspmxf(tid) = ∅, ∃ np. ¬((np ∈ U(alltids, ghostlspmxf) ↔ np ∈ ∅) ∧ U(alltids, ghostlspmxf)[np] = ∅[np]) ⊦ disjointp(U(alltids, ghostlspmxf), spmx) ∧ mkvector(r) + (U(alltids, ghostlspmxf) ∪ spmx).toMatrix(r, # x) * x = spmx.toMatrix(r, # x) * x ∧ U(alltids, ghostlspmxf) ∪ spmx ⊆ spmx

Rule argument

Additional information

Used terms: U(alltids, ghostlspmxf), ∅

Proof step 12 from proof init (previous step) (back to tree)

A spec-lemma

Proof step 13 from proof init (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  alldisjointp(alltids, ghostlspmxf), okspmx(spmx, r, # x), np ∈ U(alltids, ghostlspmxf), ∀ tid. ghostlspmxf(tid) = ∅ ⊦ disjointp(U(alltids, ghostlspmxf), spmx) ∧ mkvector(r) + (U(alltids, ghostlspmxf) ∪ spmx).toMatrix(r, # x) * x = spmx.toMatrix(r, # x) * x ∧ U(alltids, ghostlspmxf) ∪ spmx ⊆ spmx

Rule argument

Additional information

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

Proof step 14 from proof init (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

  ⊦ alldisjointp(ts, f) → (np ∈ U(ts, f) ↔ (∃ tid. tid ∈ ts ∧ np ∈ f(tid)))

• Proof step 16:

  alldisjointp(alltids, ghostlspmxf), okspmx(spmx, r, # x), ∀ tid. ghostlspmxf(tid) = ∅, ∃ tid. tid ∈ alltids ∧ np ∈ ghostlspmxf(tid) ⊦ disjointp(U(alltids, ghostlspmxf), spmx) ∧ mkvector(r) + (U(alltids, ghostlspmxf) ∪ spmx).toMatrix(r, # x) * x = spmx.toMatrix(r, # x) * x ∧ U(alltids, ghostlspmxf) ∪ spmx ⊆ spmx

Rule argument

Additional information

Used terms: np, alltids, ghostlspmxf

Proof step 15 from proof init (previous step) (back to tree)

A spec-lemma

Proof step 16 from proof init (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  alldisjointp(alltids, ghostlspmxf), okspmx(spmx, r, # x), np ∈ ghostlspmxf(tid), ∀ tid. ghostlspmxf(tid) = ∅ ⊦ disjointp(U(alltids, ghostlspmxf), spmx) ∧ mkvector(r) + (U(alltids, ghostlspmxf) ∪ spmx).toMatrix(r, # x) * x = spmx.toMatrix(r, # x) * x ∧ U(alltids, ghostlspmxf) ∪ spmx ⊆ spmx

Rule argument

Additional information

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

Proof step 17 from proof init (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

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

Proof step 18 from proof init (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  okspmx(spmx, r, # x), ¬ alldisjointp(alltids, ghostlspmxf), ∀ tid. ghostlspmxf(tid) = ∅ ⊦

Rule argument

Additional information

Proof step 19 from proof init (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

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

• Proof step 21:

  okspmx(spmx, r, # x), ∀ tid. ghostlspmxf(tid) = ∅, ∃ tid1, tid2, np. ¬(tid1 ∈ alltids ∧ tid2 ∈ alltids ∧ np ∈ ghostlspmxf(tid1) ∧ tid1 ≠ tid2 → ¬ np ∈ ghostlspmxf(tid2)) ⊦

Rule argument

Additional information

Used terms: alltids, ghostlspmxf

Proof step 20 from proof init (previous step) (back to tree)

A spec-lemma

Proof step 21 from proof init (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  tid1 ≠ tid2, okspmx(spmx, r, # x), np ∈ ghostlspmxf(tid2), np ∈ ghostlspmxf(tid1), ∀ tid. ghostlspmxf(tid) = ∅ ⊦

Rule argument

Additional information

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

Proof step 22 from proof init (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

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