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