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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  (σ from m) to n ≠ (σ to m + n) from m, ¬ # σ < ⌜m⌝ + ⌜n⌝ ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  (σ from m) to n ≠ (σ to m + n) from m, ¬ # σ < ⌜m⌝ + ⌜n⌝ ⊦

Rule argument

Additional information

Proof step 3 from proof swap-from-to (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:

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

Rule argument

Additional information

Used terms: (σ to m + n) from m, (σ from m) to n

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

Lemma extensionality

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

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

Rule argument

Additional information

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

User applied rule cut formula

And obtained the following new goals

• Proof step 7:

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

• Proof step 20:

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

Rule argument

Additional information

Used formulas: #((σ from m) to n) = #((σ to m + n) from m)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  #((σ from m) to n) = #((σ to m + n) from m), ((σ from m) to n)[n0] ≠ ((σ to m + n) from m)[n0], ⌜n0⌝ < #((σ from m) to n), ¬ # σ < ⌜m⌝ + ⌜n⌝ ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ¬ # σ < ⌜n⌝ ⊦ #(σ to n) = ⌜n⌝

• Proof step 10:

  #((σ from m) to n) = #((σ to m + n) from m), ((σ from m) to n)[n0] ≠ ((σ to m + n) from m)[n0], #(σ from m) < ⌜n⌝ , ⌜n0⌝ < #((σ from m) to n), ¬ # σ < ⌜m⌝ + ⌜n⌝ ⊦

• Proof step 15:

  ⌜n⌝ = #((σ to m + n) from m), ((σ from m) to n)[n0] ≠ ((σ to m + n) from m)[n0], ⌜n0⌝ < ⌜n⌝ , ¬ #(σ from m) < ⌜n⌝ , ¬ # σ < ⌜m⌝ + ⌜n⌝ ⊦

Rule argument

Additional information

Used terms: n, σ from m

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

Lemma size-to

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  #((σ from m) to n) = #((σ to m + n) from m), ((σ from m) to n)[n0] ≠ ((σ to m + n) from m)[n0], ⌜n0⌝ < #((σ from m) to n), #(σ from m) < ⌜n⌝ , ¬ # σ < ⌜m⌝ + ⌜n⌝ ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

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

• Proof step 13:

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

Rule argument

Additional information

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

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

Lemma fin-size-from

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

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

Rule argument

Additional information

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

User applied rule constructor cut

And closed the goal!

Rule argument

Additional information

Used simplifier rules: sel-fin: ⊦ ⌜x⌝ [n] = x[n]; length-to: ¬ # x < n ⊦ #(x to n) = n; get-from-01: m + m0 < # x ⊦ (x from m)[m0] = x[m + m0]; get-finto: ¬ # x < n, m < n ⊦ (x to n)[m] = x[m]; to-fin: ⊦ ⌜x⌝ to n = ⌜x to n⌝ ; from-fin: ⊦ ⌜x⌝ from n = ⌜x from n⌝ ; length-from: ¬ # x < n ⊦ #(x from n) = # x - n; size-fin: ⊦ # ⌜x⌝ = ⌜# x⌝ ; size-fin: ⊦ # ⌜x⌝ = ⌜# x⌝ ; length-from: ¬ # x < n ⊦ #(x from n) = # x - n; get-from-inf: ⊦ ((nf from n))(m) = nf(m + n); from-fin: ⊦ ⌜x⌝ from n = ⌜x from n⌝ ; sel-fin: ⊦ ⌜x⌝ [n] = x[n]; size-inf-to: ⊦ #(nf to n) = n; get-from-01: m + m0 < # x ⊦ (x from m)[m0] = x[m + m0]; from-inf: ⊦ ⌜nf⌝ from n = ⌜nf from n⌝ ; to-inf: ⊦ ⌜nf⌝ to n = ⌜nf to n⌝ ; inf-size-to: ⊦ # ⌜nf to n⌝ = ⌜n⌝ ; get-infto: m < n ⊦ (nf to n)[m] = nf(m); stream('a) freely generated by ⌜ ⌝, ⌜ ⌝;; ⊦ ¬ m + n < m; (s) ⊦ m + n - m = n; (s) ⊦ ⌜n⌝ = ⌜n0⌝ ↔ n = n0; (s) ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ m ≤ n → (n < m ↔ false); (s) fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic ⊦ m < n → n ≠ 0; (s) ⊦ # x = 0 ↔ x = []; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m < n → ⌜m⌝ < ⌜n⌝ + n∞0; (s) n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s) ⊦ ⌜n⌝ < ⌜m⌝ + ⌜n0⌝ ↔ n < m + n0; (s) ⊦ m < n → (n ≤ m ↔ false); (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 15 from proof swap-from-to (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  ⌜n⌝ = #((σ to m + n) from m), (σ from m)[n0] ≠ ((σ to m + n) from m)[n0], n0 < n, ¬ # σ < ⌜m⌝ + ⌜n⌝ , ¬ #(σ from m) < ⌜n⌝ ⊦

Rule argument

Additional information

Used simplifier rules: get-to: m < n, ¬ # σ < ⌜n⌝ ⊦ (σ to n)[m] = σ[m]; ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ m < n → (n ≤ m ↔ false); (s) ⊦ m < n ↔ ¬ n ≤ m; (ss)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

  ⊦ ⌜n⌝ + ⌜m⌝ < # σ → (σ from n)[m] = σ[n + m]

• Proof step 18:

  ⌜n⌝ = #((σ to m + n) from m), σ[m + n0] ≠ ((σ to m + n) from m)[n0], n0 < n, ⌜m⌝ + ⌜n0⌝ < # σ, ¬ # σ < ⌜m⌝ + ⌜n⌝ , ¬ #(σ from m) < ⌜n⌝ ⊦

Rule argument

Additional information

Used simplifier rules: lele-trans: ⊦ ¬ n∞1 < n∞ ∧ ¬ n∞2 < n∞1 → ¬ n∞2 < n∞; (forward) from specification nat-inf ⊦ ⌜n⌝ + ⌜m⌝ < ⌜n0⌝ + ⌜n1⌝ ↔ n + m < n0 + n1; (s) ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m < n → (n ≤ m ↔ false); (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic 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: n0, m, σ

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

Lemma get-from

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

  ⊦ ⌜n⌝ + ⌜m⌝ < # σ → (σ from n)[m] = σ[n + m]

Rule argument

Additional information

Used simplifier rules: size-to: ¬ # σ < ⌜n⌝ ⊦ #(σ to n) = ⌜n⌝ ; get-to: m < n, ¬ # σ < ⌜n⌝ ⊦ (σ to n)[m] = σ[m]; ⊦ m + n < m + n0 ↔ n < n0; (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 ⊦ ⌜n⌝ + ⌜m⌝ < ⌜n0⌝ + ⌜n1⌝ ↔ n + m < n0 + n1; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m < n → (n ≤ m ↔ false); (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: n0, m, σ to m + n

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

Lemma get-from

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  #((σ from m) to n) ≠ #((σ to m + n) from m), ¬ # σ < ⌜m⌝ + ⌜n⌝ ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 22:

  ¬ # σ < ⌜n⌝ ⊦ #(σ to n) = ⌜n⌝

• Proof step 23:

  #((σ from m) to n) ≠ #((σ to m + n) from m), #(σ from m) < ⌜n⌝ , ¬ # σ < ⌜m⌝ + ⌜n⌝ ⊦

• Proof step 28:

  ⌜n⌝ ≠ #((σ to m + n) from m), ¬ #(σ from m) < ⌜n⌝ , ¬ # σ < ⌜m⌝ + ⌜n⌝ ⊦

Rule argument

Additional information

Used terms: n, σ from m

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

Lemma size-to

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  #((σ from m) to n) ≠ #((σ to m + n) from m), #(σ from m) < ⌜n⌝ , ¬ # σ < ⌜m⌝ + ⌜n⌝ ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 25:

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

• Proof step 26:

  #((σ from m) to n) ≠ #((σ to m + n) from m), #(σ from m) < ⌜n⌝ , ¬ # σ < ⌜m⌝ + ⌜n⌝ ⊦ ⌜m⌝ < # σ ∧ finp(σ)

Rule argument

Additional information

Used simplifier rules: to-fin: ⊦ ⌜x⌝ to n = ⌜x to n⌝ ; from-fin: ⊦ ⌜x⌝ from n = ⌜x from n⌝ ; length-from: ¬ # x < n ⊦ #(x from n) = # x - n; size-fin: ⊦ # ⌜x⌝ = ⌜# x⌝ ; length-to: ¬ # x < n ⊦ #(x to n) = n; ⊦ finp(σ) ↔ (∃ x. ⌜x⌝ = σ); (as) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m < n → n ≠ 0; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m < n → ¬ n < m; (s) n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s) ⊦ ¬ m + n < m; (s) ⊦ ⌜n⌝ .n = n; (s) ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ ⌜n⌝ < ⌜m⌝ + ⌜n0⌝ ↔ n < m + n0; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m < n → (n ≤ m ↔ false); (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 ⊦ 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⌝ = ⌜n0⌝ ↔ n = n0; (s) Used terms: m, σ

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

Lemma fin-size-from

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  #((σ from m) to n) ≠ #((σ to m + n) from m), #(σ from m) < ⌜n⌝ , ¬ # σ < ⌜m⌝ + ⌜n⌝ ⊦ ⌜m⌝ < # σ ∧ finp(σ)

Rule argument

Additional information

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

User applied rule constructor cut

And closed the goal!

Rule argument

Additional information

Used simplifier rules: to-fin: ⊦ ⌜x⌝ to n = ⌜x to n⌝ ; length-to: ¬ # x < n ⊦ #(x to n) = n; from-fin: ⊦ ⌜x⌝ from n = ⌜x from n⌝ ; length-from: ¬ # x < n ⊦ #(x from n) = # x - n; size-fin: ⊦ # ⌜x⌝ = ⌜# x⌝ ; from-inf: ⊦ ⌜nf⌝ from n = ⌜nf from n⌝ ; inf-size-to: ⊦ # ⌜nf to n⌝ = ⌜n⌝ ; to-inf: ⊦ ⌜nf⌝ to n = ⌜nf to n⌝ ; from-fin: ⊦ ⌜x⌝ from n = ⌜x from n⌝ ; size-fin: ⊦ # ⌜x⌝ = ⌜# x⌝ ; length-from: ¬ # x < n ⊦ #(x from n) = # x - n; size-inf-to: ⊦ #(nf to n) = n; stream('a) freely generated by ⌜ ⌝, ⌜ ⌝;; ⊦ ¬ 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 ⊦ ⌜n⌝ = ⌜n0⌝ ↔ n = n0; (s) ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m < n → ⌜m⌝ < ⌜n⌝ + n∞0; (s) n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s) ⊦ ⌜n⌝ < ⌜m⌝ + ⌜n0⌝ ↔ n < m + n0; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m < n → (n ≤ m ↔ false); (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 28 from proof swap-from-to (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  ⌜n⌝ ≠ #((σ to m + n) from m), ¬ #(σ from m) < ⌜n⌝ , ¬ # σ < ⌜m⌝ + ⌜n⌝ ⊦

Rule argument

Additional information

Proof step 29 from proof swap-from-to (previous step) (back to tree)

User applied rule constructor cut

And closed the goal!

Rule argument

Additional information

Used simplifier rules: to-fin: ⊦ ⌜x⌝ to n = ⌜x to n⌝ ; length-from: ¬ # x < n ⊦ #(x from n) = # x - n; from-fin: ⊦ ⌜x⌝ from n = ⌜x from n⌝ ; size-fin: ⊦ # ⌜x⌝ = ⌜# x⌝ ; length-to: ¬ # x < n ⊦ #(x to n) = n; to-inf: ⊦ ⌜nf⌝ to n = ⌜nf to n⌝ ; from-fin: ⊦ ⌜x⌝ from n = ⌜x from n⌝ ; size-fin: ⊦ # ⌜x⌝ = ⌜# x⌝ ; length-from: ¬ # x < n ⊦ #(x from n) = # x - n; size-inf-to: ⊦ #(nf to n) = n; stream('a) freely generated by ⌜ ⌝, ⌜ ⌝;; ⊦ ¬ 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 ⊦ ⌜n⌝ = ⌜n0⌝ ↔ n = n0; (s) ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ ⌜n⌝ < ⌜m⌝ + ⌜n0⌝ ↔ n < m + n0; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m < n → (n ≤ m ↔ false); (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