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

User applied rule case distinction

And obtained the following new goals

• Proof step 2:

  finp(ext !(⌜af⌝ )) ⊦ ∃ n. ∀ m. n ≤ m → ext(af(m)) = None

• Proof step 33:

  ¬ finp(ext !(⌜af⌝ )), ∃ n. ∀ m. n ≤ m → ext(af(m)) = None ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ⌜el⌝ = ext !(⌜af⌝ ) ⊦ ∃ n. ∀ m. n ≤ m → ext(af(m)) = None

Rule argument

Additional information

Used simplifier rules: ⊦ finp(σ) ↔ (∃ x. ⌜x⌝ = σ); (as)

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

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  ⌜[]⌝ = ext !(⌜af⌝ ) ⊦ ∃ n. ∀ m. n ≤ m → ext(af(m)) = None

• Proof step 11:

  ⌜e + el0⌝ = ext !(⌜af⌝ ), ∀ ext, af. ⌜el0⌝ = ext !(⌜af⌝ ) → (∃ n. ∀ m. n ≤ m → ext(af(m)) = None) ⊦ ∃ n. ∀ m. n ≤ m → ext(af(m)) = None

Rule argument

Additional information

Used simplifier rules: List('a) freely generated by [], +;;

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  [] = ext !(⌜af⌝ ) ⊦ ∃ n. ∀ m. n ≤ m → ext(af(m)) = None

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜[]⌝ = []; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ ext !(α) = [] ↔ (∀ n. ⌜n⌝ < # α → ext(α[n]) = None)

• Proof step 7:

  ∀ n. ⌜n⌝ < # ⌜af⌝ → ext(⌜af⌝ [n]) = None ⊦ ∃ n. ∀ m. n ≤ m → ext(af(m)) = None

Rule argument

Additional information

Used terms: ext, ⌜af⌝

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

Lemma remtau-empty-equiv

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  ∀ n. ext(af(n)) = None ⊦ ∃ n. ∀ m. n ≤ m → ext(af(m)) = None

Rule argument

Additional information

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

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

User applied rule exists right

And obtained the following new goals

• Proof step 9:

  ∀ n. ext(af(n)) = None ⊦ ∀ m. 0 ≤ m → ext(af(m)) = None

Rule argument

Additional information

Used terms: 0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  ext(af(m)) ≠ None, ∀ n. ext(af(n)) = None ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 0 ≤ m; (s)

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: m

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  ⌜e '⌝ + ⌜el0⌝ = ext !(⌜af⌝ ), ∀ ext, af. ⌜el0⌝ = ext !(⌜af⌝ ) → (∃ n. ∀ m. n ≤ m → ext(af(m)) = None) ⊦ ∃ n. ∀ m. n ≤ m → ext(af(m)) = None

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ ⌜x + y⌝ = ⌜x⌝ + ⌜y⌝ ; (s) ⊦ a + x = a ' + x; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

  ⊦ ext !(α) = ⌜e '⌝ + β ↔ (∃ al, a, α0. α = ⌜al⌝ + ⌜a '⌝ + α0 ∧ ext(a) = Some(e) ∧ ext !(⌜al⌝ ) = [] ∧ ext !(α0) = β)

• Proof step 14:

  ∀ ext, af. ⌜el0⌝ = ext !(⌜af⌝ ) → (∃ n. ∀ m. n ≤ m → ext(af(m)) = None), ∃ al, a, α0. ⌜af⌝ = ⌜al⌝ + ⌜a '⌝ + α0 ∧ ext(a) = Some(e) ∧ ext !(⌜al⌝ ) = [] ∧ ext !(α0) = ⌜el0⌝ ⊦ ∃ n. ∀ m. n ≤ m → ext(af(m)) = None

Rule argument

Additional information

Used terms: e, ⌜el0⌝ , ext, ⌜af⌝

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

Lemma remtau-split-one

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  ext !(al) = [], ext !(⌜af1⌝ ) = ⌜el0⌝ , ext(a) = Some(e), ∀ ext, af. ⌜el0⌝ = ext !(⌜af⌝ ) → (∃ n. ∀ m. n ≤ m → ext(af(m)) = None) ⊦ ∃ n. ∀ m. n ≤ m → ext(((al + a ' + af1))(m)) = None

Rule argument

Additional information

Used simplifier rules: finremtau-def: ⊦ ext !(⌜al⌝ ) = ⌜ext !(al)⌝ ; append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ (⌜x⌝ + ⌜nf⌝ ).f = x + nf; (s) ⊦ finp(σ) ↔ ¬(∃ nf. ⌜nf⌝ = σ); (ss) ⊦ ⌜x⌝ + σ = ⌜nf⌝ ↔ ¬ finp(σ) ∧ x + σ.f = nf; (as) ⊦ ⌜x⌝ = [] ↔ x = []; (s)

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

User applied rule all left

And obtained the following new goals

• Proof step 16:

  ext !(⌜af1⌝ ) = ⌜el0⌝ , ext !(al) = [], ext(a) = Some(e), ⌜el0⌝ = ext !(⌜af1⌝ ) → (∃ n. ∀ m. n ≤ m → ext(af1(m)) = None) ⊦ ∃ n. ∀ m. n ≤ m → ext(((al + a ' + af1))(m)) = None

Rule argument

Additional information

Used terms: ext, af1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  ext !(al) = [], ext !(⌜af1⌝ ) = ⌜el0⌝ , ext(a) = Some(e), ∀ m. n ≤ m → ext(af1(m)) = None ⊦ ∃ n. ∀ m. n ≤ m → ext(((al + a ' + af1))(m)) = None

Rule argument

Additional information

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

User applied rule exists right

And obtained the following new goals

• Proof step 18:

  ext !(⌜af1⌝ ) = ⌜el0⌝ , ext !(al) = [], ext(a) = Some(e), ∀ m. n ≤ m → ext(af1(m)) = None ⊦ ∀ m. n + # al + 1 ≤ m → ext(((al + a ' + af1))(m)) = None

Rule argument

Additional information

Used terms: n + # al + 1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  ext !(⌜af1⌝ ) = ⌜el0⌝ , ext !(al) = [], ext(a) = Some(e), ext(((al + a ' + af1))(m)) ≠ None, n + # al < m, ∀ m. n ≤ m → ext(af1(m)) = None ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + 1 ≤ n ↔ m < n; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

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

• Proof step 21:

  ext !(al) = [], # ext !(⌜af1⌝ ) = # ⌜el0⌝ , ext(a) = Some(e), ext(((al + a ' + af1))(m)) ≠ None, n + # al < m, ∀ m. n ≤ m → ext(af1(m)) = None, ∀ n. ⌜n⌝ < # ext !(⌜af1⌝ ) → ext !(⌜af1⌝ )[n] = ⌜el0⌝ [n] ⊦

Rule argument

Additional information

Used terms: ext !(⌜af1⌝ ), ⌜el0⌝

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  ext !(al) = [], # ext !(⌜af1⌝ ) = ⌜# el0⌝ , ext(a) = Some(e), ext(((al + a ' + af1))(m)) ≠ None, n + # al < m, ∀ m. n ≤ m → ext(af1(m)) = None, ∀ n0. n0 < # el0 → ext !(⌜af1⌝ )[n0] = el0[n0] ⊦

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 23:

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

• Proof step 24:

  ext !(al) = [], # ext !(⌜af1⌝ ) = ⌜# el0⌝ , ext(a) = Some(e), ext(((al + (λ n. (n < # a ' ⊃ a '[n];af1(n - # a ')))))(m)) ≠ None, n + # al < m, ∀ n0. n0 < # el0 → ext !(⌜af1⌝ )[n0] = el0[n0], ∀ m. n ≤ m → ext(af1(m)) = None ⊦

Rule argument

Additional information

Used terms: a ', af1

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  ext !(al) = [], # ext !(⌜af1⌝ ) = ⌜# el0⌝ , ext(a) = Some(e), ext(((al + (λ n0. (n0 = 0 ⊃ a;af1(n0 - 1)))))(m)) ≠ None, n + # al < m, ∀ m. n ≤ m → ext(af1(m)) = None, ∀ n0. n0 < # el0 → ext !(⌜af1⌝ )[n0] = el0[n0] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # a ' = 0 +1; (s) ⊦ a '[0] = a; (s) ⊦ m < 1 ↔ m = 0; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 26:

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

• Proof step 27:

  ext !(al) = [], # ext !(⌜af1⌝ ) = ⌜# el0⌝ , ext(a) = Some(e), ext((λ n. (n < # al ⊃ al[n];(n - # al = 0 ⊃ a;af1(n - # al - 1))))(m)) ≠ None, n + # al < m, ∀ n0. n0 < # el0 → ext !(⌜af1⌝ )[n0] = el0[n0], ∀ m. n ≤ m → ext(af1(m)) = None ⊦

Rule argument

Additional information

Used terms: al, λ n0. (n0 = 0 ⊃ a;af1(n0 - 1))

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  ext !(al) = [], # ext !(⌜af1⌝ ) = ⌜# el0⌝ , ext(a) = Some(e), ext((m - # al = 0 ⊃ a;af1(m - # al - 1))) ≠ None, n + # al < m, ∀ n0. n0 < # el0 → ext !(⌜af1⌝ )[n0] = el0[n0], ∀ m. n ≤ m → ext(af1(m)) = None ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + m0 < n → ¬ n + n0 < m; (s) ⊦ m +1 = m + 1; (s) ⊦ # x = 0 ↔ x = []; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic trans-Nat: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 29:

  ext !(al) = [], # ext !(⌜af1⌝ ) = ⌜# el0⌝ , ext(a) = Some(e), m = n1 + # al, ext((n1 = 0 ⊃ a;af1(n1 - 1))) ≠ None, n + # al < m, # al ≤ m, ∀ m. n ≤ m → ext(af1(m)) = None, ∀ n0. n0 < # el0 → ext !(⌜af1⌝ )[n0] = el0[n0] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ n ↔ ¬ n < m; (ss) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic trans-Nat: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic ⊦ # x = 0 ↔ x = []; (s) ⊦ m +1 = m + 1; (s) ⊦ m + m0 < n → ¬ n + n0 < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: m, # al, n1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

  ext !(al) = [], # ext !(⌜af1⌝ ) = ⌜# el0⌝ , ext(a) = Some(e), ext(af1(n1 - 1)) ≠ None, n < n1, ∀ m. n ≤ m → ext(af1(m)) = None, ∀ n0. n0 < # el0 → ext !(⌜af1⌝ )[n0] = el0[n0] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic 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) ⊦ m ≤ m + n; (s)

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 31:

  ext !(al) = [], # ext !(⌜af1⌝ ) = ⌜# el0⌝ , ext(a) = Some(e), n1 = m0 + 1, ext(af1(m0)) ≠ None, n1 ≠ 0, n < n1, ∀ n0. n0 < # el0 → ext !(⌜af1⌝ )[n0] = el0[n0], ∀ m. n ≤ m → ext(af1(m)) = None ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ n < 0; (s) n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: n1, m0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

  ext !(al) = [], # ext !(⌜af1⌝ ) = ⌜# el0⌝ , ext(a) = Some(e), ext(af1(m0)) ≠ None, n ≤ m0, ∀ m. n ≤ m → ext(af1(m)) = None, ∀ n0. n0 < # el0 → ext !(⌜af1⌝ )[n0] = el0[n0] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 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 + 1 ↔ ¬ n < m; (s) ⊦ m + 1 ≠ 0; (s)

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: m0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  ⌜ef⌝ = ext !(⌜af⌝ ), ∀ m. n ≤ m → ext(af(m)) = None ⊦

Rule argument

Additional information

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

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

User applied rule induction

And obtained the following new goals

• Proof step 35:

  ⌜ef⌝ = ext !(⌜af⌝ ), ∀ m. n ≤ m → ext(af(m)) = None, ∀ n0, ef, ext, af. n0 < n → ⌜ef⌝ = ext !(⌜af⌝ ) ∧ (∀ m. n0 ≤ m → ext(af(m)) = None) → false ⊦

Rule argument

Additional information

Used simplifier rules: <; (wellfounded) Used terms: n

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 36:

  ⊦ ⌜nf⌝ = nf(0) + ⌜λ n. nf(n + 1)⌝

• Proof step 37:

  ef(0) + ⌜λ n. ef(n + 1)⌝ = ext !(⌜af⌝ ), ∀ m. n ≤ m → ext(af(m)) = None, ∀ n0, ef, ext, af. n0 < n → ⌜ef⌝ = ext !(⌜af⌝ ) ∧ (∀ m. n0 ≤ m → ext(af(m)) = None) → false ⊦

Rule argument

Additional information

Used terms: ef

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 38:

  ⌜ef(0) '⌝ + ⌜λ n. ef(n + 1)⌝ = ext !(⌜af⌝ ), ∀ m. n ≤ m → ext(af(m)) = None, ∀ n0, ef, ext, af. n0 < n → ⌜ef⌝ = ext !(⌜af⌝ ) ∧ (∀ m. n0 ≤ m → ext(af(m)) = None) → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a + σ = ⌜a '⌝ + σ; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 39:

  ⊦ ext !(α) = ⌜e '⌝ + β ↔ (∃ al, a, α0. α = ⌜al⌝ + ⌜a '⌝ + α0 ∧ ext(a) = Some(e) ∧ ext !(⌜al⌝ ) = [] ∧ ext !(α0) = β)

• Proof step 40:

  ∀ m. n ≤ m → ext(af(m)) = None, ∃ al, a, α0. ⌜af⌝ = ⌜al⌝ + ⌜a '⌝ + α0 ∧ ext(a) = Some(ef(0)) ∧ ext !(⌜al⌝ ) = [] ∧ ext !(α0) = ⌜λ n. ef(n + 1)⌝ , ∀ n0, ef, ext, af. n0 < n → ⌜ef⌝ = ext !(⌜af⌝ ) ∧ (∀ m. n0 ≤ m → ext(af(m)) = None) → false ⊦

Rule argument

Additional information

Used simplifier rules: append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream Used terms: ext, ⌜af⌝ , ef(0), ⌜λ n. ef(n + 1)⌝

Proof step 39 from proof remtau-inf (previous step) (back to tree)

Lemma remtau-split-one

Proof step 40 from proof remtau-inf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 41:

  ext !(al) = [], ext !(⌜af1⌝ ) = ⌜λ n. ef(n + 1)⌝ , ext(a) = Some(ef(0)), ∀ m. n ≤ m → ext(((al + a ' + af1))(m)) = None, ∀ n0, ef, ext, af. n0 < n → ⌜ef⌝ = ext !(⌜af⌝ ) ∧ (∀ m. n0 ≤ m → ext(af(m)) = None) → false ⊦

Rule argument

Additional information

Used simplifier rules: finremtau-def: ⊦ ext !(⌜al⌝ ) = ⌜ext !(al)⌝ ; append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ (⌜x⌝ + ⌜nf⌝ ).f = x + nf; (s) ⊦ finp(σ) ↔ ¬(∃ nf. ⌜nf⌝ = σ); (ss) ⊦ ⌜x⌝ + σ = ⌜nf⌝ ↔ ¬ finp(σ) ∧ x + σ.f = nf; (as) ⊦ ⌜x⌝ = [] ↔ x = []; (s)

Proof step 41 from proof remtau-inf (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 42:

  ext !(⌜af1⌝ ) = ⌜λ n. ef(n + 1)⌝ , ext !(al) = [], ext(a) = Some(ef(0)), n ≤ # al → ext(((al + a ' + af1))(# al)) = None, ∀ m. n ≤ m → ext(((al + a ' + af1))(m)) = None, ∀ n0, ef, ext, af. n0 < n → ⌜ef⌝ = ext !(⌜af⌝ ) ∧ (∀ m. n0 ≤ m → ext(af(m)) = None) → false ⊦

Rule argument

Additional information

Used terms: # al

Proof step 42 from proof remtau-inf (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 43:

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

• Proof step 44:

  ext !(al) = [], ext !(⌜af1⌝ ) = ⌜λ n. ef(n + 1)⌝ , ext(a) = Some(ef(0)), n ≤ # al → ext((λ n. (n < # al ⊃ al[n];((a ' + af1))(n - # al)))(# al)) = None, ∀ m. n ≤ m → ext((λ n. (n < # al ⊃ al[n];((a ' + af1))(n - # al)))(m)) = None, ∀ n0, ef, ext, af. n0 < n → ⌜ef⌝ = ext !(⌜af⌝ ) ∧ (∀ m. n0 ≤ m → ext(af(m)) = None) → false ⊦

Rule argument

Additional information

Used terms: al, a ' + af1

Proof step 43 from proof remtau-inf (previous step) (back to tree)

A spec-lemma

Proof step 44 from proof remtau-inf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 45:

  ext !(⌜af1⌝ ) = ⌜λ n. ef(n + 1)⌝ , ext !(al) = [], ext(a) = Some(ef(0)), # al < n, ∀ m. n ≤ m → ext(((a ' + af1))(m - # al)) = None, ∀ n0, ef, ext, af. n0 < n → ⌜ef⌝ = ext !(⌜af⌝ ) ∧ (∀ m. n0 ≤ m → ext(af(m)) = None) → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m < n → ¬ n < m; (s) ⊦ # x = 0 ↔ x = []; (s) trans-Nat: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ Some(a) ≠ None; (s) ⊦ ((a ' + nf))(0) = a; (s) ⊦ m - m = 0; (s) ⊦ ¬ n < n; (s)

Proof step 45 from proof remtau-inf (previous step) (back to tree)

User applied rule apply induction

And obtained the following new goals

• Proof step 46:

  ext !(al) = [], ext !(⌜af1⌝ ) = ⌜λ n. ef(n + 1)⌝ , ext(a) = Some(ef(0)), # al < n, ∀ m. n ≤ m → ext(((a ' + af1))(m - # al)) = None, ∀ n0, ef, ext, af. n0 < n → ⌜ef⌝ = ext !(⌜af⌝ ) ∧ (∀ m. n0 ≤ m → ext(af(m)) = None) → false ⊦ ⌜λ n. ef(n + 1)⌝ = ext !(⌜af1⌝ ) ∧ (∀ m. n - # al - 1 ≤ m → ext(af1(m)) = None)

Rule argument

Additional information

Used simplifier rules: n0 ≤ n ⊦ m ≤ n - n0 ↔ m + n0 ≤ n; (s) ⊦ m + 1 ≤ n ↔ m < n; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m < n → (n ≤ m ↔ false); (s) ⊦ m < n → m ≤ n; (s) n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ ¬ m + n < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: n - # al - 1, λ n. ef(n + 1), ext, af1

Proof step 46 from proof remtau-inf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 47:

  ext !(al) = [], ext !(⌜af1⌝ ) = ⌜λ n. ef(n + 1)⌝ , ext(a) = Some(ef(0)), ext(af1(m)) ≠ None, # al < n, n ≤ (m + 1) + # al, ∀ m. n ≤ m → ext(((a ' + af1))(m - # al)) = None, ∀ n0, ef, ext, af. n0 < n → ⌜ef⌝ = ext !(⌜af⌝ ) ∧ (∀ m. n0 ≤ m → ext(af(m)) = None) → false ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ ¬ m + n < m; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat n0 ≤ n ⊦ n - n0 ≤ m ↔ n ≤ m + n0; (s) ⊦ m < n → m ≤ n; (s) ⊦ m < n → (n ≤ m ↔ false); (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m + 1 ≤ n ↔ m < n; (s) n0 ≤ n ⊦ m ≤ n - n0 ↔ m + n0 ≤ n; (s)

Proof step 47 from proof remtau-inf (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 48:

  ext !(⌜af1⌝ ) = ⌜λ n. ef(n + 1)⌝ , ext !(al) = [], ext(a) = Some(ef(0)), ext(af1(m)) ≠ None, # al < n, n ≤ (m + 1) + # al, n ≤ (m + 1) + # al → ext(((a ' + af1))((m + 1) + # al - # al)) = None, ∀ n0, ef, ext, af. n0 < n → ⌜ef⌝ = ext !(⌜af⌝ ) ∧ (∀ m. n0 ≤ m → ext(af(m)) = None) → false ⊦

Rule argument

Additional information

Used terms: (m + 1) + # al

Proof step 48 from proof remtau-inf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 49:

  ext !(al) = [], ext !(⌜af1⌝ ) = ⌜λ n. ef(n + 1)⌝ , ext(a) = Some(ef(0)), ext(((a ' + af1))(m + 1)) = None, ext(af1(m)) ≠ None, # al < n, n ≤ (m + 1) + # al, ∀ n0, ef, ext, af. n0 < n → ⌜ef⌝ = ext !(⌜af⌝ ) ∧ (∀ m. n0 ≤ m → ext(af(m)) = None) → false ⊦

Rule argument

Additional information

Used simplifier rules: 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 49 from proof remtau-inf (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 50:

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

Rule argument

Additional information

Used simplifier rules: ⊦ m < 1 ↔ m = 0; (s) ⊦ a '[0] = a; (s) ⊦ # a ' = 0 +1; (s) ⊦ m + 1 ≠ 0; (s) ⊦ n ≤ m → m + n0 - n = (m - n) + n0; (s) ⊦ n + 0 = n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: a ', af1

Proof step 50 from proof remtau-inf (previous step) (back to tree)

A spec-lemma