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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(¬ monotone(compl(f)) ↔ false), monotone(f) ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  monotone(f), ¬ monotone(compl(f)) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

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

• Proof step 5:

  monotone(f), ∃ iset, iset0. ¬(iset ⊆ iset0 → compl(f)(iset) ⊆ compl(f)(iset0)) ⊦

Rule argument

Additional information

Used terms: compl(f)

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

Lemma monotone-def

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  monotone(f), iset ⊆ iset0, ¬ compl(f)(iset) ⊆ compl(f)(iset0) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

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

• Proof step 8:

  iset ⊆ iset0, ¬ compl(f)(iset) ⊆ compl(f)(iset0), ∀ iset, iset0. iset ⊆ iset0 → f(iset) ⊆ f(iset0) ⊦

Rule argument

Additional information

Used terms: f

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

Lemma monotone-def

Proof step 8 from proof compl-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, ∀ iset, iset0. iset ⊆ iset0 → f(iset) ⊆ f(iset0), ∃ x. ¬(compl(f)(iset)(x) → compl(f)(iset0)(x)) ⊦

Rule argument

Additional information

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

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

Lemma subseteq-def

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  compl(f)(iset)(x), iset ⊆ iset0, ¬ compl(f)(iset0)(x), ∀ iset, iset0. iset ⊆ iset0 → f(iset) ⊆ f(iset0) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  ⊦ compl(f)(iset)(x) ↔ ¬ f(λ x0. ¬ iset(x0))(x)

• Proof step 13:

  iset ⊆ iset0, ¬ compl(f)(iset0)(x), ¬ f(λ x0. ¬ iset(x0))(x), ∀ iset, iset0. iset ⊆ iset0 → f(iset) ⊆ f(iset0) ⊦

Rule argument

Additional information

Used terms: x, iset, f

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

Lemma compl-def

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  iset ⊆ iset0, ¬ compl(f)(iset0)(x), ¬ f(λ x0. ¬ iset(x0))(x), ∀ iset, iset0. iset ⊆ iset0 → f(iset) ⊆ f(iset0) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

  ⊦ compl(f)(iset)(x) ↔ ¬ f(λ x0. ¬ iset(x0))(x)

• Proof step 16:

  f(λ x0. ¬ iset0(x0))(x), iset ⊆ iset0, ¬ f(λ x0. ¬ iset(x0))(x), ∀ iset, iset0. iset ⊆ iset0 → f(iset) ⊆ f(iset0) ⊦

Rule argument

Additional information

Used terms: x, iset0, f

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

Lemma compl-def

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  f(λ x0. ¬ iset0(x0))(x), iset ⊆ iset0, ¬ f(λ x0. ¬ iset(x0))(x), ∀ iset, iset0. iset ⊆ iset0 → f(iset) ⊆ f(iset0) ⊦

Rule argument

Additional information

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

User applied rule all left

And obtained the following new goals

• Proof step 18:

  f(λ x0. ¬ iset0(x0))(x), iset ⊆ iset0, ¬ f(λ x0. ¬ iset(x0))(x), (λ x0. ¬ iset0(x0)) ⊆ (λ x0. ¬ iset(x0)) → f(λ x0. ¬ iset0(x0)) ⊆ f(λ x0. ¬ iset(x0)) ⊦

Rule argument

Additional information

Used terms: λ x0. ¬ iset0(x0), λ x0. ¬ iset(x0)

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

User applied rule case distinction

And obtained the following new goals

• Proof step 19:

  f(λ x0. ¬ iset0(x0))(x), iset ⊆ iset0, ¬ f(λ x0. ¬ iset(x0))(x), ¬ (λ x0. ¬ iset0(x0)) ⊆ (λ x0. ¬ iset(x0)) ⊦

• Proof step 25:

  f(λ x0. ¬ iset0(x0))(x), iset ⊆ iset0, f(λ x0. ¬ iset0(x0)) ⊆ f(λ x0. ¬ iset(x0)), ¬ f(λ x0. ¬ iset(x0))(x) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

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

• Proof step 21:

  f(λ x0. ¬ iset0(x0))(x), iset ⊆ iset0, ¬ f(λ x0. ¬ iset(x0))(x), ∃ x. ¬(¬ iset0(x) → ¬ iset(x)) ⊦

Rule argument

Additional information

Used terms: λ x0. ¬ iset(x0), λ x0. ¬ iset0(x0)

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

Lemma subseteq-def

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  f(λ x0. ¬ iset0(x0))(x), iset(x0), iset ⊆ iset0, ¬ f(λ x0. ¬ iset(x0))(x), ¬ iset0(x0) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 23:

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

• Proof step 24:

  f(λ x0. ¬ iset0(x0))(x), iset(x0), ¬ f(λ x0. ¬ iset(x0))(x), ¬ iset0(x0), ∀ x. iset(x) → iset0(x) ⊦

Rule argument

Additional information

Used terms: iset0, iset

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

Lemma subseteq-def

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 26:

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

• Proof step 27:

  f(λ x0. ¬ iset0(x0))(x), iset ⊆ iset0, ¬ f(λ x0. ¬ iset(x0))(x), ∀ x. f(λ x0. ¬ iset0(x0))(x) → f(λ x0. ¬ iset(x0))(x) ⊦

Rule argument

Additional information

Used terms: f(λ x0. ¬ iset(x0)), f(λ x0. ¬ iset0(x0))

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

Lemma subseteq-def

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: x