Proof step 1 from proof rely-L6-L7 (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, L6, a) = L7, ls.tid ≠ tid0, alldisjointp(alltids, gs.ghostlspmxf), disjointp(U(alltids, gs.ghostlspmxf), gs.gspmx), okspmx(gs.spmx, gs.r, # gs.x), pre(gs, ls, L6, a), ls.np ∈ ls.lspmx, U(alltids, gs.ghostlspmxf) ∪ gs.gspmx ⊆ gs.spmx ⊦ gs.ghostlspmxf(tid0) = gstepf(gs, ls, L6, a).ghostlspmxf(tid0) ∧ gstepf(gs, ls, L6, a).gspmx ⊆ gs.gspmx

Rule argument

Additional information

Proof step 2 from proof rely-L6-L7 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And closed the goal!

Rule argument

Additional information

Used simplifier rules: pcstepf-L6: ⊦ pcstepf(gs, ls, L6, a) = (ls.val = gs.y[ls.np.r] ⊃ L7;L3); disj-16: ⊦ L3 ≠ L7; pre-L6: ⊦ pre(gs, ls, L6, a) ↔ a = τ; updsel-54: ⊦ (gs.ghostlspmxf:= ghostlspmxf).ghostlspmxf = ghostlspmxf; gstepf-L6: ⊦ gstepf(gs, ls, L6, a) = (ls.val = gs.y[ls.np.r] ⊃ (gs.y:= gs.y[ls.np.r, ls.val + ls.lspmx[ls.np] * gs.x[ls.np.c]]) .ghostlspmxf:= gs.ghostlspmxf(ls.tid; gs.ghostlspmxf(ls.tid) -- ls.np) ;gs ); updsel-30: ⊦ (gs.ghostlspmxf:= ghostlspmxf).gspmx = gs.gspmx; updsel-29: ⊦ (gs.y:= x0).gspmx = gs.gspmx; ⊦ st ⊆ st; (s) ⊦ disjointp(spmx1, spmx2) → (spmx1 ∪ spmx2 ⊆ spmx ↔ spmx1 ⊆ spmx ∧ spmx2 ⊆ spmx); (ws)