Proof step 1 from proof KoenigsLemma-aux (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  haspathanylength(g)(a), isroot(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 ')⌝ )

Rule argument

Additional information

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

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  haspathanylength(g)(a), isroot(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 ^ 0))(a ') = 0 + 1 ∧ haspathanylength(g)(((cf ^ 0))(a ').last) ∧ pathp(g)(⌜((cf ^ 0))(a ')⌝ )

• Proof step 9:

  haspathanylength(g)(a), isroot(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), ∀ g, a, cf. haspathanylength(g)(a) ∧ isroot(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 ^ n0))(a ') = n0 + 1 ∧ haspathanylength(g)(((cf ^ n0))(a ').last) ∧ pathp(g)(⌜((cf ^ n0))(a ')⌝ ) ⊦ # ((cf ^ n0 +1))(a ') = n0 +1 + 1 ∧ haspathanylength(g)(((cf ^ n0 +1))(a ').last) ∧ pathp(g)(⌜((cf ^ n0 +1))(a ')⌝ )

Rule argument

Additional information

Used simplifier rules: Nat freely generated by 0, +1;;

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  haspathanylength(g)(a), isroot(g)(a), ¬ pathp(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) ⊦

Rule argument

Additional information

Used simplifier rules: it-zero: ⊦ ((cf ^ 0))(x) = x; ⊦ a '.last = a; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ # a ' = 0 +1; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

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

• Proof step 6:

  haspathanylength(g)(a), isroot(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), (∃ n. ¬(⌜n⌝ < # ⌜a '⌝ → dom(g)(⌜a '⌝ [n]))) ∨ (∃ n. ¬(⌜n + 1⌝ < # ⌜a '⌝ → edge(g)(⌜a '⌝ [n], ⌜a '⌝ [n + 1]))) ⊦

Rule argument

Additional information

Used terms: g, ⌜a '⌝

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  haspathanylength(g)(a), isroot(g)(a), ¬ dom(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) ⊦

Rule argument

Additional information

Used simplifier rules: 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 < 0; (s) ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ m ≤ n → (⌜(* m)⌝ + n∞2 < ⌜(* n)⌝ ↔ n∞2 < ⌜n - m⌝ ); (s) ⊦ # a ' = 0 +1; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s) ⊦ a '[0] = a; (s) ⊦ ⌜x⌝ [n] = x[n]; (s) ⊦ m < 1 ↔ m = 0; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

  ⊦ isroot(g)(b) ↔ dom(g)(b) ∧ (∀ a. ¬ edge(g)(a, b))

Rule argument

Additional information

Used terms: g, a

Proof step 8 from proof KoenigsLemma-aux (previous step) (back to tree)

A spec-lemma

Proof step 9 from proof KoenigsLemma-aux (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), ∀ g, a, cf. haspathanylength(g)(a) ∧ isroot(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 ^ n0))(a ') = n0 + 1 ∧ haspathanylength(g)(((cf ^ n0))(a ').last) ∧ pathp(g)(⌜((cf ^ n0))(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(((cf ^ n0))(a ')) = 2 + n0 ∧ haspathanylength(g)(cf(((cf ^ n0))(a ')).last) ∧ pathp(g)(⌜cf(((cf ^ n0))(a '))⌝ )

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 ⊦ m +1 = m + 1; (s)

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

User applied rule all left

And obtained the following new goals

• Proof step 11:

  haspathanylength(g)(a), isroot(g)(a), haspathanylength(g)(a) ∧ isroot(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 ^ n0))(a ') = n0 + 1 ∧ haspathanylength(g)(((cf ^ n0))(a ').last) ∧ pathp(g)(⌜((cf ^ n0))(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(((cf ^ n0))(a ')) = 2 + n0 ∧ haspathanylength(g)(cf(((cf ^ n0))(a ')).last) ∧ pathp(g)(⌜cf(((cf ^ n0))(a '))⌝ )

Rule argument

Additional information

Used terms: g, a, cf

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  # ((cf ^ n0))(a ') = n0 + 1, haspathanylength(g)(a), haspathanylength(g)(((cf ^ n0))(a ').last), isroot(g)(a), pathp(g)(⌜((cf ^ n0))(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(((cf ^ n0))(a ')) = 2 + n0 ∧ haspathanylength(g)(cf(((cf ^ n0))(a ')).last) ∧ pathp(g)(⌜cf(((cf ^ n0))(a '))⌝ )

Rule argument

Additional information

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

User applied rule all left

And obtained the following new goals

• Proof step 13:

  # ((cf ^ n0))(a ') = n0 + 1, haspathanylength(g)(((cf ^ n0))(a ').last), haspathanylength(g)(a), isroot(g)(a), pathp(g)(⌜((cf ^ n0))(a ')⌝ ), ((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) ⊦ # cf(((cf ^ n0))(a ')) = 2 + n0 ∧ haspathanylength(g)(cf(((cf ^ n0))(a ')).last) ∧ pathp(g)(⌜cf(((cf ^ n0))(a '))⌝ )

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

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

Rule argument

Additional information

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

User applied rule case distinction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: in-15: ⊦ x + a ' = y → a ∈ y; (forward) from specification list ⊦ #(x + y) = # x + # y; (s) ⊦ # a ' = 0 +1; (s) a: ⊦ (x + y) + z = x + y + z; from specification list n < n0 ⊦ m + (* n) = m0 + (* n0) ↔ m = m0 + (n0 - n); (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ # [] = 0; (s) ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; (ws)