Proof step 1 from proof init-state-inv (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  gs.ctr = (λ l. 0), gs.mem = (λ l. O), gs.p = (λ l. []), gs.readers = (λ l. ∅), gs.writers = (λ l. ∅), pcf = (λ tid. idle), ¬ FLITPSCInv(gs, lsf, pcf), ∀ t. t = lsf(t).t ⊦

Rule argument

Additional information

Proof step 2 from proof init-state-inv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  gs.ctr = (λ l. 0), gs.mem = (λ l. O), gs.p = (λ l. []), gs.readers = (λ l. ∅), gs.writers = (λ l. ∅), ¬ FLITPSCInv(gs, lsf, λ tid. idle), ∀ t. t = lsf(t).t ⊦

Rule argument

Additional information

Proof step 3 from proof init-state-inv (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

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

• Proof step 5:

  gs.ctr = (λ l. 0), gs.mem = (λ l. O), gs.p = (λ l. []), gs.readers = (λ l. ∅), gs.writers = (λ l. ∅), ∀ t. t = lsf(t).t, ¬ FLITPSCGInv(gs) ∨ (∃ t. ¬(lsf(t).t = t ∧ FLITPSCLInv(gs, lsf(t), idle))) ⊦

Rule argument

Additional information

Used terms: gs, lsf, λ tid. idle

Proof step 4 from proof init-state-inv (previous step) (back to tree)

A spec-lemma

Proof step 5 from proof init-state-inv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  gs.ctr = (λ l. 0), gs.mem = (λ l. O), gs.p = (λ l. []), gs.readers = (λ l. ∅), gs.writers = (λ l. ∅), ∀ t. t = lsf(t).t, ¬ FLITPSCGInv(gs) ∨ lsf(t).t ≠ t ∨ ¬ FLITPSCLInv(gs, lsf(t), idle) ⊦

Rule argument

Additional information

Proof step 6 from proof init-state-inv (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ FLITPSCGInv(gs) ↔ ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)

• Proof step 8:

  gs.ctr = (λ l. 0), gs.mem = (λ l. O), gs.p = (λ l. []), gs.readers = (λ l. ∅), gs.writers = (λ l. ∅), ∀ t. t = lsf(t).t, ¬(ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p)) ∨ lsf(t).t ≠ t ∨ ¬ FLITPSCLInv(gs, lsf(t), idle) ⊦

Rule argument

Additional information

Used terms: gs

Proof step 7 from proof init-state-inv (previous step) (back to tree)

A spec-lemma

Proof step 8 from proof init-state-inv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  gs.ctr = (λ l. 0), gs.mem = (λ l. O), gs.p = (λ l. []), gs.readers = (λ l. ∅), gs.writers = (λ l. ∅), ∀ t. t = lsf(t).t, ¬ ctrok(λ l. 0, λ l. ∅) ∨ ¬ writersOk(λ l. [], λ l. ∅) ∨ ¬ pendingOk(λ l. []) ∨ lsf(t).t ≠ t ∨ ¬ FLITPSCLInv(gs, lsf(t), idle) ⊦

Rule argument

Additional information

Proof step 9 from proof init-state-inv (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ 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 11:

  gs.ctr = (λ l. 0), gs.mem = (λ l. O), gs.p = (λ l. []), gs.readers = (λ l. ∅), gs.writers = (λ l. ∅), ∀ t. t = lsf(t).t, ¬ ctrok(λ l. 0, λ l. ∅) ∨ ¬ writersOk(λ l. [], λ l. ∅) ∨ ¬ pendingOk(λ l. []) ∨ lsf(t).t ≠ t ∨ ¬ ( (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 10 from proof init-state-inv (previous step) (back to tree)

A spec-lemma

Proof step 11 from proof init-state-inv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  gs.ctr = (λ l. 0), gs.mem = (λ l. O), gs.p = (λ l. []), gs.readers = (λ l. ∅), gs.writers = (λ l. ∅), ∀ t. t = lsf(t).t, ¬ ctrok(λ l. 0, λ l. ∅) ∨ ¬ writersOk(λ l. [], λ l. ∅) ∨ ¬ pendingOk(λ l. []) ∨ lsf(t).t ≠ t ∨ ¬ notMember(lsf(t).t, λ l. ∅) ∨ ¬ noPending(lsf(t).t, λ l. []) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ noPending(t, p) → noPendingW(t, p); (ss) ⊦ 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 12 from proof init-state-inv (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

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

• Proof step 14:

  gs.ctr = (λ l. 0), gs.mem = (λ l. O), gs.p = (λ l. []), gs.readers = (λ l. ∅), gs.writers = (λ l. ∅), ∀ t. t = lsf(t).t, ¬(∀ l. # ∅ = 0) ∨ ¬ writersOk(λ l. [], λ l. ∅) ∨ ¬ pendingOk(λ l. []) ∨ lsf(t).t ≠ t ∨ ¬ notMember(lsf(t).t, λ l. ∅) ∨ ¬ noPending(lsf(t).t, λ l. []) ⊦

Rule argument

Additional information

Used terms: λ l. 0, λ l. ∅

Proof step 13 from proof init-state-inv (previous step) (back to tree)

A spec-lemma

Proof step 14 from proof init-state-inv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  gs.ctr = (λ l. 0), gs.mem = (λ l. O), gs.p = (λ l. []), gs.readers = (λ l. ∅), gs.writers = (λ l. ∅), ∀ t. t = lsf(t).t, ¬ writersOk(λ l. [], λ l. ∅) ∨ ¬ pendingOk(λ l. []) ∨ lsf(t).t ≠ t ∨ ¬ notMember(lsf(t).t, λ l. ∅) ∨ ¬ noPending(lsf(t).t, λ l. []) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # ∅ = 0; (s)

Proof step 15 from proof init-state-inv (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

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

• Proof step 17:

  gs.ctr = (λ l. 0), gs.mem = (λ l. O), gs.p = (λ l. []), gs.readers = (λ l. ∅), gs.writers = (λ l. ∅), ∀ t. t = lsf(t).t, ¬(∀ l, t. (t ∈ ∅ → (∀ l0. l0 ≠ l → ¬ t ∈ ∅)) ∧ (¬ t ∈ ∅ → [] |W | t = [])) ∨ ¬ pendingOk(λ l. []) ∨ lsf(t).t ≠ t ∨ ¬ notMember(lsf(t).t, λ l. ∅) ∨ ¬ noPending(lsf(t).t, λ l. []) ⊦

Rule argument

Additional information

Used terms: λ l. [], λ l. ∅

Proof step 16 from proof init-state-inv (previous step) (back to tree)

A spec-lemma

Proof step 17 from proof init-state-inv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  gs.ctr = (λ l. 0), gs.mem = (λ l. O), gs.p = (λ l. []), gs.readers = (λ l. ∅), gs.writers = (λ l. ∅), ∀ t. t = lsf(t).t, ¬ pendingOk(λ l. []) ∨ lsf(t).t ≠ t ∨ ¬ notMember(lsf(t).t, λ l. ∅) ∨ ¬ noPending(lsf(t).t, λ l. []) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ [] | t = []; (s) ⊦ [] |W = []; (s) ⊦ ¬ a ∈ ∅; (s)

Proof step 18 from proof init-state-inv (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

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

• Proof step 20:

  gs.ctr = (λ l. 0), gs.mem = (λ l. O), gs.p = (λ l. []), gs.readers = (λ l. ∅), gs.writers = (λ l. ∅), ∀ t. t = lsf(t).t, ¬(∀ l, t. #([] |W | t) ≤ 1) ∨ lsf(t).t ≠ t ∨ ¬ notMember(lsf(t).t, λ l. ∅) ∨ ¬ noPending(lsf(t).t, λ l. []) ⊦

Rule argument

Additional information

Used terms: λ l. []

Proof step 19 from proof init-state-inv (previous step) (back to tree)

A spec-lemma

Proof step 20 from proof init-state-inv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  gs.ctr = (λ l. 0), gs.mem = (λ l. O), gs.p = (λ l. []), gs.readers = (λ l. ∅), gs.writers = (λ l. ∅), ∀ t. t = lsf(t).t, lsf(t).t ≠ t ∨ ¬ notMember(lsf(t).t, λ l. ∅) ∨ ¬ noPending(lsf(t).t, λ l. []) ⊦

Rule argument

Additional information

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

Proof step 21 from proof init-state-inv (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 22:

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

• Proof step 23:

  gs.ctr = (λ l. 0), gs.mem = (λ l. O), gs.p = (λ l. []), gs.readers = (λ l. ∅), gs.writers = (λ l. ∅), ∀ t. t = lsf(t).t, lsf(t).t ≠ t ∨ ¬ notMember(lsf(t).t, λ l. ∅) ∨ ¬(∀ l. [] | lsf(t).t = []) ⊦

Rule argument

Additional information

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

Proof step 22 from proof init-state-inv (previous step) (back to tree)

A spec-lemma

Proof step 23 from proof init-state-inv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  gs.ctr = (λ l. 0), gs.mem = (λ l. O), gs.p = (λ l. []), gs.readers = (λ l. ∅), gs.writers = (λ l. ∅), ∀ t. t = lsf(t).t, lsf(t).t ≠ t ∨ ¬ notMember(lsf(t).t, λ l. ∅) ⊦

Rule argument

Additional information

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

Proof step 24 from proof init-state-inv (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 25:

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

• Proof step 26:

  gs.ctr = (λ l. 0), gs.mem = (λ l. O), gs.p = (λ l. []), gs.readers = (λ l. ∅), gs.writers = (λ l. ∅), ∀ t. t = lsf(t).t, lsf(t).t ≠ t ∨ ¬(∀ l. ¬ lsf(t).t ∈ ∅) ⊦

Rule argument

Additional information

Used terms: lsf(t).t, λ l. ∅

Proof step 25 from proof init-state-inv (previous step) (back to tree)

A spec-lemma

Proof step 26 from proof init-state-inv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  gs.ctr = (λ l. 0), gs.mem = (λ l. O), gs.p = (λ l. []), gs.readers = (λ l. ∅), gs.writers = (λ l. ∅), lsf(t).t ≠ t, ∀ t. t = lsf(t).t ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a ∈ ∅; (s)

Proof step 27 from proof init-state-inv (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: t