Proof step 1 from proof mk-exists (conclusion) (back to tree)

User applied rule induction

And obtained the following new goals

• Proof step 2:

  ∀ h0. # h0 < # h → true → (∃ rs, f. h0 = mk(rs, f)) ⊦ ∃ rs, f. h = mk(rs, f)

Rule argument

Additional information

Used simplifier rules: <; (wellfounded) Used terms: # h

Proof step 2 from proof mk-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ∀ h0. # h0 < # h → true → (∃ rs, f. h0 = mk(rs, f)) ⊦ ∃ rs, f. h = mk(rs, f)

Rule argument

Additional information

Proof step 3 from proof mk-exists (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 4:

  h = ∅, ∀ h0. # h0 < # h → true → (∃ rs, f. h0 = mk(rs, f)) ⊦ ∃ rs, f. h = mk(rs, f)

• Proof step 6:

  h ≠ ∅, ∀ h0. # h0 < # h → true → (∃ rs, f. h0 = mk(rs, f)) ⊦ ∃ rs, f. h = mk(rs, f)

Rule argument

Additional information

Used formulas: h = ∅

Proof step 4 from proof mk-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ∀ h0. # h0 < # ∅ → true → (∃ rs, f. h0 = mk(rs, f)) ⊦ ∃ rs, f. ∅ = mk(rs, f)

Rule argument

Additional information

Proof step 5 from proof mk-exists (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: emp: ⊦ mk(∅, f) = ∅; Used terms: ∅, f

Proof step 6 from proof mk-exists (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

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

• Proof step 8:

  ∃ r. ¬((r ∈ h ↔ r ∈ ∅) ∧ (r ∈ h → h[r] = ∅[r])), ∀ h0. # h0 < # h → true → (∃ rs, f. h0 = mk(rs, f)) ⊦ ∃ rs, f. h = mk(rs, f)

Rule argument

Additional information

Used terms: ∅, h

Proof step 7 from proof mk-exists (previous step) (back to tree)

A spec-lemma

Proof step 8 from proof mk-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  r ∈ h, ∀ h0. # h0 < # h → true → (∃ rs, f. h0 = mk(rs, f)) ⊦ ∃ rs, f. h = mk(rs, f)

Rule argument

Additional information

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

Proof step 9 from proof mk-exists (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

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

• Proof step 11:

  r ≠ null, ∃ h0, o. h = (h0 ++ r)[r, o] ∧ ¬ r ∈ h0, ∀ h0. # h0 < # h → true → (∃ rs, f. h0 = mk(rs, f)) ⊦ ∃ rs, f. h = mk(rs, f)

Rule argument

Additional information

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

Proof step 10 from proof mk-exists (previous step) (back to tree)

A spec-lemma

Proof step 11 from proof mk-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  r ≠ null, ¬ r ∈ h0, ∀ h1. # h1 < # (h0 ++ r)[r, o] → true → (∃ rs, f. h1 = mk(rs, f)) ⊦ ∃ rs, f. (h0 ++ r)[r, o] = mk(rs, f)

Rule argument

Additional information

Proof step 12 from proof mk-exists (previous step) (back to tree)

User applied rule apply induction

And obtained the following new goals

• Proof step 13:

  r ≠ null, ¬ r ∈ h0, ∃ rs, f. h0 = mk(rs, f), ∀ h1. # h1 < # (h0 ++ r)[r, o] → true → (∃ rs, f. h1 = mk(rs, f)) ⊦ ∃ rs, f. (h0 ++ r)[r, o] = mk(rs, f)

Rule argument

Additional information

Used simplifier rules: r0 ≠ null, ¬ r0 ∈ h ⊦ r ∈ h ++ r0 ↔ r = r0 ∨ r ∈ h; (s) r ∈ h ⊦ # h[r, o] = # h; (s) ¬ r ∈ h, r ≠ null ⊦ #(h ++ r) = # h + 1; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ ¬ n < n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: h0

Proof step 13 from proof mk-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  r ≠ null, ¬ r ∈ rs, ∀ h1. # h1 < # (mk(rs, f) ++ r)[r, o] → true → (∃ rs, f. h1 = mk(rs, f)) ⊦ ∃ rs0, f0. (mk(rs, f) ++ r)[r, o] = mk(rs0, f0)

Rule argument

Additional information

Used simplifier rules: in-mk: ⊦ r ∈ mk(rs, f) ↔ r ∈ rs;

Proof step 14 from proof mk-exists (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 15:

  (mk(rs, f) ++ r)[r, o] ≠ mk(rs ++ r, f(r; o)), r ≠ null, ¬ r ∈ rs, ∀ h1. # h1 < # (mk(rs, f) ++ r)[r, o] → true → (∃ rs, f. h1 = mk(rs, f)) ⊦

Rule argument

Additional information

Used terms: rs ++ r, f(r; o)

Proof step 15 from proof mk-exists (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

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

• Proof step 17:

  r ≠ null, ¬ r ∈ rs, ∃ r0. ¬((r0 ∈ (mk(rs, f) ++ r)[r, o] ↔ r0 ∈ mk(rs ++ r, f(r; o))) ∧ (r0 ∈ (mk(rs, f) ++ r)[r, o] → (mk(rs, f) ++ r)[r, o][r0] = mk(rs ++ r, f(r; o))[r0])), ∀ h1. # h1 < # (mk(rs, f) ++ r)[r, o] → true → (∃ rs, f. h1 = mk(rs, f)) ⊦

Rule argument

Additional information

Used terms: mk(rs ++ r, f(r; o)), (mk(rs, f) ++ r)[r, o]

Proof step 16 from proof mk-exists (previous step) (back to tree)

A spec-lemma

Proof step 17 from proof mk-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  (r0 = r ⊃ o;(mk(rs, f) ++ r)[r0]) ≠ mk(rs ++ r, f(r; o))[r0], r ≠ null, ¬ r ∈ rs, r0 = r ∨ r0 ∈ rs, ∀ h1. # h1 < # (mk(rs, f) ++ r)[r, o] → true → (∃ rs, f. h1 = mk(rs, f)) ⊦

Rule argument

Additional information

Used simplifier rules: in-mk: ⊦ r ∈ mk(rs, f) ↔ r ∈ rs; 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) ⊦ a ∈ s ++ b ↔ a = b ∨ a ∈ s; (s)

Proof step 18 from proof mk-exists (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: in-mk: ⊦ r ∈ mk(rs, f) ↔ r ∈ rs; at-mk: ⊦ r ∈ rs → mk(rs, f)[r] = f(r); in-mk: ⊦ r ∈ mk(rs, f) ↔ r ∈ rs; r ∈ h, r0 ≠ null, ¬ r0 ∈ h ⊦ r ≠ r0 → (h ++ r0)[r] = h[r]; (s) ⊦ a ∈ s ++ b ↔ ¬(a ≠ b ∧ ¬ a ∈ s); (ss) ⊦ a ∈ s ++ b ↔ a = b ∨ a ∈ s; (s) Used formulas: r0 ∈ rs ++ r