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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  # σ = # σ1, ¬(σ + σ0 = σ1 + σ2 ↔ σ = σ1 ∧ σ0 = σ2), finp(σ) ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  # σ = # σ1, σ + σ0 = σ1 + σ2, finp(σ) ⊦ σ = σ1 ∧ σ0 = σ2

Rule argument

Additional information

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

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  # ⌜x⌝ = # σ1, ⌜x⌝ + σ0 = σ1 + σ2, finp(⌜x⌝ ) ⊦ ⌜x⌝ = σ1 ∧ σ0 = σ2

Rule argument

Additional information

Used simplifier rules: append-inf: ⊦ ⌜nf⌝ + σ = ⌜nf⌝ ; append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; size-inf: ⊦ # ⌜nf⌝ = ∞; stream('a) freely generated by ⌜ ⌝, ⌜ ⌝;; ⊦ ¬ finp(⌜nf⌝ ); (s)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ⌜x⌝ + σ0 = σ1 + σ2, ⌜# x⌝ = # σ1 ⊦ ⌜x⌝ = σ1 ∧ σ0 = σ2

Rule argument

Additional information

Used simplifier rules: size-fin: ⊦ # ⌜x⌝ = ⌜# x⌝ ; ⊦ finp(⌜x⌝ ); (s)

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

User applied rule structural induction

And obtained the following new goals

• Proof step 6:

  ⌜x⌝ + σ0 = ⌜x0⌝ + σ2, ⌜# x⌝ = # ⌜x0⌝ ⊦ ⌜x⌝ = ⌜x0⌝ ∧ σ0 = σ2

Rule argument

Additional information

Used simplifier rules: size-inf: ⊦ # ⌜nf⌝ = ∞; stream('a) freely generated by ⌜ ⌝, ⌜ ⌝;; ⊦ ⌜n⌝ ≠ ∞; (s)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  # x = # x0, ⌜x⌝ + σ0 = ⌜x0⌝ + σ2 ⊦ x = x0 ∧ σ0 = σ2

Rule argument

Additional information

Used simplifier rules: size-fin: ⊦ # ⌜x⌝ = ⌜# x⌝ ; ⊦ ⌜x⌝ = ⌜x0⌝ ↔ x = x0; (s) ⊦ ⌜n⌝ = ⌜n0⌝ ↔ n = n0; (s)

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

User applied rule structural induction

And obtained the following new goals

• Proof step 8:

  # x = # x0, ⌜x⌝ + σ0 = ⌜x0⌝ + ⌜x1⌝ ⊦ x = x0 ∧ σ0 = ⌜x1⌝

• Proof step 9:

  # x = # x0, ⌜x⌝ + σ0 = ⌜x0⌝ + ⌜nf⌝ ⊦ x = x0 ∧ σ0 = ⌜nf⌝

Rule argument

Additional information

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

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

User applied rule structural induction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: eq-stream-to-list-2-2: ⊦ ⌜x⌝ + ⌜y⌝ = ⌜x0⌝ + ⌜z⌝ ↔ x + y = x0 + z; append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; neq-fin-inf-02: ⊦ σ0 + ⌜x⌝ = σ + ⌜nf0⌝ ↔ σ0 = σ + ⌜nf0⌝ ; neq-fin-inf-01: ⊦ ⌜x⌝ ≠ σ + ⌜nf0⌝ ; append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; stream('a) freely generated by ⌜ ⌝, ⌜ ⌝;; ⊦ # x = # z → (x + y = z + y0 ↔ x = z ∧ y = y0); (ws) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ ⌜x⌝ = ⌜x0⌝ ↔ x = x0; (s)

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

User applied rule structural induction

And obtained the following new goals

• Proof step 10:

  # x = # x0, ⌜x⌝ + ⌜nf0⌝ = ⌜x0⌝ + ⌜nf⌝ ⊦ x = x0 ∧ ⌜nf0⌝ = ⌜nf⌝

Rule argument

Additional information

Used simplifier rules: neq-fin-inf-02: ⊦ σ0 + ⌜x⌝ = σ + ⌜nf0⌝ ↔ σ0 = σ + ⌜nf0⌝ ; neq-fin-inf-01: ⊦ ⌜x⌝ ≠ σ + ⌜nf0⌝ ; append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; stream('a) freely generated by ⌜ ⌝, ⌜ ⌝;;

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  # x = # x0, ⌜x⌝ + ⌜nf0⌝ = ⌜x0⌝ + ⌜nf⌝ ⊦ x = x0 ∧ nf0 = nf

Rule argument

Additional information

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

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

User applied rule structural induction

And obtained the following new goals

• Proof step 12:

  #(a + x1) = # x0, ⌜a + x1⌝ + ⌜nf0⌝ = ⌜x0⌝ + ⌜nf⌝ , ∀ x0, nf0, nf. # x1 = # x0 ∧ ⌜x1⌝ + ⌜nf0⌝ = ⌜x0⌝ + ⌜nf⌝ → x1 = x0 ∧ nf0 = nf ⊦ a + x1 = x0 ∧ nf0 = nf

Rule argument

Additional information

Used simplifier rules: empty: ⊦ ⌜[]⌝ = []; empty-append: ⊦ [] + σ = σ; append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; list('a) freely generated by [], +;; ⊦ # [] = 0; (s) ⊦ # x = 0 ↔ x = []; (s) ⊦ ⌜nf⌝ = ⌜nf0⌝ ↔ nf = nf0; (s)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  (⌜a '⌝ + ⌜x1⌝ ) + ⌜nf0⌝ = ⌜x0⌝ + ⌜nf⌝ , 1 + # x1 = # x0, ∀ x0, nf0, nf. # x1 = # x0 ∧ ⌜x1⌝ + ⌜nf0⌝ = ⌜x0⌝ + ⌜nf⌝ → x1 = x0 ∧ nf0 = nf ⊦ a ' + x1 = x0 ∧ nf0 = nf

Rule argument

Additional information

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

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

User applied rule structural induction

And obtained the following new goals

• Proof step 14:

  1 + # x1 = #(a0 + x), (⌜a '⌝ + ⌜x1⌝ ) + ⌜nf0⌝ = ⌜a0 + x⌝ + ⌜nf⌝ , ∀ x0, nf0, nf. # x1 = # x0 ∧ ⌜x1⌝ + ⌜nf0⌝ = ⌜x0⌝ + ⌜nf⌝ → x1 = x0 ∧ nf0 = nf, ∀ a, x1, nf0, nf. (⌜a '⌝ + ⌜x1⌝ ) + ⌜nf0⌝ = ⌜x⌝ + ⌜nf⌝ ∧ 1 + # x1 = # x ∧ (∀ x0, nf0, nf. # x1 = # x0 ∧ ⌜x1⌝ + ⌜nf0⌝ = ⌜x0⌝ + ⌜nf⌝ → x1 = x0 ∧ nf0 = nf) → a ' + x1 = x ∧ nf0 = nf ⊦ a ' + x1 = a0 + x ∧ nf0 = nf

Rule argument

Additional information

Used simplifier rules: empty: ⊦ ⌜[]⌝ = []; empty-append: ⊦ [] + σ = σ; append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; list('a) freely generated by [], +;; ⊦ # [] = 0; (s) ⊦ m + 1 ≠ 0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  # x1 = # x, (⌜a '⌝ + ⌜x1⌝ ) + ⌜nf0⌝ = (⌜a0 '⌝ + ⌜x⌝ ) + ⌜nf⌝ , ∀ a, x1, nf0, nf. (⌜a '⌝ + ⌜x1⌝ ) + ⌜nf0⌝ = ⌜x⌝ + ⌜nf⌝ ∧ 1 + # x1 = # x ∧ (∀ x0, nf0, nf. # x1 = # x0 ∧ ⌜x1⌝ + ⌜nf0⌝ = ⌜x0⌝ + ⌜nf⌝ → x1 = x0 ∧ nf0 = nf) → a ' + x1 = x ∧ nf0 = nf, ∀ x0, nf0, nf. # x = # x0 ∧ ⌜x1⌝ + ⌜nf0⌝ = ⌜x0⌝ + ⌜nf⌝ → x1 = x0 ∧ nf0 = nf ⊦ a ' + x1 = a0 ' + x ∧ nf0 = nf

Rule argument

Additional information

Used simplifier rules: append-finfin: ⊦ ⌜x + y⌝ = ⌜x⌝ + ⌜y⌝ ; ⊦ a + x = a ' + 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 + n0 ↔ n = n0; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ # a ' = 0 +1; (s) ⊦ #(x + y) = # x + # y; (s)

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

User applied rule weakening

And obtained the following new goals

• Proof step 16:

  # x1 = # x, (⌜a '⌝ + ⌜x1⌝ ) + ⌜nf0⌝ = (⌜a0 '⌝ + ⌜x⌝ ) + ⌜nf⌝ , ∀ x0, nf0, nf. # x = # x0 ∧ ⌜x1⌝ + ⌜nf0⌝ = ⌜x0⌝ + ⌜nf⌝ → x1 = x0 ∧ nf0 = nf ⊦ a ' + x1 = a0 ' + x ∧ nf0 = nf

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

  ⊦ a ' + x = a0 ' + y ↔ a = a0 ∧ x = y

• Proof step 18:

  # x1 = # x, (⌜a '⌝ + ⌜x1⌝ ) + ⌜nf0⌝ = (⌜a0 '⌝ + ⌜x⌝ ) + ⌜nf⌝ , ∀ x0, nf0, nf. # x = # x0 ∧ ⌜x1⌝ + ⌜nf0⌝ = ⌜x0⌝ + ⌜nf⌝ → x1 = x0 ∧ nf0 = nf ⊦ (a = a0 ∧ x1 = x) ∧ nf0 = nf

Rule argument

Additional information

Used terms: a, x1, a0, x

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  # x1 = # x, (⌜a '⌝ + ⌜x1⌝ ) + ⌜nf0⌝ = (⌜a0 '⌝ + ⌜x⌝ ) + ⌜nf⌝ , ∀ x0, nf0, nf. # x = # x0 ∧ ⌜x1⌝ + ⌜nf0⌝ = ⌜x0⌝ + ⌜nf⌝ → x1 = x0 ∧ nf0 = nf ⊦ a = a0 ∧ x1 = x ∧ nf0 = nf

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

  ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2

• Proof step 21:

  # x1 = # x, ⌜a '⌝ + ⌜x1⌝ + ⌜nf0⌝ = (⌜a0 '⌝ + ⌜x⌝ ) + ⌜nf⌝ , ∀ x0, nf0, nf. # x = # x0 ∧ ⌜x1⌝ + ⌜nf0⌝ = ⌜x0⌝ + ⌜nf⌝ → x1 = x0 ∧ nf0 = nf ⊦ a = a0 ∧ x1 = x ∧ nf0 = nf

Rule argument

Additional information

Used terms: ⌜nf0⌝ , ⌜x1⌝ , ⌜a '⌝

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

Lemma append-assoc

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 22:

  ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2

• Proof step 23:

  # x1 = # x, ⌜a '⌝ + ⌜x1⌝ + ⌜nf0⌝ = ⌜a0 '⌝ + ⌜x⌝ + ⌜nf⌝ , ∀ x0, nf0, nf. # x = # x0 ∧ ⌜x1⌝ + ⌜nf0⌝ = ⌜x0⌝ + ⌜nf⌝ → x1 = x0 ∧ nf0 = nf ⊦ a = a0 ∧ x1 = x ∧ nf0 = nf

Rule argument

Additional information

Used terms: ⌜nf⌝ , ⌜x⌝ , ⌜a0 '⌝

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

Lemma append-assoc

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 24:

  ⊦ ⌜a '⌝ + σ = ⌜a0 '⌝ + σ0 ↔ a = a0 ∧ σ = σ0

• Proof step 25:

  # x1 = # x, ⌜x1⌝ + ⌜nf0⌝ = ⌜x⌝ + ⌜nf⌝ , a = a0, ∀ x0, nf0, nf. # x = # x0 ∧ ⌜x1⌝ + ⌜nf0⌝ = ⌜x0⌝ + ⌜nf⌝ → x1 = x0 ∧ nf0 = nf ⊦ a = a0 ∧ x1 = x ∧ nf0 = nf

Rule argument

Additional information

Used terms: ⌜x⌝ + ⌜nf⌝ , a0, ⌜x1⌝ + ⌜nf0⌝ , a

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

Lemma cons-eq

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  # x1 = # x, ⌜x1⌝ + ⌜nf0⌝ = ⌜x⌝ + ⌜nf⌝ , ∀ x0, nf0, nf. # x = # x0 ∧ ⌜x1⌝ + ⌜nf0⌝ = ⌜x0⌝ + ⌜nf⌝ → x1 = x0 ∧ nf0 = nf ⊦ x1 = x ∧ nf0 = nf

Rule argument

Additional information

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

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: x, nf0, nf