Proof step 1 from proof get-known (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(g(r) = a ↔ true), (a[r => o] * hR)[rs, f, g] ⊦

Rule argument

Additional information

Proof step 2 from proof get-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  g(r) ≠ a, (a[r => o] * hR)[rs, f, g] ⊦

Rule argument

Additional information

Proof step 3 from proof get-known (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ (hR0 * hR1)[rs, f, g] ↔ (∃ rs0, rs1. rs0 ∪ rs1 = rs ∧ rs0 ∩ rs1 = ∅ ∧ hR0[rs0, f, g] ∧ hR1[rs1, f, g])

• Proof step 5:

  g(r) ≠ a, ∃ rs0, rs1. rs0 ∪ rs1 = rs ∧ rs0 ∩ rs1 = ∅ ∧ a[r => o][rs0, f, g] ∧ hR[rs1, f, g] ⊦

Rule argument

Additional information

Used terms: rs, hR, g, a[r => o], f

Proof step 4 from proof get-known (previous step) (back to tree)

A spec-lemma

Proof step 5 from proof get-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  rs0 ∩ rs1 = ∅, g(r) ≠ a, a[r => o][rs0, f, g], hR[rs1, f, g] ⊦

Rule argument

Additional information

Proof step 6 from proof get-known (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ hR[rs, f, g] ↔ hR(mk(rs, f, g))

• Proof step 8:

  rs0 ∩ rs1 = ∅, g(r) ≠ a, hR[rs1, f, g], a[r => o](mk(rs0, f, g)) ⊦

Rule argument

Additional information

Used terms: g, f, rs0, a[r => o]

Proof step 7 from proof get-known (previous step) (back to tree)

A spec-lemma

Proof step 8 from proof get-known (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ a[hP](mk(rs, f, g)) ↔ hP(mk(rs, f)) ∧ (∀ r. r ∈ rs → g(r) = a)

• Proof step 10:

  rs0 ∩ rs1 = ∅, g(r) ≠ a, ((r => o))(mk(rs0, f)), hR[rs1, f, g], ∀ r. r ∈ rs0 → g(r) = a ⊦

Rule argument

Additional information

Used terms: a, r => o, rs0, g, f

Proof step 9 from proof get-known (previous step) (back to tree)

Lemma lift-aux

Proof step 10 from proof get-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  rs0 ∩ rs1 = ∅, g(r) ≠ a, ((r => o))(mk(rs0, f)), hR[rs1, f, g], ∀ r. r ∈ rs0 → g(r) = a ⊦

Rule argument

Additional information

Proof step 11 from proof get-known (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  ⊦ ((r => o))(h) ↔ h = (∅ ++ r)[r, o] ∧ r ≠ null

• Proof step 13:

  mk(rs0, f) = (∅ ++ r)[r, o], rs0 ∩ rs1 = ∅, g(r) ≠ a, r ≠ null, hR[rs1, f, g], ∀ r. r ∈ rs0 → g(r) = a ⊦

Rule argument

Additional information

Used terms: mk(rs0, f), o, r

Proof step 12 from proof get-known (previous step) (back to tree)

A spec-lemma

Proof step 13 from proof get-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  mk(rs0, f) = (∅ ++ r)[r, o], rs0 ∩ rs1 = ∅, g(r) ≠ a, r ≠ null, hR[rs1, f, g], ∀ r. r ∈ rs0 → g(r) = a ⊦

Rule argument

Additional information

Proof step 14 from proof get-known (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

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

• Proof step 16:

  rs0 ∩ rs1 = ∅, g(r) ≠ a, r ≠ null, hR[rs1, f, g], ∀ r. r ∈ rs0 → g(r) = a, ∀ r0. (r0 ∈ mk(rs0, f) ↔ r0 ∈ (∅ ++ r)[r, o]) ∧ (r0 ∈ mk(rs0, f) → mk(rs0, f)[r0] = (∅ ++ r)[r, o][r0]) ⊦

Rule argument

Additional information

Used terms: (∅ ++ r)[r, o], mk(rs0, f)

Proof step 15 from proof get-known (previous step) (back to tree)

A spec-lemma

Proof step 16 from proof get-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  rs0 ∩ rs1 = ∅, g(r) ≠ a, r ≠ null, hR[rs1, f, g], ∀ r. r ∈ rs0 → g(r) = a, ∀ r0. (r0 ∈ rs0 ↔ r0 = r) ∧ (r0 ∈ rs0 → f(r0) = (r0 = r ⊃ o;(∅ ++ r)[r0])) ⊦

Rule argument

Additional information

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

Proof step 17 from proof get-known (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 18:

  r ∈ rs0 ↔ r = r, rs0 ∩ rs1 = ∅, g(r) ≠ a, r ≠ null, hR[rs1, f, g], r ∈ rs0 → f(r) = (r = r ⊃ o;(∅ ++ r)[r]), ∀ r0. (r0 ∈ rs0 ↔ r0 = r) ∧ (r0 ∈ rs0 → f(r0) = (r0 = r ⊃ o;(∅ ++ r)[r0])), ∀ r. r ∈ rs0 → g(r) = a ⊦

Rule argument

Additional information

Used terms: r

Proof step 18 from proof get-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  rs0 ∩ rs1 = ∅, g(r) ≠ a, r ≠ null, hR[rs1, f, g], r ∈ rs0, ∀ r. r ∈ rs0 → g(r) = a, ∀ r0. (r0 ∈ rs0 → r0 = r) ∧ (r0 ∈ rs0 → f(r0) = (r0 = r ⊃ f(r);(∅ ++ r)[r0])) ⊦

Rule argument

Additional information

Proof step 19 from proof get-known (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r