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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

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

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 ⊦ a ∈ s ++ b ↔ a = b ∨ a ∈ s; (s)

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

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 4:

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

• Proof step 6:

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

Rule argument

Additional information

Used formulas: ar[n] = ⊥

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

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

Rule argument

Additional information

Proof step 5 from proof absset-add (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-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

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

Rule argument

Additional information

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

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 8:

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

• Proof step 10:

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

Rule argument

Additional information

Used formulas: e = ar[n]

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

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

Rule argument

Additional information

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

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: n

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

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

Rule argument

Additional information

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

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 12:

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

• Proof step 14:

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

Rule argument

Additional information

Used formulas: e ∈ set

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  # set ≠ 0, ar[n] ≠ ⊥, e ≠ ar[n], set ≠ ∅, n < # ar, e ∈ set, ∀ e. e ∈ set ↔ (∃ n0. n0 < # ar ∧ e = ar[n0] ∧ ar[n0] ≠ ⊥) ⊦ ∃ n0. n0 < # ar ∧ e = ar[n0] ∧ ar[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-add (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: e

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

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

Rule argument

Additional information

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

Heuristic quantifier applied rule all left

And obtained the following new goals

• Proof step 16:

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

Rule argument

Additional information

Used terms: ar[n0]

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

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

Rule argument

Additional information

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

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: n0