Proof step 1 from proof abs-leading-write-h-restricted-non-empty (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  p(l) = W(v, t) ' + fowl, (h |W | l) | false = [], abs(h, rs, p) ⊦

Rule argument

Additional information

Proof step 2 from proof abs-leading-write-h-restricted-non-empty (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  p(l) = W(v, t) ' + fowl, (h |W | l) | false = [], abs(h, rs, p), W(v, t) ∈ p(l) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list

Proof step 3 from proof abs-leading-write-h-restricted-non-empty (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ abs(h, rs, p) ↔ (∀ l. absloc(events((h | l) | false), rs(l), p(l)))

• Proof step 5:

  p(l) = W(v, t) ' + fowl, (h |W | l) | false = [], W(v, t) ∈ p(l), ∀ l. absloc(events((h | l) | false), rs(l), p(l)) ⊦

Rule argument

Additional information

Used terms: h, rs, p

Proof step 4 from proof abs-leading-write-h-restricted-non-empty (previous step) (back to tree)

Lemma abs-def

Proof step 5 from proof abs-leading-write-h-restricted-non-empty (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 6:

  p(l) = W(v, t) ' + fowl, (h |W | l) | false = [], absloc(events((h | l) | false), rs(l), p(l)), W(v, t) ∈ p(l) ⊦

Rule argument

Additional information

Used terms: l

Proof step 6 from proof abs-leading-write-h-restricted-non-empty (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 7:

  p(l) = W(v, t) ' + fowl, ([] |W | l) | false = [], absloc(events(([] | l) | false), rs(l), p(l)), W(v, t) ∈ p(l) ⊦

• Proof step 12:

  p(l) = W(v, t) ' + fowl, ((vpe + h0)|W | l) | false = [], absloc(events((vpe + h0 | l) | false), rs(l), p(l)), W(v, t) ∈ p(l), ∀ p, l, v, t, fowl, rs. ¬(p(l) = W(v, t) ' + fowl ∧ (h0 |W | l) | false = [] ∧ absloc(events((h0 | l) | false), rs(l), p(l)) ∧ W(v, t) ∈ p(l)) ⊦

Rule argument

Additional information

Used simplifier rules: List('a) freely generated by [], +;;

Proof step 7 from proof abs-leading-write-h-restricted-non-empty (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  p(l) = W(v, t) ' + fowl, p(l) |W = [], W(v, t) ∈ p(l) ⊦

Rule argument

Additional information

Used simplifier rules: absloc-base: ⊦ absloc([], rset, fowl) ↔ fowl |W = []; ⊦ events([]) = []; (s) ⊦ [] | b = []; (s) ⊦ [] | l = []; (s) ⊦ [] |W = []; (s)

Proof step 8 from proof abs-leading-write-h-restricted-non-empty (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

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

• Proof step 10:

  p(l).filter(λ fow. fow.W?) = [], p(l) = W(v, t) ' + fowl, W(v, t) ∈ p(l) ⊦

Rule argument

Additional information

Used terms: p(l)

Proof step 9 from proof abs-leading-write-h-restricted-non-empty (previous step) (back to tree)

A spec-lemma

Proof step 10 from proof abs-leading-write-h-restricted-non-empty (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  p(l).filter(.W?) = [], p(l) = W(v, t) ' + fowl, W(v, t) ∈ p(l) ⊦

Rule argument

Additional information

Proof step 11 from proof abs-leading-write-h-restricted-non-empty (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ (a ' + x).filter(p) = (p(a) ⊃ a ';[]) + x.filter(p); (s) ⊦ W(v, tid).W?; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a ' ≠ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 12 from proof abs-leading-write-h-restricted-non-empty (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  p(l) = W(v, t) ' + fowl, ((vpe._1.W? ⊃ vpe ';[]) | l) | false = [], (h0 |W | l) | false = [], absloc(events((vpe._1.l = l ⊃ vpe ';[]) | false) + events((h0 | l) | false), rs(l), p(l)), W(v, t) ∈ p(l), ∀ p0, l0, v0, t0, fowl0, rs0. p0(l0) ≠ W(v0, t0) ' + fowl0 ∨ (h0 |W | l0) | false ≠ [] ∨ ¬ absloc(events((h0 | l0) | false), rs0(l0), p0(l0)) ∨ ¬ W(v0, t0) ∈ p0(l0) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ events(h1 + h2) = events(h1) + events(h2); (s) ⊦ h + h0 | b = (h | b) + (h0 | b); (s) ⊦ vpe ' | l = (vpe._1.l = l ⊃ vpe ';[]); (s) ⊦ h + h0 | l0 = (h | l0) + (h0 | l0); (s) ⊦ a + x = a ' + x; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ vpe ' |W = (vpe._1.W? ⊃ vpe ';[]); (s) ⊦ (h + h0)|W = h |W + h0 |W; (s)

Proof step 13 from proof abs-leading-write-h-restricted-non-empty (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 14:

  p(l) = W(v, t) ' + fowl, vpe = (e, boolvar), (h0 |W | l) | false = [], ((e.W? ⊃ vpe ';[]) | l) | false = [], absloc(events((e.l = l ⊃ vpe ';[]) | false) + events((h0 | l) | false), rs(l), p(l)), W(v, t) ∈ p(l), ∀ p0, l0, v0, t0, fowl0, rs0. p0(l0) ≠ W(v0, t0) ' + fowl0 ∨ (h0 |W | l0) | false ≠ [] ∨ ¬ absloc(events((h0 | l0) | false), rs0(l0), p0(l0)) ∨ ¬ W(v0, t0) ∈ p0(l0) ⊦

Rule argument

Additional information

Used terms: e, boolvar

Proof step 14 from proof abs-leading-write-h-restricted-non-empty (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  p(l) = W(v, t) ' + fowl, ((e.W? ⊃ (e, boolvar) ';[]) | l) | false = [], (h0 |W | l) | false = [], absloc(events((e.l = l ⊃ (e, boolvar) ';[]) | false) + events((h0 | l) | false), rs(l), p(l)), W(v, t) ∈ p(l), ∀ p0, l0, v0, t0, fowl0, rs0. p0(l0) ≠ W(v0, t0) ' + fowl0 ∨ (h0 |W | l0) | false ≠ [] ∨ ¬ absloc(events((h0 | l0) | false), rs0(l0), p0(l0)) ∨ ¬ W(v0, t0) ∈ p0(l0) ⊦

Rule argument

Additional information

Proof step 15 from proof abs-leading-write-h-restricted-non-empty (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 16:

  p(l) = W(v, t) ' + fowl, (h0 |W | l) | false = [], ((e, boolvar) ' | l) | false = [], e.W?, absloc(events((e.l = l ⊃ (e, boolvar) ';[]) | false) + events((h0 | l) | false), rs(l), p(l)), W(v, t) ∈ p(l), ∀ p0, l0, v0, t0, fowl0, rs0. p0(l0) ≠ W(v0, t0) ' + fowl0 ∨ (h0 |W | l0) | false ≠ [] ∨ ¬ absloc(events((h0 | l0) | false), rs0(l0), p0(l0)) ∨ ¬ W(v0, t0) ∈ p0(l0) ⊦

• Proof step 20:

  p(l) = W(v, t) ' + fowl, (h0 |W | l) | false = [], ([] | l) | false = [], absloc(events((e.l = l ⊃ (e, boolvar) ';[]) | false) + events((h0 | l) | false), rs(l), p(l)), W(v, t) ∈ p(l), ¬ e.W?, ∀ p0, l0, v0, t0, fowl0, rs0. p0(l0) ≠ W(v0, t0) ' + fowl0 ∨ (h0 |W | l0) | false ≠ [] ∨ ¬ absloc(events((h0 | l0) | false), rs0(l0), p0(l0)) ∨ ¬ W(v0, t0) ∈ p0(l0) ⊦

Rule argument

Additional information

Proof step 16 from proof abs-leading-write-h-restricted-non-empty (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  p(l) = W(v, t) ' + fowl, (e.l = l ⊃ (e, boolvar) ';[]) | false = [], (h0 |W | l) | false = [], e.W?, absloc(events((h0 | l) | false), rs(l), p(l)), W(v, t) ∈ p(l), ∀ p0, l0, v0, t0, fowl0, rs0. p0(l0) ≠ W(v0, t0) ' + fowl0 ∨ (h0 |W | l0) | false ≠ [] ∨ ¬ absloc(events((h0 | l0) | false), rs0(l0), p0(l0)) ∨ ¬ W(v0, t0) ∈ p0(l0) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ [] + x = x; (s) ⊦ events([]) = []; (s) ⊦ vpe ' | l = (vpe._1.l = l ⊃ vpe ';[]); (s)

Proof step 17 from proof abs-leading-write-h-restricted-non-empty (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 18:

  e = W(t1, l1, v1), p(l) = W(v, t) ' + fowl, (h0 |W | l) | false = [], (l1 = l ⊃ (e, boolvar) ';[]) | false = [], e.W?, absloc(events((h0 | l) | false), rs(l), p(l)), W(v, t) ∈ p(l), ∀ p0, l0, v0, t0, fowl0, rs0. p0(l0) ≠ W(v0, t0) ' + fowl0 ∨ (h0 |W | l0) | false ≠ [] ∨ ¬ absloc(events((h0 | l0) | false), rs0(l0), p0(l0)) ∨ ¬ W(v0, t0) ∈ p0(l0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ e.W? → ((t = e.t ∧ l = e.l) ∧ v = e.v ↔ e = W(t, l, v)); (elim) Used terms: e, t1, l1, v1

Proof step 18 from proof abs-leading-write-h-restricted-non-empty (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  p(l) = W(v, t) ' + fowl, (h0 |W | l) | false = [], (l1 = l ⊃ (W(t1, l, v1), boolvar) ';[]) | false = [], absloc(events((h0 | l) | false), rs(l), p(l)), W(v, t) ∈ p(l), ∀ p0, l0, v0, t0, fowl0, rs0. p0(l0) ≠ W(v0, t0) ' + fowl0 ∨ (h0 |W | l0) | false ≠ [] ∨ ¬ absloc(events((h0 | l0) | false), rs0(l0), p0(l0)) ∨ ¬ W(v0, t0) ∈ p0(l0) ⊦

Rule argument

Additional information

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

Proof step 19 from proof abs-leading-write-h-restricted-non-empty (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: p, l, v, t, fowl, rs

Proof step 20 from proof abs-leading-write-h-restricted-non-empty (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  p(l) = W(v, t) ' + fowl, (h0 |W | l) | false = [], absloc(events((e.l = l ⊃ (e, boolvar) ';[]) | false) + events((h0 | l) | false), rs(l), p(l)), W(v, t) ∈ p(l), ¬ e.W?, ∀ p0, l0, v0, t0, fowl0, rs0. p0(l0) ≠ W(v0, t0) ' + fowl0 ∨ (h0 |W | l0) | false ≠ [] ∨ ¬ absloc(events((h0 | l0) | false), rs0(l0), p0(l0)) ∨ ¬ W(v0, t0) ∈ p0(l0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ [] | b = []; (s) ⊦ [] | l = []; (s)

Proof step 21 from proof abs-leading-write-h-restricted-non-empty (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 22:

  e.l = l, p(l) = W(v, t) ' + fowl, (h0 |W | l) | false = [], absloc(events((e, boolvar) ' | false) + events((h0 | l) | false), rs(l), p(l)), W(v, t) ∈ p(l), ¬ e.W?, ∀ p0, l0, v0, t0, fowl0, rs0. p0(l0) ≠ W(v0, t0) ' + fowl0 ∨ (h0 |W | l0) | false ≠ [] ∨ ¬ absloc(events((h0 | l0) | false), rs0(l0), p0(l0)) ∨ ¬ W(v0, t0) ∈ p0(l0) ⊦

• Proof step 30:

  p(l) = W(v, t) ' + fowl, (h0 |W | l) | false = [], e.l ≠ l, absloc(events([] | false) + events((h0 | l) | false), rs(l), p(l)), W(v, t) ∈ p(l), ¬ e.W?, ∀ p0, l0, v0, t0, fowl0, rs0. p0(l0) ≠ W(v0, t0) ' + fowl0 ∨ (h0 |W | l0) | false ≠ [] ∨ ¬ absloc(events((h0 | l0) | false), rs0(l0), p0(l0)) ∨ ¬ W(v0, t0) ∈ p0(l0) ⊦

Rule argument

Additional information

Proof step 22 from proof abs-leading-write-h-restricted-non-empty (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  p(e.l) = W(v, t) ' + fowl, (h0 |W | e.l) | false = [], absloc(events((¬ boolvar ⊃ (e, false) ';[])) + events((h0 | e.l) | false), rs(e.l), p(e.l)), W(v, t) ∈ p(e.l), ¬ e.W?, ∀ p0, l0, v0, t0, fowl0, rs0. p0(l0) ≠ W(v0, t0) ' + fowl0 ∨ (h0 |W | l0) | false ≠ [] ∨ ¬ absloc(events((h0 | l0) | false), rs0(l0), p0(l0)) ∨ ¬ W(v0, t0) ∈ p0(l0) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list ⊦ (e, b) ' | b0 = (b ↔ b0 ⊃ (e, b) ';[]); (s)

Proof step 23 from proof abs-leading-write-h-restricted-non-empty (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 24:

  ¬ boolvar, p(e.l) = W(v, t) ' + fowl, (h0 |W | e.l) | false = [], absloc(events((e, false) ') + events((h0 | e.l) | false), rs(e.l), p(e.l)), W(v, t) ∈ p(e.l), ¬ e.W?, ∀ p0, l0, v0, t0, fowl0, rs0. p0(l0) ≠ W(v0, t0) ' + fowl0 ∨ (h0 |W | l0) | false ≠ [] ∨ ¬ absloc(events((h0 | l0) | false), rs0(l0), p0(l0)) ∨ ¬ W(v0, t0) ∈ p0(l0) ⊦

• Proof step 28:

  boolvar, p(e.l) = W(v, t) ' + fowl, (h0 |W | e.l) | false = [], absloc(events([]) + events((h0 | e.l) | false), rs(e.l), p(e.l)), W(v, t) ∈ p(e.l), ¬ e.W?, ∀ p0, l0, v0, t0, fowl0, rs0. p0(l0) ≠ W(v0, t0) ' + fowl0 ∨ (h0 |W | l0) | false ≠ [] ∨ ¬ absloc(events((h0 | l0) | false), rs0(l0), p0(l0)) ∨ ¬ W(v0, t0) ∈ p0(l0) ⊦

Rule argument

Additional information

Proof step 24 from proof abs-leading-write-h-restricted-non-empty (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  p(e.l) = W(v, t) ' + fowl, (h0 |W | e.l) | false = [], absloc(e ' + events((h0 | e.l) | false), rs(e.l), p(e.l)), W(v, t) ∈ p(e.l), ¬ e.W?, ∀ p0, l0, v0, t0, fowl0, rs0. p0(l0) ≠ W(v0, t0) ' + fowl0 ∨ (h0 |W | l0) | false ≠ [] ∨ ¬ absloc(events((h0 | l0) | false), rs0(l0), p0(l0)) ∨ ¬ W(v0, t0) ∈ p0(l0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ events(vpe ') = vpe._1 '; (s)

Proof step 25 from proof abs-leading-write-h-restricted-non-empty (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 26:

  e = R(t1, l, v1), p(e.l) = W(v, t) ' + fowl, (h0 |W | e.l) | false = [], absloc(e ' + events((h0 | e.l) | false), rs(e.l), p(e.l)), W(v, t) ∈ p(e.l), ¬ e.W?, ∀ p0, l0, v0, t0, fowl0, rs0. p0(l0) ≠ W(v0, t0) ' + fowl0 ∨ (h0 |W | l0) | false ≠ [] ∨ ¬ absloc(events((h0 | l0) | false), rs0(l0), p0(l0)) ∨ ¬ W(v0, t0) ∈ p0(l0) ⊦

Rule argument

Additional information

Used simplifier rules: RWevent freely generated by R, W;; ⊦ W(t, l, v).l = l; (s) ⊦ W(t, l, v).W?; (s)

Proof step 26 from proof abs-leading-write-h-restricted-non-empty (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  p(l) = W(v, t) ' + fowl, (h0 |W | l) | false = [], absloc(events((h0 | l) | false), rs(l), p(l)), W(v, t) ∈ p(l), ¬ t1 ∈ rs(l) → FO(t1) ∈ p(l), ∀ p0, l0, v0, t0, fowl0, rs0. p0(l0) ≠ W(v0, t0) ' + fowl0 ∨ (h0 |W | l0) | false ≠ [] ∨ ¬ absloc(events((h0 | l0) | false), rs0(l0), p0(l0)) ∨ ¬ W(v0, t0) ∈ p0(l0) ⊦

Rule argument

Additional information

Used simplifier rules: absloc-recR: ⊦ absloc(R(t, l, v) ' + el, rset, fowl) ↔ (¬ t ∈ rset → FO(t) ∈ fowl) ∧ absloc(el, rset, fowl); a: ⊦ (x + y) + z = x + y + z; from specification list in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list ⊦ ¬ R(t, l, v).W?; (s) ⊦ R(t, l, v).l = l; (s)

Proof step 27 from proof abs-leading-write-h-restricted-non-empty (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: p, l, v, t, fowl, rs

Proof step 28 from proof abs-leading-write-h-restricted-non-empty (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  p(e.l) = W(v, t) ' + fowl, (h0 |W | e.l) | false = [], absloc(events((h0 | e.l) | false), rs(e.l), p(e.l)), W(v, t) ∈ p(e.l), ¬ e.W?, ∀ p0, l0, v0, t0, fowl0, rs0. p0(l0) ≠ W(v0, t0) ' + fowl0 ∨ (h0 |W | l0) | false ≠ [] ∨ ¬ absloc(events((h0 | l0) | false), rs0(l0), p0(l0)) ∨ ¬ W(v0, t0) ∈ p0(l0) ⊦

Rule argument

Additional information

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

Proof step 29 from proof abs-leading-write-h-restricted-non-empty (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: p, e.l, v, t, fowl, rs

Proof step 30 from proof abs-leading-write-h-restricted-non-empty (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  p(l) = W(v, t) ' + fowl, (h0 |W | l) | false = [], e.l ≠ l, absloc(events((h0 | l) | false), rs(l), p(l)), W(v, t) ∈ p(l), ¬ e.W?, ∀ p0, l0, v0, t0, fowl0, rs0. p0(l0) ≠ W(v0, t0) ' + fowl0 ∨ (h0 |W | l0) | false ≠ [] ∨ ¬ absloc(events((h0 | l0) | false), rs0(l0), p0(l0)) ∨ ¬ W(v0, t0) ∈ p0(l0) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ [] + x = x; (s) ⊦ events([]) = []; (s) ⊦ [] | b = []; (s)

Proof step 31 from proof abs-leading-write-h-restricted-non-empty (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: p, l, v, t, fowl, rs