Proof step 1 from proof step-absstep-PSCCRASH-globalPSCCRASH (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  FLITPSCInv(gs0, lsf0, pcf0), FLITPSCInv(gs, lsf, pcf), PLIBInv(ags, alsf, apcf), abs(mkstate(gs, lsf, pcf), mkstate(ags, alsf, apcf)), flitpscStep(mkstate(gs, lsf, pcf), globalPSCCRASH, mkstate(gs0, lsf0, pcf0)) ⊦ ∃ ags0, alsf0, apcf0. plibStep(mkstate(ags, alsf, apcf), globalACrash, mkstate(ags0, alsf0, apcf0)) ∧ abs(mkstate(gs0, lsf0, pcf0), mkstate(ags0, alsf0, apcf0))

Rule argument

Additional information

Proof step 2 from proof step-absstep-PSCCRASH-globalPSCCRASH (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ags.pm = gs.mem, ags.vm = gs.mem ⊕ gs.p, FLITPSCInv(mkFLITPSCgs(gs.mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf, λ t. (pcf(t) = idle ⊃ idle;crashed)), FLITPSCInv(gs, lsf, pcf), PLIBInv(ags, alsf, apcf), abs(ags.h, gs.readers, gs.p), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ gs.mem = gs.mem ⊕ (λ l. []) ∧ abs(ags.h | true, λ l. ∅, λ l. []) ∧ labs (mkFLITPSCgs(gs.mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf(t), (pcf(t) = idle ⊃ idle;crashed), mkPLIBgs(gs.mem, gs.mem, ags.h | true), alsf(t), (apcf(t) = idle ⊃ idle;crashed))

Rule argument

Additional information

Used simplifier rules: abs-def: ⊦ abs(mkstate(gs, lsf, pcf), mkstate(ags, alsf, apcf)) ↔ gabs(gs, lsf, pcf, ags, alsf, apcf) ∧ (∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t))); gabs-def: ⊦ gabs(gs, lsf, pcf, ags, alsf, apcf) ↔ ags.pm = gs.mem ∧ ags.vm = gs.mem ⊕ gs.p ∧ abs(ags.h, gs.readers, gs.p); ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).p = p; (s) ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).readers = writers0; (s) ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).mem = mem; (s) ⊦ mkPLIBgs(vm, vm0, h).h = h; (s) ⊦ mkPLIBgs(vm, vm0, h).vm = vm; (s) ⊦ mkPLIBgs(vm, vm0, h).pm = vm0; (s) ⊦ globalACrash ≠ globalAPersist(l); (s) ⊦ ¬ pre(gs, ls, pc, globalACrash); (s) ⊦ lstep(gs, ls, pc, a, gs0, ls0, pc0) ↔ pre(gs, ls, pc, a) ∧ ls0 = lstepf(gs, ls, pc, a) ∧ gs0 = gstepf(gs, ls, pc, a) ∧ pc0 = pcstepf(gs, ls, pc, a); (s) ⊦ 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); (s) ⊦ globalPSCCRASH ≠ globalPSCPERSIST_FO(l); (s) ⊦ globalPSCCRASH ≠ globalPSCPERSIST_W(l); (s) ⊦ ¬ pre(gs, ls, pc, globalPSCCRASH); (s) ⊦ lstep(gs, ls, pc, a, gs0, ls0, pc0) ↔ pre(gs, ls, pc, a) ∧ ls0 = lstepf(gs, ls, pc, a) ∧ gs0 = gstepf(gs, ls, pc, a) ∧ pc0 = pcstepf(gs, ls, pc, a); (s) ⊦ flitpscStep(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)) ∨ (∃ l. a = globalPSCPERSIST_W(l) ∧ firstPersistW(gs.p(l)) < # gs.p(l) ∧ gs0 = (gs.mem:= gs.mem(l := gs.p(l)[firstPersistW(gs.p(l))].val)) .p:= gs.p(l := gs.p(l) -p firstPersistW(gs.p(l))) ∧ lsf0 = lsf ∧ pcf0 = pcf) ∨ (∃ l. a = globalPSCPERSIST_FO(l) ∧ (∃ n. isPersistFO(n, gs.p(l)) ∧ gs0 = gs.p:= gs.p(l := gs.p(l) -p n)) ∧ lsf0 = lsf ∧ pcf0 = pcf) ∨ a = globalPSCCRASH ∧ gs0 = mkFLITPSCgs(gs.mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅) ∧ lsf0 = lsf ∧ pcf0 = (λ t. (pcf(t) = idle ⊃ idle;crashed)); (s)

Proof step 3 from proof step-absstep-PSCCRASH-globalPSCCRASH (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 4:

  ags = mkPLIBgs(mem, mem0, h), mem = gs.mem ⊕ gs.p, mem0 = gs.mem, FLITPSCInv(gs, lsf, pcf), FLITPSCInv(mkFLITPSCgs(gs.mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf, λ t. (pcf(t) = idle ⊃ idle;crashed)), PLIBInv(ags, alsf, apcf), abs(h, gs.readers, gs.p), ∀ t. labs(gs, lsf(t), pcf(t), ags, alsf(t), apcf(t)) ⊦ gs.mem = gs.mem ⊕ (λ l. []) ∧ abs(h | true, λ l. ∅, λ l. []) ∧ labs (mkFLITPSCgs(gs.mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf(t), (pcf(t) = idle ⊃ idle;crashed), mkPLIBgs(gs.mem, gs.mem, h | true), alsf(t), (apcf(t) = idle ⊃ idle;crashed))

Rule argument

Additional information

Used simplifier rules: ⊦ (vm = gs.vm ∧ pm = gs.pm) ∧ h = gs.h ↔ gs = mkPLIBgs(vm, pm, h); (elim) Used terms: ags, mem, mem0, h

Proof step 4 from proof step-absstep-PSCCRASH-globalPSCCRASH (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  FLITPSCInv(mkFLITPSCgs(gs.mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf, λ t. (pcf(t) = idle ⊃ idle;crashed)), FLITPSCInv(gs, lsf, pcf), PLIBInv(mkPLIBgs(gs.mem ⊕ gs.p, gs.mem, h), alsf, apcf), abs(h, gs.readers, gs.p), ∀ t. labs(gs, lsf(t), pcf(t), mkPLIBgs(gs.mem ⊕ gs.p, gs.mem, h), alsf(t), apcf(t)) ⊦ gs.mem = gs.mem ⊕ (λ l. []) ∧ abs(h | true, λ l. ∅, λ l. []) ∧ labs (mkFLITPSCgs(gs.mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf(t), (pcf(t) = idle ⊃ idle;crashed), mkPLIBgs(gs.mem, gs.mem, h | true), alsf(t), (apcf(t) = idle ⊃ idle;crashed))

Rule argument

Additional information

Proof step 5 from proof step-absstep-PSCCRASH-globalPSCCRASH (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 6:

  gs = mkFLITPSCgs(mem, p, ctr, writers, writers0), FLITPSCInv(gs, lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf, λ t. (pcf(t) = idle ⊃ idle;crashed)), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), ∀ t. labs(gs, lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)) ⊦ mem = mem ⊕ (λ l. []) ∧ abs(h | true, λ l. ∅, λ l. []) ∧ labs (mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf(t), (pcf(t) = idle ⊃ idle;crashed), mkPLIBgs(mem, mem, h | true), alsf(t), (apcf(t) = idle ⊃ idle;crashed))

Rule argument

Additional information

Used simplifier rules: ⊦ (((mem = gs.mem ∧ p = gs.p) ∧ ctr = gs.ctr) ∧ writers = gs.writers) ∧ readers = gs.readers ↔ gs = mkFLITPSCgs(mem, p, ctr, writers, readers); (elim) Used terms: gs, mem, ctr, writers, writers0, p

Proof step 6 from proof step-absstep-PSCCRASH-globalPSCCRASH (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  FLITPSCInv(mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf, λ t. (pcf(t) = idle ⊃ idle;crashed)), FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)) ⊦ mem = mem ⊕ (λ l. []) ∧ abs(h | true, λ l. ∅, λ l. []) ∧ labs (mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf(t), (pcf(t) = idle ⊃ idle;crashed), mkPLIBgs(mem, mem, h | true), alsf(t), (apcf(t) = idle ⊃ idle;crashed))

Rule argument

Additional information

Proof step 7 from proof step-absstep-PSCCRASH-globalPSCCRASH (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 8:

  mem ≠ mem ⊕ (λ l. []), FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf, λ t. (pcf(t) = idle ⊃ idle;crashed)), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)) ⊦

• Proof step 9:

  FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf, λ t. (pcf(t) = idle ⊃ idle;crashed)), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), ¬ abs(h | true, λ l. ∅, λ l. []), ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)) ⊦

• Proof step 14:

  FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf, λ t. (pcf(t) = idle ⊃ idle;crashed)), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), ¬ labs (mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf(t), (pcf(t) = idle ⊃ idle;crashed), mkPLIBgs(mem, mem, h | true), alsf(t), (apcf(t) = idle ⊃ idle;crashed)), ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)) ⊦

Rule argument

Additional information

Proof step 8 from proof step-absstep-PSCCRASH-globalPSCCRASH (previous step) (back to tree)

User applied rule expand left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ ((mem ⊕ p))(l) = mem(l) ⊕ p(l); (s) ⊦ v ⊕ [] = v; (s)

Proof step 9 from proof step-absstep-PSCCRASH-globalPSCCRASH (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ abs(h, rs, p) ↔ (∀ l. absloc(events((h | l) | false), rs(l), p(l)))

• Proof step 11:

  FLITPSCInv(mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf, λ t. (pcf(t) = idle ⊃ idle;crashed)), FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), ∃ l. ¬ absloc(events(((h | true) | l) | false), ∅, []) ⊦

Rule argument

Additional information

Used terms: h | true, λ l. ∅, λ l. []

Proof step 10 from proof step-absstep-PSCCRASH-globalPSCCRASH (previous step) (back to tree)

A spec-lemma

Proof step 11 from proof step-absstep-PSCCRASH-globalPSCCRASH (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf, λ t. (pcf(t) = idle ⊃ idle;crashed)), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), ¬ absloc(events(((h | true) | l) | false), ∅, []), ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)) ⊦

Rule argument

Additional information

Proof step 12 from proof step-absstep-PSCCRASH-globalPSCCRASH (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

  ⊦ (h | l) | b = (h | b) | l

Rule argument

Additional information

Used simplifier rules: ⊦ h | true | false = []; (s) ⊦ [] | l = []; (s) ⊦ events([]) = []; (s) ⊦ absloc([], rset, fowl) ↔ fowl |W = []; (s) ⊦ [] |W = []; (s) Used terms: h | true, l, false

Proof step 13 from proof step-absstep-PSCCRASH-globalPSCCRASH (previous step) (back to tree)

A spec-lemma

Proof step 14 from proof step-absstep-PSCCRASH-globalPSCCRASH (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  FLITPSCInv(mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf, λ t. (pcf(t) = idle ⊃ idle;crashed)), FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)) ⊦ lsf(t).t = alsf(t).t ∧ (pcf(t) = idle → apcf(t) = idle) ∧ (pcf(t) ≠ idle → apcf(t) ≠ idle) ∧ (pcf(t) = idle → (((h | true) | l) | lsf(t).t) | false = [])

Rule argument

Additional information

Used simplifier rules: labs-def: ⊦ labs(gs, ls, pc, ags, als, apc) ↔ ls.t = als.t ∧ (pc = idle → apc = idle) ∧ (pc = ready → apc = ready) ∧ (pc = crashed → apc = crashed) ∧ (pc = R1 → apc = invRead) ∧ (pc = R2 ∨ pc = R3 ∨ pc = R4 → apc = resRead) ∧ (pc = W1 ∨ pc = W2 ∨ pc = W3 → apc = invWrite) ∧ (pc = W4 ∨ pc = W5 ∨ pc = W6 ∨ pc = W7 → apc = resWrite) ∧ (pc = R1 → ls.l = als.il) ∧ (pc = R2 ∨ pc = R3 ∨ pc = R4 → ls.v = als.ov) ∧ ( pc = W1 ∨ pc = W2 ∨ pc = W3 ∨ pc = W4 ∨ pc = W5 ∨ pc = W6 ∨ pc = W7 → ls.l = als.il ∧ ls.v = als.iv) ∧ ( pc = idle ∨ pc = ready ∨ pc = R1 ∨ pc = R4 ∨ pc = W1 ∨ pc = W5 → (∀ l. ¬ FO(ls.t) ∈ gs.p(l) → ((ags.h | l) | ls.t) | false = [])) ∧ (pc = W2 ∨ pc = W3 ∨ pc = W6 ∨ pc = W7 → (∀ l. ((ags.h | l) | ls.t) | false = [])) ∧ ( pc = R2 ∨ pc = R3 → (∀ l0. l0 ≠ ls.l ∧ ¬ FO(ls.t) ∈ gs.p(l0) → ((ags.h | l0) | ls.t) | false = [])) ∧ (pc = R2 → gs.ctr(ls.l) = 0 → ((ags.h | ls.l) | ls.t) | false = []) ∧ ( pc = W4 → ((ags.h | ls.l) | ls.t) | false = (W(ls.t, ls.l, ls.v), false) ' ∨ ((ags.h | ls.l) | ls.t) | false = []); ⊦ W4 ≠ crashed; (s) ⊦ W4 ≠ idle; (s) ⊦ R2 ≠ crashed; (s) ⊦ R2 ≠ idle; (s) ⊦ R3 ≠ crashed; (s) ⊦ R3 ≠ idle; (s) ⊦ W7 ≠ crashed; (s) ⊦ W7 ≠ idle; (s) ⊦ W6 ≠ crashed; (s) ⊦ W6 ≠ idle; (s) ⊦ W3 ≠ crashed; (s) ⊦ W3 ≠ idle; (s) ⊦ W2 ≠ crashed; (s) ⊦ W2 ≠ idle; (s) ⊦ mkPLIBgs(vm, vm0, h).h = h; (s) ⊦ ¬ a ∈ []; (s) ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).p = p; (s) ⊦ W5 ≠ crashed; (s) ⊦ W1 ≠ crashed; (s) ⊦ R4 ≠ crashed; (s) ⊦ R1 ≠ crashed; (s) ⊦ crashed ≠ ready; (s) ⊦ crashed ≠ idle; (s) ⊦ W5 ≠ idle; (s) ⊦ W1 ≠ idle; (s) ⊦ R4 ≠ idle; (s) ⊦ R1 ≠ idle; (s) ⊦ crashed ≠ idle; (s) ⊦ idle ≠ ready; (s)

Proof step 15 from proof step-absstep-PSCCRASH-globalPSCCRASH (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 16:

  alsf(t) = mkPLIBls(t0, il, iv, ov), FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf, λ t. (pcf(t) = idle ⊃ idle;crashed)), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)) ⊦ lsf(t).t = t0 ∧ (pcf(t) = idle → apcf(t) = idle) ∧ (pcf(t) ≠ idle → apcf(t) ≠ idle) ∧ (pcf(t) = idle → (((h | true) | l) | lsf(t).t) | false = [])

Rule argument

Additional information

Used simplifier rules: ⊦ ((t = ls.t ∧ il = ls.il) ∧ iv = ls.iv) ∧ ov = ls.ov ↔ ls = mkPLIBls(t, il, iv, ov); (elim) Used terms: alsf(t), iv, t0, il, ov

Proof step 16 from proof step-absstep-PSCCRASH-globalPSCCRASH (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 17:

  alsf(t) = mkPLIBls(t0, il, iv, ov), lsf(t) = mkFLITPSCls(t1, l0, v), FLITPSCInv(mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf, λ t. (pcf(t) = idle ⊃ idle;crashed)), FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)) ⊦ t1 = t0 ∧ (pcf(t) = idle → apcf(t) = idle) ∧ (pcf(t) ≠ idle → apcf(t) ≠ idle) ∧ (pcf(t) = idle → (((h | true) | l) | t1) | false = [])

Rule argument

Additional information

Used simplifier rules: ⊦ (t = ls.t ∧ l = ls.l) ∧ v = ls.v ↔ ls = mkFLITPSCls(t, l, v); (elim) Used terms: lsf(t), t1, l0, v

Proof step 17 from proof step-absstep-PSCCRASH-globalPSCCRASH (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  alsf(t) = mkPLIBls(t0, il, iv, ov), lsf(t) = mkFLITPSCls(t1, l0, v), FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf, λ t. (pcf(t) = idle ⊃ idle;crashed)), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)) ⊦ t1 = t0 ∧ (pcf(t) = idle → apcf(t) = idle) ∧ (pcf(t) ≠ idle → apcf(t) ≠ idle) ∧ (pcf(t) = idle → (((h | true) | l) | t0) | false = [])

Rule argument

Additional information

Proof step 18 from proof step-absstep-PSCCRASH-globalPSCCRASH (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

  ⊦ (h | t) | b = (h | b) | t

• Proof step 20:

  alsf(t) = mkPLIBls(t0, il, iv, ov), lsf(t) = mkFLITPSCls(t1, l0, v), FLITPSCInv(mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf, λ t. (pcf(t) = idle ⊃ idle;crashed)), FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)) ⊦ t1 = t0 ∧ (pcf(t) = idle → apcf(t) = idle) ∧ (pcf(t) ≠ idle → apcf(t) ≠ idle) ∧ (pcf(t) = idle → (((h | true) | l) | false) | t0 = [])

Rule argument

Additional information

Used terms: (h | true) | l, t0, false

Proof step 19 from proof step-absstep-PSCCRASH-globalPSCCRASH (previous step) (back to tree)

A spec-lemma

Proof step 20 from proof step-absstep-PSCCRASH-globalPSCCRASH (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

  ⊦ (h | l) | b = (h | b) | l

• Proof step 22:

  alsf(t) = mkPLIBls(t0, il, iv, ov), lsf(t) = mkFLITPSCls(t1, l0, v), FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), FLITPSCInv(mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf, λ t. (pcf(t) = idle ⊃ idle;crashed)), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)) ⊦ t1 = t0 ∧ (pcf(t) = idle → apcf(t) = idle) ∧ (pcf(t) ≠ idle → apcf(t) ≠ idle) ∧ (pcf(t) = idle → ((h | true | false) | l) | t0 = [])

Rule argument

Additional information

Used terms: h | true, l, false

Proof step 21 from proof step-absstep-PSCCRASH-globalPSCCRASH (previous step) (back to tree)

A spec-lemma

Proof step 22 from proof step-absstep-PSCCRASH-globalPSCCRASH (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  alsf(t) = mkPLIBls(t0, il, iv, ov), lsf(t) = mkFLITPSCls(t1, l0, v), FLITPSCInv(mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf, λ t. (pcf(t) = idle ⊃ idle;crashed)), FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)) ⊦ t1 = t0 ∧ (pcf(t) = idle → apcf(t) = idle) ∧ (pcf(t) ≠ idle → apcf(t) ≠ idle)

Rule argument

Additional information

Used simplifier rules: ⊦ [] | t = []; (s) ⊦ [] | l = []; (s) ⊦ h | true | false = []; (s)

Proof step 23 from proof step-absstep-PSCCRASH-globalPSCCRASH (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 24:

  ⊦ FLITPSCInv(gs, lsf, pcf) ↔ FLITPSCGInv(gs) ∧ (∀ t. lsf(t).t = t ∧ FLITPSCLInv(gs, lsf(t), pcf(t)))

• Proof step 25:

  alsf(t) = mkPLIBls(t0, il, iv, ov), lsf(t) = mkFLITPSCls(t1, l0, v), FLITPSCGInv(mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅)), FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), ∀ t. lsf(t).t = t ∧ FLITPSCLInv(mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf(t), (pcf(t) = idle ⊃ idle;crashed)) ⊦ t1 = t0 ∧ (pcf(t) = idle → apcf(t) = idle) ∧ (pcf(t) ≠ idle → apcf(t) ≠ idle)

Rule argument

Additional information

Used terms: mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf, λ t. (pcf(t) = idle ⊃ idle;crashed)

Proof step 24 from proof step-absstep-PSCCRASH-globalPSCCRASH (previous step) (back to tree)

A spec-lemma

Proof step 25 from proof step-absstep-PSCCRASH-globalPSCCRASH (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 26:

  lsf(t).t = t, alsf(t) = mkPLIBls(t0, il, iv, ov), lsf(t) = mkFLITPSCls(t1, l0, v), FLITPSCGInv(mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅)), FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), FLITPSCLInv(mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), lsf(t), (pcf(t) = idle ⊃ idle;crashed)), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)) ⊦ t1 = t0 ∧ (pcf(t) = idle → apcf(t) = idle) ∧ (pcf(t) ≠ idle → apcf(t) ≠ idle)

Rule argument

Additional information

Used terms: t

Proof step 26 from proof step-absstep-PSCCRASH-globalPSCCRASH (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  alsf(t1) = mkPLIBls(t0, il, iv, ov), lsf(t1) = mkFLITPSCls(t1, l0, v), FLITPSCGInv(mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅)), FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), FLITPSCLInv(mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), mkFLITPSCls(t1, l0, v), (pcf(t1) = idle ⊃ idle;crashed)), PLIBInv(mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf), abs(h, writers0, p), ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)) ⊦ t1 = t0 ∧ (pcf(t0) = idle → apcf(t0) = idle) ∧ (pcf(t0) ≠ idle → apcf(t0) ≠ idle)

Rule argument

Additional information

Used simplifier rules: ⊦ mkFLITPSCls(t, l, v).t = t; (s)

Proof step 27 from proof step-absstep-PSCCRASH-globalPSCCRASH (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 28:

  ⊦ PLIBInv(gs, lsf, pcf) ↔ PLIBGInv(gs) ∧ (∀ t. lsf(t).t = t ∧ PLIBLInv(gs, lsf(t), pcf(t)))

• Proof step 29:

  alsf(t1) = mkPLIBls(t0, il, iv, ov), lsf(t1) = mkFLITPSCls(t1, l0, v), FLITPSCGInv(mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅)), FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), FLITPSCLInv(mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), mkFLITPSCls(t1, l0, v), (pcf(t1) = idle ⊃ idle;crashed)), PLIBGInv(mkPLIBgs(mem ⊕ p, mem, h)), abs(h, writers0, p), ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), ∀ t. alsf(t).t = t ∧ PLIBLInv(mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)) ⊦ t1 = t0 ∧ (pcf(t0) = idle → apcf(t0) = idle) ∧ (pcf(t0) ≠ idle → apcf(t0) ≠ idle)

Rule argument

Additional information

Used terms: mkPLIBgs(mem ⊕ p, mem, h), alsf, apcf

Proof step 28 from proof step-absstep-PSCCRASH-globalPSCCRASH (previous step) (back to tree)

A spec-lemma

Proof step 29 from proof step-absstep-PSCCRASH-globalPSCCRASH (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 30:

  alsf(t1).t = t1, alsf(t1) = mkPLIBls(t0, il, iv, ov), lsf(t1) = mkFLITPSCls(t1, l0, v), FLITPSCGInv(mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅)), FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), FLITPSCLInv(mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), mkFLITPSCls(t1, l0, v), (pcf(t1) = idle ⊃ idle;crashed)), PLIBGInv(mkPLIBgs(mem ⊕ p, mem, h)), PLIBLInv(mkPLIBgs(mem ⊕ p, mem, h), alsf(t1), apcf(t1)), abs(h, writers0, p), ∀ t. alsf(t).t = t ∧ PLIBLInv(mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)) ⊦ t1 = t0 ∧ (pcf(t0) = idle → apcf(t0) = idle) ∧ (pcf(t0) ≠ idle → apcf(t0) ≠ idle)

Rule argument

Additional information

Used terms: t1

Proof step 30 from proof step-absstep-PSCCRASH-globalPSCCRASH (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  alsf(t0) = mkPLIBls(t0, il, iv, ov), lsf(t0) = mkFLITPSCls(t0, l0, v), FLITPSCGInv(mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅)), FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), FLITPSCLInv(mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), mkFLITPSCls(t0, l0, v), (pcf(t0) = idle ⊃ idle;crashed)), PLIBGInv(mkPLIBgs(mem ⊕ p, mem, h)), PLIBLInv(mkPLIBgs(mem ⊕ p, mem, h), mkPLIBls(t0, il, iv, ov), apcf(t0)), abs(h, writers0, p), ∀ t. alsf(t).t = t ∧ PLIBLInv(mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)), ∀ t. labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t), pcf(t), mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)) ⊦ (pcf(t0) = idle → apcf(t0) = idle) ∧ (pcf(t0) ≠ idle → apcf(t0) ≠ idle)

Rule argument

Additional information

Used simplifier rules: ⊦ mkPLIBls(t, il, iv, iv0).t = t; (s)

Proof step 31 from proof step-absstep-PSCCRASH-globalPSCCRASH (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 32:

  alsf(t0) = mkPLIBls(t0, il, iv, ov), lsf(t0) = mkFLITPSCls(t0, l0, v), FLITPSCGInv(mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅)), FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), FLITPSCLInv(mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), mkFLITPSCls(t0, l0, v), (pcf(t0) = idle ⊃ idle;crashed)), PLIBGInv(mkPLIBgs(mem ⊕ p, mem, h)), PLIBLInv(mkPLIBgs(mem ⊕ p, mem, h), mkPLIBls(t0, il, iv, ov), apcf(t0)), abs(h, writers0, p), labs(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf(t0), pcf(t0), mkPLIBgs(mem ⊕ p, mem, h), alsf(t0), apcf(t0)), ∀ t. alsf(t).t = t ∧ PLIBLInv(mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)) ⊦ (pcf(t0) = idle → apcf(t0) = idle) ∧ (pcf(t0) ≠ idle → apcf(t0) ≠ idle)

Rule argument

Additional information

Used terms: t0

Proof step 32 from proof step-absstep-PSCCRASH-globalPSCCRASH (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

  alsf(t0) = mkPLIBls(t0, il, iv, ov), apcf(t0) = idle, lsf(t0) = mkFLITPSCls(t0, l0, v), pcf(t0) ≠ idle, pcf(t0) ≠ W4, pcf(t0) ≠ W5, pcf(t0) ≠ W6, pcf(t0) ≠ W7, pcf(t0) ≠ W1, pcf(t0) ≠ W2, pcf(t0) ≠ W3, pcf(t0) ≠ R2, pcf(t0) ≠ R3, pcf(t0) ≠ R4, pcf(t0) ≠ R1, pcf(t0) ≠ crashed, pcf(t0) ≠ ready, FLITPSCGInv(mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅)), FLITPSCInv(mkFLITPSCgs(mem, p, ctr, writers, writers0), lsf, pcf), FLITPSCLInv(mkFLITPSCgs(mem, λ l. [], λ l. 0, λ l. ∅, λ l. ∅), mkFLITPSCls(t0, l0, v), crashed), PLIBGInv(mkPLIBgs(mem ⊕ p, mem, h)), PLIBLInv(mkPLIBgs(mem ⊕ p, mem, h), mkPLIBls(t0, il, iv, ov), idle), abs(h, writers0, p), ∀ t. alsf(t).t = t ∧ PLIBLInv(mkPLIBgs(mem ⊕ p, mem, h), alsf(t), apcf(t)) ⊦

Rule argument

Additional information

Used simplifier rules: labs-def: ⊦ labs(gs, ls, pc, ags, als, apc) ↔ ls.t = als.t ∧ (pc = idle → apc = idle) ∧ (pc = ready → apc = ready) ∧ (pc = crashed → apc = crashed) ∧ (pc = R1 → apc = invRead) ∧ (pc = R2 ∨ pc = R3 ∨ pc = R4 → apc = resRead) ∧ (pc = W1 ∨ pc = W2 ∨ pc = W3 → apc = invWrite) ∧ (pc = W4 ∨ pc = W5 ∨ pc = W6 ∨ pc = W7 → apc = resWrite) ∧ (pc = R1 → ls.l = als.il) ∧ (pc = R2 ∨ pc = R3 ∨ pc = R4 → ls.v = als.ov) ∧ ( pc = W1 ∨ pc = W2 ∨ pc = W3 ∨ pc = W4 ∨ pc = W5 ∨ pc = W6 ∨ pc = W7 → ls.l = als.il ∧ ls.v = als.iv) ∧ ( pc = idle ∨ pc = ready ∨ pc = R1 ∨ pc = R4 ∨ pc = W1 ∨ pc = W5 → (∀ l. ¬ FO(ls.t) ∈ gs.p(l) → ((ags.h | l) | ls.t) | false = [])) ∧ (pc = W2 ∨ pc = W3 ∨ pc = W6 ∨ pc = W7 → (∀ l. ((ags.h | l) | ls.t) | false = [])) ∧ ( pc = R2 ∨ pc = R3 → (∀ l0. l0 ≠ ls.l ∧ ¬ FO(ls.t) ∈ gs.p(l0) → ((ags.h | l0) | ls.t) | false = [])) ∧ (pc = R2 → gs.ctr(ls.l) = 0 → ((ags.h | ls.l) | ls.t) | false = []) ∧ ( pc = W4 → ((ags.h | ls.l) | ls.t) | false = (W(ls.t, ls.l, ls.v), false) ' ∨ ((ags.h | ls.l) | ls.t) | false = []); ⊦ idle ≠ ready; (s) ⊦ crashed ≠ idle; (s) ⊦ idle ≠ invRead; (s) ⊦ idle ≠ resRead; (s) ⊦ idle ≠ invWrite; (s) ⊦ idle ≠ resWrite; (s) ⊦ mkPLIBls(t, il, iv, iv0).il = il; (s) ⊦ mkFLITPSCls(t, l, v).l = l; (s) ⊦ mkPLIBls(t, il, iv, iv0).ov = iv0; (s) ⊦ mkFLITPSCls(t, l, v).v = v; (s) ⊦ mkPLIBls(t, il, iv, iv0).iv = iv; (s) ⊦ mkPLIBls(t, il, iv, iv0).t = t; (s) ⊦ mkFLITPSCls(t, l, v).t = t; (s) ⊦ mkPLIBgs(vm, vm0, h).h = h; (s) ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).ctr = ctr; (s) ⊦ mkFLITPSCgs(mem, p, ctr, writers, writers0).p = p; (s)

Proof step 33 from proof step-absstep-PSCCRASH-globalPSCCRASH (previous step) (back to tree)

User applied rule constructor cut

And closed the goal!

Rule argument

Additional information

Used simplifier rules: FLITPSCPC freely generated by R1, R2, R3, R4, W1, W2, W3, W4, W5, W6, W7, crashed, idle, ready ;;