Proof step 1 from proof expand-cons (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  σ ≠ [] ⊦ ∃ a, σ0. σ = ⌜a '⌝ + σ0

Rule argument

Additional information

Proof step 2 from proof expand-cons (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  σ ≠ [] ⊦ ∃ a, σ0. σ = ⌜a '⌝ + σ0

Rule argument

Additional information

Proof step 3 from proof expand-cons (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  ⌜x⌝ ≠ [] ⊦ ∃ a, σ0. ⌜x⌝ = ⌜a '⌝ + σ0

• Proof step 8:

  ⌜nf⌝ ≠ [] ⊦ ∃ a, σ0. ⌜nf⌝ = ⌜a '⌝ + σ0

Rule argument

Additional information

Used simplifier rules: stream freely generated by ⌜ ⌝, ⌜ ⌝;;

Proof step 4 from proof expand-cons (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  x ≠ [] ⊦ ∃ a, σ0. ⌜x⌝ = ⌜a '⌝ + σ0

Rule argument

Additional information

Used simplifier rules: fin-empty: ⊦ ⌜x⌝ = [] ↔ x = [];

Proof step 5 from proof expand-cons (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 6:

  a + x0 ≠ [], x0 ≠ [] → (∃ a, σ0. ⌜x0⌝ = ⌜a '⌝ + σ0) ⊦ ∃ a0, σ0. ⌜a + x0⌝ = ⌜a0 '⌝ + σ0

Rule argument

Additional information

Used simplifier rules: list freely generated by [], +;;

Proof step 6 from proof expand-cons (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  x0 ≠ [] → ⌜x0⌝ = ⌜a0 '⌝ + σ0 ⊦ ∃ a1, σ. ⌜a '⌝ + ⌜x0⌝ = ⌜a1 '⌝ + σ

Rule argument

Additional information

Used simplifier rules: append-finfin: ⊦ ⌜x + y⌝ = ⌜x⌝ + ⌜y⌝ ; a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a + x = a ' + x; (s) ⊦ a ' + x ≠ []; (s)

Proof step 7 from proof expand-cons (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: a, ⌜x0⌝

Proof step 8 from proof expand-cons (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  ⊦ ∃ a, σ0. ⌜nf⌝ = ⌜a '⌝ + σ0

Rule argument

Additional information

Used simplifier rules: fun-nonempty: ⊦ [] ≠ ⌜nf⌝ ;

Proof step 9 from proof expand-cons (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 10:

  ⌜nf⌝ ≠ ⌜nf(0) '⌝ + ⌜λ n. nf(n + 1)⌝ ⊦

Rule argument

Additional information

Used terms: nf(0), ⌜λ n. nf(n + 1)⌝

Proof step 10 from proof expand-cons (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

  ⊦ ⌜a '⌝ + ⌜nf⌝ = ⌜λ n. (n = 0 ⊃ a;nf(n -1))⌝

• Proof step 12:

  ⌜nf⌝ ≠ ⌜λ n. (n = 0 ⊃ nf(0);nf(n -1 + 1))⌝ ⊦

Rule argument

Additional information

Used terms: λ n. nf(n + 1), nf(0)

Proof step 11 from proof expand-cons (previous step) (back to tree)

Lemma one-inf

Proof step 12 from proof expand-cons (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  nf(n) ≠ (n = 0 ⊃ nf(0);nf((n - 1) + 1)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜nf⌝ = ⌜nf0⌝ ↔ nf = nf0; (s) ⊦ n -1 = n - 1; (s)

Proof step 13 from proof expand-cons (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 14:

  n ≠ 0, nf(n) ≠ nf((n - 1) + 1) ⊦

Rule argument

Additional information

Proof step 14 from proof expand-cons (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  n ≠ 0, nf(n) ≠ nf((n - 1) + 1) ⊦

Rule argument

Additional information

Proof step 15 from proof expand-cons (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

Used simplifier rules: n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: n, m