Proof step 1 from proof nu-is-UN (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ν(f) ≠ UN(λ iset. iset ⊆ f(iset)), monotone(f) ⊦

Rule argument

Additional information

Proof step 2 from proof nu-is-UN (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ν(f) ≠ UN(λ iset. iset ⊆ f(iset)), monotone(f) ⊦

Rule argument

Additional information

Proof step 3 from proof nu-is-UN (previous step) (back to tree)

User applied rule expand left

And obtained the following new goals

• Proof step 4:

  ¬(ν(f)(x) ↔ UN(λ iset. iset ⊆ f(iset))(x)), monotone(f) ⊦

Rule argument

Additional information

Proof step 4 from proof nu-is-UN (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

  ⊦ monotone(f) → (ν(f)(x) ↔ ¬ μ(compl(f))(x))

• Proof step 6:

  ¬(¬ μ(compl(f))(x) ↔ UN(λ iset. iset ⊆ f(iset))(x)), monotone(f) ⊦

Rule argument

Additional information

Used terms: x, f

Proof step 5 from proof nu-is-UN (previous step) (back to tree)

Lemma greatest-prefixpoint-def

Proof step 6 from proof nu-is-UN (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ UN(isetset)(x) ↔ (∃ iset. isetset(iset) ∧ iset(x))

• Proof step 8:

  monotone(f) ⊦ ¬ μ(compl(f))(x) ↔ (∃ iset. iset ⊆ f(iset) ∧ iset(x))

Rule argument

Additional information

Used terms: x, λ S. S ⊆ f(S)

Proof step 7 from proof nu-is-UN (previous step) (back to tree)

Lemma union-def

Proof step 8 from proof nu-is-UN (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ monotone(f) → (μ(f)(x) ↔ (∀ iset. f(iset) ⊆ iset → iset(x)))

• Proof step 10:

  monotone(f), ¬ monotone(compl(f)) ⊦ ¬ μ(compl(f))(x) ↔ (∃ iset. iset ⊆ f(iset) ∧ iset(x))

• Proof step 13:

  monotone(f), monotone(compl(f)) ⊦ ¬(∀ iset. compl(f)(iset) ⊆ iset → iset(x)) ↔ (∃ iset. iset ⊆ f(iset) ∧ iset(x))

Rule argument

Additional information

Used terms: x, compl(f)

Proof step 9 from proof nu-is-UN (previous step) (back to tree)

Lemma least-prefixpoint-def

Proof step 10 from proof nu-is-UN (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  monotone(f), ¬ monotone(compl(f)) ⊦ ¬ μ(compl(f))(x) ↔ (∃ iset. iset ⊆ f(iset) ∧ iset(x))

Rule argument

Additional information

Proof step 11 from proof nu-is-UN (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

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

Rule argument

Additional information

Used terms: f

Proof step 12 from proof nu-is-UN (previous step) (back to tree)

Lemma compl-monotone

Proof step 13 from proof nu-is-UN (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  monotone(compl(f)), monotone(f) ⊦ ¬(∀ iset. compl(f)(iset) ⊆ iset → iset(x)) ↔ (∃ iset. iset ⊆ f(iset) ∧ iset(x))

Rule argument

Additional information

Proof step 14 from proof nu-is-UN (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 15:

  monotone(f), monotone(compl(f)) ⊦ ∀ iset. compl(f)(iset) ⊆ iset → iset(x), ∃ iset. iset ⊆ f(iset) ∧ iset(x)

• Proof step 27:

  monotone(f), monotone(compl(f)), ∀ iset. compl(f)(iset) ⊆ iset → iset(x), ∃ iset. iset ⊆ f(iset) ∧ iset(x) ⊦

Rule argument

Additional information

Proof step 15 from proof nu-is-UN (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  monotone(compl(f)), monotone(f), compl(f)(iset) ⊆ iset, ¬ iset(x) ⊦ ∃ iset. iset ⊆ f(iset) ∧ iset(x)

Rule argument

Additional information

Proof step 16 from proof nu-is-UN (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

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

• Proof step 18:

  monotone(f), monotone(compl(f)), ¬ iset(x), ∀ x. compl(f)(iset)(x) → iset(x) ⊦ ∃ iset. iset ⊆ f(iset) ∧ iset(x)

Rule argument

Additional information

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

Proof step 17 from proof nu-is-UN (previous step) (back to tree)

Lemma subseteq-def

Proof step 18 from proof nu-is-UN (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 19:

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

Rule argument

Additional information

Used terms: λ x0. ¬ iset(x0)

Proof step 19 from proof nu-is-UN (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

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

Rule argument

Additional information

Proof step 20 from proof nu-is-UN (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

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

• Proof step 22:

  monotone(compl(f)), monotone(f), ¬ iset(x), ∀ x. compl(f)(iset)(x) → iset(x), ∃ x. ¬(¬ iset(x) → f(λ x0. ¬ iset(x0))(x)) ⊦

Rule argument

Additional information

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

Proof step 21 from proof nu-is-UN (previous step) (back to tree)

Lemma subseteq-def

Proof step 22 from proof nu-is-UN (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

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

Rule argument

Additional information

Proof step 23 from proof nu-is-UN (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 24:

  monotone(compl(f)), monotone(f), ¬ f(λ x0. ¬ iset(x0))(x0), ¬ iset(x), ¬ iset(x0), compl(f)(iset)(x0) → iset(x0) ⊦

Rule argument

Additional information

Used terms: x0

Proof step 24 from proof nu-is-UN (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  monotone(f), monotone(compl(f)), ¬ compl(f)(iset)(x0), ¬ f(λ x0. ¬ iset(x0))(x0), ¬ iset(x), ¬ iset(x0) ⊦

Rule argument

Additional information

Proof step 25 from proof nu-is-UN (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 26:

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

Rule argument

Additional information

Used terms: x0, iset, f

Proof step 26 from proof nu-is-UN (previous step) (back to tree)

Lemma compl-def

Proof step 27 from proof nu-is-UN (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

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

Rule argument

Additional information

Proof step 28 from proof nu-is-UN (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 29:

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

Rule argument

Additional information

Used terms: λ x0. ¬ iset(x0)

Proof step 29 from proof nu-is-UN (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

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

Rule argument

Additional information

Proof step 30 from proof nu-is-UN (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 31:

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

• Proof step 32:

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

Rule argument

Additional information

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

Proof step 31 from proof nu-is-UN (previous step) (back to tree)

Lemma subseteq-def

Proof step 32 from proof nu-is-UN (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

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

Rule argument

Additional information

Proof step 33 from proof nu-is-UN (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 34:

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

• Proof step 35:

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

Rule argument

Additional information

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

Proof step 34 from proof nu-is-UN (previous step) (back to tree)

Lemma compl-def

Proof step 35 from proof nu-is-UN (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 36:

  iset(x0), iset(x), monotone(compl(f)), monotone(f), iset ⊆ f(iset), ¬ f(iset)(x0) ⊦

Rule argument

Additional information

Proof step 36 from proof nu-is-UN (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 37:

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

• Proof step 38:

  iset(x), iset(x0), monotone(f), monotone(compl(f)), ¬ f(iset)(x0), ∀ x. iset(x) → f(iset)(x) ⊦

Rule argument

Additional information

Used terms: f(iset), iset

Proof step 37 from proof nu-is-UN (previous step) (back to tree)

Lemma subseteq-def

Proof step 38 from proof nu-is-UN (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: x0