Proof step 1 from proof modify+-sym (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(modify*(rs)(h0, h1) ↔ modify*(rs)(h1, h0)) ⊦

Rule argument

Additional information

Proof step 2 from proof modify+-sym (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 3:

  modify*(rs)(h0, h1), ¬ modify*(rs)(h1, h0) ⊦

• Proof step 78:

  modify*(rs)(h1, h0), ¬ modify*(rs)(h0, h1) ⊦

Rule argument

Additional information

Proof step 3 from proof modify+-sym (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ modify*(rs)(h0, h1) ↔ modify(rs) ^*(h0, h1)

• Proof step 5:

  modify*(rs)(h0, h1), ¬ modify(rs) ^*(h1, h0) ⊦

Rule argument

Additional information

Used terms: h0, h1, rs

Proof step 4 from proof modify+-sym (previous step) (back to tree)

Lemma modify+

Proof step 5 from proof modify+-sym (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ modify*(rs)(h0, h1) ↔ modify(rs) ^*(h0, h1)

• Proof step 7:

  modify(rs) ^*(h0, h1), ¬ modify(rs) ^*(h1, h0) ⊦

Rule argument

Additional information

Used terms: h1, h0, rs

Proof step 6 from proof modify+-sym (previous step) (back to tree)

Lemma modify+

Proof step 7 from proof modify+-sym (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

  ⊦ pelem ^*(a, b) ↔ (∃ n. rtc(n, pelem)(a, b))

• Proof step 9:

  ¬ modify(rs) ^*(h1, h0), ∃ n. rtc(n, modify(rs))(h0, h1) ⊦

Rule argument

Additional information

Used terms: h1, h0, modify(rs)

Proof step 8 from proof modify+-sym (previous step) (back to tree)

A spec-lemma

Proof step 9 from proof modify+-sym (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  rtc(n, modify(rs))(h0, h1), ¬ modify(rs) ^*(h1, h0) ⊦

Rule argument

Additional information

Proof step 10 from proof modify+-sym (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

  ⊦ pelem ^*(a, b) ↔ (∃ n. rtc(n, pelem)(a, b))

• Proof step 12:

  rtc(n, modify(rs))(h0, h1), ∀ n. ¬ rtc(n, modify(rs))(h1, h0) ⊦

Rule argument

Additional information

Used terms: h0, h1, modify(rs)

Proof step 11 from proof modify+-sym (previous step) (back to tree)

A spec-lemma

Proof step 12 from proof modify+-sym (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 13:

  rtc(0, modify(rs))(h0, h1), ∀ n. ¬ rtc(n, modify(rs))(h1, h0) ⊦

• Proof step 18:

  rtc(n0 +1, modify(rs))(h0, h1), ∀ n. ¬ rtc(n, modify(rs))(h1, h0), ∀ rs, h0, h1. ¬(rtc(n0, modify(rs))(h0, h1) ∧ (∀ n. ¬ rtc(n, modify(rs))(h1, h0))) ⊦

Rule argument

Additional information

Used simplifier rules: nat freely generated by 0, +1;;

Proof step 13 from proof modify+-sym (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

  ⊦ rtc(0, pelem)(a, b) ↔ a = b

• Proof step 15:

  h0 = h1, ∀ n. ¬ rtc(n, modify(rs))(h1, h0) ⊦

Rule argument

Additional information

Used terms: modify(rs), h0, h1

Proof step 14 from proof modify+-sym (previous step) (back to tree)

A spec-lemma

Proof step 15 from proof modify+-sym (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 16:

  h0 = h1, ¬ rtc(0, modify(rs))(h1, h0) ⊦

Rule argument

Additional information

Used terms: 0

Proof step 16 from proof modify+-sym (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

  ⊦ rtc(0, pelem)(a, b) ↔ a = b

Rule argument

Additional information

Used terms: modify(rs), h1, h0

Proof step 17 from proof modify+-sym (previous step) (back to tree)

A spec-lemma

Proof step 18 from proof modify+-sym (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  rtc(n0 + 1, modify(rs))(h0, h1), ∀ n. ¬ rtc(n, modify(rs))(h1, h0), ∀ rs0, h, h2. ¬ rtc(n0, modify(rs0))(h, h2) ∨ ¬(∀ n. ¬ rtc(n, modify(rs0))(h2, h)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m +1 = m + 1; (s)

Proof step 19 from proof modify+-sym (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

  ⊦ rtc(n + 1, pelem)(a, b) ↔ (∃ c. pelem(a, c) ∧ rtc(n, pelem)(c, b))

• Proof step 21:

  ∀ rs0, h, h2. ¬ rtc(n0, modify(rs0))(h, h2) ∨ ¬(∀ n. ¬ rtc(n, modify(rs0))(h2, h)), ∀ n. ¬ rtc(n, modify(rs))(h1, h0), ∃ c. modify(rs)(h0, c) ∧ rtc(n0, modify(rs))(c, h1) ⊦

Rule argument

Additional information

Used terms: n0, modify(rs), h0, h1

Proof step 20 from proof modify+-sym (previous step) (back to tree)

A spec-lemma

Proof step 21 from proof modify+-sym (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  modify(rs)(h0, h), rtc(n0, modify(rs))(h, h1), ∀ n. ¬ rtc(n, modify(rs))(h1, h0), ∀ rs0, h, h2. ¬ rtc(n0, modify(rs0))(h, h2) ∨ ¬(∀ n. ¬ rtc(n, modify(rs0))(h2, h)) ⊦

Rule argument

Additional information

Proof step 22 from proof modify+-sym (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 23:

  modify(rs)(h0, h), rtc(n0, modify(rs))(h, h1), ∀ n. ¬ rtc(n, modify(rs))(h1, h0), ¬ rtc(n0, modify(rs))(h, h1) ∨ ¬(∀ n. ¬ rtc(n, modify(rs))(h1, h)) ⊦

Rule argument

Additional information

Used terms: rs, h, h1

Proof step 23 from proof modify+-sym (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  modify(rs)(h0, h), rtc(n0, modify(rs))(h, h1), rtc(n, modify(rs))(h1, h), ∀ n. ¬ rtc(n, modify(rs))(h1, h0) ⊦

Rule argument

Additional information

Proof step 24 from proof modify+-sym (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 25:

  ⊦ modify(rs)(h0, h1) ↔ (∃ r. ¬ r ∈ rs ∧ r ≠ null ∧ ¬ r ∈ h0 ∧ h1 = h0 ++ r) ∨ (∃ r, o. ¬ r ∈ rs ∧ r ∈ h0 ∧ h1 = h0[r, o]) ∨ (∃ r. ¬ r ∈ rs ∧ r ∈ h0 ∧ h1 = h0 -- r)

• Proof step 26:

  rtc(n, modify(rs))(h1, h), rtc(n0, modify(rs))(h, h1), ∀ n. ¬ rtc(n, modify(rs))(h1, h0), (∃ r. ¬ r ∈ rs ∧ r ≠ null ∧ ¬ r ∈ h0 ∧ h = h0 ++ r) ∨ (∃ r, o. ¬ r ∈ rs ∧ r ∈ h0 ∧ h = h0[r, o]) ∨ (∃ r. ¬ r ∈ rs ∧ r ∈ h0 ∧ h = h0 -- r) ⊦

Rule argument

Additional information

Used terms: rs, h0, h

Proof step 25 from proof modify+-sym (previous step) (back to tree)

Lemma modify

Proof step 26 from proof modify+-sym (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  rtc(n0, modify(rs))(h, h1), rtc(n, modify(rs))(h1, h), ∀ n. ¬ rtc(n, modify(rs))(h1, h0), ¬ r ∈ rs ∧ r ≠ null ∧ ¬ r ∈ h0 ∧ h = h0 ++ r ∨ ¬ r0 ∈ rs ∧ r0 ∈ h0 ∧ h = h0[r0, o] ∨ ¬ r1 ∈ rs ∧ r1 ∈ h0 ∧ h = h0 -- r1 ⊦

Rule argument

Additional information

Proof step 27 from proof modify+-sym (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 28:

  h = h0 ++ r, r ≠ null, rtc(n, modify(rs))(h1, h), rtc(n0, modify(rs))(h, h1), ¬ r ∈ h0, ¬ r ∈ rs, ∀ n. ¬ rtc(n, modify(rs))(h1, h0) ⊦

• Proof step 39:

  h = h0[r0, o], rtc(n, modify(rs))(h1, h), rtc(n0, modify(rs))(h, h1), r0 ∈ h0, ¬ r0 ∈ rs, ∀ n. ¬ rtc(n, modify(rs))(h1, h0) ⊦

• Proof step 53:

  h = h0 -- r1, rtc(n, modify(rs))(h1, h), rtc(n0, modify(rs))(h, h1), r1 ∈ h0, ¬ r1 ∈ rs, ∀ n. ¬ rtc(n, modify(rs))(h1, h0) ⊦

Rule argument

Additional information

Proof step 28 from proof modify+-sym (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  r ≠ null, rtc(n0, modify(rs))(h0 ++ r, h1), rtc(n, modify(rs))(h1, h0 ++ r), ¬ r ∈ h0, ¬ r ∈ rs, ∀ n. ¬ rtc(n, modify(rs))(h1, h0) ⊦

Rule argument

Additional information

Proof step 29 from proof modify+-sym (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 30:

  r ≠ null, rtc(n, modify(rs))(h1, h0 ++ r), rtc(n0, modify(rs))(h0 ++ r, h1), ¬ rtc(n + 1, modify(rs))(h1, h0), ¬ r ∈ h0, ¬ r ∈ rs ⊦

Rule argument

Additional information

Used terms: n + 1

Proof step 30 from proof modify+-sym (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 31:

  ⊦ n ≠ 0 → (rtc(n, pelem)(a, b) ↔ (∃ c. rtc(n - 1, pelem)(a, c) ∧ pelem(c, b)))

• Proof step 32:

  n + 1 ≠ 0, r ≠ null, rtc(n0, modify(rs))(h0 ++ r, h1), rtc(n, modify(rs))(h1, h0 ++ r), ¬ r ∈ h0, ¬ r ∈ rs, ∀ c. ¬(rtc(n + 1 - 1, modify(rs))(h1, c) ∧ modify(rs)(c, h0)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; (ws) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: n + 1, modify(rs), h1, h0

Proof step 31 from proof modify+-sym (previous step) (back to tree)

A spec-lemma

Proof step 32 from proof modify+-sym (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

  r ≠ null, rtc(n, modify(rs))(h1, h0 ++ r), rtc(n0, modify(rs))(h0 ++ r, h1), ¬ r ∈ h0, ¬ r ∈ rs, ∀ c. ¬ rtc(n, modify(rs))(h1, c) ∨ ¬ modify(rs)(c, h0) ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ n + 0 = n; (s) ⊦ n ≤ m → m + n0 - n = (m - n) + n0; (s) ⊦ m + 1 ≠ 0; (s)

Proof step 33 from proof modify+-sym (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 34:

  r ≠ null, rtc(n0, modify(rs))(h0 ++ r, h1), rtc(n, modify(rs))(h1, h0 ++ r), ¬ r ∈ h0, ¬ r ∈ rs, ¬ rtc(n, modify(rs))(h1, h0 ++ r) ∨ ¬ modify(rs)(h0 ++ r, h0) ⊦

Rule argument

Additional information

Used terms: h0 ++ r

Proof step 34 from proof modify+-sym (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

  r ≠ null, rtc(n, modify(rs))(h1, h0 ++ r), rtc(n0, modify(rs))(h0 ++ r, h1), ¬ modify(rs)(h0 ++ r, h0), ¬ r ∈ h0, ¬ r ∈ rs ⊦

Rule argument

Additional information

Proof step 35 from proof modify+-sym (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 36:

  ⊦ modify(rs)(h0, h1) ↔ (∃ r. ¬ r ∈ rs ∧ r ≠ null ∧ ¬ r ∈ h0 ∧ h1 = h0 ++ r) ∨ (∃ r, o. ¬ r ∈ rs ∧ r ∈ h0 ∧ h1 = h0[r, o]) ∨ (∃ r. ¬ r ∈ rs ∧ r ∈ h0 ∧ h1 = h0 -- r)

• Proof step 37:

  r ≠ null, rtc(n0, modify(rs))(h0 ++ r, h1), rtc(n, modify(rs))(h1, h0 ++ r), ¬ r ∈ h0, ¬ r ∈ rs, ∀ r0. ¬(¬ r0 ∈ rs ∧ r0 ≠ null ∧ ¬ r0 ∈ h0 ++ r ∧ h0 = h0 ++ r ++ r0), ∀ r0, o. ¬(¬ r0 ∈ rs ∧ r0 ∈ h0 ++ r ∧ h0 = (h0 ++ r)[r0, o]), ∀ r0. ¬(¬ r0 ∈ rs ∧ r0 ∈ h0 ++ r ∧ h0 = (h0 ++ r) -- r0) ⊦

Rule argument

Additional information

Used terms: rs, h0 ++ r, h0

Proof step 36 from proof modify+-sym (previous step) (back to tree)

Lemma modify

Proof step 37 from proof modify+-sym (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 38:

  r ≠ null, rtc(n, modify(rs))(h1, h0 ++ r), rtc(n0, modify(rs))(h0 ++ r, h1), ¬ r ∈ h0, ¬ r ∈ rs, ∀ r0. r0 ∈ rs ∨ r0 ≠ r ∧ ¬ r0 ∈ h0 ∨ h0 ≠ (h0 ++ r) -- r0, ∀ r0, o. r0 ∈ rs ∨ r0 ≠ r ∧ ¬ r0 ∈ h0 ∨ h0 ≠ (h0 ++ r)[r0, o], ∀ r0. r0 ∈ rs ∨ r0 = null ∨ r0 = r ∨ r0 ∈ h0 ∨ h0 ≠ h0 ++ r ++ r0 ⊦

Rule argument

Additional information

Used simplifier rules: r0 ≠ null, ¬ r0 ∈ h ⊦ r ∈ h ++ r0 ↔ r = r0 ∨ r ∈ h; (s)

Proof step 38 from proof modify+-sym (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ¬ r ∈ h, r ≠ null ⊦ (h ++ r) -- r = h; (s) Used terms: r

Proof step 39 from proof modify+-sym (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 40:

  rtc(n0, modify(rs))(h0[r0, o], h1), rtc(n, modify(rs))(h1, h0[r0, o]), r0 ∈ h0, ¬ r0 ∈ rs, ∀ n. ¬ rtc(n, modify(rs))(h1, h0) ⊦

Rule argument

Additional information

Proof step 40 from proof modify+-sym (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 41:

  rtc(n, modify(rs))(h1, h0[r0, o]), rtc(n0, modify(rs))(h0[r0, o], h1), r0 ∈ h0, ¬ rtc(n + 1, modify(rs))(h1, h0), ¬ r0 ∈ rs ⊦

Rule argument

Additional information

Used terms: n + 1

Proof step 41 from proof modify+-sym (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 42:

  ⊦ n ≠ 0 → (rtc(n, pelem)(a, b) ↔ (∃ c. rtc(n - 1, pelem)(a, c) ∧ pelem(c, b)))

• Proof step 43:

  n + 1 ≠ 0, rtc(n0, modify(rs))(h0[r0, o], h1), rtc(n, modify(rs))(h1, h0[r0, o]), r0 ∈ h0, ¬ r0 ∈ rs, ∀ c. ¬(rtc(n + 1 - 1, modify(rs))(h1, c) ∧ modify(rs)(c, h0)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; (ws) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: n + 1, modify(rs), h1, h0

Proof step 42 from proof modify+-sym (previous step) (back to tree)

A spec-lemma

Proof step 43 from proof modify+-sym (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 44:

  rtc(n, modify(rs))(h1, h0[r0, o]), rtc(n0, modify(rs))(h0[r0, o], h1), r0 ∈ h0, ¬ r0 ∈ rs, ∀ c. ¬ rtc(n, modify(rs))(h1, c) ∨ ¬ modify(rs)(c, h0) ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ n + 0 = n; (s) ⊦ n ≤ m → m + n0 - n = (m - n) + n0; (s) ⊦ m + 1 ≠ 0; (s)

Proof step 44 from proof modify+-sym (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 45:

  rtc(n0, modify(rs))(h0[r0, o], h1), rtc(n, modify(rs))(h1, h0[r0, o]), r0 ∈ h0, ¬ r0 ∈ rs, ¬ rtc(n, modify(rs))(h1, h0[r0, o]) ∨ ¬ modify(rs)(h0[r0, o], h0) ⊦

Rule argument

Additional information

Used terms: h0[r0, o]

Proof step 45 from proof modify+-sym (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 46:

  rtc(n, modify(rs))(h1, h0[r0, o]), rtc(n0, modify(rs))(h0[r0, o], h1), r0 ∈ h0, ¬ modify(rs)(h0[r0, o], h0), ¬ r0 ∈ rs ⊦

Rule argument

Additional information

Proof step 46 from proof modify+-sym (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 47:

  ⊦ modify(rs)(h0, h1) ↔ (∃ r. ¬ r ∈ rs ∧ r ≠ null ∧ ¬ r ∈ h0 ∧ h1 = h0 ++ r) ∨ (∃ r, o. ¬ r ∈ rs ∧ r ∈ h0 ∧ h1 = h0[r, o]) ∨ (∃ r. ¬ r ∈ rs ∧ r ∈ h0 ∧ h1 = h0 -- r)

• Proof step 48:

  rtc(n0, modify(rs))(h0[r0, o], h1), rtc(n, modify(rs))(h1, h0[r0, o]), r0 ∈ h0, ¬ r0 ∈ rs, ∀ r. ¬(¬ r ∈ rs ∧ r ≠ null ∧ ¬ r ∈ h0[r0, o] ∧ h0 = h0[r0, o] ++ r), ∀ r, o0. ¬(¬ r ∈ rs ∧ r ∈ h0[r0, o] ∧ h0 = h0[r0, o][r, o0]), ∀ r. ¬(¬ r ∈ rs ∧ r ∈ h0[r0, o] ∧ h0 = h0[r0, o] -- r) ⊦

Rule argument

Additional information

Used terms: rs, h0[r0, o], h0

Proof step 47 from proof modify+-sym (previous step) (back to tree)

Lemma modify

Proof step 48 from proof modify+-sym (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 49:

  rtc(n, modify(rs))(h1, h0[r0, o]), rtc(n0, modify(rs))(h0[r0, o], h1), r0 ∈ h0, ¬ r0 ∈ rs, ∀ r. r ∈ rs ∨ ¬ r ∈ h0 ∨ h0 ≠ h0[r0, o] -- r, ∀ r, o0. r ∈ rs ∨ ¬ r ∈ h0 ∨ h0 ≠ h0[r0, o][r, o0], ∀ r. r ∈ rs ∨ r = null ∨ r ∈ h0 ∨ h0 ≠ h0[r0, o] ++ r ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ r ∈ h[r0, o] ↔ r ∈ h; (s)

Proof step 49 from proof modify+-sym (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 50:

  rtc(n0, modify(rs))(h0[r0, o], h1), rtc(n, modify(rs))(h1, h0[r0, o]), r0 ∈ h0, ¬ r0 ∈ rs, ∀ r. r ∈ rs ∨ r = null ∨ r ∈ h0 ∨ h0 ≠ h0[r0, o] ++ r, ∀ r. r ∈ rs ∨ ¬ r ∈ h0 ∨ h0 ≠ h0[r0, o] -- r, r0 ∈ rs ∨ ¬ r0 ∈ h0 ∨ h0 ≠ h0[r0, o][r0, h0[r0]] ⊦

Rule argument

Additional information

Used terms: r0, h0[r0]

Proof step 50 from proof modify+-sym (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 51:

  h0 ≠ h0[r0, h0[r0]], rtc(n, modify(rs))(h1, h0[r0, o]), rtc(n0, modify(rs))(h0[r0, o], h1), r0 ∈ h0, ¬ r0 ∈ rs, ∀ r. r ∈ rs ∨ ¬ r ∈ h0 ∨ h0 ≠ h0[r0, o] -- r, ∀ r. r ∈ rs ∨ r = null ∨ r ∈ h0 ∨ h0 ≠ h0[r0, o] ++ r ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ h[r, o0][r, o1] = h[r, o1]; (s)

Proof step 51 from proof modify+-sym (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 52:

  r ∈ h ⊦ h[r] = o → h[r, o] = h

Rule argument

Additional information

Used terms: h0, r0, h0[r0]

Proof step 52 from proof modify+-sym (previous step) (back to tree)

A spec-lemma

Proof step 53 from proof modify+-sym (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 54:

  rtc(n0, modify(rs))(h0 -- r1, h1), rtc(n, modify(rs))(h1, h0 -- r1), r1 ∈ h0, ¬ r1 ∈ rs, ∀ n. ¬ rtc(n, modify(rs))(h1, h0) ⊦

Rule argument

Additional information

Proof step 54 from proof modify+-sym (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 55:

  rtc(n, modify(rs))(h1, h0 -- r1), rtc(n0, modify(rs))(h0 -- r1, h1), r1 ∈ h0, ¬ rtc(n + 2, modify(rs))(h1, h0), ¬ r1 ∈ rs ⊦

Rule argument

Additional information

Used terms: n + 2

Proof step 55 from proof modify+-sym (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 56:

  ⊦ n ≠ 0 → (rtc(n, pelem)(a, b) ↔ (∃ c. rtc(n - 1, pelem)(a, c) ∧ pelem(c, b)))

• Proof step 57:

  n + 2 ≠ 0, rtc(n0, modify(rs))(h0 -- r1, h1), rtc(n, modify(rs))(h1, h0 -- r1), r1 ∈ h0, ¬ r1 ∈ rs, ∀ c. ¬(rtc(n + 2 - 1, modify(rs))(h1, c) ∧ modify(rs)(c, h0)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; (ws) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: n + 2, modify(rs), h1, h0

Proof step 56 from proof modify+-sym (previous step) (back to tree)

A spec-lemma

Proof step 57 from proof modify+-sym (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 58:

  rtc(n, modify(rs))(h1, h0 -- r1), rtc(n0, modify(rs))(h0 -- r1, h1), r1 ∈ h0, ¬ r1 ∈ rs, ∀ c. ¬ rtc(1 + n, modify(rs))(h1, c) ∨ ¬ modify(rs)(c, h0) ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ n ≤ m → m + n0 - n = (m - n) + n0; (s) n < n0 ⊦ (* n) ≠ m0 + (* n0); (s)

Proof step 58 from proof modify+-sym (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 59:

  rtc(n0, modify(rs))(h0 -- r1, h1), rtc(n, modify(rs))(h1, h0 -- r1), r1 ∈ h0, ¬ r1 ∈ rs, ¬ rtc(1 + n, modify(rs))(h1, (h0 -- r1) ++ r1) ∨ ¬ modify(rs)((h0 -- r1) ++ r1, h0) ⊦

Rule argument

Additional information

Used terms: (h0 -- r1) ++ r1

Proof step 59 from proof modify+-sym (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 60:

  rtc(n, modify(rs))(h1, h0 -- r1), rtc(n0, modify(rs))(h0 -- r1, h1), r1 ∈ h0, ¬ rtc(1 + n, modify(rs))(h1, (h0 -- r1) ++ r1), ¬ r1 ∈ rs ⊦

• Proof step 69:

  rtc(n, modify(rs))(h1, h0 -- r1), rtc(n0, modify(rs))(h0 -- r1, h1), r1 ∈ h0, ¬ modify(rs)((h0 -- r1) ++ r1, h0), ¬ r1 ∈ rs ⊦

Rule argument

Additional information

Proof step 60 from proof modify+-sym (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 61:

  ⊦ n ≠ 0 → (rtc(n, pelem)(a, b) ↔ (∃ c. rtc(n - 1, pelem)(a, c) ∧ pelem(c, b)))

• Proof step 62:

  1 + n ≠ 0, rtc(n0, modify(rs))(h0 -- r1, h1), rtc(n, modify(rs))(h1, h0 -- r1), r1 ∈ h0, ¬ r1 ∈ rs, ∀ c. ¬(rtc(1 + n - 1, modify(rs))(h1, c) ∧ modify(rs)(c, (h0 -- r1) ++ r1)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; (ws) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: 1 + n, modify(rs), h1, (h0 -- r1) ++ r1

Proof step 61 from proof modify+-sym (previous step) (back to tree)

A spec-lemma

Proof step 62 from proof modify+-sym (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 63:

  rtc(n, modify(rs))(h1, h0 -- r1), rtc(n0, modify(rs))(h0 -- r1, h1), r1 ∈ h0, ¬ r1 ∈ rs, ∀ c. ¬ rtc(n, modify(rs))(h1, c) ∨ ¬ modify(rs)(c, (h0 -- r1) ++ r1) ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ n + 0 = n; (s) ⊦ n ≤ m → m + n0 - n = (m - n) + n0; (s) ⊦ m + 1 ≠ 0; (s)

Proof step 63 from proof modify+-sym (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 64:

  rtc(n0, modify(rs))(h0 -- r1, h1), rtc(n, modify(rs))(h1, h0 -- r1), r1 ∈ h0, ¬ r1 ∈ rs, ¬ rtc(n, modify(rs))(h1, h0 -- r1) ∨ ¬ modify(rs)(h0 -- r1, (h0 -- r1) ++ r1) ⊦

Rule argument

Additional information

Used terms: h0 -- r1

Proof step 64 from proof modify+-sym (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 65:

  rtc(n, modify(rs))(h1, h0 -- r1), rtc(n0, modify(rs))(h0 -- r1, h1), r1 ∈ h0, ¬ modify(rs)(h0 -- r1, (h0 -- r1) ++ r1), ¬ r1 ∈ rs ⊦

Rule argument

Additional information

Proof step 65 from proof modify+-sym (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 66:

  ⊦ modify(rs)(h0, h1) ↔ (∃ r. ¬ r ∈ rs ∧ r ≠ null ∧ ¬ r ∈ h0 ∧ h1 = h0 ++ r) ∨ (∃ r, o. ¬ r ∈ rs ∧ r ∈ h0 ∧ h1 = h0[r, o]) ∨ (∃ r. ¬ r ∈ rs ∧ r ∈ h0 ∧ h1 = h0 -- r)

• Proof step 67:

  rtc(n0, modify(rs))(h0 -- r1, h1), rtc(n, modify(rs))(h1, h0 -- r1), r1 ∈ h0, ¬ r1 ∈ rs, ∀ r. ¬(¬ r ∈ rs ∧ r ≠ null ∧ ¬ r ∈ h0 -- r1 ∧ (h0 -- r1) ++ r1 = (h0 -- r1) ++ r), ∀ r, o. ¬(¬ r ∈ rs ∧ r ∈ h0 -- r1 ∧ (h0 -- r1) ++ r1 = (h0 -- r1)[r, o]), ∀ r. ¬(¬ r ∈ rs ∧ r ∈ h0 -- r1 ∧ (h0 -- r1) ++ r1 = h0 -- r1 -- r) ⊦

Rule argument

Additional information

Used terms: rs, h0 -- r1, (h0 -- r1) ++ r1

Proof step 66 from proof modify+-sym (previous step) (back to tree)

Lemma modify

Proof step 67 from proof modify+-sym (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 68:

  rtc(n, modify(rs))(h1, h0 -- r1), rtc(n0, modify(rs))(h0 -- r1, h1), r1 ∈ h0, ¬ r1 ∈ rs, ∀ r. r ∈ rs ∨ r = null ∨ r ≠ r1 ∧ r ∈ h0 ∨ (h0 -- r1) ++ r1 ≠ (h0 -- r1) ++ r, ∀ r. r ∈ rs ∨ r = r1 ∨ ¬ r ∈ h0 ∨ (h0 -- r1) ++ r1 ≠ h0 -- r1 -- r, ∀ r, o. r ∈ rs ∨ r = r1 ∨ ¬ r ∈ h0 ∨ (h0 -- r1) ++ r1 ≠ (h0 -- r1)[r, o] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ r ∈ h -- r0 ↔ r ≠ r0 ∧ r ∈ h; (s)

Proof step 68 from proof modify+-sym (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ r ∈ h → r ≠ null; (s) Used terms: r1

Proof step 69 from proof modify+-sym (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 70:

  ⊦ modify(rs)(h0, h1) ↔ (∃ r. ¬ r ∈ rs ∧ r ≠ null ∧ ¬ r ∈ h0 ∧ h1 = h0 ++ r) ∨ (∃ r, o. ¬ r ∈ rs ∧ r ∈ h0 ∧ h1 = h0[r, o]) ∨ (∃ r. ¬ r ∈ rs ∧ r ∈ h0 ∧ h1 = h0 -- r)

• Proof step 71:

  rtc(n0, modify(rs))(h0 -- r1, h1), rtc(n, modify(rs))(h1, h0 -- r1), r1 ∈ h0, ¬ r1 ∈ rs, ∀ r. ¬(¬ r ∈ rs ∧ r ≠ null ∧ ¬ r ∈ (h0 -- r1) ++ r1 ∧ h0 = (h0 -- r1) ++ r1 ++ r), ∀ r, o. ¬(¬ r ∈ rs ∧ r ∈ (h0 -- r1) ++ r1 ∧ h0 = ((h0 -- r1) ++ r1)[r, o]), ∀ r. ¬(¬ r ∈ rs ∧ r ∈ (h0 -- r1) ++ r1 ∧ h0 = ((h0 -- r1) ++ r1) -- r) ⊦

Rule argument

Additional information

Used terms: rs, (h0 -- r1) ++ r1, h0

Proof step 70 from proof modify+-sym (previous step) (back to tree)

Lemma modify

Proof step 71 from proof modify+-sym (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 72:

  rtc(n, modify(rs))(h1, h0 -- r1), rtc(n0, modify(rs))(h0 -- r1, h1), r1 ∈ h0, ¬ r1 ∈ rs, ∀ r. r ∈ rs ∨ ¬ r ∈ h0 ∨ h0 ≠ ((h0 -- r1) ++ r1) -- r, ∀ r, o. r ∈ rs ∨ ¬ r ∈ h0 ∨ h0 ≠ ((h0 -- r1) ++ r1)[r, o], ∀ r. r ∈ rs ∨ r = null ∨ r ∈ h0 ∨ h0 ≠ (h0 -- r1) ++ r1 ++ r ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ r ∈ h -- r0 ↔ r ≠ r0 ∧ r ∈ h; (s) r0 ≠ null, ¬ r0 ∈ h ⊦ r ∈ h ++ r0 ↔ r = r0 ∨ r ∈ h; (s) ⊦ r ∈ h → r ≠ null; (s)

Proof step 72 from proof modify+-sym (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 73:

  rtc(n0, modify(rs))(h0 -- r1, h1), rtc(n, modify(rs))(h1, h0 -- r1), r1 ∈ h0, ¬ r1 ∈ rs, ∀ r. r ∈ rs ∨ r = null ∨ r ∈ h0 ∨ h0 ≠ (h0 -- r1) ++ r1 ++ r, ∀ r. r ∈ rs ∨ ¬ r ∈ h0 ∨ h0 ≠ ((h0 -- r1) ++ r1) -- r, r1 ∈ rs ∨ ¬ r1 ∈ h0 ∨ h0 ≠ ((h0 -- r1) ++ r1)[r1, h0[r1]] ⊦

Rule argument

Additional information

Used terms: r1, h0[r1]

Proof step 73 from proof modify+-sym (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 74:

  h0 ≠ ((h0 -- r1) ++ r1)[r1, h0[r1]], rtc(n, modify(rs))(h1, h0 -- r1), rtc(n0, modify(rs))(h0 -- r1, h1), r1 ∈ h0, ¬ r1 ∈ rs, ∀ r. r ∈ rs ∨ ¬ r ∈ h0 ∨ h0 ≠ ((h0 -- r1) ++ r1) -- r, ∀ r. r ∈ rs ∨ r = null ∨ r ∈ h0 ∨ h0 ≠ (h0 -- r1) ++ r1 ++ r ⊦

Rule argument

Additional information

Proof step 74 from proof modify+-sym (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 75:

  ⊦ h0 = h1 ↔ (∀ r. (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]))

• Proof step 76:

  rtc(n0, modify(rs))(h0 -- r1, h1), rtc(n, modify(rs))(h1, h0 -- r1), r1 ∈ h0, ¬ r1 ∈ rs, ∀ r. r ∈ rs ∨ r = null ∨ r ∈ h0 ∨ h0 ≠ (h0 -- r1) ++ r1 ++ r, ∀ r. r ∈ rs ∨ ¬ r ∈ h0 ∨ h0 ≠ ((h0 -- r1) ++ r1) -- r, ∃ r. ¬((r ∈ h0 ↔ r ∈ ((h0 -- r1) ++ r1)[r1, h0[r1]]) ∧ (r ∈ h0 → h0[r] = ((h0 -- r1) ++ r1)[r1, h0[r1]][r])) ⊦

Rule argument

Additional information

Used terms: h0, ((h0 -- r1) ++ r1)[r1, h0[r1]]

Proof step 75 from proof modify+-sym (previous step) (back to tree)

A spec-lemma

Proof step 76 from proof modify+-sym (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 77:

  h0[r] ≠ (r = r1 ⊃ h0[r1];h0[r]), rtc(n, modify(rs))(h1, h0 -- r1), rtc(n0, modify(rs))(h0 -- r1, h1), r1 ∈ h0, r ∈ h0, ¬ r1 ∈ rs, ∀ r. r ∈ rs ∨ ¬ r ∈ h0 ∨ h0 ≠ ((h0 -- r1) ++ r1) -- r, ∀ r. r ∈ rs ∨ r = null ∨ r ∈ h0 ∨ h0 ≠ (h0 -- r1) ++ r1 ++ r ⊦

Rule argument

Additional information

Used simplifier rules: r ∈ h ⊦ r ≠ r0 → (h -- r0)[r] = h[r]; (s) r ∈ h, r0 ≠ null, ¬ r0 ∈ h ⊦ r ≠ r0 → (h ++ r0)[r] = h[r]; (s) ⊦ r ∈ h -- r0 ↔ r ≠ r0 ∧ r ∈ h; (s) ⊦ r ∈ h → r ≠ null; (s) r0 ≠ null, ¬ r0 ∈ h ⊦ r ∈ h ++ r0 ↔ r = r0 ∨ r ∈ h; (s) ⊦ h[r0, o][r] = (r = r0 ∧ r0 ∈ h ⊃ o;h[r]); (s) ⊦ r ∈ h[r0, o] ↔ r ∈ h; (s)

Proof step 77 from proof modify+-sym (previous step) (back to tree)

User applied rule case distinction

And closed the goal!

Rule argument

Additional information

Proof step 78 from proof modify+-sym (previous step) (back to tree)

User applied rule apply proof lemma

And obtained the following new goals

• Proof step 79:

  modify*(rs)(h0, h1), ¬ modify*(rs)(h1, h0) ⊦

Rule argument

Additional information

Proof step 79 from proof modify+-sym (previous step) (back to tree)

Proof step 3 used as proof-lemma