Proof step 1 from proof step-invWrite-resWrite (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  gs.pm = ∅ ⊕ (gs.h | true), gs.vm = ∅ ⊕ gs.h, pcstepf(gs, ls, invWrite, a) = resWrite, allReadsOK(gs.h), allWritesOK(gs.h), pre(gs, ls, invWrite, a) ⊦ ( allReadsOK(gstepf(gs, ls, invWrite, a).h) ∧ allWritesOK(gstepf(gs, ls, invWrite, a).h) ∧ gstepf(gs, ls, invWrite, a).vm = ∅ ⊕ gstepf(gs, ls, invWrite, a).h ∧ gstepf(gs, ls, invWrite, a).pm = ∅ ⊕ (gstepf(gs, ls, invWrite, a).h | true)) ∧ ( (gstepf(gs, ls, invWrite, a).h | lstepf(gs, ls, invWrite, a).t) | false = [] ∨ (gstepf(gs, ls, invWrite, a).h | lstepf(gs, ls, invWrite, a).t) | false = (W(lstepf(gs, ls, invWrite, a).t, lstepf(gs, ls, invWrite, a).il, lstepf(gs, ls, invWrite, a).iv), false) ')

Rule argument

Additional information

Proof step 2 from proof step-invWrite-resWrite (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And closed the goal!

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ' = x + a0 ' ↔ a = a0 ∧ x = []; (ws) ⊦ ls.t = t → lstepf(gs, ls, invWrite, ADoWrite(t)) = ls; (s) ⊦ h + (e, false) ' | false = (h | false) + (e, false) '; (s) ⊦ W(t, l, v).t = t; (s) ⊦ (e, b) ' | t = (t = e.t ⊃ (e, b) ';[]); (s) ⊦ h + h0 | t = (h | t) + (h0 | t); (s) ⊦ (gs.h:= h).h = h; (s) ⊦ x + a = x + a '; (s) ⊦ ls.t = t → gstepf(gs, ls, invWrite, ADoWrite(t)) = (gs.vm:= gs.vm(ls.il := ls.iv)).h:= (gs.h + (W(ls.t, ls.il, ls.iv), false)); (s) ⊦ a ' ≠ []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ h + (e, false) ' | true = h | true; (s) ⊦ (gs.vm:= vm).pm = gs.pm; (s) ⊦ (gs.h:= h).pm = gs.pm; (s) ⊦ mem ⊕ (h + (W(t, l, v), b) ') = (mem ⊕ h)(l := v); (s) ⊦ (gs.vm:= vm).vm = vm; (s) ⊦ (gs.h:= h).vm = gs.vm; (s) ⊦ (h | t) | false = [] ∧ allWritesOK(h) → allWritesOK(h + (W(t, l, v), false) '); (ss) ⊦ allReadsOK(h) → allReadsOK(h + (W(t, l, v), false) '); (ss) ⊦ ls.t = t → pcstepf(gs, ls, invWrite, ADoWrite(t)) = resWrite; (s) ⊦ pre(gs, ls, invWrite, a) ↔ a = ADoWrite(ls.t) ∧ (gs.h | ls.t) | false = []; (s)