Proof step 1 from proof absset-addboth (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ar[n] = ⊥, ¬(absset(ar[n := e], set ++ e) ↔ e ≠ ⊥), n < # ar, absset(ar, set) ⊦

Rule argument

Additional information

Proof step 2 from proof absset-addboth (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ar[n] = ⊥, n < # ar, ∀ e0. e0 ∈ set ↔ (∃ n0. n0 < # ar ∧ e0 = ar[n0] ∧ ar[n0] ≠ ⊥) ⊦ (∀ e0. e0 = e ∨ e0 ∈ set ↔ (∃ n0. n0 < # ar ∧ e0 = (ar[n := e])[n0] ∧ (ar[n := e])[n0] ≠ ⊥)) ↔ e ≠ ⊥

Rule argument

Additional information

Used simplifier rules: absset-def: ⊦ absset(ar, set) ↔ (∀ e. e ∈ set ↔ (∃ n. n < # ar ∧ e = ar[n] ∧ e ≠ ⊥)); ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ # ar[n := a] = # ar; (s) ⊦ a ∈ s ++ b ↔ a = b ∨ a ∈ s; (s)

Proof step 3 from proof absset-addboth (previous step) (back to tree)

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 4:

  ar[n] = ⊥, e = ⊥, n < # ar, ∀ e0. e0 ∈ set ↔ (∃ n0. n0 < # ar ∧ e0 = ar[n0] ∧ ar[n0] ≠ ⊥) ⊦ (∀ e0. e0 = e ∨ e0 ∈ set ↔ (∃ n0. n0 < # ar ∧ e0 = (ar[n := e])[n0] ∧ (ar[n := e])[n0] ≠ ⊥)) ↔ e ≠ ⊥

• Proof step 6:

  ar[n] = ⊥, e ≠ ⊥, n < # ar, ∀ e0. e0 ∈ set ↔ (∃ n0. n0 < # ar ∧ e0 = ar[n0] ∧ ar[n0] ≠ ⊥) ⊦ (∀ e0. e0 = e ∨ e0 ∈ set ↔ (∃ n0. n0 < # ar ∧ e0 = (ar[n := e])[n0] ∧ (ar[n := e])[n0] ≠ ⊥)) ↔ e ≠ ⊥

Rule argument

Additional information

Used formulas: e = ⊥

Proof step 4 from proof absset-addboth (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ar[n] = ⊥, n < # ar, ∀ e0. e0 ∈ set ↔ (∃ n0. n0 < # ar ∧ e0 = ar[n0] ∧ ar[n0] ≠ ⊥), ∀ e0. e0 = ⊥ ∨ e0 ∈ set ↔ (∃ n0. n0 < # ar ∧ e0 = ar[n0] ∧ ar[n0] ≠ ⊥) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ar[n] = a → ar[n := a] = ar; (s)

Proof step 5 from proof absset-addboth (previous step) (back to tree)

Heuristic quantifier applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: ar[n]

Proof step 6 from proof absset-addboth (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  ar[n] = ⊥, e ≠ ⊥, n < # ar, ∀ e0. e0 ∈ set ↔ (∃ n0. n0 < # ar ∧ e0 = ar[n0] ∧ ar[n0] ≠ ⊥) ⊦ e0 = e ∨ e0 ∈ set ↔ (∃ n0. n0 < # ar ∧ e0 = (ar[n := e])[n0] ∧ (ar[n := e])[n0] ≠ ⊥)

Rule argument

Additional information

Proof step 7 from proof absset-addboth (previous step) (back to tree)

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 8:

  ar[n] = ⊥, e0 = e, e ≠ ⊥, n < # ar, ∀ e0. e0 ∈ set ↔ (∃ n0. n0 < # ar ∧ e0 = ar[n0] ∧ ar[n0] ≠ ⊥) ⊦ e0 = e ∨ e0 ∈ set ↔ (∃ n0. n0 < # ar ∧ e0 = (ar[n := e])[n0] ∧ (ar[n := e])[n0] ≠ ⊥)

• Proof step 10:

  ar[n] = ⊥, e ≠ ⊥, e0 ≠ e, n < # ar, ∀ e0. e0 ∈ set ↔ (∃ n0. n0 < # ar ∧ e0 = ar[n0] ∧ ar[n0] ≠ ⊥) ⊦ e0 = e ∨ e0 ∈ set ↔ (∃ n0. n0 < # ar ∧ e0 = (ar[n := e])[n0] ∧ (ar[n := e])[n0] ≠ ⊥)

Rule argument

Additional information

Used formulas: e0 = e

Proof step 8 from proof absset-addboth (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  ar[n] = ⊥, e ≠ ⊥, n < # ar, ∀ e0. e0 ∈ set ↔ (∃ n0. n0 < # ar ∧ e0 = ar[n0] ∧ ar[n0] ≠ ⊥) ⊦ ∃ n0. n0 < # ar ∧ e = (ar[n := e])[n0] ∧ (ar[n := e])[n0] ≠ ⊥

Rule argument

Additional information

Proof step 9 from proof absset-addboth (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m < # ar → (ar[m := a])[m] = a; (s) Used terms: n

Proof step 10 from proof absset-addboth (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  ar[n] = ⊥, e ≠ ⊥, e0 ≠ e, n < # ar, ∀ e0. e0 ∈ set ↔ (∃ n0. n0 < # ar ∧ e0 = ar[n0] ∧ ar[n0] ≠ ⊥) ⊦ e0 ∈ set ↔ (∃ n0. n0 < # ar ∧ e0 = (ar[n := e])[n0] ∧ (ar[n := e])[n0] ≠ ⊥)

Rule argument

Additional information

Proof step 11 from proof absset-addboth (previous step) (back to tree)

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 12:

  ar[n] = ⊥, e ≠ ⊥, e0 ≠ e, n < # ar, e0 ∈ set, ∀ e0. e0 ∈ set ↔ (∃ n0. n0 < # ar ∧ e0 = ar[n0] ∧ ar[n0] ≠ ⊥) ⊦ e0 ∈ set ↔ (∃ n0. n0 < # ar ∧ e0 = (ar[n := e])[n0] ∧ (ar[n := e])[n0] ≠ ⊥)

• Proof step 20:

  ar[n] = ⊥, e ≠ ⊥, e0 ≠ e, n < # ar, ¬ e0 ∈ set, ∀ e0. e0 ∈ set ↔ (∃ n0. n0 < # ar ∧ e0 = ar[n0] ∧ ar[n0] ≠ ⊥) ⊦ e0 ∈ set ↔ (∃ n0. n0 < # ar ∧ e0 = (ar[n := e])[n0] ∧ (ar[n := e])[n0] ≠ ⊥)

Rule argument

Additional information

Used formulas: e0 ∈ set

Proof step 12 from proof absset-addboth (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  ar[n] = ⊥, # set ≠ 0, e ≠ ⊥, e0 ≠ e, set ≠ ∅, n < # ar, e0 ∈ set, ∀ e0. e0 ∈ set ↔ (∃ n0. n0 < # ar ∧ e0 = ar[n0] ∧ ar[n0] ≠ ⊥) ⊦ ∃ n0. n0 < # ar ∧ e0 = (ar[n := e])[n0] ∧ (ar[n := e])[n0] ≠ ⊥

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 13 from proof absset-addboth (previous step) (back to tree)

Heuristic quantifier applied rule all left

And obtained the following new goals

• Proof step 14:

  ar[n] = ⊥, # set ≠ 0, e ≠ ⊥, e0 ≠ e, set ≠ ∅, n < # ar, e0 ∈ set, e0 ∈ set ↔ (∃ n0. n0 < # ar ∧ e0 = ar[n0] ∧ ar[n0] ≠ ⊥), ∀ e0. e0 ∈ set ↔ (∃ n0. n0 < # ar ∧ e0 = ar[n0] ∧ ar[n0] ≠ ⊥) ⊦ ∃ n0. n0 < # ar ∧ e0 = (ar[n := e])[n0] ∧ (ar[n := e])[n0] ≠ ⊥

Rule argument

Additional information

Used terms: e0

Proof step 14 from proof absset-addboth (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  ar[n] = ⊥, # set ≠ 0, ar[n0] ≠ ⊥, ar[n0] ≠ e, e ≠ ⊥, set ≠ ∅, n0 < # ar, n < # ar, ar[n0] ∈ set, ∀ e0. e0 ∈ set ↔ (∃ n0. n0 < # ar ∧ e0 = ar[n0] ∧ ar[n0] ≠ ⊥) ⊦ ∃ n1. n1 < # ar ∧ ar[n0] = (ar[n := e])[n1] ∧ (ar[n := e])[n1] ≠ ⊥

Rule argument

Additional information

Proof step 15 from proof absset-addboth (previous step) (back to tree)

Heuristic quantifier applied rule all left

And obtained the following new goals

• Proof step 16:

  ar[n] = ⊥, # set ≠ 0, ar[n0] ≠ ⊥, ar[n0] ≠ e, e ≠ ⊥, set ≠ ∅, n < # ar, n0 < # ar, ar[n0] ∈ set, ar[n0] ∈ set ↔ (∃ n. n < # ar ∧ ar[n0] = ar[n] ∧ ar[n] ≠ ⊥), ∀ e0. e0 ∈ set ↔ (∃ n0. n0 < # ar ∧ e0 = ar[n0] ∧ ar[n0] ≠ ⊥) ⊦ ∃ n1. n1 < # ar ∧ ar[n0] = (ar[n := e])[n1] ∧ (ar[n := e])[n1] ≠ ⊥

Rule argument

Additional information

Used terms: ar[n0]

Proof step 16 from proof absset-addboth (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  ar[n0] = ar[n1], ar[n] = ⊥, # set ≠ 0, ar[n1] ≠ e, ar[n1] ≠ ⊥, e ≠ ⊥, set ≠ ∅, n1 < # ar, n < # ar, n0 < # ar, ar[n1] ∈ set, ∀ e0. e0 ∈ set ↔ (∃ n0. n0 < # ar ∧ e0 = ar[n0] ∧ ar[n0] ≠ ⊥) ⊦ ∃ n1. n1 < # ar ∧ ar[n0] = (ar[n := e])[n1] ∧ (ar[n := e])[n1] ≠ ⊥

Rule argument

Additional information

Proof step 17 from proof absset-addboth (previous step) (back to tree)

Heuristic quantifier applied rule exists right

And obtained the following new goals

• Proof step 18:

  ar[n] = ⊥, ar[n0] = ar[n1], # set ≠ 0, ar[n1] ≠ e, ar[n1] ≠ ⊥, e ≠ ⊥, set ≠ ∅, n0 < # ar, n < # ar, n1 < # ar, ar[n1] ∈ set, ∀ e0. e0 ∈ set ↔ (∃ n0. n0 < # ar ∧ e0 = ar[n0] ∧ ar[n0] ≠ ⊥) ⊦ ∃ n1. n1 < # ar ∧ ar[n0] = (ar[n := e])[n1] ∧ (ar[n := e])[n1] ≠ ⊥, n0 < # ar ∧ ar[n0] = (ar[n := e])[n0] ∧ (ar[n := e])[n0] ≠ ⊥

Rule argument

Additional information

Used terms: n0

Proof step 18 from proof absset-addboth (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  ar[n0] = ar[n1], ar[n] = ⊥, # set ≠ 0, ar[n1] ≠ e, ar[n1] ≠ ⊥, e ≠ ⊥, set ≠ ∅, n1 < # ar, n < # ar, n0 < # ar, ar[n1] ∈ set, ∀ e0. e0 ∈ set ↔ (∃ n0. n0 < # ar ∧ e0 = ar[n0] ∧ ar[n0] ≠ ⊥) ⊦ ∃ n1. n1 < # ar ∧ ar[n0] = (ar[n := e])[n1] ∧ (ar[n := e])[n1] ≠ ⊥, ar[n1] = (ar[n := e])[n0] ∧ (ar[n := e])[n0] ≠ ⊥

Rule argument

Additional information

Proof step 19 from proof absset-addboth (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m ≠ n → (ar[n := a])[m] = ar[m]; (s) ⊦ m < # ar → (ar[m := a])[m] = a; (s) Used formulas: n0 = n

Proof step 20 from proof absset-addboth (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  ar[n] = ⊥, (ar[n := e])[n0] ≠ ⊥, (ar[n := e])[n0] ≠ e, e ≠ ⊥, n0 < # ar, n < # ar, ¬ (ar[n := e])[n0] ∈ set, ∀ e0. e0 ∈ set ↔ (∃ n0. n0 < # ar ∧ e0 = ar[n0] ∧ ar[n0] ≠ ⊥) ⊦

Rule argument

Additional information

Proof step 21 from proof absset-addboth (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 22:

  ar[n] = ⊥, (ar[n := e])[n0] ≠ ⊥, (ar[n := e])[n0] ≠ e, e ≠ ⊥, n0 ≠ n, n < # ar, n0 < # ar, ¬ (ar[n := e])[n0] ∈ set, ∀ e0. e0 ∈ set ↔ (∃ n0. n0 < # ar ∧ e0 = ar[n0] ∧ ar[n0] ≠ ⊥) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < # ar → (ar[m := a])[m] = a; (s) Used formulas: n0 = n

Proof step 22 from proof absset-addboth (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  ar[n] = ⊥, ar[n0] ≠ ⊥, ar[n0] ≠ e, e ≠ ⊥, n0 ≠ n, n0 < # ar, n < # ar, ¬ ar[n0] ∈ set, ∀ e0. e0 ∈ set ↔ (∃ n0. n0 < # ar ∧ e0 = ar[n0] ∧ ar[n0] ≠ ⊥) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m ≠ n → (ar[n := a])[m] = ar[m]; (s)

Proof step 23 from proof absset-addboth (previous step) (back to tree)

Heuristic quantifier applied rule all left

And obtained the following new goals

• Proof step 24:

  ar[n] = ⊥, ar[n0] ≠ ⊥, ar[n0] ≠ e, e ≠ ⊥, n0 ≠ n, n < # ar, n0 < # ar, ¬ ar[n0] ∈ set, ar[n0] ∈ set ↔ (∃ n. n < # ar ∧ ar[n0] = ar[n] ∧ ar[n] ≠ ⊥), ∀ e0. e0 ∈ set ↔ (∃ n0. n0 < # ar ∧ e0 = ar[n0] ∧ ar[n0] ≠ ⊥) ⊦

Rule argument

Additional information

Used terms: ar[n0]

Proof step 24 from proof absset-addboth (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  ar[n] = ⊥, ar[n0] ≠ ⊥, ar[n0] ≠ e, e ≠ ⊥, n0 ≠ n, n0 < # ar, n < # ar, ¬ ar[n0] ∈ set, ∀ e0. e0 ∈ set ↔ (∃ n0. n0 < # ar ∧ e0 = ar[n0] ∧ ar[n0] ≠ ⊥) ⊦ ∃ n. n < # ar ∧ ar[n0] = ar[n] ∧ ar[n] ≠ ⊥

Rule argument

Additional information

Proof step 25 from proof absset-addboth (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: n0