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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

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

User applied rule case distinction

And obtained the following new goals

• Proof step 3:

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

• Proof step 36:

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

Rule argument

Additional information

Proof step 3 from proof modify-agree (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), ¬ ((h0 ≡ h1))(rs) ⊦

Rule argument

Additional information

Used terms: h1, h0, rs

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

Lemma modify+

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

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

• Proof step 7:

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

Rule argument

Additional information

Used terms: h1, h0, modify(rs)

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  rtc(n, modify(rs))(h0, h1), ¬ ((h0 ≡ h1))(rs) ⊦

Rule argument

Additional information

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

User applied rule structural induction

And obtained the following new goals

• Proof step 9:

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

• Proof step 12:

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

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  ¬ ((h1 ≡ h1))(rs) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ rtc(0, pelem)(a, b) ↔ a = b; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

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

Rule argument

Additional information

Used terms: rs, h1, h1

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

Lemma agree

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

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

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

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

• Proof step 15:

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

Rule argument

Additional information

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

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

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

Rule argument

Additional information

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

User applied rule all left

And obtained the following new goals

• Proof step 17:

  modify(rs)(h0, h), rtc(n0, modify(rs))(h, h1), ¬ ((h0 ≡ h1))(rs), ¬ rtc(n0, modify(rs))(h, h1) ∨ ((h ≡ h1))(rs) ⊦

Rule argument

Additional information

Used terms: rs, h, h1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  modify(rs)(h0, h), rtc(n0, modify(rs))(h, h1), ((h ≡ h1))(rs), ¬ ((h0 ≡ h1))(rs) ⊦

Rule argument

Additional information

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

User applied rule weakening

And obtained the following new goals

• Proof step 19:

  modify(rs)(h0, h), ((h ≡ h1))(rs), ¬ ((h0 ≡ h1))(rs) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

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

• Proof step 21:

  modify(rs)(h0, h), ((h ≡ h1))(rs), ∃ r. ¬(r ∈ rs → (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r])) ⊦

Rule argument

Additional information

Used terms: rs, h1, h0

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

Lemma agree

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  modify(rs)(h0, h), r ∈ rs, ((h ≡ h1))(rs) ⊦ (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r])

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 23:

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

• Proof step 24:

  modify(rs)(h0, h), r ∈ rs, ∀ r. r ∈ rs → (r ∈ h ↔ r ∈ h1) ∧ (r ∈ h → h[r] = h1[r]) ⊦ (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r])

Rule argument

Additional information

Used terms: rs, h1, h

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

Lemma agree

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

User applied rule all left

And obtained the following new goals

• Proof step 25:

  modify(rs)(h0, h), r ∈ rs, r ∈ rs → (r ∈ h ↔ r ∈ h1) ∧ (r ∈ h → h[r] = h1[r]) ⊦ (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r])

Rule argument

Additional information

Used terms: r

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  r ∈ h ↔ r ∈ h1, modify(rs)(h0, h), r ∈ rs, r ∈ h1 → h[r] = h1[r] ⊦ (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r])

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 27:

  ⊦ 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 28:

  r ∈ h ↔ r ∈ h1, r ∈ rs, r ∈ h1 → h[r] = h1[r], (∃ 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) ⊦ (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r])

Rule argument

Additional information

Used terms: h, h0, rs

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

Lemma modify

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  r ∈ h ↔ r ∈ h1, r ∈ rs, r ∈ h1 → h[r] = h1[r], ¬ r0 ∈ rs ∧ r0 ≠ null ∧ ¬ r0 ∈ h0 ∧ h = h0 ++ r0 ∨ ¬ r1 ∈ rs ∧ r1 ∈ h0 ∧ h = h0[r1, o] ∨ ¬ r2 ∈ rs ∧ r2 ∈ h0 ∧ h = h0 -- r2 ⊦ (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r])

Rule argument

Additional information

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

User applied rule case distinction

And obtained the following new goals

• Proof step 30:

  r ∈ h ↔ r ∈ h1, h = h0 ++ r0, r0 ≠ null, r ∈ rs, ¬ r0 ∈ h0, ¬ r0 ∈ rs, r ∈ h1 → h[r] = h1[r] ⊦ (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r])

• Proof step 33:

  r ∈ h ↔ r ∈ h1, h = h0 -- r2, r ∈ rs, r2 ∈ h0, ¬ r2 ∈ rs, r ∈ h1 → h[r] = h1[r] ⊦ (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r])

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  (h0 ++ r0)[r] = h1[r], h0[r] ≠ h1[r], r0 ≠ null, r ∈ rs, r ∈ h0, r ∈ h1, ¬ r0 ∈ h0, ¬ r0 ∈ rs ⊦

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 32:

  r ∈ h, r0 ≠ null, ¬ r0 ∈ h ⊦ r ≠ r0 → (h ++ r0)[r] = h[r]

Rule argument

Additional information

Used terms: r, r0, h0

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  (h0 -- r2)[r] = h1[r], h0[r] ≠ h1[r], r2 ∈ h0, r ∈ rs, r ∈ h0, r ∈ h1, ¬ r2 ∈ rs ⊦

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 35:

  r ∈ h ⊦ r ≠ r0 → (h -- r0)[r] = h[r]

Rule argument

Additional information

Used terms: r, r2, h0

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

A spec-lemma

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

User applied rule induction

And obtained the following new goals

• Proof step 37:

  ((h0 ≡ h1))(rs), ¬ modify*(rs)(h0, h1), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Used simplifier rules: <; (wellfounded) Used terms: #(h0 \ rs) + #(h1 \ rs)

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

User applied rule cut formula

And obtained the following new goals

• Proof step 38:

  h0 \ rs = ∅, ((h0 ≡ h1))(rs), ¬ modify*(rs)(h0, h1), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

• Proof step 167:

  h0 \ rs ≠ ∅, ((h0 ≡ h1))(rs), ¬ modify*(rs)(h0, h1), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Used formulas: h0 \ rs = ∅

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

User applied rule cut formula

And obtained the following new goals

• Proof step 39:

  h0 \ rs = ∅, h1 \ rs = ∅, ((h0 ≡ h1))(rs), ¬ modify*(rs)(h0, h1), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

• Proof step 62:

  h0 \ rs = ∅, h1 \ rs ≠ ∅, ((h0 ≡ h1))(rs), ¬ modify*(rs)(h0, h1), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Used formulas: h1 \ rs = ∅

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 40:

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

• Proof step 41:

  h1 \ rs = ∅, h0 \ rs = ∅, ¬ modify*(rs)(h0, h1), ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Used terms: h0, h1, rs

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

Lemma agree

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 42:

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

• Proof step 43:

  h0 \ rs = ∅, h1 \ rs = ∅, ¬ modify(rs) ^*(h0, h1), ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Used terms: rs, h0, h1

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

Lemma modify+

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 44:

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

• Proof step 45:

  h1 \ rs = ∅, h0 \ rs = ∅, ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]), ∀ n. ¬ rtc(n, modify(rs))(h0, h1), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Used terms: modify(rs), h0, h1

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

A spec-lemma

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

User applied rule all left

And obtained the following new goals

• Proof step 46:

  h0 \ rs = ∅, h1 \ rs = ∅, ¬ rtc(0, modify(rs))(h0, h1), ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Used terms: 0

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 47:

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

• Proof step 48:

  h1 \ rs = ∅, h0 \ rs = ∅, h0 ≠ h1, ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Used terms: modify(rs), h0, h1

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 49:

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

• Proof step 50:

  h0 \ rs = ∅, h1 \ rs = ∅, ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]), ∃ r. ¬((r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r])), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Used terms: h0, h1

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 51:

  h1 \ rs = ∅, h0 \ rs = ∅, ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < # ∅ + # ∅ → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦ (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r])

Rule argument

Additional information

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

User applied rule all left

And obtained the following new goals

• Proof step 52:

  h0 \ rs = ∅, h1 \ rs = ∅, r ∈ rs → (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]), ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < # ∅ + # ∅ → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦ (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r])

Rule argument

Additional information

Used terms: r

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 53:

  h1 \ rs = ∅, h0 \ rs = ∅, ¬ r ∈ rs, ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < # ∅ + # ∅ → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦ (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r])

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 54:

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

• Proof step 55:

  h0 \ rs = ∅, ¬ r ∈ rs, ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]), ∀ r. (r ∈ h1 \ rs ↔ r ∈ ∅) ∧ (r ∈ h1 \ rs → (h1 \ rs)[r] = ∅[r]), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < # ∅ + # ∅ → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦ (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r])

Rule argument

Additional information

Used terms: h1 \ rs, ∅

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 56:

  h0 \ rs = ∅, ¬ r ∈ rs, ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]), ∀ r0. ¬ r0 ∈ h1 \ rs, ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < # ∅ + # ∅ → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦ (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r])

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ r ∈ ∅; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 57:

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

• Proof step 58:

  ¬ r ∈ rs, ∀ r0. ¬ r0 ∈ h1 \ rs, ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]), ∀ r. (r ∈ h0 \ rs ↔ r ∈ ∅) ∧ (r ∈ h0 \ rs → (h0 \ rs)[r] = ∅[r]), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < # ∅ + # ∅ → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦ (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r])

Rule argument

Additional information

Used terms: h0 \ rs, ∅

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 59:

  ¬ r ∈ rs, ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]), ∀ r0. ¬ r0 ∈ h1 \ rs, ∀ r0. ¬ r0 ∈ h0 \ rs, ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < # ∅ + # ∅ → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦ (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r])

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ r ∈ ∅; (s)

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

User applied rule all left

And obtained the following new goals

• Proof step 60:

  ¬ r ∈ h0 \ rs, ¬ r ∈ rs, ∀ r0. ¬ r0 ∈ h1 \ rs, ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < # ∅ + # ∅ → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦ (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r])

Rule argument

Additional information

Used terms: r

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 61:

  r ∈ h1, ¬ r ∈ rs, ¬ r ∈ h0, ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]), ∀ r0. ¬ r0 ∈ h1 \ rs, ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < # ∅ + # ∅ → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ r ∈ h \ rs ↔ r ∈ h ∧ ¬ r ∈ rs; (ss)

Proof step 61 from proof modify-agree (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 \ rs ↔ r ∈ h ∧ ¬ r ∈ rs; (ss) Used terms: r

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

User applied rule weakening

And obtained the following new goals

• Proof step 63:

  h1 \ rs ≠ ∅, ((h0 ≡ h1))(rs), ¬ modify*(rs)(h0, h1), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 64:

  h1 \ rs ≠ ∅, ((h0 ≡ h1))(rs), ¬ modify*(rs)(h0, h1), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 65:

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

• Proof step 66:

  ((h0 ≡ h1))(rs), ¬ modify*(rs)(h0, h1), ∃ r. ¬((r ∈ h1 \ rs ↔ r ∈ ∅) ∧ (r ∈ h1 \ rs → (h1 \ rs)[r] = ∅[r])), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Used terms: h1 \ rs, ∅

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 67:

  r ∈ h1 \ rs, ((h0 ≡ h1))(rs), ¬ modify*(rs)(h0, h1), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ r ∈ ∅; (s)

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

User applied rule apply induction

And obtained the following new goals

• Proof step 68:

  r ∈ h1 \ rs, ((h0 ≡ h1))(rs), ¬ #(h0 \ rs) + #((h1 -- r) \ rs) < #(h0 \ rs) + #(h1 \ rs), ¬ modify*(rs)(h0, h1), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

• Proof step 131:

  r ∈ h1 \ rs, ((h0 ≡ h1))(rs), ¬ modify*(rs)(h0, h1), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦ ((h0 ≡ (h1 -- r)))(rs) ∧ ¬ modify*(rs)(h0, h1 -- r)

Rule argument

Additional information

Used terms: h0, rs, h1 -- r

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 69:

  ⊦ (h -- r) \ rs = (h \ rs) -- r

• Proof step 70:

  r ∈ h1 \ rs, ((h0 ≡ h1))(rs), ¬ #(h0 \ rs) + #((h1 \ rs) -- r) < #(h0 \ rs) + #(h1 \ rs), ¬ modify*(rs)(h0, h1), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Used terms: h1, r, rs

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 71:

  ⊦ r ∈ h → #(h -- r) = # h - 1

• Proof step 72:

  r ∈ h1 \ rs, ((h0 ≡ h1))(rs), ¬ #(h0 \ rs) + (#(h1 \ rs) - 1) < #(h0 \ rs) + #(h1 \ rs), ¬ modify*(rs)(h0, h1), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Used terms: h1 \ rs, r

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

A spec-lemma

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

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 73:

  #(h1 \ rs) = 0, r ∈ h1 \ rs, ((h0 ≡ h1))(rs), ¬ #(h0 \ rs) + (#(h1 \ rs) - 1) < #(h0 \ rs) + #(h1 \ rs), ¬ modify*(rs)(h0, h1), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m = n + 1 → ¬ m ≤ n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: #(h1 \ rs), m

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 74:

  #(h1 \ rs) = 0, r ∈ h1 \ rs, ((h0 ≡ h1))(rs), ¬ modify*(rs)(h0, h1), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + 0 → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 0 ≤ m; (s) leprf: ⊦ m ≤ m - 1 → m = 0; (forward) from specification nat c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m + n < m + n0 ↔ n < n0; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 75:

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

• Proof step 76:

  #(h1 \ rs) = 0, r ∈ h1 \ rs, ¬ modify*(rs)(h0, h1), ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + 0 → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Used terms: h0, h1, rs

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

Lemma agree

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 77:

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

• Proof step 78:

  #(h1 \ rs) = 0, r ∈ h1 \ rs, ¬ modify(rs) ^*(h0, h1), ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + 0 → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Used terms: rs, h0, h1

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

Lemma modify+

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 79:

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

• Proof step 80:

  #(h1 \ rs) = 0, r ∈ h1 \ rs, ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]), ∀ n. ¬ rtc(n, modify(rs))(h0, h1), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + 0 → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Used terms: modify(rs), h0, h1

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

A spec-lemma

Proof step 80 from proof modify-agree (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 81:

  #(h1 \ rs) = 0, r ∈ h1 \ rs, ¬ rtc(0, modify(rs))(h0, h1), ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + 0 → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Used terms: 0

Proof step 81 from proof modify-agree (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 82:

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

• Proof step 83:

  #(h1 \ rs) = 0, h0 ≠ h1, r ∈ h1 \ rs, ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + 0 → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Used terms: modify(rs), h0, h1

Proof step 82 from proof modify-agree (previous step) (back to tree)

A spec-lemma

Proof step 83 from proof modify-agree (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 84:

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

• Proof step 85:

  #(h1 \ rs) = 0, r ∈ h1 \ rs, ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]), ∃ r. ¬((r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r])), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + 0 → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Used terms: h0, h1

Proof step 84 from proof modify-agree (previous step) (back to tree)

A spec-lemma

Proof step 85 from proof modify-agree (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 86:

  #(h1 \ rs) = 0, r ∈ h1 \ rs, ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + 0 → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦ (r0 ∈ h0 ↔ r0 ∈ h1) ∧ (r0 ∈ h0 → h0[r0] = h1[r0])

Rule argument

Additional information

Proof step 86 from proof modify-agree (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 87:

  ⊦ r ∈ h \ rs ↔ r ∈ h ∧ ¬ r ∈ rs

• Proof step 88:

  #(h1 \ rs) = 0, r ∈ h1, ¬ r ∈ rs, ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + 0 → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦ (r0 ∈ h0 ↔ r0 ∈ h1) ∧ (r0 ∈ h0 → h0[r0] = h1[r0])

Rule argument

Additional information

Used terms: r, h1, rs

Proof step 87 from proof modify-agree (previous step) (back to tree)

A spec-lemma

Proof step 88 from proof modify-agree (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 89:

  #(h1 \ rs) = 0, r0 ∈ h0 ↔ r0 ∈ h1, r ∈ h1, ¬ r ∈ rs, ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + 0 → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦ (r0 ∈ h0 ↔ r0 ∈ h1) ∧ (r0 ∈ h0 → h0[r0] = h1[r0])

• Proof step 110:

  #(h1 \ rs) = 0, ¬(r0 ∈ h0 ↔ r0 ∈ h1), r ∈ h1, ¬ r ∈ rs, ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + 0 → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦ (r0 ∈ h0 ↔ r0 ∈ h1) ∧ (r0 ∈ h0 → h0[r0] = h1[r0])

Rule argument

Additional information

Used formulas: r0 ∈ h0 ↔ r0 ∈ h1

Proof step 89 from proof modify-agree (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 90:

  #(h1 \ rs) = 0, h0[r0] ≠ h1[r0], r ∈ h1, r0 ∈ h0, r0 ∈ h1, ¬ r ∈ rs, ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + 0 → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Proof step 90 from proof modify-agree (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 91:

  #(h1 \ rs) = 0, h0[r0] ≠ h1[r0], r0 ∈ h1, r0 ∈ h0, r ∈ h1, ¬ r ∈ rs, r0 ∈ rs → (r0 ∈ h0 ↔ r0 ∈ h1) ∧ (r0 ∈ h0 → h0[r0] = h1[r0]), ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + 0 → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Used terms: r0

Proof step 91 from proof modify-agree (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 92:

  #(h1 \ rs) = 0, h0[r0] ≠ h1[r0], r ∈ h1, r0 ∈ h0, r0 ∈ h1, ¬ r ∈ rs, ¬ r0 ∈ rs, ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + 0 → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Proof step 92 from proof modify-agree (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 93:

  ⊦ r ≠ null → (r ∈ h ↔ (∃ h0, o. h = (h0 ++ r)[r, o] ∧ ¬ r ∈ h0))

• Proof step 94:

  #(h1 \ rs) = 0, h0[r0] ≠ h1[r0], r0 ≠ null, r0 ∈ h0, r ∈ h1, ¬ r ∈ rs, ¬ r0 ∈ rs, ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]), ∃ h0, o. h1 = (h0 ++ r0)[r0, o] ∧ ¬ r0 ∈ h0, ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + 0 → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ null ∈ h; (s) Used terms: r0, h1

Proof step 93 from proof modify-agree (previous step) (back to tree)

A spec-lemma

Proof step 94 from proof modify-agree (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 95:

  #((h ++ r0)[r0, o] \ rs) = 0, h0[r0] ≠ o, r0 ∈ h0, ¬ r ∈ rs, ¬ r0 ∈ rs, ¬ r0 ∈ h, ∀ r1. r1 ∈ rs → (r1 ∈ h0 ↔ r1 ∈ h) ∧ (r1 ∈ h0 → h0[r1] = (h ++ r0)[r1]), r = r0 ∨ r ∈ h, ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + 0 → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

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

Proof step 95 from proof modify-agree (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 96:

  ¬ r ∈ h, r ≠ null ⊦ ¬ r ∈ rs → (h ++ r)[r, o] \ rs = ((h \ rs) ++ r)[r, o]

• Proof step 97:

  # ((h \ rs) ++ r0)[r0, o] = 0, h0[r0] ≠ o, r0 ≠ null, r0 ∈ h0, ¬ r ∈ rs, ¬ r0 ∈ rs, ¬ r0 ∈ h, ∀ r1. r1 ∈ rs → (r1 ∈ h0 ↔ r1 ∈ h) ∧ (r1 ∈ h0 → h0[r1] = (h ++ r0)[r1]), r = r0 ∨ r ∈ h, ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + 0 → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ r ∈ h → r ≠ null; (s) Used terms: h, r0, o, rs

Proof step 96 from proof modify-agree (previous step) (back to tree)

A spec-lemma

Proof step 97 from proof modify-agree (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 98:

  # ((h \ rs) ++ r0)[r0, o] = 0, h0[r0] ≠ o, r0 ∈ h0, ¬ r ∈ rs, ¬ r0 ∈ rs, ¬ r0 ∈ h, ∀ r1. r1 ∈ rs → (r1 ∈ h0 ↔ r1 ∈ h) ∧ (r1 ∈ h0 → h0[r1] = (h ++ r0)[r1]), r = r0 ∨ r ∈ h, ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + 0 → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

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

Proof step 98 from proof modify-agree (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 99:

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

• Proof step 100:

  # ((h \ rs) ++ r0)[r0, o] = 0, h0[r0] ≠ o, r0 ∈ h0, ¬ r0 ∈ (h \ rs) ++ r0, ¬ r ∈ rs, ¬ r0 ∈ rs, ¬ r0 ∈ h, ∀ r1. r1 ∈ rs → (r1 ∈ h0 ↔ r1 ∈ h) ∧ (r1 ∈ h0 → h0[r1] = (h ++ r0)[r1]), r = r0 ∨ r ∈ h, ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + 0 → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

• Proof step 105:

  #((h \ rs) ++ r0) = 0, h0[r0] ≠ o, r0 ∈ h0, r0 ∈ (h \ rs) ++ r0, ¬ r ∈ rs, ¬ r0 ∈ rs, ¬ r0 ∈ h, ∀ r1. r1 ∈ rs → (r1 ∈ h0 ↔ r1 ∈ h) ∧ (r1 ∈ h0 → h0[r1] = (h ++ r0)[r1]), r = r0 ∨ r ∈ h, ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + 0 → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Used terms: (h \ rs) ++ r0, r0, o

Proof step 99 from proof modify-agree (previous step) (back to tree)

A spec-lemma

Proof step 100 from proof modify-agree (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 101:

  r0 ≠ null, ¬ r0 ∈ h ⊦ r ∈ h ++ r0 ↔ r = r0 ∨ r ∈ h

• Proof step 102:

  # ((h \ rs) ++ r0)[r0, o] = 0, h0[r0] ≠ o, r0 ∈ h0, ¬ r0 ∈ (h \ rs) ++ r0, ¬ r ∈ rs, ¬ r0 ∈ rs, ¬ r0 ∈ h, ∀ r1. r1 ∈ rs → (r1 ∈ h0 ↔ r1 ∈ h) ∧ (r1 ∈ h0 → h0[r1] = (h ++ r0)[r1]), r = r0 ∨ r ∈ h, ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + 0 → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦ r0 ≠ null ∧ ¬ r0 ∈ h \ rs

Rule argument

Additional information

Used terms: r0, h \ rs, r0

Proof step 101 from proof modify-agree (previous step) (back to tree)

A spec-lemma

Proof step 102 from proof modify-agree (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 103:

  # ((h \ rs) ++ r0)[r0, o] = 0, h0[r0] ≠ o, r0 ∈ h0, r0 ∈ h \ rs, ¬ r0 ∈ (h \ rs) ++ r0, ¬ r ∈ rs, ¬ r0 ∈ rs, ¬ r0 ∈ h, ∀ r1. r1 ∈ rs → (r1 ∈ h0 ↔ r1 ∈ h) ∧ (r1 ∈ h0 → h0[r1] = (h ++ r0)[r1]), r = r0 ∨ r ∈ h, ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + 0 → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

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

Proof step 103 from proof modify-agree (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 104:

  ⊦ r ∈ h \ rs ↔ r ∈ h ∧ ¬ r ∈ rs

Rule argument

Additional information

Used terms: r0, h, rs

Proof step 104 from proof modify-agree (previous step) (back to tree)

A spec-lemma

Proof step 105 from proof modify-agree (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 106:

  r0 ≠ null, ¬ r0 ∈ h ⊦ r ∈ h ++ r0 ↔ r = r0 ∨ r ∈ h

• Proof step 107:

  #((h \ rs) ++ r0) = 0, h0[r0] ≠ o, r0 ∈ (h \ rs) ++ r0, r0 ∈ h0, ¬ r ∈ rs, ¬ r0 ∈ rs, ¬ r0 ∈ h, ∀ r1. r1 ∈ rs → (r1 ∈ h0 ↔ r1 ∈ h) ∧ (r1 ∈ h0 → h0[r1] = (h ++ r0)[r1]), r = r0 ∨ r ∈ h, ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + 0 → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦ r0 ≠ null ∧ ¬ r0 ∈ h \ rs

Rule argument

Additional information

Used simplifier rules: ¬ r ∈ h, r ≠ null ⊦ #(h ++ r) = # h + 1; (s) ⊦ 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: r0, h \ rs, r0

Proof step 106 from proof modify-agree (previous step) (back to tree)

A spec-lemma

Proof step 107 from proof modify-agree (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 108:

  #((h \ rs) ++ r0) = 0, h0[r0] ≠ o, r0 ∈ h0, r0 ∈ (h \ rs) ++ r0, r0 ∈ h \ rs, ¬ r ∈ rs, ¬ r0 ∈ rs, ¬ r0 ∈ h, ∀ r1. r1 ∈ rs → (r1 ∈ h0 ↔ r1 ∈ h) ∧ (r1 ∈ h0 → h0[r1] = (h ++ r0)[r1]), r = r0 ∨ r ∈ h, ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + 0 → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

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

Proof step 108 from proof modify-agree (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 109:

  ⊦ r ∈ h \ rs ↔ r ∈ h ∧ ¬ r ∈ rs

Rule argument

Additional information

Used terms: r0, h, rs

Proof step 109 from proof modify-agree (previous step) (back to tree)

A spec-lemma

Proof step 110 from proof modify-agree (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 111:

  #(h1 \ rs) = 0, ¬(r0 ∈ h0 ↔ r0 ∈ h1), r ∈ h1, ¬ r ∈ rs, ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + 0 → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Proof step 111 from proof modify-agree (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 112:

  #(h1 \ rs) = 0, ¬(r0 ∈ h0 ↔ r0 ∈ h1), r ∈ h1, ¬ r ∈ rs, r0 ∈ rs → (r0 ∈ h0 ↔ r0 ∈ h1) ∧ (r0 ∈ h0 → h0[r0] = h1[r0]), ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + 0 → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Used terms: r0

Proof step 112 from proof modify-agree (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 113:

  #(h1 \ rs) = 0, ¬(r0 ∈ h0 ↔ r0 ∈ h1), r ∈ h1, ¬ r ∈ rs, ¬ r0 ∈ rs, ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + 0 → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Proof step 113 from proof modify-agree (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 114:

  ⊦ r ≠ null → (r ∈ h ↔ (∃ h0, o. h = (h0 ++ r)[r, o] ∧ ¬ r ∈ h0))

• Proof step 115:

  #(h1 \ rs) = 0, ¬(r0 ∈ h0 ↔ r0 ∈ h1), r ≠ null, ¬ r ∈ rs, ¬ r0 ∈ rs, ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]), ∃ h0, o. h1 = (h0 ++ r)[r, o] ∧ ¬ r ∈ h0, ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + 0 → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ null ∈ h; (s) Used terms: r, h1

Proof step 114 from proof modify-agree (previous step) (back to tree)

A spec-lemma

Proof step 115 from proof modify-agree (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 116:

  #((h ++ r)[r, o] \ rs) = 0, ¬(r0 ∈ h0 ↔ r0 = r ∨ r0 ∈ h), r ≠ null, ¬ r ∈ rs, ¬ r0 ∈ rs, ¬ r ∈ h, ∀ r1. r1 ∈ rs → (r1 ∈ h0 ↔ r1 ∈ h) ∧ (r1 ∈ h0 → h0[r1] = (h ++ r)[r1]), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + 0 → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

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

Proof step 116 from proof modify-agree (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 117:

  ¬ r ∈ h, r ≠ null ⊦ ¬ r ∈ rs → (h ++ r)[r, o] \ rs = ((h \ rs) ++ r)[r, o]

• Proof step 118:

  # ((h \ rs) ++ r)[r, o] = 0, ¬(r0 ∈ h0 ↔ r0 = r ∨ r0 ∈ h), r ≠ null, ¬ r ∈ rs, ¬ r0 ∈ rs, ¬ r ∈ h, ∀ r1. r1 ∈ rs → (r1 ∈ h0 ↔ r1 ∈ h) ∧ (r1 ∈ h0 → h0[r1] = (h ++ r)[r1]), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + 0 → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Used terms: h, r, o, rs

Proof step 117 from proof modify-agree (previous step) (back to tree)

A spec-lemma

Proof step 118 from proof modify-agree (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 119:

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

• Proof step 120:

  # ((h \ rs) ++ r)[r, o] = 0, ¬(r0 ∈ h0 ↔ r0 = r ∨ r0 ∈ h), r ≠ null, ¬ r ∈ (h \ rs) ++ r, ¬ r ∈ rs, ¬ r0 ∈ rs, ¬ r ∈ h, ∀ r1. r1 ∈ rs → (r1 ∈ h0 ↔ r1 ∈ h) ∧ (r1 ∈ h0 → h0[r1] = (h ++ r)[r1]), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + 0 → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

• Proof step 125:

  #((h \ rs) ++ r) = 0, ¬(r0 ∈ h0 ↔ r0 = r ∨ r0 ∈ h), r ≠ null, r ∈ (h \ rs) ++ r, ¬ r ∈ rs, ¬ r0 ∈ rs, ¬ r ∈ h, ∀ r1. r1 ∈ rs → (r1 ∈ h0 ↔ r1 ∈ h) ∧ (r1 ∈ h0 → h0[r1] = (h ++ r)[r1]), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + 0 → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Used terms: (h \ rs) ++ r, r, o

Proof step 119 from proof modify-agree (previous step) (back to tree)

A spec-lemma

Proof step 120 from proof modify-agree (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 121:

  r0 ≠ null, ¬ r0 ∈ h ⊦ r ∈ h ++ r0 ↔ r = r0 ∨ r ∈ h

• Proof step 122:

  # ((h \ rs) ++ r)[r, o] = 0, ¬(r0 ∈ h0 ↔ r0 = r ∨ r0 ∈ h), r ≠ null, ¬ r ∈ (h \ rs) ++ r, ¬ r ∈ rs, ¬ r0 ∈ rs, ¬ r ∈ h, ∀ r1. r1 ∈ rs → (r1 ∈ h0 ↔ r1 ∈ h) ∧ (r1 ∈ h0 → h0[r1] = (h ++ r)[r1]), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + 0 → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦ r ≠ null ∧ ¬ r ∈ h \ rs

Rule argument

Additional information

Used terms: r, h \ rs, r

Proof step 121 from proof modify-agree (previous step) (back to tree)

A spec-lemma

Proof step 122 from proof modify-agree (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 123:

  # ((h \ rs) ++ r)[r, o] = 0, ¬(r0 ∈ h0 ↔ r0 = r ∨ r0 ∈ h), r ∈ h \ rs, ¬ r ∈ (h \ rs) ++ r, ¬ r ∈ rs, ¬ r0 ∈ rs, ¬ r ∈ h, ∀ r1. r1 ∈ rs → (r1 ∈ h0 ↔ r1 ∈ h) ∧ (r1 ∈ h0 → h0[r1] = (h ++ r)[r1]), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + 0 → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

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

Proof step 123 from proof modify-agree (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 124:

  ⊦ r ∈ h \ rs ↔ r ∈ h ∧ ¬ r ∈ rs

Rule argument

Additional information

Used terms: r, h, rs

Proof step 124 from proof modify-agree (previous step) (back to tree)

A spec-lemma

Proof step 125 from proof modify-agree (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 126:

  #((h \ rs) ++ r) = 0, ¬(r0 ∈ h0 ↔ r0 = r ∨ r0 ∈ h), r ∈ (h \ rs) ++ r, ¬ r ∈ rs, ¬ r0 ∈ rs, ¬ r ∈ h, ∀ r1. r1 ∈ rs → (r1 ∈ h0 ↔ r1 ∈ h) ∧ (r1 ∈ h0 → h0[r1] = (h ++ r)[r1]), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + 0 → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

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

Proof step 126 from proof modify-agree (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 127:

  r0 ≠ null, ¬ r0 ∈ h ⊦ r ∈ h ++ r0 ↔ r = r0 ∨ r ∈ h

• Proof step 128:

  #((h \ rs) ++ r) = 0, ¬(r0 ∈ h0 ↔ r0 = r ∨ r0 ∈ h), r ∈ (h \ rs) ++ r, ¬ r ∈ rs, ¬ r0 ∈ rs, ¬ r ∈ h, ∀ r1. r1 ∈ rs → (r1 ∈ h0 ↔ r1 ∈ h) ∧ (r1 ∈ h0 → h0[r1] = (h ++ r)[r1]), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + 0 → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦ r ≠ null ∧ ¬ r ∈ h \ rs

Rule argument

Additional information

Used simplifier rules: ¬ r ∈ h, r ≠ null ⊦ #(h ++ r) = # h + 1; (s) ⊦ 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: r, h \ rs, r

Proof step 127 from proof modify-agree (previous step) (back to tree)

A spec-lemma

Proof step 128 from proof modify-agree (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 129:

  #((h \ rs) ++ r) = 0, ¬(r0 ∈ h0 ↔ r0 = r ∨ r0 ∈ h), r ∈ (h \ rs) ++ r, r ∈ h \ rs, ¬ r ∈ rs, ¬ r0 ∈ rs, ¬ r ∈ h, ∀ r1. r1 ∈ rs → (r1 ∈ h0 ↔ r1 ∈ h) ∧ (r1 ∈ h0 → h0[r1] = (h ++ r)[r1]), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + 0 → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

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

Proof step 129 from proof modify-agree (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 130:

  ⊦ r ∈ h \ rs ↔ r ∈ h ∧ ¬ r ∈ rs

Rule argument

Additional information

Used terms: r, h, rs

Proof step 130 from proof modify-agree (previous step) (back to tree)

A spec-lemma

Proof step 131 from proof modify-agree (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 132:

  ⊦ r ∈ h \ rs ↔ r ∈ h ∧ ¬ r ∈ rs

• Proof step 133:

  r ∈ h1, ((h0 ≡ h1))(rs), ¬ modify*(rs)(h0, h1), ¬ r ∈ rs, ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦ ((h0 ≡ (h1 -- r)))(rs) ∧ ¬ modify*(rs)(h0, h1 -- r)

Rule argument

Additional information

Used terms: r, h1, rs

Proof step 132 from proof modify-agree (previous step) (back to tree)

A spec-lemma

Proof step 133 from proof modify-agree (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 134:

  modify*(rs)(h0, h1 -- r), r ∈ h1, ((h0 ≡ h1))(rs), ¬ modify*(rs)(h0, h1), ¬ r ∈ rs, ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Used simplifier rules: agree-rm-01: ⊦ ¬ r ∈ rs → (((h ≡ (h0 -- r)))(rs) ↔ ((h ≡ h0))(rs));

Proof step 134 from proof modify-agree (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 135:

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

• Proof step 136:

  modify(rs) ^*(h0, h1 -- r), r ∈ h1, ((h0 ≡ h1))(rs), ¬ modify*(rs)(h0, h1), ¬ r ∈ rs, ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Used terms: rs, h0, h1 -- r

Proof step 135 from proof modify-agree (previous step) (back to tree)

Lemma modify+

Proof step 136 from proof modify-agree (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 137:

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

• Proof step 138:

  modify(rs) ^*(h0, h1 -- r), r ∈ h1, ((h0 ≡ h1))(rs), ¬ modify(rs) ^*(h0, h1), ¬ r ∈ rs, ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Used terms: rs, h0, h1

Proof step 137 from proof modify-agree (previous step) (back to tree)

Lemma modify+

Proof step 138 from proof modify-agree (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 139:

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

• Proof step 140:

  r ∈ h1, ((h0 ≡ h1))(rs), ¬ modify(rs) ^*(h0, h1), ¬ r ∈ rs, ∃ n. rtc(n, modify(rs))(h0, h1 -- r), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Used terms: modify(rs), h0, h1 -- r

Proof step 139 from proof modify-agree (previous step) (back to tree)

A spec-lemma

Proof step 140 from proof modify-agree (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 141:

  rtc(n, modify(rs))(h0, h1 -- r), r ∈ h1, ((h0 ≡ h1))(rs), ¬ modify(rs) ^*(h0, h1), ¬ r ∈ rs, ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Proof step 141 from proof modify-agree (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 142:

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

• Proof step 143:

  rtc(n, modify(rs))(h0, h1 -- r), r ∈ h1, ((h0 ≡ h1))(rs), ¬ r ∈ rs, ∀ n. ¬ rtc(n, modify(rs))(h0, h1), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Used terms: modify(rs), h0, h1

Proof step 142 from proof modify-agree (previous step) (back to tree)

A spec-lemma

Proof step 143 from proof modify-agree (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 144:

  rtc(n, modify(rs))(h0, h1 -- r), r ∈ h1, ((h0 ≡ h1))(rs), ¬ rtc(n + 2, modify(rs))(h0, h1), ¬ r ∈ rs, ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Used terms: n + 2

Proof step 144 from proof modify-agree (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 145:

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

• Proof step 146:

  n + 2 ≠ 0, rtc(n, modify(rs))(h0, h1 -- r), r ∈ h1, ((h0 ≡ h1))(rs), ¬ r ∈ rs, ∀ c. ¬(rtc(n + 2 - 1, modify(rs))(h0, c) ∧ modify(rs)(c, h1)), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

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), h0, h1

Proof step 145 from proof modify-agree (previous step) (back to tree)

A spec-lemma

Proof step 146 from proof modify-agree (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 147:

  rtc(n, modify(rs))(h0, h1 -- r), r ∈ h1, ((h0 ≡ h1))(rs), ¬ r ∈ rs, ∀ c. ¬ rtc(1 + n, modify(rs))(h0, c) ∨ ¬ modify(rs)(c, h1), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

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 147 from proof modify-agree (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 148:

  rtc(n, modify(rs))(h0, h1 -- r), r ∈ h1, ((h0 ≡ h1))(rs), ¬ r ∈ rs, ¬ rtc(1 + n, modify(rs))(h0, (h1 -- r) ++ r) ∨ ¬ modify(rs)((h1 -- r) ++ r, h1), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Used terms: (h1 -- r) ++ r

Proof step 148 from proof modify-agree (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 149:

  rtc(n, modify(rs))(h0, h1 -- r), r ∈ h1, ((h0 ≡ h1))(rs), ¬ rtc(1 + n, modify(rs))(h0, (h1 -- r) ++ r), ¬ r ∈ rs, ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

• Proof step 158:

  rtc(n, modify(rs))(h0, h1 -- r), r ∈ h1, ((h0 ≡ h1))(rs), ¬ modify(rs)((h1 -- r) ++ r, h1), ¬ r ∈ rs, ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Proof step 149 from proof modify-agree (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 150:

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

• Proof step 151:

  1 + n ≠ 0, rtc(n, modify(rs))(h0, h1 -- r), r ∈ h1, ((h0 ≡ h1))(rs), ¬ r ∈ rs, ∀ c. ¬(rtc(1 + n - 1, modify(rs))(h0, c) ∧ modify(rs)(c, (h1 -- r) ++ r)), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

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), h0, (h1 -- r) ++ r

Proof step 150 from proof modify-agree (previous step) (back to tree)

A spec-lemma

Proof step 151 from proof modify-agree (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 152:

  rtc(n, modify(rs))(h0, h1 -- r), r ∈ h1, ((h0 ≡ h1))(rs), ¬ r ∈ rs, ∀ c. ¬ rtc(n, modify(rs))(h0, c) ∨ ¬ modify(rs)(c, (h1 -- r) ++ r), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

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 152 from proof modify-agree (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 153:

  rtc(n, modify(rs))(h0, h1 -- r), r ∈ h1, ((h0 ≡ h1))(rs), ¬ r ∈ rs, ¬ rtc(n, modify(rs))(h0, h1 -- r) ∨ ¬ modify(rs)(h1 -- r, (h1 -- r) ++ r), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Used terms: h1 -- r

Proof step 153 from proof modify-agree (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 154:

  rtc(n, modify(rs))(h0, h1 -- r), r ∈ h1, ((h0 ≡ h1))(rs), ¬ modify(rs)(h1 -- r, (h1 -- r) ++ r), ¬ r ∈ rs, ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Proof step 154 from proof modify-agree (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 155:

  ⊦ 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 156:

  rtc(n, modify(rs))(h0, h1 -- r), r ∈ h1, ((h0 ≡ h1))(rs), ¬ r ∈ rs, ∀ r0. ¬(¬ r0 ∈ rs ∧ r0 ≠ null ∧ ¬ r0 ∈ h1 -- r ∧ (h1 -- r) ++ r = (h1 -- r) ++ r0), ∀ r0, o. ¬(¬ r0 ∈ rs ∧ r0 ∈ h1 -- r ∧ (h1 -- r) ++ r = (h1 -- r)[r0, o]), ∀ r0. ¬(¬ r0 ∈ rs ∧ r0 ∈ h1 -- r ∧ (h1 -- r) ++ r = h1 -- r -- r0), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Used terms: rs, h1 -- r, (h1 -- r) ++ r

Proof step 155 from proof modify-agree (previous step) (back to tree)

Lemma modify

Proof step 156 from proof modify-agree (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 157:

  rtc(n, modify(rs))(h0, h1 -- r), r ∈ h1, ((h0 ≡ h1))(rs), ¬ r ∈ rs, ∀ r0. r0 ∈ rs ∨ r0 = null ∨ r0 ≠ r ∧ r0 ∈ h1 ∨ (h1 -- r) ++ r ≠ (h1 -- r) ++ r0, ∀ r0. r0 ∈ rs ∨ r0 = r ∨ ¬ r0 ∈ h1 ∨ (h1 -- r) ++ r ≠ h1 -- r -- r0, ∀ r0, o. r0 ∈ rs ∨ r0 = r ∨ ¬ r0 ∈ h1 ∨ (h1 -- r) ++ r ≠ (h1 -- r)[r0, o], ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

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

Proof step 157 from proof modify-agree (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: r

Proof step 158 from proof modify-agree (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 159:

  ⊦ 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 160:

  rtc(n, modify(rs))(h0, h1 -- r), r ∈ h1, ((h0 ≡ h1))(rs), ¬ r ∈ rs, ∀ r0. ¬(¬ r0 ∈ rs ∧ r0 ≠ null ∧ ¬ r0 ∈ (h1 -- r) ++ r ∧ h1 = (h1 -- r) ++ r ++ r0), ∀ r0, o. ¬(¬ r0 ∈ rs ∧ r0 ∈ (h1 -- r) ++ r ∧ h1 = ((h1 -- r) ++ r)[r0, o]), ∀ r0. ¬(¬ r0 ∈ rs ∧ r0 ∈ (h1 -- r) ++ r ∧ h1 = ((h1 -- r) ++ r) -- r0), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Used terms: rs, (h1 -- r) ++ r, h1

Proof step 159 from proof modify-agree (previous step) (back to tree)

Lemma modify

Proof step 160 from proof modify-agree (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 161:

  rtc(n, modify(rs))(h0, h1 -- r), r ∈ h1, ((h0 ≡ h1))(rs), ¬ r ∈ rs, ∀ r0. r0 ∈ rs ∨ ¬ r0 ∈ h1 ∨ h1 ≠ ((h1 -- r) ++ r) -- r0, ∀ r0, o. r0 ∈ rs ∨ ¬ r0 ∈ h1 ∨ h1 ≠ ((h1 -- r) ++ r)[r0, o], ∀ r0. r0 ∈ rs ∨ r0 = null ∨ r0 ∈ h1 ∨ h1 ≠ (h1 -- r) ++ r ++ r0, ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

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 161 from proof modify-agree (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 162:

  rtc(n, modify(rs))(h0, h1 -- r), r ∈ h1, ((h0 ≡ h1))(rs), ¬ r ∈ rs, ∀ r0. r0 ∈ rs ∨ r0 = null ∨ r0 ∈ h1 ∨ h1 ≠ (h1 -- r) ++ r ++ r0, ∀ r0. r0 ∈ rs ∨ ¬ r0 ∈ h1 ∨ h1 ≠ ((h1 -- r) ++ r) -- r0, r ∈ rs ∨ ¬ r ∈ h1 ∨ h1 ≠ ((h1 -- r) ++ r)[r, h1[r]], ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Used terms: r, h1[r]

Proof step 162 from proof modify-agree (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 163:

  h1 ≠ ((h1 -- r) ++ r)[r, h1[r]], rtc(n, modify(rs))(h0, h1 -- r), r ∈ h1, ((h0 ≡ h1))(rs), ¬ r ∈ rs, ∀ r0. r0 ∈ rs ∨ ¬ r0 ∈ h1 ∨ h1 ≠ ((h1 -- r) ++ r) -- r0, ∀ r0. r0 ∈ rs ∨ r0 = null ∨ r0 ∈ h1 ∨ h1 ≠ (h1 -- r) ++ r ++ r0, ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Proof step 163 from proof modify-agree (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 164:

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

• Proof step 165:

  rtc(n, modify(rs))(h0, h1 -- r), r ∈ h1, ((h0 ≡ h1))(rs), ¬ r ∈ rs, ∀ r0. r0 ∈ rs ∨ r0 = null ∨ r0 ∈ h1 ∨ h1 ≠ (h1 -- r) ++ r ++ r0, ∀ r0. r0 ∈ rs ∨ ¬ r0 ∈ h1 ∨ h1 ≠ ((h1 -- r) ++ r) -- r0, ∃ r0. ¬((r0 ∈ h1 ↔ r0 ∈ ((h1 -- r) ++ r)[r, h1[r]]) ∧ (r0 ∈ h1 → h1[r0] = ((h1 -- r) ++ r)[r, h1[r]][r0])), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Used terms: h1, ((h1 -- r) ++ r)[r, h1[r]]

Proof step 164 from proof modify-agree (previous step) (back to tree)

A spec-lemma

Proof step 165 from proof modify-agree (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 166:

  h1[r0] ≠ (r0 = r ⊃ h1[r];h1[r0]), rtc(n, modify(rs))(h0, h1 -- r), r ∈ h1, r0 ∈ h1, ((h0 ≡ h1))(rs), ¬ r ∈ rs, ∀ r0. r0 ∈ rs ∨ ¬ r0 ∈ h1 ∨ h1 ≠ ((h1 -- r) ++ r) -- r0, ∀ r0. r0 ∈ rs ∨ r0 = null ∨ r0 ∈ h1 ∨ h1 ≠ (h1 -- r) ++ r ++ r0, ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

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 166 from proof modify-agree (previous step) (back to tree)

User applied rule case distinction

And closed the goal!

Rule argument

Additional information

Proof step 167 from proof modify-agree (previous step) (back to tree)

User applied rule apply proof lemma

And obtained the following new goals

• Proof step 168:

  h1 \ rs ≠ ∅, ((h0 ≡ h1))(rs), ¬ modify*(rs)(h0, h1), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

• Proof step 169:

  h0 \ rs ≠ ∅, ((h0 ≡ h1))(rs), ¬ modify*(rs)(h0, h1), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦ (∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h1 \ rs) + #(h0 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false) ∧ ((h1 ≡ h0))(rs) ∧ ¬ modify*(rs)(h1, h0)

Rule argument

Additional information

Proof step 168 from proof modify-agree (previous step) (back to tree)

Proof step 63 used as proof-lemma

Proof step 169 from proof modify-agree (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 170:

  h0 \ rs ≠ ∅, ((h0 ≡ h1))(rs), ¬ modify*(rs)(h0, h1), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦ (#(h \ rs0) + #(h2 \ rs0) < #(h1 \ rs) + #(h0 \ rs) → ¬ ((h ≡ h2))(rs0) ∨ modify*(rs0)(h, h2)) ∧ ((h1 ≡ h0))(rs) ∧ ¬ modify*(rs)(h1, h0)

Rule argument

Additional information

Proof step 170 from proof modify-agree (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 171:

  h0 \ rs ≠ ∅, #(h \ rs0) + #(h2 \ rs0) < #(h1 \ rs) + #(h0 \ rs), ((h ≡ h2))(rs0), ((h0 ≡ h1))(rs), ¬ modify*(rs0)(h, h2), ¬ modify*(rs)(h0, h1), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

• Proof step 172:

  h0 \ rs ≠ ∅, ((h0 ≡ h1))(rs), ¬ modify*(rs)(h0, h1), ¬ ((h1 ≡ h0))(rs), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

• Proof step 178:

  h0 \ rs ≠ ∅, modify*(rs)(h1, h0), ((h0 ≡ h1))(rs), ¬ modify*(rs)(h0, h1), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Proof step 171 from proof modify-agree (previous step) (back to tree)

User applied rule apply induction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic Used terms: h, rs0, h2

Proof step 172 from proof modify-agree (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 173:

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

• Proof step 174:

  h0 \ rs ≠ ∅, ¬ modify*(rs)(h0, h1), ¬ ((h1 ≡ h0))(rs), ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Used terms: h0, h1, rs

Proof step 173 from proof modify-agree (previous step) (back to tree)

Lemma agree

Proof step 174 from proof modify-agree (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 175:

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

• Proof step 176:

  h0 \ rs ≠ ∅, ¬ modify*(rs)(h0, h1), ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]), ∃ r. ¬(r ∈ rs → (r ∈ h1 ↔ r ∈ h0) ∧ (r ∈ h1 → h1[r] = h0[r])), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦

Rule argument

Additional information

Used terms: h1, h0, rs

Proof step 175 from proof modify-agree (previous step) (back to tree)

Lemma agree

Proof step 176 from proof modify-agree (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 177:

  # rs ≠ 0, h0 \ rs ≠ ∅, rs ≠ ∅, r ∈ rs, ¬ modify*(rs)(h0, h1), ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0[r] = h1[r]), ∀ h, rs0, h2. #(h \ rs0) + #(h2 \ rs0) < #(h0 \ rs) + #(h1 \ rs) → ((h ≡ h2))(rs0) ∧ ¬ modify*(rs0)(h, h2) → false ⊦ (r ∈ h1 ↔ r ∈ h0) ∧ (r ∈ h1 → h1[r] = h0[r])

Rule argument

Additional information

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

Proof step 177 from proof modify-agree (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r

Proof step 178 from proof modify-agree (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 179:

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

Rule argument

Additional information

Used terms: rs, h0, h1

Proof step 179 from proof modify-agree (previous step) (back to tree)

Lemma modify+-sym