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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  f(ν(f)) ≠ ν(f), monotone(f) ⊦

Rule argument

Additional information

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

User applied rule expand left

And obtained the following new goals

• Proof step 3:

  ¬(f(ν(f))(x) ↔ ν(f)(x)), monotone(f) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

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

• Proof step 5:

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

Rule argument

Additional information

Used terms: x, f

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

Lemma greatest-prefixpoint-def

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 6:

  monotone(f) ⊦ f(μ(f)) = μ(f)

• Proof step 7:

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

• Proof step 9:

  compl(f)(μ(compl(f))) = μ(compl(f)), ¬(f(ν(f))(x) ↔ ¬ μ(compl(f))(x)), monotone(f) ⊦

Rule argument

Additional information

Used terms: compl(f)

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

Lemma fixpoint

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

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

Rule argument

Additional information

Used terms: f

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

Lemma compl-monotone

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

User applied rule subst equation

And obtained the following new goals

• Proof step 10:

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

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

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

• Proof step 12:

  ¬(f(ν(f))(x) ↔ ¬ ¬ f(λ x0. ¬ μ(compl(f))(x0))(x)), monotone(f) ⊦

Rule argument

Additional information

Used terms: x, μ(compl(f)), f

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

Lemma compl-def

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  ¬(f(ν(f))(x) ↔ f(λ x0. ¬ μ(compl(f))(x0))(x)), monotone(f) ⊦

Rule argument

Additional information

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

User applied rule cut formula

And obtained the following new goals

• Proof step 14:

  ¬(f(ν(f))(x) ↔ f(λ x0. ¬ μ(compl(f))(x0))(x)), ν(f) ≠ (λ x0. ¬ μ(compl(f))(x0)), monotone(f) ⊦

Rule argument

Additional information

Used formulas: ν(f) = (λ x0. ¬ μ(compl(f))(x0))

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  ¬(f(ν(f))(x) ↔ f(λ x0. ¬ μ(compl(f))(x0))(x)), ¬(ν(f)(x0) ↔ ¬ μ(compl(f))(x0)), monotone(f) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

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

Rule argument

Additional information

Used terms: x0, f

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

Lemma greatest-prefixpoint-def