Proof step 1 from proof cont-iterate-fix (conclusion) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 2:

  cont(f) ⊦ (∃ n. ((f ^ n))(∅)(x0)) ↔ f(λ x0. ∃ n. ((f ^ n))(∅)(x0))(x0)

Rule argument

Additional information

Proof step 2 from proof cont-iterate-fix (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 3:

  cont(f) ⊦ monotone(f)

• Proof step 4:

  cont(f), monotone(f) ⊦ (∃ n. ((f ^ n))(∅)(x0)) ↔ f(λ x0. ∃ n. ((f ^ n))(∅)(x0))(x0)

Rule argument

Additional information

Used terms: f

Proof step 3 from proof cont-iterate-fix (previous step) (back to tree)

Lemma cont-monotone

Proof step 4 from proof cont-iterate-fix (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

  ⊦ cont(f) ↔ (∀ chn. chain(chn) → (∀ x. f(λ x0. ∃ n. chn(n)(x0))(x) ↔ (∃ n. f(chn(n))(x))))

• Proof step 6:

  monotone(f), ∀ chn. chain(chn) → (∀ x. f(λ x0. ∃ n. chn(n)(x0))(x) ↔ (∃ n. f(chn(n))(x))) ⊦ (∃ n. ((f ^ n))(∅)(x0)) ↔ f(λ x0. ∃ n. ((f ^ n))(∅)(x0))(x0)

Rule argument

Additional information

Used terms: f

Proof step 5 from proof cont-iterate-fix (previous step) (back to tree)

Lemma cont-def

Proof step 6 from proof cont-iterate-fix (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 7:

  monotone(f), chain(λ n. ((f ^ n))(∅)) → (∀ x. f(λ x0. ∃ n. ((f ^ n))(∅)(x0))(x) ↔ (∃ n. f(((f ^ n))(∅))(x))) ⊦ (∃ n. ((f ^ n))(∅)(x0)) ↔ f(λ x0. ∃ n. ((f ^ n))(∅)(x0))(x0)

Rule argument

Additional information

Used terms: λ n. ((f ^ n))(∅)

Proof step 7 from proof cont-iterate-fix (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  monotone(f), chain(λ n. ((f ^ n))(∅)) → (∀ x. f(λ x0. ∃ n. ((f ^ n))(∅)(x0))(x) ↔ (∃ n. f(((f ^ n))(∅))(x))) ⊦ (∃ n. ((f ^ n))(∅)(x0)) ↔ f(λ x0. ∃ n. ((f ^ n))(∅)(x0))(x0)

Rule argument

Additional information

Proof step 8 from proof cont-iterate-fix (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 9:

  monotone(f), ¬ chain(λ n. ((f ^ n))(∅)) ⊦ (∃ n. ((f ^ n))(∅)(x0)) ↔ f(λ x0. ∃ n. ((f ^ n))(∅)(x0))(x0)

• Proof step 16:

  monotone(f), ∀ x. f(λ x0. ∃ n. ((f ^ n))(∅)(x0))(x) ↔ (∃ n. f(((f ^ n))(∅))(x)) ⊦ (∃ n. ((f ^ n))(∅)(x0)) ↔ f(λ x0. ∃ n. ((f ^ n))(∅)(x0))(x0)

Rule argument

Additional information

Proof step 9 from proof cont-iterate-fix (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ chain(chn) ↔ (∀ m, n. chn(m) ⊆ chn(n) ∨ chn(n) ⊆ chn(m))

• Proof step 11:

  monotone(f), ∃ m, n. ¬(((f ^ m))(∅) ⊆ ((f ^ n))(∅) ∨ ((f ^ n))(∅) ⊆ ((f ^ m))(∅)) ⊦ (∃ n. ((f ^ n))(∅)(x0)) ↔ f(λ x0. ∃ n. ((f ^ n))(∅)(x0))(x0)

Rule argument

Additional information

Used terms: λ n. ((f ^ n))(∅)

Proof step 10 from proof cont-iterate-fix (previous step) (back to tree)

Lemma chain-def

Proof step 11 from proof cont-iterate-fix (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  monotone(f), ¬ ((f ^ m))(∅) ⊆ ((f ^ n))(∅), ¬ ((f ^ n))(∅) ⊆ ((f ^ m))(∅) ⊦ (∃ n. ((f ^ n))(∅)(x0)) ↔ f(λ x0. ∃ n. ((f ^ n))(∅)(x0))(x0)

Rule argument

Additional information

Proof step 12 from proof cont-iterate-fix (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 13:

  monotone(f), m ≤ n ⊦ ((f ^ m))(∅) ⊆ ((f ^ n))(∅)

• Proof step 14:

  monotone(f), ¬ m ≤ n, ¬ ((f ^ m))(∅) ⊆ ((f ^ n))(∅), ¬ ((f ^ n))(∅) ⊆ ((f ^ m))(∅) ⊦ (∃ n. ((f ^ n))(∅)(x0)) ↔ f(λ x0. ∃ n. ((f ^ n))(∅)(x0))(x0)

Rule argument

Additional information

Used terms: f, m, n

Proof step 13 from proof cont-iterate-fix (previous step) (back to tree)

Lemma iterate-subseq-leq

Proof step 14 from proof cont-iterate-fix (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 15:

  monotone(f), m ≤ n ⊦ ((f ^ m))(∅) ⊆ ((f ^ n))(∅)

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m < n → m ≤ n; (s) Used terms: f, n, m

Proof step 15 from proof cont-iterate-fix (previous step) (back to tree)

Lemma iterate-subseq-leq

Proof step 16 from proof cont-iterate-fix (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 17:

  monotone(f), f(λ x0. ∃ n. ((f ^ n))(∅)(x0))(x0) ↔ (∃ n. f(((f ^ n))(∅))(x0)), ∀ x. f(λ x0. ∃ n. ((f ^ n))(∅)(x0))(x) ↔ (∃ n. f(((f ^ n))(∅))(x)) ⊦ (∃ n. ((f ^ n))(∅)(x0)) ↔ f(λ x0. ∃ n. ((f ^ n))(∅)(x0))(x0)

Rule argument

Additional information

Used terms: x0

Proof step 17 from proof cont-iterate-fix (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 18:

  monotone(f), f(λ x0. ∃ n. ((f ^ n))(∅)(x0))(x0) ↔ (∃ n. f(((f ^ n))(∅))(x0)), ∀ x. f(λ x0. ∃ n. ((f ^ n))(∅)(x0))(x) ↔ (∃ n. f(((f ^ n))(∅))(x)), ∃ n. ((f ^ n))(∅)(x0) ⊦ f(λ x0. ∃ n. ((f ^ n))(∅)(x0))(x0)

• Proof step 23:

  monotone(f), f(λ x0. ∃ n. ((f ^ n))(∅)(x0))(x0) ↔ (∃ n. f(((f ^ n))(∅))(x0)), ∀ x. f(λ x0. ∃ n. ((f ^ n))(∅)(x0))(x) ↔ (∃ n. f(((f ^ n))(∅))(x)), f(λ x0. ∃ n. ((f ^ n))(∅)(x0))(x0) ⊦ ∃ n. ((f ^ n))(∅)(x0)

Rule argument

Additional information

Proof step 18 from proof cont-iterate-fix (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  ((f ^ n))(∅)(x0), monotone(f), f(λ x0. ∃ n. ((f ^ n))(∅)(x0))(x0) ↔ (∃ n. f(((f ^ n))(∅))(x0)), ∀ x. f(λ x0. ∃ n. ((f ^ n))(∅)(x0))(x) ↔ (∃ n. f(((f ^ n))(∅))(x)) ⊦ f(λ x0. ∃ n. ((f ^ n))(∅)(x0))(x0)

Rule argument

Additional information

Proof step 19 from proof cont-iterate-fix (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 20:

  ((f ^ n))(∅)(x0), monotone(f), ∀ x. f(λ x0. ∃ n. ((f ^ n))(∅)(x0))(x) ↔ (∃ n. f(((f ^ n))(∅))(x)) ⊦ ∃ n. f(((f ^ n))(∅))(x0), f(λ x0. ∃ n. ((f ^ n))(∅)(x0))(x0)

Rule argument

Additional information

Proof step 20 from proof cont-iterate-fix (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 21:

  n = n0 +1, ((f ^ n))(∅)(x0), monotone(f), ∀ x. f(λ x0. ∃ n. ((f ^ n))(∅)(x0))(x) ↔ (∃ n. f(((f ^ n))(∅))(x)) ⊦ ∃ n. f(((f ^ n))(∅))(x0), f(λ x0. ∃ n. ((f ^ n))(∅)(x0))(x0)

Rule argument

Additional information

Used simplifier rules: iterate-base: ⊦ ((f ^ 0))(iset) = iset; empty-def: ⊦ ¬ ∅(x); nat freely generated by 0, +1;;

Proof step 21 from proof cont-iterate-fix (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  f(((f ^ n0))(∅))(x0), monotone(f), ∀ x. f(λ x0. ∃ n. ((f ^ n))(∅)(x0))(x) ↔ (∃ n. f(((f ^ n))(∅))(x)) ⊦ ∃ n. f(((f ^ n))(∅))(x0), f(λ x0. ∃ n. ((f ^ n))(∅)(x0))(x0)

Rule argument

Additional information

Used simplifier rules: iterate-rec: ⊦ ((f ^ (n + 1)))(iset) = f(((f ^ n))(iset)); c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m +1 = m + 1; (s)

Proof step 22 from proof cont-iterate-fix (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: n0

Proof step 23 from proof cont-iterate-fix (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 24:

  monotone(f), ∀ x. f(λ x0. ∃ n. ((f ^ n))(∅)(x0))(x) ↔ (∃ n. f(((f ^ n))(∅))(x)), ∃ n. f(((f ^ n))(∅))(x0), f(λ x0. ∃ n. ((f ^ n))(∅)(x0))(x0) ⊦ ∃ n. ((f ^ n))(∅)(x0)

Rule argument

Additional information

Proof step 24 from proof cont-iterate-fix (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  f(((f ^ n))(∅))(x0), monotone(f), ∀ x. f(λ x0. ∃ n. ((f ^ n))(∅)(x0))(x) ↔ (∃ n. f(((f ^ n))(∅))(x)), f(λ x0. ∃ n. ((f ^ n))(∅)(x0))(x0) ⊦ ∃ n. ((f ^ n))(∅)(x0)

Rule argument

Additional information

Proof step 25 from proof cont-iterate-fix (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: iterate-rec: ⊦ ((f ^ (n + 1)))(iset) = f(((f ^ n))(iset)); a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: n + 1