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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  cont(f), ¬ monotone(f) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

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

• Proof step 4:

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

Rule argument

Additional information

Used terms: f

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

Lemma cont-def

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

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

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

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

• Proof step 7:

  ∀ chn. chain(chn) → (∀ x. f(λ x0. ∃ n. chn(n)(x0))(x) ↔ (∃ n. f(chn(n))(x))), ∃ iset, iset0. ¬(iset ⊆ iset0 → f(iset) ⊆ f(iset0)) ⊦

Rule argument

Additional information

Used terms: f

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  iset ⊆ iset0, ¬ f(iset) ⊆ f(iset0), ∀ chn. chain(chn) → (∀ x. f(λ x0. ∃ n. chn(n)(x0))(x) ↔ (∃ n. f(chn(n))(x))) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

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

• Proof step 10:

  iset ⊆ iset0, ∀ chn. chain(chn) → (∀ x. f(λ x0. ∃ n. chn(n)(x0))(x) ↔ (∃ n. f(chn(n))(x))), ∃ x. ¬(f(iset)(x) → f(iset0)(x)) ⊦

Rule argument

Additional information

Used terms: f(iset0), f(iset)

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  f(iset)(x), iset ⊆ iset0, ¬ f(iset0)(x), ∀ chn. chain(chn) → (∀ x. f(λ x0. ∃ n. chn(n)(x0))(x) ↔ (∃ n. f(chn(n))(x))) ⊦

Rule argument

Additional information

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

User applied rule all left

And obtained the following new goals

• Proof step 12:

  f(iset)(x), iset ⊆ iset0, ¬ f(iset0)(x), chain(λ n. (n = 0 ⊃ iset;iset0)) → (∀ x. f(λ x0. ∃ n. (n = 0 ⊃ iset;iset0)(x0))(x) ↔ (∃ n. f((n = 0 ⊃ iset;iset0))(x))) ⊦

Rule argument

Additional information

Used terms: λ n. (n = 0 ⊃ iset;iset0)

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

User applied rule case distinction

And obtained the following new goals

• Proof step 13:

  f(iset)(x), iset ⊆ iset0, ¬ chain(λ n. (n = 0 ⊃ iset;iset0)), ¬ f(iset0)(x) ⊦

• Proof step 21:

  f(iset)(x), iset ⊆ iset0, ¬ f(iset0)(x), ∀ x. f(λ x0. ∃ n. (n = 0 ⊃ iset;iset0)(x0))(x) ↔ (∃ n. f((n = 0 ⊃ iset;iset0))(x)) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

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

• Proof step 15:

  f(iset)(x), iset ⊆ iset0, ¬ f(iset0)(x), ∃ m, n. ¬((m = 0 ⊃ iset;iset0) ⊆ (n = 0 ⊃ iset;iset0) ∨ (n = 0 ⊃ iset;iset0) ⊆ (m = 0 ⊃ iset;iset0)) ⊦

Rule argument

Additional information

Used terms: λ n. (n = 0 ⊃ iset;iset0)

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

Lemma chain-def

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  f(iset)(x), iset ⊆ iset0, ¬ f(iset0)(x), ¬ (m = 0 ⊃ iset;iset0) ⊆ (n = 0 ⊃ iset;iset0), ¬ (n = 0 ⊃ iset;iset0) ⊆ (m = 0 ⊃ iset;iset0) ⊦

Rule argument

Additional information

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

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 17:

  n = 0, f(iset)(x), iset ⊆ iset0, ¬ f(iset0)(x), ¬ iset ⊆ (m = 0 ⊃ iset;iset0), ¬ (m = 0 ⊃ iset;iset0) ⊆ (n = 0 ⊃ iset;iset0) ⊦

• Proof step 19:

  n ≠ 0, f(iset)(x), iset ⊆ iset0, ¬ f(iset0)(x), ¬ iset0 ⊆ (m = 0 ⊃ iset;iset0), ¬ (m = 0 ⊃ iset;iset0) ⊆ (n = 0 ⊃ iset;iset0) ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  f(iset)(x), iset ⊆ iset0, ¬ f(iset0)(x), ¬ iset ⊆ (m = 0 ⊃ iset;iset0), ¬ (m = 0 ⊃ iset;iset0) ⊆ iset ⊦

Rule argument

Additional information

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

Heuristic if-then-else split applied rule case distinction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ iset ⊆ iset; (s)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  n ≠ 0, f(iset)(x), iset ⊆ iset0, ¬ f(iset0)(x), ¬ iset0 ⊆ (m = 0 ⊃ iset;iset0), ¬ (m = 0 ⊃ iset;iset0) ⊆ iset0 ⊦

Rule argument

Additional information

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

Heuristic if-then-else split applied rule case distinction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ iset ⊆ iset; (s)

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

User applied rule all left

And obtained the following new goals

• Proof step 22:

  f(iset)(x), iset ⊆ iset0, ¬ f(iset0)(x), f(λ x0. ∃ n. (n = 0 ⊃ iset;iset0)(x0))(x) ↔ (∃ n. f((n = 0 ⊃ iset;iset0))(x)) ⊦

Rule argument

Additional information

Used terms: x

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

User applied rule case distinction

And obtained the following new goals

• Proof step 23:

  f(iset)(x), iset ⊆ iset0, ¬ f(iset0)(x) ⊦ ∃ n. f((n = 0 ⊃ iset;iset0))(x), f(λ x0. ∃ n. (n = 0 ⊃ iset;iset0)(x0))(x)

• Proof step 24:

  f(iset)(x), iset ⊆ iset0, ¬ f(iset0)(x), ∃ n. f((n = 0 ⊃ iset;iset0))(x), f(λ x0. ∃ n. (n = 0 ⊃ iset;iset0)(x0))(x) ⊦

Rule argument

Additional information

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

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: 0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  f((n = 0 ⊃ iset;iset0))(x), f(iset)(x), iset ⊆ iset0, ¬ f(iset0)(x), f(λ x0. ∃ n. (n = 0 ⊃ iset;iset0)(x0))(x) ⊦

Rule argument

Additional information

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

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 26:

  n = 0, f(iset)(x), iset ⊆ iset0, ¬ f(iset0)(x), f(λ x0. ∃ n. (n = 0 ⊃ iset;iset0)(x0))(x) ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  f(iset)(x), iset ⊆ iset0, ¬ f(iset0)(x), f(λ x0. ∃ n. (n = 0 ⊃ iset;iset0)(x0))(x) ⊦

Rule argument

Additional information

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

User applied rule cut formula

And obtained the following new goals

• Proof step 28:

  f(iset)(x), iset ⊆ iset0, ¬ f(iset0)(x), (λ x0. ∃ n. (n = 0 ⊃ iset;iset0)(x0)) = iset0, f(λ x0. ∃ n. (n = 0 ⊃ iset;iset0)(x0))(x) ⊦

• Proof step 29:

  f(iset)(x), iset ⊆ iset0, ¬ f(iset0)(x), f(λ x0. ∃ n. (n = 0 ⊃ iset;iset0)(x0))(x) ⊦ (λ x0. ∃ n. (n = 0 ⊃ iset;iset0)(x0)) = iset0

Rule argument

Additional information

Used formulas: (λ x0. ∃ n. (n = 0 ⊃ iset;iset0)(x0)) = iset0

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

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

  f(iset)(x), iset ⊆ iset0, ¬ f(iset0)(x), f(λ x0. ∃ n. (n = 0 ⊃ iset;iset0)(x0))(x) ⊦ (∃ n. (n = 0 ⊃ iset;iset0)(x0)) ↔ iset0(x0)

Rule argument

Additional information

Proof step 30 from proof cont-monotone (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 31:

  f(iset)(x), iset ⊆ iset0, ¬ f(iset0)(x), ¬ iset0(x0), ∃ n. (n = 0 ⊃ iset;iset0)(x0), f(λ x0. ∃ n. (n = 0 ⊃ iset;iset0)(x0))(x) ⊦

• Proof step 37:

  f(iset)(x), iset0(x0), iset ⊆ iset0, ¬ f(iset0)(x), f(λ x0. ∃ n. (n = 0 ⊃ iset;iset0)(x0))(x) ⊦ ∃ n. (n = 0 ⊃ iset;iset0)(x0)

Rule argument

Additional information

Proof step 31 from proof cont-monotone (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

  (n = 0 ⊃ iset;iset0)(x0), f(iset)(x), iset ⊆ iset0, ¬ f(iset0)(x), ¬ iset0(x0), f(λ x0. ∃ n. (n = 0 ⊃ iset;iset0)(x0))(x) ⊦

Rule argument

Additional information

Proof step 32 from proof cont-monotone (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 33:

  n = 0, f(iset)(x), iset(x0), iset ⊆ iset0, ¬ f(iset0)(x), ¬ iset0(x0), f(λ x0. ∃ n. (n = 0 ⊃ iset;iset0)(x0))(x) ⊦

Rule argument

Additional information

Proof step 33 from proof cont-monotone (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  f(iset)(x), iset(x0), iset ⊆ iset0, ¬ f(iset0)(x), ¬ iset0(x0), f(λ x0. ∃ n. (n = 0 ⊃ iset;iset0)(x0))(x) ⊦

Rule argument

Additional information

Proof step 34 from proof cont-monotone (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 35:

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

• Proof step 36:

  f(iset)(x), iset(x0), ¬ f(iset0)(x), ¬ iset0(x0), ∀ x. iset(x) → iset0(x), f(λ x0. ∃ n. (n = 0 ⊃ iset;iset0)(x0))(x) ⊦

Rule argument

Additional information

Used terms: iset0, iset

Proof step 35 from proof cont-monotone (previous step) (back to tree)

A spec-lemma

Proof step 36 from proof cont-monotone (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: x0

Proof step 37 from proof cont-monotone (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: 1