Proof step 1 from proof plibStep-lem (conclusion) (back to tree)

⊦ plibStep(mkstate(gs, lsf, pcf), a, mkstate(gs0, lsf0, pcf0)) ↔ (∃ t, ls, pc. lstep(gs, lsf(t), pcf(t), a, gs0, ls, pc) ∧ lsf0 = lsf(t := ls) ∧ pcf0 = pcf(t := pc)) ∨ a = globalACrash ∧ gs0 = mkPLIBgs(gs.pm, gs.pm, gs.h | true) ∧ lsf0 = lsf ∧ pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed)) ∨ (∃ l. a = globalAPersist(l) ∧ firstVolWrite(l, gs.h) < # gs.h ∧ gs0 = (gs.pm:= gs.pm(l := gs.h[firstVolWrite(l, gs.h)]._1.v)) .h:= ( gs.h.take(firstVolWrite(l, gs.h)) + ((gs.h[firstVolWrite(l, gs.h)]._1, true) + persistDependentReads(l, gs.h.drop(firstVolWrite(l, gs.h) + 1)))) ∧ lsf0 = lsf ∧ pcf0 = pcf)

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 2:
⊦ plibStep(mkstate(gs, lsf, pcf), a, mkstate(gs0, lsf0, pcf0)) ↔ (∃ t, ls, pc. lstep(gs, lsf(t), pcf(t), a, gs0, ls, pc) ∧ lsf0 = lsf(t := ls) ∧ pcf0 = pcf(t := pc)) ∨ a = globalACrash ∧ ⟨pm := gs.pm, vm := gs.vm, h := gs.h; ACrash(pm; vm, h, pcf); gs := (gs.vm:= vm).h:= h⟩ (gs0 = gs ∧ lsf0 = lsf ∧ pcf0 = pcf) ∨ (∃ l. a = globalAPersist(l) ∧ firstVolWrite(l, gs.h) < # gs.h ∧ gs0 = (gs.pm:= gs.pm(l := gs.h[firstVolWrite(l, gs.h)]._1.v)) .h:= ( gs.h.take(firstVolWrite(l, gs.h)) + ((gs.h[firstVolWrite(l, gs.h)]._1, true) + persistDependentReads(l, gs.h.drop(firstVolWrite(l, gs.h) + 1)))) ∧ lsf0 = lsf ∧ pcf0 = pcf)
Proof step 3:
⊦ (∃ t, ls, pc. lstep(gs, lsf(t), pcf(t), a, gs0, ls, pc) ∧ lsf0 = lsf(t := ls) ∧ pcf0 = pcf(t := pc)) ∨ a = globalACrash ∧ ⟨pm := gs.pm, vm := gs.vm, h := gs.h; ACrash(pm; vm, h, pcf); gs := (gs.vm:= vm).h:= h⟩ (gs0 = gs ∧ lsf0 = lsf ∧ pcf0 = pcf) ∨ (∃ l. a = globalAPersist(l) ∧ firstVolWrite(l, gs.h) < # gs.h ∧ gs0 = (gs.pm:= gs.pm(l := gs.h[firstVolWrite(l, gs.h)]._1.v)) .h:= ( gs.h.take(firstVolWrite(l, gs.h)) + ((gs.h[firstVolWrite(l, gs.h)]._1, true) + persistDependentReads(l, gs.h.drop(firstVolWrite(l, gs.h) + 1)))) ∧ lsf0 = lsf ∧ pcf0 = pcf) ↔ (∃ t, ls, pc. lstep(gs, lsf(t), pcf(t), a, gs0, ls, pc) ∧ lsf0 = lsf(t := ls) ∧ pcf0 = pcf(t := pc)) ∨ a = globalACrash ∧ gs0 = mkPLIBgs(gs.pm, gs.pm, gs.h | true) ∧ lsf0 = lsf ∧ pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed)) ∨ (∃ l. a = globalAPersist(l) ∧ firstVolWrite(l, gs.h) < # gs.h ∧ gs0 = (gs.pm:= gs.pm(l := gs.h[firstVolWrite(l, gs.h)]._1.v)) .h:= ( gs.h.take(firstVolWrite(l, gs.h)) + ((gs.h[firstVolWrite(l, gs.h)]._1, true) + persistDependentReads(l, gs.h.drop(firstVolWrite(l, gs.h) + 1)))) ∧ lsf0 = lsf ∧ pcf0 = pcf)

Rule argument

spec: <toplevel>, name:plibStep, seq:⊦ plibStep(mkstate(gs, lsf, pcf), a, mkstate(gs0, lsf0, pcf0)) ↔ (∃ t, ls, pc. lstep(gs, lsf(t), pcf(t), a, gs0, ls, pc) ∧ lsf0 = lsf(t := ls) ∧ pcf0 = pcf(t := pc)) ∨ a = globalACrash ∧ ⟨pm := gs.pm, vm := gs.vm, h := gs.h; ACrash(pm; vm, h, pcf); gs := (gs.vm:= vm).h:= h⟩ (gs0 = gs ∧ lsf0 = lsf ∧ pcf0 = pcf) ∨ (∃ l. a = globalAPersist(l) ∧ firstVolWrite(l, gs.h) < # gs.h ∧ gs0 = (gs.pm:= gs.pm(l := gs.h[firstVolWrite(l, gs.h)]._1.v)) .h:= ( gs.h.take(firstVolWrite(l, gs.h)) + ( (gs.h[firstVolWrite(l, gs.h)]._1, true) + persistDependentReads (l, gs.h.drop(firstVolWrite(l, gs.h) + 1)))) ∧ lsf0 = lsf ∧ pcf0 = pcf), subst:[pcf, lsf0, lsf, gs, pcf0, a, gs0] → [pcf, lsf0, lsf, gs, pcf0, a, gs0], <all paths>

Additional information

Used terms: pcf0, gs0, lsf0, pcf, lsf, gs, a

Proof step 2 from proof plibStep-lem (previous step) (back to tree)

⊦ plibStep(mkstate(gs, lsf, pcf), a, mkstate(gs0, lsf0, pcf0)) ↔ (∃ t, ls, pc. lstep(gs, lsf(t), pcf(t), a, gs0, ls, pc) ∧ lsf0 = lsf(t := ls) ∧ pcf0 = pcf(t := pc)) ∨ a = globalACrash ∧ ⟨pm := gs.pm, vm := gs.vm, h := gs.h; ACrash(pm; vm, h, pcf); gs := (gs.vm:= vm).h:= h⟩ (gs0 = gs ∧ lsf0 = lsf ∧ pcf0 = pcf) ∨ (∃ l. a = globalAPersist(l) ∧ firstVolWrite(l, gs.h) < # gs.h ∧ gs0 = (gs.pm:= gs.pm(l := gs.h[firstVolWrite(l, gs.h)]._1.v)) .h:= ( gs.h.take(firstVolWrite(l, gs.h)) + ((gs.h[firstVolWrite(l, gs.h)]._1, true) + persistDependentReads(l, gs.h.drop(firstVolWrite(l, gs.h) + 1)))) ∧ lsf0 = lsf ∧ pcf0 = pcf)

Lemma plibStep

Proof step 3 from proof plibStep-lem (previous step) (back to tree)

⊦ (∃ t, ls, pc. lstep(gs, lsf(t), pcf(t), a, gs0, ls, pc) ∧ lsf0 = lsf(t := ls) ∧ pcf0 = pcf(t := pc)) ∨ a = globalACrash ∧ ⟨pm := gs.pm, vm := gs.vm, h := gs.h; ACrash(pm; vm, h, pcf); gs := (gs.vm:= vm).h:= h⟩ (gs0 = gs ∧ lsf0 = lsf ∧ pcf0 = pcf) ∨ (∃ l. a = globalAPersist(l) ∧ firstVolWrite(l, gs.h) < # gs.h ∧ gs0 = (gs.pm:= gs.pm(l := gs.h[firstVolWrite(l, gs.h)]._1.v)) .h:= ( gs.h.take(firstVolWrite(l, gs.h)) + ((gs.h[firstVolWrite(l, gs.h)]._1, true) + persistDependentReads(l, gs.h.drop(firstVolWrite(l, gs.h) + 1)))) ∧ lsf0 = lsf ∧ pcf0 = pcf) ↔ (∃ t, ls, pc. lstep(gs, lsf(t), pcf(t), a, gs0, ls, pc) ∧ lsf0 = lsf(t := ls) ∧ pcf0 = pcf(t := pc)) ∨ a = globalACrash ∧ gs0 = mkPLIBgs(gs.pm, gs.pm, gs.h | true) ∧ lsf0 = lsf ∧ pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed)) ∨ (∃ l. a = globalAPersist(l) ∧ firstVolWrite(l, gs.h) < # gs.h ∧ gs0 = (gs.pm:= gs.pm(l := gs.h[firstVolWrite(l, gs.h)]._1.v)) .h:= ( gs.h.take(firstVolWrite(l, gs.h)) + ((gs.h[firstVolWrite(l, gs.h)]._1, true) + persistDependentReads(l, gs.h.drop(firstVolWrite(l, gs.h) + 1)))) ∧ lsf0 = lsf ∧ pcf0 = pcf)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 4:
⊦ ⟨pm := gs.pm, vm := gs.vm, h := gs.h; ACrash(pm; vm, h, pcf); gs := (gs.vm:= vm).h:= h⟩ (gs0 = gs ∧ lsf0 = lsf ∧ pcf0 = pcf) ↔ gs0 = mkPLIBgs(gs.pm, gs.pm, gs.h | true) ∧ lsf0 = lsf ∧ pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed)), ∃ t, ls, pc. lstep(gs, lsf(t), pcf(t), globalACrash, gs0, ls, pc) ∧ lsf0 = lsf(t := ls) ∧ pcf0 = pcf(t := pc)

Rule argument

Additional information

Used simplifier rules: disj-globalACrash-globalAPersist: ⊦ globalACrash ≠ globalAPersist(l); a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a + x = a ' + x; (s) ⊦ firstVolWrite(l, h) < # h ↔ (h |W | l) | false ≠ []; (s)

Proof step 4 from proof plibStep-lem (previous step) (back to tree)

⊦ ⟨pm := gs.pm, vm := gs.vm, h := gs.h; ACrash(pm; vm, h, pcf); gs := (gs.vm:= vm).h:= h⟩ (gs0 = gs ∧ lsf0 = lsf ∧ pcf0 = pcf) ↔ gs0 = mkPLIBgs(gs.pm, gs.pm, gs.h | true) ∧ lsf0 = lsf ∧ pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed)), ∃ t, ls, pc. lstep(gs, lsf(t), pcf(t), globalACrash, gs0, ls, pc) ∧ lsf0 = lsf(t := ls) ∧ pcf0 = pcf(t := pc)

Heuristic dl case distinction applied rule case distinction

And obtained the following new goals

Proof step 5:
⟨pm := gs.pm, vm := gs.vm, h := gs.h; ACrash(pm; vm, h, pcf); gs := (gs.vm:= vm).h:= h⟩ (gs0 = gs ∧ lsf0 = lsf ∧ pcf0 = pcf) ⊦ ∃ t, ls, pc. lstep(gs, lsf(t), pcf(t), globalACrash, gs0, ls, pc) ∧ lsf0 = lsf(t := ls) ∧ pcf0 = pcf(t := pc), gs0 = mkPLIBgs(gs.pm, gs.pm, gs.h | true) ∧ lsf0 = lsf ∧ pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed))
Proof step 13:
gs0 = mkPLIBgs(gs.pm, gs.pm, gs.h | true), lsf0 = lsf, pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed)) ⊦ ⟨pm := gs.pm, vm := gs.vm, h := gs.h; ACrash(pm; vm, h, pcf); gs := (gs.vm:= vm).h:= h⟩ (gs0 = gs ∧ lsf0 = lsf ∧ pcf0 = pcf), ∃ t, ls, pc. lstep(gs, lsf(t), pcf(t), globalACrash, gs0, ls, pc) ∧ lsf0 = lsf(t := ls) ∧ pcf0 = pcf(t := pc)

Rule argument

pos: right 1

Additional information

Proof step 5 from proof plibStep-lem (previous step) (back to tree)

⟨pm := gs.pm, vm := gs.vm, h := gs.h; ACrash(pm; vm, h, pcf); gs := (gs.vm:= vm).h:= h⟩ (gs0 = gs ∧ lsf0 = lsf ∧ pcf0 = pcf) ⊦ ∃ t, ls, pc. lstep(gs, lsf(t), pcf(t), globalACrash, gs0, ls, pc) ∧ lsf0 = lsf(t := ls) ∧ pcf0 = pcf(t := pc), gs0 = mkPLIBgs(gs.pm, gs.pm, gs.h | true) ∧ lsf0 = lsf ∧ pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed))

Heuristic symbolic execution applied rule assign left

And obtained the following new goals

Proof step 6:
⟨ACrash(pm; vm, h, pcf); gs := (gs.vm:= vm).h:= h⟩ (gs0 = gs ∧ lsf0 = lsf ∧ pcf0 = pcf), h = gs.h, pm = gs.pm, vm = gs.vm ⊦ ∃ t, ls, pc. lstep(gs, lsf(t), pcf(t), globalACrash, gs0, ls, pc) ∧ lsf0 = lsf(t := ls) ∧ pcf0 = pcf(t := pc), gs0 = mkPLIBgs(gs.pm, gs.pm, gs.h | true) ∧ lsf0 = lsf ∧ pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed))

Rule argument

Additional information

Proof step 6 from proof plibStep-lem (previous step) (back to tree)

⟨ACrash(pm; vm, h, pcf); gs := (gs.vm:= vm).h:= h⟩ (gs0 = gs ∧ lsf0 = lsf ∧ pcf0 = pcf), h = gs.h, pm = gs.pm, vm = gs.vm ⊦ ∃ t, ls, pc. lstep(gs, lsf(t), pcf(t), globalACrash, gs0, ls, pc) ∧ lsf0 = lsf(t := ls) ∧ pcf0 = pcf(t := pc), gs0 = mkPLIBgs(gs.pm, gs.pm, gs.h | true) ∧ lsf0 = lsf ∧ pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed))

Heuristic split applied rule split left

And obtained the following new goals

Proof step 7:
⟨gs := (gs.vm:= vm0).h:= h0⟩ (gs0 = gs ∧ lsf0 = lsf ∧ pcf0 = pcf1), ⟨ACrash(pm; vm, h, pcf)⟩ (vm = vm0 ∧ h = h0 ∧ pcf = pcf1), h = gs.h, pm = gs.pm, vm = gs.vm ⊦ ∃ t, ls, pc. lstep(gs, lsf(t), pcf(t), globalACrash, gs0, ls, pc) ∧ lsf0 = lsf(t := ls) ∧ pcf0 = pcf(t := pc), gs0 = mkPLIBgs(gs.pm, gs.pm, gs.h | true) ∧ lsf0 = lsf ∧ pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed))

Rule argument

pos: left 1

Additional information

Proof step 7 from proof plibStep-lem (previous step) (back to tree)

⟨gs := (gs.vm:= vm0).h:= h0⟩ (gs0 = gs ∧ lsf0 = lsf ∧ pcf0 = pcf1), ⟨ACrash(pm; vm, h, pcf)⟩ (vm = vm0 ∧ h = h0 ∧ pcf = pcf1), h = gs.h, pm = gs.pm, vm = gs.vm ⊦ ∃ t, ls, pc. lstep(gs, lsf(t), pcf(t), globalACrash, gs0, ls, pc) ∧ lsf0 = lsf(t := ls) ∧ pcf0 = pcf(t := pc), gs0 = mkPLIBgs(gs.pm, gs.pm, gs.h | true) ∧ lsf0 = lsf ∧ pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed))

Heuristic symbolic execution applied rule assign left

And obtained the following new goals

Proof step 8:
⟨ACrash(pm; vm, h, pcf)⟩ (vm = vm0 ∧ h = h0 ∧ pcf = pcf1), gs0 = (gs.vm:= vm0).h:= h0, h = gs.h, lsf0 = lsf, pcf0 = pcf1, pm = gs.pm, vm = gs.vm ⊦ ∃ t, ls, pc. lstep(gs, lsf(t), pcf(t), globalACrash, gs0, ls, pc) ∧ lsf0 = lsf(t := ls) ∧ pcf0 = pcf(t := pc), gs0 = mkPLIBgs(gs.pm, gs.pm, gs.h | true) ∧ lsf0 = lsf ∧ pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed))

Rule argument

Additional information

Proof step 8 from proof plibStep-lem (previous step) (back to tree)

⟨ACrash(pm; vm, h, pcf)⟩ (vm = vm0 ∧ h = h0 ∧ pcf = pcf1), gs0 = (gs.vm:= vm0).h:= h0, h = gs.h, lsf0 = lsf, pcf0 = pcf1, pm = gs.pm, vm = gs.vm ⊦ ∃ t, ls, pc. lstep(gs, lsf(t), pcf(t), globalACrash, gs0, ls, pc) ∧ lsf0 = lsf(t := ls) ∧ pcf0 = pcf(t := pc), gs0 = mkPLIBgs(gs.pm, gs.pm, gs.h | true) ∧ lsf0 = lsf ∧ pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed))

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 9:
⟨ACrash(gs.pm; vm, h, pcf)⟩ (vm = vm0 ∧ h = h0 ∧ pcf = pcf1), h = gs.h, vm = gs.vm ⊦ ∃ t0, pc. lstep(gs, lsf(t0), pcf(t0), globalACrash, (gs.vm:= vm0).h:= h0, lsf(t0), pc) ∧ pcf1 = pcf(t0 := pc), (gs.vm:= vm0).h:= h0 = mkPLIBgs(gs.pm, gs.pm, gs.h | true) ∧ pcf1(t) = (pcf(t) = idle ⊃ idle;crashed)

Rule argument

Additional information

Proof step 9 from proof plibStep-lem (previous step) (back to tree)

⟨ACrash(gs.pm; vm, h, pcf)⟩ (vm = vm0 ∧ h = h0 ∧ pcf = pcf1), h = gs.h, vm = gs.vm ⊦ ∃ t0, pc. lstep(gs, lsf(t0), pcf(t0), globalACrash, (gs.vm:= vm0).h:= h0, lsf(t0), pc) ∧ pcf1 = pcf(t0 := pc), (gs.vm:= vm0).h:= h0 = mkPLIBgs(gs.pm, gs.pm, gs.h | true) ∧ pcf1(t) = (pcf(t) = idle ⊃ idle;crashed)

Heuristic unfold applied rule call left

And obtained the following new goals

Proof step 10:
⟨pcf := λ t. (pcf(t) = idle ⊃ idle;crashed), vm := pm, h := h | true⟩ (vm = vm0 ∧ h = h0 ∧ pcf = pcf1), h = gs.h, pm = gs.pm, vm = gs.vm ⊦ ∃ t0, pc. lstep(gs, lsf(t0), pcf(t0), globalACrash, (gs.vm:= vm0).h:= h0, lsf(t0), pc) ∧ pcf1 = pcf(t0 := pc), (gs.vm:= vm0).h:= h0 = mkPLIBgs(gs.pm, gs.pm, gs.h | true) ∧ pcf1(t) = (pcf(t) = idle ⊃ idle;crashed)

Rule argument

pos: left 1

Additional information

Used simplifier rules: ACrash: ⊦ ;

Proof step 10 from proof plibStep-lem (previous step) (back to tree)

⟨pcf := λ t. (pcf(t) = idle ⊃ idle;crashed), vm := pm, h := h | true⟩ (vm = vm0 ∧ h = h0 ∧ pcf = pcf1), h = gs.h, pm = gs.pm, vm = gs.vm ⊦ ∃ t0, pc. lstep(gs, lsf(t0), pcf(t0), globalACrash, (gs.vm:= vm0).h:= h0, lsf(t0), pc) ∧ pcf1 = pcf(t0 := pc), (gs.vm:= vm0).h:= h0 = mkPLIBgs(gs.pm, gs.pm, gs.h | true) ∧ pcf1(t) = (pcf(t) = idle ⊃ idle;crashed)

Heuristic symbolic execution applied rule assign left

And obtained the following new goals

Proof step 11:
(λ t. (pcf(t) = idle ⊃ idle;crashed)) = pcf1, h = gs.h, pm = gs.pm, pm = vm0, vm = gs.vm, h | true = h0 ⊦ ∃ t0, pc. lstep(gs, lsf(t0), pcf(t0), globalACrash, (gs.vm:= vm0).h:= h0, lsf(t0), pc) ∧ pcf1 = pcf(t0 := pc), (gs.vm:= vm0).h:= h0 = mkPLIBgs(gs.pm, gs.pm, gs.h | true) ∧ pcf1(t) = (pcf(t) = idle ⊃ idle;crashed)

Rule argument

Additional information

Proof step 11 from proof plibStep-lem (previous step) (back to tree)

(λ t. (pcf(t) = idle ⊃ idle;crashed)) = pcf1, h = gs.h, pm = gs.pm, pm = vm0, vm = gs.vm, h | true = h0 ⊦ ∃ t0, pc. lstep(gs, lsf(t0), pcf(t0), globalACrash, (gs.vm:= vm0).h:= h0, lsf(t0), pc) ∧ pcf1 = pcf(t0 := pc), (gs.vm:= vm0).h:= h0 = mkPLIBgs(gs.pm, gs.pm, gs.h | true) ∧ pcf1(t) = (pcf(t) = idle ⊃ idle;crashed)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 12:
(gs.vm:= gs.pm).h:= (gs.h | true) ≠ mkPLIBgs(gs.pm, gs.pm, gs.h | true) ⊦ ∃ t0, pc. lstep(gs, lsf(t0), pcf(t0), globalACrash, (gs.vm:= gs.pm).h:= (gs.h | true), lsf(t0), pc) ∧ (λ t. (pcf(t) = idle ⊃ idle;crashed)) = pcf(t0 := pc)

Rule argument

Additional information

Proof step 12 from proof plibStep-lem (previous step) (back to tree)

(gs.vm:= gs.pm).h:= (gs.h | true) ≠ mkPLIBgs(gs.pm, gs.pm, gs.h | true) ⊦ ∃ t0, pc. lstep(gs, lsf(t0), pcf(t0), globalACrash, (gs.vm:= gs.pm).h:= (gs.h | true), lsf(t0), pc) ∧ (λ t. (pcf(t) = idle ⊃ idle;crashed)) = pcf(t0 := pc)

User applied rule constructor cut

And closed the goal!

Rule argument

var: gs

Additional information

Used simplifier rules: gen-PLIBGState: ⊦ ; upd-mkPLIBgs-dotvm: ⊦ mkPLIBgs(vm, vm0, h).vm:= vm1 = mkPLIBgs(vm1, vm0, h); upd-mkPLIBgs-doth: ⊦ mkPLIBgs(vm, vm0, h).h:= h0 = mkPLIBgs(vm, vm0, h0); sel-mkPLIBgs-dotpm: ⊦ mkPLIBgs(vm, vm0, h).pm = vm0; sel-mkPLIBgs-doth: ⊦ mkPLIBgs(vm, vm0, h).h = h; inj-mkPLIBgs: ⊦ mkPLIBgs(vm, vm0, h) = mkPLIBgs(vm1, vm2, h0) ↔ vm = vm1 ∧ vm0 = vm2 ∧ h = h0;

Proof step 13 from proof plibStep-lem (previous step) (back to tree)

gs0 = mkPLIBgs(gs.pm, gs.pm, gs.h | true), lsf0 = lsf, pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed)) ⊦ ⟨pm := gs.pm, vm := gs.vm, h := gs.h; ACrash(pm; vm, h, pcf); gs := (gs.vm:= vm).h:= h⟩ (gs0 = gs ∧ lsf0 = lsf ∧ pcf0 = pcf), ∃ t, ls, pc. lstep(gs, lsf(t), pcf(t), globalACrash, gs0, ls, pc) ∧ lsf0 = lsf(t := ls) ∧ pcf0 = pcf(t := pc)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

Proof step 14:
gs0 = mkPLIBgs(gs.pm, gs.pm, gs.h | true), h = gs.h, lsf0 = lsf, pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed)), pm = gs.pm, vm = gs.vm ⊦ ⟨ACrash(pm; vm, h, pcf); gs := (gs.vm:= vm).h:= h⟩ (gs0 = gs ∧ lsf0 = lsf ∧ pcf0 = pcf), ∃ t, ls, pc. lstep(gs, lsf(t), pcf(t), globalACrash, gs0, ls, pc) ∧ lsf0 = lsf(t := ls) ∧ pcf0 = pcf(t := pc)

Rule argument

Additional information

Proof step 14 from proof plibStep-lem (previous step) (back to tree)

gs0 = mkPLIBgs(gs.pm, gs.pm, gs.h | true), h = gs.h, lsf0 = lsf, pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed)), pm = gs.pm, vm = gs.vm ⊦ ⟨ACrash(pm; vm, h, pcf); gs := (gs.vm:= vm).h:= h⟩ (gs0 = gs ∧ lsf0 = lsf ∧ pcf0 = pcf), ∃ t, ls, pc. lstep(gs, lsf(t), pcf(t), globalACrash, gs0, ls, pc) ∧ lsf0 = lsf(t := ls) ∧ pcf0 = pcf(t := pc)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 15:
gs0 = mkPLIBgs(gs.pm, gs.pm, gs.h | true), h = gs.h, pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed)), vm = gs.vm ⊦ ⟨ACrash(gs.pm; vm, h, pcf); gs := (gs.vm:= vm).h:= h⟩ (gs0 = gs ∧ pcf0 = pcf), ∃ t, pc. lstep(gs, lsf(t), pcf(t), globalACrash, mkPLIBgs(gs.pm, gs.pm, gs.h | true), lsf(t), pc) ∧ (λ t. (pcf(t) = idle ⊃ idle;crashed)) = pcf(t := pc)

Rule argument

Additional information

Proof step 15 from proof plibStep-lem (previous step) (back to tree)

gs0 = mkPLIBgs(gs.pm, gs.pm, gs.h | true), h = gs.h, pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed)), vm = gs.vm ⊦ ⟨ACrash(gs.pm; vm, h, pcf); gs := (gs.vm:= vm).h:= h⟩ (gs0 = gs ∧ pcf0 = pcf), ∃ t, pc. lstep(gs, lsf(t), pcf(t), globalACrash, mkPLIBgs(gs.pm, gs.pm, gs.h | true), lsf(t), pc) ∧ (λ t. (pcf(t) = idle ⊃ idle;crashed)) = pcf(t := pc)

Heuristic unfold applied rule call right

And obtained the following new goals

Proof step 16:
gs0 = mkPLIBgs(gs.pm, gs.pm, gs.h | true), h = gs.h, pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed)), pm = gs.pm, vm = gs.vm ⊦ ⟨pcf := λ t. (pcf(t) = idle ⊃ idle;crashed), vm := pm, h := h | true; gs := (gs.vm:= vm).h:= h⟩ (gs0 = gs ∧ pcf0 = pcf), ∃ t, pc. lstep(gs, lsf(t), pcf(t), globalACrash, mkPLIBgs(gs.pm, gs.pm, gs.h | true), lsf(t), pc) ∧ (λ t. (pcf(t) = idle ⊃ idle;crashed)) = pcf(t := pc)

Rule argument

pos: right 1

Additional information

Used simplifier rules: ACrash: ⊦ ;

Proof step 16 from proof plibStep-lem (previous step) (back to tree)

gs0 = mkPLIBgs(gs.pm, gs.pm, gs.h | true), h = gs.h, pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed)), pm = gs.pm, vm = gs.vm ⊦ ⟨pcf := λ t. (pcf(t) = idle ⊃ idle;crashed), vm := pm, h := h | true; gs := (gs.vm:= vm).h:= h⟩ (gs0 = gs ∧ pcf0 = pcf), ∃ t, pc. lstep(gs, lsf(t), pcf(t), globalACrash, mkPLIBgs(gs.pm, gs.pm, gs.h | true), lsf(t), pc) ∧ (λ t. (pcf(t) = idle ⊃ idle;crashed)) = pcf(t := pc)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

Proof step 17:
gs0 = mkPLIBgs(gs.pm, gs.pm, gs.h | true), h = gs.h, pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed)), pm = gs.pm, vm = gs.vm ⊦ ⟨gs := (gs.vm:= pm).h:= (h | true)⟩ (gs0 = gs ∧ pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed))), ∃ t, pc. lstep(gs, lsf(t), pcf(t), globalACrash, mkPLIBgs(gs.pm, gs.pm, gs.h | true), lsf(t), pc) ∧ (λ t. (pcf(t) = idle ⊃ idle;crashed)) = pcf(t := pc)

Rule argument

Additional information

Proof step 17 from proof plibStep-lem (previous step) (back to tree)

gs0 = mkPLIBgs(gs.pm, gs.pm, gs.h | true), h = gs.h, pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed)), pm = gs.pm, vm = gs.vm ⊦ ⟨gs := (gs.vm:= pm).h:= (h | true)⟩ (gs0 = gs ∧ pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed))), ∃ t, pc. lstep(gs, lsf(t), pcf(t), globalACrash, mkPLIBgs(gs.pm, gs.pm, gs.h | true), lsf(t), pc) ∧ (λ t. (pcf(t) = idle ⊃ idle;crashed)) = pcf(t := pc)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

Proof step 18:
gs0 = mkPLIBgs(gs.pm, gs.pm, gs.h | true), h = gs.h, pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed)), pm = gs.pm, vm = gs.vm ⊦ ∃ t, pc. lstep(gs, lsf(t), pcf(t), globalACrash, mkPLIBgs(gs.pm, gs.pm, gs.h | true), lsf(t), pc) ∧ (λ t. (pcf(t) = idle ⊃ idle;crashed)) = pcf(t := pc), gs0 = (gs.vm:= pm).h:= (h | true) ∧ pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed))

Rule argument

Additional information

Proof step 18 from proof plibStep-lem (previous step) (back to tree)

gs0 = mkPLIBgs(gs.pm, gs.pm, gs.h | true), h = gs.h, pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed)), pm = gs.pm, vm = gs.vm ⊦ ∃ t, pc. lstep(gs, lsf(t), pcf(t), globalACrash, mkPLIBgs(gs.pm, gs.pm, gs.h | true), lsf(t), pc) ∧ (λ t. (pcf(t) = idle ⊃ idle;crashed)) = pcf(t := pc), gs0 = (gs.vm:= pm).h:= (h | true) ∧ pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed))

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 19:
mkPLIBgs(gs.pm, gs.pm, gs.h | true) ≠ (gs.vm:= gs.pm).h:= (gs.h | true) ⊦ ∃ t, pc. lstep(gs, lsf(t), pcf(t), globalACrash, mkPLIBgs(gs.pm, gs.pm, gs.h | true), lsf(t), pc) ∧ (λ t. (pcf(t) = idle ⊃ idle;crashed)) = pcf(t := pc)

Rule argument

Additional information

Proof step 19 from proof plibStep-lem (previous step) (back to tree)

mkPLIBgs(gs.pm, gs.pm, gs.h | true) ≠ (gs.vm:= gs.pm).h:= (gs.h | true) ⊦ ∃ t, pc. lstep(gs, lsf(t), pcf(t), globalACrash, mkPLIBgs(gs.pm, gs.pm, gs.h | true), lsf(t), pc) ∧ (λ t. (pcf(t) = idle ⊃ idle;crashed)) = pcf(t := pc)

User applied rule constructor cut

And closed the goal!

Rule argument

var: gs

Additional information

Used simplifier rules: gen-PLIBGState: ⊦ ; sel-mkPLIBgs-dotpm: ⊦ mkPLIBgs(vm, vm0, h).pm = vm0; upd-mkPLIBgs-dotvm: ⊦ mkPLIBgs(vm, vm0, h).vm:= vm1 = mkPLIBgs(vm1, vm0, h); sel-mkPLIBgs-doth: ⊦ mkPLIBgs(vm, vm0, h).h = h; upd-mkPLIBgs-doth: ⊦ mkPLIBgs(vm, vm0, h).h:= h0 = mkPLIBgs(vm, vm0, h0); inj-mkPLIBgs: ⊦ mkPLIBgs(vm, vm0, h) = mkPLIBgs(vm1, vm2, h0) ↔ vm = vm1 ∧ vm0 = vm2 ∧ h = h0;