Proof step 1 from proof rely-L2-L3 (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) = L3, 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-L3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And closed the goal!

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); inj-04: ⊦ chooseL2(lspmx) = chooseL2(lspmx0) ↔ lspmx = lspmx0; disj-07: ⊦ τ ≠ chooseL2(lspmx); updsel-54: ⊦ (gs.ghostlspmxf:= ghostlspmxf).ghostlspmxf = ghostlspmxf; 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); updsel-11: ⊦ (ls.lspmx:= lspmx).tid = ls.tid; updsel-14: ⊦ (ls.lspmx:= lspmx).lspmx = lspmx; updsel-30: ⊦ (gs.ghostlspmxf:= ghostlspmxf).gspmx = gs.gspmx; updsel-26: ⊦ (gs.gspmx:= spmx0).gspmx = spmx0; ⊦ st \ s ⊆ st; (s) ⊦ disjointp(spmx1, spmx2) → (spmx1 ∪ spmx2 ⊆ spmx ↔ spmx1 ⊆ spmx ∧ spmx2 ⊆ spmx); (ws)