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

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

• Proof step 7:

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

Rule argument

Additional information

Used terms: modify(rs), h0, h1

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

• Proof step 15:

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

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

  (h ≡ h1)(rs), modify(rs)(h0, h), rtc(n0, modify(rs))(h, h1), ¬ (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:

  (h ≡ h1)(rs), modify(rs)(h0, h), ¬ (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:

  (h ≡ h1)(rs), modify(rs)(h0, h), ∃ 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:

  (h ≡ h1)(rs), modify(rs)(h0, h), r ∈ 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, obj. ¬ r ∈ rs ∧ r ∈ h0 ∧ h1 = h0(r := obj)) ∨ (∃ 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, obj. ¬ r ∈ rs ∧ r ∈ h0 ∧ h = h0(r := obj)) ∨ (∃ 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, ¬ r0 ∈ rs ∧ r0 ≠ null ∧ ¬ r0 ∈ h0 ∧ h = h0 ++ r0 ∨ ¬ r1 ∈ rs ∧ r1 ∈ h0 ∧ h = h0(r1 := ob) ∨ ¬ r2 ∈ rs ∧ r2 ∈ h0 ∧ h = h0 -- r2, r ∈ h1 → h(r) = h1(r) ⊦ (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:

  h = h0 ++ r0, r ∈ h ↔ r ∈ h1, 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 36:

  h = h0(r1 := ob), r ∈ h ↔ r ∈ h1, r ∈ rs, r1 ∈ h0, ¬ r1 ∈ rs, r ∈ h1 → h(r) = h1(r) ⊦ (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0(r) = h1(r))

• Proof step 38:

  h = h0 -- r2, r ∈ h ↔ r ∈ h1, 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

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:

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

Rule argument

Additional information

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 ⊦ (h ++ r0)(r) = h(r)

• Proof step 33:

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

• Proof step 34:

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

Rule argument

Additional information

Used terms: r, h0, r0

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 closed the goal!

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

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

Rule argument

Additional information

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

Heuristic nonsplitting cut applied rule cut formula

And closed the goal!

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 37:

  r ∈ h0(r1 := ob) ↔ r ∈ h1, r ∈ rs, r1 ∈ h0, ¬ r1 ∈ rs, r ∈ h1 → h0(r1 := ob)(r) = h1(r) ⊦ (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0(r) = h1(r))

Rule argument

Additional information

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

Heuristic nonsplitting cut applied rule cut formula

And closed the goal!

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) Used formulas: r ∈ h0(r1 := ob)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 39:

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

Rule argument

Additional information

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:

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

• Proof step 41:

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

• Proof step 44:

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

Rule argument

Additional information

Used terms: r, r2, h0

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 42:

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

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 43:

  ⊦ r ∈ h -- r0 ↔ r ≠ r0 ∧ r ∈ h

Rule argument

Additional information

Used terms: r, h0, r2

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 45:

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

Rule argument

Additional information

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

Heuristic nonsplitting cut applied rule cut formula

And closed the goal!

Rule argument

Additional information

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

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

User applied rule induction

And obtained the following new goals

• Proof step 47:

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

User applied rule cut formula

And obtained the following new goals

• Proof step 48:

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

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

User applied rule cut formula

And obtained the following new goals

• Proof step 49:

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 50:

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

• Proof step 51:

  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: h0, h1, rs

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

Lemma agree

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 52:

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

• Proof step 53:

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

Lemma modify+

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:

  ⊦ pelem.^*(a1, a2) ↔ (∃ n. rtc(n, pelem)(a1, a2))

• Proof step 55:

  h0 \ rs = ∅, h1 \ rs = ∅, ∀ n. ¬ rtc(n, 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: modify(rs), h0, h1

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)

User applied rule all left

And obtained the following new goals

• Proof step 56:

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

  ⊦ rtc(0, pelem)(a1, a2) ↔ a1 = a2

• Proof step 58:

  h0 \ rs = ∅, h1 \ 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 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)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 59:

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

• Proof step 60:

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

A spec-lemma

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:

  h0 \ rs = ∅, 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

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

User applied rule all left

And obtained the following new goals

• Proof step 62:

  h0 \ rs = ∅, h1 \ rs = ∅, ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0(r) = h1(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 62 from proof modify-agree (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 63:

  h0 \ rs = ∅, h1 \ 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 63 from proof modify-agree (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 64:

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

• Proof step 65:

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 66:

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 67:

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

• Proof step 68:

  ¬ r ∈ 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)), ∀ 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 terms: h0 \ rs, ∅

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 69:

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

User applied rule all left

And obtained the following new goals

• Proof step 70:

  ¬ r ∈ 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 terms: r

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 71:

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

User applied rule weakening

And obtained the following new goals

• Proof step 73:

  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 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 ≠ ∅, (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 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 ↔ (∀ r. (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0(r) = h1(r)))

• Proof step 76:

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 77:

  (h0 ≡ h1)(rs), r ∈ 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 77 from proof modify-agree (previous step) (back to tree)

User applied rule apply induction

And obtained the following new goals

• Proof step 78:

  (h0 ≡ h1)(rs), r ∈ 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 145:

  (h0 ≡ h1)(rs), r ∈ 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 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:

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

• Proof step 80:

  (h0 ≡ h1)(rs), r ∈ 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 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 apply rewrite lemma

And obtained the following new goals

• Proof step 81:

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

• Proof step 82:

  (h0 ≡ h1)(rs), r ∈ 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 81 from proof modify-agree (previous step) (back to tree)

A spec-lemma

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

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 83:

  #(h1 \ rs) = 0, (h0 ≡ h1)(rs), r ∈ 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), n0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 84:

  #(h1 \ rs) = 0, (h0 ≡ h1)(rs), r ∈ 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 84 from proof modify-agree (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 85:

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

• Proof step 86:

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

Lemma agree

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:

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

• Proof step 88:

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

Lemma modify+

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 89:

  ⊦ pelem.^*(a1, a2) ↔ (∃ n. rtc(n, pelem)(a1, a2))

• Proof step 90:

  #(h1 \ rs) = 0, r ∈ h1 \ rs, ∀ n. ¬ rtc(n, 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: modify(rs), h0, h1

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 92:

  ⊦ rtc(0, pelem)(a1, a2) ↔ a1 = a2

• Proof step 93:

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 94:

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

• Proof step 95:

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 96:

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 97:

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

• Proof step 98:

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

A spec-lemma

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

User applied rule cut formula

And obtained the following new goals

• Proof step 99:

  #(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 122:

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 100:

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

User applied rule all left

And obtained the following new goals

• Proof step 101:

  #(h1 \ rs) = 0, h0(r0) ≠ h1(r0), r ∈ h1, r0 ∈ h1, r0 ∈ h0, ¬ r ∈ rs, ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0(r) = h1(r)), r0 ∈ rs → (r0 ∈ h0 ↔ r0 ∈ h1) ∧ (r0 ∈ h0 → h0(r0) = h1(r0)), ∀ 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 101 from proof modify-agree (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 102:

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 103:

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

• Proof step 104:

  #(h1 \ rs) = 0, h0(r0) ≠ h1(r0), r0 ≠ null, r ∈ h1, r0 ∈ h0, ¬ r ∈ rs, ¬ r0 ∈ rs, ∃ h0, ob. h1 = (h0 ++ r0)(r0 := ob) ∧ ¬ r0 ∈ h0, ∀ 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 simplifier rules: ⊦ ¬ null ∈ h; (s) Used terms: r0, h1

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 105:

  #((h ++ r0)(r0 := ob) \ rs) = 0, h0(r0) ≠ (h ++ r0)(r0 := ob)(r0), r ∈ (h ++ r0)(r0 := ob), r0 ∈ h0, ¬ r ∈ rs, ¬ r0 ∈ rs, ¬ r0 ∈ h, ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ (h ++ r0)(r0 := ob)) ∧ (r ∈ h0 → h0(r) = (h ++ r0)(r0 := ob)(r)), ∀ 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 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:

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

• Proof step 107:

  # ((h \ rs) ++ r0)(r0 := ob) = 0, h0(r0) ≠ (h ++ r0)(r0 := ob)(r0), r0 ≠ null, r ∈ (h ++ r0)(r0 := ob), r0 ∈ h0, ¬ r ∈ rs, ¬ r0 ∈ rs, ¬ r0 ∈ h, ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ (h ++ r0)(r0 := ob)) ∧ (r ∈ h0 → h0(r) = (h ++ r0)(r0 := ob)(r)), ∀ 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, ob, rs

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)(r0 := ob) = 0, h0(r0) ≠ (h ++ r0)(r0 := ob)(r0), r ∈ (h ++ r0)(r0 := ob), r0 ∈ h0, ¬ r ∈ rs, ¬ r0 ∈ rs, ¬ r0 ∈ h, ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ (h ++ r0)(r0 := ob)) ∧ (r ∈ h0 → h0(r) = (h ++ r0)(r0 := ob)(r)), ∀ 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 ⊦ # h(r := o) = # h

• Proof step 110:

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

• Proof step 115:

  #((h \ rs) ++ r0) = 0, h0(r0) ≠ (h ++ r0)(r0 := ob)(r0), r ∈ (h ++ r0)(r0 := ob), r0 ∈ h0, r0 ∈ (h \ rs) ++ r0, ¬ r ∈ rs, ¬ r0 ∈ rs, ¬ r0 ∈ h, ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ (h ++ r0)(r0 := ob)) ∧ (r ∈ h0 → h0(r) = (h ++ r0)(r0 := ob)(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: (h \ rs) ++ r0, r0, ob

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)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 111:

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

• Proof step 112:

  # ((h \ rs) ++ r0)(r0 := ob) = 0, h0(r0) ≠ (h ++ r0)(r0 := ob)(r0), r ∈ (h ++ r0)(r0 := ob), r0 ∈ h0, ¬ r ∈ rs, ¬ r0 ∈ (h \ rs) ++ r0, ¬ r0 ∈ rs, ¬ r0 ∈ h, ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ (h ++ r0)(r0 := ob)) ∧ (r ∈ h0 → h0(r) = (h ++ r0)(r0 := ob)(r)), ∀ 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 111 from proof modify-agree (previous step) (back to tree)

A spec-lemma

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:

  # ((h \ rs) ++ r0)(r0 := ob) = 0, h0(r0) ≠ (h ++ r0)(r0 := ob)(r0), r ∈ (h ++ r0)(r0 := ob), r0 ∈ h0, r0 ∈ h \ rs, ¬ r ∈ rs, ¬ r0 ∈ (h \ rs) ++ r0, ¬ r0 ∈ rs, ¬ r0 ∈ h, ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ (h ++ r0)(r0 := ob)) ∧ (r ∈ h0 → h0(r) = (h ++ r0)(r0 := ob)(r)), ∀ 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 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 ∈ h \ rs ↔ r ∈ h ∧ ¬ r ∈ rs

Rule argument

Additional information

Used terms: r0, h, rs

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)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 116:

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

• Proof step 117:

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

• Proof step 120:

  #((h \ rs) ++ r0) = 0, h0(r0) ≠ (h ++ r0)(r0 := ob)(r0), r0 ≠ null, r ∈ (h ++ r0)(r0 := ob), r0 ∈ h0, ¬ r ∈ rs, ¬ r0 ∈ h \ rs, ¬ r0 ∈ rs, ¬ r0 ∈ h, ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ (h ++ r0)(r0 := ob)) ∧ (r ∈ h0 → h0(r) = (h ++ r0)(r0 := ob)(r)), r0 = r0 ∨ r0 ∈ h \ rs, ∀ 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, h \ rs, r0

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 118:

  #((h \ rs) ++ r0) = 0, h0(r0) ≠ (h ++ r0)(r0 := ob)(r0), r ∈ (h ++ r0)(r0 := ob), r0 ∈ h0, r0 ∈ (h \ rs) ++ r0, r0 ∈ h \ rs, ¬ r ∈ rs, ¬ r0 ∈ rs, ¬ r0 ∈ h, ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ (h ++ r0)(r0 := ob)) ∧ (r ∈ h0 → h0(r) = (h ++ r0)(r0 := ob)(r)), ∀ 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 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 \ rs ↔ r ∈ h ∧ ¬ r ∈ rs

Rule argument

Additional information

Used terms: r0, h, rs

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)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 121:

  #((h \ rs) ++ r0) = 0, h0(r0) ≠ (h ++ r0)(r0 := ob)(r0), r0 ≠ null, r ∈ (h ++ r0)(r0 := ob), r0 ∈ h0, ¬ r ∈ rs, ¬ r0 ∈ h \ rs, ¬ r0 ∈ rs, ¬ r0 ∈ h, ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ (h ++ r0)(r0 := ob)) ∧ (r ∈ h0 → h0(r) = (h ++ r0)(r0 := ob)(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 121 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; (s) ¬ 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

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:

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

User applied rule all left

And obtained the following new goals

• Proof step 124:

  #(h1 \ rs) = 0, ¬(r0 ∈ h0 ↔ r0 ∈ h1), r ∈ h1, ¬ r ∈ rs, ∀ r. r ∈ rs → (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0(r) = h1(r)), r0 ∈ rs → (r0 ∈ h0 ↔ r0 ∈ h1) ∧ (r0 ∈ h0 → h0(r0) = h1(r0)), ∀ 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 124 from proof modify-agree (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 125:

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 126:

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

• Proof step 127:

  #(h1 \ rs) = 0, r ≠ null, ¬(r0 ∈ h0 ↔ r0 ∈ h1), ¬ r ∈ rs, ¬ r0 ∈ rs, ∃ h0, ob. h1 = (h0 ++ r)(r := ob) ∧ ¬ r ∈ h0, ∀ 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 simplifier rules: ⊦ ¬ null ∈ h; (s) Used terms: r, h1

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 128:

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

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 129:

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

• Proof step 130:

  # ((h \ rs) ++ r)(r := ob) = 0, r ≠ null, ¬(r0 ∈ h0 ↔ r0 ∈ (h ++ r)(r := ob)), ¬ r ∈ rs, ¬ r ∈ h, ¬ r0 ∈ rs, ∀ r0. r0 ∈ rs → (r0 ∈ h0 ↔ r0 ∈ (h ++ r)(r := ob)) ∧ (r0 ∈ h0 → h0(r0) = (h ++ r)(r := ob)(r0)), ∀ 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, ob, rs

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 131:

  r ∈ h ⊦ # h(r := o) = # h

• Proof step 132:

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

• Proof step 137:

  #((h \ rs) ++ r) = 0, r ≠ null, ¬(r0 ∈ h0 ↔ r0 ∈ (h ++ r)(r := ob)), r ∈ (h \ rs) ++ r, ¬ r ∈ rs, ¬ r ∈ h, ¬ r0 ∈ rs, ∀ r0. r0 ∈ rs → (r0 ∈ h0 ↔ r0 ∈ (h ++ r)(r := ob)) ∧ (r0 ∈ h0 → h0(r0) = (h ++ r)(r := ob)(r0)), ∀ 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, ob

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 133:

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

• Proof step 134:

  # ((h \ rs) ++ r)(r := ob) = 0, r ≠ null, ¬(r0 ∈ h0 ↔ r0 ∈ (h ++ r)(r := ob)), ¬ r ∈ (h \ rs) ++ r, ¬ r ∈ rs, ¬ r ∈ h, ¬ r0 ∈ rs, ∀ r0. r0 ∈ rs → (r0 ∈ h0 ↔ r0 ∈ (h ++ r)(r := ob)) ∧ (r0 ∈ h0 → h0(r0) = (h ++ r)(r := ob)(r0)), ∀ 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 133 from proof modify-agree (previous step) (back to tree)

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 135:

  # ((h \ rs) ++ r)(r := ob) = 0, ¬(r0 ∈ h0 ↔ r0 ∈ (h ++ r)(r := ob)), r ∈ h \ rs, ¬ r ∈ (h \ rs) ++ r, ¬ r ∈ rs, ¬ r ∈ h, ¬ r0 ∈ rs, ∀ r0. r0 ∈ rs → (r0 ∈ h0 ↔ r0 ∈ (h ++ r)(r := ob)) ∧ (r0 ∈ h0 → h0(r0) = (h ++ r)(r := ob)(r0)), ∀ 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 135 from proof modify-agree (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 136:

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

Rule argument

Additional information

Used terms: r, h, rs

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 138:

  #((h \ rs) ++ r) = 0, ¬(r0 ∈ h0 ↔ r0 ∈ (h ++ r)(r := ob)), r ∈ (h \ rs) ++ r, ¬ r ∈ rs, ¬ r ∈ h, ¬ r0 ∈ rs, ∀ r0. r0 ∈ rs → (r0 ∈ h0 ↔ r0 ∈ (h ++ r)(r := ob)) ∧ (r0 ∈ h0 → h0(r0) = (h ++ r)(r := ob)(r0)), ∀ 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 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:

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

• Proof step 140:

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

• Proof step 143:

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

Rule argument

Additional information

Used terms: r, h \ rs, 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:

  #((h \ rs) ++ r) = 0, ¬(r0 ∈ h0 ↔ r0 ∈ (h ++ r)(r := ob)), r ∈ (h \ rs) ++ r, r ∈ h \ rs, ¬ r ∈ rs, ¬ r ∈ h, ¬ r0 ∈ rs, ∀ r0. r0 ∈ rs → (r0 ∈ h0 ↔ r0 ∈ (h ++ r)(r := ob)) ∧ (r0 ∈ h0 → h0(r0) = (h ++ r)(r := ob)(r0)), ∀ 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 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:

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

Rule argument

Additional information

Used terms: r, h, rs

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)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 144:

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

Rule argument

Additional information

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

Heuristic nonsplitting cut applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ r ∈ h \ rs ↔ r ∈ h ∧ ¬ r ∈ rs; (s) ¬ 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 formulas: r0 ∈ h0

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 146:

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

• Proof step 147:

  (h0 ≡ h1)(rs), r ∈ h1, ¬ 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 146 from proof modify-agree (previous step) (back to tree)

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 148:

  (h0 ≡ h1)(rs), r ∈ h1, ¬ 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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 149:

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

• Proof step 150:

  (h0 ≡ h1)(rs), r ∈ h1, ¬ 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: rs, h0, h1 -- r

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

Lemma modify+

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 151:

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

• Proof step 152:

  (h0 ≡ h1)(rs), r ∈ h1, ¬ 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: rs, h0, h1

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

Lemma modify+

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 153:

  ⊦ pelem.^*(a1, a2) ↔ (∃ n. rtc(n, pelem)(a1, a2))

• Proof step 154:

  (h0 ≡ h1)(rs), r ∈ h1, ¬ 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) ∧ ¬(∃ n. rtc(n, modify(rs))(h0, h1 -- r))

Rule argument

Additional information

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

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 155:

  (h0 ≡ h1)(rs), r ∈ h1, ¬ 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) ∧ ¬ rtc(n, modify(rs))(h0, h1 -- r)

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 156:

  ⊦ pelem.^*(a1, a2) ↔ (∃ n. rtc(n, pelem)(a1, a2))

• Proof step 157:

  (h0 ≡ h1)(rs), r ∈ h1, ¬ 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 ⊦ (h0 ≡ (h1 -- r))(rs) ∧ ¬ rtc(n, modify(rs))(h0, h1 -- r)

Rule argument

Additional information

Used terms: modify(rs), h0, h1

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

A spec-lemma

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

User applied rule all left

And obtained the following new goals

• Proof step 158:

  (h0 ≡ h1)(rs), r ∈ h1, ¬ r ∈ rs, ¬ rtc(n + 2, 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) ∧ ¬ rtc(n, modify(rs))(h0, h1 -- r)

Rule argument

Additional information

Used terms: n + 2

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:

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

• Proof step 160:

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

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

A spec-lemma

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:

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

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

User applied rule all left

And obtained the following new goals

• Proof step 162:

  (h0 ≡ h1)(rs), r ∈ h1, ¬ 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 ⊦ (h0 ≡ (h1 -- r))(rs) ∧ ¬ rtc(n, modify(rs))(h0, h1 -- r)

Rule argument

Additional information

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

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

User applied rule case distinction

And obtained the following new goals

• Proof step 163:

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

• Proof step 174:

  (h0 ≡ h1)(rs), r ∈ h1, ¬ 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 ⊦ (h0 ≡ (h1 -- r))(rs) ∧ ¬ rtc(n, modify(rs))(h0, h1 -- r)

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:

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

• Proof step 165:

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

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

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

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

User applied rule all left

And obtained the following new goals

• Proof step 167:

  (h0 ≡ h1)(rs), r ∈ h1, ¬ 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 ⊦ (h0 ≡ (h1 -- r))(rs) ∧ ¬ rtc(n, modify(rs))(h0, h1 -- r)

Rule argument

Additional information

Used terms: h1 -- r

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 168:

  (h0 ≡ h1)(rs), r ∈ h1, ¬ 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 ⊦ (h0 ≡ (h1 -- r))(rs) ∧ ¬ rtc(n, modify(rs))(h0, h1 -- r)

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 169:

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

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

Rule argument

Additional information

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

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

Lemma modify

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 171:

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

Rule argument

Additional information

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

User applied rule case distinction

And obtained the following new goals

• Proof step 172:

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

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 173:

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

Rule argument

Additional information

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

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

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

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

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:

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

  (h0 ≡ h1)(rs), r ∈ h1, ¬ r ∈ rs, ∀ r0. ¬(¬ r0 ∈ rs ∧ r0 ≠ null ∧ ¬ r0 ∈ (h1 -- r) ++ r ∧ h1 = (h1 -- r) ++ r ++ r0), ∀ r0, obj. ¬(¬ r0 ∈ rs ∧ r0 ∈ (h1 -- r) ++ r ∧ h1 = ((h1 -- r) ++ r)(r0 := obj)), ∀ 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 ⊦ (h0 ≡ (h1 -- r))(rs) ∧ ¬ rtc(n, modify(rs))(h0, h1 -- r)

Rule argument

Additional information

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

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

Lemma modify

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:

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

Rule argument

Additional information

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

User applied rule all left

And obtained the following new goals

• Proof step 178:

  (h0 ≡ h1)(rs), r ∈ h1, ¬ r ∈ rs, r ∈ rs ∨ ¬ r ∈ (h1 -- r) ++ r ∨ h1 ≠ ((h1 -- r) ++ r)(r := h1(r)), ∀ r0. r0 ∈ rs ∨ r0 = null ∨ r0 ∈ (h1 -- r) ++ r ∨ h1 ≠ (h1 -- r) ++ r ++ r0, ∀ 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 ⊦ (h0 ≡ (h1 -- r))(rs) ∧ ¬ rtc(n, modify(rs))(h0, h1 -- r)

Rule argument

Additional information

Used terms: r, h1(r)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 179:

  (h0 ≡ h1)(rs), r ∈ h1, ¬ r ∈ rs, ¬ r ∈ (h1 -- r) ++ r ∨ h1 ≠ ((h1 -- r) ++ r)(r := h1(r)), ∀ r0. r0 ∈ rs ∨ ¬ r0 ∈ (h1 -- r) ++ r ∨ h1 ≠ ((h1 -- r) ++ r) -- r0, ∀ r0. r0 ∈ rs ∨ r0 = null ∨ 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 ⊦ (h0 ≡ (h1 -- r))(rs) ∧ ¬ rtc(n, modify(rs))(h0, h1 -- r)

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 180:

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

• Proof step 181:

  (h0 ≡ h1)(rs), r ∈ h1, ¬ r ∈ rs, ¬ r ∈ (h1 -- r) ++ r ∨ ¬(∀ r0. (r0 ∈ h1 ↔ r0 ∈ ((h1 -- r) ++ r)(r := h1(r))) ∧ (r0 ∈ h1 → h1(r0) = ((h1 -- r) ++ r)(r := h1(r))(r0))), ∀ r0. r0 ∈ rs ∨ r0 = null ∨ r0 ∈ (h1 -- r) ++ r ∨ h1 ≠ (h1 -- r) ++ r ++ r0, ∀ 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 ⊦ (h0 ≡ (h1 -- r))(rs) ∧ ¬ rtc(n, modify(rs))(h0, h1 -- r)

Rule argument

Additional information

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

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 182:

  (h0 ≡ h1)(rs), r ∈ h1, ¬ r ∈ rs, ¬ r ∈ (h1 -- r) ++ r ∨ ¬(r0 ∈ h1 ↔ r0 ∈ ((h1 -- r) ++ r)(r := h1(r))) ∨ ¬(r0 ∈ h1 → h1(r0) = ((h1 -- r) ++ r)(r := h1(r))(r0)), ∀ r0. r0 ∈ rs ∨ ¬ r0 ∈ (h1 -- r) ++ r ∨ h1 ≠ ((h1 -- r) ++ r) -- r0, ∀ r0. r0 ∈ rs ∨ r0 = null ∨ 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 ⊦ (h0 ≡ (h1 -- r))(rs) ∧ ¬ rtc(n, modify(rs))(h0, h1 -- r)

Rule argument

Additional information

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

User applied rule case distinction

And obtained the following new goals

• Proof step 183:

  (h0 ≡ h1)(rs), r ∈ h1, ¬ r ∈ (h1 -- r) ++ r, ¬ r ∈ rs, ∀ r0. r0 ∈ rs ∨ r0 = null ∨ r0 ∈ (h1 -- r) ++ r ∨ h1 ≠ (h1 -- r) ++ r ++ r0, ∀ 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 ⊦ (h0 ≡ (h1 -- r))(rs) ∧ ¬ rtc(n, modify(rs))(h0, h1 -- r)

• Proof step 184:

  ¬(r0 ∈ h1 ↔ r0 ∈ ((h1 -- r) ++ r)(r := h1(r))), (h0 ≡ h1)(rs), r ∈ h1, ¬ r ∈ rs, ∀ r0. r0 ∈ rs ∨ r0 = null ∨ r0 ∈ (h1 -- r) ++ r ∨ h1 ≠ (h1 -- r) ++ r ++ r0, ∀ 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 ⊦ (h0 ≡ (h1 -- r))(rs) ∧ ¬ rtc(n, modify(rs))(h0, h1 -- r)

• Proof step 185:

  h1(r0) ≠ ((h1 -- r) ++ r)(r := h1(r))(r0), (h0 ≡ h1)(rs), r ∈ h1, r0 ∈ h1, ¬ r ∈ rs, ∀ r0. r0 ∈ rs ∨ r0 = null ∨ r0 ∈ (h1 -- r) ++ r ∨ h1 ≠ (h1 -- r) ++ r ++ r0, ∀ 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 ⊦ (h0 ≡ (h1 -- r))(rs) ∧ ¬ rtc(n, modify(rs))(h0, h1 -- r)

Rule argument

Additional information

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

Heuristic nonsplitting cut applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: agree-rm-01: ⊦ ¬ r ∈ rs → ((h ≡ (h0 -- r))(rs) ↔ (h ≡ h0)(rs)); agree-rm-01: ⊦ ¬ r ∈ rs → ((h ≡ (h0 -- r))(rs) ↔ (h ≡ h0)(rs)); ⊦ r ∈ h → r ≠ null; (s) ⊦ r ∈ h -- r0 ↔ r ≠ r0 ∧ r ∈ h; (s) r0 ≠ null, ¬ r0 ∈ h ⊦ r ∈ h ++ r0 ↔ r = r0 ∨ r ∈ h; (s) Used formulas: (h0 ≡ (h1 -- r))(rs)

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

Heuristic nonsplitting cut applied rule cut formula

And closed the goal!

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 186:

  ⊦ h(r0 := o)(r) = (r = r0 ∧ r0 ∈ h ⊃ o;h(r))

• Proof step 187:

  h1(r0) ≠ (r0 = r ∧ r ∈ (h1 -- r) ++ r ⊃ h1(r);((h1 -- r) ++ r)(r0)), (h0 ≡ h1)(rs), r ∈ h1, r0 ∈ h1, ¬ r ∈ rs, ∀ r0. r0 ∈ rs ∨ ¬ r0 ∈ (h1 -- r) ++ r ∨ h1 ≠ ((h1 -- r) ++ r) -- r0, ∀ r0. r0 ∈ rs ∨ r0 = null ∨ 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 ⊦ (h0 ≡ (h1 -- r))(rs) ∧ ¬ rtc(n, modify(rs))(h0, h1 -- r)

Rule argument

Additional information

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

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 188:

  h1(r0) ≠ (r0 = r ⊃ h1(r);((h1 -- r) ++ r)(r0)), (h0 ≡ h1)(rs), r ∈ h1, r0 ∈ h1, rtc(n, modify(rs))(h0, h1 -- r), ¬ r ∈ rs, ∀ r1. r1 ∈ rs ∨ r1 = null ∨ r1 ∈ h1 ∨ h1 ≠ (h1 -- r) ++ r ++ r1, ∀ r1. r1 ∈ rs ∨ ¬ r1 ∈ h1 ∨ h1 ≠ ((h1 -- r) ++ r) -- r1, ∀ 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)); ⊦ 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 188 from proof modify-agree (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 189:

  h1(r0) ≠ (r0 = r ⊃ h1(r);((h1 -- r) ++ r)(r0)), r0 ≠ r, (h0 ≡ h1)(rs), r ∈ h1, r0 ∈ h1, rtc(n, modify(rs))(h0, h1 -- r), ¬ r ∈ rs, ∀ r1. r1 ∈ rs ∨ ¬ r1 ∈ h1 ∨ h1 ≠ ((h1 -- r) ++ r) -- r1, ∀ r1. r1 ∈ rs ∨ r1 = null ∨ r1 ∈ h1 ∨ h1 ≠ (h1 -- r) ++ r ++ r1, ∀ 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: r0 = r

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 190:

  h1(r0) ≠ ((h1 -- r) ++ r)(r0), r0 ≠ r, (h0 ≡ h1)(rs), r ∈ h1, r0 ∈ h1, rtc(n, modify(rs))(h0, h1 -- r), ¬ r ∈ rs, ∀ r1. r1 ∈ rs ∨ r1 = null ∨ r1 ∈ h1 ∨ h1 ≠ (h1 -- r) ++ r ++ r1, ∀ r1. r1 ∈ rs ∨ ¬ r1 ∈ h1 ∨ h1 ≠ ((h1 -- r) ++ r) -- r1, ∀ 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 190 from proof modify-agree (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 191:

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

Rule argument

Additional information

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

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

A spec-lemma

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

User applied rule apply proof lemma

And obtained the following new goals

• Proof step 193:

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

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

Proof step 73 used as proof-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 195:

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

User applied rule case distinction

And obtained the following new goals

• Proof step 196:

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

  h0 \ rs ≠ ∅, (h0 ≡ h1)(rs), ¬ (h1 ≡ h0)(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 203:

  h0 \ rs ≠ ∅, (h0 ≡ h1)(rs), modify*(rs)(h1, h0), ¬ 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 196 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 197 from proof modify-agree (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 198:

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

• Proof step 199:

  h0 \ rs ≠ ∅, ¬ (h1 ≡ 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 198 from proof modify-agree (previous step) (back to tree)

Lemma agree

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 200:

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

• Proof step 201:

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

Lemma agree

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 202:

  # 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 ne-01: ⊦ a ∈ s → s ≠ ∅; (forward) from specification set-basic

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 204:

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

Rule argument

Additional information

Used terms: rs, h0, h1

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

Lemma modify+-sym