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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  monotone(f), ¬ ((f ^ n))(λ x. false) ⊆ ((f ^ (n + 1)))(λ x. false) ⊦

Rule argument

Additional information

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

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  monotone(f), ¬ ((f ^ 0))(λ x. false) ⊆ ((f ^ (0 + 1)))(λ x. false) ⊦

• Proof step 8:

  monotone(f), ¬ ((f ^ n0 +1))(λ x. false) ⊆ ((f ^ (n0 +1 + 1)))(λ x. false), ∀ f. ¬(monotone(f) ∧ ¬ ((f ^ n0))(λ x. false) ⊆ ((f ^ (n0 + 1)))(λ x. false)) ⊦

Rule argument

Additional information

Used simplifier rules: nat freely generated by 0, +1;;

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

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

• Proof step 5:

  monotone(f), ¬ ((f ^ 0))(λ x. false) ⊆ f(((f ^ 0))(λ x. false)) ⊦

Rule argument

Additional information

Used terms: λ x. false, 0, f

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

Lemma iterate-rec

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  monotone(f), ¬ (λ x. false) ⊆ f(λ x. false) ⊦

Rule argument

Additional information

Used simplifier rules: iterate-base: ⊦ ((f ^ 0))(iset) = iset;

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ iset ⊆ iset0 ↔ (∀ x. iset(x) → iset0(x))

Rule argument

Additional information

Used terms: f(λ x. false), λ x. false

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

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

• Proof step 10:

  monotone(f), ¬ ((f ^ n0 +1))(λ x. false) ⊆ f(((f ^ n0 +1))(λ x. false)), ∀ f. ¬(monotone(f) ∧ ¬ ((f ^ n0))(λ x. false) ⊆ ((f ^ (n0 + 1)))(λ x. false)) ⊦

Rule argument

Additional information

Used terms: λ x. false, n0 +1, f

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

Lemma iterate-rec

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  monotone(f), ¬ ((f ^ (n0 + 1)))(λ x. false) ⊆ f(((f ^ (n0 + 1)))(λ x. false)), ∀ f0. ¬ monotone(f0) ∨ ((f0 ^ n0))(λ x. false) ⊆ ((f0 ^ (n0 + 1)))(λ x. false) ⊦

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

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

• Proof step 13:

  monotone(f), ¬ f(((f ^ n0))(λ x. false)) ⊆ f(f(((f ^ n0))(λ x. false))), ∀ f0. ¬ monotone(f0) ∨ ((f0 ^ n0))(λ x. false) ⊆ ((f0 ^ (n0 + 1)))(λ x. false) ⊦

Rule argument

Additional information

Used terms: λ x. false, n0, f

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

Lemma iterate-rec

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

User applied rule all left

And obtained the following new goals

• Proof step 14:

  monotone(f), ¬ f(((f ^ n0))(λ x. false)) ⊆ f(f(((f ^ n0))(λ x. false))), ¬ monotone(f) ∨ ((f ^ n0))(λ x. false) ⊆ ((f ^ (n0 + 1)))(λ x. false) ⊦

Rule argument

Additional information

Used terms: f

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  monotone(f), ((f ^ n0))(λ x. false) ⊆ ((f ^ (n0 + 1)))(λ x. false), ¬ f(((f ^ n0))(λ x. false)) ⊆ f(f(((f ^ n0))(λ x. false))) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

  ⊦ monotone(f) ↔ (∀ iset, iset0. iset ⊆ iset0 → f(iset) ⊆ f(iset0))

• Proof step 17:

  ((f ^ n0))(λ x. false) ⊆ ((f ^ (n0 + 1)))(λ x. false), ¬ f(((f ^ n0))(λ x. false)) ⊆ f(f(((f ^ n0))(λ x. false))), ∀ iset, iset0. iset ⊆ iset0 → f(iset) ⊆ f(iset0) ⊦

Rule argument

Additional information

Used terms: f

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

A spec-lemma

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

User applied rule all left

And obtained the following new goals

• Proof step 18:

  ((f ^ n0))(λ x. false) ⊆ ((f ^ (n0 + 1)))(λ x. false), ¬ f(((f ^ n0))(λ x. false)) ⊆ f(f(((f ^ n0))(λ x. false))), ((f ^ n0))(λ x. false) ⊆ f(((f ^ n0))(λ x. false)) → f(((f ^ n0))(λ x. false)) ⊆ f(f(((f ^ n0))(λ x. false))) ⊦

Rule argument

Additional information

Used terms: ((f ^ n0))(λ x. false), f(((f ^ n0))(λ x. false))

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  ((f ^ n0))(λ x. false) ⊆ ((f ^ (n0 + 1)))(λ x. false), ¬ f(((f ^ n0))(λ x. false)) ⊆ f(f(((f ^ n0))(λ x. false))), ¬ ((f ^ n0))(λ x. false) ⊆ f(((f ^ n0))(λ x. false)) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

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

Rule argument

Additional information

Used terms: λ x. false, n0, f

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

Lemma iterate-rec