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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(fragω(IOAut(start, step, ext))(s ' + sf, a ' + af) ↔ step(s, a, sf(0)) ∧ fragω(IOAut(start, step, ext))(sf, af)) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ fragω(ioa)(sf, af) ↔ (∀ n. ioa.step(sf(n), af(n), sf(n +1)))

• Proof step 4:

  ⊦ (∀ n. IOAut(start, step, ext).step(((s ' + sf))(n), ((a ' + af))(n), ((s ' + sf))(n +1))) ↔ step(s, a, sf(0)) ∧ fragω(IOAut(start, step, ext))(sf, af)

Rule argument

Additional information

Used terms: IOAut(start, step, ext), s ' + sf, a ' + af

Proof step 3 from proof inffrag-rec (previous step) (back to tree)

Lemma fraginf

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

  ⊦ fragω(ioa)(sf, af) ↔ (∀ n. ioa.step(sf(n), af(n), sf(n +1)))

• Proof step 6:

  ⊦ (∀ n. IOAut(start, step, ext).step(((s ' + sf))(n), ((a ' + af))(n), ((s ' + sf))(n +1))) ↔ step(s, a, sf(0)) ∧ (∀ n. IOAut(start, step, ext).step(sf(n), af(n), sf(n +1)))

Rule argument

Additional information

Used terms: IOAut(start, step, ext), sf, af

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

Lemma fraginf

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  ⊦ (∀ n. step(((s ' + sf))(n), ((a ' + af))(n), ((s ' + sf))(n + 1))) ↔ step(s, a, sf(0)) ∧ (∀ n. step(sf(n), af(n), sf(n + 1)))

Rule argument

Additional information

Used simplifier rules: ⊦ IOAut(start, step, ext).step = step; (s) ⊦ m +1 = m + 1; (s)

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

User applied rule case distinction

And obtained the following new goals

• Proof step 8:

  ∀ n. step(((s ' + sf))(n), ((a ' + af))(n), ((s ' + sf))(n + 1)) ⊦ step(s, a, sf(0)) ∧ (∀ n. step(sf(n), af(n), sf(n + 1)))

• Proof step 18:

  step(s, a, sf(0)), ∀ n. step(sf(n), af(n), sf(n + 1)) ⊦ ∀ n. step(((s ' + sf))(n), ((a ' + af))(n), ((s ' + sf))(n + 1))

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  ∀ n. step(((s ' + sf))(n), ((a ' + af))(n), ((s ' + sf))(n + 1)) ⊦ step(s, a, sf(0)) ∧ step(sf(n), af(n), sf(n + 1))

Rule argument

Additional information

Proof step 9 from proof inffrag-rec (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)))

• Proof step 11:

  ∀ n. step((λ n. (n < # s ' ⊃ s '[n];sf(n - # s ')))(n), ((a ' + af))(n), (λ n. (n < # s ' ⊃ s '[n];sf(n - # s ')))(n + 1)) ⊦ step(s, a, sf(0)) ∧ step(sf(n), af(n), sf(n + 1))

Rule argument

Additional information

Used terms: s ', sf

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  ∀ n0. step((n0 = 0 ⊃ s;sf(n0 - 1)), ((a ' + af))(n0), sf(n0)) ⊦ step(s, a, sf(0)) ∧ step(sf(n), af(n), sf(n + 1))

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 ⊦ n + 0 = n; (s) ⊦ n ≤ m → m + n0 - n = (m - n) + n0; (s) ⊦ m + 1 ≠ 0; (s) ⊦ # a ' = 0 +1; (s) ⊦ a '[0] = a; (s) ⊦ m < 1 ↔ m = 0; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

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

• Proof step 14:

  ∀ n0. step((n0 = 0 ⊃ s;sf(n0 - 1)), (λ n. (n < # a ' ⊃ a '[n];af(n - # a ')))(n0), sf(n0)) ⊦ step(s, a, sf(0)) ∧ step(sf(n), af(n), sf(n + 1))

Rule argument

Additional information

Used terms: a ', af

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  ∀ n0. step((n0 = 0 ⊃ s;sf(n0 - 1)), (n0 = 0 ⊃ a;af(n0 - 1)), sf(n0)) ⊦ step(s, a, sf(0)) ∧ step(sf(n), af(n), sf(n + 1))

Rule argument

Additional information

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

Proof step 15 from proof inffrag-rec (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 16:

  step((0 = 0 ⊃ s;sf(0 - 1)), (0 = 0 ⊃ a;af(0 - 1)), sf(0)), ∀ n0. step((n0 = 0 ⊃ s;sf(n0 - 1)), (n0 = 0 ⊃ a;af(n0 - 1)), sf(n0)) ⊦ step(s, a, sf(0)) ∧ step(sf(n), af(n), sf(n + 1))

Rule argument

Additional information

Used terms: 0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  step(s, a, sf(0)), ¬ step(sf(n), af(n), sf(n + 1)), ∀ n0. step((n0 = 0 ⊃ s;sf(n0 - 1)), (n0 = 0 ⊃ a;af(n0 - 1)), sf(n0)) ⊦

Rule argument

Additional information

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

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ 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: n + 1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  step(s, a, sf(0)), ¬ step(((s ' + sf))(n), ((a ' + af))(n), ((s ' + sf))(n + 1)), ∀ n. step(sf(n), af(n), sf(n + 1)) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

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

• Proof step 21:

  step(s, a, sf(0)), ¬ step((λ n. (n < # s ' ⊃ s '[n];sf(n - # s ')))(n), ((a ' + af))(n), (λ n. (n < # s ' ⊃ s '[n];sf(n - # s ')))(n + 1)), ∀ n. step(sf(n), af(n), sf(n + 1)) ⊦

Rule argument

Additional information

Used terms: s ', sf

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  step(s, a, sf(0)), ¬ step((n = 0 ⊃ s;sf(n - 1)), ((a ' + af))(n), sf(n)), ∀ n. step(sf(n), af(n), sf(n + 1)) ⊦

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 ⊦ n + 0 = n; (s) ⊦ n ≤ m → m + n0 - n = (m - n) + n0; (s) ⊦ m + 1 ≠ 0; (s) ⊦ # a ' = 0 +1; (s) ⊦ a '[0] = a; (s) ⊦ m < 1 ↔ m = 0; (s)

Proof step 22 from proof inffrag-rec (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:

  step(s, a, sf(0)), ¬ step((n = 0 ⊃ s;sf(n - 1)), (λ n. (n < # a ' ⊃ a '[n];af(n - # a ')))(n), sf(n)), ∀ n. step(sf(n), af(n), sf(n + 1)) ⊦

Rule argument

Additional information

Used terms: a ', af

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  step(s, a, sf(0)), ¬ step((n = 0 ⊃ s;sf(n - 1)), (n = 0 ⊃ a;af(n - 1)), sf(n)), ∀ n. step(sf(n), af(n), sf(n + 1)) ⊦

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 inffrag-rec (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 26:

  n ≠ 0, step(s, a, sf(0)), ¬ step(sf(n - 1), (n = 0 ⊃ a;af(n - 1)), sf(n)), ∀ n. step(sf(n), af(n), sf(n + 1)) ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  n ≠ 0, step(s, a, sf(0)), ¬ step(sf(n - 1), af(n - 1), sf(n)), ∀ n. step(sf(n), af(n), sf(n + 1)) ⊦

Rule argument

Additional information

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 28:

  n = m + 1, n ≠ 0, step(s, a, sf(0)), ¬ step(sf(m), af(m), sf(n)), ∀ n. step(sf(n), af(n), sf(n + 1)) ⊦

Rule argument

Additional information

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

Proof step 28 from proof inffrag-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  step(s, a, sf(0)), ¬ step(sf(m), af(m), sf(m + 1)), ∀ n. step(sf(n), af(n), sf(n + 1)) ⊦

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 + 1 ≠ 0; (s)

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: m