Proof step 1 from proof relyp-one-pending-stable (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  onePendingW(t, l, p0), pendingOk(p), relyp(t, p0, p1), ¬ onePendingW(t, l, p1) ⊦

Rule argument

Additional information

Proof step 2 from proof relyp-one-pending-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  p1(l0).filter(.W?).filter(λ fow. fow.tid = t) ≠ [], l0 ≠ l, relyp(t, p0, p1), ∀ l0, t0. p(l0).filter(.W?).count(λ fow. fow.tid = t0) ≤ 1, ∀ l0. l0 ≠ l → p0(l0).filter(.W?).filter(λ fow. fow.tid = t) = [] ⊦

Rule argument

Additional information

Used simplifier rules: pendingOk: ⊦ pendingOk(p) ↔ (∀ l, t. #(p(l) |W | t) ≤ 1); onePendingW: ⊦ onePendingW(t, l, p) ↔ (∀ l0. l0 ≠ l → p(l0) |W | t = []); filterwrites-def: ⊦ fowl |W = fowl.filter(λ fow. fow.W?); filtertid-def: ⊦ fowl | t = fowl.filter(λ fow. fow.tid = t); ⊦ # x.filter(p) = x.count(p); (s)

Proof step 3 from proof relyp-one-pending-stable (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ relyp(t, p, p0) ↔ (∀ l. relyp(t, p(l), p0(l)))

• Proof step 5:

  p1(l0).filter(.W?).filter(λ fow. fow.tid = t) ≠ [], l0 ≠ l, ∀ l0. l0 ≠ l → p0(l0).filter(.W?).filter(λ fow. fow.tid = t) = [], ∀ l0, t0. p(l0).filter(.W?).count(λ fow. fow.tid = t0) ≤ 1, ∀ l. relyp(t, p0(l), p1(l)) ⊦

Rule argument

Additional information

Used terms: t, p0, p1

Proof step 4 from proof relyp-one-pending-stable (previous step) (back to tree)

Lemma allrelyp-def

Proof step 5 from proof relyp-one-pending-stable (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 6:

  p1(l0).filter(.W?).filter(λ fow. fow.tid = t) ≠ [], l0 ≠ l, relyp(t, p0(l0), p1(l0)), ∀ l0, t0. p(l0).filter(.W?).count(λ fow. fow.tid = t0) ≤ 1, ∀ l0. l0 ≠ l → p0(l0).filter(.W?).filter(λ fow. fow.tid = t) = [] ⊦

Rule argument

Additional information

Used terms: l0

Proof step 6 from proof relyp-one-pending-stable (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ relyp(t, fowl, fowl0) ↔ (∃ fowl1, fowl2. fowl ⊒ fowl1 ∧ fowl0 = fowl1 + fowl2 ∧ fowl2 | t = [])

• Proof step 8:

  p1(l0).filter(.W?).filter(λ fow. fow.tid = t) ≠ [], l0 ≠ l, ∀ l0. l0 ≠ l → p0(l0).filter(.W?).filter(λ fow. fow.tid = t) = [], ∀ l0, t0. p(l0).filter(.W?).count(λ fow. fow.tid = t0) ≤ 1, ∃ fowl1, fowl2. p0(l0) ⊒ fowl1 ∧ p1(l0) = fowl1 + fowl2 ∧ fowl2 | t = [] ⊦

Rule argument

Additional information

Used terms: t, p0(l0), p1(l0)

Proof step 7 from proof relyp-one-pending-stable (previous step) (back to tree)

Lemma relyp-def

Proof step 8 from proof relyp-one-pending-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  fowl2.filter(λ fow. fow.tid = t) = [], p1(l0) = fowl1 + fowl2, l0 ≠ l, p0(l0) ⊒ fowl1, ∀ l0. l0 ≠ l → p0(l0).filter(.W?).filter(λ fow. fow.tid = t) = [], ∀ l0, t0. p(l0).filter(.W?).count(λ fow. fow.tid = t0) ≤ 1 ⊦ fowl1.filter(.W?).filter(λ fow. fow.tid = t) = [] ∧ fowl2.filter(.W?).filter(λ fow. fow.tid = t) = []

Rule argument

Additional information

Used simplifier rules: filtertid-def: ⊦ fowl | t = fowl.filter(λ fow. fow.tid = t); a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ (x + y).filter(p) = x.filter(p) + y.filter(p); (s)

Proof step 9 from proof relyp-one-pending-stable (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

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

• Proof step 11:

  fowl2.filter(λ fow. fow.tid = t) = [], p1(l0) = fowl1 + fowl2, l0 ≠ l, ∀ l0, t0. p(l0).filter(.W?).count(λ fow. fow.tid = t0) ≤ 1, ∀ l0. l0 ≠ l → p0(l0).filter(.W?).filter(λ fow. fow.tid = t) = [], ∃ z. z + fowl1 = p0(l0) ⊦ fowl1.filter(.W?).filter(λ fow. fow.tid = t) = [] ∧ fowl2.filter(.W?).filter(λ fow. fow.tid = t) = []

Rule argument

Additional information

Used terms: p0(l0), fowl1

Proof step 10 from proof relyp-one-pending-stable (previous step) (back to tree)

A spec-lemma

Proof step 11 from proof relyp-one-pending-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  fowl + fowl1 = p0(l0), fowl2.filter(λ fow. fow.tid = t) = [], p1(l0) = fowl1 + fowl2, l0 ≠ l, ∀ l0. l0 ≠ l → p0(l0).filter(.W?).filter(λ fow. fow.tid = t) = [], ∀ l0, t0. p(l0).filter(.W?).count(λ fow. fow.tid = t0) ≤ 1 ⊦ fowl1.filter(.W?).filter(λ fow. fow.tid = t) = [] ∧ fowl2.filter(.W?).filter(λ fow. fow.tid = t) = []

Rule argument

Additional information

Proof step 12 from proof relyp-one-pending-stable (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 13:

  fowl + fowl1 = p0(l0), fowl2.filter(λ fow. fow.tid = t) = [], p1(l0) = fowl1 + fowl2, fowl1.filter(.W?).filter(λ fow. fow.tid = t) ≠ [], l0 ≠ l, ∀ l0, t0. p(l0).filter(.W?).count(λ fow. fow.tid = t0) ≤ 1, ∀ l0. l0 ≠ l → p0(l0).filter(.W?).filter(λ fow. fow.tid = t) = [] ⊦

• Proof step 22:

  fowl + fowl1 = p0(l0), fowl2.filter(λ fow. fow.tid = t) = [], p1(l0) = fowl1 + fowl2, fowl2.filter(.W?).filter(λ fow. fow.tid = t) ≠ [], l0 ≠ l, ∀ l0, t0. p(l0).filter(.W?).count(λ fow. fow.tid = t0) ≤ 1, ∀ l0. l0 ≠ l → p0(l0).filter(.W?).filter(λ fow. fow.tid = t) = [] ⊦

Rule argument

Additional information

Proof step 13 from proof relyp-one-pending-stable (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

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

• Proof step 15:

  fowl + fowl1 = p0(l0), fowl2.filter(λ fow. fow.tid = t) = [], p1(l0) = fowl1 + fowl2, l0 ≠ l, ∀ l0. l0 ≠ l → p0(l0).filter(.W?).filter(λ fow. fow.tid = t) = [], ∀ l0, t0. p(l0).filter(.W?).count(λ fow. fow.tid = t0) ≤ 1, ∃ a. a ∈ fowl1.filter(.W?).filter(λ fow. fow.tid = t) ⊦

Rule argument

Additional information

Used terms: fowl1.filter(.W?).filter(λ fow. fow.tid = t)

Proof step 14 from proof relyp-one-pending-stable (previous step) (back to tree)

A spec-lemma

Proof step 15 from proof relyp-one-pending-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  fowl + fowl1 = p0(l0), fowl2.filter(λ fow0. fow0.tid = fow.tid) = [], p1(l0) = fowl1 + fowl2, l0 ≠ l, fow.W?, fow ∈ fowl1, ∀ l0. l0 ≠ l → p0(l0).filter(.W?).filter(λ fow0. fow0.tid = fow.tid) = [], ∀ l0, t0. p(l0).filter(.W?).count(λ fow. fow.tid = t0) ≤ 1 ⊦

Rule argument

Additional information

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

Proof step 16 from proof relyp-one-pending-stable (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 17:

  fowl + fowl1 = p0(l0), fowl2.filter(λ fow0. fow0.tid = fow.tid) = [], p1(l0) = fowl1 + fowl2, l0 ≠ l, fow.W?, fow ∈ fowl1, l0 ≠ l → p0(l0).filter(.W?).filter(λ fow0. fow0.tid = fow.tid) = [], ∀ l0, t0. p(l0).filter(.W?).count(λ fow. fow.tid = t0) ≤ 1 ⊦

Rule argument

Additional information

Used terms: l0

Proof step 17 from proof relyp-one-pending-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  fowl + fowl1 = p0(l0), fowl2.filter(λ fow0. fow0.tid = fow.tid) = [], fowl.filter(.W?).filter(λ fow0. fow0.tid = fow.tid) = [], fowl1.filter(.W?).filter(λ fow0. fow0.tid = fow.tid) = [], p1(l0) = fowl1 + fowl2, l0 ≠ l, fow.W?, fow ∈ fowl1, ∀ l0, t0. p(l0).filter(.W?).count(λ fow. fow.tid = t0) ≤ 1 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ (x + y).filter(p) = x.filter(p) + y.filter(p); (s)

Proof step 18 from proof relyp-one-pending-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 + fowl1 = p0(l0), fowl.filter(.W?).filter(λ fow0. fow0.tid = fow.tid) = [], fowl2.filter(λ fow0. fow0.tid = fow.tid) = [], p1(l0) = fowl1 + fowl2, l0 ≠ l, fow.W?, fow ∈ fowl1, ∀ l0, t0. p(l0).filter(.W?).count(λ fow. fow.tid = t0) ≤ 1, ∀ a. ¬ a ∈ fowl1.filter(.W?).filter(λ fow0. fow0.tid = fow.tid) ⊦

Rule argument

Additional information

Used terms: fowl1.filter(.W?).filter(λ fow0. fow0.tid = fow.tid)

Proof step 19 from proof relyp-one-pending-stable (previous step) (back to tree)

A spec-lemma

Proof step 20 from proof relyp-one-pending-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  fowl + fowl1 = p0(l0), fowl2.filter(λ fow0. fow0.tid = fow.tid) = [], fowl.filter(.W?).filter(λ fow0. fow0.tid = fow.tid) = [], p1(l0) = fowl1 + fowl2, l0 ≠ l, fow.W?, fow ∈ fowl1, ∀ l0, t0. p(l0).filter(.W?).count(λ fow. fow.tid = t0) ≤ 1, ∀ a. ¬ a ∈ fowl1 ∨ ¬ a.W? ∨ a.tid ≠ fow.tid ⊦

Rule argument

Additional information

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

Proof step 21 from proof relyp-one-pending-stable (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: fow

Proof step 22 from proof relyp-one-pending-stable (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 23:

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

• Proof step 24:

  fowl + fowl1 = p0(l0), fowl2.filter(λ fow. fow.tid = t) = [], p1(l0) = fowl1 + fowl2, l0 ≠ l, ∀ l0. l0 ≠ l → p0(l0).filter(.W?).filter(λ fow. fow.tid = t) = [], ∀ l0, t0. p(l0).filter(.W?).count(λ fow. fow.tid = t0) ≤ 1, ∃ a. a ∈ fowl2.filter(.W?).filter(λ fow. fow.tid = t) ⊦

Rule argument

Additional information

Used terms: fowl2.filter(.W?).filter(λ fow. fow.tid = t)

Proof step 23 from proof relyp-one-pending-stable (previous step) (back to tree)

A spec-lemma

Proof step 24 from proof relyp-one-pending-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  fowl + fowl1 = p0(l0), fowl2.filter(λ fow0. fow0.tid = fow.tid) = [], p1(l0) = fowl1 + fowl2, l0 ≠ l, fow.W?, fow ∈ fowl2, ∀ l0. l0 ≠ l → p0(l0).filter(.W?).filter(λ fow0. fow0.tid = fow.tid) = [], ∀ l0, t0. p(l0).filter(.W?).count(λ fow. fow.tid = t0) ≤ 1 ⊦

Rule argument

Additional information

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

Proof step 25 from proof relyp-one-pending-stable (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 26:

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

• Proof step 27:

  fowl + fowl1 = p0(l0), p1(l0) = fowl1 + fowl2, l0 ≠ l, fow.W?, fow ∈ fowl2, ∀ l0, t0. p(l0).filter(.W?).count(λ fow. fow.tid = t0) ≤ 1, ∀ l0. l0 ≠ l → p0(l0).filter(.W?).filter(λ fow0. fow0.tid = fow.tid) = [], ∀ a. ¬ a ∈ fowl2.filter(λ fow0. fow0.tid = fow.tid) ⊦

Rule argument

Additional information

Used terms: fowl2.filter(λ fow0. fow0.tid = fow.tid)

Proof step 26 from proof relyp-one-pending-stable (previous step) (back to tree)

A spec-lemma

Proof step 27 from proof relyp-one-pending-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  fowl + fowl1 = p0(l0), p1(l0) = fowl1 + fowl2, l0 ≠ l, fow.W?, fow ∈ fowl2, ∀ l0. l0 ≠ l → p0(l0).filter(.W?).filter(λ fow0. fow0.tid = fow.tid) = [], ∀ l0, t0. p(l0).filter(.W?).count(λ fow. fow.tid = t0) ≤ 1, ∀ a. ¬ a ∈ fowl2 ∨ a.tid ≠ fow.tid ⊦

Rule argument

Additional information

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

Proof step 28 from proof relyp-one-pending-stable (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: fow