Proof step 1 from proof del-three (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  #(s -- a -- a0) = 0, 2 < # s ⊦

Rule argument

Additional information

Proof step 2 from proof del-three (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  s -- a = ∅ ++ a0, a ≠ a0, s ≠ ∅, s ≠ ∅ ++ a, 2 < # s, a0 ∈ s ⊦

Rule argument

Additional information

Used simplifier rules: del-e-02: ⊦ s -- a = ∅ ↔ s = ∅ ∨ s = ∅ ++ a; del-addeq-05: ⊦ (s ++ a) -- a = s -- a; del-e-01: ⊦ ∅ -- a = ∅; one-min: ⊦ s = ∅ ++ a → s -- a = ∅; del-feq: ⊦ s -- a = s0 ++ a0 → a ≠ a0 ∧ a0 ∈ s ∧ ¬ a ∈ s0; ⊦ #(∅ ++ a) = 1; (s) ne-01: ⊦ a ∈ s → s ≠ ∅; (forward) from specification set-basic ⊦ ¬ a ∈ ∅; (s) one-size: ⊦ s = ∅ ++ a → # s = 1; (forward) from specification set-basic ⊦ m < n → n ≠ 0; (s) ⊦ # ∅ = 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic size-zero-02: ⊦ # s = 0 → s = ∅; (forward) from specification set-basic

Proof step 3 from proof del-three (previous step) (back to tree)

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 4:

  s -- a = ∅ ++ a0, a ≠ a0, s ≠ ∅, s ≠ ∅ ++ a, 2 < # s, a0 ∈ s, a0 ∈ s -- a ⊦

Rule argument

Additional information

Used simplifier rules: del-in-01: ⊦ a ≠ a0 → (a ∈ s -- a0 ↔ a ∈ s); Used formulas: a0 ∈ s -- a

Proof step 4 from proof del-three (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  s -- a = ∅ ++ a0, a ≠ a0, s ≠ ∅, s ≠ ∅ ++ a, 2 < # s, a0 ∈ s ⊦

Rule argument

Additional information

Used simplifier rules: Delete: ⊦ a ∈ s -- a0 ↔ a ≠ a0 ∧ a ∈ s;

Proof step 5 from proof del-three (previous step) (back to tree)

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 6:

  s -- a = ∅ ++ a0, a ≠ a0, s ≠ ∅, s ≠ ∅ ++ a, 2 < # s, a0 ∈ s, a ∈ s ⊦

Rule argument

Additional information

Used simplifier rules: del-in: ⊦ ¬ a ∈ s → s -- a = s; one-size: ⊦ s = ∅ ++ a → # s = 1; (forward) from specification set-basic in-06: ⊦ a ∈ s ∧ s = ∅ ++ b → a = b; (forward) from specification set-basic ⊦ ∅ ≠ s ++ a; (s) ⊦ #(∅ ++ a) = 1; (s) Used formulas: a ∈ s

Proof step 6 from proof del-three (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  s -- a = ∅ ++ a0, a ≠ a0, s ≠ ∅, s ≠ ∅ ++ a, 2 < # s, a ∈ s, a0 ∈ s ⊦

Rule argument

Additional information

Proof step 7 from proof del-three (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

  ⊦ a ∈ s ↔ (∃ s0. s = s0 ++ a ∧ ¬ a ∈ s0)

Rule argument

Additional information

Used simplifier rules: del-addeq-04: ⊦ ¬ a ∈ s → (s ++ a) -- a = s; ⊦ ∅ ≠ s ++ a; (s) ⊦ ¬ a ∈ s → (s ++ a = ∅ ++ b ↔ a = b ∧ s = ∅); (s) ⊦ a ≠ b → (a ∈ s ++ b ↔ a ∈ s); (s) ⊦ ¬ a ∈ s → #(s ++ a) = # s + 1; (s) n0 < n ⊦ (* n) < m0 + (* n0) ↔ n - n0 < m0; (s) ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1); (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic one-size: ⊦ s = ∅ ++ a → # s = 1; (forward) from specification set-basic in-06: ⊦ a ∈ s ∧ s = ∅ ++ b → a = b; (forward) from specification set-basic ne-01: ⊦ a ∈ s → s ≠ ∅; (forward) from specification set-basic size-zero-01: ⊦ s ≠ ∅ → # s ≠ 0; (forward) from specification set-basic Used terms: a, s

Proof step 8 from proof del-three (previous step) (back to tree)

A spec-lemma