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)(λ x. false)(x0)) ↔ f(λ x0. ∃ n. (f ^ n)(λ x. false)(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)(λ x. false)(x0)) ↔ f(λ x0. ∃ n. (f ^ n)(λ x. false)(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)(λ x. false)(x0)) ↔ f(λ x0. ∃ n. (f ^ n)(λ x. false)(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. false)) → (∀ x. f(λ x0. ∃ n. (f ^ n)(λ x. false)(x0))(x) ↔ (∃ n. f((f ^ n)(λ x. false))(x))) ⊦ (∃ n. (f ^ n)(λ x. false)(x0)) ↔ f(λ x0. ∃ n. (f ^ n)(λ x. false)(x0))(x0)

Rule argument

Additional information

Used terms: λ n. (f ^ n)(λ x. false)

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. false)) → (∀ x. f(λ x0. ∃ n. (f ^ n)(λ x. false)(x0))(x) ↔ (∃ n. f((f ^ n)(λ x. false))(x))) ⊦ (∃ n. (f ^ n)(λ x. false)(x0)) ↔ f(λ x0. ∃ n. (f ^ n)(λ x. false)(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)(λ x. false)) ⊦ (∃ n. (f ^ n)(λ x. false)(x0)) ↔ f(λ x0. ∃ n. (f ^ n)(λ x. false)(x0))(x0)

• Proof step 16:

  monotone(f), ∀ x. f(λ x0. ∃ n. (f ^ n)(λ x. false)(x0))(x) ↔ (∃ n. f((f ^ n)(λ x. false))(x)) ⊦ (∃ n. (f ^ n)(λ x. false)(x0)) ↔ f(λ x0. ∃ n. (f ^ n)(λ x. false)(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)(λ x. false) ⊆ (f ^ n)(λ x. false) ∨ (f ^ n)(λ x. false) ⊆ (f ^ m)(λ x. false)) ⊦ (∃ n. (f ^ n)(λ x. false)(x0)) ↔ f(λ x0. ∃ n. (f ^ n)(λ x. false)(x0))(x0)

Rule argument

Additional information

Used terms: λ n. (f ^ n)(λ x. false)

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)(λ x. false) ⊆ (f ^ n)(λ x. false), ¬ (f ^ n)(λ x. false) ⊆ (f ^ m)(λ x. false) ⊦ (∃ n. (f ^ n)(λ x. false)(x0)) ↔ f(λ x0. ∃ n. (f ^ n)(λ x. false)(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)(λ x. false) ⊆ (f ^ n)(λ x. false)

• Proof step 14:

  monotone(f), ¬ m ≤ n, ¬ (f ^ m)(λ x. false) ⊆ (f ^ n)(λ x. false), ¬ (f ^ n)(λ x. false) ⊆ (f ^ m)(λ x. false) ⊦ (∃ n. (f ^ n)(λ x. false)(x0)) ↔ f(λ x0. ∃ n. (f ^ n)(λ x. false)(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)(λ x. false) ⊆ (f ^ n)(λ x. false)

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m < n → ¬ n < m; (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)(λ x. false)(x0))(x0) ↔ (∃ n. f((f ^ n)(λ x. false))(x0)), ∀ x. f(λ x0. ∃ n. (f ^ n)(λ x. false)(x0))(x) ↔ (∃ n. f((f ^ n)(λ x. false))(x)) ⊦ (∃ n. (f ^ n)(λ x. false)(x0)) ↔ f(λ x0. ∃ n. (f ^ n)(λ x. false)(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)(λ x. false)(x0))(x0) ↔ (∃ n. f((f ^ n)(λ x. false))(x0)), ∀ x. f(λ x0. ∃ n. (f ^ n)(λ x. false)(x0))(x) ↔ (∃ n. f((f ^ n)(λ x. false))(x)), ∃ n. (f ^ n)(λ x. false)(x0) ⊦ f(λ x0. ∃ n. (f ^ n)(λ x. false)(x0))(x0)

• Proof step 25:

  monotone(f), f(λ x0. ∃ n. (f ^ n)(λ x. false)(x0))(x0) ↔ (∃ n. f((f ^ n)(λ x. false))(x0)), ∀ x. f(λ x0. ∃ n. (f ^ n)(λ x. false)(x0))(x) ↔ (∃ n. f((f ^ n)(λ x. false))(x)), f(λ x0. ∃ n. (f ^ n)(λ x. false)(x0))(x0) ⊦ ∃ n. (f ^ n)(λ x. false)(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)(λ x. false)(x0), monotone(f), f(λ x0. ∃ n. (f ^ n)(λ x. false)(x0))(x0) ↔ (∃ n. f((f ^ n)(λ x. false))(x0)), ∀ x. f(λ x0. ∃ n. (f ^ n)(λ x. false)(x0))(x) ↔ (∃ n. f((f ^ n)(λ x. false))(x)) ⊦ f(λ x0. ∃ n. (f ^ n)(λ x. false)(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)(λ x. false)(x0), monotone(f), ∀ x. f(λ x0. ∃ n. (f ^ n)(λ x. false)(x0))(x) ↔ (∃ n. f((f ^ n)(λ x. false))(x)) ⊦ ∃ n. f((f ^ n)(λ x. false))(x0), f(λ x0. ∃ n. (f ^ n)(λ x. false)(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)(λ x. false)(x0), monotone(f), ∀ x. f(λ x0. ∃ n. (f ^ n)(λ x. false)(x0))(x) ↔ (∃ n. f((f ^ n)(λ x. false))(x)) ⊦ ∃ n. f((f ^ n)(λ x. false))(x0), f(λ x0. ∃ n. (f ^ n)(λ x. false)(x0))(x0)

Rule argument

Additional information

Used simplifier rules: iterate-base: ⊦ (f ^ 0)(iset) = iset; 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 ^ (n0 + 1))(λ x. false)(x0), monotone(f), ∀ x. f(λ x0. ∃ n. (f ^ n)(λ x. false)(x0))(x) ↔ (∃ n. f((f ^ n)(λ x. false))(x)) ⊦ ∃ n. f((f ^ n)(λ x. false))(x0), f(λ x0. ∃ n. (f ^ n)(λ x. false)(x0))(x0)

Rule argument

Additional information

Used simplifier rules: ⊦ m.+1 = m + 1; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 23:

  ⊦ (f ^ (n + 1))(iset) = f((f ^ n)(iset))

• Proof step 24:

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

Rule argument

Additional information

Used terms: λ x. false, n0, f

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

Lemma iterate-rec

Proof step 24 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 25 from proof cont-iterate-fix (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 26:

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

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

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

Rule argument

Additional information

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

User applied rule exists right

And obtained the following new goals

• Proof step 28:

  f((f ^ n)(λ x. false))(x0), monotone(f), ¬ (f ^ (n + 1))(λ x. false)(x0), ∀ x. f(λ x0. ∃ n. (f ^ n)(λ x. false)(x0))(x) ↔ (∃ n. f((f ^ n)(λ x. false))(x)), f(λ x0. ∃ n. (f ^ n)(λ x. false)(x0))(x0) ⊦ ∃ n. (f ^ n)(λ x. false)(x0)

Rule argument

Additional information

Used terms: n + 1

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 29:

  ⊦ (f ^ (n + 1))(iset) = f((f ^ n)(iset))

Rule argument

Additional information

Used terms: λ x. false, n, f

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

Lemma iterate-rec