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 75:

  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.^*(a1, a2) ↔ (∃ n. rtc(n, pelem)(a1, a2))

• Proof step 9:

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

Rule argument

Additional information

Used terms: modify(rs), h0, h1

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.^*(a1, a2) ↔ (∃ n. rtc(n, pelem)(a1, a2))

• Proof step 12:

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

Rule argument

Additional information

Used terms: modify(rs), h1, h0

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)(a1, a2) ↔ a1 = a2

• 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)(a1, a2) ↔ a1 = a2

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)(a1, a2) ↔ (∃ a. pelem(a1, a) ∧ rtc(n, pelem)(a, a2))

• Proof step 21:

  ∃ a. modify(rs)(h0, a) ∧ rtc(n0, modify(rs))(a, 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: a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: modify(rs), h0, h1, n0

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, obj. ¬ r ∈ rs ∧ r ∈ h0 ∧ h1 = h0(r := obj)) ∨ (∃ 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, obj. ¬ r ∈ rs ∧ r ∈ h0 ∧ h = h0(r := obj)) ∨ (∃ 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 := ob) ∨ ¬ 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 := ob), r0 ∈ h0, rtc(n, modify(rs))(h1, h), rtc(n0, modify(rs))(h, h1), ¬ r0 ∈ rs, ∀ n. ¬ rtc(n, modify(rs))(h1, h0) ⊦

• Proof step 50:

  h = h0 -- r1, r1 ∈ h0, rtc(n, modify(rs))(h1, h), rtc(n0, modify(rs))(h, h1), ¬ 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), ¬ r ∈ h0, ¬ r ∈ rs, ¬ rtc(n + 1, modify(rs))(h1, h0) ⊦

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)(a1, a2) ↔ (∃ a. rtc(n - 1, pelem)(a1, a) ∧ pelem(a, a2)))

• 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, ∀ a. ¬(rtc(n + 1 - 1, modify(rs))(h1, a) ∧ modify(rs)(a, 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, ∀ a. ¬ rtc(n, modify(rs))(h1, a) ∨ ¬ modify(rs)(a, 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, obj. ¬ r ∈ rs ∧ r ∈ h0 ∧ h1 = h0(r := obj)) ∨ (∃ 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, obj. ¬(¬ r0 ∈ rs ∧ r0 ∈ h0 ++ r ∧ h0 = (h0 ++ r)(r0 := obj)), ∀ 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, obj. r0 ∈ rs ∨ r0 ≠ r ∧ ¬ r0 ∈ h0 ∨ h0 ≠ (h0 ++ r)(r0 := obj), ∀ 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:

  r0 ∈ h0, rtc(n0, modify(rs))(h0(r0 := ob), h1), rtc(n, modify(rs))(h1, h0(r0 := ob)), ¬ 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:

  r0 ∈ h0, rtc(n, modify(rs))(h1, h0(r0 := ob)), rtc(n0, modify(rs))(h0(r0 := ob), h1), ¬ r0 ∈ rs, ¬ rtc(n + 1, modify(rs))(h1, h0) ⊦

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)(a1, a2) ↔ (∃ a. rtc(n - 1, pelem)(a1, a) ∧ pelem(a, a2)))

• Proof step 43:

  n + 1 ≠ 0, r0 ∈ h0, rtc(n0, modify(rs))(h0(r0 := ob), h1), rtc(n, modify(rs))(h1, h0(r0 := ob)), ¬ r0 ∈ rs, ∀ a. ¬(rtc(n + 1 - 1, modify(rs))(h1, a) ∧ modify(rs)(a, 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:

  r0 ∈ h0, rtc(n, modify(rs))(h1, h0(r0 := ob)), rtc(n0, modify(rs))(h0(r0 := ob), h1), ¬ r0 ∈ rs, ∀ a. ¬ rtc(n, modify(rs))(h1, a) ∨ ¬ modify(rs)(a, 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:

  r0 ∈ h0, rtc(n0, modify(rs))(h0(r0 := ob), h1), rtc(n, modify(rs))(h1, h0(r0 := ob)), ¬ r0 ∈ rs, ¬ rtc(n, modify(rs))(h1, h0(r0 := ob)) ∨ ¬ modify(rs)(h0(r0 := ob), h0) ⊦

Rule argument

Additional information

Used terms: h0(r0 := ob)

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:

  r0 ∈ h0, rtc(n, modify(rs))(h1, h0(r0 := ob)), rtc(n0, modify(rs))(h0(r0 := ob), h1), ¬ modify(rs)(h0(r0 := ob), 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, obj. ¬ r ∈ rs ∧ r ∈ h0 ∧ h1 = h0(r := obj)) ∨ (∃ r. ¬ r ∈ rs ∧ r ∈ h0 ∧ h1 = h0 -- r)

• Proof step 48:

  r0 ∈ h0, rtc(n0, modify(rs))(h0(r0 := ob), h1), rtc(n, modify(rs))(h1, h0(r0 := ob)), ¬ r0 ∈ rs, ∀ r. ¬(¬ r ∈ rs ∧ r ≠ null ∧ ¬ r ∈ h0(r0 := ob) ∧ h0 = h0(r0 := ob) ++ r), ∀ r, obj. ¬(¬ r ∈ rs ∧ r ∈ h0(r0 := ob) ∧ h0 = h0(r0 := ob)(r := obj)), ∀ r. ¬(¬ r ∈ rs ∧ r ∈ h0(r0 := ob) ∧ h0 = h0(r0 := ob) -- r) ⊦

Rule argument

Additional information

Used terms: rs, h0(r0 := ob), 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:

  r0 ∈ h0, rtc(n, modify(rs))(h1, h0(r0 := ob)), rtc(n0, modify(rs))(h0(r0 := ob), h1), ¬ r0 ∈ rs, ∀ r. r ∈ rs ∨ ¬ r ∈ h0 ∨ h0 ≠ h0(r0 := ob) -- r, ∀ r, obj. r ∈ rs ∨ ¬ r ∈ h0 ∨ h0 ≠ h0(r0 := ob)(r := obj), ∀ r. r ∈ rs ∨ r = null ∨ r ∈ h0 ∨ h0 ≠ h0(r0 := ob) ++ 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 closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ h(r := o0)(r := o1) = h(r := o1); (s) r ∈ h ⊦ h(r) = o → h(r := o) = h; (s) 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:

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

Rule argument

Additional information

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

User applied rule all left

And obtained the following new goals

• Proof step 52:

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

Rule argument

Additional information

Used terms: n + 2

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 53:

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

• Proof step 54:

  n + 2 ≠ 0, r1 ∈ h0, rtc(n0, modify(rs))(h0 -- r1, h1), rtc(n, modify(rs))(h1, h0 -- r1), ¬ r1 ∈ rs, ∀ a. ¬(rtc(n + 2 - 1, modify(rs))(h1, a) ∧ modify(rs)(a, 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 53 from proof modify+-sym (previous step) (back to tree)

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 55:

  r1 ∈ h0, rtc(n, modify(rs))(h1, h0 -- r1), rtc(n0, modify(rs))(h0 -- r1, h1), ¬ r1 ∈ rs, ∀ a. ¬ rtc(1 + n, modify(rs))(h1, a) ∨ ¬ modify(rs)(a, 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 55 from proof modify+-sym (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 56:

  r1 ∈ h0, rtc(n0, modify(rs))(h0 -- r1, h1), rtc(n, modify(rs))(h1, h0 -- r1), ¬ 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 56 from proof modify+-sym (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 57:

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

• Proof step 66:

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

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 58:

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

• Proof step 59:

  1 + n ≠ 0, r1 ∈ h0, rtc(n0, modify(rs))(h0 -- r1, h1), rtc(n, modify(rs))(h1, h0 -- r1), ¬ r1 ∈ rs, ∀ a. ¬(rtc(1 + n - 1, modify(rs))(h1, a) ∧ modify(rs)(a, (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 58 from proof modify+-sym (previous step) (back to tree)

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 60:

  r1 ∈ h0, rtc(n, modify(rs))(h1, h0 -- r1), rtc(n0, modify(rs))(h0 -- r1, h1), ¬ r1 ∈ rs, ∀ a. ¬ rtc(n, modify(rs))(h1, a) ∨ ¬ modify(rs)(a, (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 60 from proof modify+-sym (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 61:

  r1 ∈ h0, rtc(n0, modify(rs))(h0 -- r1, h1), rtc(n, modify(rs))(h1, h0 -- r1), ¬ 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 61 from proof modify+-sym (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 62:

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

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 63:

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

• Proof step 64:

  r1 ∈ h0, rtc(n0, modify(rs))(h0 -- r1, h1), rtc(n, modify(rs))(h1, h0 -- r1), ¬ r1 ∈ rs, ∀ r. ¬(¬ r ∈ rs ∧ r ≠ null ∧ ¬ r ∈ h0 -- r1 ∧ (h0 -- r1) ++ r1 = (h0 -- r1) ++ r), ∀ r, obj. ¬(¬ r ∈ rs ∧ r ∈ h0 -- r1 ∧ (h0 -- r1) ++ r1 = (h0 -- r1)(r := obj)), ∀ 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 63 from proof modify+-sym (previous step) (back to tree)

Lemma modify

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:

  r1 ∈ h0, rtc(n, modify(rs))(h1, h0 -- r1), rtc(n0, modify(rs))(h0 -- r1, h1), ¬ 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, obj. r ∈ rs ∨ r = r1 ∨ ¬ r ∈ h0 ∨ (h0 -- r1) ++ r1 ≠ (h0 -- r1)(r := obj) ⊦

Rule argument

Additional information

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

Proof step 65 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 66 from proof modify+-sym (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 67:

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

• Proof step 68:

  r1 ∈ h0, rtc(n0, modify(rs))(h0 -- r1, h1), rtc(n, modify(rs))(h1, h0 -- r1), ¬ r1 ∈ rs, ∀ r. ¬(¬ r ∈ rs ∧ r ≠ null ∧ ¬ r ∈ (h0 -- r1) ++ r1 ∧ h0 = (h0 -- r1) ++ r1 ++ r), ∀ r, obj. ¬(¬ r ∈ rs ∧ r ∈ (h0 -- r1) ++ r1 ∧ h0 = ((h0 -- r1) ++ r1)(r := obj)), ∀ 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 67 from proof modify+-sym (previous step) (back to tree)

Lemma modify

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 69:

  r1 ∈ h0, rtc(n, modify(rs))(h1, h0 -- r1), rtc(n0, modify(rs))(h0 -- r1, h1), ¬ r1 ∈ rs, ∀ r. r ∈ rs ∨ ¬ r ∈ h0 ∨ h0 ≠ ((h0 -- r1) ++ r1) -- r, ∀ r, obj. r ∈ rs ∨ ¬ r ∈ h0 ∨ h0 ≠ ((h0 -- r1) ++ r1)(r := obj), ∀ 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 69 from proof modify+-sym (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 70:

  r1 ∈ h0, rtc(n0, modify(rs))(h0 -- r1, h1), rtc(n, modify(rs))(h1, h0 -- r1), ¬ 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 70 from proof modify+-sym (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 71:

  h0 ≠ ((h0 -- r1) ++ r1)(r1 := h0(r1)), r1 ∈ h0, rtc(n, modify(rs))(h1, h0 -- r1), rtc(n0, modify(rs))(h0 -- r1, h1), ¬ 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 71 from proof modify+-sym (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 72:

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

• Proof step 73:

  r1 ∈ h0, rtc(n0, modify(rs))(h0 -- r1, h1), rtc(n, modify(rs))(h1, h0 -- r1), ¬ 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 72 from proof modify+-sym (previous step) (back to tree)

A spec-lemma

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(r) ≠ (r = r1 ⊃ h0(r1);h0(r)), r ∈ h0, r1 ∈ h0, rtc(n, modify(rs))(h1, h0 -- r1), rtc(n0, modify(rs))(h0 -- r1, h1), ¬ 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 ⊦ (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 74 from proof modify+-sym (previous step) (back to tree)

User applied rule case distinction

And closed the goal!

Rule argument

Additional information

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

User applied rule apply proof lemma

And obtained the following new goals

• Proof step 76:

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

Rule argument

Additional information

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

Proof step 3 used as proof-lemma