Proof step 1 from proof stable-L4 (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  # gs.y = gs.r, # gs0.y = gs0.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, gs0.y + (U(alltids, gs0.ghostlspmxf) ∪ gs0.gspmx).toMatrix(gs0.r, # gs0.x) * gs0.x = gs0.spmx.toMatrix(gs0.r, # gs0.x) * gs0.x, gs.ghostlspmxf(ls.tid) = ls.lspmx, gs.ghostlspmxf(ls.tid) = gs0.ghostlspmxf(ls.tid), ls.lspmx ≠ ∅, alldisjointp(alltids, gs.ghostlspmxf), alldisjointp(alltids, gs0.ghostlspmxf), disjointp(U(alltids, gs.ghostlspmxf), gs.gspmx), disjointp(U(alltids, gs0.ghostlspmxf), gs0.gspmx), okspmx(gs.spmx, gs.r, # gs.x), okspmx(gs0.spmx, gs0.r, # gs0.x), U(alltids, gs.ghostlspmxf) ∪ gs.gspmx ⊆ gs.spmx, U(alltids, gs0.ghostlspmxf) ∪ gs0.gspmx ⊆ gs0.spmx, gs0.gspmx ⊆ gs.gspmx ⊦ ls.lspmx ≠ ∅ ∧ gs0.ghostlspmxf(ls.tid) = ls.lspmx

Rule argument

Additional information

Proof step 2 from proof stable-L4 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And closed the goal!

Rule argument

Additional information

Used simplifier rules: sub-trans: ⊦ st ⊆ st0 ∧ st0 ⊆ st1 → st ⊆ st1; (forward) from specification store[sparsearray] ⊦ disjointp(spmx1, spmx2) → (spmx1 ∪ spmx2 ⊆ spmx ↔ spmx1 ⊆ spmx ∧ spmx2 ⊆ spmx); (ws)