Proof step 1 from proof hpal-root (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  allreachable(g), finout(g), finroot(g), infgraph(g) ⊦ ∃ a. isroot(g)(a) ∧ haspathanylength(g)(a)

Rule argument

Additional information

Proof step 2 from proof hpal-root (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ finroot(g) ↔ (∃ s. ∀ a. isroot(g)(a) ↔ a ∈ s)

• Proof step 4:

  allreachable(g), finout(g), infgraph(g), ∃ s. ∀ a. isroot(g)(a) ↔ a ∈ s ⊦ ∃ a. isroot(g)(a) ∧ haspathanylength(g)(a)

Rule argument

Additional information

Used terms: g

Proof step 3 from proof hpal-root (previous step) (back to tree)

Lemma finroot-def

Proof step 4 from proof hpal-root (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ∀ a. isroot(g)(a) ↔ a ∈ s, ∀ s. ∃ a. dom(g)(a) ∧ ¬ a ∈ s, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ b. dom(g)(b) → (∃ a. isroot(g)(a) ∧ path(g)(a, b)) ⊦ ∃ a. isroot(g)(a) ∧ haspathanylength(g)(a)

Rule argument

Additional information

Used simplifier rules: infgraph-def: ⊦ infgraph(g) ↔ (∀ s. ∃ a. dom(g)(a) ∧ ¬ a ∈ s); finout-def: ⊦ finout(g) ↔ (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s); allreachable-def: ⊦ allreachable(g) ↔ (∀ b. dom(g)(b) → (∃ a. isroot(g)(a) ∧ path(g)(a, b)));

Proof step 5 from proof hpal-root (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 6:

  finout(g), ∀ a. a ∈ s → ¬ haspathanylength(g)(a) ⊦ ∃ s0. ∀ b. (∃ a. a ∈ s ∧ path(g)(a, b)) ↔ b ∈ s0

• Proof step 7:

  ∀ b. dom(g)(b) → (∃ a. isroot(g)(a) ∧ path(g)(a, b)), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s. ∃ a. dom(g)(a) ∧ ¬ a ∈ s, ∀ a. isroot(g)(a) ↔ a ∈ s ⊦ ∃ a. isroot(g)(a) ∧ haspathanylength(g)(a), finout(g) ∧ (∀ a. a ∈ s → ¬ haspathanylength(g)(a))

• Proof step 11:

  ∀ b. dom(g)(b) → (∃ a. isroot(g)(a) ∧ path(g)(a, b)), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s. ∃ a. dom(g)(a) ∧ ¬ a ∈ s, ∀ a. isroot(g)(a) ↔ a ∈ s, ∃ s0. ∀ b. (∃ a. a ∈ s ∧ path(g)(a, b)) ↔ b ∈ s0 ⊦ ∃ a. isroot(g)(a) ∧ haspathanylength(g)(a)

Rule argument

Additional information

Used terms: g, s

Proof step 6 from proof hpal-root (previous step) (back to tree)

Lemma hpal-reachset-set

Proof step 7 from proof hpal-root (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  # s ≠ 0, s ≠ ∅, haspathanylength(g)(a), a ∈ s, ∀ b. dom(g)(b) → (∃ a. isroot(g)(a) ∧ path(g)(a, b)), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s. ∃ a. dom(g)(a) ∧ ¬ a ∈ s, ∀ a. isroot(g)(a) ↔ a ∈ s ⊦ ∃ a. isroot(g)(a) ∧ haspathanylength(g)(a)

Rule argument

Additional information

Used simplifier rules: finout-def: ⊦ finout(g) ↔ (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s); size-zero-01: ⊦ s ≠ ∅ → # s ≠ 0; (forward) from specification set-basic ne-01: ⊦ a ∈ s → s ≠ ∅; (forward) from specification set-basic

Proof step 8 from proof hpal-root (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 9:

  # s ≠ 0, s ≠ ∅, haspathanylength(g)(a), a ∈ s, ∀ a. isroot(g)(a) ↔ a ∈ s, ∀ s. ∃ a. dom(g)(a) ∧ ¬ a ∈ s, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ b. dom(g)(b) → (∃ a. isroot(g)(a) ∧ path(g)(a, b)) ⊦ isroot(g)(a) ∧ haspathanylength(g)(a)

Rule argument

Additional information

Used terms: a

Proof step 9 from proof hpal-root (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  # s ≠ 0, s ≠ ∅, haspathanylength(g)(a), a ∈ s, ¬ isroot(g)(a), ∀ b. dom(g)(b) → (∃ a. isroot(g)(a) ∧ path(g)(a, b)), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ s. ∃ a. dom(g)(a) ∧ ¬ a ∈ s, ∀ a. isroot(g)(a) ↔ a ∈ s ⊦

Rule argument

Additional information

Proof step 10 from proof hpal-root (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: a

Proof step 11 from proof hpal-root (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  ∀ b. (∃ a. a ∈ s ∧ path(g)(a, b)) ↔ b ∈ s0, ∀ a. isroot(g)(a) ↔ a ∈ s, ∀ s. ∃ a. dom(g)(a) ∧ ¬ a ∈ s, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ b. dom(g)(b) → (∃ a. isroot(g)(a) ∧ path(g)(a, b)) ⊦ ∃ a. isroot(g)(a) ∧ haspathanylength(g)(a)

Rule argument

Additional information

Proof step 12 from proof hpal-root (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 13:

  ∀ b. dom(g)(b) → (∃ a. isroot(g)(a) ∧ path(g)(a, b)), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. isroot(g)(a) ↔ a ∈ s, ∀ b. (∃ a. a ∈ s ∧ path(g)(a, b)) ↔ b ∈ s0, ∃ a. dom(g)(a) ∧ ¬ a ∈ s0 ⊦ ∃ a. isroot(g)(a) ∧ haspathanylength(g)(a)

Rule argument

Additional information

Used terms: s0

Proof step 13 from proof hpal-root (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  dom(g)(a), ¬ a ∈ s0, ∀ b. (∃ a. a ∈ s ∧ path(g)(a, b)) ↔ b ∈ s0, ∀ a. isroot(g)(a) ↔ a ∈ s, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ b. dom(g)(b) → (∃ a. isroot(g)(a) ∧ path(g)(a, b)) ⊦ ∃ a. isroot(g)(a) ∧ haspathanylength(g)(a)

Rule argument

Additional information

Proof step 14 from proof hpal-root (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 15:

  dom(g)(a), ¬ a ∈ s0, (∃ a0. a0 ∈ s ∧ path(g)(a0, a)) ↔ a ∈ s0, ∀ b. dom(g)(b) → (∃ a. isroot(g)(a) ∧ path(g)(a, b)), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. isroot(g)(a) ↔ a ∈ s ⊦ ∃ a. isroot(g)(a) ∧ haspathanylength(g)(a)

Rule argument

Additional information

Used terms: a

Proof step 15 from proof hpal-root (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  dom(g)(a), ¬ a ∈ s0, ∀ a. isroot(g)(a) ↔ a ∈ s, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ b. dom(g)(b) → (∃ a. isroot(g)(a) ∧ path(g)(a, b)) ⊦ ∃ a. isroot(g)(a) ∧ haspathanylength(g)(a), ∃ a0. a0 ∈ s ∧ path(g)(a0, a)

Rule argument

Additional information

Proof step 16 from proof hpal-root (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 17:

  dom(g)(a), ¬ a ∈ s0, dom(g)(a) → (∃ a0. isroot(g)(a0) ∧ path(g)(a0, a)), ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s, ∀ a. isroot(g)(a) ↔ a ∈ s ⊦ ∃ a0. a0 ∈ s ∧ path(g)(a0, a), ∃ a. isroot(g)(a) ∧ haspathanylength(g)(a)

Rule argument

Additional information

Used terms: a

Proof step 17 from proof hpal-root (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  dom(g)(a), isroot(g)(a0), path(g)(a0, a), ¬ a ∈ s0, ∀ a. isroot(g)(a) ↔ a ∈ s, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s ⊦ ∃ a. isroot(g)(a) ∧ haspathanylength(g)(a), ∃ a0. a0 ∈ s ∧ path(g)(a0, a)

Rule argument

Additional information

Proof step 18 from proof hpal-root (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 19:

  isroot(g)(a0) ↔ a0 ∈ s, dom(g)(a), isroot(g)(a0), path(g)(a0, a), ¬ a ∈ s0, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s ⊦ ∃ a0. a0 ∈ s ∧ path(g)(a0, a), ∃ a. isroot(g)(a) ∧ haspathanylength(g)(a)

Rule argument

Additional information

Used terms: a0

Proof step 19 from proof hpal-root (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  # s ≠ 0, s ≠ ∅, dom(g)(a), isroot(g)(a0), path(g)(a0, a), a0 ∈ s, ¬ a ∈ s0, ∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s ⊦ ∃ a0. a0 ∈ s ∧ path(g)(a0, a), ∃ a. isroot(g)(a) ∧ haspathanylength(g)(a)

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 20 from proof hpal-root (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: a0