Proof step 1 from proof rely-fo-follows-w-stable (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  FOFollowsW(t, p0(l)), rely(t, p0, p1), ¬ FOFollowsW(t, p1(l)) ⊦

Rule argument

Additional information

Proof step 2 from proof rely-fo-follows-w-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  FOFollowsW(t, p0(l)), ¬ FOFollowsW(t, p1(l)), ∀ l0. ∃ fowl1, fowl2. (∃ fowl2, fowl3, fowl4, fowl5. p0(l0) = fowl2 + fowl3 + fowl4 ∧ fowl5 ⊆ fowl3 |FO ∧ fowl1 = fowl5 + fowl4) ∧ p1(l0) = fowl1 + fowl2 ∧ fowl2 | t = [] ⊦

Rule argument

Additional information

Used simplifier rules: allrely-def: ⊦ rely(t, p, p0) ↔ (∀ l. rely(t, p(l), p0(l))); rely-def: ⊦ rely(t, fowl, fowl0) ↔ (∃ fowl1, fowl2. fowl ⊒W fowl1 ∧ fowl0 = fowl1 + fowl2 ∧ fowl2 | t = []); weak-write-postfix: ⊦ fowl0 ⊒W fowl1 ↔ (∃ fowl2, fowl3, fowl4, fowl5. fowl0 = fowl2 + fowl3 + fowl4 ∧ fowl5 ⊆ fowl3 |FO ∧ fowl1 = fowl5 + fowl4);

Proof step 3 from proof rely-fo-follows-w-stable (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 4:

  FOFollowsW(t, p0(l)), ¬ FOFollowsW(t, p1(l)), ∃ fowl1, fowl2. (∃ fowl2, fowl3, fowl4, fowl5. p0(l) = fowl2 + fowl3 + fowl4 ∧ fowl5 ⊆ fowl3 |FO ∧ fowl1 = fowl5 + fowl4) ∧ p1(l) = fowl1 + fowl2 ∧ fowl2 | t = [] ⊦

Rule argument

Additional information

Used terms: l

Proof step 4 from proof rely-fo-follows-w-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  p0(l) = fowl + fowl3 + fowl4, p1(l) = (fowl5 + fowl4) + fowl2, fowl2 | t = [], FOFollowsW(t, p0(l)), fowl5 ⊆ fowl3 |FO, ¬ FOFollowsW(t, p1(l)) ⊦

Rule argument

Additional information

Proof step 5 from proof rely-fo-follows-w-stable (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ FOFollowsW(t, fowl) ↔ (∀ n. n < # fowl ∧ fowl[n].W? ∧ fowl[n].tid = t → (∃ n0. n < n0 ∧ n0 < # fowl ∧ fowl[n0] = FO(t)))

• Proof step 7:

  p0(l) = fowl + fowl3 + fowl4, p1(l) = (fowl5 + fowl4) + fowl2, fowl2 | t = [], fowl5 ⊆ fowl3 |FO, ¬ FOFollowsW(t, p1(l)), ∀ n. n < # p0(l) ∧ p0(l)[n].W? ∧ p0(l)[n].tid = t → (∃ n0. n < n0 ∧ n0 < # p0(l) ∧ p0(l)[n0] = FO(t)) ⊦

Rule argument

Additional information

Used terms: t, p0(l)

Proof step 6 from proof rely-fo-follows-w-stable (previous step) (back to tree)

A spec-lemma

Proof step 7 from proof rely-fo-follows-w-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  p0(l) = fowl + fowl3 + fowl4, p1(l) = (fowl5 + fowl4) + fowl2, fowl2 | t = [], fowl5 ⊆ fowl3 |FO, ¬ FOFollowsW(t, p1(l)), ∀ n. n < # p0(l) ∧ p0(l)[n].W? ∧ p0(l)[n].tid = t → (∃ n0. n < n0 ∧ n0 < # p0(l) ∧ p0(l)[n0] = FO(p0(l)[n].tid)) ⊦

Rule argument

Additional information

Proof step 8 from proof rely-fo-follows-w-stable (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ FOFollowsW(t, fowl) ↔ (∀ n. n < # fowl ∧ fowl[n].W? ∧ fowl[n].tid = t → (∃ n0. n < n0 ∧ n0 < # fowl ∧ fowl[n0] = FO(t)))

• Proof step 10:

  p0(l) = fowl + fowl3 + fowl4, p1(l) = (fowl5 + fowl4) + fowl2, fowl2 | t = [], fowl5 ⊆ fowl3 |FO, ∀ n. n < # p0(l) ∧ p0(l)[n].W? ∧ p0(l)[n].tid = t → (∃ n0. n < n0 ∧ n0 < # p0(l) ∧ p0(l)[n0] = FO(p0(l)[n].tid)), ∃ n. ¬(n < # p1(l) ∧ p1(l)[n].W? ∧ p1(l)[n].tid = t → (∃ n0. n < n0 ∧ n0 < # p1(l) ∧ p1(l)[n0] = FO(t))) ⊦

Rule argument

Additional information

Used terms: t, p1(l)

Proof step 9 from proof rely-fo-follows-w-stable (previous step) (back to tree)

A spec-lemma

Proof step 10 from proof rely-fo-follows-w-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  p0(l) = fowl + fowl3 + fowl4, p1(l) = (fowl5 + fowl4) + fowl2, fowl2 | p1(l)[n].tid = [], p1(l) ≠ [], p1(l)[n].W?, n < # p1(l), fowl5 ⊆ fowl3 |FO, ∀ n0. n0 < # p0(l) ∧ p0(l)[n0].W? ∧ p0(l)[n0].tid = p1(l)[n].tid → (∃ n1. n0 < n1 ∧ n1 < # p0(l) ∧ p0(l)[n1] = FO(p0(l)[n0].tid)) ⊦ ∃ n0. n < n0 ∧ n0 < # p1(l) ∧ p1(l)[n0] = FO(p1(l)[n].tid)

Rule argument

Additional information

Used simplifier rules: ⊦ # x = 0 ↔ x = []; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 11 from proof rely-fo-follows-w-stable (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 12:

  p1(l)[n] = W(v, t), p0(l) = fowl + fowl3 + fowl4, p1(l) = (fowl5 + fowl4) + fowl2, fowl2 | t = [], p1(l) ≠ [], p1(l)[n].W?, n < # p1(l), fowl5 ⊆ fowl3 |FO, ∀ n0. n0 < # p0(l) ∧ p0(l)[n0].W? ∧ p0(l)[n0].tid = t → (∃ n1. n0 < n1 ∧ n1 < # p0(l) ∧ p0(l)[n1] = FO(p0(l)[n0].tid)) ⊦ ∃ n0. n < n0 ∧ n0 < # p1(l) ∧ p1(l)[n0] = FO(t)

Rule argument

Additional information

Used simplifier rules: ⊦ fow.W? → (val = fow.val ∧ tid = fow.tid ↔ fow = W(val, tid)); (elim) Used terms: p1(l)[n], v, t

Proof step 12 from proof rely-fo-follows-w-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  p1(l)[n] = W(v, t), p0(l) = fowl + fowl3 + fowl4, p1(l) = (fowl5 + fowl4) + fowl2, fowl2 | t = [], p1(l) ≠ [], n < # p1(l), fowl5 ⊆ fowl3 |FO, ∀ n0. n0 < # p0(l) ∧ p0(l)[n0].W? ∧ p0(l)[n0].tid = t → (∃ n1. n0 < n1 ∧ n1 < # p0(l) ∧ p0(l)[n1] = FO(p0(l)[n0].tid)) ⊦ ∃ n0. n < n0 ∧ n0 < # p1(l) ∧ p1(l)[n0] = FO(t)

Rule argument

Additional information

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

Proof step 13 from proof rely-fo-follows-w-stable (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 14:

  ((fowl5 + fowl4) + fowl2)[n] = W(v, t), p0(l) = fowl + fowl3 + fowl4, fowl2 | t = [], (fowl5 + fowl4) + fowl2 ≠ [], n < #((fowl5 + fowl4) + fowl2), fowl5 ⊆ fowl3 |FO, ∀ n0. n0 < # p0(l) ∧ p0(l)[n0].W? ∧ p0(l)[n0].tid = t → (∃ n1. n0 < n1 ∧ n1 < # p0(l) ∧ p0(l)[n1] = FO(p0(l)[n0].tid)) ⊦ ∃ n0. n < n0 ∧ n0 < #((fowl5 + fowl4) + fowl2) ∧ ((fowl5 + fowl4) + fowl2)[n0] = FO(t)

Rule argument

Additional information

Proof step 14 from proof rely-fo-follows-w-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  ((fowl5 + fowl4) + fowl2)[n] = W(v, t), p0(l) = fowl + fowl3 + fowl4, fowl2 | t = [], n < # fowl5 + # fowl4 + # fowl2, fowl5 ⊆ fowl3 |FO, ∀ n0. n0 < # p0(l) ∧ p0(l)[n0].W? ∧ p0(l)[n0].tid = t → (∃ n1. n0 < n1 ∧ n1 < # p0(l) ∧ p0(l)[n1] = FO(p0(l)[n0].tid)) ⊦ ∃ n0. n < n0 ∧ n0 < # fowl5 + # fowl4 + # fowl2 ∧ ((fowl5 + fowl4) + fowl2)[n0] = FO(t), fowl5 = [] ∧ fowl4 = [] ∧ fowl2 = []

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ #(x + y) = # x + # y; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s)

Proof step 15 from proof rely-fo-follows-w-stable (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

  ⊦ n < # x → (x + y)[n] = x[n]

• Proof step 17:

  ((fowl5 + fowl4) + fowl2)[n] = W(v, t), p0(l) = fowl + fowl3 + fowl4, fowl2 | t = [], n < # fowl5 + # fowl4 + # fowl2, fowl5 ⊆ fowl3 |FO, ¬ n < #(fowl5 + fowl4), ∀ n0. n0 < # p0(l) ∧ p0(l)[n0].W? ∧ p0(l)[n0].tid = t → (∃ n1. n0 < n1 ∧ n1 < # p0(l) ∧ p0(l)[n1] = FO(p0(l)[n0].tid)) ⊦ ∃ n0. n < n0 ∧ n0 < # fowl5 + # fowl4 + # fowl2 ∧ ((fowl5 + fowl4) + fowl2)[n0] = FO(t), fowl5 = [] ∧ fowl4 = [] ∧ fowl2 = []

• Proof step 29:

  (fowl5 + fowl4)[n] = W(v, t), p0(l) = fowl + fowl3 + fowl4, fowl2 | t = [], n < # fowl5 + # fowl4 + # fowl2, n < #(fowl5 + fowl4), fowl5 ⊆ fowl3 |FO, ∀ n0. n0 < # p0(l) ∧ p0(l)[n0].W? ∧ p0(l)[n0].tid = t → (∃ n1. n0 < n1 ∧ n1 < # p0(l) ∧ p0(l)[n1] = FO(p0(l)[n0].tid)) ⊦ ∃ n0. n < n0 ∧ n0 < # fowl5 + # fowl4 + # fowl2 ∧ ((fowl5 + fowl4) + fowl2)[n0] = FO(t), fowl5 = [] ∧ fowl4 = [] ∧ fowl2 = []

Rule argument

Additional information

Used terms: fowl5 + fowl4, fowl2, n

Proof step 16 from proof rely-fo-follows-w-stable (previous step) (back to tree)

A spec-lemma

Proof step 17 from proof rely-fo-follows-w-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  fowl2[n - # fowl5 + # fowl4] = W(v, t), p0(l) = fowl + fowl3 + fowl4, fowl2 | t = [], fowl2 ≠ [], n < # fowl5 + # fowl4 + # fowl2, # fowl5 + # fowl4 ≤ n, fowl5 ⊆ fowl3 |FO, ∀ n0. n0 < # p0(l) ∧ p0(l)[n0].W? ∧ p0(l)[n0].tid = t → (∃ n1. n0 < n1 ∧ n1 < # p0(l) ∧ p0(l)[n1] = FO(p0(l)[n0].tid)) ⊦ ∃ n0. n < n0 ∧ n0 < # fowl5 + # fowl4 + # fowl2 ∧ ((fowl5 + fowl4) + fowl2)[n0] = FO(t)

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ # x = 0 ↔ x = []; (s) ⊦ m < m + n ↔ n ≠ 0; (s) ⊦ m + n < m + n0 ↔ n < n0; (s) fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat ⊦ m < n ↔ ¬ n ≤ m; (ss) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ #(x + y) = # x + # y; (s) ⊦ ¬ n < # x → (x + y)[n] = y[n - # x]; (s)

Proof step 18 from proof rely-fo-follows-w-stable (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 19:

  fowl2[n2] = W(v, t), n = n2 + # fowl5 + # fowl4, p0(l) = fowl + fowl3 + fowl4, fowl2 | t = [], fowl2 ≠ [], n < # fowl5 + # fowl4 + # fowl2, # fowl5 + # fowl4 ≤ n, fowl5 ⊆ fowl3 |FO, ∀ n0. n0 < # p0(l) ∧ p0(l)[n0].W? ∧ p0(l)[n0].tid = t → (∃ n1. n0 < n1 ∧ n1 < # p0(l) ∧ p0(l)[n1] = FO(p0(l)[n0].tid)) ⊦ ∃ n0. n < n0 ∧ n0 < # fowl5 + # fowl4 + # fowl2 ∧ ((fowl5 + fowl4) + fowl2)[n0] = FO(t)

Rule argument

Additional information

Used simplifier rules: n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: n, # fowl5 + # fowl4, n2

Proof step 19 from proof rely-fo-follows-w-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  fowl2[n2] = W(v, t), p0(l) = fowl + fowl3 + fowl4, fowl2 | t = [], fowl2 ≠ [], n2 < # fowl2, fowl5 ⊆ fowl3 |FO, ∀ n0. n0 < # p0(l) ∧ p0(l)[n0].W? ∧ p0(l)[n0].tid = t → (∃ n1. n0 < n1 ∧ n1 < # p0(l) ∧ p0(l)[n1] = FO(p0(l)[n0].tid)) ⊦ ∃ n0. n2 + # fowl5 + # fowl4 < n0 ∧ n0 < # fowl5 + # fowl4 + # fowl2 ∧ ((fowl5 + fowl4) + fowl2)[n0] = FO(t)

Rule argument

Additional information

Used simplifier rules: ⊦ # x = 0 ↔ x = []; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ m ≤ m + n; (s) ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s)

Proof step 20 from proof rely-fo-follows-w-stable (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

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

• Proof step 22:

  fowl2[n2] = W(v, t), p0(l) = fowl + fowl3 + fowl4, fowl2 ≠ [], n2 < # fowl2, fowl5 ⊆ fowl3 |FO, ∀ n0. n0 < # p0(l) ∧ p0(l)[n0].W? ∧ p0(l)[n0].tid = t → (∃ n1. n0 < n1 ∧ n1 < # p0(l) ∧ p0(l)[n1] = FO(p0(l)[n0].tid)), ∀ a. ¬ a ∈ fowl2 | t ⊦ ∃ n0. n2 + # fowl5 + # fowl4 < n0 ∧ n0 < # fowl5 + # fowl4 + # fowl2 ∧ ((fowl5 + fowl4) + fowl2)[n0] = FO(t)

Rule argument

Additional information

Used terms: fowl2 | t

Proof step 21 from proof rely-fo-follows-w-stable (previous step) (back to tree)

A spec-lemma

Proof step 22 from proof rely-fo-follows-w-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  fowl2[n2] = W(v, t), p0(l) = fowl + fowl3 + fowl4, fowl2 ≠ [], n2 < # fowl2, fowl5 ⊆ fowl3 |FO, ∀ n0. n0 < # p0(l) ∧ p0(l)[n0].W? ∧ p0(l)[n0].tid = t → (∃ n1. n0 < n1 ∧ n1 < # p0(l) ∧ p0(l)[n1] = FO(p0(l)[n0].tid)), ∀ a. ¬ a ∈ fowl2 ∨ a.tid ≠ t ⊦ ∃ n0. n2 + # fowl5 + # fowl4 < n0 ∧ n0 < # fowl5 + # fowl4 + # fowl2 ∧ ((fowl5 + fowl4) + fowl2)[n0] = FO(t)

Rule argument

Additional information

Used simplifier rules: ⊦ fow ∈ fowl | t ↔ fow ∈ fowl ∧ fow.tid = t; (s)

Proof step 23 from proof rely-fo-follows-w-stable (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 24:

  fowl2[n2] = W(v, t), p0(l) = fowl + fowl3 + fowl4, fowl2 ≠ [], n2 < # fowl2, fowl5 ⊆ fowl3 |FO, ∀ n0. n0 < # p0(l) ∧ p0(l)[n0].W? ∧ p0(l)[n0].tid = t → (∃ n1. n0 < n1 ∧ n1 < # p0(l) ∧ p0(l)[n1] = FO(p0(l)[n0].tid)), ¬ W(v, t) ∈ fowl2 ∨ W(v, t).tid ≠ t ⊦ ∃ n0. n2 + # fowl5 + # fowl4 < n0 ∧ n0 < # fowl5 + # fowl4 + # fowl2 ∧ ((fowl5 + fowl4) + fowl2)[n0] = FO(t)

Rule argument

Additional information

Used terms: W(v, t)

Proof step 24 from proof rely-fo-follows-w-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  fowl2[n2] = W(v, t), p0(l) = fowl + fowl3 + fowl4, fowl2 ≠ [], n2 < # fowl2, fowl5 ⊆ fowl3 |FO, ¬ W(v, t) ∈ fowl2, ∀ n0. n0 < # p0(l) ∧ p0(l)[n0].W? ∧ p0(l)[n0].tid = t → (∃ n1. n0 < n1 ∧ n1 < # p0(l) ∧ p0(l)[n1] = FO(p0(l)[n0].tid)) ⊦ ∃ n0. n2 + # fowl5 + # fowl4 < n0 ∧ n0 < # fowl5 + # fowl4 + # fowl2 ∧ ((fowl5 + fowl4) + fowl2)[n0] = FO(t)

Rule argument

Additional information

Used simplifier rules: ⊦ W(v, tid).tid = tid; (s)

Proof step 25 from proof rely-fo-follows-w-stable (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 26:

  ⊦ a ∈ x ↔ (∃ n. n < # x ∧ x[n] = a)

• Proof step 27:

  fowl2[n2] = W(v, t), p0(l) = fowl + fowl3 + fowl4, fowl2 ≠ [], n2 < # fowl2, fowl5 ⊆ fowl3 |FO, ∀ n0. n0 < # p0(l) ∧ p0(l)[n0].W? ∧ p0(l)[n0].tid = t → (∃ n1. n0 < n1 ∧ n1 < # p0(l) ∧ p0(l)[n1] = FO(p0(l)[n0].tid)), ∀ n. ¬(n < # fowl2 ∧ fowl2[n] = W(v, t)) ⊦ ∃ n0. n2 + # fowl5 + # fowl4 < n0 ∧ n0 < # fowl5 + # fowl4 + # fowl2 ∧ ((fowl5 + fowl4) + fowl2)[n0] = FO(t)

Rule argument

Additional information

Used terms: W(v, t), fowl2

Proof step 26 from proof rely-fo-follows-w-stable (previous step) (back to tree)

A spec-lemma

Proof step 27 from proof rely-fo-follows-w-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  fowl2[n2] = W(v, t), p0(l) = fowl + fowl3 + fowl4, fowl2 ≠ [], n2 < # fowl2, fowl5 ⊆ fowl3 |FO, ∀ n0. n0 < # p0(l) ∧ p0(l)[n0].W? ∧ p0(l)[n0].tid = t → (∃ n1. n0 < n1 ∧ n1 < # p0(l) ∧ p0(l)[n1] = FO(p0(l)[n0].tid)), ∀ n. ¬ n < # fowl2 ∨ fowl2[n] ≠ W(v, t) ⊦ ∃ n0. n2 + # fowl5 + # fowl4 < n0 ∧ n0 < # fowl5 + # fowl4 + # fowl2 ∧ ((fowl5 + fowl4) + fowl2)[n0] = FO(t)

Rule argument

Additional information

Proof step 28 from proof rely-fo-follows-w-stable (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: n2

Proof step 29 from proof rely-fo-follows-w-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

  (fowl5 + fowl4)[n] = W(v, t), p0(l) = fowl + fowl3 + fowl4, fowl2 | t = [], n < # fowl5 + # fowl4, n < # fowl5 + # fowl4 + # fowl2, fowl5 ⊆ fowl3 |FO, ∀ n0. n0 < # p0(l) ∧ p0(l)[n0].W? ∧ p0(l)[n0].tid = t → (∃ n1. n0 < n1 ∧ n1 < # p0(l) ∧ p0(l)[n1] = FO(p0(l)[n0].tid)) ⊦ ∃ n0. n < n0 ∧ n0 < # fowl5 + # fowl4 + # fowl2 ∧ ((fowl5 + fowl4) + fowl2)[n0] = FO(t), fowl5 = [] ∧ fowl4 = [] ∧ fowl2 = []

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ #(x + y) = # x + # y; (s)

Proof step 30 from proof rely-fo-follows-w-stable (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 31:

  ⊦ n < # x → (x + y)[n] = x[n]

• Proof step 32:

  (fowl5 + fowl4)[n] = W(v, t), p0(l) = fowl + fowl3 + fowl4, fowl2 | t = [], n < # fowl5 + # fowl4 + # fowl2, n < # fowl5 + # fowl4, fowl5 ⊆ fowl3 |FO, ¬ n < # fowl5, ∀ n0. n0 < # p0(l) ∧ p0(l)[n0].W? ∧ p0(l)[n0].tid = t → (∃ n1. n0 < n1 ∧ n1 < # p0(l) ∧ p0(l)[n1] = FO(p0(l)[n0].tid)) ⊦ ∃ n0. n < n0 ∧ n0 < # fowl5 + # fowl4 + # fowl2 ∧ ((fowl5 + fowl4) + fowl2)[n0] = FO(t), fowl5 = [] ∧ fowl4 = [] ∧ fowl2 = []

• Proof step 50:

  fowl5[n] = W(v, t), p0(l) = fowl + fowl3 + fowl4, fowl2 | t = [], n < # fowl5 + # fowl4 + # fowl2, n < # fowl5 + # fowl4, n < # fowl5, fowl5 ⊆ fowl3 |FO, ∀ n0. n0 < # p0(l) ∧ p0(l)[n0].W? ∧ p0(l)[n0].tid = t → (∃ n1. n0 < n1 ∧ n1 < # p0(l) ∧ p0(l)[n1] = FO(p0(l)[n0].tid)) ⊦ ∃ n0. n < n0 ∧ n0 < # fowl5 + # fowl4 + # fowl2 ∧ ((fowl5 + fowl4) + fowl2)[n0] = FO(t), fowl5 = [] ∧ fowl4 = [] ∧ fowl2 = []

Rule argument

Additional information

Used terms: fowl5, fowl4, n

Proof step 31 from proof rely-fo-follows-w-stable (previous step) (back to tree)

A spec-lemma

Proof step 32 from proof rely-fo-follows-w-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

  fowl4[n - # fowl5] = W(v, t), p0(l) = fowl + fowl3 + fowl4, fowl2 | t = [], # fowl4 + # fowl2 ≠ 0, fowl4 ≠ [], n < # fowl5 + # fowl4 + # fowl2, n < # fowl5 + # fowl4, # fowl5 ≤ n, fowl5 ⊆ fowl3 |FO, ∀ n0. n0 < # p0(l) ∧ p0(l)[n0].W? ∧ p0(l)[n0].tid = t → (∃ n1. n0 < n1 ∧ n1 < # p0(l) ∧ p0(l)[n1] = FO(p0(l)[n0].tid)) ⊦ ∃ n0. n < n0 ∧ n0 < # fowl5 + # fowl4 + # fowl2 ∧ ((fowl5 + fowl4) + fowl2)[n0] = FO(t)

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ # x = 0 ↔ x = []; (s) ⊦ m < m + n ↔ n ≠ 0; (s) fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat ⊦ m < n ↔ ¬ n ≤ m; (ss) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ ¬ n < # x → (x + y)[n] = y[n - # x]; (s)

Proof step 33 from proof rely-fo-follows-w-stable (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 34:

  fowl4[n2] = W(v, t), n = n2 + # fowl5, p0(l) = fowl + fowl3 + fowl4, fowl2 | t = [], # fowl4 + # fowl2 ≠ 0, fowl4 ≠ [], n < # fowl5 + # fowl4, n < # fowl5 + # fowl4 + # fowl2, # fowl5 ≤ n, fowl5 ⊆ fowl3 |FO, ∀ n0. n0 < # p0(l) ∧ p0(l)[n0].W? ∧ p0(l)[n0].tid = t → (∃ n1. n0 < n1 ∧ n1 < # p0(l) ∧ p0(l)[n1] = FO(p0(l)[n0].tid)) ⊦ ∃ n0. n < n0 ∧ n0 < # fowl5 + # fowl4 + # fowl2 ∧ ((fowl5 + fowl4) + fowl2)[n0] = FO(t)

Rule argument

Additional information

Used simplifier rules: n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: n, # fowl5, n2

Proof step 34 from proof rely-fo-follows-w-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

  fowl4[n2] = W(v, t), p0(l) = fowl + fowl3 + fowl4, fowl2 | t = [], # fowl4 + # fowl2 ≠ 0, fowl4 ≠ [], n2 < # fowl4, fowl5 ⊆ fowl3 |FO, ∀ n0. n0 < # p0(l) ∧ p0(l)[n0].W? ∧ p0(l)[n0].tid = t → (∃ n1. n0 < n1 ∧ n1 < # p0(l) ∧ p0(l)[n1] = FO(p0(l)[n0].tid)) ⊦ ∃ n0. n2 + # fowl5 < n0 ∧ n0 < # fowl5 + # fowl4 + # fowl2 ∧ ((fowl5 + fowl4) + fowl2)[n0] = FO(t)

Rule argument

Additional information

Used simplifier rules: ⊦ # x = 0 ↔ x = []; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ m + n < m0 → m + n < m0 + n0; (s) ⊦ m ≤ m + n; (s)

Proof step 35 from proof rely-fo-follows-w-stable (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 36:

  fowl4[n2] = W(v, t), fowl2 | t = [], # fowl4 + # fowl2 ≠ 0, fowl4 ≠ [], n2 < # fowl4, fowl5 ⊆ fowl3 |FO, ∀ n0. n0 < #(fowl + fowl3 + fowl4) ∧ (fowl + fowl3 + fowl4)[n0].W? ∧ (fowl + fowl3 + fowl4)[n0].tid = t → (∃ n1. n0 < n1 ∧ n1 < #(fowl + fowl3 + fowl4) ∧ (fowl + fowl3 + fowl4)[n1] = FO((fowl + fowl3 + fowl4)[n0].tid)) ⊦ ∃ n0. n2 + # fowl5 < n0 ∧ n0 < # fowl5 + # fowl4 + # fowl2 ∧ ((fowl5 + fowl4) + fowl2)[n0] = FO(t)

Rule argument

Additional information

Proof step 36 from proof rely-fo-follows-w-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 37:

  fowl4[n2] = W(v, t), fowl2 | t = [], # fowl4 + # fowl2 ≠ 0, fowl4 ≠ [], n2 < # fowl4, fowl5 ⊆ fowl3 |FO, ∀ n0. n0 < # fowl + # fowl3 + # fowl4 ∧ (fowl + fowl3 + fowl4)[n0].W? ∧ (fowl + fowl3 + fowl4)[n0].tid = t → (∃ n1. n0 < n1 ∧ n1 < # fowl + # fowl3 + # fowl4 ∧ (fowl + fowl3 + fowl4)[n1] = FO((fowl + fowl3 + fowl4)[n0].tid)) ⊦ ∃ n0. n2 + # fowl5 < n0 ∧ n0 < # fowl5 + # fowl4 + # fowl2 ∧ ((fowl5 + fowl4) + fowl2)[n0] = FO(t)

Rule argument

Additional information

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

Proof step 37 from proof rely-fo-follows-w-stable (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 38:

  fowl4[n2] = W(v, t), fowl2 | t = [], # fowl4 + # fowl2 ≠ 0, fowl4 ≠ [], n2 < # fowl4, fowl5 ⊆ fowl3 |FO, # fowl + # fowl3 + n2 < # fowl + # fowl3 + # fowl4 ∧ (fowl + fowl3 + fowl4)[# fowl + # fowl3 + n2].W? ∧ (fowl + fowl3 + fowl4)[# fowl + # fowl3 + n2].tid = t → (∃ n1. # fowl + # fowl3 + n2 < n1 ∧ n1 < # fowl + # fowl3 + # fowl4 ∧ (fowl + fowl3 + fowl4)[n1] = FO((fowl + fowl3 + fowl4)[# fowl + # fowl3 + n2].tid)) ⊦ ∃ n0. n2 + # fowl5 < n0 ∧ n0 < # fowl5 + # fowl4 + # fowl2 ∧ ((fowl5 + fowl4) + fowl2)[n0] = FO(t)

Rule argument

Additional information

Used terms: # fowl + # fowl3 + n2

Proof step 38 from proof rely-fo-follows-w-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 39:

  (fowl + fowl3 + fowl4)[n1] = FO(t), fowl4[n2] = W(v, t), fowl2 | t = [], # fowl4 + # fowl2 ≠ 0, fowl4 ≠ [], n1 < # fowl + # fowl3 + # fowl4, # fowl + # fowl3 + n2 < n1, n2 + 1 < # fowl4, n2 < # fowl4, fowl5 ⊆ fowl3 |FO ⊦ ∃ n0. n2 + # fowl5 < n0 ∧ n0 < # fowl5 + # fowl4 + # fowl2 ∧ ((fowl5 + fowl4) + fowl2)[n0] = FO(t)

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ m +1 = m + 1; (s) ⊦ m < n → n ≠ 0; (s) trans-Nat: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ W(v, tid).tid = tid; (s) ⊦ W(v, tid).W?; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (x + y)[n + # x] = y[n]; (s)

Proof step 39 from proof rely-fo-follows-w-stable (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 40:

  ⊦ ¬ n < # x → (x + y)[n] = y[n - # x]

• Proof step 41:

  fowl4[n2] = W(v, t), (fowl3 + fowl4)[n1 - # fowl] = FO(t), fowl2 | t = [], # fowl4 + # fowl2 ≠ 0, fowl4 ≠ [], n2 < # fowl4, n2 + 1 < # fowl4, # fowl + # fowl3 + n2 < n1, n1 < # fowl + # fowl3 + # fowl4, fowl5 ⊆ fowl3 |FO, ¬ n1 < # fowl ⊦ ∃ n0. n2 + # fowl5 < n0 ∧ n0 < # fowl5 + # fowl4 + # fowl2 ∧ ((fowl5 + fowl4) + fowl2)[n0] = FO(t)

Rule argument

Additional information

Used simplifier rules: ⊦ n < # x → (x + y)[n] = x[n]; (s) a: ⊦ (x + y) + z = x + y + z; from specification list f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic trans-Nat: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic ⊦ # x = 0 ↔ x = []; (s) ⊦ m +1 = m + 1; (s) ⊦ m + m0 < n → ¬ n + n0 < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: n1, fowl, fowl3 + fowl4

Proof step 40 from proof rely-fo-follows-w-stable (previous step) (back to tree)

A spec-lemma

Proof step 41 from proof rely-fo-follows-w-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 42:

  fowl4[n2] = W(v, t), (fowl3 + fowl4)[n1 - # fowl] = FO(t), fowl2 | t = [], # fowl4 + # fowl2 ≠ 0, # fowl3 + # fowl4 ≠ 0, fowl4 ≠ [], n2 < # fowl4, n2 + 1 < # fowl4, # fowl + # fowl3 + n2 < n1, n1 < # fowl + # fowl3 + # fowl4, # fowl ≤ n1, fowl5 ⊆ fowl3 |FO ⊦ ∃ n0. n2 + # fowl5 < n0 ∧ n0 < # fowl5 + # fowl4 + # fowl2 ∧ ((fowl5 + fowl4) + fowl2)[n0] = FO(t)

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m < m + n ↔ n ≠ 0; (s) fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 42 from proof rely-fo-follows-w-stable (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 43:

  (fowl3 + fowl4)[n3] = FO(t), fowl4[n2] = W(v, t), n1 = n3 + # fowl, fowl2 | t = [], # fowl4 + # fowl2 ≠ 0, # fowl3 + # fowl4 ≠ 0, fowl4 ≠ [], n1 < # fowl + # fowl3 + # fowl4, # fowl + # fowl3 + n2 < n1, n2 + 1 < # fowl4, n2 < # fowl4, # fowl ≤ n1, fowl5 ⊆ fowl3 |FO ⊦ ∃ n0. n2 + # fowl5 < n0 ∧ n0 < # fowl5 + # fowl4 + # fowl2 ∧ ((fowl5 + fowl4) + fowl2)[n0] = FO(t)

Rule argument

Additional information

Used simplifier rules: n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: n1, # fowl, n3

Proof step 43 from proof rely-fo-follows-w-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 44:

  (fowl3 + fowl4)[n3] = FO(t), fowl4[n2] = W(v, t), fowl2 | t = [], # fowl4 + # fowl2 ≠ 0, fowl4 ≠ [], n3 < # fowl3 + # fowl4, # fowl3 + n2 < n3, n2 + 1 < # fowl4, n2 < # fowl4, fowl5 ⊆ fowl3 |FO ⊦ ∃ n0. n2 + # fowl5 < n0 ∧ n0 < # fowl5 + # fowl4 + # fowl2 ∧ ((fowl5 + fowl4) + fowl2)[n0] = FO(t)

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ m +1 = m + 1; (s) ⊦ m < n → n ≠ 0; (s) trans-Nat: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m ≤ m + n; (s)

Proof step 44 from proof rely-fo-follows-w-stable (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 45:

  ⊦ ¬ n < # x → (x + y)[n] = y[n - # x]

• Proof step 46:

  fowl4[n2] = W(v, t), fowl4[n3 - # fowl3] = FO(t), fowl2 | t = [], # fowl4 + # fowl2 ≠ 0, fowl4 ≠ [], n2 < # fowl4, n2 + 1 < # fowl4, # fowl3 + n2 < n3, n3 < # fowl3 + # fowl4, fowl5 ⊆ fowl3 |FO, ¬ n3 < # fowl3 ⊦ ∃ n0. n2 + # fowl5 < n0 ∧ n0 < # fowl5 + # fowl4 + # fowl2 ∧ ((fowl5 + fowl4) + fowl2)[n0] = FO(t)

Rule argument

Additional information

Used simplifier rules: ⊦ n < # x → (x + y)[n] = x[n]; (s) a: ⊦ (x + y) + z = x + y + z; from specification list f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic trans-Nat: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic ⊦ # x = 0 ↔ x = []; (s) ⊦ m +1 = m + 1; (s) ⊦ m + m0 < n → ¬ n + n0 < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: n3, fowl3, fowl4

Proof step 45 from proof rely-fo-follows-w-stable (previous step) (back to tree)

A spec-lemma

Proof step 46 from proof rely-fo-follows-w-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 47:

  fowl4[n2] = W(v, t), fowl4[n3 - # fowl3] = FO(t), fowl2 | t = [], # fowl4 + # fowl2 ≠ 0, fowl4 ≠ [], n2 < # fowl4, n2 + 1 < # fowl4, # fowl3 + n2 < n3, n3 < # fowl3 + # fowl4, # fowl3 ≤ n3, fowl5 ⊆ fowl3 |FO ⊦ ∃ n0. n2 + # fowl5 < n0 ∧ n0 < # fowl5 + # fowl4 + # fowl2 ∧ ((fowl5 + fowl4) + fowl2)[n0] = FO(t)

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ # x = 0 ↔ x = []; (s) ⊦ m < m + n ↔ n ≠ 0; (s) fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 47 from proof rely-fo-follows-w-stable (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 48:

  fowl4[n1] = FO(t), fowl4[n2] = W(v, t), n3 = n1 + # fowl3, fowl2 | t = [], # fowl4 + # fowl2 ≠ 0, fowl4 ≠ [], n3 < # fowl3 + # fowl4, # fowl3 + n2 < n3, n2 + 1 < # fowl4, n2 < # fowl4, # fowl3 ≤ n3, fowl5 ⊆ fowl3 |FO ⊦ ∃ n0. n2 + # fowl5 < n0 ∧ n0 < # fowl5 + # fowl4 + # fowl2 ∧ ((fowl5 + fowl4) + fowl2)[n0] = FO(t)

Rule argument

Additional information

Used simplifier rules: n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: n3, # fowl3, n1

Proof step 48 from proof rely-fo-follows-w-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 49:

  fowl4[n1] = FO(t), fowl4[n2] = W(v, t), fowl2 | t = [], # fowl4 + # fowl2 ≠ 0, fowl4 ≠ [], n2 < # fowl4, n1 < # fowl4, n2 < n1, n2 + 1 < # fowl4, fowl5 ⊆ fowl3 |FO ⊦ ∃ n0. n2 + # fowl5 < n0 ∧ n0 < # fowl5 + # fowl4 + # fowl2 ∧ ((fowl5 + fowl4) + fowl2)[n0] = FO(t)

Rule argument

Additional information

Used simplifier rules: ⊦ m +1 = m + 1; (s) ⊦ m < n → n ≠ 0; (s) trans-Nat: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ m ≤ m + n; (s)

Proof step 49 from proof rely-fo-follows-w-stable (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ (x + y)[n + # x] = y[n]; (s) ⊦ n < # x → (x + y)[n] = x[n]; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ m < n ↔ ¬ n ≤ m; (ss) fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat ⊦ ¬ m + n < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: # fowl5 + n1

Proof step 50 from proof rely-fo-follows-w-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 51:

  fowl5[n] = W(v, t), p0(l) = fowl + fowl3 + fowl4, fowl2 | t = [], fowl5 ≠ [], n < # fowl5 + # fowl4 + # fowl2, n < # fowl5 + # fowl4, n < # fowl5, fowl5 ⊆ fowl3 |FO, ∀ n0. n0 < # p0(l) ∧ p0(l)[n0].W? ∧ p0(l)[n0].tid = t → (∃ n1. n0 < n1 ∧ n1 < # p0(l) ∧ p0(l)[n1] = FO(p0(l)[n0].tid)) ⊦ ∃ n0. n < n0 ∧ n0 < # fowl5 + # fowl4 + # fowl2 ∧ ((fowl5 + fowl4) + fowl2)[n0] = FO(t)

Rule argument

Additional information

Used simplifier rules: ⊦ # x = 0 ↔ x = []; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 51 from proof rely-fo-follows-w-stable (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 52:

  ⊦ x ⊆ y ↔ (∀ a. a ∈ x → a ∈ y)

• Proof step 53:

  fowl5[n] = W(v, t), p0(l) = fowl + fowl3 + fowl4, fowl2 | t = [], fowl5 ≠ [], n < # fowl5, n < # fowl5 + # fowl4, n < # fowl5 + # fowl4 + # fowl2, ∀ n0. n0 < # p0(l) ∧ p0(l)[n0].W? ∧ p0(l)[n0].tid = t → (∃ n1. n0 < n1 ∧ n1 < # p0(l) ∧ p0(l)[n1] = FO(p0(l)[n0].tid)), ∀ a. a ∈ fowl5 → a ∈ fowl3 |FO ⊦ ∃ n0. n < n0 ∧ n0 < # fowl5 + # fowl4 + # fowl2 ∧ ((fowl5 + fowl4) + fowl2)[n0] = FO(t)

Rule argument

Additional information

Used terms: fowl5, fowl3 |FO

Proof step 52 from proof rely-fo-follows-w-stable (previous step) (back to tree)

A spec-lemma

Proof step 53 from proof rely-fo-follows-w-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 54:

  fowl5[n] = W(v, t), p0(l) = fowl + fowl3 + fowl4, fowl2 | t = [], fowl5 ≠ [], n < # fowl5 + # fowl4 + # fowl2, n < # fowl5 + # fowl4, n < # fowl5, ∀ n0. n0 < # p0(l) ∧ p0(l)[n0].W? ∧ p0(l)[n0].tid = t → (∃ n1. n0 < n1 ∧ n1 < # p0(l) ∧ p0(l)[n1] = FO(p0(l)[n0].tid)), ∀ a. a ∈ fowl5 → a ∈ fowl3 ∧ a.FO? ⊦ ∃ n0. n < n0 ∧ n0 < # fowl5 + # fowl4 + # fowl2 ∧ ((fowl5 + fowl4) + fowl2)[n0] = FO(t)

Rule argument

Additional information

Used simplifier rules: ⊦ fow ∈ fowl |FO ↔ fow ∈ fowl ∧ fow.FO?; (s)

Proof step 54 from proof rely-fo-follows-w-stable (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 55:

  fowl5[n] = W(v, t), p0(l) = fowl + fowl3 + fowl4, fowl2 | t = [], fowl5 ≠ [], n < # fowl5, n < # fowl5 + # fowl4, n < # fowl5 + # fowl4 + # fowl2, W(v, t) ∈ fowl5 → W(v, t) ∈ fowl3 ∧ W(v, t).FO?, ∀ n0. n0 < # p0(l) ∧ p0(l)[n0].W? ∧ p0(l)[n0].tid = t → (∃ n1. n0 < n1 ∧ n1 < # p0(l) ∧ p0(l)[n1] = FO(p0(l)[n0].tid)) ⊦ ∃ n0. n < n0 ∧ n0 < # fowl5 + # fowl4 + # fowl2 ∧ ((fowl5 + fowl4) + fowl2)[n0] = FO(t)

Rule argument

Additional information

Used terms: W(v, t)

Proof step 55 from proof rely-fo-follows-w-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 56:

  fowl5[n] = W(v, t), p0(l) = fowl + fowl3 + fowl4, fowl2 | t = [], fowl5 ≠ [], n < # fowl5 + # fowl4 + # fowl2, n < # fowl5 + # fowl4, n < # fowl5, ¬ W(v, t) ∈ fowl5, ∀ n0. n0 < # p0(l) ∧ p0(l)[n0].W? ∧ p0(l)[n0].tid = t → (∃ n1. n0 < n1 ∧ n1 < # p0(l) ∧ p0(l)[n1] = FO(p0(l)[n0].tid)) ⊦ ∃ n0. n < n0 ∧ n0 < # fowl5 + # fowl4 + # fowl2 ∧ ((fowl5 + fowl4) + fowl2)[n0] = FO(t)

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ W(v, tid).FO?; (s)

Proof step 56 from proof rely-fo-follows-w-stable (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 57:

  ⊦ a ∈ x ↔ (∃ n. n < # x ∧ x[n] = a)

• Proof step 58:

  fowl5[n] = W(v, t), p0(l) = fowl + fowl3 + fowl4, fowl2 | t = [], fowl5 ≠ [], n < # fowl5, n < # fowl5 + # fowl4, n < # fowl5 + # fowl4 + # fowl2, ∀ n0. n0 < # p0(l) ∧ p0(l)[n0].W? ∧ p0(l)[n0].tid = t → (∃ n1. n0 < n1 ∧ n1 < # p0(l) ∧ p0(l)[n1] = FO(p0(l)[n0].tid)), ∀ n. ¬(n < # fowl5 ∧ fowl5[n] = W(v, t)) ⊦ ∃ n0. n < n0 ∧ n0 < # fowl5 + # fowl4 + # fowl2 ∧ ((fowl5 + fowl4) + fowl2)[n0] = FO(t)

Rule argument

Additional information

Used terms: W(v, t), fowl5

Proof step 57 from proof rely-fo-follows-w-stable (previous step) (back to tree)

A spec-lemma

Proof step 58 from proof rely-fo-follows-w-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 59:

  fowl5[n] = W(v, t), p0(l) = fowl + fowl3 + fowl4, fowl2 | t = [], fowl5 ≠ [], n < # fowl5 + # fowl4 + # fowl2, n < # fowl5 + # fowl4, n < # fowl5, ∀ n0. n0 < # p0(l) ∧ p0(l)[n0].W? ∧ p0(l)[n0].tid = t → (∃ n1. n0 < n1 ∧ n1 < # p0(l) ∧ p0(l)[n1] = FO(p0(l)[n0].tid)), ∀ n0. ¬ n0 < # fowl5 ∨ fowl5[n0] ≠ W(v, t) ⊦ ∃ n0. n < n0 ∧ n0 < # fowl5 + # fowl4 + # fowl2 ∧ ((fowl5 + fowl4) + fowl2)[n0] = FO(t)

Rule argument

Additional information

Proof step 59 from proof rely-fo-follows-w-stable (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: n