DEV Community

Discussion on: Daily Challenge #168 - [Code golf] f (f (f b)) = f b

Collapse
 
cattheory profile image
joomy

You have a typo in the lemma statement, f is applied twice instead of three times.

Collapse
 
jose_a_alonso profile image
José A. Alonso

In Isabelle/HOL equivalent to the above but with a different notation

lemma "∀(f :: bool ⇒ bool). f (f (f b)) = f b"
  by smt
Thread Thread
 
jose_a_alonso profile image
José A. Alonso

And with another notation

lemma 
  fixes f :: "bool ⇒ bool"
  shows "f (f (f b)) = f b"
  by smt