Proof step 1 from proof absloc-no-W-leading-W (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  fowl |W | t = [], absloc(W(t, l, v) ' + el, rset, fowl) ⊦

Rule argument

Additional information

Proof step 2 from proof absloc-no-W-leading-W (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  (fow + fowl0)|W | t = [], absloc(W(t, l, v) ' + el, rset, fow + fowl0), ∀ t, l, v, el, rset. ¬(fowl0 |W | t = [] ∧ absloc(W(t, l, v) ' + el, rset, fowl0)) ⊦

Rule argument

Additional information

Used simplifier rules: absloc-recW-empty: ⊦ ¬ absloc(W(t, l, v) ' + el, rset, []); List('a) freely generated by [], +;; ⊦ [] |W = []; (s) ⊦ [] | t = []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 3 from proof absloc-no-W-leading-W (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  fow ' |W | t = [], fowl0 |W | t = [], absloc(W(t, l, v) ' + el, rset, fow ' + fowl0), ∀ t0, l0, v0, el0, rset0. fowl0 |W | t0 ≠ [] ∨ ¬ absloc(W(t0, l0, v0) ' + el0, rset0, fowl0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ fowl + fowl0 | t = (fowl | t) + (fowl0 | t); (s) ⊦ (fowl + fowl0)|W = fowl |W + fowl0 |W; (s)

Proof step 4 from proof absloc-no-W-leading-W (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 5:

  fow = FO(t1), fowl0 |W | t = [], fow ' |W | t = [], absloc(W(t, l, v) ' + el, rset, fow ' + fowl0), ∀ t0, l0, v0, el0, rset0. fowl0 |W | t0 ≠ [] ∨ ¬ absloc(W(t0, l0, v0) ' + el0, rset0, fowl0) ⊦

Rule argument

Additional information

Used simplifier rules: absloc-recW-W: ⊦ absloc(W(t, l, v) ' + el, rset, W(v0, t0) ' + fowl) ↔ t0 = t ∧ v0 = v ∧ absloc(el, rset, fowl); FOW freely generated by FO, W;; ⊦ W(v, t) ' |W = W(v, t) '; (s) ⊦ fow ' | t = (t = fow.tid ⊃ fow ';[]); (s) ⊦ W(v, tid).tid = tid; (s) ⊦ a ' ≠ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 5 from proof absloc-no-W-leading-W (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  fowl0 |W | t = [], absloc(W(t, l, v) ' + el, rset, fowl0), ∀ t0, l0, v0, el0, rset0. fowl0 |W | t0 ≠ [] ∨ ¬ absloc(W(t0, l0, v0) ' + el0, rset0, fowl0) ⊦

Rule argument

Additional information

Used simplifier rules: absloc-recW-FO: ⊦ absloc(W(t, l, v) ' + el, rset, FO(t0) ' + fowl) ↔ absloc(W(t, l, v) ' + el, rset, fowl); a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ [] | t = []; (s) ⊦ FO(t) ' |W = []; (s)

Proof step 6 from proof absloc-no-W-leading-W (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: t, l, v, el, rset