Proof step 1 from proof append-assoc (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  (σ + σ1) + σ2 ≠ σ + σ1 + σ2 ⊦

Rule argument

Additional information

Proof step 2 from proof append-assoc (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  (⌜x⌝ + σ1) + σ2 ≠ ⌜x⌝ + σ1 + σ2 ⊦

Rule argument

Additional information

Used simplifier rules: append-inf: ⊦ ⌜nf⌝ + σ = ⌜nf⌝ ; stream('a) freely generated by ⌜ ⌝, ⌜ ⌝;; ⊦ ⌜nf⌝ = ⌜nf0⌝ ↔ nf = nf0; (s)

Proof step 3 from proof append-assoc (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  (⌜x⌝ + ⌜x0⌝ ) + σ2 ≠ ⌜x⌝ + ⌜x0⌝ + σ2 ⊦

• Proof step 25:

  (⌜x⌝ + ⌜nf⌝ ) + σ2 ≠ ⌜x⌝ + ⌜nf⌝ + σ2 ⊦

Rule argument

Additional information

Used simplifier rules: stream('a) freely generated by ⌜ ⌝, ⌜ ⌝;;

Proof step 4 from proof append-assoc (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 5:

  (⌜x⌝ + ⌜x0⌝ ) + ⌜x1⌝ ≠ ⌜x⌝ + ⌜x0⌝ + ⌜x1⌝ ⊦

• Proof step 9:

  (⌜x⌝ + ⌜x0⌝ ) + ⌜nf⌝ ≠ ⌜x⌝ + ⌜x0⌝ + ⌜nf⌝ ⊦

Rule argument

Additional information

Used simplifier rules: stream('a) freely generated by ⌜ ⌝, ⌜ ⌝;;

Proof step 5 from proof append-assoc (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ ⌜x + y⌝ = ⌜x⌝ + ⌜y⌝

• Proof step 7:

  ⌜x + x0⌝ + ⌜x1⌝ ≠ ⌜x⌝ + ⌜x0⌝ + ⌜x1⌝ ⊦

Rule argument

Additional information

Used terms: x0, x

Proof step 6 from proof append-assoc (previous step) (back to tree)

Lemma append-finfin

Proof step 7 from proof append-assoc (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

  ⊦ ⌜x + y⌝ = ⌜x⌝ + ⌜y⌝

Rule argument

Additional information

Used simplifier rules: append-finfin: ⊦ ⌜x + y⌝ = ⌜x⌝ + ⌜y⌝ ; eq-stream-to-list-3-3: ⊦ ⌜x1⌝ + ⌜x⌝ + ⌜y⌝ = ⌜x2⌝ + ⌜x0⌝ + ⌜z⌝ ↔ x1 + x + y = x2 + x0 + z; a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: x1, x + x0

Proof step 8 from proof append-assoc (previous step) (back to tree)

Lemma append-finfin

Proof step 9 from proof append-assoc (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ ⌜x⌝ + ⌜nf⌝ = ⌜λ n. (n < # x ⊃ x[n];nf(n - # x))⌝

• Proof step 11:

  (⌜x⌝ + ⌜x0⌝ ) + ⌜nf⌝ ≠ ⌜x⌝ + ⌜λ n. (n < # x0 ⊃ x0[n];nf(n - # x0))⌝ ⊦

Rule argument

Additional information

Used terms: nf, x0

Proof step 10 from proof append-assoc (previous step) (back to tree)

Lemma append-fininf

Proof step 11 from proof append-assoc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  (⌜x⌝ + ⌜x0⌝ ) + ⌜nf⌝ ≠ ⌜x⌝ + ⌜λ n. (n < # x0 ⊃ x0[n];nf(n - # x0))⌝ ⊦

Rule argument

Additional information

Proof step 12 from proof append-assoc (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

  ⊦ ⌜x⌝ + ⌜nf⌝ = ⌜λ n. (n < # x ⊃ x[n];nf(n - # x))⌝

• Proof step 14:

  (⌜x⌝ + ⌜x0⌝ ) + ⌜nf⌝ ≠ ⌜λ n. (n < # x ⊃ x[n];(n - # x < # x0 ⊃ x0[n - # x];nf(n - # x - # x0)))⌝ ⊦

Rule argument

Additional information

Used terms: λ n. (n < # x0 ⊃ x0[n];nf(n - # x0)), x

Proof step 13 from proof append-assoc (previous step) (back to tree)

Lemma append-fininf

Proof step 14 from proof append-assoc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  (⌜x⌝ + ⌜x0⌝ ) + ⌜nf⌝ ≠ ⌜λ n. (n < # x ⊃ x[n];(n < # x0 + # x ⊃ x0[n - # x];nf(n - # x - # x0)))⌝ ⊦

Rule argument

Additional information

Used simplifier rules: n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss)

Proof step 15 from proof append-assoc (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

  ⊦ ⌜x + y⌝ = ⌜x⌝ + ⌜y⌝

• Proof step 17:

  ⌜x + x0⌝ + ⌜nf⌝ ≠ ⌜λ n. (n < # x ⊃ x[n];(n < # x0 + # x ⊃ x0[n - # x];nf(n - # x - # x0)))⌝ ⊦

Rule argument

Additional information

Used terms: x0, x

Proof step 16 from proof append-assoc (previous step) (back to tree)

Lemma append-finfin

Proof step 17 from proof append-assoc (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 18:

  ⊦ ⌜x⌝ + ⌜nf⌝ = ⌜λ n. (n < # x ⊃ x[n];nf(n - # x))⌝

• Proof step 19:

  ⌜λ n. (n < #(x + x0) ⊃ (x + x0)[n];nf(n - #(x + x0)))⌝ ≠ ⌜λ n. (n < # x ⊃ x[n];(n < # x0 + # x ⊃ x0[n - # x];nf(n - # x - # x0)))⌝ ⊦

Rule argument

Additional information

Used terms: nf, x + x0

Proof step 18 from proof append-assoc (previous step) (back to tree)

Lemma append-fininf

Proof step 19 from proof append-assoc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  (n < # x + # x0 ⊃ (x + x0)[n];nf(n - # x + # x0)) ≠ (n < # x ⊃ x[n];(n < # x0 + # x ⊃ x0[n - # x];nf(n - # x - # x0))) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜nf⌝ = ⌜nf0⌝ ↔ nf = nf0; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ #(x + y) = # x + # y; (s)

Proof step 20 from proof append-assoc (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 21:

  (x + x0)[n] ≠ (n < # x ⊃ x[n];(n < # x0 + # x ⊃ x0[n - # x];nf(n - # x - # x0))), n < # x + # x0 ⊦

• Proof step 23:

  nf(n - # x + # x0) ≠ (n < # x ⊃ x[n];(n < # x0 + # x ⊃ x0[n - # x];nf(n - # x - # x0))), ¬ n < # x + # x0 ⊦

Rule argument

Additional information

Proof step 21 from proof append-assoc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  (x + x0)[n] ≠ (n < # x ⊃ x[n];x0[n - # x]), n < # x + # x0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic

Proof step 22 from proof append-assoc (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And closed the goal!

Rule argument

Additional information

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

Proof step 23 from proof append-assoc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  nf(n - # x + # x0) ≠ nf(n - # x - # x0), # x + # x0 ≤ n ⊦

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; (s) ⊦ # x = 0 ↔ x = []; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 24 from proof append-assoc (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m + n - m = n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: n, # x + # x0, n0

Proof step 25 from proof append-assoc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  (⌜x⌝ + ⌜nf⌝ ) + σ2 ≠ ⌜x⌝ + ⌜nf⌝ ⊦

Rule argument

Additional information

Used simplifier rules: append-inf: ⊦ ⌜nf⌝ + σ = ⌜nf⌝ ;

Proof step 26 from proof append-assoc (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 27:

  ⊦ ⌜x⌝ + ⌜nf⌝ = ⌜λ n. (n < # x ⊃ x[n];nf(n - # x))⌝

Rule argument

Additional information

Used simplifier rules: append-inf: ⊦ ⌜nf⌝ + σ = ⌜nf⌝ ; ⊦ ⌜nf⌝ = ⌜nf0⌝ ↔ nf = nf0; (s) Used terms: nf, x

Proof step 27 from proof append-assoc (previous step) (back to tree)

Lemma append-fininf