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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  HashsetInv(gs, lsf, pcf), hashsetInit(mkstate(gs, lsf, pcf)) ⊦ ∃ ags, alsf, apcf. setInit(mkstate(ags, alsf, apcf)) ∧ abs(mkstate(gs, lsf, pcf), mkstate(ags, alsf, apcf))

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  HashsetInv(gs, lsf, pcf), hashsetInit(mkstate(gs, lsf, pcf)) ⊦ ∃ ags, alsf. ags.set = ∅ ∧ (∀ tid. alsf(tid).tid = tid) ∧ absset(gs.ar, ags.set) ∧ (∀ tid. labs(gs, lsf(tid), pcf(tid), ags, alsf(tid), idle))

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) ∧ (∀ tid. labs(gs, lsf(tid), pcf(tid), ags, alsf(tid), apcf(tid))); gabs-def: ⊦ gabs(gs, lsf, pcf, ags, alsf, apcf) ↔ absset(gs.ar, ags.set); ⊦ setInit(mkstate(gs, lsf, pcf)) ↔ (gs.set = ∅ ∧ pcf = (λ tid. idle)) ∧ (∀ tid. lsf(tid).tid = tid); (s)

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

User applied rule exists right

And obtained the following new goals

• Proof step 4:

  HashsetInv(gs, lsf, pcf), hashsetInit(mkstate(gs, lsf, pcf)) ⊦ mkgs(∅).set = ∅ ∧ (∀ tid. mkls(tid, ⊥, false).tid = tid) ∧ absset(gs.ar, mkgs(∅).set) ∧ (∀ tid. labs(gs, lsf(tid), pcf(tid), mkgs(∅), mkls(tid, ⊥, false), idle))

Rule argument

Additional information

Used terms: mkgs(∅), λ tid. mkls(tid, ⊥, false)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  gs.ar = mkar(n, ⊥), n ≠ 0, HashsetInv(gs, lsf, λ tid. idle), ∀ tid. lsf(tid).tid = tid ⊦ absset(mkar(n, ⊥), ∅) ∧ labs(gs, lsf(tid), idle, mkgs(∅), mkls(tid, ⊥, false), idle)

Rule argument

Additional information

Used simplifier rules: ⊦ mkgs(set).set = set; (s) ⊦ mkls(tid, le, lb).tid = tid; (s) ⊦ 0 < m ↔ m ≠ 0; (s) ⊦ m > n ↔ n < m; (s) ⊦ hashsetInit(mkstate(gs, lsf, pcf)) ↔ (∃ n. n > 0 ∧ gs.ar = mkar(n, ⊥) ∧ pcf = (λ tid. idle)) ∧ (∀ tid. lsf(tid).tid = tid); (s)

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

Heuristic use patterns applied rule case distinction

And obtained the following new goals

• Proof step 6:

  gs.ar = mkar(n, ⊥), n ≠ 0, HashsetInv(gs, lsf, λ tid. idle), ¬ absset(mkar(n, ⊥), ∅), ∀ tid. lsf(tid).tid = tid ⊦

• Proof step 8:

  gs.ar = mkar(n, ⊥), n ≠ 0, HashsetInv(gs, lsf, λ tid. idle), ¬ labs(gs, lsf(tid), idle, mkgs(∅), mkls(tid, ⊥, false), idle), ∀ tid. lsf(tid).tid = tid ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ absset(ar, set) ↔ (∀ e. e ∈ set ↔ (∃ n. n < # ar ∧ e = ar[n] ∧ e ≠ ⊥))

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a ∈ ∅; (s) ⊦ # mkar(n, e) = n; (s) ⊦ m < n → mkar(n, e)[m] = e; (s) Used terms: mkar(n, ⊥), ∅

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  gs.ar = mkar(n, ⊥), lsf(tid).tid ≠ tid, n ≠ 0, HashsetInv(gs, lsf, λ tid. idle), ∀ tid. lsf(tid).tid = tid ⊦

Rule argument

Additional information

Used simplifier rules: labs-def: ⊦ labs(gs, ls, pc, ags, als, apc) ↔ ls.tid = als.tid ∧ (pc = idle → apc = idle) ∧ ( pc = I1 ∨ pc = I2 ∨ pc = I3 ∨ pc = I4 ∨ pc = I6 ∨ pc = I10 ∨ pc = I11 ∨ pc = I12 ∨ pc = I16 ∨ pc = I17 ∨ pc = I18 ∨ pc = I20 → apc = invInsert) ∧ (pc = I5 → apc = (ls.b ⊃ retInsert;invInsert)) ∧ (pc = I7 ∨ pc = I13 → apc = (ls.e = ls.e0 ⊃ retInsert;invInsert)) ∧ (pc = I8 → apc = retInsert) ∧ (pc = I9 ∨ pc = I14 ∨ pc = I15 ∨ pc = I19 ∨ pc = I21 → apc = retInsert) ∧ (pc = I7 ∨ pc = I8 ∨ pc = I13 ∨ pc = I14 → ls.e = ls.e0 → als.lb) ∧ (pc = I9 ∨ pc = I15 ∨ pc = I19 → (als.lb ↔ ls.b)) ∧ (pc = I5 → ls.b → ¬ als.lb) ∧ (pc = I21 → ¬ als.lb) ∧ ( pc = M1 ∨ pc = M2 ∨ pc = M3 ∨ pc = M4 ∨ pc = M5 ∨ pc = M6 ∨ pc = M17 → apc = invMember) ∧ ( pc = M7 → apc = (ls.e0 ≠ ls.e ∧ ls.e0 ≠ ⊥ ∧ (ls.n + 1) % # gs.ar ≠ ls.n0 ⊃ invMember;retMember)) ∧ (pc = M10 → apc = (ls.e0 ≠ ⊥ ∧ (ls.n + 1) % # gs.ar ≠ ls.n0 ⊃ invMember;retMember)) ∧ (pc = M13 → apc = ((ls.n + 1) % # gs.ar ≠ ls.n0 ⊃ invMember;retMember)) ∧ (pc = M14 → apc = (ls.n ≠ ls.n0 ⊃ invMember;retMember)) ∧ (pc = M8 ∨ pc = M9 ∨ pc = M11 ∨ pc = M12 ∨ pc = M15 ∨ pc = M16 → apc = retMember) ∧ ( pc = M7 → ls.e0 = ls.e ∨ ls.e0 = ⊥ ∨ (ls.n + 1) % # gs.ar = ls.n0 → (ls.e = ls.e0 ↔ als.lb)) ∧ (pc = M10 → ls.e0 = ⊥ ∨ (ls.n + 1) % # gs.ar = ls.n0 → ¬ als.lb) ∧ (pc = M13 → (ls.n + 1) % # gs.ar = ls.n0 → ¬ als.lb) ∧ (pc = M14 → ls.n = ls.n0 → ¬ als.lb) ∧ (pc = M9 ∨ pc = M12 ∨ pc = M16 → (als.lb ↔ ls.b)) ∧ (pc = M11 ∨ pc = M15 → ¬ als.lb) ∧ (pc = M8 → als.lb) ∧ (apc = invMember ∨ apc = invInsert → ls.e = als.le); ⊦ idle ≠ invInsert; (s) ⊦ idle ≠ invMember; (s) ⊦ M8 ≠ idle; (s) ⊦ M15 ≠ idle; (s) ⊦ M11 ≠ idle; (s) ⊦ M16 ≠ idle; (s) ⊦ M12 ≠ idle; (s) ⊦ M9 ≠ idle; (s) ⊦ M14 ≠ idle; (s) ⊦ M13 ≠ idle; (s) ⊦ M10 ≠ idle; (s) ⊦ M7 ≠ idle; (s) ⊦ M17 ≠ idle; (s) ⊦ M6 ≠ idle; (s) ⊦ M5 ≠ idle; (s) ⊦ M4 ≠ idle; (s) ⊦ M3 ≠ idle; (s) ⊦ M2 ≠ idle; (s) ⊦ M1 ≠ idle; (s) ⊦ I21 ≠ idle; (s) ⊦ I5 ≠ idle; (s) ⊦ I19 ≠ idle; (s) ⊦ I15 ≠ idle; (s) ⊦ I9 ≠ idle; (s) ⊦ I14 ≠ idle; (s) ⊦ I13 ≠ idle; (s) ⊦ I8 ≠ idle; (s) ⊦ I7 ≠ idle; (s) ⊦ I20 ≠ idle; (s) ⊦ I18 ≠ idle; (s) ⊦ I17 ≠ idle; (s) ⊦ I16 ≠ idle; (s) ⊦ I12 ≠ idle; (s) ⊦ I11 ≠ idle; (s) ⊦ I10 ≠ idle; (s) ⊦ I6 ≠ idle; (s) ⊦ I4 ≠ idle; (s) ⊦ I3 ≠ idle; (s) ⊦ I2 ≠ idle; (s) ⊦ I1 ≠ idle; (s) ⊦ mkls(tid, le, lb).tid = tid; (s)

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: tid