Proof step 1 from proof KoenigsLemma (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) ⊦ ∃ nf. isroot(g)(nf(0)) ∧ pathp(g)(⌜nf⌝ )

Rule argument

Additional information

Proof step 2 from proof KoenigsLemma (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 3:

  finout(g) ⊦ ∀ x. x ≠ [] ∧ pathp(g)(⌜x⌝ ) ∧ haspathanylength(g)(x.last) → (∃ y. (∃ b. y = x + b ') ∧ pathp(g)(⌜y⌝ ) ∧ haspathanylength(g)(y.last))

• Proof step 4:

  allreachable(g), finout(g), finroot(g), infgraph(g), ∀ x. x ≠ [] ∧ pathp(g)(⌜x⌝ ) ∧ haspathanylength(g)(x.last) → (∃ y. (∃ b. y = x + b ') ∧ pathp(g)(⌜y⌝ ) ∧ haspathanylength(g)(y.last)) ⊦ ∃ nf. isroot(g)(nf(0)) ∧ pathp(g)(⌜nf⌝ )

Rule argument

Additional information

Used terms: g

Proof step 3 from proof KoenigsLemma (previous step) (back to tree)

Lemma hpal-next

Proof step 4 from proof KoenigsLemma (previous step) (back to tree)

User applied rule choice left

And obtained the following new goals

• Proof step 5:

  allreachable(g), finout(g), finroot(g), infgraph(g), ∀ x0. x0 ≠ [] ∧ pathp(g)(⌜x0⌝ ) ∧ haspathanylength(g)(x0.last) → (∃ b. cf(x0) = x0 + b ') ∧ pathp(g)(⌜cf(x0)⌝ ) ∧ haspathanylength(g)(cf(x0).last) ⊦ ∃ nf. isroot(g)(nf(0)) ∧ pathp(g)(⌜nf⌝ )

Rule argument

Additional information

Proof step 5 from proof KoenigsLemma (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 6:

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

• Proof step 7:

  allreachable(g), finout(g), finroot(g), infgraph(g), ∀ x0. x0 ≠ [] ∧ pathp(g)(⌜x0⌝ ) ∧ haspathanylength(g)(x0.last) → (∃ b. cf(x0) = x0 + b ') ∧ pathp(g)(⌜cf(x0)⌝ ) ∧ haspathanylength(g)(cf(x0).last), ∃ a. isroot(g)(a) ∧ haspathanylength(g)(a) ⊦ ∃ nf. isroot(g)(nf(0)) ∧ pathp(g)(⌜nf⌝ )

Rule argument

Additional information

Used terms: g

Proof step 6 from proof KoenigsLemma (previous step) (back to tree)

Lemma hpal-root

Proof step 7 from proof KoenigsLemma (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  haspathanylength(g)(a), isroot(g)(a), ∀ x0. x0 ≠ [] ∧ pathp(g)(⌜x0⌝ ) ∧ haspathanylength(g)(x0.last) → (∃ b. cf(x0) = x0 + b ') ∧ pathp(g)(⌜cf(x0)⌝ ) ∧ haspathanylength(g)(cf(x0).last), ∀ s. ∃ a. dom(g)(a) ∧ ¬ a ∈ s, ∀ 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)) ⊦ ∃ nf. isroot(g)(nf(0)) ∧ pathp(g)(⌜nf⌝ )

Rule argument

Additional information

Used simplifier rules: infgraph-def: ⊦ infgraph(g) ↔ (∀ s. ∃ a. dom(g)(a) ∧ ¬ a ∈ s); finroot-def: ⊦ finroot(g) ↔ (∃ s. ∀ a. isroot(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 8 from proof KoenigsLemma (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 9:

  haspathanylength(g)(a), isroot(g)(a), ∀ 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, ∀ s. ∃ a. dom(g)(a) ∧ ¬ a ∈ s, ∀ x0. x0 ≠ [] ∧ pathp(g)(⌜x0⌝ ) ∧ haspathanylength(g)(x0.last) → (∃ b. cf(x0) = x0 + b ') ∧ pathp(g)(⌜cf(x0)⌝ ) ∧ haspathanylength(g)(cf(x0).last) ⊦ isroot(g)(((cf ^ 0))(a ')[0]) ∧ pathp(g)(⌜λ n. ((cf ^ n))(a ')[n]⌝ )

Rule argument

Additional information

Used terms: λ n. ((cf ^ n))(a ')[n]

Proof step 9 from proof KoenigsLemma (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  haspathanylength(g)(a), isroot(g)(a), ¬ pathp(g)(⌜λ n. ((cf ^ n))(a ')[n]⌝ ), ∀ x0. x0 ≠ [] ∧ pathp(g)(⌜x0⌝ ) ∧ haspathanylength(g)(x0.last) → (∃ b. cf(x0) = x0 + b ') ∧ pathp(g)(⌜cf(x0)⌝ ) ∧ haspathanylength(g)(cf(x0).last), ∀ s. ∃ a. dom(g)(a) ∧ ¬ a ∈ s, ∀ 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)) ⊦

Rule argument

Additional information

Used simplifier rules: it-zero: ⊦ ((cf ^ 0))(x) = x; ⊦ a '[0] = a; (s)

Proof step 10 from proof KoenigsLemma (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

  ⊦ pathp(g)(σ) ↔ (∀ n. ⌜n⌝ < # σ → dom(g)(σ[n])) ∧ (∀ n. ⌜n + 1⌝ < # σ → edge(g)(σ[n], σ[n + 1]))

• Proof step 12:

  haspathanylength(g)(a), isroot(g)(a), ∀ 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, ∀ s. ∃ a. dom(g)(a) ∧ ¬ a ∈ s, ∀ x0. x0 ≠ [] ∧ pathp(g)(⌜x0⌝ ) ∧ haspathanylength(g)(x0.last) → (∃ b. cf(x0) = x0 + b ') ∧ pathp(g)(⌜cf(x0)⌝ ) ∧ haspathanylength(g)(cf(x0).last), (∃ n. ¬(⌜n⌝ < # ⌜λ n. ((cf ^ n))(a ')[n]⌝ → dom(g)(⌜λ n. ((cf ^ n))(a ')[n]⌝ [n]))) ∨ (∃ n. ¬(⌜n + 1⌝ < # ⌜λ n. ((cf ^ n))(a ')[n]⌝ → edge(g)(⌜λ n. ((cf ^ n))(a ')[n]⌝ [n], ⌜λ n. ((cf ^ n))(a ')[n]⌝ [n + 1]))) ⊦

Rule argument

Additional information

Used terms: ⌜λ n. ((cf ^ n))(a ')[n]⌝ , g

Proof step 11 from proof KoenigsLemma (previous step) (back to tree)

A spec-lemma

Proof step 12 from proof KoenigsLemma (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  haspathanylength(g)(a), isroot(g)(a), ∀ x0. x0 ≠ [] ∧ pathp(g)(⌜x0⌝ ) ∧ haspathanylength(g)(x0.last) → (∃ b. cf(x0) = x0 + b ') ∧ pathp(g)(⌜cf(x0)⌝ ) ∧ haspathanylength(g)(cf(x0).last), ∀ s. ∃ a. dom(g)(a) ∧ ¬ a ∈ s, ∀ 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)), ¬ dom(g)(((cf ^ n))(a ')[n]) ∨ ¬ edge(g)(((cf ^ n0))(a ')[n0], cf(((cf ^ n0))(a '))[n0 + 1]) ⊦

Rule argument

Additional information

Used simplifier rules: it-succ: ⊦ ((cf ^ (n + 1)))(x) = cf(((cf ^ n))(x)); c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ ⌜nf⌝ [n] = nf(n); (s) add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf ⊦ ⌜n⌝ ≠ ∞; (s) ⊦ ⌜m⌝ + n∞ = ∞ ↔ n∞ = ∞; (s) ⊦ n∞ < ∞ ↔ n∞ ≠ ∞; (s) ⊦ # ⌜nf⌝ = ∞; (s) ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s) ⊦ ⌜m⌝ < ∞; (s)

Proof step 13 from proof KoenigsLemma (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 14:

  haspathanylength(g)(a), isroot(g)(a), ¬ dom(g)(((cf ^ n))(a ')[n]), ∀ 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, ∀ s. ∃ a. dom(g)(a) ∧ ¬ a ∈ s, ∀ x0. x0 ≠ [] ∧ pathp(g)(⌜x0⌝ ) ∧ haspathanylength(g)(x0.last) → (∃ b. cf(x0) = x0 + b ') ∧ pathp(g)(⌜cf(x0)⌝ ) ∧ haspathanylength(g)(cf(x0).last) ⊦

• Proof step 24:

  haspathanylength(g)(a), isroot(g)(a), ¬ edge(g)(((cf ^ n0))(a ')[n0], cf(((cf ^ n0))(a '))[n0 + 1]), ∀ 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, ∀ s. ∃ a. dom(g)(a) ∧ ¬ a ∈ s, ∀ x0. x0 ≠ [] ∧ pathp(g)(⌜x0⌝ ) ∧ haspathanylength(g)(x0.last) → (∃ b. cf(x0) = x0 + b ') ∧ pathp(g)(⌜cf(x0)⌝ ) ∧ haspathanylength(g)(cf(x0).last) ⊦

Rule argument

Additional information

Proof step 14 from proof KoenigsLemma (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  haspathanylength(g)(a), isroot(g)(a), ¬ dom(g)(((cf ^ n))(a ')[n]), ∀ x0. x0 ≠ [] ∧ pathp(g)(⌜x0⌝ ) ∧ haspathanylength(g)(x0.last) → (∃ b. cf(x0) = x0 + b ') ∧ pathp(g)(⌜cf(x0)⌝ ) ∧ haspathanylength(g)(cf(x0).last), ∀ s. ∃ a. dom(g)(a) ∧ ¬ a ∈ s, ∀ 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)) ⊦

Rule argument

Additional information

Proof step 15 from proof KoenigsLemma (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 16:

  isroot(g)(a), haspathanylength(g)(a), ∀ x. x ≠ [] ∧ pathp(g)(⌜x⌝ ) ∧ haspathanylength(g)(x.last) → (∃ b. cf(x) = x + b ') ∧ pathp(g)(⌜cf(x)⌝ ) ∧ haspathanylength(g)(cf(x).last) ⊦ # ((cf ^ n))(a ') = n + 1 ∧ haspathanylength(g)(((cf ^ n))(a ').last) ∧ pathp(g)(⌜((cf ^ n))(a ')⌝ )

• Proof step 17:

  haspathanylength(g)(a), isroot(g)(a), ¬ dom(g)(((cf ^ n))(a ')[n]), ∀ 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, ∀ s. ∃ a. dom(g)(a) ∧ ¬ a ∈ s, ∀ x0. x0 ≠ [] ∧ pathp(g)(⌜x0⌝ ) ∧ haspathanylength(g)(x0.last) → (∃ b. cf(x0) = x0 + b ') ∧ pathp(g)(⌜cf(x0)⌝ ) ∧ haspathanylength(g)(cf(x0).last) ⊦ ∀ x. x ≠ [] ∧ pathp(g)(⌜x⌝ ) ∧ haspathanylength(g)(x.last) → (∃ b. cf(x) = x + b ') ∧ pathp(g)(⌜cf(x)⌝ ) ∧ haspathanylength(g)(cf(x).last)

• Proof step 19:

  # ((cf ^ n))(a ') = n + 1, haspathanylength(g)(a), haspathanylength(g)(((cf ^ n))(a ').last), isroot(g)(a), pathp(g)(⌜((cf ^ n))(a ')⌝ ), ¬ dom(g)(((cf ^ n))(a ')[n]), ∀ 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, ∀ s. ∃ a. dom(g)(a) ∧ ¬ a ∈ s, ∀ x0. x0 ≠ [] ∧ pathp(g)(⌜x0⌝ ) ∧ haspathanylength(g)(x0.last) → (∃ b. cf(x0) = x0 + b ') ∧ pathp(g)(⌜cf(x0)⌝ ) ∧ haspathanylength(g)(cf(x0).last) ⊦

Rule argument

Additional information

Used terms: g, a, cf, n

Proof step 16 from proof KoenigsLemma (previous step) (back to tree)

Lemma KoenigsLemma-aux

Proof step 17 from proof KoenigsLemma (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  x ≠ [], haspathanylength(g)(x.last), haspathanylength(g)(a), isroot(g)(a), pathp(g)(⌜x⌝ ), ¬ dom(g)(((cf ^ n))(a ')[n]), ∀ x0. x0 ≠ [] ∧ pathp(g)(⌜x0⌝ ) ∧ haspathanylength(g)(x0.last) → (∃ b. cf(x0) = x0 + b ') ∧ pathp(g)(⌜cf(x0)⌝ ) ∧ haspathanylength(g)(cf(x0).last), ∀ s. ∃ a. dom(g)(a) ∧ ¬ a ∈ s, ∀ 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)) ⊦ (∃ b. cf(x) = x + b ') ∧ pathp(g)(⌜cf(x)⌝ ) ∧ haspathanylength(g)(cf(x).last)

Rule argument

Additional information

Proof step 18 from proof KoenigsLemma (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: x

Proof step 19 from proof KoenigsLemma (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  # ((cf ^ n))(a ') = n + 1, haspathanylength(g)(((cf ^ n))(a ').last), haspathanylength(g)(a), isroot(g)(a), pathp(g)(⌜((cf ^ n))(a ')⌝ ), ¬ dom(g)(((cf ^ n))(a ')[n]), ∀ x0. x0 ≠ [] ∧ pathp(g)(⌜x0⌝ ) ∧ haspathanylength(g)(x0.last) → (∃ b. cf(x0) = x0 + b ') ∧ pathp(g)(⌜cf(x0)⌝ ) ∧ haspathanylength(g)(cf(x0).last), ∀ s. ∃ a. dom(g)(a) ∧ ¬ a ∈ s, ∀ 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)) ⊦

Rule argument

Additional information

Proof step 20 from proof KoenigsLemma (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

  ⊦ pathp(g)(σ) ↔ (∀ n. ⌜n⌝ < # σ → dom(g)(σ[n])) ∧ (∀ n. ⌜n + 1⌝ < # σ → edge(g)(σ[n], σ[n + 1]))

• Proof step 22:

  # ((cf ^ n))(a ') = n + 1, haspathanylength(g)(a), haspathanylength(g)(((cf ^ n))(a ').last), isroot(g)(a), ¬ dom(g)(((cf ^ n))(a ')[n]), ∀ 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, ∀ s. ∃ a. dom(g)(a) ∧ ¬ a ∈ s, ∀ x0. x0 ≠ [] ∧ pathp(g)(⌜x0⌝ ) ∧ haspathanylength(g)(x0.last) → (∃ b. cf(x0) = x0 + b ') ∧ pathp(g)(⌜cf(x0)⌝ ) ∧ haspathanylength(g)(cf(x0).last), ∀ n0. ⌜n0⌝ < # ⌜((cf ^ n))(a ')⌝ → dom(g)(⌜((cf ^ n))(a ')⌝ [n0]), ∀ n0. ⌜n0 + 1⌝ < # ⌜((cf ^ n))(a ')⌝ → edge(g)(⌜((cf ^ n))(a ')⌝ [n0], ⌜((cf ^ n))(a ')⌝ [n0 + 1]) ⊦

Rule argument

Additional information

Used terms: ⌜((cf ^ n))(a ')⌝ , g

Proof step 21 from proof KoenigsLemma (previous step) (back to tree)

A spec-lemma

Proof step 22 from proof KoenigsLemma (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  # ((cf ^ n))(a ') = n + 1, haspathanylength(g)(a), haspathanylength(g)(((cf ^ n))(a ').last), isroot(g)(a), ¬ dom(g)(((cf ^ n))(a ')[n]), ∀ 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, ∀ s. ∃ a. dom(g)(a) ∧ ¬ a ∈ s, ∀ x0. x0 ≠ [] ∧ pathp(g)(⌜x0⌝ ) ∧ haspathanylength(g)(x0.last) → (∃ b. cf(x0) = x0 + b ') ∧ pathp(g)(⌜cf(x0)⌝ ) ∧ haspathanylength(g)(cf(x0).last), ∀ n0. ¬ n < n0 → dom(g)(((cf ^ n))(a ')[n0]), ∀ n0. n0 < n → edge(g)(((cf ^ n))(a ')[n0], ((cf ^ n))(a ')[n0 + 1]) ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ ⌜x⌝ [n] = x[n]; (s) ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf ⊦ ⌜n⌝ + ⌜m⌝ < ⌜n0⌝ ↔ n + m < n0; (s) ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s)

Proof step 23 from proof KoenigsLemma (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ n < n; (s) Used terms: n

Proof step 24 from proof KoenigsLemma (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  haspathanylength(g)(a), isroot(g)(a), ¬ edge(g)(((cf ^ n0))(a ')[n0], cf(((cf ^ n0))(a '))[n0 + 1]), ∀ x0. x0 ≠ [] ∧ pathp(g)(⌜x0⌝ ) ∧ haspathanylength(g)(x0.last) → (∃ b. cf(x0) = x0 + b ') ∧ pathp(g)(⌜cf(x0)⌝ ) ∧ haspathanylength(g)(cf(x0).last), ∀ s. ∃ a. dom(g)(a) ∧ ¬ a ∈ s, ∀ 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)) ⊦

Rule argument

Additional information

Proof step 25 from proof KoenigsLemma (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 26:

  isroot(g)(a), haspathanylength(g)(a), ∀ x. x ≠ [] ∧ pathp(g)(⌜x⌝ ) ∧ haspathanylength(g)(x.last) → (∃ b. cf(x) = x + b ') ∧ pathp(g)(⌜cf(x)⌝ ) ∧ haspathanylength(g)(cf(x).last) ⊦ # ((cf ^ n))(a ') = n + 1 ∧ haspathanylength(g)(((cf ^ n))(a ').last) ∧ pathp(g)(⌜((cf ^ n))(a ')⌝ )

• Proof step 27:

  haspathanylength(g)(a), isroot(g)(a), ¬ edge(g)(((cf ^ n0))(a ')[n0], cf(((cf ^ n0))(a '))[n0 + 1]), ∀ 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, ∀ s. ∃ a. dom(g)(a) ∧ ¬ a ∈ s, ∀ x0. x0 ≠ [] ∧ pathp(g)(⌜x0⌝ ) ∧ haspathanylength(g)(x0.last) → (∃ b. cf(x0) = x0 + b ') ∧ pathp(g)(⌜cf(x0)⌝ ) ∧ haspathanylength(g)(cf(x0).last) ⊦ ∀ x. x ≠ [] ∧ pathp(g)(⌜x⌝ ) ∧ haspathanylength(g)(x.last) → (∃ b. cf(x) = x + b ') ∧ pathp(g)(⌜cf(x)⌝ ) ∧ haspathanylength(g)(cf(x).last)

• Proof step 29:

  # ((cf ^ n0))(a ') = n0 + 1, haspathanylength(g)(a), haspathanylength(g)(((cf ^ n0))(a ').last), isroot(g)(a), pathp(g)(⌜((cf ^ n0))(a ')⌝ ), ¬ edge(g)(((cf ^ n0))(a ')[n0], cf(((cf ^ n0))(a '))[n0 + 1]), ∀ 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, ∀ s. ∃ a. dom(g)(a) ∧ ¬ a ∈ s, ∀ x0. x0 ≠ [] ∧ pathp(g)(⌜x0⌝ ) ∧ haspathanylength(g)(x0.last) → (∃ b. cf(x0) = x0 + b ') ∧ pathp(g)(⌜cf(x0)⌝ ) ∧ haspathanylength(g)(cf(x0).last) ⊦

Rule argument

Additional information

Used terms: g, a, cf, n0

Proof step 26 from proof KoenigsLemma (previous step) (back to tree)

Lemma KoenigsLemma-aux

Proof step 27 from proof KoenigsLemma (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  x ≠ [], haspathanylength(g)(x.last), haspathanylength(g)(a), isroot(g)(a), pathp(g)(⌜x⌝ ), ¬ edge(g)(((cf ^ n0))(a ')[n0], cf(((cf ^ n0))(a '))[n0 + 1]), ∀ x0. x0 ≠ [] ∧ pathp(g)(⌜x0⌝ ) ∧ haspathanylength(g)(x0.last) → (∃ b. cf(x0) = x0 + b ') ∧ pathp(g)(⌜cf(x0)⌝ ) ∧ haspathanylength(g)(cf(x0).last), ∀ s. ∃ a. dom(g)(a) ∧ ¬ a ∈ s, ∀ 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)) ⊦ (∃ b. cf(x) = x + b ') ∧ pathp(g)(⌜cf(x)⌝ ) ∧ haspathanylength(g)(cf(x).last)

Rule argument

Additional information

Proof step 28 from proof KoenigsLemma (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: x

Proof step 29 from proof KoenigsLemma (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

  # ((cf ^ n0))(a ') = n0 + 1, haspathanylength(g)(((cf ^ n0))(a ').last), haspathanylength(g)(a), isroot(g)(a), pathp(g)(⌜((cf ^ n0))(a ')⌝ ), ¬ edge(g)(((cf ^ n0))(a ')[n0], cf(((cf ^ n0))(a '))[n0 + 1]), ∀ x0. x0 ≠ [] ∧ pathp(g)(⌜x0⌝ ) ∧ haspathanylength(g)(x0.last) → (∃ b. cf(x0) = x0 + b ') ∧ pathp(g)(⌜cf(x0)⌝ ) ∧ haspathanylength(g)(cf(x0).last), ∀ s. ∃ a. dom(g)(a) ∧ ¬ a ∈ s, ∀ 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)) ⊦

Rule argument

Additional information

Proof step 30 from proof KoenigsLemma (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 31:

  # ((cf ^ n0))(a ') = n0 + 1, haspathanylength(g)(a), haspathanylength(g)(((cf ^ n0))(a ').last), isroot(g)(a), pathp(g)(⌜((cf ^ n0))(a ')⌝ ), ¬ edge(g)(((cf ^ n0))(a ')[n0], cf(((cf ^ n0))(a '))[n0 + 1]), ((cf ^ n0))(a ') ≠ [] ∧ pathp(g)(⌜((cf ^ n0))(a ')⌝ ) ∧ haspathanylength(g)(((cf ^ n0))(a ').last) → (∃ b. cf(((cf ^ n0))(a ')) = ((cf ^ n0))(a ') + b ') ∧ pathp(g)(⌜cf(((cf ^ n0))(a '))⌝ ) ∧ haspathanylength(g)(cf(((cf ^ n0))(a ')).last), ∀ 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, ∀ s. ∃ a. dom(g)(a) ∧ ¬ a ∈ s ⊦

Rule argument

Additional information

Used terms: ((cf ^ n0))(a ')

Proof step 31 from proof KoenigsLemma (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

  # ((cf ^ n0))(a ') = n0 + 1, haspathanylength(g)(((cf ^ n0))(a ').last), haspathanylength(g)(a), isroot(g)(a), pathp(g)(⌜((cf ^ n0))(a ')⌝ ), ¬ edge(g)(((cf ^ n0))(a ')[n0], cf(((cf ^ n0))(a '))[n0 + 1]), ((cf ^ n0))(a ') ≠ [] → cf(((cf ^ n0))(a ')) = ((cf ^ n0))(a ') + b ' ∧ pathp(g)(⌜cf(((cf ^ n0))(a '))⌝ ) ∧ haspathanylength(g)(cf(((cf ^ n0))(a ')).last), ∀ s. ∃ a. dom(g)(a) ∧ ¬ a ∈ s, ∀ 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)) ⊦

Rule argument

Additional information

Proof step 32 from proof KoenigsLemma (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 33:

  # ((cf ^ n0))(a ') = n0 + 1, cf(((cf ^ n0))(a ')) = ((cf ^ n0))(a ') + b ', haspathanylength(g)(a), haspathanylength(g)(((cf ^ n0))(a ').last), haspathanylength(g)(cf(((cf ^ n0))(a ')).last), isroot(g)(a), pathp(g)(⌜((cf ^ n0))(a ')⌝ ), pathp(g)(⌜cf(((cf ^ n0))(a '))⌝ ), ¬ edge(g)(((cf ^ n0))(a ')[n0], cf(((cf ^ n0))(a '))[n0 + 1]), ∀ 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, ∀ s. ∃ a. dom(g)(a) ∧ ¬ a ∈ s ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # [] = 0; (s) ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; (ws) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic

Proof step 33 from proof KoenigsLemma (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  # ((cf ^ n0))(a ') = n0 + 1, cf(((cf ^ n0))(a ')) = ((cf ^ n0))(a ') + b ', haspathanylength(g)(b), haspathanylength(g)(((cf ^ n0))(a ').last), haspathanylength(g)(a), isroot(g)(a), pathp(g)(⌜((cf ^ n0))(a ')⌝ + ⌜b '⌝ ), pathp(g)(⌜((cf ^ n0))(a ')⌝ ), ¬ edge(g)(((cf ^ n0))(a ')[n0], b), ∀ s. ∃ a. dom(g)(a) ∧ ¬ a ∈ s, ∀ 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)) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ n = # x → (x + a ')[n] = a; (s) ⊦ ⌜x + y⌝ = ⌜x⌝ + ⌜y⌝ ; (s) ⊦ (x + a ').last = a; (s) in-15: ⊦ x + a ' = y → a ∈ y; (forward) from specification list

Proof step 34 from proof KoenigsLemma (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 35:

  ⊦ pathp(g)(σ) ↔ (∀ n. ⌜n⌝ < # σ → dom(g)(σ[n])) ∧ (∀ n. ⌜n + 1⌝ < # σ → edge(g)(σ[n], σ[n + 1]))

• Proof step 36:

  # ((cf ^ n0))(a ') = n0 + 1, cf(((cf ^ n0))(a ')) = ((cf ^ n0))(a ') + b ', haspathanylength(g)(a), haspathanylength(g)(((cf ^ n0))(a ').last), haspathanylength(g)(b), isroot(g)(a), pathp(g)(⌜((cf ^ n0))(a ')⌝ ), ¬ edge(g)(((cf ^ n0))(a ')[n0], b), ∀ 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, ∀ s. ∃ a. dom(g)(a) ∧ ¬ a ∈ s, ∀ n. ⌜n⌝ < #(⌜((cf ^ n0))(a ')⌝ + ⌜b '⌝ ) → dom(g)((⌜((cf ^ n0))(a ')⌝ + ⌜b '⌝ )[n]), ∀ n. ⌜n + 1⌝ < #(⌜((cf ^ n0))(a ')⌝ + ⌜b '⌝ ) → edge(g)((⌜((cf ^ n0))(a ')⌝ + ⌜b '⌝ )[n], (⌜((cf ^ n0))(a ')⌝ + ⌜b '⌝ )[n + 1]) ⊦

Rule argument

Additional information

Used terms: ⌜((cf ^ n0))(a ')⌝ + ⌜b '⌝ , g

Proof step 35 from proof KoenigsLemma (previous step) (back to tree)

A spec-lemma

Proof step 36 from proof KoenigsLemma (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 37:

  # ((cf ^ n0))(a ') = n0 + 1, cf(((cf ^ n0))(a ')) = ((cf ^ n0))(a ') + b ', haspathanylength(g)(a), haspathanylength(g)(((cf ^ n0))(a ').last), haspathanylength(g)(b), isroot(g)(a), pathp(g)(⌜((cf ^ n0))(a ')⌝ ), ¬ edge(g)(((cf ^ n0))(a ')[n0], b), ∀ n. ¬ n0 + 1 < n → dom(g)((((cf ^ n0))(a ') + b ')[n]), ∀ 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, ∀ s. ∃ a. dom(g)(a) ∧ ¬ a ∈ s, ∀ n. ¬ n0 < n → edge(g)(((cf ^ n0))(a ')[n], (((cf ^ n0))(a ') + b ')[n + 1]) ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m < n + 1 ↔ ¬ n < m; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ (⌜x⌝ + ⌜x0⌝ )[m] = (x + x0)[m]; (s) add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ ⌜n⌝ < ⌜1⌝ + n∞ ↔ ¬ n∞ < ⌜n⌝ ; (s) ⊦ # a ' = 0 +1; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ #(σ + σ1) = # σ + # σ1; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ n < # x → (x + a ')[n] = x[n]; (s) ⊦ n∞ + ⌜0⌝ = n∞; (s) ⊦ m ≤ n → (⌜(* m)⌝ + n∞2 < ⌜(* n)⌝ + n∞1 ↔ n∞2 < ⌜n - m⌝ + n∞1); (s) ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s)

Proof step 37 from proof KoenigsLemma (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ n < n; (s) ⊦ n = # x → (x + a ')[n] = a; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: n0