Proof step 1 from proof finset-nextfin (conclusion) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 2:

  ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s ⊦ ∃ s0. ∀ b. b ∈ s0 ↔ (∃ a. a ∈ s ∧ edge(g)(a, b))

Rule argument

Additional information

Used simplifier rules: finout-def: ⊦ finout(g) ↔ (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s);

Proof step 2 from proof finset-nextfin (previous step) (back to tree)

User applied rule induction

And obtained the following new goals

• Proof step 3:

  ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) → (∃ s1. ∀ b. b ∈ s1 ↔ (∃ a. a ∈ s0 ∧ edge(g)(a, b))) ⊦ ∃ s0. ∀ b. b ∈ s0 ↔ (∃ a. a ∈ s ∧ edge(g)(a, b))

Rule argument

Additional information

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

Proof step 3 from proof finset-nextfin (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 4:

  ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∃ a. a ∈ s, ∀ s0, g. # s0 < # s → (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) → (∃ s1. ∀ b. b ∈ s1 ↔ (∃ a. a ∈ s0 ∧ edge(g)(a, b))) ⊦ ∃ s0. ∀ b. b ∈ s0 ↔ (∃ a. a ∈ s ∧ edge(g)(a, b))

• Proof step 34:

  ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) → (∃ s1. ∀ b. b ∈ s1 ↔ (∃ a. a ∈ s0 ∧ edge(g)(a, b))) ⊦ ∃ s0. ∀ b. b ∈ s0 ↔ (∃ a. a ∈ s ∧ edge(g)(a, b)), ∃ a. a ∈ s

Rule argument

Additional information

Used formulas: ∃ a. a ∈ s

Proof step 4 from proof finset-nextfin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  # s ≠ 0, s ≠ ∅, a ∈ s, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) → (∃ s1. ∀ b. b ∈ s1 ↔ (∃ a. a ∈ s0 ∧ edge(g)(a, b))) ⊦ ∃ s0. ∀ b. b ∈ s0 ↔ (∃ a. a ∈ s ∧ edge(g)(a, b))

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 5 from proof finset-nextfin (previous step) (back to tree)

User applied rule apply induction

And obtained the following new goals

• Proof step 6:

  # s ≠ 0, s ≠ ∅, a ∈ s, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) → (∃ s1. ∀ b. b ∈ s1 ↔ (∃ a. a ∈ s0 ∧ edge(g)(a, b))) ⊦ ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∃ s0. ∀ b. b ∈ s0 ↔ (∃ a. a ∈ s ∧ edge(g)(a, b))

• Proof step 12:

  # s ≠ 0, s ≠ ∅, a ∈ s, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∃ s1. ∀ b. b ∈ s1 ↔ (∃ a0. a0 ∈ s -- a ∧ edge(g)(a0, b)), ∀ s0, g. # s0 < # s → (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) → (∃ s1. ∀ b. b ∈ s1 ↔ (∃ a. a ∈ s0 ∧ edge(g)(a, b))) ⊦ ∃ s0. ∀ b. b ∈ s0 ↔ (∃ a. a ∈ s ∧ edge(g)(a, b))

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ s → #(s -- a) = # s - 1; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m < 1 ↔ m = 0; (s) n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (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: s -- a, g

Proof step 6 from proof finset-nextfin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  # s ≠ 0, s ≠ ∅, a ∈ s, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) → (∃ s1. ∀ b. b ∈ s1 ↔ (∃ a. a ∈ s0 ∧ edge(g)(a, b))) ⊦ ∃ s0. ∀ b. b ∈ s0 ↔ (∃ a. a ∈ s ∧ edge(g)(a, b)), ∃ s. ∀ b. edge(g)(a0, b) ↔ b ∈ s

Rule argument

Additional information

Proof step 7 from proof finset-nextfin (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And obtained the following new goals

• Proof step 8:

  # s ≠ 0, s ≠ ∅, a ∈ s, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∃ s. ∀ b. edge(g)(a0, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) → (∃ s1. ∀ b. b ∈ s1 ↔ (∃ a. a ∈ s0 ∧ edge(g)(a, b))) ⊦ ∃ s. ∀ b. edge(g)(a0, b) ↔ b ∈ s, ∃ s0. ∀ b. b ∈ s0 ↔ (∃ a. a ∈ s ∧ edge(g)(a, b))

Rule argument

Additional information

Used terms: a0

Proof step 8 from proof finset-nextfin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  # s ≠ 0, s ≠ ∅, a ∈ s, ∀ b. edge(g)(a0, b) ↔ b ∈ s0, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) → (∃ s1. ∀ b. b ∈ s1 ↔ (∃ a. a ∈ s0 ∧ edge(g)(a, b))) ⊦ ∃ s0. ∀ b. b ∈ s0 ↔ (∃ a. a ∈ s ∧ edge(g)(a, b)), ∃ s. ∀ b. edge(g)(a0, b) ↔ b ∈ s

Rule argument

Additional information

Proof step 9 from proof finset-nextfin (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 10:

  # s ≠ 0, s ≠ ∅, a ∈ s, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ b. edge(g)(a0, b) ↔ b ∈ s0, ∀ s0, g. # s0 < # s → (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) → (∃ s1. ∀ b. b ∈ s1 ↔ (∃ a. a ∈ s0 ∧ edge(g)(a, b))) ⊦ ∀ b. edge(g)(a0, b) ↔ b ∈ s0, ∃ s0. ∀ b. b ∈ s0 ↔ (∃ a. a ∈ s ∧ edge(g)(a, b))

Rule argument

Additional information

Used terms: s0

Proof step 10 from proof finset-nextfin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  # s ≠ 0, ¬(edge(g)(a0, b) ↔ b ∈ s0), s ≠ ∅, a ∈ s, ∀ b. edge(g)(a0, b) ↔ b ∈ s0, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) → (∃ s1. ∀ b. b ∈ s1 ↔ (∃ a. a ∈ s0 ∧ edge(g)(a, b))) ⊦ ∃ s0. ∀ b. b ∈ s0 ↔ (∃ a. a ∈ s ∧ edge(g)(a, b))

Rule argument

Additional information

Proof step 11 from proof finset-nextfin (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: b

Proof step 12 from proof finset-nextfin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  # s ≠ 0, s ≠ ∅, a ∈ s, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ b. b ∈ s1 ↔ (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ edge(g)(a0, b)), ∀ s0, g. # s0 < # s → (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) → (∃ s1. ∀ b. b ∈ s1 ↔ (∃ a. a ∈ s0 ∧ edge(g)(a, b))) ⊦ ∃ s0. ∀ b. b ∈ s0 ↔ (∃ a. a ∈ s ∧ edge(g)(a, b))

Rule argument

Additional information

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

Proof step 13 from proof finset-nextfin (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 14:

  # s ≠ 0, s ≠ ∅, a ∈ s, ∀ b. b ∈ s1 ↔ (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ edge(g)(a0, b)), ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) → (∃ s1. ∀ b. b ∈ s1 ↔ (∃ a. a ∈ s0 ∧ edge(g)(a, b))) ⊦ ∃ s0. ∀ b. b ∈ s0 ↔ (∃ a. a ∈ s ∧ edge(g)(a, b))

Rule argument

Additional information

Used terms: a

Proof step 14 from proof finset-nextfin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  # s ≠ 0, s ≠ ∅, a ∈ s, ∀ b. edge(g)(a, b) ↔ b ∈ s0, ∀ b. b ∈ s1 ↔ (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ edge(g)(a0, b)), ∀ s0, g. # s0 < # s → (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) → (∃ s1. ∀ b. b ∈ s1 ↔ (∃ a. a ∈ s0 ∧ edge(g)(a, b))) ⊦ ∃ s0. ∀ b. b ∈ s0 ↔ (∃ a. a ∈ s ∧ edge(g)(a, b))

Rule argument

Additional information

Proof step 15 from proof finset-nextfin (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 16:

  # s ≠ 0, s ≠ ∅, a ∈ s, ∀ b. b ∈ s1 ↔ (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ edge(g)(a0, b)), ∀ b. edge(g)(a, b) ↔ b ∈ s0, ∀ s0, g. # s0 < # s → (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) → (∃ s1. ∀ b. b ∈ s1 ↔ (∃ a. a ∈ s0 ∧ edge(g)(a, b))) ⊦ ∀ b. b ∈ s1 ∪ s0 ↔ (∃ a. a ∈ s ∧ edge(g)(a, b))

Rule argument

Additional information

Used terms: s1 ∪ s0

Proof step 16 from proof finset-nextfin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  # s ≠ 0, s ≠ ∅, a ∈ s, ∀ b. edge(g)(a, b) ↔ b ∈ s0, ∀ b. b ∈ s1 ↔ (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ edge(g)(a0, b)), ∀ s0, g. # s0 < # s → (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) → (∃ s1. ∀ b. b ∈ s1 ↔ (∃ a. a ∈ s0 ∧ edge(g)(a, b))) ⊦ b ∈ s1 ∨ b ∈ s0 ↔ (∃ a. a ∈ s ∧ edge(g)(a, b))

Rule argument

Additional information

Used simplifier rules: unc: ⊦ s ∪ s0 = s0 ∪ s; from specification set-union una: ⊦ (s ∪ s0) ∪ s1 = s ∪ s0 ∪ s1; from specification set-union ⊦ a ∈ s1 ∪ s2 ↔ a ∈ s1 ∨ a ∈ s2; (s)

Proof step 17 from proof finset-nextfin (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 18:

  # s ≠ 0, s ≠ ∅, a ∈ s, ∀ b. b ∈ s1 ↔ (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ edge(g)(a0, b)), ∀ b. edge(g)(a, b) ↔ b ∈ s0, b ∈ s1 ∨ b ∈ s0, ∀ s0, g. # s0 < # s → (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) → (∃ s1. ∀ b. b ∈ s1 ↔ (∃ a. a ∈ s0 ∧ edge(g)(a, b))) ⊦ ∃ a. a ∈ s ∧ edge(g)(a, b)

• Proof step 28:

  # s ≠ 0, s ≠ ∅, a ∈ s, ¬ b ∈ s1, ¬ b ∈ s0, ∀ b. b ∈ s1 ↔ (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ edge(g)(a0, b)), ∀ b. edge(g)(a, b) ↔ b ∈ s0, ∃ a. a ∈ s ∧ edge(g)(a, b), ∀ s0, g. # s0 < # s → (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) → (∃ s1. ∀ b. b ∈ s1 ↔ (∃ a. a ∈ s0 ∧ edge(g)(a, b))) ⊦

Rule argument

Additional information

Proof step 18 from proof finset-nextfin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  # s ≠ 0, s ≠ ∅, a ∈ s, ∀ b. edge(g)(a, b) ↔ b ∈ s0, ∀ b. b ∈ s1 ↔ (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ edge(g)(a0, b)), b ∈ s1 ∨ b ∈ s0, ∀ s0, g. # s0 < # s → (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) → (∃ s1. ∀ b. b ∈ s1 ↔ (∃ a. a ∈ s0 ∧ edge(g)(a, b))) ⊦ ∃ a. a ∈ s ∧ edge(g)(a, b)

Rule argument

Additional information

Proof step 19 from proof finset-nextfin (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 20:

  # s ≠ 0, s ≠ ∅, a ∈ s, b ∈ s1, ∀ b. b ∈ s1 ↔ (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ edge(g)(a0, b)), ∀ b. edge(g)(a, b) ↔ b ∈ s0, ∀ s0, g. # s0 < # s → (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) → (∃ s1. ∀ b. b ∈ s1 ↔ (∃ a. a ∈ s0 ∧ edge(g)(a, b))) ⊦ ∃ a. a ∈ s ∧ edge(g)(a, b)

• Proof step 24:

  # s ≠ 0, s ≠ ∅, a ∈ s, b ∈ s0, ∀ b. b ∈ s1 ↔ (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ edge(g)(a0, b)), ∀ b. edge(g)(a, b) ↔ b ∈ s0, ∀ s0, g. # s0 < # s → (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) → (∃ s1. ∀ b. b ∈ s1 ↔ (∃ a. a ∈ s0 ∧ edge(g)(a, b))) ⊦ ∃ a. a ∈ s ∧ edge(g)(a, b)

Rule argument

Additional information

Proof step 20 from proof finset-nextfin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  # s ≠ 0, # s1 ≠ 0, s ≠ ∅, s1 ≠ ∅, a ∈ s, b ∈ s1, ∀ b. b ∈ s1 ↔ (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ edge(g)(a0, b)), ∀ b. edge(g)(a, b) ↔ b ∈ s0, ∀ s0, g. # s0 < # s → (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) → (∃ s1. ∀ b. b ∈ s1 ↔ (∃ a. a ∈ s0 ∧ edge(g)(a, b))) ⊦ ∃ a. a ∈ s ∧ edge(g)(a, b)

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 21 from proof finset-nextfin (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 22:

  # s ≠ 0, # s1 ≠ 0, s ≠ ∅, s1 ≠ ∅, b ∈ s1, a ∈ s, b ∈ s1 ↔ (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ edge(g)(a0, b)), ∀ b. edge(g)(a, b) ↔ b ∈ s0, ∀ s0, g. # s0 < # s → (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) → (∃ s1. ∀ b. b ∈ s1 ↔ (∃ a. a ∈ s0 ∧ edge(g)(a, b))) ⊦ ∃ a. a ∈ s ∧ edge(g)(a, b)

Rule argument

Additional information

Used terms: b

Proof step 22 from proof finset-nextfin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  # s ≠ 0, # s1 ≠ 0, a0 ≠ a, s ≠ ∅, s1 ≠ ∅, edge(g)(a0, b), a ∈ s, b ∈ s1, a0 ∈ s, ∀ b. edge(g)(a, b) ↔ b ∈ s0, ∀ s0, g. # s0 < # s → (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) → (∃ s1. ∀ b. b ∈ s1 ↔ (∃ a. a ∈ s0 ∧ edge(g)(a, b))) ⊦ ∃ a. a ∈ s ∧ edge(g)(a, b)

Rule argument

Additional information

Proof step 23 from proof finset-nextfin (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: a0

Proof step 24 from proof finset-nextfin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  # s ≠ 0, # s0 ≠ 0, s ≠ ∅, s0 ≠ ∅, a ∈ s, b ∈ s0, ∀ b. b ∈ s1 ↔ (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ edge(g)(a0, b)), ∀ b. edge(g)(a, b) ↔ b ∈ s0, ∀ s0, g. # s0 < # s → (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) → (∃ s1. ∀ b. b ∈ s1 ↔ (∃ a. a ∈ s0 ∧ edge(g)(a, b))) ⊦ ∃ a. a ∈ s ∧ edge(g)(a, b)

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 25 from proof finset-nextfin (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 26:

  edge(g)(a, b) ↔ b ∈ s0, # s ≠ 0, # s0 ≠ 0, s ≠ ∅, s0 ≠ ∅, b ∈ s0, a ∈ s, ∀ b. b ∈ s1 ↔ (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ edge(g)(a0, b)), ∀ s0, g. # s0 < # s → (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) → (∃ s1. ∀ b. b ∈ s1 ↔ (∃ a. a ∈ s0 ∧ edge(g)(a, b))) ⊦ ∃ a. a ∈ s ∧ edge(g)(a, b)

Rule argument

Additional information

Used terms: b

Proof step 26 from proof finset-nextfin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  # s ≠ 0, # s0 ≠ 0, s ≠ ∅, s0 ≠ ∅, edge(g)(a, b), a ∈ s, b ∈ s0, ∀ b. b ∈ s1 ↔ (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ edge(g)(a0, b)), ∀ s0, g. # s0 < # s → (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) → (∃ s1. ∀ b. b ∈ s1 ↔ (∃ a. a ∈ s0 ∧ edge(g)(a, b))) ⊦ ∃ a. a ∈ s ∧ edge(g)(a, b)

Rule argument

Additional information

Proof step 27 from proof finset-nextfin (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: a

Proof step 28 from proof finset-nextfin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  # s ≠ 0, s ≠ ∅, edge(g)(a0, b), a0 ∈ s, a ∈ s, ¬ b ∈ s1, ¬ b ∈ s0, ∀ b. edge(g)(a, b) ↔ b ∈ s0, ∀ b. b ∈ s1 ↔ (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ edge(g)(a0, b)), ∀ s0, g. # s0 < # s → (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) → (∃ s1. ∀ b. b ∈ s1 ↔ (∃ a. a ∈ s0 ∧ edge(g)(a, b))) ⊦

Rule argument

Additional information

Proof step 29 from proof finset-nextfin (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 30:

  # s ≠ 0, s ≠ ∅, edge(g)(a0, b), a ∈ s, a0 ∈ s, ¬ b ∈ s1, ¬ b ∈ s0, b ∈ s1 ↔ (∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ edge(g)(a0, b)), ∀ b. edge(g)(a, b) ↔ b ∈ s0, ∀ s0, g. # s0 < # s → (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) → (∃ s1. ∀ b. b ∈ s1 ↔ (∃ a. a ∈ s0 ∧ edge(g)(a, b))) ⊦

Rule argument

Additional information

Used terms: b

Proof step 30 from proof finset-nextfin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  # s ≠ 0, s ≠ ∅, edge(g)(a0, b), a0 ∈ s, a ∈ s, ¬ b ∈ s1, ¬ b ∈ s0, ∀ b. edge(g)(a, b) ↔ b ∈ s0, ∀ s0, g. # s0 < # s → (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) → (∃ s1. ∀ b. b ∈ s1 ↔ (∃ a. a ∈ s0 ∧ edge(g)(a, b))) ⊦ ∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ edge(g)(a0, b)

Rule argument

Additional information

Proof step 31 from proof finset-nextfin (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 32:

  # s ≠ 0, s ≠ ∅, edge(g)(a0, b), a ∈ s, a0 ∈ s, ¬ b ∈ s1, ¬ b ∈ s0, ∀ b. edge(g)(a, b) ↔ b ∈ s0, ∀ s0, g. # s0 < # s → (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) → (∃ s1. ∀ b. b ∈ s1 ↔ (∃ a. a ∈ s0 ∧ edge(g)(a, b))) ⊦ ∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ edge(g)(a0, b), a0 ≠ a ∧ a0 ∈ s ∧ edge(g)(a0, b)

Rule argument

Additional information

Used terms: a0

Proof step 32 from proof finset-nextfin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

  # s ≠ 0, s ≠ ∅, edge(g)(a, b), a ∈ s, ¬ b ∈ s0, ¬ b ∈ s1, ∀ b. edge(g)(a, b) ↔ b ∈ s0, ∀ s0, g. # s0 < # s → (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) → (∃ s1. ∀ b. b ∈ s1 ↔ (∃ a. a ∈ s0 ∧ edge(g)(a, b))) ⊦ ∃ a0. a0 ≠ a ∧ a0 ∈ s ∧ edge(g)(a0, b)

Rule argument

Additional information

Proof step 33 from proof finset-nextfin (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: b

Proof step 34 from proof finset-nextfin (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 35:

  ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) → (∃ s1. ∀ b. b ∈ s1 ↔ (∃ a. a ∈ s0 ∧ edge(g)(a, b))) ⊦ ∀ b. b ∈ ∅ ↔ (∃ a. a ∈ s ∧ edge(g)(a, b)), ∃ a. a ∈ s

Rule argument

Additional information

Used terms: ∅

Proof step 35 from proof finset-nextfin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 36:

  # s ≠ 0, s ≠ ∅, edge(g)(a, b), a ∈ s, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s0, g. # s0 < # s → (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s) → (∃ s1. ∀ b. b ∈ s1 ↔ (∃ a. a ∈ s0 ∧ edge(g)(a, b))) ⊦ ∃ a. a ∈ s

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 ⊦ ¬ a ∈ ∅; (s)

Proof step 36 from proof finset-nextfin (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: a