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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  FLITPSCLInv(gs, lsf(t), pcf(t)), ctrok(gs.ctr, gs.writers), pendingOk(gs.p), writersOk(gs.p, gs.writers) ⊦ ⟪p := gs.p, ctr := gs.ctr, writers := gs.writers, readers := gs.readers; PSCCRASH(; p, ctr, writers, readers, pcf); gs := (((gs.p:= p).ctr:= ctr).writers:= writers).readers:= readers⟫ ((ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) ∧ FLITPSCLInv(gs, lsf(t), pcf(t)))

Rule argument

Additional information

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

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 3:

  ctr = gs.ctr, p = gs.p, readers = gs.readers, writers = gs.writers, FLITPSCLInv(gs, lsf(t), pcf(t)), ctrok(gs.ctr, gs.writers), pendingOk(gs.p), writersOk(gs.p, gs.writers) ⊦ ⟪PSCCRASH(; p, ctr, writers, readers, pcf); gs := (((gs.p:= p).ctr:= ctr).writers:= writers).readers:= readers⟫ ((ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) ∧ FLITPSCLInv(gs, lsf(t), pcf(t)))

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  ctr = gs.ctr, p = gs.p, readers = gs.readers, writers = gs.writers, FLITPSCLInv(gs, lsf(t), pcf(t)), ctrok(gs.ctr, gs.writers), pendingOk(gs.p), writersOk(gs.p, gs.writers) ⊦ ⟪PSCCRASH(; p, ctr, writers, readers, pcf); gs := (((gs.p:= p).ctr:= ctr).writers:= writers).readers:= readers⟫ (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p) ∧ FLITPSCLInv(gs, lsf(t), pcf(t)))

Rule argument

Additional information

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

Heuristic unfold applied rule call right

And obtained the following new goals

• Proof step 5:

  ctr = gs.ctr, p = gs.p, readers = gs.readers, writers = gs.writers, FLITPSCLInv(gs, lsf(t), pcf(t)), ctrok(gs.ctr, gs.writers), pendingOk(gs.p), writersOk(gs.p, gs.writers) ⊦ ⟪pcf := λ t. (pcf(t) = idle ⊃ idle;crashed), p := λ l. [], ctr := λ l. 0, readers := λ l. ∅, writers := λ l. ∅; gs := (((gs.p:= p).ctr:= ctr).writers:= writers).readers:= readers⟫ (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p) ∧ FLITPSCLInv(gs, lsf(t), pcf(t)))

Rule argument

Additional information

Used simplifier rules: decl: PSCCRASH(; p, ctr, writers, readers, pcf) {pcf := λ t. (pcf(t) = idle ⊃ idle;crashed), p := λ l. [], ctr := λ l. 0, readers := λ l. ∅, writers := λ l. ∅ };

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

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 6:

  ctr = gs.ctr, p = gs.p, readers = gs.readers, writers = gs.writers, FLITPSCLInv(gs, lsf(t), pcf(t)), ctrok(gs.ctr, gs.writers), pendingOk(gs.p), writersOk(gs.p, gs.writers) ⊦ ⟪gs := (((gs.p:= (λ l. [])).ctr:= (λ l. 0)).writers:= (λ l. ∅)).readers:= (λ l. ∅)⟫ (ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p) ∧ FLITPSCLInv(gs, lsf(t), (pcf(t) = idle ⊃ idle;crashed)))

Rule argument

Additional information

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

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 7:

  ctr = gs.ctr, p = gs.p, readers = gs.readers, writers = gs.writers, FLITPSCLInv(gs, lsf(t), pcf(t)), ctrok(gs.ctr, gs.writers), pendingOk(gs.p), writersOk(gs.p, gs.writers) ⊦ ctrok (((((gs.p:= (λ l. [])).ctr:= (λ l. 0)).writers:= (λ l. ∅)).readers:= (λ l. ∅)).ctr, ((((gs.p:= (λ l. [])).ctr:= (λ l. 0)).writers:= (λ l. ∅)).readers:= (λ l. ∅)).writers) ∧ writersOk (((((gs.p:= (λ l. [])).ctr:= (λ l. 0)).writers:= (λ l. ∅)).readers:= (λ l. ∅)).p, ((((gs.p:= (λ l. [])).ctr:= (λ l. 0)).writers:= (λ l. ∅)).readers:= (λ l. ∅)).writers) ∧ pendingOk(((((gs.p:= (λ l. [])).ctr:= (λ l. 0)).writers:= (λ l. ∅)).readers:= (λ l. ∅)).p) ∧ FLITPSCLInv((((gs.p:= (λ l. [])).ctr:= (λ l. 0)).writers:= (λ l. ∅)).readers:= (λ l. ∅), lsf(t), (pcf(t) = idle ⊃ idle;crashed))

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  FLITPSCLInv(gs, lsf(t), pcf(t)), ctrok(gs.ctr, gs.writers), pendingOk(gs.p), writersOk(gs.p, gs.writers) ⊦ ctrok(λ l. 0, λ l. ∅) ∧ writersOk(λ l. [], λ l. ∅) ∧ pendingOk(λ l. []) ∧ FLITPSCLInv((((gs.p:= (λ l. [])).ctr:= (λ l. 0)).writers:= (λ l. ∅)).readers:= (λ l. ∅), lsf(t), (pcf(t) = idle ⊃ idle;crashed))

Rule argument

Additional information

Used simplifier rules: ⊦ (gs.p:= p).p = p; (s) ⊦ (gs.ctr:= ctr).p = gs.p; (s) ⊦ (gs.writers:= writers).p = gs.p; (s) ⊦ (gs.readers:= writers0).p = gs.p; (s) ⊦ (gs.writers:= writers).writers = writers; (s) ⊦ (gs.readers:= writers0).writers = gs.writers; (s) ⊦ (gs.ctr:= ctr).ctr = ctr; (s) ⊦ (gs.writers:= writers).ctr = gs.ctr; (s) ⊦ (gs.readers:= writers0).ctr = gs.ctr; (s)

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

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 9:

  FLITPSCLInv(gs, lsf(t), pcf(t)), ctrok(gs.ctr, gs.writers), pendingOk(gs.p), writersOk(gs.p, gs.writers), ¬ ctrok(λ l. 0, λ l. ∅) ⊦

• Proof step 11:

  FLITPSCLInv(gs, lsf(t), pcf(t)), ctrok(gs.ctr, gs.writers), pendingOk(gs.p), writersOk(gs.p, gs.writers), ¬ writersOk(λ l. [], λ l. ∅) ⊦

• Proof step 13:

  FLITPSCLInv(gs, lsf(t), pcf(t)), ctrok(gs.ctr, gs.writers), pendingOk(gs.p), writersOk(gs.p, gs.writers), ¬ pendingOk(λ l. []) ⊦

• Proof step 15:

  FLITPSCLInv(gs, lsf(t), pcf(t)), ctrok(gs.ctr, gs.writers), pendingOk(gs.p), writersOk(gs.p, gs.writers), ¬ FLITPSCLInv((((gs.p:= (λ l. [])).ctr:= (λ l. 0)).writers:= (λ l. ∅)).readers:= (λ l. ∅), lsf(t), (pcf(t) = idle ⊃ idle;crashed)) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ ctrok(ctr, writers) ↔ (∀ l. # writers(l) = ctr(l))

Rule argument

Additional information

Used simplifier rules: ⊦ # ∅ = 0; (s) Used terms: λ l. 0, λ l. ∅

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  ⊦ writersOk(p, writers) ↔ (∀ l, t. (t ∈ writers(l) → (∀ l0. l0 ≠ l → ¬ t ∈ writers(l0))) ∧ (¬ t ∈ writers(l) → p(l) |W | t = []))

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a ∈ ∅; (s) ⊦ [] |W = []; (s) ⊦ [] | t = []; (s) Used terms: λ l. [], λ l. ∅

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

  ⊦ pendingOk(p) ↔ (∀ l, t. #(p(l) |W | t) ≤ 1)

Rule argument

Additional information

Used simplifier rules: ⊦ [] |W = []; (s) ⊦ [] | t = []; (s) ⊦ # [] = 0; (s) Used terms: λ l. []

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

A spec-lemma

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

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 16:

  pcf(t) = idle, FLITPSCLInv(gs, lsf(t), pcf(t)), ctrok(gs.ctr, gs.writers), pendingOk(gs.p), writersOk(gs.p, gs.writers), ¬ FLITPSCLInv((((gs.p:= (λ l. [])).ctr:= (λ l. 0)).writers:= (λ l. ∅)).readers:= (λ l. ∅), lsf(t), idle) ⊦

• Proof step 28:

  pcf(t) ≠ idle, FLITPSCLInv(gs, lsf(t), pcf(t)), ctrok(gs.ctr, gs.writers), pendingOk(gs.p), writersOk(gs.p, gs.writers), ¬ FLITPSCLInv((((gs.p:= (λ l. [])).ctr:= (λ l. 0)).writers:= (λ l. ∅)).readers:= (λ l. ∅), lsf(t), crashed) ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  pcf(t) = idle, FLITPSCLInv(gs, lsf(t), idle), ctrok(gs.ctr, gs.writers), pendingOk(gs.p), writersOk(gs.p, gs.writers), ¬ FLITPSCLInv((((gs.p:= (λ l. [])).ctr:= (λ l. 0)).writers:= (λ l. ∅)).readers:= (λ l. ∅), lsf(t), idle) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 18:

  ⊦ FLITPSCLInv(gs, ls, pc) ↔ (pc = W1 ∨ pc = W2 ∨ pc = W3 ∨ pc = W4 ∨ pc = W5 ∨ pc = W6 ∨ pc = W7 → notMember(ls.t, gs.readers)) ∧ (pc = W1 ∨ pc = W2 ∨ pc = W7 → notMember(ls.t, gs.writers)) ∧ (pc = W3 ∨ pc = W4 ∨ pc = W5 ∨ pc = W6 → oneMember(ls.t, ls.l, gs.writers)) ∧ (pc = W1 ∨ pc = W2 → noPendingW(ls.t, gs.p)) ∧ (pc = W2 ∨ pc = W3 ∨ pc = W6 ∨ pc = W7 → noPending(ls.t, gs.p)) ∧ (pc = W4 ∨ pc = W5 → onePendingW(ls.t, ls.l, gs.p)) ∧ (pc = W5 → FOFollowsW(ls.t, gs.p(ls.l))) ∧ (pc = R1 ∨ pc = R2 ∨ pc = R3 ∨ pc = R4 → notMember(ls.t, gs.writers)) ∧ (pc = R1 ∨ pc = R4 → notMember(ls.t, gs.readers)) ∧ (pc = R2 ∨ pc = R3 → oneMember(ls.t, ls.l, gs.readers)) ∧ (pc = R1 ∨ pc = R2 ∨ pc = R3 ∨ pc = R4 → noPendingW(ls.t, gs.p)) ∧ (pc = idle ∨ pc = ready → notMember(ls.t, gs.writers)) ∧ (pc = idle ∨ pc = ready → notMember(ls.t, gs.readers)) ∧ (pc = idle ∨ pc = ready → noPendingW(ls.t, gs.p)) ∧ (pc = idle → noPending(ls.t, gs.p))

• Proof step 19:

  pcf(t) = idle, ctrok(gs.ctr, gs.writers), pendingOk(gs.p), writersOk(gs.p, gs.writers), ¬ FLITPSCLInv((((gs.p:= (λ l. [])).ctr:= (λ l. 0)).writers:= (λ l. ∅)).readers:= (λ l. ∅), lsf(t), idle), idle = W1 ∨ idle = W2 ∨ idle = W3 ∨ idle = W4 ∨ idle = W5 ∨ idle = W6 ∨ idle = W7 → notMember(lsf(t).t, gs.readers), idle = W1 ∨ idle = W2 ∨ idle = W7 → notMember(lsf(t).t, gs.writers), idle = W3 ∨ idle = W4 ∨ idle = W5 ∨ idle = W6 → oneMember(lsf(t).t, lsf(t).l, gs.writers), idle = W1 ∨ idle = W2 → noPendingW(lsf(t).t, gs.p), idle = W2 ∨ idle = W3 ∨ idle = W6 ∨ idle = W7 → noPending(lsf(t).t, gs.p), idle = W4 ∨ idle = W5 → onePendingW(lsf(t).t, lsf(t).l, gs.p), idle = W5 → FOFollowsW(lsf(t).t, gs.p(lsf(t).l)), idle = R1 ∨ idle = R2 ∨ idle = R3 ∨ idle = R4 → notMember(lsf(t).t, gs.writers), idle = R1 ∨ idle = R4 → notMember(lsf(t).t, gs.readers), idle = R2 ∨ idle = R3 → oneMember(lsf(t).t, lsf(t).l, gs.readers), idle = R1 ∨ idle = R2 ∨ idle = R3 ∨ idle = R4 → noPendingW(lsf(t).t, gs.p), idle = idle ∨ idle = ready → notMember(lsf(t).t, gs.writers), idle = idle ∨ idle = ready → notMember(lsf(t).t, gs.readers), idle = idle ∨ idle = ready → noPendingW(lsf(t).t, gs.p), idle = idle → noPending(lsf(t).t, gs.p) ⊦

Rule argument

Additional information

Used terms: gs, lsf(t), idle

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  pcf(t) = idle, ctrok(gs.ctr, gs.writers), noPending(lsf(t).t, gs.p), noPendingW(lsf(t).t, gs.p), notMember(lsf(t).t, gs.readers), notMember(lsf(t).t, gs.writers), pendingOk(gs.p), writersOk(gs.p, gs.writers), ¬ FLITPSCLInv((((gs.p:= (λ l. [])).ctr:= (λ l. 0)).writers:= (λ l. ∅)).readers:= (λ l. ∅), lsf(t), idle) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ W7 ≠ idle; (s) ⊦ W6 ≠ idle; (s) ⊦ W5 ≠ idle; (s) ⊦ W4 ≠ idle; (s) ⊦ W3 ≠ idle; (s) ⊦ W2 ≠ idle; (s) ⊦ W1 ≠ idle; (s) ⊦ R4 ≠ idle; (s) ⊦ R3 ≠ idle; (s) ⊦ R2 ≠ idle; (s) ⊦ R1 ≠ idle; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

  ⊦ FLITPSCLInv(gs, ls, pc) ↔ (pc = W1 ∨ pc = W2 ∨ pc = W3 ∨ pc = W4 ∨ pc = W5 ∨ pc = W6 ∨ pc = W7 → notMember(ls.t, gs.readers)) ∧ (pc = W1 ∨ pc = W2 ∨ pc = W7 → notMember(ls.t, gs.writers)) ∧ (pc = W3 ∨ pc = W4 ∨ pc = W5 ∨ pc = W6 → oneMember(ls.t, ls.l, gs.writers)) ∧ (pc = W1 ∨ pc = W2 → noPendingW(ls.t, gs.p)) ∧ (pc = W2 ∨ pc = W3 ∨ pc = W6 ∨ pc = W7 → noPending(ls.t, gs.p)) ∧ (pc = W4 ∨ pc = W5 → onePendingW(ls.t, ls.l, gs.p)) ∧ (pc = W5 → FOFollowsW(ls.t, gs.p(ls.l))) ∧ (pc = R1 ∨ pc = R2 ∨ pc = R3 ∨ pc = R4 → notMember(ls.t, gs.writers)) ∧ (pc = R1 ∨ pc = R4 → notMember(ls.t, gs.readers)) ∧ (pc = R2 ∨ pc = R3 → oneMember(ls.t, ls.l, gs.readers)) ∧ (pc = R1 ∨ pc = R2 ∨ pc = R3 ∨ pc = R4 → noPendingW(ls.t, gs.p)) ∧ (pc = idle ∨ pc = ready → notMember(ls.t, gs.writers)) ∧ (pc = idle ∨ pc = ready → notMember(ls.t, gs.readers)) ∧ (pc = idle ∨ pc = ready → noPendingW(ls.t, gs.p)) ∧ (pc = idle → noPending(ls.t, gs.p))

• Proof step 22:

  pcf(t) = idle, ctrok(gs.ctr, gs.writers), noPending(lsf(t).t, gs.p), noPendingW(lsf(t).t, gs.p), notMember(lsf(t).t, gs.writers), notMember(lsf(t).t, gs.readers), pendingOk(gs.p), writersOk(gs.p, gs.writers), ¬ ( idle = W1 ∨ idle = W2 ∨ idle = W3 ∨ idle = W4 ∨ idle = W5 ∨ idle = W6 ∨ idle = W7 → notMember(lsf(t).t, ((((gs.p:= (λ l. [])).ctr:= (λ l. 0)).writers:= (λ l. ∅)).readers:= (λ l. ∅)).readers)) ∨ ¬(idle = W1 ∨ idle = W2 ∨ idle = W7 → notMember(lsf(t).t, ((((gs.p:= (λ l. [])).ctr:= (λ l. 0)).writers:= (λ l. ∅)).readers:= (λ l. ∅)).writers)) ∨ ¬ ( idle = W3 ∨ idle = W4 ∨ idle = W5 ∨ idle = W6 → oneMember(lsf(t).t, lsf(t).l, ((((gs.p:= (λ l. [])).ctr:= (λ l. 0)).writers:= (λ l. ∅)).readers:= (λ l. ∅)).writers)) ∨ ¬(idle = W1 ∨ idle = W2 → noPendingW(lsf(t).t, ((((gs.p:= (λ l. [])).ctr:= (λ l. 0)).writers:= (λ l. ∅)).readers:= (λ l. ∅)).p)) ∨ ¬ ( idle = W2 ∨ idle = W3 ∨ idle = W6 ∨ idle = W7 → noPending(lsf(t).t, ((((gs.p:= (λ l. [])).ctr:= (λ l. 0)).writers:= (λ l. ∅)).readers:= (λ l. ∅)).p)) ∨ ¬(idle = W4 ∨ idle = W5 → onePendingW(lsf(t).t, lsf(t).l, ((((gs.p:= (λ l. [])).ctr:= (λ l. 0)).writers:= (λ l. ∅)).readers:= (λ l. ∅)).p)) ∨ ¬(idle = W5 → FOFollowsW(lsf(t).t, ((((gs.p:= (λ l. [])).ctr:= (λ l. 0)).writers:= (λ l. ∅)).readers:= (λ l. ∅)).p(lsf(t).l))) ∨ ¬ ( idle = R1 ∨ idle = R2 ∨ idle = R3 ∨ idle = R4 → notMember(lsf(t).t, ((((gs.p:= (λ l. [])).ctr:= (λ l. 0)).writers:= (λ l. ∅)).readers:= (λ l. ∅)).writers)) ∨ ¬(idle = R1 ∨ idle = R4 → notMember(lsf(t).t, ((((gs.p:= (λ l. [])).ctr:= (λ l. 0)).writers:= (λ l. ∅)).readers:= (λ l. ∅)).readers)) ∨ ¬(idle = R2 ∨ idle = R3 → oneMember(lsf(t).t, lsf(t).l, ((((gs.p:= (λ l. [])).ctr:= (λ l. 0)).writers:= (λ l. ∅)).readers:= (λ l. ∅)).readers)) ∨ ¬ ( idle = R1 ∨ idle = R2 ∨ idle = R3 ∨ idle = R4 → noPendingW(lsf(t).t, ((((gs.p:= (λ l. [])).ctr:= (λ l. 0)).writers:= (λ l. ∅)).readers:= (λ l. ∅)).p)) ∨ ¬(idle = idle ∨ idle = ready → notMember(lsf(t).t, ((((gs.p:= (λ l. [])).ctr:= (λ l. 0)).writers:= (λ l. ∅)).readers:= (λ l. ∅)).writers)) ∨ ¬(idle = idle ∨ idle = ready → notMember(lsf(t).t, ((((gs.p:= (λ l. [])).ctr:= (λ l. 0)).writers:= (λ l. ∅)).readers:= (λ l. ∅)).readers)) ∨ ¬(idle = idle ∨ idle = ready → noPendingW(lsf(t).t, ((((gs.p:= (λ l. [])).ctr:= (λ l. 0)).writers:= (λ l. ∅)).readers:= (λ l. ∅)).p)) ∨ ¬(idle = idle → noPending(lsf(t).t, ((((gs.p:= (λ l. [])).ctr:= (λ l. 0)).writers:= (λ l. ∅)).readers:= (λ l. ∅)).p)) ⊦

Rule argument

Additional information

Used terms: (((gs.p:= (λ l. [])).ctr:= (λ l. 0)).writers:= (λ l. ∅)).readers:= (λ l. ∅), lsf(t), idle

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  pcf(t) = idle, ctrok(gs.ctr, gs.writers), noPending(lsf(t).t, gs.p), noPendingW(lsf(t).t, gs.p), notMember(lsf(t).t, gs.readers), notMember(lsf(t).t, gs.writers), pendingOk(gs.p), writersOk(gs.p, gs.writers), ¬ notMember(lsf(t).t, λ l. ∅) ∨ ¬ noPending(lsf(t).t, λ l. []) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ noPending(t, p) → noPendingW(t, p); (ss) ⊦ (gs.p:= p).p = p; (s) ⊦ (gs.ctr:= ctr).p = gs.p; (s) ⊦ (gs.writers:= writers).p = gs.p; (s) ⊦ (gs.readers:= writers0).p = gs.p; (s) ⊦ (gs.readers:= writers0).readers = writers0; (s) ⊦ (gs.writers:= writers).writers = writers; (s) ⊦ (gs.readers:= writers0).writers = gs.writers; (s) ⊦ R4 ≠ idle; (s) ⊦ R3 ≠ idle; (s) ⊦ R2 ≠ idle; (s) ⊦ R1 ≠ idle; (s) ⊦ W5 ≠ idle; (s) ⊦ W4 ≠ idle; (s) ⊦ W7 ≠ idle; (s) ⊦ W6 ≠ idle; (s) ⊦ W3 ≠ idle; (s) ⊦ W2 ≠ idle; (s) ⊦ W1 ≠ idle; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 24:

  ⊦ noPending(t, p) ↔ (∀ l. p(l) | t = [])

• Proof step 25:

  pcf(t) = idle, ctrok(gs.ctr, gs.writers), noPending(lsf(t).t, gs.p), noPendingW(lsf(t).t, gs.p), notMember(lsf(t).t, gs.writers), notMember(lsf(t).t, gs.readers), pendingOk(gs.p), writersOk(gs.p, gs.writers), ¬ notMember(lsf(t).t, λ l. ∅) ∨ ¬(∀ l. [] | lsf(t).t = []) ⊦

Rule argument

Additional information

Used terms: lsf(t).t, λ l. []

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  pcf(t) = idle, ctrok(gs.ctr, gs.writers), noPending(lsf(t).t, gs.p), noPendingW(lsf(t).t, gs.p), notMember(lsf(t).t, gs.readers), notMember(lsf(t).t, gs.writers), pendingOk(gs.p), writersOk(gs.p, gs.writers), ¬ notMember(lsf(t).t, λ l. ∅) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ [] | t = []; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 27:

  ⊦ notMember(t, tsf) ↔ (∀ l. ¬ t ∈ tsf(l))

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a ∈ ∅; (s) Used terms: lsf(t).t, λ l. ∅

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 29:

  ⊦ FLITPSCLInv(gs, ls, pc) ↔ (pc = W1 ∨ pc = W2 ∨ pc = W3 ∨ pc = W4 ∨ pc = W5 ∨ pc = W6 ∨ pc = W7 → notMember(ls.t, gs.readers)) ∧ (pc = W1 ∨ pc = W2 ∨ pc = W7 → notMember(ls.t, gs.writers)) ∧ (pc = W3 ∨ pc = W4 ∨ pc = W5 ∨ pc = W6 → oneMember(ls.t, ls.l, gs.writers)) ∧ (pc = W1 ∨ pc = W2 → noPendingW(ls.t, gs.p)) ∧ (pc = W2 ∨ pc = W3 ∨ pc = W6 ∨ pc = W7 → noPending(ls.t, gs.p)) ∧ (pc = W4 ∨ pc = W5 → onePendingW(ls.t, ls.l, gs.p)) ∧ (pc = W5 → FOFollowsW(ls.t, gs.p(ls.l))) ∧ (pc = R1 ∨ pc = R2 ∨ pc = R3 ∨ pc = R4 → notMember(ls.t, gs.writers)) ∧ (pc = R1 ∨ pc = R4 → notMember(ls.t, gs.readers)) ∧ (pc = R2 ∨ pc = R3 → oneMember(ls.t, ls.l, gs.readers)) ∧ (pc = R1 ∨ pc = R2 ∨ pc = R3 ∨ pc = R4 → noPendingW(ls.t, gs.p)) ∧ (pc = idle ∨ pc = ready → notMember(ls.t, gs.writers)) ∧ (pc = idle ∨ pc = ready → notMember(ls.t, gs.readers)) ∧ (pc = idle ∨ pc = ready → noPendingW(ls.t, gs.p)) ∧ (pc = idle → noPending(ls.t, gs.p))

• Proof step 30:

  pcf(t) ≠ idle, ctrok(gs.ctr, gs.writers), pendingOk(gs.p), writersOk(gs.p, gs.writers), ¬ FLITPSCLInv((((gs.p:= (λ l. [])).ctr:= (λ l. 0)).writers:= (λ l. ∅)).readers:= (λ l. ∅), lsf(t), crashed), pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → notMember(lsf(t).t, gs.readers), pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W7 → notMember(lsf(t).t, gs.writers), pcf(t) = W3 ∨ pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 → oneMember(lsf(t).t, lsf(t).l, gs.writers), pcf(t) = W1 ∨ pcf(t) = W2 → noPendingW(lsf(t).t, gs.p), pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → noPending(lsf(t).t, gs.p), pcf(t) = W4 ∨ pcf(t) = W5 → onePendingW(lsf(t).t, lsf(t).l, gs.p), pcf(t) = W5 → FOFollowsW(lsf(t).t, gs.p(lsf(t).l)), pcf(t) = R1 ∨ pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → notMember(lsf(t).t, gs.writers), pcf(t) = R1 ∨ pcf(t) = R4 → notMember(lsf(t).t, gs.readers), pcf(t) = R2 ∨ pcf(t) = R3 → oneMember(lsf(t).t, lsf(t).l, gs.readers), pcf(t) = R1 ∨ pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → noPendingW(lsf(t).t, gs.p), pcf(t) = idle ∨ pcf(t) = ready → notMember(lsf(t).t, gs.writers), pcf(t) = idle ∨ pcf(t) = ready → notMember(lsf(t).t, gs.readers), pcf(t) = idle ∨ pcf(t) = ready → noPendingW(lsf(t).t, gs.p), pcf(t) = idle → noPending(lsf(t).t, gs.p) ⊦

Rule argument

Additional information

Used terms: gs, lsf(t), pcf(t)

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  pcf(t) ≠ idle, ctrok(gs.ctr, gs.writers), pendingOk(gs.p), writersOk(gs.p, gs.writers), ¬ FLITPSCLInv((((gs.p:= (λ l. [])).ctr:= (λ l. 0)).writers:= (λ l. ∅)).readers:= (λ l. ∅), lsf(t), crashed), pcf(t) = R1 ∨ pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → noPendingW(lsf(t).t, gs.p), pcf(t) = R2 ∨ pcf(t) = R3 → oneMember(lsf(t).t, lsf(t).l, gs.readers), pcf(t) = R1 ∨ pcf(t) = R4 → notMember(lsf(t).t, gs.readers), pcf(t) = R1 ∨ pcf(t) = R2 ∨ pcf(t) = R3 ∨ pcf(t) = R4 → notMember(lsf(t).t, gs.writers), pcf(t) = W5 → FOFollowsW(lsf(t).t, gs.p(lsf(t).l)), pcf(t) = W4 ∨ pcf(t) = W5 → onePendingW(lsf(t).t, lsf(t).l, gs.p), pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → noPending(lsf(t).t, gs.p), pcf(t) = W1 ∨ pcf(t) = W2 → noPendingW(lsf(t).t, gs.p), pcf(t) = W3 ∨ pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 → oneMember(lsf(t).t, lsf(t).l, gs.writers), pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W7 → notMember(lsf(t).t, gs.writers), pcf(t) = W1 ∨ pcf(t) = W2 ∨ pcf(t) = W3 ∨ pcf(t) = W4 ∨ pcf(t) = W5 ∨ pcf(t) = W6 ∨ pcf(t) = W7 → notMember(lsf(t).t, gs.readers), pcf(t) = ready → noPendingW(lsf(t).t, gs.p), pcf(t) = ready → notMember(lsf(t).t, gs.readers), pcf(t) = ready → notMember(lsf(t).t, gs.writers) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 32:

  ⊦ FLITPSCLInv(gs, ls, pc) ↔ (pc = W1 ∨ pc = W2 ∨ pc = W3 ∨ pc = W4 ∨ pc = W5 ∨ pc = W6 ∨ pc = W7 → notMember(ls.t, gs.readers)) ∧ (pc = W1 ∨ pc = W2 ∨ pc = W7 → notMember(ls.t, gs.writers)) ∧ (pc = W3 ∨ pc = W4 ∨ pc = W5 ∨ pc = W6 → oneMember(ls.t, ls.l, gs.writers)) ∧ (pc = W1 ∨ pc = W2 → noPendingW(ls.t, gs.p)) ∧ (pc = W2 ∨ pc = W3 ∨ pc = W6 ∨ pc = W7 → noPending(ls.t, gs.p)) ∧ (pc = W4 ∨ pc = W5 → onePendingW(ls.t, ls.l, gs.p)) ∧ (pc = W5 → FOFollowsW(ls.t, gs.p(ls.l))) ∧ (pc = R1 ∨ pc = R2 ∨ pc = R3 ∨ pc = R4 → notMember(ls.t, gs.writers)) ∧ (pc = R1 ∨ pc = R4 → notMember(ls.t, gs.readers)) ∧ (pc = R2 ∨ pc = R3 → oneMember(ls.t, ls.l, gs.readers)) ∧ (pc = R1 ∨ pc = R2 ∨ pc = R3 ∨ pc = R4 → noPendingW(ls.t, gs.p)) ∧ (pc = idle ∨ pc = ready → notMember(ls.t, gs.writers)) ∧ (pc = idle ∨ pc = ready → notMember(ls.t, gs.readers)) ∧ (pc = idle ∨ pc = ready → noPendingW(ls.t, gs.p)) ∧ (pc = idle → noPending(ls.t, gs.p))

Rule argument

Additional information

Used simplifier rules: ⊦ W1 ≠ crashed; (s) ⊦ W2 ≠ crashed; (s) ⊦ W3 ≠ crashed; (s) ⊦ W6 ≠ crashed; (s) ⊦ W7 ≠ crashed; (s) ⊦ W4 ≠ crashed; (s) ⊦ W5 ≠ crashed; (s) ⊦ R1 ≠ crashed; (s) ⊦ R2 ≠ crashed; (s) ⊦ R3 ≠ crashed; (s) ⊦ R4 ≠ crashed; (s) ⊦ crashed ≠ ready; (s) ⊦ crashed ≠ idle; (s) Used terms: (((gs.p:= (λ l. [])).ctr:= (λ l. 0)).writers:= (λ l. ∅)).readers:= (λ l. ∅), lsf(t), crashed

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

A spec-lemma