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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  [] + σ ≠ σ ⊦

Rule argument

Additional information

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

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  [] + ⌜x⌝ ≠ ⌜x⌝ ⊦

• Proof step 7:

  [] + ⌜nf⌝ ≠ ⌜nf⌝ ⊦

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ ⌜[]⌝ = []

• Proof step 5:

  ⌜[]⌝ + ⌜x⌝ ≠ ⌜x⌝ ⊦

Rule argument

Additional information

Used terms:

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

Lemma empty

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

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

Rule argument

Additional information

Used simplifier rules: ⊦ [] + x = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ ⌜x⌝ = ⌜x0⌝ ↔ x = x0; (s) Used terms: x, []

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

Lemma append-finfin

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

  ⊦ ⌜[]⌝ = []

• Proof step 9:

  ⌜[]⌝ + ⌜nf⌝ ≠ ⌜nf⌝ ⊦

Rule argument

Additional information

Used terms:

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

Lemma empty

Proof step 9 from proof empty-append (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))⌝

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ n < 0; (s) ⊦ # [] = 0; (s) ⊦ m - 0 = m; (s) ⊦ ⌜nf⌝ = ⌜nf0⌝ ↔ nf = nf0; (s) Used terms: nf, []

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

Lemma append-fininf