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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  #(σ + σ1) ≠ # σ + # σ1 ⊦

Rule argument

Additional information

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

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

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

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 ⌜ ⌝, ⌜ ⌝;; ⊦ n∞ + ∞ = ∞; (s) add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

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

Rule argument

Additional information

Used simplifier rules: size-fin: ⊦ # ⌜x⌝ = ⌜# x⌝ ;

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

User applied rule structural induction

And obtained the following new goals

• Proof step 5:

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

• Proof step 10:

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

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

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

Rule argument

Additional information

Used simplifier rules: size-fin: ⊦ # ⌜x⌝ = ⌜# x⌝ ;

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

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

• Proof step 8:

  # ⌜x + x0⌝ ≠ ⌜# x⌝ + ⌜# x0⌝ ⊦

Rule argument

Additional information

Used terms: x0, x

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

Lemma append-finfin

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ # ⌜x⌝ = ⌜# x⌝

Rule argument

Additional information

Used simplifier rules: ⊦ #(x + y) = # x + # y; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ ⌜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⌝ + n∞1 = ⌜n⌝ + n∞2 ↔ n∞1 = n∞2; (s) add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf Used terms: x + x0

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

Lemma size-fin

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

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

Rule argument

Additional information

Used simplifier rules: size-inf: ⊦ # ⌜nf⌝ = ∞; ⊦ ∞ + ⌜m⌝ = ∞; (s) add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf Used terms: nf, x

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

Lemma append-fininf