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

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And closed the goal!

Rule argument

Additional information

Used simplifier rules: pcstepf-L5: ⊦ pcstepf(gs, ls, L5, a) = L6; pre-L5: ⊦ pre(gs, ls, L5, a) ↔ a = τ; updsel-57: ⊦ (ls.val:= val).np = ls.np; updsel-55: ⊦ (ls.val:= val).tid = ls.tid; gstepf-L5: ⊦ gstepf(gs, ls, L5, τ) = gs; lstepf-L5: ⊦ lstepf(gs, ls, L5, τ) = ls.val:= gs.y[ls.np.r]; updsel-56: ⊦ (ls.val:= val).lspmx = ls.lspmx; ⊦ disjointp(spmx1, spmx2) → (spmx1 ∪ spmx2 ⊆ spmx ↔ spmx1 ⊆ spmx ∧ spmx2 ⊆ spmx); (ws)