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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 2:

  ⌜ef⌝ = ext !(⌜af⌝ ) ⊦ ⌜ef⌝ = ext !(⌜af0⌝ ) ↔ (∀ n. ∃ m. ext !(af.take(n)) = ext !(af0.take(m)))

Rule argument

Additional information

Used simplifier rules: ⊦ finp(σ) ↔ ¬(∃ nf. ⌜nf⌝ = σ); (ss)

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

User applied rule case distinction

And obtained the following new goals

• Proof step 3:

  ⌜ef⌝ = ext !(⌜af⌝ ), ⌜ef⌝ = ext !(⌜af0⌝ ) ⊦ ∀ n. ∃ m. ext !(af.take(n)) = ext !(af0.take(m))

• Proof step 11:

  ⌜ef⌝ = ext !(⌜af⌝ ), ⌜ef⌝ ≠ ext !(⌜af0⌝ ), ∀ n. ∃ m. ext !(af.take(n)) = ext !(af0.take(m)) ⊦

Rule argument

Additional information

Proof step 3 from proof remtau-equiv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  ⌜ef⌝ = ext !(⌜af0⌝ ), ⌜ef⌝ = ext !(⌜af⌝ ) ⊦ ∃ m. ext !(af.take(n)) = ext !(af0.take(m))

Rule argument

Additional information

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 5:

  ⊦ ¬ # α < ⌜n⌝ → (∃ m. ¬ # ext !(α) < ⌜m⌝ ∧ ext !(⌜α.take(n)⌝ ) = ⌜ext !(α).take(m)⌝ )

• Proof step 6:

  ⌜ef⌝ = ext !(⌜af⌝ ), ⌜ef⌝ = ext !(⌜af0⌝ ), ¬ # ⌜af⌝ < ⌜n⌝ → (∃ m. ¬ # ext !(⌜af⌝ ) < ⌜m⌝ ∧ ext !(⌜⌜af⌝ .take(n)⌝ ) = ⌜ext !(⌜af⌝ ).take(m)⌝ ) ⊦ ∃ m. ext !(af.take(n)) = ext !(af0.take(m))

Rule argument

Additional information

Used terms: ⌜af⌝ , n, ext

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

Lemma to_of_remtau-remtau_of_to

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  ext !(af.take(n)) = ef.take(m), ⌜ef⌝ = ext !(⌜af⌝ ), ⌜ef⌝ = ext !(⌜af0⌝ ) ⊦ ∃ m. ext !(af.take(n)) = ext !(af0.take(m))

Rule argument

Additional information

Used simplifier rules: finremtau-def: ⊦ ext !(⌜al⌝ ) = ⌜ext !(al)⌝ ; ⊦ ¬ ∞ < n∞; (s) ⊦ # ⌜nf⌝ = ∞; (s) ⊦ ⌜nf⌝ .take(n) = nf.take(n); (s) ⊦ ⌜x⌝ = ⌜x0⌝ ↔ x = x0; (s)

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 8:

  ⊦ ¬ # ext !(α) < ⌜n⌝ → (∃ m. ¬ # α < ⌜m⌝ ∧ ext !(α).take(n) = ext !(α.take(m)))

• Proof step 9:

  ext !(af.take(n)) = ef.take(m), ⌜ef⌝ = ext !(⌜af0⌝ ), ⌜ef⌝ = ext !(⌜af⌝ ), ¬ # ext !(⌜af0⌝ ) < ⌜m⌝ → (∃ m0. ¬ # ⌜af0⌝ < ⌜m0⌝ ∧ ext !(⌜af0⌝ ).take(m) = ext !(⌜af0⌝ .take(m0))) ⊦ ∃ m. ext !(af.take(n)) = ext !(af0.take(m))

Rule argument

Additional information

Used terms: ext, ⌜af0⌝ , m

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

Lemma remtau_of_to-to_of_rmtau

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  ext !(af.take(n)) = ef.take(m), ef.take(m) = ext !(af0.take(m0)), ⌜ef⌝ = ext !(⌜af0⌝ ), ⌜ef⌝ = ext !(⌜af⌝ ) ⊦ ∃ m. ext !(af.take(n)) = ext !(af0.take(m))

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜nf⌝ .take(n) = nf.take(n); (s) ⊦ ¬ ∞ < n∞; (s) ⊦ # ⌜nf⌝ = ∞; (s)

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

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: m0

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

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

• Proof step 13:

  ⌜ef⌝ = ext !(⌜af⌝ ), ∀ n. ∃ m. ext !(af.take(n)) = ext !(af0.take(m)), # ⌜ef⌝ ≠ # ext !(⌜af0⌝ ) ∨ (∃ n. ¬(¬ # ⌜ef⌝ < ⌜n⌝ → ⌜ef⌝ .take(n) = ext !(⌜af0⌝ ).take(n))) ⊦

Rule argument

Additional information

Used terms: ⌜ef⌝ , ext !(⌜af0⌝ )

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  ⌜ef⌝ = ext !(⌜af⌝ ), ∀ n. ∃ m. ext !(af.take(n)) = ext !(af0.take(m)), ∞ ≠ # ext !(⌜af0⌝ ) ∨ ef.take(n) ≠ ext !(⌜af0⌝ ).take(n) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜nf⌝ .take(n) = nf.take(n); (s) ⊦ ¬ ∞ < n∞; (s) ⊦ # ⌜nf⌝ = ∞; (s)

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

User applied rule cut formula

And obtained the following new goals

• Proof step 15:

  ⌜ef⌝ = ext !(⌜af⌝ ), ∞ ≠ # ext !(⌜af0⌝ ), ∀ n. ∃ m. ext !(af.take(n)) = ext !(af0.take(m)), ∞ ≠ # ext !(⌜af0⌝ ) ∨ ef.take(n) ≠ ext !(⌜af0⌝ ).take(n) ⊦

• Proof step 29:

  ∞ = # ext !(⌜af0⌝ ), ⌜ef⌝ = ext !(⌜af⌝ ), ∀ n. ∃ m. ext !(af.take(n)) = ext !(af0.take(m)), ∞ ≠ # ext !(⌜af0⌝ ) ∨ ef.take(n) ≠ ext !(⌜af0⌝ ).take(n) ⊦

Rule argument

Additional information

Used formulas: ∞ ≠ # ext !(⌜af0⌝ )

Proof step 15 from proof remtau-equiv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  ⌜ef⌝ = ext !(⌜af⌝ ), ∞ ≠ # ext !(⌜af0⌝ ), ∀ n. ∃ m. ext !(af.take(n)) = ext !(af0.take(m)) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

  ⊦ n∞ = ∞ ↔ ¬(∃ n. n∞ = ⌜n⌝ )

• Proof step 18:

  ⌜ef⌝ = ext !(⌜af⌝ ), ∀ n. ∃ m. ext !(af.take(n)) = ext !(af0.take(m)), ∃ n. # ext !(⌜af0⌝ ) = ⌜n⌝ ⊦

Rule argument

Additional information

Used terms: # ext !(⌜af0⌝ )

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  # ext !(⌜af0⌝ ) = ⌜n⌝ , ⌜ef⌝ = ext !(⌜af⌝ ), ∀ n. ∃ m. ext !(af.take(n)) = ext !(af0.take(m)) ⊦

Rule argument

Additional information

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 20:

  ⊦ ¬ # ext !(α) < ⌜n⌝ → (∃ m. ¬ # α < ⌜m⌝ ∧ ext !(α).take(n) = ext !(α.take(m)))

• Proof step 21:

  # ext !(⌜af0⌝ ) = ⌜n⌝ , ⌜ef⌝ = ext !(⌜af⌝ ), ¬ # ext !(⌜af⌝ ) < ⌜n + 1⌝ → (∃ m. ¬ # ⌜af⌝ < ⌜m⌝ ∧ ext !(⌜af⌝ ).take(n + 1) = ext !(⌜af⌝ .take(m))), ∀ n. ∃ m. ext !(af.take(n)) = ext !(af0.take(m)) ⊦

Rule argument

Additional information

Used terms: ext, ⌜af⌝ , n + 1

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

Lemma remtau_of_to-to_of_rmtau

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  # ext !(⌜af0⌝ ) = ⌜n⌝ , ef.take(n + 1) = ext !(af.take(m)), ⌜ef⌝ = ext !(⌜af⌝ ), ∀ n. ∃ m. ext !(af.take(n)) = ext !(af0.take(m)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜nf⌝ .take(n) = nf.take(n); (s) ⊦ ⌜m⌝ < ∞; (s) ⊦ # ⌜nf⌝ = ∞; (s) ⊦ ¬ ∞ < n∞; (s) 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⌝ + ⌜1⌝ ↔ ¬ ⌜n⌝ < # σ; (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)

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

User applied rule all left

And obtained the following new goals

• Proof step 23:

  # ext !(⌜af0⌝ ) = ⌜n⌝ , ef.take(n + 1) = ext !(af.take(m)), ⌜ef⌝ = ext !(⌜af⌝ ), ∀ n. ∃ m. ext !(af.take(n)) = ext !(af0.take(m)), ∃ m0. ext !(af.take(m)) = ext !(af0.take(m0)) ⊦

Rule argument

Additional information

Used terms: m

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  # ext !(⌜af0⌝ ) = ⌜n⌝ , ef.take(n + 1) = ext !(af0.take(m0)), ef.take(n + 1) = ext !(af.take(m)), ⌜ef⌝ = ext !(⌜af⌝ ), ∀ n. ∃ m. ext !(af.take(n)) = ext !(af0.take(m)) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 25:

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

• Proof step 26:

  # ⌜ef⌝ = # ext !(⌜af⌝ ), # ext !(⌜af0⌝ ) = ⌜n⌝ , ef.take(n + 1) = ext !(af.take(m)), ef.take(n + 1) = ext !(af0.take(m0)), ∀ n. ∃ m. ext !(af.take(n)) = ext !(af0.take(m)), ∀ n. ⌜n⌝ < # ⌜ef⌝ → ⌜ef⌝ [n] = ext !(⌜af⌝ )[n] ⊦

Rule argument

Additional information

Used terms: ⌜ef⌝ , ext !(⌜af⌝ )

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  # ext !(⌜af0⌝ ) = ⌜n⌝ , ef.take(n + 1) = ext !(af0.take(m0)), ef.take(n + 1) = ext !(af.take(m)), ∞ = # ext !(⌜af⌝ ), ∀ n. ∃ m. ext !(af.take(n)) = ext !(af0.take(m)), ∀ n0. ef(n0) = ext !(⌜af⌝ )[n0] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜nf⌝ [n] = nf(n); (s) ⊦ ⌜m⌝ < ∞; (s) ⊦ # ⌜nf⌝ = ∞; (s)

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 28:

  ¬ # α < ⌜n⌝ ⊦ ¬ # ext !(α) < # ⌜ext !(α.take(n))⌝

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜nf⌝ .take(n) = nf.take(n); (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ # nf.take(n) = n; (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⌝ < ⌜1⌝ + n∞ ↔ ¬ n∞ < ⌜n⌝ ; (s) ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ ¬ n < 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 ⊦ # ⌜nf⌝ = ∞; (s) ⊦ ¬ ∞ < n∞; (s) Used terms: ⌜af0⌝ , m0, ext

Proof step 28 from proof remtau-equiv (previous step) (back to tree)

Lemma not-lessto

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

  ∞ = # ext !(⌜af0⌝ ), ⌜ef⌝ = ext !(⌜af⌝ ), ef.take(n) ≠ ext !(⌜af0⌝ ).take(n), ∀ n. ∃ m. ext !(af.take(n)) = ext !(af0.take(m)) ⊦

Rule argument

Additional information

Proof step 30 from proof remtau-equiv (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 31:

  ⊦ ¬ # ext !(α) < ⌜n⌝ → (∃ m. ¬ # α < ⌜m⌝ ∧ ext !(α).take(n) = ext !(α.take(m)))

• Proof step 32:

  ∞ = # ext !(⌜af0⌝ ), ⌜ef⌝ = ext !(⌜af⌝ ), ef.take(n) ≠ ext !(⌜af0⌝ ).take(n), ¬ # ext !(⌜af⌝ ) < ⌜n⌝ → (∃ m. ¬ # ⌜af⌝ < ⌜m⌝ ∧ ext !(⌜af⌝ ).take(n) = ext !(⌜af⌝ .take(m))), ∀ n. ∃ m. ext !(af.take(n)) = ext !(af0.take(m)) ⊦

Rule argument

Additional information

Used terms: ext, ⌜af⌝ , n

Proof step 31 from proof remtau-equiv (previous step) (back to tree)

Lemma remtau_of_to-to_of_rmtau

Proof step 32 from proof remtau-equiv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

  ef.take(n) = ext !(af.take(m)), ∞ = # ext !(⌜af0⌝ ), ⌜ef⌝ = ext !(⌜af⌝ ), ef.take(n) ≠ ext !(⌜af0⌝ ).take(n), ∀ n. ∃ m. ext !(af.take(n)) = ext !(af0.take(m)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜nf⌝ .take(n) = nf.take(n); (s) ⊦ ¬ ∞ < n∞; (s) ⊦ # ⌜nf⌝ = ∞; (s)

Proof step 33 from proof remtau-equiv (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 34:

  ef.take(n) = ext !(af.take(m)), ∞ = # ext !(⌜af0⌝ ), ⌜ef⌝ = ext !(⌜af⌝ ), ef.take(n) ≠ ext !(⌜af0⌝ ).take(n), ∀ n. ∃ m. ext !(af.take(n)) = ext !(af0.take(m)), ∃ m0. ext !(af.take(m)) = ext !(af0.take(m0)) ⊦

Rule argument

Additional information

Used terms: m

Proof step 34 from proof remtau-equiv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

  ef.take(n) = ext !(af0.take(m0)), ef.take(n) = ext !(af.take(m)), ∞ = # ext !(⌜af0⌝ ), ⌜ef⌝ = ext !(⌜af⌝ ), ef.take(n) ≠ ext !(⌜af0⌝ ).take(n), ∀ n. ∃ m. ext !(af.take(n)) = ext !(af0.take(m)) ⊦

Rule argument

Additional information

Proof step 35 from proof remtau-equiv (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 36:

  # al = m0, ef.take(n) = ext !(af.take(m)), ef.take(n) = ext !(al), af0 = (⌜al⌝ + ⌜nf0⌝ ).f, ∞ = # ext !(⌜af0⌝ ), ⌜ef⌝ = ext !(⌜af⌝ ), ef.take(n) ≠ ext !(⌜af0⌝ ).take(n), ∀ n. ∃ m. ext !(af.take(n)) = ext !(af0.take(m)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ x0 = nf.take(n) ∧ nf0 = nf.drop(n) ↔ nf = (⌜x0⌝ + ⌜nf0⌝ ).f ∧ # x0 = n; (elim) Used terms: af0, m0, al, nf0

Proof step 36 from proof remtau-equiv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 37:

  # ext !(⌜nf0⌝ ) = ∞, ef.take(n) = ext !(al), ef.take(n) = ext !(af.take(m)), ⌜ef⌝ = ext !(⌜af⌝ ), ef.take(n) ≠ (⌜ef.take(n)⌝ + ext !(⌜nf0⌝ )).take(n), ∀ n. ∃ m. ext !(af.take(n)) = ext !((⌜al⌝ + ⌜nf0⌝ ).f.take(m)) ⊦

Rule argument

Additional information

Used simplifier rules: remtau-append: ⊦ ext !(⌜al⌝ + α2) = ⌜ext !(al)⌝ + ext !(α2); append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ ⌜(⌜x⌝ + ⌜nf⌝ ).f⌝ = ⌜x⌝ + ⌜nf⌝ ; (s) 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 ⊦ ⌜m⌝ + n∞ = ∞ ↔ n∞ = ∞; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ #(σ + σ1) = # σ + # σ1; (s)

Proof step 37 from proof remtau-equiv (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 38:

  ⊦ # σ < ⌜n⌝ → (σ + σ0).take(n) = σ.l + σ0.take(n - # σ.l)

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x⌝ .l = x; (s) ⊦ # nf.take(n) = n; (s) ⊦ m - m = 0; (s) ⊦ σ.take(0) = []; (s) ⊦ x + [] = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ ¬ # σ < ⌜n⌝ → (σ + σ0).take(n) = σ.take(n); (s) ⊦ ⌜x⌝ .take(n) = x.take(n); (s) ⊦ nf.take(n).take(n) = nf.take(n); (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream Used terms: ⌜ef.take(n)⌝ , ext !(⌜nf0⌝ ), n

Proof step 38 from proof remtau-equiv (previous step) (back to tree)

A spec-lemma