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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ⌜σ to n⌝ + σ0 from n1 + n ≠ σ0 from n1, ¬ # σ0 < ⌜n1⌝ , ¬ # σ < ⌜n⌝ ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ⌜σ to n⌝ + σ0 from n1 + n ≠ σ0 from n1, ¬ # σ0 < ⌜n1⌝ , ¬ # σ < ⌜n⌝ ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ σ0 = σ1 ↔ # σ0 = # σ1 ∧ (∀ n. ⌜n⌝ < # σ0 → σ0[n] = σ1[n])

• Proof step 5:

  ¬ # σ0 < ⌜n1⌝ , ¬ # σ < ⌜n⌝ , #(⌜σ to n⌝ + σ0 from n1 + n) ≠ #(σ0 from n1) ∨ (∃ n0. ¬(⌜n0⌝ < #(⌜σ to n⌝ + σ0 from n1 + n) → (⌜σ to n⌝ + σ0 from n1 + n)[n0] = (σ0 from n1)[n0])) ⊦

Rule argument

Additional information

Used terms: ⌜σ to n⌝ + σ0 from n1 + n, σ0 from n1

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

Lemma extensionality

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  ¬ # σ0 < ⌜n1⌝ , ¬ # σ < ⌜n⌝ , #(⌜σ to n⌝ + σ0 from n1 + n) ≠ #(σ0 from n1) ∨ ¬(⌜n0⌝ < #(⌜σ to n⌝ + σ0 from n1 + n) → (⌜σ to n⌝ + σ0 from n1 + n)[n0] = (σ0 from n1)[n0]) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ ¬ # σ < ⌜n⌝ ∧ finp(σ) → #(σ from n) = ⌜(# σ).n - n⌝

• Proof step 8:

  ¬ # σ0 < ⌜n1⌝ , ¬ # σ < ⌜n⌝ , #(⌜σ to n⌝ + σ0 from n1 + n) ≠ #(σ0 from n1) ∨ ¬(⌜n0⌝ < #(⌜σ to n⌝ + σ0 from n1 + n) → (⌜σ to n⌝ + σ0 from n1 + n)[n0] = (σ0 from n1)[n0]) ⊦ ¬ # σ0 < ⌜n1⌝ ∧ finp(σ0)

• Proof step 11:

  finp(σ0), ¬ # σ0 < ⌜n1⌝ , ¬ # σ < ⌜n⌝ , #(⌜σ to n⌝ + σ0 from n1 + n) ≠ ⌜(# σ0).n - n1⌝ ∨ ¬(⌜n0⌝ < #(⌜σ to n⌝ + σ0 from n1 + n) → (⌜σ to n⌝ + σ0 from n1 + n)[n0] = (σ0 from n1)[n0]) ⊦

Rule argument

Additional information

Used terms: σ0, n1

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

Lemma fin-size-from

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  ¬ # σ < ⌜n⌝ , #(⌜σ to n⌝ + ⌜nf⌝ from n1 + n) ≠ ∞ ∨ (⌜σ to n⌝ + ⌜nf⌝ from n1 + n)[n0] ≠ nf(n1 + n0) ⊦

Rule argument

Additional information

Used simplifier rules: less-size-from: ⌜n⌝ < # σ ⊦ ⌜n0⌝ < #(σ from n) ↔ ⌜n0 + n⌝ < # σ; size-append: ⊦ #(σ + σ1) = # σ + # σ1; size-to-02: ⊦ # ⌜σ to n⌝ = ⌜#(σ to n)⌝ ; size-to: ¬ # σ < ⌜n⌝ ⊦ #(σ to n) = n; append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; get-from: ⊦ ⌜n⌝ + ⌜m⌝ < # σ → (σ from n)[m] = σ[n + m]; from-inf: ⊦ ⌜nf⌝ from n = ⌜nf from n⌝ ; size-inf: ⊦ # ⌜nf⌝ = ∞; sel-inf: ⊦ ⌜nf⌝ [n] = nf(n); add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf ⊦ ⌜n⌝ ≠ ∞; (s) ⊦ ⌜m⌝ + n∞ = ∞ ↔ n∞ = ∞; (s) ⊦ n∞ < ∞ ↔ n∞ ≠ ∞; (s) ⊦ ¬ ∞ < n∞; (s) ⊦ ⌜n⌝ + n∞1 < ⌜n⌝ + n∞2 ↔ n∞1 < n∞2; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s) ⊦ ⌜m⌝ + ∞ = ∞; (s) ⊦ finp(σ) ↔ ¬(∃ nf. ⌜nf⌝ = σ); (ss)

Proof step 9 from proof from-append-add (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: size-inf: ⊦ # ⌜nf⌝ = ∞; get-to: m < n, ¬ # σ < ⌜n⌝ ⊦ (σ to n)[m] = σ[m]; size-to: ¬ # σ < ⌜n⌝ ⊦ #(σ to n) = n; from-inf: ⊦ ⌜nf⌝ from n = ⌜nf from n⌝ ; sel-inf: ⊦ ⌜nf⌝ [n] = nf(n); get-from-inf: ⊦ ((nf from n))(m) = nf(m + n); ⊦ ¬ m + n < m; (s) ⊦ 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 Used terms: σ to n, nf

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

Lemma append-fininf

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  ((σ to n) + x)[(n1 + n) + n0] ≠ x[n1 + n0], x ≠ [], n0 + n1 < # x, n1 ≤ # x, ¬ # σ < ⌜n⌝ ⊦

Rule argument

Additional information

Used simplifier rules: size-fin: ⊦ # ⌜x⌝ = ⌜# x⌝ ; length-from: ¬ # x < n ⊦ #(x from n) = # x - n; from-appfin: ⊦ ⌜x⌝ + ⌜y⌝ from n = ⌜x + y from n⌝ ; append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; size-to: ¬ # σ < ⌜n⌝ ⊦ #(σ to n) = n; from-fin: ⊦ ⌜x⌝ from n = ⌜x from n⌝ ; sel-fin: ⊦ ⌜x⌝ [n] = x[n]; get-from-01: m + m0 < # x ⊦ (x from m)[m0] = x[m + m0]; ⊦ # x = 0 ↔ x = []; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m < n → (n ≤ m ↔ false); (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) 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 ⊦ #(x + y) = # x + # y; (s) n0 ≤ n ⊦ m < n - n0 ↔ m + n0 < n; (s) ⊦ m ≤ n → (n < m ↔ false); (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ m + n - n + n1 = m - n1; (s) ⊦ ⌜n⌝ = ⌜n0⌝ ↔ n = n0; (s) ⊦ ⌜n⌝ .n = n; (s) ⊦ finp(σ) ↔ (∃ x. ⌜x⌝ = σ); (as)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

  ⊦ ¬ n < # x → (x + y)[n] = y[n - # x]

Rule argument

Additional information

Used simplifier rules: size-to: ¬ # σ < ⌜n⌝ ⊦ #(σ to n) = n; size-to: ¬ # σ < ⌜n⌝ ⊦ #(σ to n) = n; ⊦ 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 < # x → (x + y)[n] = x[n]; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ ¬ m + n < m; (s) Used terms: σ to n, x, (n1 + n) + n0

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

A spec-lemma