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.set = ∅, pcf = (λ tid. idle), ¬ SetInv(gs, lsf, pcf), ∀ tid. tid = lsf(tid).tid ⊦

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.set = ∅, ¬ SetInv(gs, lsf, λ tid. idle), ∀ tid. tid = lsf(tid).tid ⊦

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:

  ⊦ SetInv(gs, lsf, pcf) ↔ SetGInv(gs) ∧ (∀ tid. lsf(tid).tid = tid ∧ SetLInv(gs, lsf(tid), pcf(tid)))

• Proof step 5:

  gs.set = ∅, ∀ tid. tid = lsf(tid).tid, ¬ SetGInv(gs) ∨ (∃ tid. ¬(lsf(tid).tid = tid ∧ SetLInv(gs, lsf(tid), 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.set = ∅, ∀ tid. tid = lsf(tid).tid, ¬ SetGInv(gs) ∨ lsf(tid).tid ≠ tid ∨ ¬ SetLInv(gs, lsf(tid), 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:

  ⊦ SetGInv(gs) ↔ true

• Proof step 8:

  gs.set = ∅, ∀ tid. tid = lsf(tid).tid, ¬ true ∨ lsf(tid).tid ≠ tid ∨ ¬ SetLInv(gs, lsf(tid), 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.set = ∅, ∀ tid. tid = lsf(tid).tid, lsf(tid).tid ≠ tid ∨ ¬ SetLInv(gs, lsf(tid), 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:

  ⊦ SetLInv(gs, ls, pc) ↔ (pc = invInsert ∨ pc = retInsert ∨ pc = invMember ∨ pc = retMember → ls.le ≠ ⊥) ∧ (pc = retMember ∨ pc = retInsert → ls.lb → ls.le ∈ gs.set)

• Proof step 11:

  gs.set = ∅, ∀ tid. tid = lsf(tid).tid, lsf(tid).tid ≠ tid ∨ ¬ ( (idle = invInsert ∨ idle = retInsert ∨ idle = invMember ∨ idle = retMember → lsf(tid).le ≠ ⊥) ∧ (idle = retMember ∨ idle = retInsert → lsf(tid).lb → lsf(tid).le ∈ gs.set)) ⊦

Rule argument

Additional information

Used terms: gs, lsf(tid), 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.set = ∅, lsf(tid).tid ≠ tid, ∀ tid. tid = lsf(tid).tid ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ idle ≠ retInsert; (s) ⊦ idle ≠ retMember; (s) ⊦ idle ≠ invMember; (s) ⊦ idle ≠ invInsert; (s)

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: tid