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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(absloc(el + R(t, l, v) ', rset, fowl) ↔ absloc(el, rset, fowl)), t ∈ rset ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  # rset ≠ 0, ¬(absloc(el + R(t, l, v) ', rset, fowl) ↔ absloc(el, rset, fowl)), rset ≠ ∅, t ∈ rset ⊦

Rule argument

Additional information

Used simplifier rules: size-zero-01: ⊦ s ≠ ∅ → # s ≠ 0; (forward) from specification set-basic ne-01: ⊦ a ∈ s → s ≠ ∅; (forward) from specification set-basic

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

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  # rset ≠ 0, ¬(absloc((e + el0) + R(t, l, v) ', rset, fowl) ↔ absloc(e + el0, rset, fowl)), rset ≠ ∅, t ∈ rset, ∀ rset, t, l, v, fowl. ¬(# rset ≠ 0 ∧ ¬(absloc(el0 + R(t, l, v) ', rset, fowl) ↔ absloc(el0, rset, fowl)) ∧ rset ≠ ∅ ∧ t ∈ rset) ⊦

Rule argument

Additional information

Used simplifier rules: absloc-base: ⊦ absloc([], rset, fowl) ↔ fowl |W = []; absloc-recR-one: ⊦ absloc(R(t, l, v) ', rset, fowl) ↔ (¬ t ∈ rset → FO(t) ∈ fowl) ∧ fowl |W = []; List('a) freely generated by [], +;; ⊦ [] + x = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  # rset ≠ 0, ¬(absloc((e ' + el0) + R(t, l, v) ', rset, fowl) ↔ absloc(e ' + el0, rset, fowl)), rset ≠ ∅, t ∈ rset, ∀ rset0, t0, l0, v0, fowl0. # rset0 = 0 ∨ (absloc(el0 + R(t0, l0, v0) ', rset0, fowl0) ↔ absloc(el0, rset0, fowl0)) ∨ rset0 = ∅ ∨ ¬ t0 ∈ rset0 ⊦

Rule argument

Additional information

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

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

User applied rule constructor cut

And obtained the following new goals

• Proof step 6:

  e = R(t1, l1, v1), # rset ≠ 0, ¬(absloc((e ' + el0) + R(t, l, v) ', rset, fowl) ↔ absloc(e ' + el0, rset, fowl)), rset ≠ ∅, t ∈ rset, ∀ rset0, t0, l0, v0, fowl0. # rset0 = 0 ∨ (absloc(el0 + R(t0, l0, v0) ', rset0, fowl0) ↔ absloc(el0, rset0, fowl0)) ∨ rset0 = ∅ ∨ ¬ t0 ∈ rset0 ⊦

• Proof step 8:

  e = W(t1, l1, v1), # rset ≠ 0, ¬(absloc((e ' + el0) + R(t, l, v) ', rset, fowl) ↔ absloc(e ' + el0, rset, fowl)), rset ≠ ∅, t ∈ rset, ∀ rset0, t0, l0, v0, fowl0. # rset0 = 0 ∨ (absloc(el0 + R(t0, l0, v0) ', rset0, fowl0) ↔ absloc(el0, rset0, fowl0)) ∨ rset0 = ∅ ∨ ¬ t0 ∈ rset0 ⊦

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  # rset ≠ 0, ¬(absloc(el0 + R(t, l, v) ', rset, fowl) ↔ absloc(el0, rset, fowl)), rset ≠ ∅, t ∈ rset, ¬ t1 ∈ rset → FO(t1) ∈ fowl, ∀ rset0, t0, l0, v0, fowl0. # rset0 = 0 ∨ (absloc(el0 + R(t0, l0, v0) ', rset0, fowl0) ↔ absloc(el0, rset0, fowl0)) ∨ rset0 = ∅ ∨ ¬ t0 ∈ rset0 ⊦

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

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

User applied rule all left

And closed the goal!

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  # rset ≠ 0, ¬(absloc((W(t1, l1, v1) ' + el0) + R(t, l, v) ', rset, fowl) ↔ absloc(W(t1, l1, v1) ' + el0, rset, fowl)), rset ≠ ∅, t ∈ rset, ∀ rset0, t0, l0, v0, fowl0. # rset0 = 0 ∨ (absloc(el0 + R(t0, l0, v0) ', rset0, fowl0) ↔ absloc(el0, rset0, fowl0)) ∨ rset0 = ∅ ∨ ¬ t0 ∈ rset0 ⊦

Rule argument

Additional information

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

User applied rule structural induction

And obtained the following new goals

• Proof step 10:

  # rset ≠ 0, ¬(absloc((W(t1, l1, v1) ' + el0) + R(t, l, v) ', rset, fow + fowl0) ↔ absloc(W(t1, l1, v1) ' + el0, rset, fow + fowl0)), rset ≠ ∅, t ∈ rset, ∀ rset0, t0, l0, v0, fowl0. # rset0 = 0 ∨ (absloc(el0 + R(t0, l0, v0) ', rset0, fowl0) ↔ absloc(el0, rset0, fowl0)) ∨ rset0 = ∅ ∨ ¬ t0 ∈ rset0, ∀ rset, t1, l1, v1, el0, t, l, v. ¬ ( # rset ≠ 0 ∧ ¬(absloc((W(t1, l1, v1) ' + el0) + R(t, l, v) ', rset, fowl0) ↔ absloc(W(t1, l1, v1) ' + el0, rset, fowl0)) ∧ rset ≠ ∅ ∧ t ∈ rset ∧ (∀ rset0, t0, l0, v0, fowl0. # rset0 = 0 ∨ (absloc(el0 + R(t0, l0, v0) ', rset0, fowl0) ↔ absloc(el0, rset0, fowl0)) ∨ rset0 = ∅ ∨ ¬ t0 ∈ rset0)) ⊦

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 10 from proof absloc-addRead (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  # rset ≠ 0, ¬(absloc((W(t1, l1, v1) ' + el0) + R(t, l, v) ', rset, fow ' + fowl0) ↔ absloc(W(t1, l1, v1) ' + el0, rset, fow ' + fowl0)), rset ≠ ∅, t ∈ rset, ∀ rset0, t0, l0, v0, fowl0. # rset0 = 0 ∨ (absloc(el0 + R(t0, l0, v0) ', rset0, fowl0) ↔ absloc(el0, rset0, fowl0)) ∨ rset0 = ∅ ∨ ¬ t0 ∈ rset0, ∀ rset0, t0, l0, v0, el, t2, l2, v2. # rset0 = 0 ∨ (absloc((W(t0, l0, v0) ' + el) + R(t2, l2, v2) ', rset0, fowl0) ↔ absloc(W(t0, l0, v0) ' + el, rset0, fowl0)) ∨ rset0 = ∅ ∨ ¬ t2 ∈ rset0 ∨ ¬ (∀ rset0, t0, l0, v0, fowl0. # rset0 = 0 ∨ (absloc(el + R(t0, l0, v0) ', rset0, fowl0) ↔ absloc(el, rset0, fowl0)) ∨ rset0 = ∅ ∨ ¬ t0 ∈ rset0) ⊦

Rule argument

Additional information

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

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

User applied rule constructor cut

And obtained the following new goals

• Proof step 12:

  fow = FO(t3), # rset ≠ 0, ¬(absloc((W(t1, l1, v1) ' + el0) + R(t, l, v) ', rset, fow ' + fowl0) ↔ absloc(W(t1, l1, v1) ' + el0, rset, fow ' + fowl0)), rset ≠ ∅, t ∈ rset, ∀ rset0, t0, l0, v0, el, t2, l2, v2. # rset0 = 0 ∨ (absloc((W(t0, l0, v0) ' + el) + R(t2, l2, v2) ', rset0, fowl0) ↔ absloc(W(t0, l0, v0) ' + el, rset0, fowl0)) ∨ rset0 = ∅ ∨ ¬ t2 ∈ rset0 ∨ ¬ (∀ rset0, t0, l0, v0, fowl0. # rset0 = 0 ∨ (absloc(el + R(t0, l0, v0) ', rset0, fowl0) ↔ absloc(el, rset0, fowl0)) ∨ rset0 = ∅ ∨ ¬ t0 ∈ rset0), ∀ rset0, t0, l0, v0, fowl0. # rset0 = 0 ∨ (absloc(el0 + R(t0, l0, v0) ', rset0, fowl0) ↔ absloc(el0, rset0, fowl0)) ∨ rset0 = ∅ ∨ ¬ t0 ∈ rset0 ⊦

• Proof step 14:

  fow = W(v3, t3), # rset ≠ 0, ¬(absloc((W(t1, l1, v1) ' + el0) + R(t, l, v) ', rset, fow ' + fowl0) ↔ absloc(W(t1, l1, v1) ' + el0, rset, fow ' + fowl0)), rset ≠ ∅, t ∈ rset, ∀ rset0, t0, l0, v0, el, t2, l2, v2. # rset0 = 0 ∨ (absloc((W(t0, l0, v0) ' + el) + R(t2, l2, v2) ', rset0, fowl0) ↔ absloc(W(t0, l0, v0) ' + el, rset0, fowl0)) ∨ rset0 = ∅ ∨ ¬ t2 ∈ rset0 ∨ ¬ (∀ rset0, t0, l0, v0, fowl0. # rset0 = 0 ∨ (absloc(el + R(t0, l0, v0) ', rset0, fowl0) ↔ absloc(el, rset0, fowl0)) ∨ rset0 = ∅ ∨ ¬ t0 ∈ rset0), ∀ rset0, t0, l0, v0, fowl0. # rset0 = 0 ∨ (absloc(el0 + R(t0, l0, v0) ', rset0, fowl0) ↔ absloc(el0, rset0, fowl0)) ∨ rset0 = ∅ ∨ ¬ t0 ∈ rset0 ⊦

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  # rset ≠ 0, ¬(absloc((W(t1, l1, v1) ' + el0) + R(t, l, v) ', rset, fowl0) ↔ absloc(W(t1, l1, v1) ' + el0, rset, fowl0)), rset ≠ ∅, t ∈ rset, ∀ rset0, t0, l0, v0, fowl0. # rset0 = 0 ∨ (absloc(el0 + R(t0, l0, v0) ', rset0, fowl0) ↔ absloc(el0, rset0, fowl0)) ∨ rset0 = ∅ ∨ ¬ t0 ∈ rset0, ∀ rset0, t0, l0, v0, el, t2, l2, v2. # rset0 = 0 ∨ (absloc((W(t0, l0, v0) ' + el) + R(t2, l2, v2) ', rset0, fowl0) ↔ absloc(W(t0, l0, v0) ' + el, rset0, fowl0)) ∨ rset0 = ∅ ∨ ¬ t2 ∈ rset0 ∨ ¬ (∀ rset0, t0, l0, v0, fowl0. # rset0 = 0 ∨ (absloc(el + R(t0, l0, v0) ', rset0, fowl0) ↔ absloc(el, rset0, fowl0)) ∨ rset0 = ∅ ∨ ¬ t0 ∈ rset0) ⊦

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 13 from proof absloc-addRead (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  # rset ≠ 0, ¬(absloc(el0 + R(t, l, v) ', rset, fowl0) ↔ absloc(el0, rset, fowl0)), rset ≠ ∅, t ∈ rset, ∀ rset0, t0, l0, v0, el, t2, l2, v2. # rset0 = 0 ∨ (absloc((W(t0, l0, v0) ' + el) + R(t2, l2, v2) ', rset0, fowl0) ↔ absloc(W(t0, l0, v0) ' + el, rset0, fowl0)) ∨ rset0 = ∅ ∨ ¬ t2 ∈ rset0 ∨ ¬ (∀ rset0, t0, l0, v0, fowl0. # rset0 = 0 ∨ (absloc(el + R(t0, l0, v0) ', rset0, fowl0) ↔ absloc(el, rset0, fowl0)) ∨ rset0 = ∅ ∨ ¬ t0 ∈ rset0), ∀ rset0, t0, l0, v0, fowl0. # rset0 = 0 ∨ (absloc(el0 + R(t0, l0, v0) ', rset0, fowl0) ↔ absloc(el0, rset0, fowl0)) ∨ rset0 = ∅ ∨ ¬ t0 ∈ rset0 ⊦

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 15 from proof absloc-addRead (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

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