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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

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

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  ¬(absloc([] + W(t, l, v) ', rset, fowl + W(v, t) ') ↔ absloc([], rset, fowl)) ⊦

• Proof step 9:

  ¬(absloc((e + el0) + W(t, l, v) ', rset, fowl + W(v, t) ') ↔ absloc(e + el0, rset, fowl)), ∀ t, l, v, rset, fowl. absloc(el0 + W(t, l, v) ', rset, fowl + W(v, t) ') ↔ absloc(el0, rset, fowl) ⊦

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

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

Rule argument

Additional information

Used simplifier rules: absloc-base: ⊦ absloc([], rset, fowl) ↔ fowl |W = []; a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ [] + x = x; (s)

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

User applied rule structural induction

And obtained the following new goals

• Proof step 5:

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

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

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

Rule argument

Additional information

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

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

User applied rule constructor cut

And obtained the following new goals

• Proof step 7:

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

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

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

Rule argument

Additional information

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

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

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: t, l, v, rset

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  ¬(absloc((e ' + el0) + W(t, l, v) ', rset, fowl + W(v, t) ') ↔ absloc(e ' + el0, rset, fowl)), ∀ t, l, v, rset, fowl. absloc(el0 + W(t, l, v) ', rset, fowl + W(v, t) ') ↔ absloc(el0, rset, fowl) ⊦

Rule argument

Additional information

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

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

User applied rule constructor cut

And obtained the following new goals

• Proof step 11:

  e = R(t0, l0, v0), ¬(absloc((e ' + el0) + W(t, l, v) ', rset, fowl + W(v, t) ') ↔ absloc(e ' + el0, rset, fowl)), ∀ t, l, v, rset, fowl. absloc(el0 + W(t, l, v) ', rset, fowl + W(v, t) ') ↔ absloc(el0, rset, fowl) ⊦

• Proof step 13:

  e = W(t0, l0, v0), ¬(absloc((e ' + el0) + W(t, l, v) ', rset, fowl + W(v, t) ') ↔ absloc(e ' + el0, rset, fowl)), ∀ t, l, v, rset, fowl. absloc(el0 + W(t, l, v) ', rset, fowl + W(v, t) ') ↔ absloc(el0, rset, fowl) ⊦

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  ¬(absloc(el0 + W(t, l, v) ', rset, fowl + W(v, t) ') ↔ absloc(el0, rset, fowl)), ¬ t0 ∈ rset → FO(t0) ∈ fowl, ∀ t, l, v, rset, fowl. absloc(el0 + W(t, l, v) ', rset, fowl + W(v, t) ') ↔ absloc(el0, rset, 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 ⊦ FO(tid) ≠ W(v, tid0); (s) ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s)

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

User applied rule all left

And closed the goal!

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  ¬(absloc((W(t0, l0, v0) ' + el0) + W(t, l, v) ', rset, fowl + W(v, t) ') ↔ absloc(W(t0, l0, v0) ' + el0, rset, fowl)), ∀ t, l, v, rset, fowl. absloc(el0 + W(t, l, v) ', rset, fowl + W(v, t) ') ↔ absloc(el0, rset, fowl) ⊦

Rule argument

Additional information

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

User applied rule structural induction

And obtained the following new goals

• Proof step 15:

  ¬(absloc((W(t0, l0, v0) ' + el0) + W(t, l, v) ', rset, [] + W(v, t) ') ↔ absloc(W(t0, l0, v0) ' + el0, rset, [])), ∀ t, l, v, rset, fowl. absloc(el0 + W(t, l, v) ', rset, fowl + W(v, t) ') ↔ absloc(el0, rset, fowl) ⊦

• Proof step 22:

  ¬(absloc((W(t0, l0, v0) ' + el0) + W(t, l, v) ', rset, (fow + fowl0) + W(v, t) ') ↔ absloc(W(t0, l0, v0) ' + el0, rset, fow + fowl0)), ∀ t, l, v, rset, fowl. absloc(el0 + W(t, l, v) ', rset, fowl + W(v, t) ') ↔ absloc(el0, rset, fowl), ∀ t0, l0, v0, el0, t, l, v, rset. ¬ ( ¬(absloc((W(t0, l0, v0) ' + el0) + W(t, l, v) ', rset, fowl0 + W(v, t) ') ↔ absloc(W(t0, l0, v0) ' + el0, rset, fowl0)) ∧ (∀ t, l, v, rset, fowl. absloc(el0 + W(t, l, v) ', rset, fowl + W(v, t) ') ↔ absloc(el0, rset, fowl))) ⊦

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  absloc(el0 + W(t0, l, v0) ', rset, []), ∀ t, l, v, rset, fowl. absloc(el0 + W(t, l, v) ', rset, fowl + W(v, t) ') ↔ absloc(el0, rset, fowl) ⊦

Rule argument

Additional information

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

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

User applied rule weakening

And obtained the following new goals

• Proof step 17:

  absloc(el0 + W(t0, l, v0) ', rset, []) ⊦

Rule argument

Additional information

Proof step 17 from proof absloc-addWrite (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 18:

  absloc((e + el) + W(t0, l, v0) ', rset, []), ∀ t0, l, v0, rset. ¬ absloc(el + W(t0, l, v0) ', rset, []) ⊦

Rule argument

Additional information

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

Proof step 18 from proof absloc-addWrite (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  absloc((e ' + el) + W(t0, l, v0) ', rset, []), ∀ t0, l, v0, rset. ¬ absloc(el + W(t0, l, v0) ', rset, []) ⊦

Rule argument

Additional information

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

Proof step 19 from proof absloc-addWrite (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 20:

  e = R(t, l0, v), absloc((e ' + el) + W(t0, l, v0) ', rset, []), ∀ t0, l, v0, rset. ¬ absloc(el + W(t0, l, v0) ', rset, []) ⊦

Rule argument

Additional information

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

Proof step 20 from proof absloc-addWrite (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  # rset ≠ 0, rset ≠ ∅, absloc(el + W(t0, l, v0) ', rset, []), t ∈ rset, ∀ t0, l, v0, rset. ¬ absloc(el + W(t0, l, v0) ', rset, []) ⊦

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); size-zero-01: ⊦ s ≠ ∅ → # s ≠ 0; (forward) from specification set-basic ne-01: ⊦ a ∈ s → s ≠ ∅; (forward) from specification set-basic a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ ¬ a ∈ []; (s)

Proof step 21 from proof absloc-addWrite (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: t0, l, v0, rset

Proof step 22 from proof absloc-addWrite (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

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

Rule argument

Additional information

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

Proof step 23 from proof absloc-addWrite (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 24:

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

• Proof step 26:

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

Rule argument

Additional information

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

Proof step 24 from proof absloc-addWrite (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  ¬(absloc((W(t0, l0, v0) ' + el0) + W(t, l, v) ', rset, fowl0 + W(v, t) ') ↔ absloc(W(t0, l0, v0) ' + el0, rset, fowl0)), ∀ t, l, v, rset, fowl. absloc(el0 + W(t, l, v) ', rset, fowl + W(v, t) ') ↔ absloc(el0, rset, fowl), ∀ t1, l1, v1, el, t2, l2, v2, rset0. (absloc((W(t1, l1, v1) ' + el) + W(t2, l2, v2) ', rset0, fowl0 + W(v2, t2) ') ↔ absloc(W(t1, l1, v1) ' + el, rset0, fowl0)) ∨ ¬(∀ t, l, v, rset, fowl. absloc(el + W(t, l, v) ', rset, fowl + W(v, t) ') ↔ absloc(el, rset, fowl)) ⊦

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

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: t0, l0, v0, el0, t, l, v, rset

Proof step 26 from proof absloc-addWrite (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  ¬(absloc(el0 + W(t, l, v) ', rset, fowl0 + W(v, t) ') ↔ absloc(el0, rset, fowl0)), ∀ t1, l1, v1, el, t2, l2, v2, rset0. (absloc((W(t1, l1, v1) ' + el) + W(t2, l2, v2) ', rset0, fowl0 + W(v2, t2) ') ↔ absloc(W(t1, l1, v1) ' + el, rset0, fowl0)) ∨ ¬(∀ t, l, v, rset, fowl. absloc(el + W(t, l, v) ', rset, fowl + W(v, t) ') ↔ absloc(el, rset, fowl)), ∀ t, l, v, rset, fowl. absloc(el0 + W(t, l, v) ', rset, fowl + W(v, t) ') ↔ absloc(el0, rset, fowl) ⊦

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

User applied rule all left

And closed the goal!

Rule argument

Additional information

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