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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(absloc(el, rset -- t, fowl + FO(t) ') ↔ absloc(el, rset, fowl)), t ∈ rset ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  # rset ≠ 0, ¬(absloc(el, rset -- t, fowl + FO(t) ') ↔ 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-addReadFO (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

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

Rule argument

Additional information

Used simplifier rules: absloc-base: ⊦ absloc([], rset, fowl) ↔ fowl |W = []; List('a) freely generated by [], +;; ⊦ (fowl + fowl0)|W = fowl |W + fowl0 |W; (s) ⊦ FO(t) ' |W = []; (s) ⊦ x + [] = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  # rset ≠ 0, ¬(absloc(e ' + el0, rset -- t, fowl + FO(t) ') ↔ absloc(e ' + el0, rset, fowl)), rset ≠ ∅, t ∈ rset, ∀ rset0, t0, fowl0. # rset0 = 0 ∨ (absloc(el0, rset0 -- t0, fowl0 + FO(t0) ') ↔ absloc(el0, rset0, fowl0)) ∨ rset0 = ∅ ∨ ¬ t0 ∈ rset0 ⊦

Rule argument

Additional information

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

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

User applied rule constructor cut

And obtained the following new goals

• Proof step 6:

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

• Proof step 8:

  e = W(t1, l, v), # rset ≠ 0, ¬(absloc(e ' + el0, rset -- t, fowl + FO(t) ') ↔ absloc(e ' + el0, rset, fowl)), rset ≠ ∅, t ∈ rset, ∀ rset0, t0, fowl0. # rset0 = 0 ∨ (absloc(el0, rset0 -- t0, fowl0 + FO(t0) ') ↔ 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-addReadFO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  # rset ≠ 0, ¬(absloc(el0, rset -- t, fowl + FO(t) ') ↔ absloc(el0, rset, fowl)), rset ≠ ∅, t ∈ rset, ¬ t1 ∈ rset → FO(t1) ∈ fowl, ∀ rset0, t0, fowl0. # rset0 = 0 ∨ (absloc(el0, rset0 -- t0, fowl0 + FO(t0) ') ↔ 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 ⊦ FO(tid) = FO(tid0) ↔ tid = tid0; (s) ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ a ∈ s -- a0 ↔ a ≠ a0 ∧ a ∈ s; (s)

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

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: rset, t, fowl

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

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

Rule argument

Additional information

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

User applied rule structural induction

And obtained the following new goals

• Proof step 10:

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

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  # rset ≠ 0, ¬(absloc(W(t1, l, v) ' + el0, rset -- t, (fow ' + fowl0) + FO(t) ') ↔ absloc(W(t1, l, v) ' + el0, rset, fow ' + fowl0)), rset ≠ ∅, t ∈ rset, ∀ rset0, t0, fowl0. # rset0 = 0 ∨ (absloc(el0, rset0 -- t0, fowl0 + FO(t0) ') ↔ absloc(el0, rset0, fowl0)) ∨ rset0 = ∅ ∨ ¬ t0 ∈ rset0, ∀ rset0, t0, l0, v0, el, t2. # rset0 = 0 ∨ (absloc(W(t0, l0, v0) ' + el, rset0 -- t2, fowl0 + FO(t2) ') ↔ absloc(W(t0, l0, v0) ' + el, rset0, fowl0)) ∨ rset0 = ∅ ∨ ¬ t2 ∈ rset0 ∨ ¬(∀ rset0, t0, fowl0. # rset0 = 0 ∨ (absloc(el, rset0 -- t0, fowl0 + FO(t0) ') ↔ absloc(el, 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 11 from proof absloc-addReadFO (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, l, v) ' + el0, rset -- t, (fow ' + fowl0) + FO(t) ') ↔ absloc(W(t1, l, v) ' + el0, rset, fow ' + fowl0)), rset ≠ ∅, t ∈ rset, ∀ rset0, t0, l0, v0, el, t2. # rset0 = 0 ∨ (absloc(W(t0, l0, v0) ' + el, rset0 -- t2, fowl0 + FO(t2) ') ↔ absloc(W(t0, l0, v0) ' + el, rset0, fowl0)) ∨ rset0 = ∅ ∨ ¬ t2 ∈ rset0 ∨ ¬(∀ rset0, t0, fowl0. # rset0 = 0 ∨ (absloc(el, rset0 -- t0, fowl0 + FO(t0) ') ↔ absloc(el, rset0, fowl0)) ∨ rset0 = ∅ ∨ ¬ t0 ∈ rset0), ∀ rset0, t0, fowl0. # rset0 = 0 ∨ (absloc(el0, rset0 -- t0, fowl0 + FO(t0) ') ↔ absloc(el0, rset0, fowl0)) ∨ rset0 = ∅ ∨ ¬ t0 ∈ rset0 ⊦

• Proof step 14:

  fow = W(v1, t3), # rset ≠ 0, ¬(absloc(W(t1, l, v) ' + el0, rset -- t, (fow ' + fowl0) + FO(t) ') ↔ absloc(W(t1, l, v) ' + el0, rset, fow ' + fowl0)), rset ≠ ∅, t ∈ rset, ∀ rset0, t0, l0, v0, el, t2. # rset0 = 0 ∨ (absloc(W(t0, l0, v0) ' + el, rset0 -- t2, fowl0 + FO(t2) ') ↔ absloc(W(t0, l0, v0) ' + el, rset0, fowl0)) ∨ rset0 = ∅ ∨ ¬ t2 ∈ rset0 ∨ ¬(∀ rset0, t0, fowl0. # rset0 = 0 ∨ (absloc(el, rset0 -- t0, fowl0 + FO(t0) ') ↔ absloc(el, rset0, fowl0)) ∨ rset0 = ∅ ∨ ¬ t0 ∈ rset0), ∀ rset0, t0, fowl0. # rset0 = 0 ∨ (absloc(el0, rset0 -- t0, fowl0 + FO(t0) ') ↔ 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-addReadFO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  # rset ≠ 0, ¬(absloc(W(t1, l, v) ' + el0, rset -- t, fowl0 + FO(t) ') ↔ absloc(W(t1, l, v) ' + el0, rset, fowl0)), rset ≠ ∅, t ∈ rset, ∀ rset0, t0, fowl0. # rset0 = 0 ∨ (absloc(el0, rset0 -- t0, fowl0 + FO(t0) ') ↔ absloc(el0, rset0, fowl0)) ∨ rset0 = ∅ ∨ ¬ t0 ∈ rset0, ∀ rset0, t0, l0, v0, el, t2. # rset0 = 0 ∨ (absloc(W(t0, l0, v0) ' + el, rset0 -- t2, fowl0 + FO(t2) ') ↔ absloc(W(t0, l0, v0) ' + el, rset0, fowl0)) ∨ rset0 = ∅ ∨ ¬ t2 ∈ rset0 ∨ ¬(∀ rset0, t0, fowl0. # rset0 = 0 ∨ (absloc(el, rset0 -- t0, fowl0 + FO(t0) ') ↔ 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-addReadFO (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  # rset ≠ 0, ¬(absloc(el0, rset -- t, fowl0 + FO(t) ') ↔ absloc(el0, rset, fowl0)), rset ≠ ∅, t ∈ rset, ∀ rset0, t0, l0, v0, el, t2. # rset0 = 0 ∨ (absloc(W(t0, l0, v0) ' + el, rset0 -- t2, fowl0 + FO(t2) ') ↔ absloc(W(t0, l0, v0) ' + el, rset0, fowl0)) ∨ rset0 = ∅ ∨ ¬ t2 ∈ rset0 ∨ ¬(∀ rset0, t0, fowl0. # rset0 = 0 ∨ (absloc(el, rset0 -- t0, fowl0 + FO(t0) ') ↔ absloc(el, rset0, fowl0)) ∨ rset0 = ∅ ∨ ¬ t0 ∈ rset0), ∀ rset0, t0, fowl0. # rset0 = 0 ∨ (absloc(el0, rset0 -- t0, fowl0 + FO(t0) ') ↔ 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-addReadFO (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: rset, t, fowl0