Proof step 1 from proof rely-noPendingW-stable (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  noPendingW(t, bq, pq), rely(t, pq, bq, pq0, bq0), ¬ noPendingW(t, bq0, pq0) ⊦

Rule argument

Additional information

Proof step 2 from proof rely-noPendingW-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ∀ l. (pq(l) | t) + bq(t).FOWs(t, l) ⊒ (pq0(l) | t) + bq0(t).FOWs(t, l), ∀ l. pq(l) |W | t = [] ∧ bq(t) |WL l = [] ⊦ pq0(l) |W | t = [] ∧ bq0(t) |WL l = []

Rule argument

Additional information

Used simplifier rules: rely-def: ⊦ rely(t, pq, bq, pq0, bq0) ↔ (∀ l. rely(t, l, pq(l), bq(t), pq0(l), bq0(t))); rely-local-def: ⊦ rely(t, l, fowl, bel, fowl0, bel0) ↔ (fowl | t) + bel.FOWs(t, l) ⊒ (fowl0 | t) + bel0.FOWs(t, l); noPendingW: ⊦ noPendingW(t, bq, p) ↔ (∀ l. p(l) |W | t = [] ∧ bq(t) |WL l = []);

Proof step 3 from proof rely-noPendingW-stable (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 4:

  (pq(l) | t) + bq(t).FOWs(t, l) ⊒ (pq0(l) | t) + bq0(t).FOWs(t, l), ∀ l. pq(l) |W | t = [] ∧ bq(t) |WL l = [] ⊦ pq0(l) |W | t = [] ∧ bq0(t) |WL l = []

Rule argument

Additional information

Used terms: l

Proof step 4 from proof rely-noPendingW-stable (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 5:

  pq(l) |W | t = [], bq(t) |WL l = [], (pq(l) | t) + bq(t).FOWs(t, l) ⊒ (pq0(l) | t) + bq0(t).FOWs(t, l) ⊦ pq0(l) |W | t = [] ∧ bq0(t) |WL l = []

Rule argument

Additional information

Used terms: l

Proof step 5 from proof rely-noPendingW-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  pq(l) |W | t = [], bq(t) |WL l = [], (pq(l) | t) + bq(t).FOWs(t, l) ⊒ (pq0(l) | t) + bq0(t).FOWs(t, l) ⊦ pq0(l) |W | t = [] ∧ bq0(t) |WL l = []

Rule argument

Additional information

Proof step 6 from proof rely-noPendingW-stable (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ fowl |W | t = (fowl | t)|W

• Proof step 8:

  (pq(l) | t)|W = [], bq(t) |WL l = [], (pq(l) | t) + bq(t).FOWs(t, l) ⊒ (pq0(l) | t) + bq0(t).FOWs(t, l) ⊦ pq0(l) |W | t = [] ∧ bq0(t) |WL l = []

Rule argument

Additional information

Used terms: pq(l), t

Proof step 7 from proof rely-noPendingW-stable (previous step) (back to tree)

A spec-lemma

Proof step 8 from proof rely-noPendingW-stable (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ fowl |W | t = (fowl | t)|W

• Proof step 10:

  (pq(l) | t)|W = [], bq(t) |WL l = [], (pq(l) | t) + bq(t).FOWs(t, l) ⊒ (pq0(l) | t) + bq0(t).FOWs(t, l) ⊦ (pq0(l) | t)|W = [] ∧ bq0(t) |WL l = []

Rule argument

Additional information

Used terms: pq0(l), t

Proof step 9 from proof rely-noPendingW-stable (previous step) (back to tree)

A spec-lemma

Proof step 10 from proof rely-noPendingW-stable (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

  ⊦ x ⊒ y ↔ (∃ z. z + y = x)

• Proof step 12:

  (pq(l) | t)|W = [], bq(t) |WL l = [], ∃ z. z + (pq0(l) | t) + bq0(t).FOWs(t, l) = (pq(l) | t) + bq(t).FOWs(t, l) ⊦ (pq0(l) | t)|W = [] ∧ bq0(t) |WL l = []

Rule argument

Additional information

Used terms: (pq(l) | t) + bq(t).FOWs(t, l), (pq0(l) | t) + bq0(t).FOWs(t, l)

Proof step 11 from proof rely-noPendingW-stable (previous step) (back to tree)

A spec-lemma

Proof step 12 from proof rely-noPendingW-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  fowl + (pq0(l) | t) + bq0(t).FOWs(t, l) = (pq(l) | t) + bq(t).FOWs(t, l), (pq(l) | t)|W = [], bq(t) |WL l = [] ⊦ (pq0(l) | t)|W = [] ∧ bq0(t) |WL l = []

Rule argument

Additional information

Proof step 13 from proof rely-noPendingW-stable (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 14:

  fowl + (pq0(l) | t) + bq0(t).FOWs(t, l) = (pq(l) | t) + bq(t).FOWs(t, l), (pq(l) | t)|W = [], (fowl + (pq0(l) | t) + bq0(t).FOWs(t, l))|W = ((pq(l) | t) + bq(t).FOWs(t, l))|W, bq(t) |WL l = [] ⊦ (pq0(l) | t)|W = [] ∧ bq0(t) |WL l = []

• Proof step 30:

  fowl + (pq0(l) | t) + bq0(t).FOWs(t, l) = (pq(l) | t) + bq(t).FOWs(t, l), (pq(l) | t)|W = [], bq(t) |WL l = [], (fowl + (pq0(l) | t) + bq0(t).FOWs(t, l))|W ≠ ((pq(l) | t) + bq(t).FOWs(t, l))|W ⊦ (pq0(l) | t)|W = [] ∧ bq0(t) |WL l = []

Rule argument

Additional information

Used formulas: (fowl + (pq0(l) | t) + bq0(t).FOWs(t, l))|W = ((pq(l) | t) + bq(t).FOWs(t, l))|W

Proof step 14 from proof rely-noPendingW-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  fowl + (pq0(l) | t) + bq0(t).FOWs(t, l) = (pq(l) | t) + bq(t).FOWs(t, l), (pq(l) | t)|W = [], fowl |W = [], (pq0(l) | t)|W = [], (bq0(t).FOWs(t, l))|W = [], bq(t) |WL l = [], bq0(t) |WL l ≠ [] ⊦

Rule argument

Additional information

Used simplifier rules: FOWs-loc-empty: ⊦ bel |WL l = [] → (bel.FOWs(t, l))|W = []; a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ x + [] = x; (s) ⊦ (fowl + fowl0)|W = fowl |W + fowl0 |W; (s)

Proof step 15 from proof rely-noPendingW-stable (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

  ⊦ fowl |W = fowl.filter(λ fow. fow.W?)

• Proof step 17:

  fowl + (pq0(l) | t) + bq0(t).FOWs(t, l) = (pq(l) | t) + bq(t).FOWs(t, l), bq0(t).FOWs(t, l).filter(λ fow. fow.W?) = [], (pq0(l) | t)|W = [], fowl |W = [], (pq(l) | t)|W = [], bq(t) |WL l = [], bq0(t) |WL l ≠ [] ⊦

Rule argument

Additional information

Used terms: bq0(t).FOWs(t, l)

Proof step 16 from proof rely-noPendingW-stable (previous step) (back to tree)

A spec-lemma

Proof step 17 from proof rely-noPendingW-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  fowl + (pq0(l) | t) + bq0(t).FOWs(t, l) = (pq(l) | t) + bq(t).FOWs(t, l), bq0(t).FOWs(t, l).filter(.W?) = [], (pq(l) | t)|W = [], fowl |W = [], (pq0(l) | t)|W = [], bq(t) |WL l = [], bq0(t) |WL l ≠ [] ⊦

Rule argument

Additional information

Proof step 18 from proof rely-noPendingW-stable (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

  ⊦ x = [] ↔ ¬(∃ a. a ∈ x)

• Proof step 20:

  fowl + (pq0(l) | t) + bq0(t).FOWs(t, l) = (pq(l) | t) + bq(t).FOWs(t, l), bq0(t).FOWs(t, l).filter(.W?) = [], (pq0(l) | t)|W = [], fowl |W = [], (pq(l) | t)|W = [], bq(t) |WL l = [], ∃ a. a ∈ bq0(t) |WL l ⊦

Rule argument

Additional information

Used terms: bq0(t) |WL l

Proof step 19 from proof rely-noPendingW-stable (previous step) (back to tree)

A spec-lemma

Proof step 20 from proof rely-noPendingW-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  fowl + (pq0(l) | t) + bq0(t).FOWs(t, l) = (pq(l) | t) + bq(t).FOWs(t, l), bq0(t).FOWs(t, l).filter(.W?) = [], (pq(l) | t)|W = [], fowl |W = [], (pq0(l) | t)|W = [], bq(t) |WL l = [], be ∈ bq0(t) |WL l ⊦

Rule argument

Additional information

Proof step 21 from proof rely-noPendingW-stable (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 22:

  ⊦ bel |WL l = bel.filter(λ be. be.W? ∧ be.l = l)

• Proof step 23:

  fowl + (pq0(l) | t) + bq0(t).FOWs(t, l) = (pq(l) | t) + bq(t).FOWs(t, l), bq0(t).FOWs(t, l).filter(.W?) = [], (pq0(l) | t)|W = [], fowl |W = [], (pq(l) | t)|W = [], bq(t) |WL l = [], be ∈ bq0(t).filter(λ be. be.W? ∧ be.l = l) ⊦

Rule argument

Additional information

Used terms: bq0(t), l

Proof step 22 from proof rely-noPendingW-stable (previous step) (back to tree)

Lemma BrestrictL-def

Proof step 23 from proof rely-noPendingW-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  fowl + (pq0(be.l) | t) + bq0(t).FOWs(t, be.l) = (pq(be.l) | t) + bq(t).FOWs(t, be.l), bq0(t).FOWs(t, be.l).filter(.W?) = [], (pq0(be.l) | t)|W = [], fowl |W = [], (pq(be.l) | t)|W = [], bq(t) |WL be.l = [], be.W?, be ∈ bq0(t) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ x.filter(p) ↔ a ∈ x ∧ p(a); (s)

Proof step 24 from proof rely-noPendingW-stable (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 25:

  fowl + (pq0(l) | t) + bq0(t).FOWs(t, l) = (pq(l) | t) + bq(t).FOWs(t, l), bq0(t).FOWs(t, l).filter(.W?) = [], be = W(l, v), (pq(l) | t)|W = [], fowl |W = [], (pq0(l) | t)|W = [], bq(t) |WL l = [], be.W?, be ∈ bq0(t) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ be.W? → (l = be.l ∧ v = be.v ↔ be = W(l, v)); (elim) Used terms: be, l, v

Proof step 25 from proof rely-noPendingW-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  fowl + (pq0(l) | t) + bq0(t).FOWs(t, l) = (pq(l) | t) + bq(t).FOWs(t, l), bq0(t).FOWs(t, l).filter(.W?) = [], (pq0(l) | t)|W = [], fowl |W = [], (pq(l) | t)|W = [], bq(t) |WL l = [], W(l, v) ∈ bq0(t) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ W(l, v).W?; (s)

Proof step 26 from proof rely-noPendingW-stable (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 27:

  ⊦ x = [] ↔ ¬(∃ a. a ∈ x)

• Proof step 28:

  fowl + (pq0(l) | t) + bq0(t).FOWs(t, l) = (pq(l) | t) + bq(t).FOWs(t, l), (pq(l) | t)|W = [], fowl |W = [], (pq0(l) | t)|W = [], bq(t) |WL l = [], W(l, v) ∈ bq0(t), ∀ a. ¬ a ∈ bq0(t).FOWs(t, l).filter(.W?) ⊦

Rule argument

Additional information

Used terms: bq0(t).FOWs(t, l).filter(.W?)

Proof step 27 from proof rely-noPendingW-stable (previous step) (back to tree)

A spec-lemma

Proof step 28 from proof rely-noPendingW-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  fowl + (pq0(l) | t) + bq0(t).FOWs(t, l) = (pq(l) | t) + bq(t).FOWs(t, l), (pq0(l) | t)|W = [], fowl |W = [], (pq(l) | t)|W = [], bq(t) |WL l = [], W(l, v) ∈ bq0(t), ∀ a. ¬ a ∈ bq0(t).FOWs(t, l) ∨ ¬ a.W? ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ x.filter(p) ↔ a ∈ x ∧ p(a); (s)

Proof step 29 from proof rely-noPendingW-stable (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: W-in-FOWs: ⊦ W(v, t0) ∈ bel.FOWs(t, l) ↔ t = t0 ∧ W(l, v) ∈ bel; ⊦ W(v, tid).W?; (s) Used terms: W(v, t)

Proof step 30 from proof rely-noPendingW-stable (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list