Proof step 1 from proof absloc-addReader (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  absloc(el, rset, fowl), ¬ absloc(el, rset ++ t, fowl) ⊦

Rule argument

Additional information

Proof step 2 from proof absloc-addReader (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  absloc(e + el0, rset, fowl), ¬ absloc(e + el0, rset ++ t, fowl), ∀ rset, fowl, t. ¬(absloc(el0, rset, fowl) ∧ ¬ absloc(el0, rset ++ t, fowl)) ⊦

Rule argument

Additional information

Used simplifier rules: absloc-base: ⊦ absloc([], rset, fowl) ↔ fowl |W = []; List('a) freely generated by [], +;;

Proof step 3 from proof absloc-addReader (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  absloc(e ' + el0, rset, fowl), ¬ absloc(e ' + el0, rset ++ t, fowl), ∀ rset0, fowl0, t0. ¬ absloc(el0, rset0, fowl0) ∨ absloc(el0, rset0 ++ t0, fowl0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s)

Proof step 4 from proof absloc-addReader (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 5:

  e = R(t1, l, v), absloc(e ' + el0, rset, fowl), ¬ absloc(e ' + el0, rset ++ t, fowl), ∀ rset0, fowl0, t0. ¬ absloc(el0, rset0, fowl0) ∨ absloc(el0, rset0 ++ t0, fowl0) ⊦

• Proof step 9:

  e = W(t1, l, v), absloc(e ' + el0, rset, fowl), ¬ absloc(e ' + el0, rset ++ t, fowl), ∀ rset0, fowl0, t0. ¬ absloc(el0, rset0, fowl0) ∨ absloc(el0, rset0 ++ t0, fowl0) ⊦

Rule argument

Additional information

Used simplifier rules: RWevent freely generated by R, W;;

Proof step 5 from proof absloc-addReader (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  absloc(el0, rset, fowl), ¬ t1 ∈ rset → FO(t1) ∈ fowl, ∀ rset0, fowl0, t0. ¬ absloc(el0, rset0, fowl0) ∨ absloc(el0, rset0 ++ t0, fowl0) ⊦ (t1 ≠ t ∧ ¬ t1 ∈ rset → FO(t1) ∈ fowl) ∧ absloc(el0, rset ++ t, fowl)

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 ⊦ a ∈ s ++ b ↔ a = b ∨ a ∈ s; (s)

Proof step 6 from proof absloc-addReader (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 7:

  absloc(el0, rset, fowl), ¬ absloc(el0, rset ++ t, fowl), ¬ t1 ∈ rset → FO(t1) ∈ fowl, ∀ rset0, fowl0, t0. ¬ absloc(el0, rset0, fowl0) ∨ absloc(el0, rset0 ++ t0, fowl0) ⊦ (t1 ≠ t ∧ ¬ t1 ∈ rset → FO(t1) ∈ fowl) ∧ absloc(el0, rset ++ t, fowl)

Rule argument

Additional information

Used formulas: absloc(el0, rset ++ t, fowl)

Proof step 7 from proof absloc-addReader (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  absloc(el0, rset, fowl), ¬ absloc(el0, rset ++ t, fowl), ¬ t1 ∈ rset → FO(t1) ∈ fowl, ∀ rset0, fowl0, t0. ¬ absloc(el0, rset0, fowl0) ∨ absloc(el0, rset0 ++ t0, fowl0) ⊦

Rule argument

Additional information

Proof step 8 from proof absloc-addReader (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: rset, fowl, t

Proof step 9 from proof absloc-addReader (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  absloc(W(t1, l, v) ' + el0, rset, fowl), ¬ absloc(W(t1, l, v) ' + el0, rset ++ t, fowl), ∀ rset0, fowl0, t0. ¬ absloc(el0, rset0, fowl0) ∨ absloc(el0, rset0 ++ t0, fowl0) ⊦

Rule argument

Additional information

Proof step 10 from proof absloc-addReader (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 11:

  absloc(W(t1, l, v) ' + el0, rset, fow + fowl0), ¬ absloc(W(t1, l, v) ' + el0, rset ++ t, fow + fowl0), ∀ rset0, fowl0, t0. ¬ absloc(el0, rset0, fowl0) ∨ absloc(el0, rset0 ++ t0, fowl0), ∀ t1, l, v, el0, rset, t. ¬ ( absloc(W(t1, l, v) ' + el0, rset, fowl0) ∧ ¬ absloc(W(t1, l, v) ' + el0, rset ++ t, fowl0) ∧ (∀ rset0, fowl0, t0. ¬ absloc(el0, rset0, fowl0) ∨ absloc(el0, rset0 ++ t0, fowl0))) ⊦

Rule argument

Additional information

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

Proof step 11 from proof absloc-addReader (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  absloc(W(t1, l, v) ' + el0, rset, fow ' + fowl0), ¬ absloc(W(t1, l, v) ' + el0, rset ++ t, fow ' + fowl0), ∀ rset0, fowl0, t0. ¬ absloc(el0, rset0, fowl0) ∨ absloc(el0, rset0 ++ t0, fowl0), ∀ t0, l0, v0, el, rset0, t2. ¬ absloc(W(t0, l0, v0) ' + el, rset0, fowl0) ∨ absloc(W(t0, l0, v0) ' + el, rset0 ++ t2, fowl0) ∨ ¬(∀ rset0, fowl0, t0. ¬ absloc(el, rset0, fowl0) ∨ absloc(el, rset0 ++ t0, fowl0)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s)

Proof step 12 from proof absloc-addReader (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 13:

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

• Proof step 15:

  fow = W(v1, t3), absloc(W(t1, l, v) ' + el0, rset, fow ' + fowl0), ¬ absloc(W(t1, l, v) ' + el0, rset ++ t, fow ' + fowl0), ∀ t0, l0, v0, el, rset0, t2. ¬ absloc(W(t0, l0, v0) ' + el, rset0, fowl0) ∨ absloc(W(t0, l0, v0) ' + el, rset0 ++ t2, fowl0) ∨ ¬(∀ rset0, fowl0, t0. ¬ absloc(el, rset0, fowl0) ∨ absloc(el, rset0 ++ t0, fowl0)), ∀ rset0, fowl0, t0. ¬ absloc(el0, rset0, fowl0) ∨ absloc(el0, rset0 ++ t0, fowl0) ⊦

Rule argument

Additional information

Used simplifier rules: FOW freely generated by FO, W;;

Proof step 13 from proof absloc-addReader (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  absloc(W(t1, l, v) ' + el0, rset, fowl0), ¬ absloc(W(t1, l, v) ' + el0, rset ++ t, fowl0), ∀ rset0, fowl0, t0. ¬ absloc(el0, rset0, fowl0) ∨ absloc(el0, rset0 ++ t0, fowl0), ∀ t0, l0, v0, el, rset0, t2. ¬ absloc(W(t0, l0, v0) ' + el, rset0, fowl0) ∨ absloc(W(t0, l0, v0) ' + el, rset0 ++ t2, fowl0) ∨ ¬(∀ rset0, fowl0, t0. ¬ absloc(el, rset0, fowl0) ∨ absloc(el, rset0 ++ t0, 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

Proof step 14 from proof absloc-addReader (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: t1, l, v, el0, rset, t

Proof step 15 from proof absloc-addReader (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  absloc(el0, rset, fowl0), ¬ absloc(el0, rset ++ t, fowl0), ∀ t0, l0, v0, el, rset0, t2. ¬ absloc(W(t0, l0, v0) ' + el, rset0, fowl0) ∨ absloc(W(t0, l0, v0) ' + el, rset0 ++ t2, fowl0) ∨ ¬(∀ rset0, fowl0, t0. ¬ absloc(el, rset0, fowl0) ∨ absloc(el, rset0 ++ t0, fowl0)), ∀ rset0, fowl0, t0. ¬ absloc(el0, rset0, fowl0) ∨ absloc(el0, rset0 ++ t0, 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); a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 16 from proof absloc-addReader (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: rset, fowl0, t